Support generalized rewriting with leibniz equality in let bindings

Author: mattam82

doc/changelog/04-tactics/20985-rewrite-in-lets-Added.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  Add support for rewriting in let bindings (using Leibniz equality)
+  to generalized rewriting 
+  (`#20985 <https://github.com/rocq-prover/rocq/pull/20985>`_,
+  by Matthieu Sozeau).

tactics/rewrite.ml

@@ -1223,6 +1223,66 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
           | Fail | Identity -> b'
         in state, res
 
+      | LetIn (n, v, t, b) ->
+        let eq = Rocqlib.build_rocq_eq_data () in
+        let evars', eqty = Evd.fresh_global env (fst evars) eq.Rocqlib.eq in
+        let eqty = EConstr.mkApp (eqty, [| t |]) in
+        let state, v' =
+          s.strategy { state ; term1 = v ; ty1 = t ; cstr = (prop,Some eqty); evars = (evars', snd evars); env; unfresh }
+        in
+        let res =
+          match v' with
+          | Success r ->
+            let env' = EConstr.push_rel (LocalDef (n, v, t)) env in
+            let bty = Retyping.get_type_of env' (goalevars evars) b in
+            if not @@ noccurn (goalevars evars) 1 bty then Fail
+            else
+              let bty = subst1 mkProp bty in
+              let r = match r.rew_prf with
+              | RewPrf (_rel, prf) ->
+                let sigma, eqt = Evd.fresh_global env (fst r.rew_evars) eq.Rocqlib.eq in
+                let sigma, congr = Evd.fresh_global env sigma eq.Rocqlib.congr in
+                let congr = mkApp (congr, [| t; bty; mkLambda (n, t, b); r.rew_from; r.rew_to; prf |]) in
+                { r with rew_prf = RewPrf (mkApp (eqt, [| bty |]), congr); rew_evars = (sigma, snd r.rew_evars) }
+              | x -> r
+              in
+              Success { r with
+                rew_car = bty;
+                rew_from = mkLetIn(n, r.rew_from, t, b);
+                rew_to = mkLetIn (n, r.rew_to, t, b) }
+          | Fail | Identity -> v'
+        in
+        let res =
+          match res with
+          | Success res ->
+            (match res.rew_prf with
+            | RewPrf (rel, prf) ->
+              Success (apply_constraint env res.rew_car rel prf (prop,cstr) res)
+            | _ -> Success res)
+          | _ -> res
+        in
+        (match res with
+        | Success _ -> state, res
+        | Fail | Identity ->
+          let env' = EConstr.push_rel (LocalDef (n, v, t)) env in
+          let bty = Retyping.get_type_of env' (goalevars evars) b in
+          let state, b' =  s.strategy { state ; term1 = b ; ty1 = bty ; cstr = (prop, Option.map (lift 1) cstr);
+            evars; env = env'; unfresh }
+          in
+          let res =
+            match b' with
+            | Success r ->
+              let mklet t' = mkLetIn (n, v, t, t') in
+              Success { r with rew_car = r.rew_car;
+                rew_prf =
+                  (match r.rew_prf with
+                  | RewPrf (rel, prf) -> RewPrf (mklet rel, mklet prf)
+                  | RewCast k -> RewCast k);
+                rew_from = mklet r.rew_from;
+                rew_to = mklet r.rew_to; }
+            | _ -> res
+          in state, res)
+
       | Case (ci, u, pms, p, iv, c, brs) ->
         let (ci, (p,rp), iv, c, brs) = EConstr.expand_case env (goalevars evars) (ci, u, pms, p, iv, c, brs) in
         let cty = Retyping.get_type_of env (goalevars evars) c in
@@ -1618,7 +1678,7 @@ let solve_constraints env (evars,cstrs) =
   let evars' = TC.resolve_typeclasses env ~filter:TC.all_evars ~fail:true evars' in
   Evd.set_typeclass_evars evars' oldtcs
 
-let nf_zeta =
+let _nf_zeta =
   Reductionops.clos_norm_flags (RedFlags.mkflags [RedFlags.fZETA])
 
 exception RewriteFailure of Environ.env * Evd.evar_map * pretype_error
@@ -1662,7 +1722,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
     let res = match res.rew_prf with
       | RewCast c -> None
       | RewPrf (rel, p) ->
-        let p = nf_zeta env evars p in
+        (* let p = nf_zeta env evars p in *)
         let term =
           match abs with
           | None -> p

test-suite/success/rewrite_strat.v

@@ -189,3 +189,33 @@ Module StratTactic.
   Qed.
 
 End StratTactic.
+
+Module RewriteLet.
+  Import Nat.
+
+  (* In a "deep" context *)
+
+  Axiom f : nat -> nat.
+
+  Goal forall x : nat, f (let x0 := x + 1 in x0 + x0) = f (S (S (x + x))).
+  Proof.
+    intros x.
+    rewrite_strat (topdown (choice (<- plus_n_Sm) (<- plus_n_O))).
+    reflexivity.
+  Qed.
+
+  (* In a toplevel context, requiring to mediate between [eq] and [impl] / [flip impl] *)
+  Goal forall x : nat, let x0 := x + 1 in x0 = x0.
+  Proof.
+    intros x.
+    now rewrite_strat (topdown (choice (<- plus_n_Sm) (<- plus_n_O))).
+  Qed.
+
+  Goal forall x : nat, (let x0 := x + 1 in x0 = x0) -> S x = S x.
+  Proof.
+    intros x H.
+    rewrite_strat (topdown (choice (<- plus_n_Sm) (<- plus_n_O))) in H.
+    exact H.
+  Qed.
+
+End RewriteLet.

theories/Corelib/Classes/Morphisms.v

@@ -313,7 +313,15 @@ Ltac proper_subrelation :=
 #[global]
 Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances.
 
-(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
+(** Essential subrelation instances for [eq], [iff], [impl] and [pointwise_relation]. *)
+
+#[global]
+Instance eq_flip_impl_subrelation : subrelation eq (Basics.flip Basics.impl).
+Proof. now intros x y ->. Qed.
+
+#[global]
+Instance eq_impl_subrelation : subrelation eq Basics.impl.
+Proof. now intros x y ->. Qed.
 
 #[global]
 Instance iff_impl_subrelation : subrelation iff impl | 2.