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

Require Export Forces_Gamma.
Require Export Derivable_Tools.

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


Lemma minimal_derivable_forces :
 forall (gamma : flist) (work : nf_list) (context : flist) (k : kripke_tree),
 Is_Monotone_kripke_tree k ->
 forces_gamma gamma work k ->
 minimal gamma work context ->
 forall a : form, Derivable context a -> forces_t k a.
(* Goal: forall (gamma : flist) (work : nf_list) (context : flist) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (_ : forces_gamma gamma work k) (_ : minimal gamma work context) (a : form) (_ : Derivable context a), forces_t k a *)
intros gamma work context k k_is_mon k_forces_gamma minimal0 a der_a.
(* Goal: forces_t k a *)
elim der_a; clear der_a.
(* Goal: forall (t : proof_term) (_ : derives context t a), forces_t k a *)
intros t der_t.
(* Goal: forces_t k a *)
apply soundness_t with t context; try assumption.
(* Goal: forall (c : form) (_ : @In form c context), forces_t k c *)
intros c in_c.
(* Goal: forces_t k c *)
apply minimal0; assumption.
Qed.


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

Lemma minimal_shift_gamma_work :
 forall (a : normal_form) (gamma : flist) (work : nf_list) (context : flist),
 minimal (nf2form a :: gamma) work context ->
 minimal gamma (a :: work) context.
(* Goal: forall (a : normal_form) (gamma : flist) (work : nf_list) (context : flist) (_ : minimal gamma (@cons normal_form a work) context), minimal (@cons form (nf2form a) gamma) work context *)
intros a gamma work context minimal0.
(* Goal: minimal (@cons form b (@cons form c gamma)) work context *)
unfold minimal in |- *.
(* Goal: forall (a0 : form) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (_ : forces_gamma (@cons form a gamma) work k) (_ : @In form a0 (@cons form a context)), forces_t k a0 *)
intros b k k_is_mon k_forces_gamma in_b.
(* Goal: forces_t k d *)
apply minimal0; try assumption.
(* Goal: forces_gamma (@cons form (nf2form a) gamma) work k *)
apply forces_gamma_shift_work_gamma; assumption.
Qed.


Lemma minimal_shift_work_gamma :
 forall (a : normal_form) (gamma : flist) (work : nf_list) (context : flist),
 minimal gamma (a :: work) context ->
 minimal (nf2form a :: gamma) work context.
(* Goal: forall (a : normal_form) (gamma : flist) (work : nf_list) (context : flist) (_ : minimal gamma (@cons normal_form a work) context), minimal (@cons form (nf2form a) gamma) work context *)
intros a gamma work context minimal0.
(* Goal: minimal (@cons form b (@cons form c gamma)) work context *)
unfold minimal in |- *.
(* Goal: forall (a0 : form) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (_ : forces_gamma (@cons form a gamma) work k) (_ : @In form a0 (@cons form a context)), forces_t k a0 *)
intros b k k_is_mon k_forces_gamma in_b.
(* Goal: forces_t k d *)
apply minimal0; try assumption.
(* Goal: forces_gamma gamma (@cons normal_form a work) k *)
apply forces_gamma_shift_gamma_work; assumption.
Qed.

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

Lemma minimal_cons_gamma_cons_context :
 forall (gamma : flist) (work : nf_list) (context : flist) (a : form),
 minimal gamma work context -> minimal (a :: gamma) work (a :: context).
(* Goal: forall (gamma : flist) (work : nf_list) (context : flist) (a : form) (_ : minimal gamma work context), minimal (@cons form a gamma) work (@cons form a context) *)
intros gamma work context a minimal0.
(* Goal: minimal (@cons form b (@cons form c gamma)) work context *)
unfold minimal in |- *.
(* Goal: forall (a0 : form) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (_ : forces_gamma (@cons form a gamma) work k) (_ : @In form a0 (@cons form a context)), forces_t k a0 *)
intros b k k_is_mon k_forces_gamma in_b.
(* Goal: forces_t k b *)
inversion_clear in_b.
(* Goal: forces_t k b *)
(* Goal: forces_t k b *)
apply k_forces_gamma.
(* Goal: in_gamma (@cons form a gamma) work b *)
(* Goal: forces_t k b *)
 rewrite H.
(* Goal: in_gamma (@cons form b gamma) work b *)
(* Goal: forces_t k b *)
apply in_gamma_cons_gamma_head.
(* Goal: forces_t k b *)
apply minimal0.
(* Goal: @In form b context *)
assumption.
(* Goal: @In form b context *)
apply forces_gamma_cons_gamma_tail with a; assumption.
(* Goal: @In form b context *)
assumption.
Qed.

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

Lemma minimal_cons_gamma_weak :
 forall (gamma : flist) (work : nf_list) (context : flist) (a b : form),
 (forall k : kripke_tree,
  Is_Monotone_kripke_tree k -> forces_t k b -> forces_t k a) ->
 minimal (a :: gamma) work context -> minimal (b :: gamma) work context.
(* Goal: forall (gamma : flist) (work : nf_list) (context : flist) (a b : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (_ : forces_t k b), forces_t k a) (_ : minimal (@cons form a gamma) work context), minimal (@cons form b gamma) work context *)
intros gamma work context a b forces_ba minimal0.
(* Goal: minimal (@cons form b (@cons form c gamma)) work context *)
unfold minimal in |- *.
(* Goal: forall (a : form) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (_ : forces_gamma (@cons form b gamma) work k) (_ : @In form a context), forces_t k a *)
intros c k k_is_mon k_forces_gamma in_c.
(* Goal: forces_t k d *)
apply minimal0; try assumption.
(* Goal: @In form b context *)
apply forces_gamma_cons_gamma_weak with b; try assumption.
(* Goal: @In form b context *)
intros; apply forces_ba; assumption.
Qed.



Lemma minimal_cons_gamma_weak2 :
 forall (gamma : flist) (work : nf_list) (context : flist) (a b c : form),
 (forall k : kripke_tree,
  Is_Monotone_kripke_tree k -> forces_t k b -> forces_t k c -> forces_t k a) ->
 minimal (a :: gamma) work context -> minimal (b :: c :: gamma) work context.
(* Goal: forall (gamma : flist) (work : nf_list) (context : flist) (a b c : form) (_ : forall (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (_ : forces_t k b) (_ : forces_t k c), forces_t k a) (_ : minimal (@cons form a gamma) work context), minimal (@cons form b (@cons form c gamma)) work context *)
intros gamma work context a b c forces_bca minimal0.
(* Goal: minimal (@cons form b (@cons form c gamma)) work context *)
unfold minimal in |- *.
(* Goal: forall (a : form) (k : kripke_tree) (_ : Is_Monotone_kripke_tree k) (_ : forces_gamma (@cons form b (@cons form c gamma)) work k) (_ : @In form a context), forces_t k a *)
intros d k k_is_mon k_forces_gamma in_d.
(* Goal: forces_t k d *)
apply minimal0; try assumption.
(* Goal: @In form b context *)
apply forces_gamma_cons_gamma_weak2 with b c; try assumption.
(* Goal: @In form b context *)
intros; apply forces_bca; assumption.
Qed.


