(* File: Forces_Gamma.v  (last edited on 27/10/2000) (c) Klaus Weich  *)

Require Export In_Gamma.
Require Export Forces_NGamma.


Definition forces_gamma (gamma : flist) (work : nf_list) 
  (k : kripke_tree) := forall a : form, in_gamma gamma work a -> forces_t k a.



Lemma forces_gamma_cons_gamma :
 forall (gamma : flist) (work : nf_list) (k : kripke_tree) (a : form),
 forces_t k a ->
 forces_gamma gamma work k -> forces_gamma (a :: gamma) work k.
(* Goal: forall (gamma : flist) (work : nf_list) (k : kripke_tree) (a : form) (_ : forces_t k a) (_ : forces_gamma gamma work k), forces_gamma (@cons form a gamma) work k *)
intros gamma work k a forces_a forces_gamma0.
(* Goal: forces_gamma (@cons form (nf2form a) gamma) work k *)
unfold forces_gamma in |- *.
(* Goal: forall (a : form) (_ : in_gamma gamma work a), forces_t k a *)
intros c in_gamma0.
(* Goal: forces_t k c *)
elim (in_gamma_cons_gamma_rev a gamma work c in_gamma0); clear in_gamma0.
(* Goal: forall _ : in_gamma gamma work c, forces_t k c *)
(* Goal: forall _ : @eq form c a, forces_t k c *)
intros in_gamma0.
(* Goal: forces_t k c *)
(* Goal: forall _ : @eq form c a, forces_t k c *)
apply forces_gamma0; assumption.
intros eq_c;  rewrite eq_c; assumption.
Qed.


Lemma forces_gamma_cons_gamma_tail :
 forall (gamma : flist) (work : nf_list) (k : kripke_tree) (a : form),
 forces_gamma (a :: gamma) work k -> forces_gamma gamma work k.
(* Goal: forall (gamma : flist) (work : nf_list) (k : kripke_tree) (a : form) (_ : forces_gamma (@cons form a gamma) work k), forces_t k a *)
intros gamma work k a forces_gamma0.
(* Goal: forces_gamma (@cons form (nf2form a) gamma) work k *)
unfold forces_gamma in |- *.
(* Goal: forall (a : form) (_ : in_gamma gamma work a), forces_t k a *)
intros c in_gamma0.
(* Goal: forces_t k c *)
apply forces_gamma0.
(* Goal: in_gamma (@cons form a gamma) work c *)
apply in_gamma_cons_gamma_tail; assumption.
Qed.


Lemma forces_gamma_cons_gamma_head :
 forall (gamma : flist) (work : nf_list) (k : kripke_tree) (a : form),
 forces_gamma (a :: gamma) work k -> forces_t k a.
(* Goal: forall (gamma : flist) (work : nf_list) (k : kripke_tree) (a : form) (_ : forces_gamma (@cons form a gamma) work k), forces_t k a *)
intros gamma work k a forces_gamma0.
(* Goal: forces_t k c *)
apply forces_gamma0.
(* Goal: in_gamma (@cons form a gamma) work a *)
apply in_gamma_cons_gamma_head; assumption.
Qed.

(*********************************************************************)

Lemma forces_gamma_shift_gamma_work :
 forall (a : normal_form) (gamma : flist) (work : nf_list) (k : kripke_tree),
 forces_gamma (nf2form a :: gamma) work k -> forces_gamma gamma (a :: work) k.
(* Goal: forall (a : normal_form) (gamma : flist) (work : nf_list) (k : kripke_tree) (_ : forces_gamma gamma (@cons normal_form a work) k), forces_gamma (@cons form (nf2form a) gamma) work k *)
intros a gamma work k forces_gamma0.
(* Goal: forces_gamma (@cons form (nf2form a) gamma) work k *)
unfold forces_gamma in |- *.
(* Goal: forall (a0 : form) (_ : in_gamma (@cons form (nf2form a) gamma) work a0), forces_t k a0 *)
intros c in_gamma.
(* Goal: forces_t k c *)
apply forces_gamma0.
(* Goal: In_Gamma.in_gamma (@cons form (nf2form a) gamma) work c *)
apply in_gamma_shift_work_gamma; assumption.
Qed.

Lemma forces_gamma_shift_work_gamma :
 forall (a : normal_form) (gamma : flist) (work : nf_list) (k : kripke_tree),
 forces_gamma gamma (a :: work) k -> forces_gamma (nf2form a :: gamma) work k.
(* Goal: forall (a : normal_form) (gamma : flist) (work : nf_list) (k : kripke_tree) (_ : forces_gamma gamma (@cons normal_form a work) k), forces_gamma (@cons form (nf2form a) gamma) work k *)
intros a gamma work k forces_gamma0.
(* Goal: forces_gamma (@cons form (nf2form a) gamma) work k *)
unfold forces_gamma in |- *.
(* Goal: forall (a0 : form) (_ : in_gamma (@cons form (nf2form a) gamma) work a0), forces_t k a0 *)
intros c in_gamma.
(* Goal: forces_t k c *)
apply forces_gamma0.
(* Goal: In_Gamma.in_gamma gamma (@cons normal_form a work) c *)
apply in_gamma_shift_gamma_work; assumption.
Qed.

(*********************************************************************)

Lemma forces_gamma_cons_gamma_weak :
 forall (gamma : flist) (work : nf_list) (k : kripke_tree) (a b : form),
 (forces_t k a -> forces_t k b) ->
 forces_gamma (a :: gamma) work k -> forces_gamma (b :: gamma) work k.
(* Goal: forall (gamma : flist) (work : nf_list) (k : kripke_tree) (a b : form) (_ : forall _ : forces_t k a, forces_t k b) (_ : forces_gamma (@cons form a gamma) work k), forces_gamma (@cons form b gamma) work k *)
intros gamma work k a b forces_ab forces_gamma0.
(* Goal: forces_gamma (@cons form c gamma) work k *)
apply forces_gamma_cons_gamma.
(* Goal: forces_t k b *)
(* Goal: forces_gamma gamma work k *)
apply forces_ab.
(* Goal: forces_t k a *)
(* Goal: forces_gamma gamma work k *)
apply forces_gamma_cons_gamma_head with gamma work; assumption.
(* Goal: forces_gamma (@cons form b gamma) work k *)
apply forces_gamma_cons_gamma_tail with a; assumption.
Qed.


Lemma forces_gamma_cons_gamma_weak2 :
 forall (gamma : flist) (work : nf_list) (k : kripke_tree) (a b c : form),
 (forces_t k a -> forces_t k b -> forces_t k c) ->
 forces_gamma (a :: b :: gamma) work k -> forces_gamma (c :: gamma) work k.
(* Goal: forall (gamma : flist) (work : nf_list) (k : kripke_tree) (a b c : form) (_ : forall (_ : forces_t k a) (_ : forces_t k b), forces_t k c) (_ : forces_gamma (@cons form a (@cons form b gamma)) work k), forces_gamma (@cons form c gamma) work k *)
intros gamma work k a b c forces_abc forces_gamma0.
(* Goal: forces_gamma (@cons form c gamma) work k *)
apply forces_gamma_cons_gamma.
(* Goal: forces_t k c *)
(* Goal: forces_gamma gamma work k *)
apply forces_abc.
(* Goal: forces_t k a *)
(* Goal: forces_t k b *)
(* Goal: forces_gamma gamma work k *)
apply forces_gamma_cons_gamma_head with (b :: gamma) work; assumption.
(* Goal: forces_t k b *)
(* Goal: forces_gamma gamma work k *)
apply forces_gamma_cons_gamma_head with gamma work.
(* Goal: forces_gamma (@cons form b gamma) work k *)
apply forces_gamma_cons_gamma_tail with a; assumption.
(* Goal: forces_gamma gamma work k *)
apply forces_gamma_cons_gamma_tail with b.
(* Goal: forces_gamma (@cons form b gamma) work k *)
apply forces_gamma_cons_gamma_tail with a; assumption.
Qed.
