From edb21eab674b170d125a5b6fbc8213066b356d17 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 6 Apr 2017 10:10:03 +0200 Subject: Fixing "decide equality"'s bug #5449. The code was assuming that the terms t and u for which {t=u}+{t<>u} is proved were distinct. We refine an internal "generalize" of "u" so that it works on the two precise occurrences to abstract, even if other occurrences of u occur as subterm of t too. We also reuse the global constants found in the statement rather than reconstructing them (this seems better in case the global constants eventually get polymorphic universes?). --- tactics/eqdecide.ml | 57 ++++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 46 insertions(+), 11 deletions(-) (limited to 'tactics/eqdecide.ml') diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index bac3980d2..7d8b84f9c 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -67,9 +67,27 @@ let choose_noteq eqonleft = else left_with_bindings false Misctypes.NoBindings -let mkBranches c1 c2 = +open Sigma.Notations +open Context.Rel.Declaration + +(* A surgical generalize which selects the right occurrences by hand *) +(* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *) + +let generalize_right mk typ c1 c2 = + Proofview.Goal.enter { Proofview.Goal.enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let store = Proofview.Goal.extra gl in + Refine.refine ~unsafe:true { Sigma.run = begin fun sigma -> + let na = Name (next_name_away_with_default "x" Anonymous (Termops.ids_of_context env)) in + let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in + let Sigma (x, sigma, p) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in + Sigma (mkApp (x, [|c2|]), sigma, p) + end } + end } + +let mkBranches (eqonleft,mk,c1,c2,typ) = tclTHENLIST - [generalize [c2]; + [generalize_right mk typ c1 c2; Simple.elim c1; intros; onLastHyp Simple.case; @@ -145,15 +163,32 @@ let diseqCase hyps eqonleft = open Proofview.Notations -(* spiwack: a small wrapper around [Hipattern]. *) +(* spiwack: a PatternMatchingFailure wrapper around [Hipattern]. *) let match_eqdec sigma c = - try Proofview.tclUNIT (match_eqdec sigma c) + try + let (eqonleft,_,c1,c2,ty) = match_eqdec sigma c in + let (op,eq1,noteq,eq2) = + match EConstr.kind sigma c with + | App (op,[|ty1;ty2|]) -> + let ty1, ty2 = if eqonleft then ty1, ty2 else ty2, ty1 in + (match EConstr.kind sigma ty1, EConstr.kind sigma ty2 with + | App (eq1,_), App (noteq,[|neq|]) -> + (match EConstr.kind sigma neq with + | App (eq2,_) -> op,eq1,noteq,eq2 + | _ -> assert false) + | _ -> assert false) + | _ -> assert false in + let mk t x y = + let eq = mkApp (eq1,[|t;x;y|]) in + let neq = mkApp (noteq,[|mkApp (eq2,[|t;x;y|])|]) in + if eqonleft then mkApp (op,[|eq;neq|]) else mkApp (op,[|neq;eq|]) in + Proofview.tclUNIT (eqonleft,mk,c1,c2,ty) with PatternMatchingFailure -> Proofview.tclZERO PatternMatchingFailure (* /spiwack *) -let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with +let rec solveArg hyps eqonleft mk largs rargs = match largs, rargs with | [], [] -> tclTHENLIST [ choose_eq eqonleft; @@ -163,8 +198,8 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with | a1 :: largs, a2 :: rargs -> Proofview.Goal.enter { enter = begin fun gl -> let rectype = pf_unsafe_type_of gl a1 in - let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in - let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in + let decide = mk rectype a1 a2 in + let tac hyp = solveArg (hyp :: hyps) eqonleft mk largs rargs in let subtacs = if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto] else [diseqCase hyps eqonleft;eqCase tac;default_auto] in @@ -178,13 +213,13 @@ let solveEqBranch rectype = Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_concl gl in let sigma = project gl in - match_eqdec sigma concl >>= fun (eqonleft,op,lhs,rhs,_) -> + match_eqdec sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) -> let (mib,mip) = Global.lookup_inductive rectype in let nparams = mib.mind_nparams in let getargs l = List.skipn nparams (snd (decompose_app sigma l)) in let rargs = getargs rhs and largs = getargs lhs in - solveArg [] eqonleft op largs rargs + solveArg [] eqonleft mk largs rargs end } end begin function (e, info) -> match e with @@ -204,14 +239,14 @@ let decideGralEquality = Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_concl gl in let sigma = project gl in - match_eqdec sigma concl >>= fun (eqonleft,_,c1,c2,typ) -> + match_eqdec sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) -> let headtyp = hd_app sigma (pf_compute gl typ) in begin match EConstr.kind sigma headtyp with | Ind (mi,_) -> Proofview.tclUNIT mi | _ -> tclZEROMSG (Pp.str"This decision procedure only works for inductive objects.") end >>= fun rectype -> (tclTHEN - (mkBranches c1 c2) + (mkBranches data) (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype))) end } end -- cgit v1.2.3