diff options
Diffstat (limited to 'contrib/rtauto')
| -rw-r--r-- | contrib/rtauto/Bintree.v | 489 | ||||
| -rw-r--r-- | contrib/rtauto/Rtauto.v | 398 | ||||
| -rw-r--r-- | contrib/rtauto/g_rtauto.ml4 | 16 | ||||
| -rw-r--r-- | contrib/rtauto/proof_search.ml | 546 | ||||
| -rw-r--r-- | contrib/rtauto/proof_search.mli | 49 | ||||
| -rw-r--r-- | contrib/rtauto/refl_tauto.ml | 337 | ||||
| -rw-r--r-- | contrib/rtauto/refl_tauto.mli | 26 |
7 files changed, 0 insertions, 1861 deletions
diff --git a/contrib/rtauto/Bintree.v b/contrib/rtauto/Bintree.v deleted file mode 100644 index e90fea84..00000000 --- a/contrib/rtauto/Bintree.v +++ /dev/null @@ -1,489 +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: Bintree.v 10681 2008-03-16 13:40:45Z msozeau $ *) - -Require Export List. -Require Export BinPos. - -Unset Boxed Definitions. - -Open Scope positive_scope. - -Ltac clean := try (simpl; congruence). -Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t. - -Functional Scheme Pcompare_ind := Induction for Pcompare Sort Prop. - -Lemma Gt_Eq_Gt : forall p q cmp, - (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt. -apply (Pcompare_ind (fun p q cmp _ => (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt)); -simpl;auto;congruence. -Qed. - -Lemma Gt_Lt_Gt : forall p q cmp, - (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt. -apply (Pcompare_ind (fun p q cmp _ => (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt)); -simpl;auto;congruence. -Qed. - -Lemma Gt_Psucc_Eq: forall p q, - (p ?= Psucc q) Gt = Gt -> (p ?= q) Eq = Gt. -intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence. -intro;apply Gt_Eq_Gt;auto. -apply Gt_Lt_Gt. -Qed. - -Lemma Eq_Psucc_Gt: forall p q, - (p ?= Psucc q) Eq = Eq -> (p ?= q) Eq = Gt. -intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence. -intro H;elim (Pcompare_not_Eq p (Psucc q));tauto. -intro H;apply Gt_Eq_Gt;auto. -intro H;rewrite Pcompare_Eq_eq with p q;auto. -generalize q;clear q IHq p H;induction q;simpl;auto. -intro H;elim (Pcompare_not_Eq p q);tauto. -Qed. - -Lemma Gt_Psucc_Gt : forall n p cmp cmp0, - (n?=p) cmp = Gt -> (Psucc n?=p) cmp0 = Gt. -induction n;intros [ | p | p];simpl;try congruence. -intros; apply IHn with cmp;trivial. -intros; apply IHn with Gt;trivial. -intros;apply Gt_Lt_Gt;trivial. -intros [ | | ] _ H. -apply Gt_Eq_Gt;trivial. -apply Gt_Lt_Gt;trivial. -trivial. -Qed. - -Lemma Gt_Psucc: forall p q, - (p ?= Psucc q) Eq = Gt -> (p ?= q) Eq = Gt. -intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence. -apply Gt_Psucc_Eq. -intro;apply Gt_Eq_Gt;apply IHq;auto. -apply Gt_Eq_Gt. -apply Gt_Lt_Gt. -Qed. - -Lemma Psucc_Gt : forall p, - (Psucc p ?= p) Eq = Gt. -induction p;simpl. -apply Gt_Eq_Gt;auto. -generalize p;clear p IHp. -induction p;simpl;auto. -reflexivity. -Qed. - -Fixpoint pos_eq (m n:positive) {struct m} :bool := -match m, n with - xI mm, xI nn => pos_eq mm nn -| xO mm, xO nn => pos_eq mm nn -| xH, xH => true -| _, _ => false -end. - -Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n. -induction m;simpl;intro n;destruct n;congruence || -(intro e;apply f_equal with positive;auto). -Defined. - -Theorem refl_pos_eq : forall m, pos_eq m m = true. -induction m;simpl;auto. -Qed. - -Definition pos_eq_dec (m n:positive) :{m=n}+{m<>n} . -fix 1;intros [mm|mm|] [nn|nn|];try (right;congruence). -case (pos_eq_dec mm nn). -intro e;left;apply (f_equal xI e). -intro ne;right;congruence. -case (pos_eq_dec mm nn). -intro e;left;apply (f_equal xO e). -intro ne;right;congruence. -left;reflexivity. -Defined. - -Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left _ (refl_equal m). -fix 1;intros [mm|mm|]. -simpl; rewrite pos_eq_dec_refl; reflexivity. -simpl; rewrite pos_eq_dec_refl; reflexivity. -reflexivity. -Qed. - -Theorem pos_eq_dec_ex : forall m n, - pos_eq m n =true -> exists h:m=n, - pos_eq_dec m n = left _ h. -fix 1;intros [mm|mm|] [nn|nn|];try (simpl;congruence). -simpl;intro e. -elim (pos_eq_dec_ex _ _ e). -intros x ex; rewrite ex. -exists (f_equal xI x). -reflexivity. -simpl;intro e. -elim (pos_eq_dec_ex _ _ e). -intros x ex; rewrite ex. -exists (f_equal xO x). -reflexivity. -simpl. -exists (refl_equal xH). -reflexivity. -Qed. - -Fixpoint nat_eq (m n:nat) {struct m}: bool:= -match m, n with -O,O => true -| S mm,S nn => nat_eq mm nn -| _,_ => false -end. - -Theorem nat_eq_refl : forall m n, nat_eq m n = true -> m = n. -induction m;simpl;intro n;destruct n;congruence || -(intro e;apply f_equal with nat;auto). -Defined. - -Theorem refl_nat_eq : forall n, nat_eq n n = true. -induction n;simpl;trivial. -Defined. - -Fixpoint Lget (A:Set) (n:nat) (l:list A) {struct l}:option A := -match l with nil => None -| x::q => -match n with O => Some x -| S m => Lget A m q -end end . - -Implicit Arguments Lget [A]. - -Lemma map_app : forall (A B:Set) (f:A -> B) l m, -List.map f (l ++ m) = List.map f l ++ List.map f m. -induction l. -reflexivity. -simpl. -intro m ; apply f_equal with (list B);apply IHl. -Qed. - -Lemma length_map : forall (A B:Set) (f:A -> B) l, -length (List.map f l) = length l. -induction l. -reflexivity. -simpl; apply f_equal with nat;apply IHl. -Qed. - -Lemma Lget_map : forall (A B:Set) (f:A -> B) i l, -Lget i (List.map f l) = -match Lget i l with Some a => -Some (f a) | None => None end. -induction i;intros [ | x l ] ;trivial. -simpl;auto. -Qed. - -Lemma Lget_app : forall (A:Set) (a:A) l i, -Lget i (l ++ a :: nil) = if nat_eq i (length l) then Some a else Lget i l. -induction l;simpl Lget;simpl length. -intros [ | i];simpl;reflexivity. -intros [ | i];simpl. -reflexivity. -auto. -Qed. - -Lemma Lget_app_Some : forall (A:Set) l delta i (a: A), -Lget i l = Some a -> -Lget i (l ++ delta) = Some a. -induction l;destruct i;simpl;try congruence;auto. -Qed. - -Section Store. - -Variable A:Type. - -Inductive Poption : Type:= - PSome : A -> Poption -| PNone : Poption. - -Inductive Tree : Type := - Tempty : Tree - | Branch0 : Tree -> Tree -> Tree - | Branch1 : A -> Tree -> Tree -> Tree. - -Fixpoint Tget (p:positive) (T:Tree) {struct p} : Poption := - match T with - Tempty => PNone - | Branch0 T1 T2 => - match p with - xI pp => Tget pp T2 - | xO pp => Tget pp T1 - | xH => PNone - end - | Branch1 a T1 T2 => - match p with - xI pp => Tget pp T2 - | xO pp => Tget pp T1 - | xH => PSome a - end -end. - -Fixpoint Tadd (p:positive) (a:A) (T:Tree) {struct p}: Tree := - match T with - | Tempty => - match p with - | xI pp => Branch0 Tempty (Tadd pp a Tempty) - | xO pp => Branch0 (Tadd pp a Tempty) Tempty - | xH => Branch1 a Tempty Tempty - end - | Branch0 T1 T2 => - match p with - | xI pp => Branch0 T1 (Tadd pp a T2) - | xO pp => Branch0 (Tadd pp a T1) T2 - | xH => Branch1 a T1 T2 - end - | Branch1 b T1 T2 => - match p with - | xI pp => Branch1 b T1 (Tadd pp a T2) - | xO pp => Branch1 b (Tadd pp a T1) T2 - | xH => Branch1 a T1 T2 - end - end. - -Definition mkBranch0 (T1 T2:Tree) := - match T1,T2 with - Tempty ,Tempty => Tempty - | _,_ => Branch0 T1 T2 - end. - -Fixpoint Tremove (p:positive) (T:Tree) {struct p}: Tree := - match T with - | Tempty => Tempty - | Branch0 T1 T2 => - match p with - | xI pp => mkBranch0 T1 (Tremove pp T2) - | xO pp => mkBranch0 (Tremove pp T1) T2 - | xH => T - end - | Branch1 b T1 T2 => - match p with - | xI pp => Branch1 b T1 (Tremove pp T2) - | xO pp => Branch1 b (Tremove pp T1) T2 - | xH => mkBranch0 T1 T2 - end - end. - - -Theorem Tget_Tempty: forall (p : positive), Tget p (Tempty) = PNone. -destruct p;reflexivity. -Qed. - -Theorem Tget_Tadd: forall i j a T, - Tget i (Tadd j a T) = - match (i ?= j) Eq with - Eq => PSome a - | Lt => Tget i T - | Gt => Tget i T - end. -intros i j. -caseq ((i ?= j) Eq). -intro H;rewrite (Pcompare_Eq_eq _ _ H);intros a;clear i H. -induction j;destruct T;simpl;try (apply IHj);congruence. -generalize i;clear i;induction j;destruct T;simpl in H|-*; -destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence. -generalize i;clear i;induction j;destruct T;simpl in H|-*; -destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence. -Qed. - -Record Store : Type := -mkStore {index:positive;contents:Tree}. - -Definition empty := mkStore xH Tempty. - -Definition push a S := -mkStore (Psucc (index S)) (Tadd (index S) a (contents S)). - -Definition get i S := Tget i (contents S). - -Lemma get_empty : forall i, get i empty = PNone. -intro i; case i; unfold empty,get; simpl;reflexivity. -Qed. - -Inductive Full : Store -> Type:= - F_empty : Full empty - | F_push : forall a S, Full S -> Full (push a S). - -Theorem get_Full_Gt : forall S, Full S -> - forall i, (i ?= index S) Eq = Gt -> get i S = PNone. -intros S W;induction W. -unfold empty,index,get,contents;intros;apply Tget_Tempty. -unfold index,get,push;simpl contents. -intros i e;rewrite Tget_Tadd. -rewrite (Gt_Psucc _ _ e). -unfold get in IHW. -apply IHW;apply Gt_Psucc;assumption. -Qed. - -Theorem get_Full_Eq : forall S, Full S -> get (index S) S = PNone. -intros [index0 contents0] F. -case F. -unfold empty,index,get,contents;intros;apply Tget_Tempty. -unfold index,get,push;simpl contents. -intros a S. -rewrite Tget_Tadd. -rewrite Psucc_Gt. -intro W. -change (get (Psucc (index S)) S =PNone). -apply get_Full_Gt; auto. -apply Psucc_Gt. -Qed. - -Theorem get_push_Full : - forall i a S, Full S -> - get i (push a S) = - match (i ?= index S) Eq with - Eq => PSome a - | Lt => get i S - | Gt => PNone -end. -intros i a S F. -caseq ((i ?= index S) Eq). -intro e;rewrite (Pcompare_Eq_eq _ _ e). -destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd. -rewrite Pcompare_refl;reflexivity. -intros;destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd. -simpl index in H;rewrite H;reflexivity. -intro H;generalize H;clear H. -unfold get,push;simpl index;simpl contents. -rewrite Tget_Tadd;intro e;rewrite e. -change (get i S=PNone). -apply get_Full_Gt;auto. -Qed. - -Lemma Full_push_compat : forall i a S, Full S -> -forall x, get i S = PSome x -> - get i (push a S) = PSome x. -intros i a S F x H. -caseq ((i ?= index S) Eq);intro test. -rewrite (Pcompare_Eq_eq _ _ test) in H. -rewrite (get_Full_Eq _ F) in H;congruence. -rewrite <- H. -rewrite (get_push_Full i a). -rewrite test;reflexivity. -assumption. -rewrite (get_Full_Gt _ F) in H;congruence. -Qed. - -Lemma Full_index_one_empty : forall S, Full S -> index S = 1 -> S=empty. -intros [ind cont] F one; inversion F. -reflexivity. -simpl index in one;assert (h:=Psucc_not_one (index S)). -congruence. -Qed. - -Lemma push_not_empty: forall a S, (push a S) <> empty. -intros a [ind cont];unfold push,empty. -simpl;intro H;injection H; intros _ ; apply Psucc_not_one. -Qed. - -Fixpoint In (x:A) (S:Store) (F:Full S) {struct F}: Prop := -match F with -F_empty => False -| F_push a SS FF => x=a \/ In x SS FF -end. - -Lemma get_In : forall (x:A) (S:Store) (F:Full S) i , -get i S = PSome x -> In x S F. -induction F. -intro i;rewrite get_empty; congruence. -intro i;rewrite get_push_Full;trivial. -caseq ((i ?= index S) Eq);simpl. -left;congruence. -right;eauto. -congruence. -Qed. - -End Store. - -Implicit Arguments PNone [A]. -Implicit Arguments PSome [A]. - -Implicit Arguments Tempty [A]. -Implicit Arguments Branch0 [A]. -Implicit Arguments Branch1 [A]. - -Implicit Arguments Tget [A]. -Implicit Arguments Tadd [A]. - -Implicit Arguments Tget_Tempty [A]. -Implicit Arguments Tget_Tadd [A]. - -Implicit Arguments mkStore [A]. -Implicit Arguments index [A]. -Implicit Arguments contents [A]. - -Implicit Arguments empty [A]. -Implicit Arguments get [A]. -Implicit Arguments push [A]. - -Implicit Arguments get_empty [A]. -Implicit Arguments get_push_Full [A]. - -Implicit Arguments Full [A]. -Implicit Arguments F_empty [A]. -Implicit Arguments F_push [A]. -Implicit Arguments In [A]. - -Section Map. - -Variables A B:Set. - -Variable f: A -> B. - -Fixpoint Tmap (T: Tree A) : Tree B := -match T with -Tempty => Tempty -| Branch0 t1 t2 => Branch0 (Tmap t1) (Tmap t2) -| Branch1 a t1 t2 => Branch1 (f a) (Tmap t1) (Tmap t2) -end. - -Lemma Tget_Tmap: forall T i, -Tget i (Tmap T)= match Tget i T with PNone => PNone -| PSome a => PSome (f a) end. -induction T;intro i;case i;simpl;auto. -Defined. - -Lemma Tmap_Tadd: forall i a T, -Tmap (Tadd i a T) = Tadd i (f a) (Tmap T). -induction i;intros a T;case T;simpl;intros;try (rewrite IHi);simpl;reflexivity. -Defined. - -Definition map (S:Store A) : Store B := -mkStore (index S) (Tmap (contents S)). - -Lemma get_map: forall i S, -get i (map S)= match get i S with PNone => PNone -| PSome a => PSome (f a) end. -destruct S;unfold get,map,contents,index;apply Tget_Tmap. -Defined. - -Lemma map_push: forall a S, -map (push a S) = push (f a) (map S). -intros a S. -case S. -unfold push,map,contents,index. -intros;rewrite Tmap_Tadd;reflexivity. -Defined. - -Theorem Full_map : forall S, Full S -> Full (map S). -intros S F. -induction F. -exact F_empty. -rewrite map_push;constructor 2;assumption. -Defined. - -End Map. - -Implicit Arguments Tmap [A B]. -Implicit Arguments map [A B]. -Implicit Arguments Full_map [A B f]. - -Notation "hyps \ A" := (push A hyps) (at level 72,left associativity). 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. -*) diff --git a/contrib/rtauto/g_rtauto.ml4 b/contrib/rtauto/g_rtauto.ml4 deleted file mode 100644 index d7bb6e31..00000000 --- a/contrib/rtauto/g_rtauto.ml4 +++ /dev/null @@ -1,16 +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: g_rtauto.ml4 7734 2005-12-26 14:06:51Z herbelin $*) - -(*i camlp4deps: "parsing/grammar.cma" i*) - -TACTIC EXTEND rtauto - [ "rtauto" ] -> [ Refl_tauto.rtauto_tac ] -END - diff --git a/contrib/rtauto/proof_search.ml b/contrib/rtauto/proof_search.ml deleted file mode 100644 index 98643e0f..00000000 --- a/contrib/rtauto/proof_search.ml +++ /dev/null @@ -1,546 +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: proof_search.ml 7233 2005-07-15 12:34:56Z corbinea $ *) - -open Term -open Util -open Goptions - -type s_info= - {mutable created_steps : int; (* node count*) - mutable pruned_steps : int; - mutable created_branches : int; (* path count *) - mutable pruned_branches : int; - mutable created_hyps : int; (* hyps count *) - mutable pruned_hyps : int; - mutable branch_failures : int; - mutable branch_successes : int; - mutable nd_branching : int} - -let s_info= - {created_steps = 0; (* node count*) - pruned_steps = 0; - created_branches = 0; (* path count *) - pruned_branches = 0; - created_hyps = 0; (* hyps count *) - pruned_hyps = 0; - branch_failures = 0; - branch_successes = 0; - nd_branching = 0} - -let reset_info () = - s_info.created_steps <- 0; (* node count*) - s_info.pruned_steps <- 0; - s_info.created_branches <- 0; (* path count *) - s_info.pruned_branches <- 0; - s_info.created_hyps <- 0; (* hyps count *) - s_info.pruned_hyps <- 0; - s_info.branch_failures <- 0; - s_info.branch_successes <- 0; - s_info.nd_branching <- 0 - -let pruning = ref true - -let opt_pruning= - {optsync=true; - optname="Rtauto Pruning"; - optkey=SecondaryTable("Rtauto","Pruning"); - optread=(fun () -> !pruning); - optwrite=(fun b -> pruning:=b)} - -let _ = declare_bool_option opt_pruning - -type form= - Atom of int - | Arrow of form * form - | Bot - | Conjunct of form * form - | Disjunct of form * form - -type tag=int - -let decomp_form=function - Atom i -> Some (i,[]) - | Arrow (f1,f2) -> Some (-1,[f1;f2]) - | Bot -> Some (-2,[]) - | Conjunct (f1,f2) -> Some (-3,[f1;f2]) - | Disjunct (f1,f2) -> Some (-4,[f1;f2]) - -module Fmap=Map.Make(struct type t=form let compare=compare end) - -type sequent = - {rev_hyps: form Intmap.t; - norev_hyps: form Intmap.t; - size:int; - left:int Fmap.t; - right:(int*form) list Fmap.t; - cnx:(int*int*form*form) list; - abs:int option; - gl:form} - -let add_one_arrow i f1 f2 m= - try Fmap.add f1 ((i,f2)::(Fmap.find f1 m)) m with - Not_found -> - Fmap.add f1 [i,f2] m - -type proof = - Ax of int - | I_Arrow of proof - | E_Arrow of int*int*proof - | D_Arrow of int*proof*proof - | E_False of int - | I_And of proof*proof - | E_And of int*proof - | D_And of int*proof - | I_Or_l of proof - | I_Or_r of proof - | E_Or of int*proof*proof - | D_Or of int*proof - | Pop of int*proof - -type rule = - SAx of int - | SI_Arrow - | SE_Arrow of int*int - | SD_Arrow of int - | SE_False of int - | SI_And - | SE_And of int - | SD_And of int - | SI_Or_l - | SI_Or_r - | SE_Or of int - | SD_Or of int - -let add_step s sub = - match s,sub with - SAx i,[] -> Ax i - | SI_Arrow,[p] -> I_Arrow p - | SE_Arrow(i,j),[p] -> E_Arrow (i,j,p) - | SD_Arrow i,[p1;p2] -> D_Arrow (i,p1,p2) - | SE_False i,[] -> E_False i - | SI_And,[p1;p2] -> I_And(p1,p2) - | SE_And i,[p] -> E_And(i,p) - | SD_And i,[p] -> D_And(i,p) - | SI_Or_l,[p] -> I_Or_l p - | SI_Or_r,[p] -> I_Or_r p - | SE_Or i,[p1;p2] -> E_Or(i,p1,p2) - | SD_Or i,[p] -> D_Or(i,p) - | _,_ -> anomaly "add_step: wrong arity" - -type 'a with_deps = - {dep_it:'a; - dep_goal:bool; - dep_hyps:Intset.t} - -type slice= - {proofs_done:proof list; - proofs_todo:sequent with_deps list; - step:rule; - needs_goal:bool; - needs_hyps:Intset.t; - changes_goal:bool; - creates_hyps:Intset.t} - -type state = - Complete of proof - | Incomplete of sequent * slice list - -let project = function - Complete prf -> prf - | Incomplete (_,_) -> anomaly "not a successful state" - -let pop n prf = - let nprf= - match prf.dep_it with - Pop (i,p) -> Pop (i+n,p) - | p -> Pop(n,p) in - {prf with dep_it = nprf} - -let rec fill stack proof = - match stack with - [] -> Complete proof.dep_it - | slice::super -> - if - !pruning && - slice.proofs_done=[] && - not (slice.changes_goal && proof.dep_goal) && - not (Intset.exists - (fun i -> Intset.mem i proof.dep_hyps) - slice.creates_hyps) - then - begin - s_info.pruned_steps<-s_info.pruned_steps+1; - s_info.pruned_branches<- s_info.pruned_branches + - List.length slice.proofs_todo; - let created_here=Intset.cardinal slice.creates_hyps in - s_info.pruned_hyps<-s_info.pruned_hyps+ - List.fold_left - (fun sum dseq -> sum + Intset.cardinal dseq.dep_hyps) - created_here slice.proofs_todo; - fill super (pop (Intset.cardinal slice.creates_hyps) proof) - end - else - let dep_hyps= - Intset.union slice.needs_hyps - (Intset.diff proof.dep_hyps slice.creates_hyps) in - let dep_goal= - slice.needs_goal || - ((not slice.changes_goal) && proof.dep_goal) in - let proofs_done= - proof.dep_it::slice.proofs_done in - match slice.proofs_todo with - [] -> - fill super {dep_it = - add_step slice.step (List.rev proofs_done); - dep_goal = dep_goal; - dep_hyps = dep_hyps} - | current::next -> - let nslice= - {proofs_done=proofs_done; - proofs_todo=next; - step=slice.step; - needs_goal=dep_goal; - needs_hyps=dep_hyps; - changes_goal=current.dep_goal; - creates_hyps=current.dep_hyps} in - Incomplete (current.dep_it,nslice::super) - -let append stack (step,subgoals) = - s_info.created_steps<-s_info.created_steps+1; - match subgoals with - [] -> - s_info.branch_successes<-s_info.branch_successes+1; - fill stack {dep_it=add_step step.dep_it []; - dep_goal=step.dep_goal; - dep_hyps=step.dep_hyps} - | hd :: next -> - s_info.created_branches<- - s_info.created_branches+List.length next; - let slice= - {proofs_done=[]; - proofs_todo=next; - step=step.dep_it; - needs_goal=step.dep_goal; - needs_hyps=step.dep_hyps; - changes_goal=hd.dep_goal; - creates_hyps=hd.dep_hyps} in - Incomplete(hd.dep_it,slice::stack) - -let embed seq= - {dep_it=seq; - dep_goal=false; - dep_hyps=Intset.empty} - -let change_goal seq gl= - {seq with - dep_it={seq.dep_it with gl=gl}; - dep_goal=true} - -let add_hyp seqwd f= - s_info.created_hyps<-s_info.created_hyps+1; - let seq=seqwd.dep_it in - let num = seq.size+1 in - let left = Fmap.add f num seq.left in - let cnx,right= - try - let l=Fmap.find f seq.right in - List.fold_right (fun (i,f0) l0 -> (num,i,f,f0)::l0) l seq.cnx, - Fmap.remove f seq.right - with Not_found -> seq.cnx,seq.right in - let nseq= - match f with - Bot -> - {seq with - left=left; - right=right; - size=num; - abs=Some num; - cnx=cnx} - | Atom _ -> - {seq with - size=num; - left=left; - right=right; - cnx=cnx} - | Conjunct (_,_) | Disjunct (_,_) -> - {seq with - rev_hyps=Intmap.add num f seq.rev_hyps; - size=num; - left=left; - right=right; - cnx=cnx} - | Arrow (f1,f2) -> - let ncnx,nright= - try - let i = Fmap.find f1 seq.left in - (i,num,f1,f2)::cnx,right - with Not_found -> - cnx,(add_one_arrow num f1 f2 right) in - match f1 with - Conjunct (_,_) | Disjunct (_,_) -> - {seq with - rev_hyps=Intmap.add num f seq.rev_hyps; - size=num; - left=left; - right=nright; - cnx=ncnx} - | Arrow(_,_) -> - {seq with - norev_hyps=Intmap.add num f seq.norev_hyps; - size=num; - left=left; - right=nright; - cnx=ncnx} - | _ -> - {seq with - size=num; - left=left; - right=nright; - cnx=ncnx} in - {seqwd with - dep_it=nseq; - dep_hyps=Intset.add num seqwd.dep_hyps} - -exception Here_is of (int*form) - -let choose m= - try - Intmap.iter (fun i f -> raise (Here_is (i,f))) m; - raise Not_found - with - Here_is (i,f) -> (i,f) - - -let search_or seq= - match seq.gl with - Disjunct (f1,f2) -> - [{dep_it = SI_Or_l; - dep_goal = true; - dep_hyps = Intset.empty}, - [change_goal (embed seq) f1]; - {dep_it = SI_Or_r; - dep_goal = true; - dep_hyps = Intset.empty}, - [change_goal (embed seq) f2]] - | _ -> [] - -let search_norev seq= - let goals=ref (search_or seq) in - let add_one i f= - match f with - Arrow (Arrow (f1,f2),f3) -> - let nseq = - {seq with norev_hyps=Intmap.remove i seq.norev_hyps} in - goals:= - ({dep_it=SD_Arrow(i); - dep_goal=false; - dep_hyps=Intset.singleton i}, - [add_hyp - (add_hyp - (change_goal (embed nseq) f2) - (Arrow(f2,f3))) - f1; - add_hyp (embed nseq) f3]):: !goals - | _ -> anomaly "search_no_rev: can't happen" in - Intmap.iter add_one seq.norev_hyps; - List.rev !goals - -let search_in_rev_hyps seq= - try - let i,f=choose seq.rev_hyps in - let make_step step= - {dep_it=step; - dep_goal=false; - dep_hyps=Intset.singleton i} in - let nseq={seq with rev_hyps=Intmap.remove i seq.rev_hyps} in - match f with - Conjunct (f1,f2) -> - [make_step (SE_And(i)), - [add_hyp (add_hyp (embed nseq) f1) f2]] - | Disjunct (f1,f2) -> - [make_step (SE_Or(i)), - [add_hyp (embed nseq) f1;add_hyp (embed nseq) f2]] - | Arrow (Conjunct (f1,f2),f0) -> - [make_step (SD_And(i)), - [add_hyp (embed nseq) (Arrow (f1,Arrow (f2,f0)))]] - | Arrow (Disjunct (f1,f2),f0) -> - [make_step (SD_Or(i)), - [add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]] - | _ -> anomaly "search_in_rev_hyps: can't happen" - with - Not_found -> search_norev seq - -let search_rev seq= - match seq.cnx with - (i,j,f1,f2)::next -> - let nseq= - match f1 with - Conjunct (_,_) | Disjunct (_,_) -> - {seq with cnx=next; - rev_hyps=Intmap.remove j seq.rev_hyps} - | Arrow (_,_) -> - {seq with cnx=next; - norev_hyps=Intmap.remove j seq.norev_hyps} - | _ -> - {seq with cnx=next} in - [{dep_it=SE_Arrow(i,j); - dep_goal=false; - dep_hyps=Intset.add i (Intset.singleton j)}, - [add_hyp (embed nseq) f2]] - | [] -> - match seq.gl with - Arrow (f1,f2) -> - [{dep_it=SI_Arrow; - dep_goal=true; - dep_hyps=Intset.empty}, - [add_hyp (change_goal (embed seq) f2) f1]] - | Conjunct (f1,f2) -> - [{dep_it=SI_And; - dep_goal=true; - dep_hyps=Intset.empty},[change_goal (embed seq) f1; - change_goal (embed seq) f2]] - | _ -> search_in_rev_hyps seq - -let search_all seq= - match seq.abs with - Some i -> - [{dep_it=SE_False (i); - dep_goal=false; - dep_hyps=Intset.singleton i},[]] - | None -> - try - let ax = Fmap.find seq.gl seq.left in - [{dep_it=SAx (ax); - dep_goal=true; - dep_hyps=Intset.singleton ax},[]] - with Not_found -> search_rev seq - -let bare_sequent = embed - {rev_hyps=Intmap.empty; - norev_hyps=Intmap.empty; - size=0; - left=Fmap.empty; - right=Fmap.empty; - cnx=[]; - abs=None; - gl=Bot} - -let init_state hyps gl= - let init = change_goal bare_sequent gl in - let goal=List.fold_right (fun (_,f,_) seq ->add_hyp seq f) hyps init in - Incomplete (goal.dep_it,[]) - -let success= function - Complete _ -> true - | Incomplete (_,_) -> false - -let branching = function - Incomplete (seq,stack) -> - check_for_interrupt (); - let successors = search_all seq in - let _ = - match successors with - [] -> s_info.branch_failures<-s_info.branch_failures+1 - | _::next -> - s_info.nd_branching<-s_info.nd_branching+List.length next in - List.map (append stack) successors - | Complete prf -> anomaly "already succeeded" - -open Pp - -let rec pp_form = - function - Arrow(f1,f2) -> (pp_or f1) ++ (str " -> ") ++ (pp_form f2) - | f -> pp_or f -and pp_or = function - Disjunct(f1,f2) -> - (pp_or f1) ++ (str " \\/ ") ++ (pp_and f2) - | f -> pp_and f -and pp_and = function - Conjunct(f1,f2) -> - (pp_and f1) ++ (str " /\\ ") ++ (pp_atom f2) - | f -> pp_atom f -and pp_atom= function - Bot -> str "#" - | Atom n -> int n - | f -> str "(" ++ hv 2 (pp_form f) ++ str ")" - -let pr_form f = msg (pp_form f) - -let pp_intmap map = - let pp=ref (str "") in - Intmap.iter (fun i obj -> pp:= (!pp ++ - pp_form obj ++ cut ())) map; - str "{ " ++ v 0 (!pp) ++ str " }" - -let pp_list pp_obj l= -let pp=ref (str "") in - List.iter (fun o -> pp := !pp ++ (pp_obj o) ++ str ", ") l; - str "[ " ++ !pp ++ str "]" - -let pp_mapint map = - let pp=ref (str "") in - Fmap.iter (fun obj l -> pp:= (!pp ++ - pp_form obj ++ str " => " ++ - pp_list (fun (i,f) -> pp_form f) l ++ - cut ()) ) map; - str "{ " ++ vb 0 ++ (!pp) ++ str " }" ++ close () - -let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2 - -let pp_gl gl= cut () ++ - str "{ " ++ vb 0 ++ - begin - match gl.abs with - None -> str "" - | Some i -> str "ABSURD" ++ cut () - end ++ - str "rev =" ++ pp_intmap gl.rev_hyps ++ cut () ++ - str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++ - str "arrows=" ++ pp_mapint gl.right ++ cut () ++ - str "cnx =" ++ pp_list pp_connect gl.cnx ++ cut () ++ - str "goal =" ++ pp_form gl.gl ++ str " }" ++ close () - -let pp = - function - Incomplete(gl,ctx) -> msgnl (pp_gl gl) - | _ -> msg (str "<complete>") - -let pp_info () = - let count_info = - if !pruning then - str "Proof steps : " ++ - int s_info.created_steps ++ str " created / " ++ - int s_info.pruned_steps ++ str " pruned" ++ fnl () ++ - str "Proof branches : " ++ - int s_info.created_branches ++ str " created / " ++ - int s_info.pruned_branches ++ str " pruned" ++ fnl () ++ - str "Hypotheses : " ++ - int s_info.created_hyps ++ str " created / " ++ - int s_info.pruned_hyps ++ str " pruned" ++ fnl () - else - str "Pruning is off" ++ fnl () ++ - str "Proof steps : " ++ - int s_info.created_steps ++ str " created" ++ fnl () ++ - str "Proof branches : " ++ - int s_info.created_branches ++ str " created" ++ fnl () ++ - str "Hypotheses : " ++ - int s_info.created_hyps ++ str " created" ++ fnl () in - msgnl - ( str "Proof-search statistics :" ++ fnl () ++ - count_info ++ - str "Branch ends: " ++ - int s_info.branch_successes ++ str " successes / " ++ - int s_info.branch_failures ++ str " failures" ++ fnl () ++ - str "Non-deterministic choices : " ++ - int s_info.nd_branching ++ str " branches") - - - diff --git a/contrib/rtauto/proof_search.mli b/contrib/rtauto/proof_search.mli deleted file mode 100644 index eb11aeae..00000000 --- a/contrib/rtauto/proof_search.mli +++ /dev/null @@ -1,49 +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: proof_search.mli 7233 2005-07-15 12:34:56Z corbinea $ *) - -type form= - Atom of int - | Arrow of form * form - | Bot - | Conjunct of form * form - | Disjunct of form * form - -type proof = - Ax of int - | I_Arrow of proof - | E_Arrow of int*int*proof - | D_Arrow of int*proof*proof - | E_False of int - | I_And of proof*proof - | E_And of int*proof - | D_And of int*proof - | I_Or_l of proof - | I_Or_r of proof - | E_Or of int*proof*proof - | D_Or of int*proof - | Pop of int*proof - -type state - -val project: state -> proof - -val init_state : ('a * form * 'b) list -> form -> state - -val branching: state -> state list - -val success: state -> bool - -val pp: state -> unit - -val pr_form : form -> unit - -val reset_info : unit -> unit - -val pp_info : unit -> unit diff --git a/contrib/rtauto/refl_tauto.ml b/contrib/rtauto/refl_tauto.ml deleted file mode 100644 index 81256f4a..00000000 --- a/contrib/rtauto/refl_tauto.ml +++ /dev/null @@ -1,337 +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: refl_tauto.ml 10478 2008-01-29 10:31:39Z notin $ *) - -module Search = Explore.Make(Proof_search) - -open Util -open Term -open Termops -open Names -open Evd -open Tacmach -open Proof_search - -let force count lazc = incr count;Lazy.force lazc - -let step_count = ref 0 - -let node_count = ref 0 - -let logic_constant = - Coqlib.gen_constant "refl_tauto" ["Init";"Logic"] - -let li_False = lazy (destInd (logic_constant "False")) -let li_and = lazy (destInd (logic_constant "and")) -let li_or = lazy (destInd (logic_constant "or")) - -let data_constant = - Coqlib.gen_constant "refl_tauto" ["Init";"Datatypes"] - -let l_true_equals_true = - lazy (mkApp(logic_constant "refl_equal", - [|data_constant "bool";data_constant "true"|])) - -let pos_constant = - Coqlib.gen_constant "refl_tauto" ["NArith";"BinPos"] - -let l_xI = lazy (pos_constant "xI") -let l_xO = lazy (pos_constant "xO") -let l_xH = lazy (pos_constant "xH") - -let store_constant = - Coqlib.gen_constant "refl_tauto" ["rtauto";"Bintree"] - -let l_empty = lazy (store_constant "empty") -let l_push = lazy (store_constant "push") - -let constant= - Coqlib.gen_constant "refl_tauto" ["rtauto";"Rtauto"] - -let l_Reflect = lazy (constant "Reflect") - -let l_Atom = lazy (constant "Atom") -let l_Arrow = lazy (constant "Arrow") -let l_Bot = lazy (constant "Bot") -let l_Conjunct = lazy (constant "Conjunct") -let l_Disjunct = lazy (constant "Disjunct") - -let l_Ax = lazy (constant "Ax") -let l_I_Arrow = lazy (constant "I_Arrow") -let l_E_Arrow = lazy (constant "E_Arrow") -let l_D_Arrow = lazy (constant "D_Arrow") -let l_E_False = lazy (constant "E_False") -let l_I_And = lazy (constant "I_And") -let l_E_And = lazy (constant "E_And") -let l_D_And = lazy (constant "D_And") -let l_I_Or_l = lazy (constant "I_Or_l") -let l_I_Or_r = lazy (constant "I_Or_r") -let l_E_Or = lazy (constant "E_Or") -let l_D_Or = lazy (constant "D_Or") - - -let special_whd gl= - let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in - (fun t -> Closure.whd_val infos (Closure.inject t)) - -let special_nf gl= - let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in - (fun t -> Closure.norm_val infos (Closure.inject t)) - -type atom_env= - {mutable next:int; - mutable env:(constr*int) list} - -let make_atom atom_env term= - try - let (_,i)= - List.find (fun (t,_)-> eq_constr term t) atom_env.env - in Atom i - with Not_found -> - let i=atom_env.next in - atom_env.env <- (term,i)::atom_env.env; - atom_env.next<- i + 1; - Atom i - -let rec make_form atom_env gls term = - let normalize=special_nf gls in - let cciterm=special_whd gls term in - match kind_of_term cciterm with - Prod(_,a,b) -> - if not (dependent (mkRel 1) b) && - Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) a = InProp - then - let fa=make_form atom_env gls a in - let fb=make_form atom_env gls b in - Arrow (fa,fb) - else - make_atom atom_env (normalize term) - | Cast(a,_,_) -> - make_form atom_env gls a - | Ind ind -> - if ind = Lazy.force li_False then - Bot - else - make_atom atom_env (normalize term) - | App(hd,argv) when Array.length argv = 2 -> - begin - try - let ind = destInd hd in - if ind = Lazy.force li_and then - let fa=make_form atom_env gls argv.(0) in - let fb=make_form atom_env gls argv.(1) in - Conjunct (fa,fb) - else if ind = Lazy.force li_or then - let fa=make_form atom_env gls argv.(0) in - let fb=make_form atom_env gls argv.(1) in - Disjunct (fa,fb) - else make_atom atom_env (normalize term) - with Invalid_argument _ -> make_atom atom_env (normalize term) - end - | _ -> make_atom atom_env (normalize term) - -let rec make_hyps atom_env gls lenv = function - [] -> [] - | (_,Some body,typ)::rest -> - make_hyps atom_env gls (typ::body::lenv) rest - | (id,None,typ)::rest -> - let hrec= - make_hyps atom_env gls (typ::lenv) rest in - if List.exists (dependent (mkVar id)) lenv || - (Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) typ <> InProp) - then - hrec - else - (id,make_form atom_env gls typ)::hrec - -let rec build_pos n = - if n<=1 then force node_count l_xH - else if n land 1 = 0 then - mkApp (force node_count l_xO,[|build_pos (n asr 1)|]) - else - mkApp (force node_count l_xI,[|build_pos (n asr 1)|]) - -let rec build_form = function - Atom n -> mkApp (force node_count l_Atom,[|build_pos n|]) - | Arrow (f1,f2) -> - mkApp (force node_count l_Arrow,[|build_form f1;build_form f2|]) - | Bot -> force node_count l_Bot - | Conjunct (f1,f2) -> - mkApp (force node_count l_Conjunct,[|build_form f1;build_form f2|]) - | Disjunct (f1,f2) -> - mkApp (force node_count l_Disjunct,[|build_form f1;build_form f2|]) - -let rec decal k = function - [] -> k - | (start,delta)::rest -> - if k>start then - k - delta - else - decal k rest - -let add_pop size d pops= - match pops with - [] -> [size+d,d] - | (_,sum)::_ -> (size+sum,sum+d)::pops - -let rec build_proof pops size = - function - Ax i -> - mkApp (force step_count l_Ax, - [|build_pos (decal i pops)|]) - | I_Arrow p -> - mkApp (force step_count l_I_Arrow, - [|build_proof pops (size + 1) p|]) - | E_Arrow(i,j,p) -> - mkApp (force step_count l_E_Arrow, - [|build_pos (decal i pops); - build_pos (decal j pops); - build_proof pops (size + 1) p|]) - | D_Arrow(i,p1,p2) -> - mkApp (force step_count l_D_Arrow, - [|build_pos (decal i pops); - build_proof pops (size + 2) p1; - build_proof pops (size + 1) p2|]) - | E_False i -> - mkApp (force step_count l_E_False, - [|build_pos (decal i pops)|]) - | I_And(p1,p2) -> - mkApp (force step_count l_I_And, - [|build_proof pops size p1; - build_proof pops size p2|]) - | E_And(i,p) -> - mkApp (force step_count l_E_And, - [|build_pos (decal i pops); - build_proof pops (size + 2) p|]) - | D_And(i,p) -> - mkApp (force step_count l_D_And, - [|build_pos (decal i pops); - build_proof pops (size + 1) p|]) - | I_Or_l(p) -> - mkApp (force step_count l_I_Or_l, - [|build_proof pops size p|]) - | I_Or_r(p) -> - mkApp (force step_count l_I_Or_r, - [|build_proof pops size p|]) - | E_Or(i,p1,p2) -> - mkApp (force step_count l_E_Or, - [|build_pos (decal i pops); - build_proof pops (size + 1) p1; - build_proof pops (size + 1) p2|]) - | D_Or(i,p) -> - mkApp (force step_count l_D_Or, - [|build_pos (decal i pops); - build_proof pops (size + 2) p|]) - | Pop(d,p) -> - build_proof (add_pop size d pops) size p - -let build_env gamma= - List.fold_right (fun (p,_) e -> - mkApp(force node_count l_push,[|mkProp;p;e|])) - gamma.env (mkApp (force node_count l_empty,[|mkProp|])) - -open Goptions - -let verbose = ref false - -let opt_verbose= - {optsync=true; - optname="Rtauto Verbose"; - optkey=SecondaryTable("Rtauto","Verbose"); - optread=(fun () -> !verbose); - optwrite=(fun b -> verbose:=b)} - -let _ = declare_bool_option opt_verbose - -let check = ref false - -let opt_check= - {optsync=true; - optname="Rtauto Check"; - optkey=SecondaryTable("Rtauto","Check"); - optread=(fun () -> !check); - optwrite=(fun b -> check:=b)} - -let _ = declare_bool_option opt_check - -open Pp - -let rtauto_tac gls= - Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"]; - let gamma={next=1;env=[]} in - let gl=gls.it.evar_concl in - let _= - if Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) gl <> InProp - then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in - let glf=make_form gamma gls gl in - let hyps=make_hyps gamma gls [gl] - (Environ.named_context_of_val gls.it.evar_hyps) in - let formula= - List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in - let search_fun = - if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then - Search.debug_depth_first - else - Search.depth_first in - let _ = - begin - reset_info (); - if !verbose then - msgnl (str "Starting proof-search ..."); - end in - let search_start_time = System.get_time () in - let prf = - try project (search_fun (init_state [] formula)) - with Not_found -> - errorlabstrm "rtauto" (Pp.str "rtauto couldn't find any proof") in - let search_end_time = System.get_time () in - let _ = if !verbose then - begin - msgnl (str "Proof tree found in " ++ - System.fmt_time_difference search_start_time search_end_time); - pp_info (); - msgnl (str "Building proof term ... ") - end in - let build_start_time=System.get_time () in - let _ = step_count := 0; node_count := 0 in - let main = mkApp (force node_count l_Reflect, - [|build_env gamma; - build_form formula; - build_proof [] 0 prf|]) in - let term= - Term.applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in - let build_end_time=System.get_time () in - let _ = if !verbose then - begin - msgnl (str "Proof term built in " ++ - System.fmt_time_difference build_start_time build_end_time ++ - fnl () ++ - str "Proof size : " ++ int !step_count ++ - str " steps" ++ fnl () ++ - str "Proof term size : " ++ int (!step_count+ !node_count) ++ - str " nodes (constants)" ++ fnl () ++ - str "Giving proof term to Coq ... ") - end in - let tac_start_time = System.get_time () in - let result= - if !check then - Tactics.exact_check term gls - else - Tactics.exact_no_check term gls in - let tac_end_time = System.get_time () in - let _ = - if !check then msgnl (str "Proof term type-checking is on"); - if !verbose then - msgnl (str "Internal tactic executed in " ++ - System.fmt_time_difference tac_start_time tac_end_time) in - result - diff --git a/contrib/rtauto/refl_tauto.mli b/contrib/rtauto/refl_tauto.mli deleted file mode 100644 index 480dbb30..00000000 --- a/contrib/rtauto/refl_tauto.mli +++ /dev/null @@ -1,26 +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: refl_tauto.mli 7233 2005-07-15 12:34:56Z corbinea $ *) - -(* raises Not_found if no proof is found *) - -type atom_env= - {mutable next:int; - mutable env:(Term.constr*int) list} - -val make_form : atom_env -> - Proof_type.goal Tacmach.sigma -> Term.types -> Proof_search.form - -val make_hyps : - atom_env -> - Proof_type.goal Tacmach.sigma -> - Term.types list -> - (Names.identifier * Term.types option * Term.types) list -> - (Names.identifier * Proof_search.form) list - -val rtauto_tac : Proof_type.tactic |