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

Require Export In_NGamma.

Inductive in_gamma (gamma : flist) (work : nf_list) : form -> Set :=
  | In_Gamma :
      forall (n : nat) (a : form),
      my_nth form n gamma a -> in_gamma gamma work a
  | In_Work1 :
      forall (n : nat) (a : normal_form),
      my_nth normal_form n work a -> in_gamma gamma work (nf2form a).


Lemma in_gamma_cons_gamma_tail :
 forall (a : form) (gamma : flist) (work : nf_list) (c : form),
 in_gamma gamma work c -> in_gamma (a :: gamma) work c.
(* Goal: forall (a : normal_form) (gamma : flist) (work : nf_list) (c : form) (_ : in_gamma gamma (@cons normal_form a work) c), in_gamma (@cons form (nf2form a) gamma) work c *)
intros a gamma work c in_gamma0.
(* Goal: sumor (in_gamma gamma work c) (@eq form c (nf2form a)) *)
elim in_gamma0; clear in_gamma0 c.
(* Goal: forall (n : nat) (a0 : form) (_ : my_nth form n gamma a0), sumor (in_gamma gamma work a0) (@eq form a0 (nf2form a)) *)
(* Goal: forall (n : nat) (a0 : normal_form) (_ : my_nth normal_form n (@cons normal_form a work) a0), sumor (in_gamma gamma work (nf2form a0)) (@eq form (nf2form a0) (nf2form a)) *)
intros n c nth.
(* Goal: in_gamma (@cons form a gamma) work c *)
(* Goal: forall (n : nat) (a0 : normal_form) (_ : my_nth normal_form n work a0), in_gamma (@cons form a gamma) work (nf2form a0) *)
apply In_Gamma with (S n).
(* Goal: my_nth normal_form (S n) (@cons normal_form a work) c *)
apply My_NthS; assumption.
(* Goal: forall (n : nat) (a0 : form) (_ : my_nth form n gamma a0), sumor (in_gamma gamma work a0) (@eq form a0 (nf2form a)) *)
(* Goal: forall (n : nat) (a0 : normal_form) (_ : my_nth normal_form n (@cons normal_form a work) a0), sumor (in_gamma gamma work (nf2form a0)) (@eq form (nf2form a0) (nf2form a)) *)
intros n c nth.
(* Goal: in_gamma (@cons form a gamma) work (nf2form c) *)
apply In_Work1 with n; assumption.
Qed.


Lemma in_gamma_cons_gamma_head :
 forall (a : form) (gamma : flist) (work : nf_list),
 in_gamma (a :: gamma) work a.
(* Goal: forall (a : normal_form) (gamma : flist) (work : nf_list), in_gamma gamma (@cons normal_form a work) (nf2form a) *)
intros a gamma work.
(* Goal: in_gamma (@cons form a gamma) work a *)
apply In_Gamma with 0.
(* Goal: my_nth normal_form O (@cons normal_form a work) a *)
apply My_NthO.
Qed.

Lemma in_gamma_cons_gamma_rev :
 forall (a : form) (gamma : flist) (work : nf_list) (c : form),
 in_gamma (a :: gamma) work c -> in_gamma gamma work c + {c = a}.
(* Goal: forall (a : normal_form) (gamma : flist) (work : nf_list) (c : form) (_ : in_gamma gamma (@cons normal_form a work) c), in_gamma (@cons form (nf2form a) gamma) work c *)
intros a gamma work c in_gamma0.
(* Goal: sumor (in_gamma gamma work c) (@eq form c (nf2form a)) *)
elim in_gamma0; clear in_gamma0 c.
(* Goal: forall (n : nat) (a0 : normal_form) (_ : my_nth normal_form n (@cons normal_form a work) a0), sumor (in_gamma gamma work (nf2form a0)) (@eq form (nf2form a0) (nf2form a)) *)
intros n c; case n; clear n. 
(* Goal: forall _ : my_nth normal_form O (@cons normal_form a work) c, sumor (in_gamma gamma work (nf2form c)) (@eq form (nf2form c) (nf2form a)) *)
(* Goal: forall (n : nat) (_ : my_nth normal_form (S n) (@cons normal_form a work) c), sumor (in_gamma gamma work (nf2form c)) (@eq form (nf2form c) (nf2form a)) *)
intros nth.
(* Goal: sumor (in_gamma gamma work (nf2form c)) (@eq form (nf2form c) (nf2form a)) *)
(* Goal: forall (n : nat) (_ : my_nth normal_form (S n) (@cons normal_form a work) c), sumor (in_gamma gamma work (nf2form c)) (@eq form (nf2form c) (nf2form a)) *)
right; inversion_clear nth; trivial.
(* Goal: forall (n : nat) (_ : my_nth normal_form (S n) (@cons normal_form a work) c), sumor (in_gamma gamma work (nf2form c)) (@eq form (nf2form c) (nf2form a)) *)
intros n nth.
(* Goal: sumor (in_gamma gamma work c) (@eq form c a) *)
(* Goal: forall (n : nat) (a0 : normal_form) (_ : my_nth normal_form n work a0), sumor (in_gamma gamma work (nf2form a0)) (@eq form (nf2form a0) a) *)
left; apply In_Gamma with n.
(* Goal: my_nth normal_form n work c *)
inversion_clear nth; assumption.
(* Goal: forall (n : nat) (a0 : form) (_ : my_nth form n gamma a0), sumor (in_gamma gamma work a0) (@eq form a0 (nf2form a)) *)
(* Goal: forall (n : nat) (a0 : normal_form) (_ : my_nth normal_form n (@cons normal_form a work) a0), sumor (in_gamma gamma work (nf2form a0)) (@eq form (nf2form a0) (nf2form a)) *)
intros n c nth.
(* Goal: in_gamma (@cons form a gamma) work (nf2form c) *)
left; apply In_Work1 with n; assumption.
Qed.


Lemma in_gamma_cons_work_tail :
 forall (a : normal_form) (gamma : flist) (work : nf_list) (c : form),
 in_gamma gamma work c -> in_gamma gamma (a :: work) c.
(* Goal: forall (a : normal_form) (gamma : flist) (work : nf_list) (c : form) (_ : in_gamma gamma (@cons normal_form a work) c), in_gamma (@cons form (nf2form a) gamma) work c *)
intros a gamma work c in_gamma0.
(* Goal: sumor (in_gamma gamma work c) (@eq form c (nf2form a)) *)
elim in_gamma0; clear in_gamma0 c.
(* Goal: forall (n : nat) (a0 : form) (_ : my_nth form n gamma a0), sumor (in_gamma gamma work a0) (@eq form a0 (nf2form a)) *)
(* Goal: forall (n : nat) (a0 : normal_form) (_ : my_nth normal_form n (@cons normal_form a work) a0), sumor (in_gamma gamma work (nf2form a0)) (@eq form (nf2form a0) (nf2form a)) *)
intros n c nth.
(* Goal: in_gamma gamma (@cons normal_form a work) c *)
(* Goal: forall (n : nat) (a0 : normal_form) (_ : my_nth normal_form n work a0), in_gamma gamma (@cons normal_form a work) (nf2form a0) *)
apply In_Gamma with n; assumption.
(* Goal: forall (n : nat) (a0 : form) (_ : my_nth form n gamma a0), sumor (in_gamma gamma work a0) (@eq form a0 (nf2form a)) *)
(* Goal: forall (n : nat) (a0 : normal_form) (_ : my_nth normal_form n (@cons normal_form a work) a0), sumor (in_gamma gamma work (nf2form a0)) (@eq form (nf2form a0) (nf2form a)) *)
intros n c nth.
(* Goal: in_gamma gamma (@cons normal_form a work) (nf2form c) *)
apply In_Work1 with (S n).
(* Goal: my_nth normal_form (S n) (@cons normal_form a work) c *)
apply My_NthS; assumption.
Qed.


Lemma in_gamma_cons_work_head :
 forall (a : normal_form) (gamma : flist) (work : nf_list),
 in_gamma gamma (a :: work) (nf2form a).
(* Goal: forall (a : normal_form) (gamma : flist) (work : nf_list), in_gamma gamma (@cons normal_form a work) (nf2form a) *)
intros a gamma work.
(* Goal: in_gamma gamma (@cons normal_form a work) (nf2form a) *)
apply In_Work1 with 0.
(* Goal: my_nth normal_form O (@cons normal_form a work) a *)
apply My_NthO.
Qed.

Lemma in_gamma_cons_work_rev :
 forall (a : normal_form) (gamma : flist) (work : nf_list) (c : form),
 in_gamma gamma (a :: work) c -> in_gamma gamma work c + {c = nf2form a}.
(* Goal: forall (a : normal_form) (gamma : flist) (work : nf_list) (c : form) (_ : in_gamma gamma (@cons normal_form a work) c), in_gamma (@cons form (nf2form a) gamma) work c *)
intros a gamma work c in_gamma0.
(* Goal: sumor (in_gamma gamma work c) (@eq form c (nf2form a)) *)
elim in_gamma0; clear in_gamma0 c.
(* Goal: forall (n : nat) (a0 : form) (_ : my_nth form n gamma a0), sumor (in_gamma gamma work a0) (@eq form a0 (nf2form a)) *)
(* Goal: forall (n : nat) (a0 : normal_form) (_ : my_nth normal_form n (@cons normal_form a work) a0), sumor (in_gamma gamma work (nf2form a0)) (@eq form (nf2form a0) (nf2form a)) *)
intros n c nth.
(* Goal: in_gamma gamma (@cons normal_form a work) c *)
(* Goal: forall (n : nat) (a0 : normal_form) (_ : my_nth normal_form n work a0), in_gamma gamma (@cons normal_form a work) (nf2form a0) *)
left; apply In_Gamma with n; assumption.
(* Goal: forall (n : nat) (a0 : normal_form) (_ : my_nth normal_form n (@cons normal_form a work) a0), sumor (in_gamma gamma work (nf2form a0)) (@eq form (nf2form a0) (nf2form a)) *)
intros n c; case n; clear n. 
(* Goal: forall _ : my_nth normal_form O (@cons normal_form a work) c, sumor (in_gamma gamma work (nf2form c)) (@eq form (nf2form c) (nf2form a)) *)
(* Goal: forall (n : nat) (_ : my_nth normal_form (S n) (@cons normal_form a work) c), sumor (in_gamma gamma work (nf2form c)) (@eq form (nf2form c) (nf2form a)) *)
intros nth.
(* Goal: sumor (in_gamma gamma work (nf2form c)) (@eq form (nf2form c) (nf2form a)) *)
(* Goal: forall (n : nat) (_ : my_nth normal_form (S n) (@cons normal_form a work) c), sumor (in_gamma gamma work (nf2form c)) (@eq form (nf2form c) (nf2form a)) *)
right; inversion_clear nth; trivial.
(* Goal: forall (n : nat) (_ : my_nth normal_form (S n) (@cons normal_form a work) c), sumor (in_gamma gamma work (nf2form c)) (@eq form (nf2form c) (nf2form a)) *)
intros n nth.
(* Goal: sumor (in_gamma gamma work (nf2form c)) (@eq form (nf2form c) (nf2form a)) *)
left; apply In_Work1 with n.
(* Goal: my_nth normal_form n work c *)
inversion_clear nth; assumption.
Qed.

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


Lemma in_gamma_shift_gamma_work :
 forall (a : normal_form) (gamma : flist) (work : nf_list) (c : form),
 in_gamma (nf2form a :: gamma) work c -> in_gamma gamma (a :: work) c.
(* Goal: forall (a : normal_form) (gamma : flist) (work : nf_list) (c : form) (_ : in_gamma gamma (@cons normal_form a work) c), in_gamma (@cons form (nf2form a) gamma) work c *)
intros a gamma work c in_gamma0.
elim (in_gamma_cons_gamma_rev (nf2form a) gamma work c in_gamma0);
 clear in_gamma0.
(* Goal: forall _ : in_gamma gamma work c, in_gamma (@cons form (nf2form a) gamma) work c *)
(* Goal: forall _ : @eq form c (nf2form a), in_gamma (@cons form (nf2form a) gamma) work c *)
intros in_gamma0.
(* Goal: in_gamma gamma (@cons normal_form a work) c *)
(* Goal: forall _ : @eq form c (nf2form a), in_gamma gamma (@cons normal_form a work) c *)
apply in_gamma_cons_work_tail; assumption.
intros eq_c;  rewrite eq_c; clear eq_c c.
(* Goal: in_gamma gamma (@cons normal_form a work) (nf2form a) *)
apply in_gamma_cons_work_head.
Qed.


Lemma in_gamma_shift_work_gamma :
 forall (a : normal_form) (gamma : flist) (work : nf_list) (c : form),
 in_gamma gamma (a :: work) c -> in_gamma (nf2form a :: gamma) work c.
(* Goal: forall (a : normal_form) (gamma : flist) (work : nf_list) (c : form) (_ : in_gamma gamma (@cons normal_form a work) c), in_gamma (@cons form (nf2form a) gamma) work c *)
intros a gamma work c in_gamma0.
(* Goal: in_gamma (@cons form (nf2form a) gamma) work c *)
elim (in_gamma_cons_work_rev a gamma work c in_gamma0); clear in_gamma0.
(* Goal: forall _ : in_gamma gamma work c, in_gamma (@cons form (nf2form a) gamma) work c *)
(* Goal: forall _ : @eq form c (nf2form a), in_gamma (@cons form (nf2form a) gamma) work c *)
intros in_gamma0.
(* Goal: in_gamma (@cons form (nf2form a) gamma) work c *)
(* Goal: forall _ : @eq form c (nf2form a), in_gamma (@cons form (nf2form a) gamma) work c *)
apply in_gamma_cons_gamma_tail; assumption.
intros eq_c;  rewrite eq_c; clear eq_c c.
(* Goal: in_gamma (@cons form (nf2form a) gamma) work (nf2form a) *)
apply in_gamma_cons_gamma_head.
Qed.
