
Require Refine.

Inductive term : Set :=
	nil : term
      | cons : term -> term -> term
      | t : term -> term
      | c : term -> term -> term
      | pubk : term -> term
      | privk : term -> term
      | symk : term -> term -> term
      | nonce : nat -> term -> term (* nonce (version, cons(x, cons(y, ...nil))). *)
	.

Lemma exists_term : (EX x : term | True).
Proof.
  Exists (nonce O nil). Trivial.
Qed.

Inductive knows : term -> Prop :=
	knows_nil : (knows nil)
      | knows_enc : (m, k:term) (knows m) -> (knows k) -> (knows (c m k))
      | knows_dec_privk : (m, a:term) (knows (c m (pubk a))) -> (knows (privk a)) -> (knows m)
      | knows_dec_pubk : (m, a:term) (knows (c m (privk a))) -> (knows (pubk a)) -> (knows m)
      | knows_dec_symk : (m, a, b:term) (knows (c m (symk a b))) -> (knows (symk a b)) -> (knows m)
      | knows_cons : (m, l:term) (knows m) -> (knows l) -> (knows (cons m l))
      | knows_p1 : (m, l:term) (knows (cons m l)) -> (knows m)
      | knows_p2 : (m, l:term) (knows (cons m l)) -> (knows l)
.

(* A la main: aucun resolvent sauf tautologies.
	Donne donne l'automate suivant: *)

Inductive auto_knows : term -> Prop :=
	auto_knows_nil : (auto_knows nil)
      | auto_knows_enc : (m, k:term) (auto_knows m) -> (auto_knows k) -> (auto_knows (c m k))
      | auto_knows_cons : (m, l:term) (auto_knows m) -> (auto_knows l) -> (auto_knows (cons m l))
.

Lemma auto_knows_dec_privk : (m, a:term) (auto_knows (c m (pubk a))) -> (auto_knows (privk a))
	-> (auto_knows m).
Proof.
  Intros m a p. Inversion p. Trivial.
Qed.

Lemma auto_knows_dec_pubk : (m, a:term) (auto_knows (c m (privk a))) -> (auto_knows (pubk a))
	-> (auto_knows m).
Proof.
  Intros m a p. Inversion p. Trivial.
Qed.

Lemma auto_knows_dec_symk : (m, a, b:term) (auto_knows (c m (symk a b))) -> (auto_knows (symk a b))
	-> (auto_knows m).
Proof.
  Intros m a b p. Inversion p. Trivial.
Qed.

Lemma auto_knows_p1 : (m, l:term) (auto_knows (cons m l)) -> (auto_knows m).
Proof.
  Intros m l p. Inversion p. Trivial.
Qed.

Lemma auto_knows_p2 : (m, l:term) (auto_knows (cons m l)) -> (auto_knows l).
Proof.
  Intros m l p. Inversion p. Trivial.
Qed.

Lemma auto_in_gnrl : (t:term) (knows t) -> (auto_knows t).
Proof.
  Intros t p. Elim p; Intros.
  Apply auto_knows_nil.
  Apply (auto_knows_enc m k); Assumption.
  Apply (auto_knows_dec_privk m a); Assumption.
  Apply (auto_knows_dec_pubk m a); Assumption.
  Apply (auto_knows_dec_symk m a b); Assumption.
  Apply (auto_knows_cons m l); Assumption.
  Apply (auto_knows_p1 m l); Assumption.
  Apply (auto_knows_p2 m l); Assumption.
Qed.

(*--------------------------------------------------------------------------------------*)

Variable P, Q, R : term -> Prop.

Variable rem1 : (x,y,z:term) (P x) -> (P y) -> (P z) -> (Q (c x y)).
Variable rem2 : (X,Y,Z:term) (Q (c (t (cons X (cons Y nil))) X)) -> (P Z) -> (R (c X Z)).
Remark rem3 : (z,X,Y,Z:term) (P (t (cons X (cons Y nil)))) -> (P X) -> (P z) -> (P Z) -> (R (c X Z)).
Proof.
  Intros. Refine (rem2 X Y Z (rem1 (t (cons X (cons Y nil))) X z ? ? ?) ?); Assumption.
Qed.

(*
Proof.
  Intros. Cut (Q (c (t (cons X (cons Y nil))) X)).
  Intro.
  Apply (rem2 X Y Z); Assumption.
  Apply (rem1 (t (cons X (cons Y nil))) X z); Assumption.
Qed.
*)

(*
Proof.
  Intros. Apply (rem2 X Y Z). Apply (rem1 (t (cons X (cons Y nil))) X z).
  Assumption. Assumption. Assumption. Assumption.
Qed.
*)

Variable rem4 : (x,y,z:term) (P x) -> (Q x) -> (P y) -> (P z) -> (R z).
Lemma rem5 : (z:term) (EX x:term | (P x) /\ (Q x)) -> (EX x:term | (P x)) -> (P z) -> (R z).
Proof.
  Intros z.
  Intro p; Elim p; Clear p; Intros x p1.
  Intro p; Elim p; Clear p; Intros y p2.
  Intros.
  Apply (rem4 x y z); Tauto.
Qed.

(*
Proof.
  Intros z. Intros.
  Elim H; Clear H; Intros x p1.
  Elim H0; Clear H0; Intros y p2.
  Apply (rem4 x y z); Tauto.
Qed.
*)

Lemma rem6 : (z:term) (P z) -> (Q z) -> (EX x:term | (P x) /\ (Q x)).
Proof.
  Intros z. Intros. Exists z; Tauto.
Qed.

(*--------------------------------------------------------------------------------------*)

Inductive P1 : term -> Prop :=
    P1_nil_1 : (P1 nil)
  | P1_cons_1 : (x,y:term) (Q1 x) -> (P1 y) -> (P1 (cons x y))
with Q1 : term -> Prop :=
    Q1_t_1 : (x:term) (P1 x) -> (Q1 (t x))
with P2 : term -> Prop :=
    P2_nil_1 : (P2 nil)
  | P2_cons_1 : (x,y:term) (Q1 x) -> (P1 y) -> (P2 (cons x y))
with P3 : term -> Prop :=
    P3_nil_1 : (P3 nil)
  | P3_cons_1 : (x,y:term) (Q1 x) -> (P3 y) -> (P3 (cons x y))
with P4 : term -> Prop :=
    P4_nil_1 : (P4 nil)
  | P4_cons_1 : (x,y:term) (Q4 x) -> (P4 y) -> (P4 (cons x y))
with Q4 : term -> Prop :=
    Q4_t_1 : (x:term) (P4 x) -> (Q4 (t x)).

Lemma P2_in_P1 : (x:term) (P2 x) -> (P1 x).
Proof.
  Intros x H.
  Case H.
  Exact P1_nil_1.
  Exact P1_cons_1.
Qed.

Lemma P3_in_P1 : (x:term) (P3 x) -> (P1 x).
Proof.
  Fix 2.
  Intros x H. Case H. Exact P1_nil_1.
  Intros. Apply P1_cons_1. Assumption.
  Apply P3_in_P1. Assumption.
Qed.

(*
Proof.
  Intros x H. Elim H. Exact P1_nil_1.
  Intros. Apply P1_cons_1; Assumption.
Qed.
*)

Lemma P4_in_P1 : (x:term) (P4 x) -> (P1 x).
Proof.
  Fix rec 2.
  Intros x H. Case H. Exact P1_nil_1.
  Intros x0 y H1 H2. Case H1. Intros. Apply P1_cons_1. Apply Q1_t_1.
  Apply rec. Assumption.
  Apply rec. Assumption.
Qed.

Lemma P4_in_P1_aux : ((x:term) (P4 x) -> (P1 x)) -> ((x:term) (P4 x) -> (P1 x)).
Proof.
  Intro rec.
  Intros x H. Case H. Exact P1_nil_1.
  Intros x0 y H1 H2. Case H1. Intros. Apply P1_cons_1. Apply Q1_t_1.
  Apply rec. Assumption.
  Apply rec. Assumption.
Defined. (* Important! pas Qed, sinon ca ne marche pas dans P4_in_P1_alt. *)

Lemma P4_in_P1_alt : (x:term) (P4 x) -> (P1 x).
Proof.
  Fix rec 2.
  Intros x H.
  Exact (P4_in_P1_aux rec x H). (* Exact (P4_in_P1_aux_2 rec).
	ne suffit pas, il faut eta-expanser pour que Coq accepte... *)
Qed.

(*--------------------------------------------------------------------------------------*)

Lemma history_1 : ((x:term) (P x) -> (Q x) \/ (R x)) -> (x,y,z:term) (P1 x) -> (P (c x y)) -> (R (c x y)) \/ (P4 z) \/ (Q (c x y)).
Proof.
  Intro H0.
  Intros x y z.
  Cut (P (c x y))->(Q (c x y))\/(R (c x y)).
  Tauto.
  Exact (H0 (c x y)).
Defined.

Variable gag_1 : ((x:term) (P x) -> (Q x) \/ (R x)) -> (x,y:term) (Q1 x) -> (P1 y) -> (P x).

Lemma elim_neg_1 : ((x:term) (P x) -> (Q x) \/ (R x)) -> (x,y:term) (P1 (cons x y)) -> (P x).
Proof.
  Intros H1 x y H.
  Refine (P1_ind [z:term]Cases z of
                         (cons x y) => (P x)
                       | _ => True
                       end ? ? ? H); Try Exact I.
  Intros. Exact (gag_1 H1 x0 y0 H0 H2).
Defined.

(*
  Intros H1 x y H.
  Refine (P1_ind [z:term]Cases z of (cons x y) => (P x) | _ => True end ? ? ? H);[Exact I | Intros; Exact (gag_1 H1 x0 y0 H0 H2)].
*)

(*
Proof.
  Intros H1 x y H.
  Inversion H.
  Apply (gag_1 H1 x y); Assumption.
Defined.
*)

Inductive or_3 [H1,H2,H3:Prop] : Prop :=
    or_3_1 : H1 -> (or_3 H1 H2 H3)
  | or_3_2 : H2 -> (or_3 H1 H2 H3)
  | or_3_3 : H3 -> (or_3 H1 H2 H3).

(*
Lemma or_tauto : (A,B,C:Prop) (or_3 A B C) -> (or_3 B A C).
Tauto failed!
*)

Inductive R1 : term -> Prop :=
    R1_cons_1 : (x,y:term) (R1 x) -> (P2 y) -> (P3 y) -> (R1 (cons x y))
  | R1_cons_2 : (x,y:term) (P4 x) -> (R1 y) -> (R1 (cons x y))
  | R1_cons_3 : (x,y:term) (P3 x) -> (R1 (cons x y))
  | R1_t_1 : (x:term) (R1 x) -> (P1 x) -> (R1 (t x))
  | R1_t_2 : (x:term) (P3 x) -> (R1 (t x)).

Lemma R1_cons_inversion : (x,y:term) (R1 (cons x y)) -> (or_3
	((R1 x) /\ (P2 y) /\ (P3 y))
	((P4 x) /\ (R1 y))
	(P3 x)).
Proof.
  Intros. Inversion H.
  Apply or_3_1; Tauto.
  Apply or_3_2; Tauto.
  Apply or_3_3; Tauto.
Qed.

Variable R1_gag1 : (x,y:term) (P4 x) -> (R1 x) \/ (P4 x) \/ (P3 x) \/ (P3 y).
Variable R1_gag2 : (x,y:term) (P4 x) -> (R1 x) \/ (R1 y) \/ (P3 x) \/ (P3 y).
Variable R1_gag3 : (x,y:term) (P4 x) -> (P2 y) \/ (P4 x) \/ (P3 x) \/ (P3 y).
Variable R1_gag4 : (x,y:term) (P4 x) -> (P2 y) \/ (R1 y) \/ (P3 x) \/ (P3 y).
Variable R1_gag5 : (x,y:term) (P4 x) -> (P3 y) \/ (P4 x) \/ (P3 x).
Variable R1_gag6 : (x,y:term) (P4 x) -> (P3 y) \/ (R1 y) \/ (P3 x).

Lemma R1_gag_1 : (x,y:term) (P4 x) ->
	(R1 x) /\ (P2 y) /\ (P3 y) \/
	(P4 x) /\ (R1 y) \/
	(P3 x) \/
	(P3 y).
Proof.
  Intros x y A1.
  Cut (R1 x) \/ (R1 y) \/ (P3 x) \/ (P3 y).
  2:Apply R1_gag2; Assumption.
  Cut (P2 y) \/ (R1 y) \/ (P3 x) \/ (P3 y).
  2:Apply R1_gag4; Assumption.
  Cut (P3 y) \/ (R1 y) \/ (P3 x).
  2:Apply R1_gag6; Assumption.
  Tauto.
Defined.

(*
Proof.
  Intros x y A1.
  Cut (R1 x) \/ (P4 x) \/ (P3 x) \/ (P3 y).
  2:Apply R1_gag1; Assumption.
  Cut (R1 x) \/ (R1 y) \/ (P3 x) \/ (P3 y).
  2:Apply R1_gag2; Assumption.
  Cut (P2 y) \/ (P4 x) \/ (P3 x) \/ (P3 y).
  2:Apply R1_gag3; Assumption.
  Cut (P2 y) \/ (R1 y) \/ (P3 x) \/ (P3 y).
  2:Apply R1_gag4; Assumption.
  Cut (P3 y) \/ (P4 x) \/ (P3 x).
  2:Apply R1_gag5; Assumption.
  Cut (P3 y) \/ (R1 y) \/ (P3 x).
  2:Apply R1_gag6; Assumption.
  Clear A1.
  Tauto.
Defined.
*)

Lemma R1_gag_2 : (x,y:term) (P4 x) -> (P3 y) \/ (R1 (cons x y)).
Proof.
  Intros x y.
  Intros H1.
  Case (R1_gag_1 x y H1). Clear H1. Intros. Right. Apply R1_cons_1; Tauto.
  Intro H. Case H; Clear H. Clear H1. Intros. Right. Apply R1_cons_2; Tauto.
  Intro H. Case H; Clear H. Clear H1. Intros. Right. Apply R1_cons_3; Tauto.
  Clear H1. Tauto.
Defined.

Inductive or_2 [H1,H2:Prop] : Prop :=
    or_2_1 : H1 -> (or_2 H1 H2)
  | or_2_2 : H2 -> (or_2 H1 H2).

Inductive ex0 [P : Prop] : Prop :=
    ex0_intro : P -> (ex0 P).

Inductive ex1 [P : term -> Prop] : Prop :=
    ex1_intro : (x1:term) (P x1) -> (ex1 P).

Inductive ex2 [P : term -> term -> Prop] : Prop :=
    ex2_intro : (x1:term) (x2:term) (P x1 x2) -> (ex2 P).

Lemma R1_inversion : (x:term) (R1 x) -> (or_2
  (ex2 [x1,x2:term] x=(cons x1 x2))
  (ex1 [x1:term] x=(t x1))
  ).
Proof.
  Intros x H. Inversion H.
  Apply or_2_1. EApply ex2_intro. Reflexivity.
  Apply or_2_1. EApply ex2_intro. Reflexivity.
  Apply or_2_1. EApply ex2_intro. Reflexivity.
  Apply or_2_2. EApply ex1_intro. Reflexivity.
  Apply or_2_2. EApply ex1_intro. Reflexivity.
Qed.

(*
Lemma R1_dummy : (x:term) (R1 x) -> (R1 x).
*)

(*--------------------------------------------------------------------------------------*)

Variable rem_1 : ((_x:term) (P4 _x) -> (P3 _x)) -> (x:term) (P1 x) -> ((P2 x) /\ (P3 x)) \/ (P4 x).

Lemma rem_2 : ((_x:term) (P4 _x) -> (P3 _x)) -> (x,y:term) (P1 x) ->
	((P2 y) /\ (P4 x)) \/ ((P2 x) /\ (P3 x)) \/ (P4 x).
Proof.
  Intro H1. Intros x y. Intro A1. Case (rem_1 H1 x A1); Tauto.
Defined.

(*--------------------------------------------------------------------------------------*)


Inductive term : Set :=
	nil : term
      | cons : term -> term -> term
      | t : term -> term
      | c : term -> term -> term
      | pubk : term -> term
      | privk : term -> term
      | symk : term -> term -> term
      | nonce : nat -> term -> term (* nonce (version, cons(x, cons(y, ...nil))). *)
	.

Variable P, Q, R : term -> Prop.

Parameter term_witness : term.

Axiom A : (x,y:term) (Q x) -> (P (cons x y)).
Axiom B : (x,y:term) (P (cons x y)) -> (R x).

Goal (x:term) (Q x) -> (R x).
Intros.
Refine (B x term_witness (A x term_witness ?)); Assumption.


