Support generalized rewriting in let bindings

dev/ci/user-overlays/20985-mattam82-rewrite-in-lets.sh

@@ -0,0 +1 @@
+overlay stdlib https://github.com/mattam82/stdlib rewrite-in-lets 20985

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

@@ -1007,9 +1007,73 @@ let unfold_match env sigma sk app =
 
 let is_rew_cast = function RewCast _ -> true | _ -> false
 
+let rocq_eqdata = Lazy.from_fun Rocqlib.build_rocq_eq_data
+
+let subterm_letin { env; evars; state; unfresh; cstr = (prop, cstr) } s n v t b =
+  let eq = Lazy.force rocq_eqdata 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) }
+           | RewCast _ -> 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
+
 let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
-  let aux { state ; env ; unfresh ;
-                term1 = t ; ty1 = ty ; cstr = (prop, cstr) ; evars } =
+  let aux ({ state ; env ; unfresh ;
+                term1 = t ; ty1 = ty ; cstr = (prop, cstr) ; evars } as info) =
     let cstr' = Option.map (fun c -> (ty, Some c)) cstr in
       match EConstr.kind (goalevars evars) t with
       | App (m, args) ->
@@ -1223,6 +1287,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
           | Fail | Identity -> b'
         in state, res
 
+      | LetIn (n, v, t, b) ->
+        subterm_letin info s n v t b
+
       | 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

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,16 +313,40 @@ 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]. *)
+Lemma eq_iff_subrelation : subrelation eq iff.
+Proof. now intros x y ->. Qed.
 
+(* We force exact matching, so this doesn't influence inference of signatures for existing morphisms *)
 #[global]
-Instance iff_impl_subrelation : subrelation iff impl | 2.
+Hint Extern 4 (subrelation eq iff) => exact eq_iff_subrelation : typeclass_instances.
+
+Lemma eq_flip_impl_subrelation : subrelation eq (Basics.flip Basics.impl).
+Proof. now intros x y ->. Qed.
+
+(* We force exact matching, so this doesn't influence inference of signatures for existing morphisms *)
+#[global]
+Hint Extern 5 (subrelation eq (Basics.flip Basics.impl)) => exact eq_flip_impl_subrelation : typeclass_instances.
+
+Lemma eq_impl_subrelation : subrelation eq Basics.impl.
+Proof. now intros x y ->. Qed.
+
+(* We force exact matching, so this doesn't influence inference of signatures for existing morphisms *)
+#[global]
+Hint Extern 5 (subrelation eq Basics.impl) => exact eq_impl_subrelation : typeclass_instances.
+
+Lemma iff_impl_subrelation : subrelation iff impl.
 Proof. firstorder. Qed.
 
 #[global]
-Instance iff_flip_impl_subrelation : subrelation iff (flip impl) | 2.
+Hint Extern 5 (subrelation iff impl) => exact iff_impl_subrelation : typeclass_instances.
+
+Lemma iff_flip_impl_subrelation : subrelation iff (flip impl).
 Proof. firstorder. Qed.
 
+#[global]
+Hint Extern 5 (subrelation iff (flip impl)) => exact iff_flip_impl_subrelation : typeclass_instances.
+
 (** We use an extern hint to help unification. *)
 
 #[global]

theories/Corelib/Classes/RelationClasses.v

@@ -238,8 +238,12 @@ Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass
 Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances.
 
 #[global]
-Hint Extern 4 (subrelation (flip _) _) => 
-  class_apply @subrelation_symmetric : typeclass_instances.
+Hint Extern 4 (subrelation (flip ?R) _) =>
+  match R with
+  | Basics.impl => fail 1
+  | flip Basics.impl => fail 1
+  | _ => class_apply @subrelation_symmetric
+  end : typeclass_instances.
 
 Arguments irreflexivity {A R Irreflexive} [x] _ : rename.
 Arguments symmetry {A} {R} {_} [x] [y] _.