aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend43
-rw-r--r--.depend.coq10
-rw-r--r--tactics/tauto.ml434
-rw-r--r--test-suite/success/Tauto.v9
4 files changed, 63 insertions, 33 deletions
diff --git a/.depend b/.depend
index 55e4b14bf..a660d5660 100644
--- a/.depend
+++ b/.depend
@@ -309,11 +309,10 @@ contrib/correctness/pwp.cmi: contrib/correctness/peffect.cmi \
contrib/extraction/common.cmi: contrib/extraction/miniml.cmi \
contrib/extraction/mlutil.cmi kernel/names.cmi library/nametab.cmi \
lib/pp.cmi
-contrib/extraction/extract_env.cmi: parsing/genarg.cmi kernel/names.cmi \
- library/nametab.cmi lib/util.cmi
-contrib/extraction/extraction.cmi: kernel/environ.cmi \
- contrib/extraction/miniml.cmi kernel/names.cmi library/nametab.cmi \
- kernel/term.cmi
+contrib/extraction/extract_env.cmi: kernel/names.cmi library/nametab.cmi \
+ lib/util.cmi
+contrib/extraction/extraction.cmi: contrib/extraction/miniml.cmi \
+ library/nametab.cmi
contrib/extraction/haskell.cmi: contrib/extraction/miniml.cmi \
kernel/names.cmi library/nametab.cmi lib/pp.cmi
contrib/extraction/miniml.cmi: kernel/names.cmi library/nametab.cmi \
@@ -1576,7 +1575,8 @@ toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi toplevel/class.cmi \
kernel/reduction.cmi proofs/refiner.cmi kernel/safe_typing.cmi \
library/states.cmi pretyping/syntax_def.cmi proofs/tacmach.cmi \
pretyping/tacred.cmi kernel/term.cmi pretyping/termops.cmi \
- kernel/typeops.cmi lib/util.cmi toplevel/command.cmi
+ kernel/typeops.cmi lib/util.cmi toplevel/vernacexpr.cmo \
+ toplevel/command.cmi
toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx toplevel/class.cmx \
parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \
kernel/environ.cmx pretyping/evd.cmx library/global.cmx \
@@ -1588,7 +1588,8 @@ toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx toplevel/class.cmx \
kernel/reduction.cmx proofs/refiner.cmx kernel/safe_typing.cmx \
library/states.cmx pretyping/syntax_def.cmx proofs/tacmach.cmx \
pretyping/tacred.cmx kernel/term.cmx pretyping/termops.cmx \
- kernel/typeops.cmx lib/util.cmx toplevel/command.cmi
+ kernel/typeops.cmx lib/util.cmx toplevel/vernacexpr.cmx \
+ toplevel/command.cmi
toplevel/coqinit.cmo: config/coq_config.cmi toplevel/mltop.cmi \
library/nameops.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
lib/system.cmi toplevel/toplevel.cmi toplevel/vernac.cmi \
@@ -2043,17 +2044,15 @@ contrib/extraction/common.cmx: library/declare.cmx \
lib/pp_control.cmx parsing/printer.cmx contrib/extraction/scheme.cmx \
contrib/extraction/table.cmx pretyping/termops.cmx lib/util.cmx \
contrib/extraction/common.cmi
-contrib/extraction/extract_env.cmo: parsing/astterm.cmi \
- contrib/extraction/common.cmi library/declare.cmi pretyping/evd.cmi \
- contrib/extraction/extraction.cmi library/global.cmi library/lib.cmi \
+contrib/extraction/extract_env.cmo: contrib/extraction/common.cmi \
+ library/declare.cmi contrib/extraction/extraction.cmi library/lib.cmi \
library/libobject.cmi library/library.cmi contrib/extraction/miniml.cmi \
contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \
library/nametab.cmi lib/pp.cmi contrib/extraction/table.cmi \
kernel/term.cmi lib/util.cmi toplevel/vernacinterp.cmi \
contrib/extraction/extract_env.cmi
-contrib/extraction/extract_env.cmx: parsing/astterm.cmx \
- contrib/extraction/common.cmx library/declare.cmx pretyping/evd.cmx \
- contrib/extraction/extraction.cmx library/global.cmx library/lib.cmx \
+contrib/extraction/extract_env.cmx: contrib/extraction/common.cmx \
+ library/declare.cmx contrib/extraction/extraction.cmx library/lib.cmx \
library/libobject.cmx library/library.cmx contrib/extraction/miniml.cmi \
contrib/extraction/mlutil.cmx library/nameops.cmx kernel/names.cmx \
library/nametab.cmx lib/pp.cmx contrib/extraction/table.cmx \
@@ -2123,15 +2122,17 @@ contrib/extraction/scheme.cmx: contrib/extraction/miniml.cmi \
library/nametab.cmx contrib/extraction/ocaml.cmx lib/options.cmx \
lib/pp.cmx contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \
contrib/extraction/scheme.cmi
-contrib/extraction/table.cmo: kernel/declarations.cmi parsing/extend.cmi \
- library/global.cmi library/goptions.cmi library/lib.cmi \
- library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
- parsing/printer.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \
+contrib/extraction/table.cmo: kernel/declarations.cmi kernel/environ.cmi \
+ parsing/extend.cmi library/global.cmi library/goptions.cmi \
+ library/lib.cmi library/libobject.cmi kernel/names.cmi \
+ library/nametab.cmi lib/pp.cmi parsing/printer.cmi kernel/reduction.cmi \
+ library/summary.cmi kernel/term.cmi lib/util.cmi \
toplevel/vernacinterp.cmi contrib/extraction/table.cmi
-contrib/extraction/table.cmx: kernel/declarations.cmx parsing/extend.cmx \
- library/global.cmx library/goptions.cmx library/lib.cmx \
- library/libobject.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
- parsing/printer.cmx library/summary.cmx kernel/term.cmx lib/util.cmx \
+contrib/extraction/table.cmx: kernel/declarations.cmx kernel/environ.cmx \
+ parsing/extend.cmx library/global.cmx library/goptions.cmx \
+ library/lib.cmx library/libobject.cmx kernel/names.cmx \
+ library/nametab.cmx lib/pp.cmx parsing/printer.cmx kernel/reduction.cmx \
+ library/summary.cmx kernel/term.cmx lib/util.cmx \
toplevel/vernacinterp.cmx contrib/extraction/table.cmi
contrib/field/field.cmo: parsing/astterm.cmi toplevel/cerrors.cmi \
parsing/coqast.cmi library/declare.cmi parsing/egrammar.cmi \
diff --git a/.depend.coq b/.depend.coq
index 29ffc37cc..0f4703012 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -30,12 +30,16 @@ theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/PolyList.
theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/PolyList.vo theories/Sets/Multiset.vo
theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo
theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v
-theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rsigma.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/Rgeom.vo theories/Reals/Rderiv.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rcomplet.vo theories/Reals/Alembert_compl.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Ranalysis.vo theories/Reals/DiscrR.vo theories/Reals/SplitRmult.vo theories/Reals/SplitAbsolu.vo
-theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rtrigo.vo
+theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/R_sqrt.vo theories/Reals/Rsigma.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/Rderiv.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rcomplet.vo theories/Reals/Alembert_compl.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Ranalysis.vo theories/Reals/DiscrR.vo theories/Reals/SplitRmult.vo theories/Reals/SplitAbsolu.vo
+theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Ranalysis4.vo
-theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo
+theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Sqrt_reg.vo
+theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rderiv.vo theories/Reals/R_sqr.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo
theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo
theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo contrib/omega/Omega.vo
+theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
+theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rsqrt_def.vo
+theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Rcomplet.vo theories/Reals/AltSeries.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cv_prop.vo theories/Reals/Ranalysis1.vo
theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo
theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rfunctions.vo theories/Reals/Rsigma.vo theories/Reals/Rlimit.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_plus.vo
theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Arith/Max.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Rprod.vo theories/Reals/Cv_prop.vo theories/Reals/Cos_rel.vo
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index a54b69360..f4f8452fa 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -57,7 +57,7 @@ let axioms ist =
and t_is_empty = tacticIn is_empty in
<:tactic<
Match Reverse Context With
- |[|- ?1] -> $t_is_unit;Constructor
+ |[|- ?1] -> $t_is_unit;Constructor 1
|[_:?1 |- ?] -> $t_is_empty
|[_:?1 |- ?1] -> Assumption>>
@@ -76,14 +76,28 @@ let simplif t_reduce ist =
| [id: (?1 ? ?) |- ?] -> $t_is_disj;Elim id;Intro;Clear id;$t_reduce
| [id0: ?1-> ?2; id1: ?1|- ?] -> Generalize (id0 id1);Intro;Clear id0
| [id: ?1 -> ?2|- ?] ->
- $t_is_unit;Cut ?2;[Intro;Clear id|Intros;Apply id;Constructor;Fail]
+ $t_is_unit;Cut ?2;
+ [Intro;Clear id
+ | (* id : ?1 -> ?2 |- ?2 *)
+ Cut ?1;[Exact id|Constructor 1;Fail]
+ ]
| [id: (?1 ?2 ?3) -> ?4|- ?] ->
- $t_is_conj;Cut ?2-> ?3-> ?4;[Intro;Clear id;$t_reduce|
- Intros;Apply id;Try Split;Assumption]
+ $t_is_conj;Cut ?2-> ?3-> ?4;
+ [Intro;Clear id;$t_reduce
+ | (* id: (?1 ?2 ?3) -> ?4 |- ?2 -> ?3 -> ?4 *)
+ Intro;Intro; Cut (?1 ?2 ?3);[Exact id|Split;Assumption]
+ ]
| [id: (?1 ?2 ?3) -> ?4|- ?] ->
- $t_is_disj;Cut ?3-> ?4;[Cut ?2-> ?4;[Intros;Clear id;$t_reduce|
- Intros;Apply id;
- Try Left;Assumption]|Intros;Apply id;Try Right;Assumption]
+ $t_is_disj;
+ Cut ?3-> ?4;
+ [Cut ?2-> ?4;
+ [Intro;Intro;Clear id;$t_reduce
+ | (* id: (?1 ?2 ?3) -> ?4 |- ?2 -> ?4 *)
+ Intro; Cut (?1 ?2 ?3);[Exact id|Left;Assumption]
+ ]
+ | (* id: (?1 ?2 ?3) -> ?4 |- ?3 -> ?4 *)
+ Intro; Cut (?1 ?2 ?3);[Exact id|Right;Assumption]
+ ]
| [|- (?1 ? ?)] -> $t_is_conj;Split;$t_reduce);
$t_not_dep_intros)>>
@@ -100,7 +114,7 @@ let rec tauto_intuit t_reduce t_solver ist =
| [id:(?1-> ?2)-> ?3|- ?] ->
Cut ?3;
[Intro;Clear id
- |Cut ?1 -> ?2;
+ | Cut ?1 -> ?2;
[Exact id|Generalize [y:?2](id [x:?1]y);Intro;Clear id]
]; Solve [ $t_tauto_intuit ]
| [|- (?1 ? ?)] ->
@@ -129,7 +143,9 @@ let simplif_gen = interp (tacticIn (simplif t_reduction_not_iff))
let tauto g =
try intuition_gen <:tactic<Fail>> g
- with UserError _ -> errorlabstrm "tauto" [< str "Tauto failed" >]
+ with
+ Refiner.FailError _ | UserError _ ->
+ errorlabstrm "tauto" [< str "Tauto failed" >]
let default_intuition_tac = <:tactic< Auto with * >>
diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index bbc67f669..3afe7a6bc 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -179,6 +179,13 @@ Proof.
Tauto.
Save.
+(* sometimes, the behaviour of Tauto depends on the order of the hyps *)
+Lemma old_bug3bis:
+ ~((A->B)->B)->((~B\/~B)/\(~B\/~A)/\(B\/~B)/\(B\/~A)->False)->False.
+Proof.
+ Tauto.
+Save.
+
(* A bug found by Freek Wiedijk <freek@cs.kun.nl> *)
Lemma new_bug:
((A<->B)->(B<->C)) ->
@@ -189,6 +196,7 @@ Proof.
Tauto.
Save.
+
(* A private club has the following rules :
*
* . rule 1 : Every non-scottish member wears red socks
@@ -229,3 +237,4 @@ Lemma intu1:((A:Prop)A\/~A)->(x,y:nat)(x=y\/~x=y).
Proof.
Intuition.
Save.
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 17:06:51 +0000