summaryrefslogtreecommitdiff
path: root/theories/Init
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init')
-rw-r--r--theories/Init/Datatypes.v2
-rw-r--r--theories/Init/Logic_Type.v2
-rw-r--r--theories/Init/Notations.v8
-rw-r--r--theories/Init/Peano.v3
-rw-r--r--theories/Init/Prelude.v1
-rw-r--r--theories/Init/Specif.v3
-rw-r--r--theories/Init/Tactics.v8
-rw-r--r--theories/Init/Tauto.v101
-rw-r--r--theories/Init/Wf.v2
-rw-r--r--theories/Init/vo.itarget3
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-25 07:05:53 +0000