diff options
Diffstat (limited to 'theories/Init')
-rw-r--r-- | theories/Init/Datatypes.v | 2 | ||||
-rw-r--r-- | theories/Init/Logic_Type.v | 2 | ||||
-rw-r--r-- | theories/Init/Notations.v | 8 | ||||
-rw-r--r-- | theories/Init/Peano.v | 3 | ||||
-rw-r--r-- | theories/Init/Prelude.v | 1 | ||||
-rw-r--r-- | theories/Init/Specif.v | 3 | ||||
-rw-r--r-- | theories/Init/Tactics.v | 8 | ||||
-rw-r--r-- | theories/Init/Tauto.v | 101 | ||||
-rw-r--r-- | theories/Init/Wf.v | 2 | ||||
-rw-r--r-- | theories/Init/vo.itarget | 3 |
10 files changed, 117 insertions, 16 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 4850c9ca..ddaf08bf 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -151,6 +151,7 @@ Inductive option (A:Type) : Type := | Some : A -> option A | None : option A. +Arguments Some {A} a. Arguments None {A}. Definition option_map (A B:Type) (f:A->B) (o : option A) : option B := @@ -225,6 +226,7 @@ Inductive list (A : Type) : Type := | cons : A -> list A -> list A. Arguments nil {A}. +Arguments cons {A} a l. Infix "::" := cons (at level 60, right associativity) : list_scope. Delimit Scope list_scope with list. Bind Scope list_scope with list. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 4a5f2ad6..4536dfc0 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -64,7 +64,7 @@ Definition identity_rect_r : intros A x P H y H0; case identity_sym with (1 := H0); trivial. Defined. -Hint Immediate identity_sym not_identity_sym: core v62. +Hint Immediate identity_sym not_identity_sym: core. Notation refl_id := identity_refl (compat "8.3"). Notation sym_id := identity_sym (compat "8.3"). diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index ab6bf472..48fbe079 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -76,17 +76,21 @@ Reserved Notation "{ x : A & P }" (at level 0, x at level 99). Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99). Delimit Scope type_scope with type. +Delimit Scope function_scope with function. Delimit Scope core_scope with core. +Bind Scope type_scope with Sortclass. +Bind Scope function_scope with Funclass. + Open Scope core_scope. +Open Scope function_scope. Open Scope type_scope. (** ML Tactic Notations *) Declare ML Module "coretactics". Declare ML Module "extratactics". -Declare ML Module "eauto". +Declare ML Module "g_auto". Declare ML Module "g_class". Declare ML Module "g_eqdecide". Declare ML Module "g_rewrite". -Declare ML Module "tauto". diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 3749baf6..6c4a6350 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -33,7 +33,6 @@ Open Scope nat_scope. Definition eq_S := f_equal S. Definition f_equal_nat := f_equal (A:=nat). -Hint Resolve eq_S: v62. Hint Resolve f_equal_nat: core. (** The predecessor function *) @@ -41,7 +40,6 @@ Hint Resolve f_equal_nat: core. Notation pred := Nat.pred (compat "8.4"). Definition f_equal_pred := f_equal pred. -Hint Resolve f_equal_pred: v62. Theorem pred_Sn : forall n:nat, n = pred (S n). Proof. @@ -85,7 +83,6 @@ Notation plus := Nat.add (compat "8.4"). Infix "+" := Nat.add : nat_scope. Definition f_equal2_plus := f_equal2 plus. -Hint Resolve f_equal2_plus: v62. Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat). Hint Resolve f_equal2_nat: core. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 04a263ad..03f2328d 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -15,6 +15,7 @@ Require Coq.Init.Nat. Require Export Peano. Require Export Coq.Init.Wf. Require Export Coq.Init.Tactics. +Require Export Coq.Init.Tauto. (* Initially available plugins (+ nat_syntax_plugin loaded in Datatypes) *) Declare ML Module "extraction_plugin". diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 6c022185..9fc00e80 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -9,6 +9,7 @@ (** Basic specifications : sets that may contain logical information *) Set Implicit Arguments. +Set Reversible Pattern Implicit. Require Import Notations. Require Import Datatypes. @@ -298,7 +299,7 @@ Proof. apply (h2 h1). Defined. -Hint Resolve left right inleft inright: core v62. +Hint Resolve left right inleft inright: core. Hint Resolve exist exist2 existT existT2: core. (* Compatibility *) diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 59fdbb42..5d1e87ae 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -55,12 +55,6 @@ Ltac contradict H := | _ => (elim H;fail) || pos H end. -(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*) - -Ltac swap H := - idtac "swap is OBSOLETE: use contradict instead."; - intro; apply H; clear H. - (* To contradict an hypothesis without copying its type. *) Ltac absurd_hyp H := @@ -79,7 +73,7 @@ Ltac case_eq x := generalize (eq_refl x); pattern x at -1; case x. (* use either discriminate or injection on a hypothesis *) -Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)). +Ltac destr_eq H := discriminate H || (try (injection H as H)). (* Similar variants of destruct *) diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v new file mode 100644 index 00000000..1e409607 --- /dev/null +++ b/theories/Init/Tauto.v @@ -0,0 +1,101 @@ +Require Import Notations. +Require Import Datatypes. +Require Import Logic. + +Local Declare ML Module "tauto". + +Local Ltac not_dep_intros := + repeat match goal with + | |- (forall (_: ?X1), ?X2) => intro + | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1; intro + end. + +Local Ltac axioms flags := + match reverse goal with + | |- ?X1 => is_unit_or_eq flags X1; constructor 1 + | _:?X1 |- _ => is_empty flags X1; elimtype X1; assumption + | _:?X1 |- ?X1 => assumption + end. + +Local Ltac simplif flags := + not_dep_intros; + repeat + (match reverse goal with + | id: ?X1 |- _ => is_conj flags X1; elim id; do 2 intro; clear id + | id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id + | id: (Coq.Init.Logic.not _) |- _ => red in id + | id: ?X1 |- _ => is_disj flags X1; elim id; intro; clear id + | id0: (forall (_: ?X1), ?X2), id1: ?X1|- _ => + (* generalize (id0 id1); intro; clear id0 does not work + (see Marco Maggiesi's bug PR#301) + so we instead use Assert and exact. *) + assert X2; [exact (id0 id1) | clear id0] + | id: forall (_ : ?X1), ?X2|- _ => + is_unit_or_eq flags X1; cut X2; + [ intro; clear id + | (* id : forall (_: ?X1), ?X2 |- ?X2 *) + cut X1; [exact id| constructor 1; fail] + ] + | id: forall (_ : ?X1), ?X2|- _ => + flatten_contravariant_conj flags X1 X2 id + (* moved from "id:(?A/\?B)->?X2|-" to "?A->?B->?X2|-" *) + | id: forall (_: Coq.Init.Logic.iff ?X1 ?X2), ?X3|- _ => + assert (forall (_: forall _:X1, X2), forall (_: forall _: X2, X1), X3) + by (do 2 intro; apply id; split; assumption); + clear id + | id: forall (_:?X1), ?X2|- _ => + flatten_contravariant_disj flags X1 X2 id + (* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2,?B->?X2|-" *) + | |- ?X1 => is_conj flags X1; split + | |- (Coq.Init.Logic.iff _ _) => split + | |- (Coq.Init.Logic.not _) => red + end; + not_dep_intros). + +Local Ltac tauto_intuit flags t_reduce t_solver := + let rec t_tauto_intuit := + (simplif flags; axioms flags + || match reverse goal with + | id:forall(_: forall (_: ?X1), ?X2), ?X3|- _ => + cut X3; + [ intro; clear id; t_tauto_intuit + | cut (forall (_: X1), X2); + [ exact id + | generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id; + solve [ t_tauto_intuit ]]] + | id:forall (_:not ?X1), ?X3|- _ => + cut X3; + [ intro; clear id; t_tauto_intuit + | cut (not X1); [ exact id | clear id; intro; solve [t_tauto_intuit ]]] + | |- ?X1 => + is_disj flags X1; solve [left;t_tauto_intuit | right;t_tauto_intuit] + end + || + (* NB: [|- _ -> _] matches any product *) + match goal with | |- forall (_ : _), _ => intro; t_tauto_intuit + | |- _ => t_reduce;t_solver + end + || + t_solver + ) in t_tauto_intuit. + +Local Ltac intuition_gen flags solver := tauto_intuit flags reduction_not_iff solver. +Local Ltac tauto_intuitionistic flags := intuition_gen flags fail || fail "tauto failed". +Local Ltac tauto_classical flags := + (apply_nnpp || fail "tauto failed"); (tauto_intuitionistic flags || fail "Classical tauto failed"). +Local Ltac tauto_gen flags := tauto_intuitionistic flags || tauto_classical flags. + +Ltac tauto := with_uniform_flags ltac:(fun flags => tauto_gen flags). +Ltac dtauto := with_power_flags ltac:(fun flags => tauto_gen flags). + +Ltac intuition := with_uniform_flags ltac:(fun flags => intuition_gen flags ltac:(auto with *)). +Local Ltac intuition_then tac := with_uniform_flags ltac:(fun flags => intuition_gen flags tac). + +Ltac dintuition := with_power_flags ltac:(fun flags => intuition_gen flags ltac:(auto with *)). +Local Ltac dintuition_then tac := with_power_flags ltac:(fun flags => intuition_gen flags tac). + +Tactic Notation "intuition" := intuition. +Tactic Notation "intuition" tactic(t) := intuition_then t. + +Tactic Notation "dintuition" := dintuition. +Tactic Notation "dintuition" tactic(t) := dintuition_then t. diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 985ecaf2..b5b17e5e 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -34,7 +34,7 @@ Section Well_founded. destruct 1; trivial. Defined. - Global Implicit Arguments Acc_inv [x y] [x]. + Global Arguments Acc_inv [x] _ [y] _, [x] _ y _. (** A relation is well-founded if every element is accessible *) diff --git a/theories/Init/vo.itarget b/theories/Init/vo.itarget index cc62e66c..99877065 100644 --- a/theories/Init/vo.itarget +++ b/theories/Init/vo.itarget @@ -7,4 +7,5 @@ Prelude.vo Specif.vo Tactics.vo Wf.vo -Nat.vo
\ No newline at end of file +Nat.vo +Tauto.vo |