From 7d220f8b61649646692983872626d6a8042446a9 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 20 Mar 2009 01:22:58 +0000 Subject: Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/rtauto/Bintree.v | 489 +++++++++++++++++++++++++++++++++ plugins/rtauto/Rtauto.v | 400 +++++++++++++++++++++++++++ plugins/rtauto/g_rtauto.ml4 | 16 ++ plugins/rtauto/proof_search.ml | 546 +++++++++++++++++++++++++++++++++++++ plugins/rtauto/proof_search.mli | 49 ++++ plugins/rtauto/refl_tauto.ml | 337 +++++++++++++++++++++++ plugins/rtauto/refl_tauto.mli | 26 ++ plugins/rtauto/rtauto_plugin.mllib | 3 + 8 files changed, 1866 insertions(+) create mode 100644 plugins/rtauto/Bintree.v create mode 100644 plugins/rtauto/Rtauto.v create mode 100644 plugins/rtauto/g_rtauto.ml4 create mode 100644 plugins/rtauto/proof_search.ml create mode 100644 plugins/rtauto/proof_search.mli create mode 100644 plugins/rtauto/refl_tauto.ml create mode 100644 plugins/rtauto/refl_tauto.mli create mode 100644 plugins/rtauto/rtauto_plugin.mllib (limited to 'plugins/rtauto') diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v new file mode 100644 index 000000000..cd0f1afe9 --- /dev/null +++ b/plugins/rtauto/Bintree.v @@ -0,0 +1,489 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (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/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v new file mode 100644 index 000000000..4b95097e2 --- /dev/null +++ b/plugins/rtauto/Rtauto.v @@ -0,0 +1,400 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 new file mode 100644 index 000000000..4cbe84368 --- /dev/null +++ b/plugins/rtauto/g_rtauto.ml4 @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [ Refl_tauto.rtauto_tac ] +END + diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml new file mode 100644 index 000000000..9d9d66bb2 --- /dev/null +++ b/plugins/rtauto/proof_search.ml @@ -0,0 +1,546 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* !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 "") + +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/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli new file mode 100644 index 000000000..a0e86b8d6 --- /dev/null +++ b/plugins/rtauto/proof_search.mli @@ -0,0 +1,49 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml new file mode 100644 index 000000000..6cde1ddcf --- /dev/null +++ b/plugins/rtauto/refl_tauto.ml @@ -0,0 +1,337 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli new file mode 100644 index 000000000..a6d68a226 --- /dev/null +++ b/plugins/rtauto/refl_tauto.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + 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 diff --git a/plugins/rtauto/rtauto_plugin.mllib b/plugins/rtauto/rtauto_plugin.mllib new file mode 100644 index 000000000..61c5e945b --- /dev/null +++ b/plugins/rtauto/rtauto_plugin.mllib @@ -0,0 +1,3 @@ +Proof_search +Refl_tauto +G_rtauto -- cgit v1.2.3