diff options
Diffstat (limited to 'tactics/eqdecide.ml4')
| -rw-r--r-- | tactics/eqdecide.ml4 | 188 |
1 files changed, 0 insertions, 188 deletions
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 deleted file mode 100644 index 4a11d586..00000000 --- a/tactics/eqdecide.ml4 +++ /dev/null @@ -1,188 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(************************************************************************) -(* EqDecide *) -(* A tactic for deciding propositional equality on inductive types *) -(* by Eduardo Gimenez *) -(************************************************************************) - -(*i camlp4deps: "parsing/grammar.cma" i*) - -open Util -open Names -open Namegen -open Term -open Declarations -open Tactics -open Tacticals -open Hiddentac -open Equality -open Auto -open Pattern -open Matching -open Hipattern -open Proof_type -open Tacmach -open Coqlib - -(* This file containts the implementation of the tactics ``Decide - Equality'' and ``Compare''. They can be used to decide the - propositional equality of two objects that belongs to a small - inductive datatype --i.e., an inductive set such that all the - arguments of its constructors are non-functional sets. - - The procedure for proving (x,y:R){x=y}+{~x=y} can be scketched as - follows: - 1. Eliminate x and then y. - 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 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 remaining half - of the disjunction by reflexivity. - - Eduardo Gimenez (30/3/98). -*) - -let clear_last = (onLastHyp (fun c -> (clear [destVar c]))) - -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 - [generalize [c2]; - h_simplest_elim c1; - intros; - onLastHyp h_simplest_case; - clear_last; - intros] - -let solveNoteqBranch side = - tclTHEN (choose_noteq side) - (tclTHEN introf - (onLastHypId (fun id -> Extratactics.h_discrHyp id))) - -let h_solveNoteqBranch side = - Refiner.abstract_extended_tactic "solveNoteqBranch" [] - (solveNoteqBranch side) - -(* Constructs the type {c1=c2}+{~c1=c2} *) - -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 - if eqonleft then mkApp(op, [|equality; disequality |]) - else mkApp(op, [|disequality; equality |]) - - -(* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *) - -let mkGenDecideEqGoal rectype g = - let hypnames = pf_ids_of_hyps g in - let xname = next_ident_away (id_of_string "x") hypnames - and yname = next_ident_away (id_of_string "y") hypnames in - (mkNamedProd xname rectype - (mkNamedProd yname rectype - (mkDecideEqGoal true (build_coq_sumbool ()) - rectype (mkVar xname) (mkVar yname) g))) - -let eqCase tac = - (tclTHEN intro - (tclTHEN (onLastHyp Equality.rewriteLR) - (tclTHEN clear_last - tac))) - -let diseqCase eqonleft = - let diseq = id_of_string "diseq" in - let absurd = id_of_string "absurd" in - (tclTHEN (intro_using diseq) - (tclTHEN (choose_noteq eqonleft) - (tclTHEN red_in_concl - (tclTHEN (intro_using absurd) - (tclTHEN (h_simplest_apply (mkVar diseq)) - (tclTHEN (Extratactics.h_injHyp absurd) - (full_trivial []))))))) - -let solveArg eqonleft op a1 a2 tac g = - let rectype = pf_type_of g a1 in - 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 solveEqBranch rectype g = - try - let (eqonleft,op,lhs,rhs,_) = match_eqdec (pf_concl g) in - let (mib,mip) = Global.lookup_inductive rectype 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 eqonleft op) largs rargs - (tclTHEN (choose_eq eqonleft) h_reflexivity) g - with PatternMatchingFailure -> error "Unexpected conclusion!" - -(* The tactic Decide Equality *) - -let hd_app c = match kind_of_term c with - | App (h,_) -> h - | _ -> c - -let decideGralEquality g = - try - 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 - (tclTHEN - (mkBranches c1 c2) - (tclORELSE (h_solveNoteqBranch eqonleft) (solveEqBranch rectype))) - g - with PatternMatchingFailure -> - error "The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}." - -let decideEqualityGoal = tclTHEN intros decideGralEquality - -let decideEquality rectype g = - let decide = mkGenDecideEqGoal rectype g in - (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 true (build_coq_sumbool ()) rectype c1 c2 g in - (tclTHENS (cut decide) - [(tclTHEN intro - (tclTHEN (onLastHyp simplest_case) - clear_last)); - decideEquality (pf_type_of g c1)]) g - - -(* User syntax *) - -TACTIC EXTEND decide_equality -| [ "decide" "equality" ] -> [ decideEqualityGoal ] -END - -TACTIC EXTEND compare -| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ] -END |