1 files changed, 101 insertions, 52 deletions

diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index b1d3290a..b0deeed1 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (************************************************************************)
@@ -16,6 +18,7 @@ open Util
 open Names
 open Namegen
 open Term
+open EConstr
 open Declarations
 open Tactics
 open Tacticals.New
@@ -23,7 +26,7 @@ open Auto
 open Constr_matching
 open Misctypes
 open Hipattern
-open Pretyping
+open Proofview.Notations
 open Tacmach.New
 open Coqlib
 
@@ -49,7 +52,9 @@ open Coqlib
    Eduardo Gimenez (30/3/98).
 *)
 
-let clear_last = (onLastHyp (fun c -> (clear [destVar c])))
+let clear_last =
+  Proofview.tclEVARMAP >>= fun sigma ->
+  (onLastHyp (fun c -> (clear [destVar sigma c])))
 
 let choose_eq eqonleft =
   if eqonleft then
@@ -62,18 +67,39 @@ let choose_noteq eqonleft =
   else
     left_with_bindings false Misctypes.NoBindings
 
-let mkBranches c1 c2 =
+(* 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 begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let store = Proofview.Goal.extra gl in
+  Refine.refine ~typecheck:false begin fun sigma ->
+    let na = Name (next_name_away_with_default "x" Anonymous (Termops.vars_of_env env)) in
+    let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in
+    let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in
+    (sigma, mkApp (x, [|c2|]))
+  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;
      clear_last;
      intros]
 
+let inj_flags = Some {
+    Equality.keep_proof_equalities = true; (* necessary *)
+    Equality.injection_in_context = true; (* does not matter here *)
+    Equality.injection_pattern_l2r_order = true; (* does not matter here *)
+  }
+
 let discrHyp id =
-  let c = { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } in
-  let tac c = Equality.discr_tac false (Some (None, Tacexpr.ElimOnConstr c)) in
+  let c env sigma = (sigma, (mkVar id, NoBindings)) in
+  let tac c = Equality.discr_tac false (Some (None, ElimOnConstr c)) in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
 
 let solveNoteqBranch side =
@@ -83,12 +109,9 @@ let solveNoteqBranch side =
 
 (* Constructs the type {c1=c2}+{~c1=c2} *)
 
-let make_eq () =
-(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
-
-let mkDecideEqGoal eqonleft op rectype c1 c2 =
-  let equality    = mkApp(make_eq(), [|rectype; c1; c2|]) in
-  let disequality = mkApp(build_coq_not (), [|equality|]) in
+let mkDecideEqGoal eqonleft (op,eq,neg) rectype c1 c2 =
+  let equality    = mkApp(eq, [|rectype; c1; c2|]) in
+  let disequality = mkApp(neg, [|equality|]) in
   if eqonleft then mkApp(op, [|equality; disequality |])
   else mkApp(op, [|disequality; equality |])
 
@@ -98,13 +121,13 @@ let mkDecideEqGoal eqonleft op rectype c1 c2 =
 let idx = Id.of_string "x"
 let idy = Id.of_string "y"
 
-let mkGenDecideEqGoal rectype g =
-  let hypnames = pf_ids_of_hyps g in
+let mkGenDecideEqGoal rectype ops g =
+  let hypnames = pf_ids_set_of_hyps g in
   let xname    = next_ident_away idx hypnames
   and yname    = next_ident_away idy hypnames in
   (mkNamedProd xname rectype
      (mkNamedProd yname rectype
-        (mkDecideEqGoal true (build_coq_sumbool ())
+        (mkDecideEqGoal true ops
           rectype (mkVar xname) (mkVar yname))))
 
 let rec rewrite_and_clear hyps = match hyps with
@@ -120,8 +143,8 @@ let eqCase tac =
   tclTHEN intro (onLastHypId tac)
 
 let injHyp id =
-  let c = { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } in
-  let tac c = Equality.injClause None false (Some (None, Tacexpr.ElimOnConstr c)) in
+  let c env sigma = (sigma, (mkVar id, NoBindings)) in
+  let tac c = Equality.injClause inj_flags None false (Some (None, ElimOnConstr c)) in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
 
 let diseqCase hyps eqonleft =
@@ -138,15 +161,32 @@ let diseqCase hyps eqonleft =
 
 open Proofview.Notations
 
-(* spiwack: a small wrapper around [Hipattern]. *)
-
-let match_eqdec c =
-  try Proofview.tclUNIT (match_eqdec c)
+(* spiwack: a PatternMatchingFailure wrapper around [Hipattern]. *)
+
+let match_eqdec env sigma c =
+  try
+    let (eqonleft,_,c1,c2,ty) = match_eqdec env 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;
@@ -154,30 +194,33 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
     intros_reflexivity;
   ]
 | a1 :: largs, a2 :: rargs ->
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.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
   (tclTHENS (elim_type decide) subtacs)
-  end }
+  end
 | _ -> invalid_arg "List.fold_right2"
 
 let solveEqBranch rectype =
   Proofview.tclORELSE
     begin
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let concl = pf_nf_concl gl in
-        match_eqdec concl >>= fun (eqonleft,op,lhs,rhs,_) ->
+      Proofview.Goal.enter begin fun gl ->
+        let concl = pf_concl gl in
+        let env = Proofview.Goal.env gl in
+        let sigma = project gl in
+        match_eqdec env 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 l)) 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
-      end }
+
+          solveArg [] eqonleft mk largs rargs
+      end
     end
     begin function (e, info) -> match e with
       | PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!")
@@ -186,25 +229,27 @@ let solveEqBranch rectype =
 
 (* The tactic Decide Equality *)
 
-let hd_app c = match kind_of_term c with
+let hd_app sigma c = match EConstr.kind sigma c with
   | App (h,_) -> h
   | _ -> c
 
 let decideGralEquality =
   Proofview.tclORELSE
     begin
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let concl = pf_nf_concl gl in
-        match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) ->
-        let headtyp = hd_app (pf_compute gl typ) in
-        begin match kind_of_term headtyp with
+      Proofview.Goal.enter begin fun gl ->
+        let concl = pf_concl gl in
+        let env = Proofview.Goal.env gl in
+        let sigma = project gl in
+        match_eqdec env 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
     end
     begin function (e, info) -> match e with
       | PatternMatchingFailure ->
@@ -214,21 +259,25 @@ let decideGralEquality =
 
 let decideEqualityGoal = tclTHEN intros decideGralEquality
 
-let decideEquality rectype =
-  Proofview.Goal.enter { enter = begin fun gl ->
-  let decide = mkGenDecideEqGoal rectype gl in
+let decideEquality rectype ops =
+  Proofview.Goal.enter begin fun gl ->
+  let decide = mkGenDecideEqGoal rectype ops gl in
   (tclTHENS (cut decide) [default_auto;decideEqualityGoal])
-  end }
+  end
 
 
 (* The tactic Compare *)
 
 let compare c1 c2 =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  pf_constr_of_global (build_coq_sumbool ()) >>= fun opc ->
+  pf_constr_of_global (Coqlib.build_coq_eq ()) >>= fun eqc ->
+  pf_constr_of_global (build_coq_not ()) >>= fun notc ->
+  Proofview.Goal.enter begin fun gl ->
   let rectype = pf_unsafe_type_of gl c1 in
-  let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
+  let ops = (opc,eqc,notc) in
+  let decide = mkDecideEqGoal true ops rectype c1 c2 in
   (tclTHENS (cut decide)
             [(tclTHEN  intro
              (tclTHEN (onLastHyp simplest_case) clear_last));
-             decideEquality rectype])
-  end }
+             decideEquality rectype ops])
+  end