From 8057bfa1cbd381801dc10dbea805b34ecfc3b770 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Thu, 7 May 2026 14:22:24 +0200 Subject: [PATCH 1/2] Check equality of expressions up to convertibility Co-authored-by: Copilot --- src/ecReduction.ml | 32 +++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/src/ecReduction.ml b/src/ecReduction.ml index d28cb2058..cb11a76ef 100644 --- a/src/ecReduction.ml +++ b/src/ecReduction.ml @@ -1864,26 +1864,28 @@ let hs_inv_alpha_eq hyps (inv1 : hs_inv) (inv2 : hs_inv) = module EqTest = struct include EqTest_base - include EqMod_base(struct - let for_expr env ~norm:_ alpha e1 e2 = - let convert e = - let f = (ss_inv_of_expr (EcIdent.create "&dummy") e).inv in + let for_expr env ~norm:_ alpha e1 e2 = + let convert e = + let f = (ss_inv_of_expr (EcIdent.create "&dummy") e).inv in + + if Mid.is_empty alpha then f else - if Mid.is_empty alpha then f else + let subst = + Mid.fold + (fun x (y, ty) subst -> + Fsubst.f_bind_local subst x (f_local y ty)) + alpha Fsubst.f_subst_id - let subst = - Mid.fold - (fun x (y, ty) subst -> - Fsubst.f_bind_local subst x (f_local y ty)) - alpha Fsubst.f_subst_id + in Fsubst.f_subst subst f in - in Fsubst.f_subst subst f in + let f1 = convert e1 in + let f2 = convert e2 in - let f1 = convert e1 in - let f2 = convert e2 in + is_conv (LDecl.init env []) f1 f2 - is_conv (LDecl.init env []) f1 f2 - end) + include EqMod_base(struct + let for_expr = for_expr + end) let for_pv = fun env ?(norm = true) -> for_pv env ~norm let for_lv = fun env ?(norm = true) -> for_lv env ~norm From 1c7b4556862076386bf8fc79b4a19848f9b47560 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Thu, 7 May 2026 15:35:16 +0200 Subject: [PATCH 2/2] fall back to checking equality of expressions in `sim` Co-authored-by: Copilot --- src/ecPV.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/ecPV.ml b/src/ecPV.ml index 3d173b9b6..d25f946a3 100644 --- a/src/ecPV.ml +++ b/src/ecPV.ml @@ -1127,6 +1127,11 @@ module Mpv2 = struct when EcReduction.EqTest.for_type env ty1 ty2 && EcReduction.EqTest.for_type env b1.e_ty b2.e_ty -> List.fold_left2 (add_eqs_loc env local) eqs (b1::es1) (b2::es2) + | _, _ when EcReduction.EqTest.for_expr env e1 e2 -> + let fv1 = e_read env e1 in + let fv2 = e_read env e2 in + union eqs (eq_refl (PV.union fv1 fv2)) + | _, _ -> raise EqObsInError let add_eqs env e1 e2 eqs = add_eqs_loc env Mid.empty eqs e1 e2