From 37c239a073bc540f0b3e9fcc94008b5bfc6b3271 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 31 Jul 2025 03:04:17 +0200 Subject: [PATCH] Support generalized rewriting with leibniz equality in let bindings --- .../20985-mattam82-rewrite-in-lets.sh | 1 + .../20985-rewrite-in-lets-Added.rst | 5 ++ tactics/rewrite.ml | 71 ++++++++++++++++++- test-suite/success/rewrite_strat.v | 30 ++++++++ theories/Corelib/Classes/Morphisms.v | 30 +++++++- theories/Corelib/Classes/RelationClasses.v | 8 ++- 6 files changed, 138 insertions(+), 7 deletions(-) create mode 100644 dev/ci/user-overlays/20985-mattam82-rewrite-in-lets.sh create mode 100644 doc/changelog/04-tactics/20985-rewrite-in-lets-Added.rst diff --git a/dev/ci/user-overlays/20985-mattam82-rewrite-in-lets.sh b/dev/ci/user-overlays/20985-mattam82-rewrite-in-lets.sh new file mode 100644 index 000000000000..f3cd0eac711b --- /dev/null +++ b/dev/ci/user-overlays/20985-mattam82-rewrite-in-lets.sh @@ -0,0 +1 @@ +overlay stdlib https://github.com/mattam82/stdlib rewrite-in-lets 20985 diff --git a/doc/changelog/04-tactics/20985-rewrite-in-lets-Added.rst b/doc/changelog/04-tactics/20985-rewrite-in-lets-Added.rst new file mode 100644 index 000000000000..7e74d8e47eed --- /dev/null +++ b/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 `_, + by Matthieu Sozeau). diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 3fbddc077d7b..f349ae61793d 100644 --- a/tactics/rewrite.ml +++ b/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 diff --git a/test-suite/success/rewrite_strat.v b/test-suite/success/rewrite_strat.v index 22d23b7c885d..53be32eb8644 100644 --- a/test-suite/success/rewrite_strat.v +++ b/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. diff --git a/theories/Corelib/Classes/Morphisms.v b/theories/Corelib/Classes/Morphisms.v index 79b24b3dff00..d8e2ef7c6b43 100644 --- a/theories/Corelib/Classes/Morphisms.v +++ b/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] diff --git a/theories/Corelib/Classes/RelationClasses.v b/theories/Corelib/Classes/RelationClasses.v index 27869a342746..4037b6e68ab9 100644 --- a/theories/Corelib/Classes/RelationClasses.v +++ b/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] _.