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

Require Export NSound.
Require Export In_Gamma.

Definition sound (Gamma : flist) (work : nf_list) (context : flist) :=
  forall a : form, in_gamma Gamma work a -> Derivable context a.


Lemma sound_cons_gamma :
 forall (gamma : flist) (work : nf_list) (context : flist) (a : form),
 Derivable context a ->
 sound gamma work context -> sound (a :: gamma) work context.
(* Goal: forall (gamma : flist) (work : nf_list) (context : flist) (a : form) (_ : Derivable context a) (_ : sound gamma work context), sound (@cons form a gamma) work context *)
intros gamma work context a der_a sound0.
(* Goal: sound gamma work (@cons form a context) *)
unfold sound in |- *.
(* Goal: forall (a0 : form) (_ : in_gamma gamma work a0), Derivable (@cons form a context) a0 *)
intros c in_gamma0.
(* Goal: Derivable context c *)
elim (in_gamma_cons_gamma_rev a gamma work c in_gamma0); clear in_gamma0.
(* Goal: forall _ : in_gamma gamma work c, Derivable context c *)
(* Goal: forall _ : @eq form c a, Derivable context c *)
intros in_gamma0.
(* Goal: Derivable context c *)
(* Goal: forall _ : @eq form c a, Derivable context c *)
apply sound0; assumption.
(* Goal: Derivable context c *)
(* Goal: sound gamma work context *)
(* Goal: Derivable context a *)
intros eq_c;  rewrite eq_c; assumption.
Qed.

Lemma sound_cons_gamma_tail :
 forall (gamma : flist) (work : nf_list) (context : flist) (a : form),
 sound (a :: gamma) work context -> sound gamma work context.
(* Goal: forall (gamma : flist) (work : nf_list) (context : flist) (a : form) (_ : sound gamma work context), sound (@cons form a gamma) work (@cons form a context) *)
intros gamma work context a sound0.
(* Goal: sound gamma work (@cons form a context) *)
unfold sound in |- *.
(* Goal: forall (a0 : form) (_ : in_gamma gamma work a0), Derivable (@cons form a context) a0 *)
intros c in_gamma0.
(* Goal: Derivable context c *)
apply sound0.
(* Goal: in_gamma (@cons form a gamma) work c *)
apply in_gamma_cons_gamma_tail; assumption.
Qed.


Lemma sound_cons_gamma_head :
 forall (gamma : flist) (work : nf_list) (context : flist) (a : form),
 sound (a :: gamma) work context -> Derivable context a.
(* Goal: forall (gamma : flist) (work : nf_list) (context : flist) (a : form) (_ : sound gamma work context), sound (@cons form a gamma) work (@cons form a context) *)
intros gamma work context a sound0.
(* Goal: Derivable context c *)
apply sound0.
(* Goal: in_gamma (@cons form a gamma) work a *)
apply in_gamma_cons_gamma_head; assumption.
Qed.

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

Lemma sound_shift_gamma_work :
 forall (a : normal_form) (gamma : flist) (work : nf_list) (context : flist),
 sound (nf2form a :: gamma) work context -> sound gamma (a :: work) context.
(* Goal: forall (a : normal_form) (gamma : flist) (work : nf_list) (context : flist) (_ : sound gamma (@cons normal_form a work) context), sound (@cons form (nf2form a) gamma) work context *)
intros a gamma work context sound0.
(* Goal: sound gamma work (@cons form a context) *)
unfold sound in |- *.
(* Goal: forall (a0 : form) (_ : in_gamma (@cons form (nf2form a) gamma) work a0), Derivable context a0 *)
intros c in_gamma.
(* Goal: Derivable context c *)
apply sound0.
(* Goal: In_Gamma.in_gamma (@cons form (nf2form a) gamma) work c *)
apply in_gamma_shift_work_gamma; assumption.
Qed.


Lemma sound_shift_work_gamma :
 forall (a : normal_form) (gamma : flist) (work : nf_list) (context : flist),
 sound gamma (a :: work) context -> sound (nf2form a :: gamma) work context.
(* Goal: forall (a : normal_form) (gamma : flist) (work : nf_list) (context : flist) (_ : sound gamma (@cons normal_form a work) context), sound (@cons form (nf2form a) gamma) work context *)
intros a gamma work context sound0.
(* Goal: sound gamma work (@cons form a context) *)
unfold sound in |- *.
(* Goal: forall (a0 : form) (_ : in_gamma (@cons form (nf2form a) gamma) work a0), Derivable context a0 *)
intros c in_gamma.
(* Goal: Derivable context c *)
apply sound0.
(* Goal: In_Gamma.in_gamma gamma (@cons normal_form a work) c *)
apply in_gamma_shift_gamma_work; assumption.
Qed.


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

Lemma sound_cons_gamma_cons_context :
 forall (gamma : flist) (work : nf_list) (context : flist) (a : form),
 sound gamma work context -> sound (a :: gamma) work (a :: context).
(* Goal: forall (gamma : flist) (work : nf_list) (context : flist) (a : form) (_ : sound gamma work context), sound (@cons form a gamma) work (@cons form a context) *)
intros gamma work context a sound0.
(* Goal: sound (@cons form c gamma) work context *)
(* Goal: Derivable context a *)
apply sound_cons_gamma.
(* Goal: Derivable (@cons form a context) a *)
(* Goal: sound gamma work (@cons form a context) *)
apply Derivable_Intro with (Var 0).
(* Goal: derives (@cons form a context) (Var O) a *)
(* Goal: sound gamma work (@cons form a context) *)
apply ByAssumption.
(* Goal: my_nth form O (@cons form a context) a *)
(* Goal: sound gamma work (@cons form a context) *)
apply My_NthO.
(* Goal: sound gamma work (@cons form a context) *)
unfold sound in |- *.
(* Goal: forall (a0 : form) (_ : in_gamma gamma work a0), Derivable (@cons form a context) a0 *)
intros c in_gamma0.
(* Goal: Derivable (@cons form a context) c *)
elim (sound0 c in_gamma0).
(* Goal: forall (t : proof_term) (_ : derives context t c), Derivable (@cons form a context) c *)
intros t der_t.
(* Goal: Derivable (@cons form a context) c *)
apply Derivable_Intro with (Shift t).
(* Goal: derives (@cons form a context) (Shift t) c *)
apply ShiftIntro; assumption.
Qed.


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

Lemma sound_cons_gamma_weak :
 forall (gamma : flist) (work : nf_list) (context : flist) (a b : form),
 (Derivable context a -> Derivable context b) ->
 sound (a :: gamma) work context -> sound (b :: gamma) work context.
(* Goal: forall (gamma : flist) (work : nf_list) (context : flist) (a b : form) (_ : forall _ : Derivable context a, Derivable context b) (_ : sound (@cons form a gamma) work context), sound (@cons form b gamma) work context *)
intros gamma work context a b der_ab sound0.
(* Goal: sound (@cons form c gamma) work context *)
(* Goal: Derivable context a *)
apply sound_cons_gamma.
(* Goal: Derivable context b *)
(* Goal: sound gamma work context *)
apply der_ab.
(* Goal: Derivable context a *)
apply sound_cons_gamma_head with gamma work; assumption.
(* Goal: sound gamma work context *)
(* Goal: Derivable context a *)
apply sound_cons_gamma_tail with a; assumption.
Qed.


Lemma sound_cons_gamma_weak2 :
 forall (gamma : flist) (work : nf_list) (context : flist) (a b c : form),
 (Derivable context a -> Derivable2 context b c) ->
 sound (a :: gamma) work context -> sound (b :: c :: gamma) work context.
(* Goal: forall (gamma : flist) (work : nf_list) (context : flist) (a b c : form) (_ : forall _ : Derivable context a, Derivable2 context b c) (_ : sound (@cons form a gamma) work context), sound (@cons form b (@cons form c gamma)) work context *)
intros gamma work context a b c der_abc sound0.
(* Goal: sound (@cons form b (@cons form c gamma)) work context *)
elim der_abc; clear der_abc.
(* Goal: forall (_ : Derivable context b) (_ : Derivable context c), sound (@cons form b (@cons form c gamma)) work context *)
(* Goal: Derivable context a *)
intros der_b der_c.
(* Goal: sound (@cons form c gamma) work context *)
(* Goal: Derivable context a *)
apply sound_cons_gamma.
(* Goal: Derivable context c *)
(* Goal: sound gamma work context *)
(* Goal: Derivable context a *)
assumption.
(* Goal: sound (@cons form c gamma) work context *)
(* Goal: Derivable context a *)
apply sound_cons_gamma.
(* Goal: Derivable context c *)
(* Goal: sound gamma work context *)
(* Goal: Derivable context a *)
assumption.
(* Goal: sound gamma work context *)
(* Goal: Derivable context a *)
apply sound_cons_gamma_tail with a; assumption.
(* Goal: Derivable context a *)
apply sound_cons_gamma_head with gamma work; assumption.
Qed.

