aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tactics/Tauto.v15
-rw-r--r--tactics/tacticals.mli1
-rw-r--r--tactics/tauto.ml465
-rw-r--r--theories/Reals/Rbase.v97
4 files changed, 104 insertions, 74 deletions
diff --git a/tactics/Tauto.v b/tactics/Tauto.v
index e6b8b5e835..d4fafc277f 100644
--- a/tactics/Tauto.v
+++ b/tactics/Tauto.v
@@ -12,8 +12,19 @@ Declare ML Module "tauto".
Grammar tactic simple_tactic: ast :=
tauto [ "Tauto" ] -> [(Tauto)]
-| intuition [ "Intuition" ] -> [(Intuition)].
+| intuition [ "Intuition" ] -> [(Intuition)]
+| intuition_t [ "Intuition" tactic($t) ] -> [(Intuition (TACTIC $t))]
+(*
+| intuitionnr [ "Intuitionnr"] -> [(Intuitionnr)]
+| intuitionr [ "Intuitionr"] -> [(Intuitionr)]
+| intuitionnr_t [ "Intuitionnr" tactic($t) ] -> [(Intuitionnr (TACTIC $t))]
+| intuitionr_t [ "Intuitionr" tactic($t) ] -> [(Intuitionr (TACTIC $t))]
+| intsimplif [ "IntSimplif" ] -> [(IntSimplif)]
+| intreduce [ "IntReduce" ] -> [(IntReduce)]
+*)
+.
Syntax tactic level 0:
tauto [(Tauto)] -> ["Tauto"]
-| intuition [(Intuition)] -> ["Intuition"].
+| intuition [(Intuition)] -> ["Intuition"]
+| intuition_t [<<(Intuition $t)>>] -> ["Intuition" $t].
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 7693e7f777..90cb04f3ea 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -32,6 +32,7 @@ val tclTHENSi : tactic -> tactic list -> (int -> tactic) -> tactic
val tclTHENSEQ : tactic list -> tactic
val tclREPEAT : tactic -> tactic
val tclFIRST : tactic list -> tactic
+val tclSOLVE : tactic list -> tactic
val tclTRY : tactic -> tactic
val tclINFO : tactic -> tactic
val tclCOMPLETE : tactic -> tactic
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 5421d46a45..cfe768acb7 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -103,7 +103,8 @@ let rec tauto_intuit t_reduce t_solver ist =
$t_is_disj;Solve [Left;$t_tauto_intuit | Right;$t_tauto_intuit]
)
Orelse
- (Intro;$t_tauto_intuit)
+ (* NB: [|- ? -> ?] matches any product *)
+ (Match Context With |[ |- ? -> ? ] -> Intro;$t_tauto_intuit)
Orelse
$t_solver
) >>
@@ -121,6 +122,8 @@ let unfold_not_iff = function
let reduction_not_iff = Tacticals.onAllClauses (fun ido -> unfold_not_iff ido)
+let no_reduction = tclIDTAC
+
(* Reduce until finding atoms in head normal form *)
open Term
open Termops
@@ -129,7 +132,7 @@ open Environ
let rec reduce env sigma c =
let c = Tacred.hnf_constr env sigma c in
match Term.kind_of_term c with
- | Prod (na,t,u) when noccurn 1 u ->
+ | Prod (na,t,u) (* when noccurn 1 u*) ->
mkProd (na,reduce env sigma t, reduce (push_rel (na,None,t) env) sigma u)
| _ -> c
@@ -137,6 +140,7 @@ let reduction =
Tacticals.onAllClauses
(fun cl -> reduct_option reduce (option_app (fun id -> InHyp id) cl))
+let t_no_reduction = valueIn (VTactic no_reduction)
let t_reduction = valueIn (VTactic reduction)
let t_reduction_not_iff = valueIn (VTactic reduction_not_iff)
@@ -152,12 +156,65 @@ let tauto g =
(* ) *)
g
with UserError _ -> errorlabstrm "tauto" [< str "Tauto failed" >]
-
+(*
let intuition =
(* tclTHEN init_intros*)
(tclORELSE
(interp (tacticIn (intuition_main t_reduction_not_iff)))
(interp (tacticIn (intuition_main t_reduction))))
+*)
+
+let intuition_not_reducing tac =
+ interp (tacticIn (tauto_intuit t_no_reduction tac))
+
+let intuition_reducing tac =
+ interp (tacticIn (tauto_intuit t_reduction tac))
+
+let intuition_reducing_not_iff tac =
+ interp (tacticIn (tauto_intuit t_reduction_not_iff tac))
+
+(* Idea: we want to destructure the goal and the hyps but we do not
+ want to unfold constants unless we can solve the obtained goals.
+ Moreover, we need to unfold "not" and "iff" in order to solve all
+ propositionnal tautologies but we should do it only if necessary;
+ otherwise, if tac=Auto, it may fail to recognize that a given goal
+ is an instance of one of its Hints *)
+let intuition_gen tac =
+ let tnored = tclSOLVE [ intuition_not_reducing tac ]
+ and tr = tclTRY (tclSOLVE [ intuition_reducing tac ])
+ and trnotiff = intuition_reducing_not_iff tac in
+ tclORELSE tnored
+ (tclORELSE
+ (tclTHEN trnotiff tr)
+ tr
+ )
+
+let v_intuition args =
+ match args with
+ | [] -> intuition_gen <:tactic< Auto with * >>
+ | [ Tac(_, t)] -> intuition_gen t
+ | _ -> assert false
+
+let v_intuitnred args =
+ match args with
+ | [] -> intuition_not_reducing <:tactic< Auto with * >>
+ | [ Tac(_, t)] -> intuition_not_reducing t
+ | _ -> assert false
+
+let v_intuitred args =
+ match args with
+ | [] -> intuition_reducing <:tactic< Auto with * >>
+ | [ Tac(_, t)] -> intuition_reducing t
+ | _ -> assert false
+
+let _ = hide_atomic_tactic "IntSimplif" (interp (tacticIn (simplif t_reduction_not_iff)))
+let _ = hide_atomic_tactic "IntReduce" (interp (tacticIn (simplif t_reduction_not_iff)))
let _ = hide_atomic_tactic "Tauto" tauto
-let _ = hide_atomic_tactic "Intuition" intuition
+(* let _ = hide_atomic_tactic "Intuition" intuition*)
+let _ = hide_tactic "Intuition" v_intuition
+
+let _ = hide_tactic "Intuitionr" v_intuitred
+let _ = hide_tactic "Intuitionnr" v_intuitnred
+
+
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index 3554915608..c1f0feb9ad 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -47,7 +47,7 @@ Add Field R Rplus Rmult R1 R0 Ropp [x,y:R]false Rinv RTheory Rinv_l
(**********)
Lemma Rlt_antirefl:(r:R)~``r<r``.
- Red; Intros; Apply (Rlt_antisym r r H); Auto with zarith real.
+ Generalize Rlt_antisym. Intuition EAuto.
Save.
Hints Resolve Rlt_antirefl : real.
@@ -62,9 +62,7 @@ Save.
(**********)
Lemma imp_not_Req:(r1,r2:R)(``r1<r2``\/ ``r1>r2``) -> ``r1<>r2``.
-Intros r1 r2 [H|H].
-Apply Rlt_not_eq; Auto with real.
-Apply Rgt_not_eq; Auto with real.
+Generalize Rlt_not_eq Rgt_not_eq. Intuition EAuto.
Save.
Hints Resolve imp_not_Req : real.
@@ -72,24 +70,18 @@ Hints Resolve imp_not_Req : real.
(**********)
Lemma Req_EM:(r1,r2:R)(r1==r2)\/``r1<>r2``.
-Intros;Elim (total_order_T r1 r2);Intro.
-Case a; Auto with real.
-Auto with real.
+Intros ; Generalize (total_order_T r1 r2) ; Intuition EAuto with real.
Save.
Hints Resolve Req_EM : real.
(**********)
Lemma total_order:(r1,r2:R)``r1<r2``\/(r1==r2)\/``r1>r2``.
-Intros;Elim (total_order_T r1 r2);Intro;Auto.
-Elim a;Intro;Auto.
+Intros;Generalize (total_order_T r1 r2);Tauto.
Save.
(**********)
Lemma not_Req:(r1,r2:R)``r1<>r2``->(``r1<r2``\/``r1>r2``).
-Intros; Case (total_order r1 r2); Intros; Auto with real.
-Case H0; Intros.
-Absurd r1==r2; Auto with real.
-Auto with real.
+Intros; Generalize (total_order_T r1 r2) ; Tauto.
Save.
@@ -99,7 +91,7 @@ Save.
(**********)
Lemma Rlt_le:(r1,r2:R)``r1<r2``-> ``r1<=r2``.
-Unfold Rle; Auto.
+Intuition Auto.
Save.
Hints Resolve Rlt_le : real.
@@ -115,19 +107,14 @@ Save.
(**********)
Lemma not_Rle:(r1,r2:R)~(``r1<=r2``)->``r1>r2``.
-Intros; Unfold Rle in H; Elim (total_order r1 r2); Intro.
-Elim H;Left; Assumption.
-Elim H0; Intro;Auto.
-Elim H;Right; Assumption.
+Intros r1 r2 ; Generalize (total_order r1 r2) ; Tauto.
Save.
Hints Immediate Rle_ge Rge_le not_Rle : real.
(**********)
Lemma Rlt_le_not:(r1,r2:R)``r2<r1``->~(``r1<=r2``).
-Intros; Red; Intro; Elim H0; Clear H0; Intro.
-Exact (Rlt_antisym r1 r2 H0 H).
-Case (imp_not_Req r1 r2); Auto with real.
+Intros r1 r2 ; Generalize (Rlt_antisym r1 r2) (imp_not_Req r1 r2) ; Intuition.
Save.
Lemma Rle_not:(r1,r2:R)``r1>r2`` -> ~(``r1<=r2``).
@@ -136,27 +123,24 @@ Proof Rlt_le_not.
Hints Immediate Rlt_le_not : real.
Lemma Rle_not_lt: (r1, r2:R) ``r2 <= r1`` ->~ (``r1<r2``).
-Intros r1 r2 H'; Elim H';Auto with real.
-Intro H; Rewrite H; Auto with real.
+Intros r1 r2. Generalize (Rlt_antisym r1 r2) (imp_not_Req r1 r2); Intuition.
Save.
(**********)
Lemma Rlt_ge_not:(r1,r2:R)``r1<r2``->~(``r1>=r2``).
-Unfold Rge; Red; Intros.
-Apply (Rlt_le_not r2 r1 H).
-Red; Case H0; Auto with real.
+Generalize Rlt_le_not. Intuition EAuto 3.
Save.
Hints Immediate Rlt_ge_not : real.
(**********)
Lemma eq_Rle:(r1,r2:R)r1==r2->``r1<=r2``.
-Unfold Rle; Auto.
+Unfold Rle; Tauto.
Save.
Hints Immediate eq_Rle : real.
Lemma eq_Rge:(r1,r2:R)r1==r2->``r1>=r2``.
-Unfold Rge; Auto.
+Unfold Rge; Tauto.
Save.
Hints Immediate eq_Rge : real.
@@ -171,78 +155,58 @@ Save.
Hints Immediate eq_Rge_sym : real.
Lemma Rle_antisym : (r1,r2:R)``r1<=r2`` -> ``r2<=r1``-> r1==r2.
-Unfold Rle; Intros.
-Case H; Intro; Auto with real.
-Case H0; Intro; Auto with real.
-Case (Rlt_antisym r1 r2 H1 H2).
+Intros r1 r2; Generalize (Rlt_antisym r1 r2) ; Intuition.
Save.
Hints Resolve Rle_antisym : real.
(**********)
Lemma Rle_le_eq:(r1,r2:R)(``r1<=r2``/\``r2<=r1``)<->(r1==r2).
-Split; Auto with real.
-Intros (H1,H2); Auto with real.
+Intuition.
+Save.
+
+Lemma Rlt_rew : (x,x',y,y':R)``x==x'``->``x'<y'`` -> `` y' == y`` -> ``x < y``.
+Intros; Replace x with x'; Replace y with y'; Assumption.
Save.
(**********)
Lemma Rle_trans:(r1,r2,r3:R) ``r1<=r2``->``r2<=r3``->``r1<=r3``.
-Intros r1 r2 r3; Unfold Rle; Intros.
-Elim H; Elim H0; Intros.
-Left; Apply Rlt_trans with r2; Trivial.
-Left; Rewrite <- H1; Trivial.
-Left; Rewrite H2; Trivial.
-Right; Transitivity r2; Trivial.
+Generalize trans_eqT Rlt_trans Rlt_rew.
+Intuition EAuto 2.
Save.
(**********)
Lemma Rle_lt_trans:(r1,r2,r3:R)``r1<=r2``->``r2<r3``->``r1<r3``.
-Intros; Unfold Rle in H; Elim H; Intro.
-Apply (Rlt_trans r1 r2 r3 H1 H0).
-Rewrite -> H1; Auto with zarith real.
+Generalize Rlt_trans Rlt_rew. Intuition EAuto 2.
Save.
(**********)
Lemma Rlt_le_trans:(r1,r2,r3:R)``r1<r2``->``r2<=r3``->``r1<r3``.
-Intros; Unfold Rle in H0; Elim H0; Intro.
-Apply (Rlt_trans r1 r2 r3 H H1).
-Rewrite <- H1; Auto with zarith real.
+Generalize Rlt_trans Rlt_rew; Intuition EAuto 2.
Save.
(** Decidability of the order *)
Lemma total_order_Rlt:(r1,r2:R)(sumboolT ``r1<r2`` ~(``r1<r2``)).
-Intros;Elim (total_order_T r1 r2);Intros.
-Elim a;Intro.
-Left;Assumption.
-Right;Rewrite b;Apply Rlt_antirefl.
-Right;Unfold Rgt in b;Apply Rlt_antisym;Assumption.
+Intros;Generalize (total_order_T r1 r2) (imp_not_Req r1 r2) ; Intuition.
Save.
(**********)
Lemma total_order_Rle:(r1,r2:R)(sumboolT ``r1<=r2`` ~(``r1<=r2``)).
-Intros;Elim (total_order_T r1 r2);Intros.
-Left;Unfold Rle;Elim a;Auto with real.
-Right; Auto with real.
+Intros r1 r2; Generalize (total_order_T r1 r2);Intuition EAuto with real.
Save.
(**********)
Lemma total_order_Rgt:(r1,r2:R)(sumboolT ``r1>r2`` ~(``r1>r2``)).
-Unfold Rgt;Intros;Apply total_order_Rlt.
+Intros;Unfold Rgt;Intros;Apply total_order_Rlt.
Save.
(**********)
Lemma total_order_Rge:(r1,r2:R)(sumboolT (``r1>=r2``) ~(``r1>=r2``)).
-Intros;Elim (total_order_Rle r2 r1);Intro.
-Left; Auto with real.
-Right; Auto with real.
+Intros;Generalize (total_order_Rle r2 r1);Intuition.
Save.
Lemma total_order_Rlt_Rle:(r1,r2:R)(sumboolT ``r1<r2`` ``r2<=r1``).
-Intros;Elim (total_order_T r1 r2); Intro H.
-Case H; Intro.
-Left; Trivial.
-Right; Auto with real.
-Right; Auto with real.
+Intros;Generalize (total_order_T r1 r2); Intuition.
Save.
Lemma Rle_or_lt: (n, m:R)(Rle n m) \/ (Rlt m n).
@@ -251,15 +215,12 @@ Save.
Lemma total_order_Rle_Rlt_eq :(r1,r2:R)``r1<=r2``->
(sumboolT ``r1<r2`` ``r1==r2``).
-Intros r1 r2 H;Elim (total_order_T r1 r2); Trivial; Intro.
-Elim (Rlt_le_not r1 r2); Trivial.
+Intros r1 r2 H;Generalize (total_order_T r1 r2); Intuition.
Save.
(**********)
Lemma inser_trans_R:(n,m,p,q:R)``n<=m<p``-> (sumboolT ``n<=m<q`` ``q<=m<p``).
-Intros n m p q H; Case (total_order_Rlt_Rle m q); Intro.
-Left; Case H; Auto.
-Right; Case H; Auto.
+Intros; Generalize (total_order_Rlt_Rle m q); Intuition.
Save.
(****************************************************************)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 23:49:30 +0000