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

Require Export In_NGamma.


(*******************************************************************)
(* Decorated nested implications are pairs of a nested implication *)
(* and a counter-model of the premisses.                           *)

Definition decorated_nested_imp := (nimp * kripke_tree)%type.
Definition decorated_nested_imps := list decorated_nested_imp.
Definition DNI_NIL := nil (A:=decorated_nested_imp).

Definition decorated_nested_imp2nimp (x : decorated_nested_imp) :=
  match x with
  | (x0, _) => x0
  end.

Definition decorated_nested_imp2k (x : decorated_nested_imp) :=
  match x with
  | (_, k) => k
  end.

Definition decorated_nested_imp2form (x : decorated_nested_imp) :=
  nimp2form (decorated_nested_imp2nimp x).



Fixpoint rev_app (ds : decorated_nested_imps) :
 nested_imps -> nested_imps :=
  match ds with
  | nil => fun ni : nested_imps => ni
  | (x, k) :: ds => fun ni : nested_imps => rev_app ds (Decorated x k :: ni)
  end.





Lemma rev_app_app :
 forall (dni : decorated_nested_imps) (ni : nested_imps),
 rev_app dni ni = rev_app dni NNil ++ ni.
(* Goal: forall (dni : decorated_nested_imps) (ni : nested_imps), rev_app_spec dni ni *)
intros dni; elim dni; clear dni.
(* Goal: forall ni : nested_imps, @eq nested_imps (rev_app (@nil decorated_nested_imp) ni) (@app nested_imp (rev_app (@nil decorated_nested_imp) NNil) ni) *)
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall ni : nested_imps, @eq nested_imps (rev_app l ni) (@app nested_imp (rev_app l NNil) ni)) (ni : nested_imps), @eq nested_imps (rev_app (@cons decorated_nested_imp a l) ni) (@app nested_imp (rev_app (@cons decorated_nested_imp a l) NNil) ni) *)
intros ni; simpl in |- *.
(* Goal: @eq nested_imps ni ni *)
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall ni : nested_imps, @eq nested_imps (rev_app l ni) (@app nested_imp (rev_app l NNil) ni)) (ni : nested_imps), @eq nested_imps (rev_app (@cons decorated_nested_imp a l) ni) (@app nested_imp (rev_app (@cons decorated_nested_imp a l) NNil) ni) *)
trivial.
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall ni : nested_imps, @eq nested_imps (rev_app l ni) (@app nested_imp (rev_app l NNil) ni)) (ni : nested_imps), @eq nested_imps (rev_app (@cons decorated_nested_imp a l) ni) (@app nested_imp (rev_app (@cons decorated_nested_imp a l) NNil) ni) *)
intros a; case a; clear a.
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list decorated_nested_imp) (_ : forall ni : nested_imps, @eq nested_imps (rev_app l ni) (@app nested_imp (rev_app l NNil) ni)) (ni : nested_imps), @eq nested_imps (rev_app (@cons decorated_nested_imp (@pair nimp kripke_tree n k) l) ni) (@app nested_imp (rev_app (@cons decorated_nested_imp (@pair nimp kripke_tree n k) l) NNil) ni) *)
intros x k dni ih ni.
(* Goal: @eq nested_imps (rev_app (@cons decorated_nested_imp (@pair nimp kripke_tree x k) dni) ni) (@app nested_imp (rev_app (@cons decorated_nested_imp (@pair nimp kripke_tree x k) dni) NNil) ni) *)
simpl in |- *.
(* Goal: @eq nested_imps (rev_app dni (@cons nested_imp (Decorated x k) ni)) (@app nested_imp (rev_app dni (@cons nested_imp (Decorated x k) NNil)) ni) *)
 rewrite (ih (Decorated x k :: ni)).
(* Goal: @eq nested_imps (@app nested_imp (rev_app dni NNil) (@cons nested_imp (Decorated x k) ni)) (@app nested_imp (rev_app dni (@cons nested_imp (Decorated x k) NNil)) ni) *)
 rewrite (ih (Decorated x k :: NNil)).
symmetry  in |- *.
(* Goal: @eq nested_imps (@app nested_imp (@app nested_imp (rev_app dni NNil) (@cons nested_imp (Decorated x k) NNil)) ni) (@app nested_imp (rev_app dni NNil) (@cons nested_imp (Decorated x k) ni)) *)
apply (app_ass (rev_app dni NNil) (Decorated x k :: NNil) ni).
Qed.


Lemma in_app_or_ni :
 forall (x : nested_imp) (ni1 ni2 : nested_imps),
 In x (ni1 ++ ni2) -> In x ni1 \/ In x ni2.
(* Goal: forall (x : nested_imp) (ni1 ni2 : nested_imps) (_ : @In nested_imp x ni2), @In nested_imp x (@app nested_imp ni1 ni2) *)
intros x ni1 ni2 in_x.
(* Goal: or (@In nested_imp x ni1) (@In nested_imp x ni2) *)
apply in_app_or.
(* Goal: forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app dni (@cons nested_imp (Decorated n k) ni))), A *)
assumption.
Qed.

Lemma in_ni0_in_nini :
 forall (x : nested_imp) (ni1 ni2 : nested_imps),
 In x ni1 -> In x (ni1 ++ ni2).
(* Goal: forall (x : nested_imp) (ni1 ni2 : nested_imps) (_ : @In nested_imp x ni2), @In nested_imp x (@app nested_imp ni1 ni2) *)
intros x ni1 ni2 in_x.
(* Goal: @In nested_imp x (@app nested_imp ni1 ni2) *)
apply in_or_app.
(* Goal: forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app dni (@cons nested_imp (Decorated n k) ni))), A *)
left; assumption.
Qed.

Lemma in_ni1_in_nini :
 forall (x : nested_imp) (ni1 ni2 : nested_imps),
 In x ni2 -> In x (ni1 ++ ni2).
(* Goal: forall (x : nested_imp) (ni1 ni2 : nested_imps) (_ : @In nested_imp x ni2), @In nested_imp x (@app nested_imp ni1 ni2) *)
intros x ni1 ni2 in_x.
(* Goal: @In nested_imp x (@app nested_imp ni1 ni2) *)
apply in_or_app.
(* Goal: forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app dni (@cons nested_imp (Decorated n k) ni))), A *)
right; assumption.
Qed.


Lemma in_ni_x_ni_rev :
 forall (x x' : nested_imp) (ni1 ni2 : nested_imps),
 In x (ni1 ++ x' :: ni2) -> In x (ni1 ++ ni2) \/ x = x'.
(* Goal: forall (x x' : nested_imp) (ni1 ni2 : nested_imps) (_ : @In nested_imp x (@app nested_imp ni1 (@cons nested_imp x' ni2))), or (@In nested_imp x (@app nested_imp ni1 ni2)) (@eq nested_imp x x') *)
intros x x' ni1 ni2 in_ni_x_ni.
(* Goal: or (@In nested_imp x (@app nested_imp ni1 ni2)) (@eq nested_imp x x') *)
elim (in_app_or_ni x ni1 (x' :: ni2) in_ni_x_ni); clear in_ni_x_ni.
(* Goal: forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app dni (@cons nested_imp (Decorated n k) ni))), A *)
intros in_ni1; left; apply in_ni0_in_nini; assumption.
(* Goal: forall _ : @In nested_imp x (@cons nested_imp x' ni2), or (@In nested_imp x (@app nested_imp ni1 ni2)) (@eq nested_imp x x') *)
intros in_ni2; inversion_clear in_ni2.
(* Goal: or (@In nested_imp x (@app nested_imp ni1 ni2)) (@eq nested_imp x x') *)
(* Goal: or (@In nested_imp x (@app nested_imp ni1 ni2)) (@eq nested_imp x x') *)
right. 
(* Goal: forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app dni (@cons nested_imp (Decorated n k) ni))), A *)
symmetry  in |- *; assumption.
(* Goal: forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app dni (@cons nested_imp (Decorated n k) ni))), A *)
left; apply in_ni1_in_nini; assumption.
Qed.



Lemma in_ni_x_ni_tail :
 forall (x x' : nested_imp) (ni1 ni2 : nested_imps),
 In x (ni1 ++ ni2) -> In x (ni1 ++ x' :: ni2).
(* Goal: forall (x x' : nested_imp) (ni1 ni2 : nested_imps) (_ : @In nested_imp x (@app nested_imp ni1 ni2)), @In nested_imp x (@app nested_imp ni1 (@cons nested_imp x' ni2)) *)
intros x x' ni1 ni2 in_nini.
(* Goal: @In nested_imp x (@app nested_imp ni1 (@cons nested_imp x' ni2)) *)
elim (in_app_or_ni x ni1 ni2 in_nini); clear in_nini.
(* Goal: forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app dni (@cons nested_imp (Decorated n k) ni))), A *)
intros in_ni1; apply in_ni0_in_nini; assumption.
(* Goal: forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app dni (@cons nested_imp (Decorated n k) ni))), A *)
intros in_ni2; apply in_ni1_in_nini; right; assumption.
Qed.



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

Lemma rev_app_lemma0 :
 forall (dni : decorated_nested_imps) (ni : nested_imps),
 {dni_ni : nested_imps | dni_ni = rev_app dni ni}.
(* Goal: forall (dni : decorated_nested_imps) (ni : nested_imps), rev_app_spec dni ni *)
intros dni; elim dni; clear dni.
(* Goal: @eq nested_imps ni ni *)
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall ni : nested_imps, @eq nested_imps (rev_app l ni) (@app nested_imp (rev_app l NNil) ni)) (ni : nested_imps), @eq nested_imps (rev_app (@cons decorated_nested_imp a l) ni) (@app nested_imp (rev_app (@cons decorated_nested_imp a l) NNil) ni) *)
intros ni; exists ni; trivial.
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall (ni : nested_imps) (_ : forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app l ni)), A), A) (ni : nested_imps) (_ : forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app (@cons decorated_nested_imp a l) ni)), A), A *)
intros x; case x; clear x.
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list decorated_nested_imp) (_ : forall (ni : nested_imps) (_ : forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app l ni)), A), A) (ni : nested_imps) (_ : forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app (@cons decorated_nested_imp (@pair nimp kripke_tree n k) l) ni)), A), A *)
intros n k dni ih ni.
(* Goal: A *)
apply (ih (Decorated n k :: ni)).
Qed.

Inductive rev_app_spec (dni : decorated_nested_imps) 
(ni : nested_imps) : Set :=
    Rev_App_Spec_Intro :
      forall dni_ni : nested_imps,
      dni_ni = rev_app dni ni -> rev_app_spec dni ni.

Lemma rev_app_lemma1 :
 forall (dni : decorated_nested_imps) (ni : nested_imps), rev_app_spec dni ni.
(* Goal: forall (dni : decorated_nested_imps) (ni : nested_imps), rev_app_spec dni ni *)
intros dni; elim dni; clear dni.
(* Goal: @eq nested_imps ni ni *)
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall ni : nested_imps, @eq nested_imps (rev_app l ni) (@app nested_imp (rev_app l NNil) ni)) (ni : nested_imps), @eq nested_imps (rev_app (@cons decorated_nested_imp a l) ni) (@app nested_imp (rev_app (@cons decorated_nested_imp a l) NNil) ni) *)
intros ni; exists ni; trivial.
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall (ni : nested_imps) (_ : forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app l ni)), A), A) (ni : nested_imps) (_ : forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app (@cons decorated_nested_imp a l) ni)), A), A *)
intros x; case x; clear x.
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list decorated_nested_imp) (_ : forall (ni : nested_imps) (_ : forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app l ni)), A), A) (ni : nested_imps) (_ : forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app (@cons decorated_nested_imp (@pair nimp kripke_tree n k) l) ni)), A), A *)
intros n k dni ih ni.
(* Goal: rev_app_spec (@cons decorated_nested_imp (@pair nimp kripke_tree n k) dni) ni *)
elim (ih (Decorated n k :: ni)).
(* Goal: forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app dni (@cons nested_imp (Decorated n k) ni))), rev_app_spec (@cons decorated_nested_imp (@pair nimp kripke_tree n k) dni) ni *)
intros dni_ni eq.
(* Goal: forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app dni (@cons nested_imp (Decorated n k) ni))), A *)
exists dni_ni; assumption.
Qed.

Lemma rev_app_lemma2 :
 forall (A : Set) (dni : decorated_nested_imps) (ni : nested_imps),
 (forall dni_ni : nested_imps, dni_ni = rev_app dni ni -> A) -> A.
(* Goal: forall (A : Set) (dni : decorated_nested_imps) (ni : nested_imps) (_ : forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app dni ni)), A), A *)
intros A dni; elim dni; clear dni.
(* Goal: @eq nested_imps ni ni *)
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall ni : nested_imps, @eq nested_imps (rev_app l ni) (@app nested_imp (rev_app l NNil) ni)) (ni : nested_imps), @eq nested_imps (rev_app (@cons decorated_nested_imp a l) ni) (@app nested_imp (rev_app (@cons decorated_nested_imp a l) NNil) ni) *)
intros ni sk; apply (sk ni); trivial.
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall (ni : nested_imps) (_ : forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app l ni)), A), A) (ni : nested_imps) (_ : forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app (@cons decorated_nested_imp a l) ni)), A), A *)
intros x; case x; clear x.
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list decorated_nested_imp) (_ : forall (ni : nested_imps) (_ : forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app l ni)), A), A) (ni : nested_imps) (_ : forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app (@cons decorated_nested_imp (@pair nimp kripke_tree n k) l) ni)), A), A *)
intros n k dni ih ni.
(* Goal: forall _ : forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app (@cons decorated_nested_imp (@pair nimp kripke_tree n k) dni) ni)), A, A *)
intros sk.
(* Goal: A *)
apply (ih (Decorated n k :: ni)).
(* Goal: forall (dni_ni : nested_imps) (_ : @eq nested_imps dni_ni (rev_app dni (@cons nested_imp (Decorated n k) ni))), A *)
assumption.
(*
Intros A dni ni sk.
Apply (sk (rev_app dni ni)).
Trivial.
*)
Qed.