Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 0 insertions, 398 deletions

diff --git a/contrib/rtauto/Rtauto.v b/contrib/rtauto/Rtauto.v
deleted file mode 100644
index 98fca90f..00000000
--- a/contrib/rtauto/Rtauto.v
+++ /dev/null
@@ -1,398 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: Rtauto.v 7639 2005-12-02 10:01:15Z gregoire $ *)
-
-
-Require Export List.
-Require Export Bintree.
-Require Import Bool.
-Unset Boxed Definitions.
-
-Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
-Ltac clean:=try (simpl;congruence).
-
-Inductive form:Set:=
-  Atom : positive -> form
-| Arrow : form -> form -> form
-| Bot
-| Conjunct : form -> form -> form 
-| Disjunct : form -> form -> form.
-
-Notation "[ n ]":=(Atom n).
-Notation "A =>> B":= (Arrow A B) (at level 59, right associativity).
-Notation "#" := Bot.
-Notation "A //\\ B" := (Conjunct A B) (at level 57, left associativity).
-Notation "A \\// B" := (Disjunct A B) (at level 58, left associativity).
-
-Definition ctx := Store form.
-
-Fixpoint pos_eq (m n:positive) {struct m} :bool :=
-match m with
-  xI mm => match n with xI nn => pos_eq mm nn | _ => false end
-| xO mm => match n with xO nn => pos_eq mm nn | _ => false end
-| xH => match n with xH => true | _ => false end
-end. 
-
-Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n.
-induction m;simpl;destruct n;congruence ||
-(intro e;apply f_equal with positive;auto).
-Qed.
-
-Fixpoint form_eq (p q:form) {struct p} :bool :=
-match p with
-  Atom m => match q with Atom n => pos_eq m n | _ => false end
-| Arrow p1 p2 => 
-match q with 
-  Arrow q1 q2 => form_eq p1 q1 && form_eq p2 q2 
-| _ => false end
-| Bot => match q with Bot => true | _ => false end
-| Conjunct p1 p2 => 
-match q with 
-  Conjunct q1 q2 => form_eq p1 q1 && form_eq p2 q2 
-| _ => false 
-end
-| Disjunct p1 p2 => 
-match q with 
-  Disjunct q1 q2 => form_eq p1 q1 && form_eq p2 q2 
-| _ => false 
-end
-end. 
-
-Theorem form_eq_refl: forall p q, form_eq p q = true -> p = q.
-induction p;destruct q;simpl;clean.
-intro h;generalize (pos_eq_refl _ _ h);congruence.
-caseq (form_eq p1 q1);clean.
-intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. 
-caseq (form_eq p1 q1);clean.
-intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. 
-caseq (form_eq p1 q1);clean.
-intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. 
-Qed.
-
-Implicit Arguments form_eq_refl [p q].
-
-Section with_env.
-
-Variable env:Store Prop.
-
-Fixpoint interp_form (f:form): Prop :=
-match f with
-[n]=> match get n env with PNone => True | PSome P => P end
-| A =>> B => (interp_form A) -> (interp_form B)
-| # => False
-| A //\\ B => (interp_form A) /\ (interp_form B)
-| A \\// B => (interp_form A) \/ (interp_form B)
-end.
-
-Notation "[[ A ]]" := (interp_form A).
-
-Fixpoint interp_ctx (hyps:ctx) (F:Full hyps) (G:Prop) {struct F} : Prop :=
-match F with
-  F_empty => G
-| F_push H hyps0 F0 =>  interp_ctx hyps0 F0  ([[H]] -> G)
-end.
-
-Require Export BinPos.
-
-Ltac wipe := intros;simpl;constructor.  
-
-Lemma compose0 : 
-forall hyps F (A:Prop),
- A -> 
- (interp_ctx hyps F A).
-induction F;intros A H;simpl;auto.
-Qed.
-
-Lemma compose1 : 
-forall hyps F (A B:Prop),
- (A -> B) ->
- (interp_ctx hyps F A) ->
- (interp_ctx hyps F B).
-induction F;intros A B H;simpl;auto.
-apply IHF;auto.
-Qed.
-
-Theorem compose2 : 
-forall hyps F (A B C:Prop),
- (A -> B -> C) -> 
- (interp_ctx hyps F A) ->
- (interp_ctx hyps F B) ->
- (interp_ctx hyps F C).
-induction F;intros A B C H;simpl;auto.
-apply IHF;auto.
-Qed.
-
-Theorem compose3 : 
-forall hyps F (A B C D:Prop),
- (A -> B -> C -> D) -> 
- (interp_ctx hyps F A) -> 
- (interp_ctx hyps F B) ->
- (interp_ctx hyps F C) ->
- (interp_ctx hyps F D).
-induction F;intros A B C D H;simpl;auto.
-apply IHF;auto.
-Qed.
-
-Lemma weaken : forall hyps F f G,
- (interp_ctx hyps F G) ->
- (interp_ctx (hyps\f)  (F_push f hyps F) G).
-induction F;simpl;intros;auto.
-apply compose1 with ([[a]]-> G);auto.
-Qed.
-
-Theorem project_In : forall hyps F g, 
-In g hyps F ->
-interp_ctx hyps F [[g]].
-induction F;simpl.
-contradiction.
-intros g H;destruct H.
-subst;apply compose0;simpl;trivial.
-apply compose1 with [[g]];auto.
-Qed.
-
-Theorem project : forall hyps F p g, 
-get  p hyps = PSome g->
-interp_ctx hyps F [[g]].
-intros hyps F p g e; apply project_In.
-apply get_In with p;assumption.
-Qed.
-
-Implicit Arguments project [hyps p g].
-
-Inductive proof:Set :=
-  Ax : positive -> proof
-| I_Arrow : proof -> proof
-| E_Arrow : positive -> positive -> proof -> proof
-| D_Arrow : positive -> proof -> proof -> proof
-| E_False : positive -> proof
-| I_And: proof -> proof -> proof
-| E_And: positive -> proof -> proof
-| D_And: positive -> proof -> proof
-| I_Or_l: proof -> proof
-| I_Or_r: proof -> proof
-| E_Or: positive -> proof -> proof -> proof
-| D_Or: positive -> proof -> proof
-| Cut: form -> proof -> proof -> proof.
-
-Notation "hyps \ A" := (push A hyps) (at level 72,left associativity).
-
-Fixpoint check_proof (hyps:ctx) (gl:form) (P:proof) {struct P}: bool :=
- match P with
-   Ax i => 
-     match get i hyps with
-         PSome F => form_eq F gl
- | _ => false
-    end 
-| I_Arrow p =>
-   match gl with
-      A  =>> B  => check_proof (hyps \ A) B p
-   | _ => false        
-    end 
-| E_Arrow i j p =>
-   match get i hyps,get j hyps with
-       PSome A,PSome (B =>>C) =>
-         form_eq A B && check_proof (hyps \ C) (gl) p
-    | _,_ => false
-    end
-| D_Arrow i p1 p2 => 
-   match get i hyps with
-      PSome  ((A =>>B)=>>C) =>
-     (check_proof ( hyps \ B =>> C \ A) B p1) && (check_proof (hyps \ C) gl p2)
-    | _ => false
-  end
-| E_False i =>
-  match get i hyps with
-    PSome # => true
-  | _ => false
-  end
-| I_And p1 p2 =>
-   match gl with
-      A //\\ B =>
-      check_proof hyps A p1 && check_proof hyps B p2
-      | _ => false
-      end
-| E_And i p => 
-   match get i hyps with
-      PSome  (A //\\ B) => check_proof (hyps \ A \ B) gl p
-    | _=> false
-   end
-| D_And i p => 
-   match get i hyps with
-      PSome  (A //\\ B =>> C) => check_proof (hyps \ A=>>B=>>C) gl p
-    | _=> false
-   end
-| I_Or_l p =>
-   match gl with
-      (A \\// B) => check_proof hyps A p
-      | _ => false
-      end
-| I_Or_r p =>
-   match gl with
-      (A \\// B) => check_proof hyps B p
-      | _ => false
-      end
-| E_Or i p1 p2 =>
-  match get i hyps with
-  PSome (A \\// B) =>
-  check_proof (hyps \ A) gl p1 && check_proof (hyps \ B) gl p2
-  | _=> false
-  end
-| D_Or i p => 
-   match get i hyps with
-      PSome  (A \\// B =>> C) =>
-      (check_proof (hyps \ A=>>C \ B=>>C) gl p)
-    | _=> false
-   end
-| Cut A p1 p2 =>
-  check_proof hyps A p1 && check_proof (hyps \ A) gl p2
-end. 
-
-Theorem interp_proof: 
-forall p hyps F gl, 
-check_proof hyps gl p = true -> interp_ctx hyps F [[gl]].
-
-induction p;intros hyps F gl.
-
-(* cas Axiom *)
-Focus 1.
-simpl;caseq (get p hyps);clean.
-intros f nth_f e;rewrite <- (form_eq_refl e).
-apply project with p;trivial.
-
-(* Cas Arrow_Intro *)
-Focus 1.
-destruct gl;clean.
-simpl;intros.
-change (interp_ctx (hyps\gl1)  (F_push gl1 hyps F) [[gl2]]).
-apply IHp;try constructor;trivial.
-
-(* Cas Arrow_Elim *)
-Focus 1.
-simpl check_proof;caseq (get p hyps);clean.
-intros f ef;caseq (get p0 hyps);clean.
-intros f0 ef0;destruct f0;clean.
-caseq (form_eq f f0_1);clean.
-simpl;intros e check_p1.
-generalize  (project  F ef) (project  F ef0) 
-(IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1);
-clear check_p1 IHp p p0 p1 ef ef0.
-simpl.
-apply compose3.
-rewrite (form_eq_refl e).
-auto.
-
-(* cas Arrow_Destruct *)
-Focus 1.
-simpl;caseq (get p1 hyps);clean.
-intros f ef;destruct f;clean.
-destruct f1;clean.
-caseq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2);clean.
-intros check_p1 check_p2.
-generalize (project F ef)
-(IHp1 (hyps \ f1_2 =>> f2 \ f1_1)   
-(F_push f1_1 (hyps \ f1_2 =>> f2)
- (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1)
-(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2).
-simpl;apply compose3;auto.
-
-(* Cas False_Elim *)
-Focus 1.
-simpl;caseq (get p hyps);clean.
-intros f ef;destruct f;clean.
-intros _; generalize (project F ef).
-apply compose1;apply False_ind.
-
-(* Cas And_Intro *)
-Focus 1.
-simpl;destruct gl;clean.
-caseq (check_proof hyps gl1 p1);clean.
-intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2).
-apply compose2 ;simpl;auto.
-
-(* cas And_Elim *)
-Focus 1.
-simpl;caseq (get p hyps);clean.
-intros f ef;destruct f;clean.
-intro check_p;generalize  (project F ef)
-(IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p).
-simpl;apply compose2;intros [h1 h2];auto.
-
-(* cas And_Destruct *)
-Focus 1.
-simpl;caseq (get p hyps);clean.
-intros f ef;destruct f;clean.
-destruct f1;clean.
-intro H;generalize  (project F ef)
-(IHp (hyps \ f1_1 =>> f1_2 =>> f2)  
-(F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H);clear H;simpl.
-apply compose2;auto.
-
-(* cas Or_Intro_left *)
-Focus 1.
-destruct gl;clean.
-intro Hp;generalize (IHp hyps F gl1 Hp).
-apply compose1;simpl;auto.
-
-(* cas Or_Intro_right *)
-Focus 1.
-destruct gl;clean.
-intro Hp;generalize (IHp hyps F gl2 Hp).
-apply compose1;simpl;auto.
-
-(* cas Or_elim *)
-Focus 1.
-simpl;caseq (get p1 hyps);clean.
-intros f ef;destruct f;clean.
-caseq (check_proof (hyps \ f1) gl p2);clean.
-intros check_p1 check_p2;generalize (project F ef)
-(IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1)
-(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2);
-simpl;apply compose3;simpl;intro h;destruct h;auto.
-
-(* cas Or_Destruct *)
-Focus 1.
-simpl;caseq (get p hyps);clean.
-intros f ef;destruct f;clean.
-destruct f1;clean.
-intro check_p0;generalize (project F ef)
-(IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2)
-(F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) 
- (F_push (f1_1 =>> f2) hyps F)) gl check_p0);simpl.
-apply compose2;auto.
-
-(* cas Cut *)
-Focus 1.
-simpl;caseq (check_proof hyps f p1);clean.
-intros check_p1 check_p2;
-generalize (IHp1 hyps F f check_p1) 
-(IHp2 (hyps\f) (F_push f hyps F) gl check_p2);
-simpl; apply compose2;auto.
-Qed.
-
-Theorem Reflect: forall gl prf, if check_proof empty gl prf then [[gl]] else True.
-intros gl prf;caseq (check_proof empty gl prf);intro check_prf.
-change (interp_ctx empty F_empty [[gl]]) ;
-apply interp_proof with prf;assumption.
-trivial.
-Qed.
-
-End with_env.
-
-(*
-(* A small example *)
-Parameters A B C D:Prop.
-Theorem toto:A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).
-exact (Reflect (empty \ A \ B \ C)
-([1] //\\ ([2] \\// [3]) =>> [1] //\\ [2] \\// [1] //\\ [3])
-(I_Arrow (E_And 1 (E_Or 3 
-  (I_Or_l (I_And (Ax 2) (Ax 4))) 
-  (I_Or_r (I_And (Ax 2) (Ax 4))))))).
-Qed.
-Print toto.
-*)