add a generic mechanism for rewriting with any equality satisfying J

Author: tabareau

tactics/equality.ml

@@ -1265,7 +1265,7 @@ let index_of_ind_arg sigma t =
  *)
 
 type eliminator =
-| ElimConstant of (Constant.t * EInstance.t)
+| ElimConstant of EConstr.constr * int option
   (* Constant generated by a scheme function *)
 | ElimClause of EConstr.constr with_bindings
   (* Arbitrary expression provided by the user *)
@@ -1275,10 +1275,13 @@ let general_elim_clause0 with_evars flags (submetas, c, ty) elim =
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let clause, bindings, index =  match elim with
-  | ElimConstant cst ->
-    let elimc = mkConstU cst in
+  | ElimConstant (elimc, i) ->
     let elimt = Retyping.get_type_of env sigma elimc in
-    let i = index_of_ind_arg sigma elimt in
+    let elimt = Reductionops.whd_all env sigma elimt in
+    let i = match i with
+    | Some i -> i
+    | None -> index_of_ind_arg sigma elimt
+    in
     (elimc, elimt), NoBindings, Some i
   | ElimClause (elimc, lbindelimc) ->
     let elimt = Retyping.get_type_of env sigma elimc in
@@ -1293,13 +1296,18 @@ let general_elim_clause0 with_evars flags (submetas, c, ty) elim =
   Clenv.res_pf elimclause ~with_evars ~with_classes:true ~flags
   end
 
-let general_elim_clause_in0 with_evars flags id (submetas, c, ty) elim =
+let dbg = CDebug.create ~name:"general_elim" ()
+
+let general_elim_clause_in0 with_evars flags id (submetas, c, ty) elimc indarg =
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.project gl in
-  let elimc = mkConstU elim in
   let elimt = Retyping.get_type_of env sigma elimc in
-  let i = index_of_ind_arg sigma elimt in
+  let elimt = Reductionops.whd_all env sigma elimt in
+  let i = match indarg with
+      | Some i -> i
+      | None -> index_of_ind_arg sigma elimt
+  in
   let elimclause = mk_clenv_from env sigma (elimc, elimt) in
   let indmv =
     try nth_arg (Some i) (clenv_arguments elimclause)
@@ -1314,6 +1322,8 @@ let general_elim_clause_in0 with_evars flags id (submetas, c, ty) elim =
   let elimclause = clenv_instantiate ~flags ~submetas indmv elimclause (c, ty) in
   let hyp = mkVar id in
   let hyp_typ = Retyping.get_type_of env sigma hyp in
+  let _ = dbg (fun () -> Printer.pr_etype_env env sigma elimc) in
+  let _ = dbg (fun () -> Printer.pr_etype_env env sigma elimt) in
   let elimclause =
     try clenv_instantiate ~flags hypmv elimclause (hyp, hyp_typ)
     with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
@@ -1343,14 +1353,10 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
     (apply_clear_request clear_flag (use_clear_hyp_by_default ()) id)
   end
 
-let general_elim_clause with_evars flags where arg elim =
-  Proofview.tclENV >>= fun env ->
-  Proofview.tclEVARMAP >>= fun sigma ->
-  let (sigma, (elim, u)) = Evd.fresh_constant_instance env sigma elim in
-  Proofview.Unsafe.tclEVARS sigma <*>
+let general_elim_clause with_evars flags where arg elimc indarg =
   match where with
-  | None -> general_elim_clause0 with_evars flags arg (ElimConstant (elim, EInstance.make u))
-  | Some id -> general_elim_clause_in0 with_evars flags id arg (elim, EInstance.make u)
+  | None -> general_elim_clause0 with_evars flags arg (ElimConstant (elimc, indarg))
+  | Some id -> general_elim_clause_in0 with_evars flags id arg elimc indarg
 
 (* Case analysis tactics *)
 
@@ -1425,7 +1431,7 @@ let default_elim with_evars clear_flag (c,_ as cx) =
       let sigma, elim = find_ind_eliminator env sigma ind
                           (Retyping.get_sort_quality_of env sigma concl) in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-      (general_elim with_evars clear_flag cx (ElimConstant elim))
+      (general_elim with_evars clear_flag cx (ElimConstant (mkConstU elim, None)))
     end)
     begin function (e, info) -> match e with
       | IsNonrec ->
@@ -2126,7 +2132,7 @@ let intro_decomp_eq ?loc l thin tac id =
   | Some (eq,u,eq_args) ->
     !intro_decomp_eq_function
       (fun n -> tac ((CAst.make id)::thin) (Some n) l)
-      (eq,t,eq_args) (c, t)
+      (eq,u,t,eq_args) (c, t)
   | None ->
     let info = Exninfo.reify () in
     Tacticals.tclZEROMSG ~info (str "Not a primitive equality here.")

tactics/tactics.ml

@@ -455,7 +455,7 @@ val default_elim : evars_flag -> clear_flag -> constr with_bindings ->
   unit Proofview.tactic
 
 val general_elim_clause : evars_flag -> unify_flags -> Id.t option ->
-    ((metavariable list * Unification.Meta.t) * EConstr.t * EConstr.types) -> Constant.t -> unit Proofview.tactic
+    ((metavariable list * Unification.Meta.t) * EConstr.t * EConstr.types) -> EConstr.t -> int option -> unit Proofview.tactic
 
 (** [general_case_analysis with_evars clear (t, bindings)] performs case analysis on [t].
     If [t] is a variable which is not in the context, we attempt to perform introductions
@@ -677,7 +677,7 @@ val subst_one :
   (bool -> Id.t -> Id.t * constr * bool -> unit Proofview.tactic) Hook.t
 
 val declare_intro_decomp_eq :
-  ((int -> unit Proofview.tactic) -> Rocqlib.rocq_eq_data * types *
+  ((int -> unit Proofview.tactic) -> Rocqlib.rocq_eq_data * EInstance.t * types *
    (types * constr * constr) ->
    constr * types -> unit Proofview.tactic) -> unit
 

tactics/tactics.mli

@@ -11,15 +11,12 @@ Definition nand@{q; |} (a b : bool@{q;}) : bool@{q;} :=
 Inductive seq@{q;u|} {A : Type@{q;u}} (a : A) : A -> Type@{q;u} := | srefl : seq a a.
 Arguments srefl {_ _}.
 
-Definition seq_elim@{q;u v|} :=
-  fun (A : Type@{q;u}) (x : A) (P : A -> Type@{q;v}) (f : P x) (a : A) (e : seq x a) =>
-  match e in (seq _ a0) return (P a0) with
-  | srefl => f
-  end.
+#[universes(polymorphic=yes)]
+Instance seq_Has_Leibniz_elim@{s; l l' l''} : Has_Leibniz@{s s s;l l' l''} (@seq) :=
+  fun A x P t y e => match e with srefl => t end.
 
 Register seq as core.eq.type.
 Register srefl as core.eq.refl.
-Register seq_elim as core.eq.rect.
 
 Lemma foo@{q; |} (f : bool@{q;} -> bool@{q;}) (x : bool@{q;}) : seq (f true) (f true).
 Proof.

test-suite/bugs/bug_19203.v

@@ -100,7 +100,10 @@ Register eq_elim as core.eq.rect.
 
   End equality.
 
-  Inductive comparison : Set :=
+Instance eq_Has_Leibniz_elim@{s s'; l l' l''} : Has_Leibniz@{s s' s' ; l l' l''} (@eq@{s s' ; l l'}) :=
+  fun A x P t y e => match e with eq_refl => t end.
+
+Inductive comparison : Set :=
   | Eq : comparison
   | Lt : comparison
   | Gt : comparison.

test-suite/bugs/bug_19215.v

@@ -18,8 +18,9 @@ End Nat.
 
 Notation eq_nat_dec := Nat.eq_dec (only parsing).
 
+#[universes(polymorphic=yes)]
 Theorem eq_rect_nat_double : forall T (a b c : nat) x ab bc,
-  eq_rect b T (eq_rect a T x b ab) c bc = eq_rect a T x c (eq_trans ab bc).
+  @eq_Has_Leibniz_r_elim _ b T (eq_rect a T x b ab) c bc = eq_rect a T x c (eq_trans ab (eq_sym bc)).
 Admitted.
 
 Ltac eq_rect_simpl :=

test-suite/bugs/bug_20397_1.v

@@ -27,5 +27,5 @@ Goal
 Proof.
   intros a b H.
   inversion H.
-  Fail reflexivity.
+  reflexivity.
 Abort.

test-suite/bugs/bug_3125.v

@@ -22,6 +22,10 @@ Register eq_refl as core.eq.refl.
 Register eq_ind as core.eq.ind.
 Register eq_rect as core.eq.rect.
 
+#[universes(polymorphic=yes)]
+Instance eq_Has_Leibniz_elim@{s ; l l'} : Has_Leibniz@{Type Prop s;l Set l'} (@eq) :=
+  fun A x P t y e => match e with eq_refl => t end.
+
 Lemma foo (H : true = false) : False.
 Proof.
   discriminate.
@@ -31,6 +35,6 @@ Print foo.
 Goal False.
   let c := eval cbv delta [foo] in foo in
     match c with
-      context[eq_ind] => idtac
+      context[eq_Has_Leibniz_elim] => idtac
     end.
 Abort.

test-suite/bugs/bug_3132.v

@@ -21,8 +21,8 @@
 <div class="code">
 <span class="id" title="keyword">Definition</span> <a id="a" class="idref" href="#a"><span class="id" title="definition">a</span></a> := 0. #[   <span class="id" title="var">universes</span>( <span class="id" title="var">template</span>) ]<br/>
 <span class="id" title="keyword">Inductive</span> <a id="mysum" class="idref" href="#mysum"><span class="id" title="definition, inductive"><span id="mysum_rect" class="id"><span id="mysum_ind" class="id"><span id="mysum_rec" class="id"><span id="mysum_sind" class="id">mysum</span></span></span></span></span></a> (<a id="A:1" class="idref" href="#A:1"><span class="id" title="binder">A</span></a> <a id="B:2" class="idref" href="#B:2"><span class="id" title="binder">B</span></a>:<span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/>
-&nbsp;&nbsp;| <a id="myinl" class="idref" href="#myinl"><span class="id" title="constructor">myinl</span></a> : <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum:3"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a><br/>
-&nbsp;&nbsp;| <a id="myinr" class="idref" href="#myinr"><span class="id" title="constructor">myinr</span></a> : <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum:3"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a>.<br/>
+&nbsp;&nbsp;| <a id="myinl" class="idref" href="#myinl"><span class="id" title="constructor">myinl</span></a> : <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Corelib.Init.Equality.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum:3"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a><br/>
+&nbsp;&nbsp;| <a id="myinr" class="idref" href="#myinr"><span class="id" title="constructor">myinr</span></a> : <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Corelib.Init.Equality.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum:3"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a>.<br/>
 
 <br/>
 #[<span class="id" title="var">local</span>]<span class="id" title="keyword">Definition</span> <a id="b" class="idref" href="#b"><span class="id" title="definition">b</span></a> := 1.<br/>

test-suite/coqdoc/bug11353.html.out

@@ -24,9 +24,9 @@
 \coqdocnoindent
 \coqdockw{Inductive} \coqdef{Coqdoc.bug11353.mysum}{mysum}{\coqdocinductive{mysum}} (\coqdef{Coqdoc.bug11353.A:1}{A}{\coqdocbinder{A}} \coqdef{Coqdoc.bug11353.B:2}{B}{\coqdocbinder{B}}:\coqdockw{Type}) : \coqdockw{Type} :=\coqdoceol
 \coqdocindent{1.00em}
-\ensuremath{|} \coqdef{Coqdoc.bug11353.myinl}{myinl}{\coqdocconstructor{myinl}} : \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum:3}{\coqdocinductive{mysum}} \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}}\coqdoceol
+\ensuremath{|} \coqdef{Coqdoc.bug11353.myinl}{myinl}{\coqdocconstructor{myinl}} : \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Equality}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum:3}{\coqdocinductive{mysum}} \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}}\coqdoceol
 \coqdocindent{1.00em}
-\ensuremath{|} \coqdef{Coqdoc.bug11353.myinr}{myinr}{\coqdocconstructor{myinr}} : \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum:3}{\coqdocinductive{mysum}} \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}}.\coqdoceol
+\ensuremath{|} \coqdef{Coqdoc.bug11353.myinr}{myinr}{\coqdocconstructor{myinr}} : \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Equality}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum:3}{\coqdocinductive{mysum}} \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}}.\coqdoceol
 \coqdocemptyline
 \coqdocnoindent
 \#[\coqdocvar{local}]\coqdockw{Definition} \coqdef{Coqdoc.bug11353.b}{b}{\coqdocdefinition{b}} := 1.\coqdoceol