diff options
Diffstat (limited to 'contrib/rtauto/Rtauto.v')
| -rw-r--r-- | contrib/rtauto/Rtauto.v | 398 |
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. -*) |