summaryrefslogtreecommitdiff
path: root/tactics/eqdecide.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/eqdecide.ml4')
-rw-r--r--tactics/eqdecide.ml497
1 files changed, 51 insertions, 46 deletions
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 8edfcb3e..9cbc549f 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -14,7 +14,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: eqdecide.ml4,v 1.6.2.1 2004/07/16 19:30:53 herbelin Exp $ *)
+(* $Id: eqdecide.ml4 8652 2006-03-22 08:27:14Z herbelin $ *)
open Util
open Names
@@ -46,11 +46,11 @@ open Coqlib
2. Try discrimination to solve those goals where x and y has
been introduced by different constructors.
3. If x and y have been introduced by the same constructor,
- then analyse one by one the correspoing pairs of arguments.
+ then analyse one by one the corresponding pairs of arguments.
If they are equal, rewrite one into the other. If they are
not, derive a contradiction from the injectiveness of the
constructor.
- 4. Once all the arguments have been rewritten, solve the left half
+ 4. Once all the arguments have been rewritten, solve the remaining half
of the disjunction by reflexivity.
Eduardo Gimenez (30/3/98).
@@ -58,35 +58,36 @@ open Coqlib
let clear_last = (tclLAST_HYP (fun c -> (clear [destVar c])))
-let mkBranches =
+let choose_eq eqonleft =
+ if eqonleft then h_simplest_left else h_simplest_right
+let choose_noteq eqonleft =
+ if eqonleft then h_simplest_right else h_simplest_left
+
+let mkBranches c1 c2 =
tclTHENSEQ
- [intro;
- tclLAST_HYP h_simplest_elim;
- clear_last;
- intros ;
+ [generalize [c2];
+ h_simplest_elim c1;
+ intros;
tclLAST_HYP h_simplest_case;
clear_last;
intros]
-let solveRightBranch =
- tclTHEN h_simplest_right
+let solveNoteqBranch side =
+ tclTHEN (choose_noteq side)
(tclTHEN (intro_force true)
(onLastHyp (fun id -> Extratactics.h_discrHyp (Rawterm.NamedHyp id))))
-let h_solveRightBranch =
- Refiner.abstract_extended_tactic "solveRightBranch" [] solveRightBranch
-
-(*
-let h_solveRightBranch =
- hide_atomic_tactic "solveRightBranch" solveRightBranch
-*)
+let h_solveNoteqBranch side =
+ Refiner.abstract_extended_tactic "solveNoteqBranch" []
+ (solveNoteqBranch side)
(* Constructs the type {c1=c2}+{~c1=c2} *)
-let mkDecideEqGoal rectype c1 c2 g =
+let mkDecideEqGoal eqonleft op rectype c1 c2 g =
let equality = mkApp(build_coq_eq(), [|rectype; c1; c2|]) in
let disequality = mkApp(build_coq_not (), [|equality|]) in
- mkApp(build_coq_sumbool (), [|equality; disequality |])
+ if eqonleft then mkApp(op, [|equality; disequality |])
+ else mkApp(op, [|disequality; equality |])
(* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *)
@@ -97,42 +98,45 @@ let mkGenDecideEqGoal rectype g =
and yname = next_ident_away (id_of_string "y") hypnames in
(mkNamedProd xname rectype
(mkNamedProd yname rectype
- (mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g)))
+ (mkDecideEqGoal true (build_coq_sumbool ())
+ rectype (mkVar xname) (mkVar yname) g)))
-let eqCase tac =
+let eqCase tac =
(tclTHEN intro
(tclTHEN (tclLAST_HYP Extratactics.h_rewriteLR)
(tclTHEN clear_last
tac)))
-let diseqCase =
+let diseqCase eqonleft =
let diseq = id_of_string "diseq" in
let absurd = id_of_string "absurd" in
(tclTHEN (intro_using diseq)
- (tclTHEN h_simplest_right
+ (tclTHEN (choose_noteq eqonleft)
(tclTHEN red_in_concl
(tclTHEN (intro_using absurd)
(tclTHEN (h_simplest_apply (mkVar diseq))
(tclTHEN (Extratactics.h_injHyp (Rawterm.NamedHyp absurd))
- full_trivial))))))
+ (full_trivial [])))))))
-let solveArg a1 a2 tac g =
+let solveArg eqonleft op a1 a2 tac g =
let rectype = pf_type_of g a1 in
- let decide = mkDecideEqGoal rectype a1 a2 g in
- (tclTHENS
- (h_elim_type decide)
- [(eqCase tac);diseqCase;default_auto]) g
+ let decide = mkDecideEqGoal eqonleft op rectype a1 a2 g in
+ let subtacs =
+ if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto]
+ else [diseqCase eqonleft;eqCase tac;default_auto] in
+ (tclTHENS (h_elim_type decide) subtacs) g
-let solveLeftBranch rectype g =
+let solveEqBranch rectype g =
try
- let (lhs,rhs) = match_eqdec_partial (pf_concl g) in
+ let (eqonleft,op,lhs,rhs,_) = match_eqdec (pf_concl g) in
let (mib,mip) = Global.lookup_inductive rectype in
- let nparams = mip.mind_nparams in
+ let nparams = mib.mind_nparams in
let getargs l = list_skipn nparams (snd (decompose_app l)) in
let rargs = getargs rhs
and largs = getargs lhs in
List.fold_right2
- solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g
+ (solveArg eqonleft op) largs rargs
+ (tclTHEN (choose_eq eqonleft) h_reflexivity) g
with PatternMatchingFailure -> error "Unexpected conclusion!"
(* The tactic Decide Equality *)
@@ -143,31 +147,33 @@ let hd_app c = match kind_of_term c with
let decideGralEquality g =
try
- let typ = match_eqdec (pf_concl g) in
+ let eqonleft,_,c1,c2,typ = match_eqdec (pf_concl g) in
let headtyp = hd_app (pf_compute g typ) in
let rectype =
match kind_of_term headtyp with
| Ind mi -> mi
| _ -> error "This decision procedure only works for inductive objects"
- in
+ in
(tclTHEN
- mkBranches
- (tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g
+ (mkBranches c1 c2)
+ (tclORELSE (h_solveNoteqBranch eqonleft) (solveEqBranch rectype)))
+ g
with PatternMatchingFailure ->
- error "The goal does not have the expected form"
+ error "The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}"
+let decideEqualityGoal = tclTHEN intros decideGralEquality
let decideEquality c1 c2 g =
let rectype = (pf_type_of g c1) in
let decide = mkGenDecideEqGoal rectype g in
- (tclTHENS (cut decide) [default_auto;decideGralEquality]) g
+ (tclTHENS (cut decide) [default_auto;decideEqualityGoal]) g
(* The tactic Compare *)
let compare c1 c2 g =
let rectype = pf_type_of g c1 in
- let decide = mkDecideEqGoal rectype c1 c2 g in
+ let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 g in
(tclTHENS (cut decide)
[(tclTHEN intro
(tclTHEN (tclLAST_HYP simplest_case)
@@ -177,12 +183,11 @@ let compare c1 c2 g =
(* User syntax *)
-TACTIC EXTEND DecideEquality
- [ "Decide" "Equality" constr(c1) constr(c2) ] -> [ decideEquality c1 c2 ]
-| [ "Decide" "Equality" ] -> [ decideGralEquality ]
+TACTIC EXTEND decide_equality
+ [ "decide" "equality" constr(c1) constr(c2) ] -> [ decideEquality c1 c2 ]
+| [ "decide" "equality" ] -> [ decideEqualityGoal ]
END
-TACTIC EXTEND Compare
-| [ "Compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ]
+TACTIC EXTEND compare
+| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ]
END
-
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-17 01:52:39 +0000