From 8266190b856e1f438d6097279debfc31fe091ab4 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Mon, 1 Jun 2026 20:05:49 +0200 Subject: [PATCH] congr: add `congr pat` and `congr *` variants `congr pat` requires the pattern to match both sides of the goal equality (or iff); each pattern variable yields one subgoal equating its bindings on the two sides. `congr *` walks both sides in lock-step without any reduction, emitting one subgoal per pair of differing positions. Both variants are first-order (binders are opaque, matching the existing `congr`'s behavior). --- src/ecHiGoal.ml | 28 ++++++- src/ecHiGoal.mli | 2 +- src/ecHiTacticals.ml | 2 +- src/ecLowGoal.ml | 175 +++++++++++++++++++++++++++++++++++++++++ src/ecLowGoal.mli | 15 ++++ src/ecParser.mly | 8 +- src/ecParsetree.ml | 8 +- src/phl/ecPhlDeno.ml | 6 +- tests/congr-pattern.ec | 86 ++++++++++++++++++++ 9 files changed, 322 insertions(+), 8 deletions(-) create mode 100644 tests/congr-pattern.ec diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index c58de527f6..5505e655fe 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -2262,7 +2262,8 @@ let process_exists args (tc : tcenv1) = EcLowGoal.t_exists_intro_s args tc (* -------------------------------------------------------------------- *) -let process_congr tc = +(* Default [congr]: one structural step on the head of the equality. *) +let process_congr_default tc = let (env, hyps, concl) = FApi.tc1_eflat tc in if not (EcFol.is_eq_or_iff concl) then @@ -2310,6 +2311,31 @@ let process_congr tc = | _, _ -> tacuerror "not a congruence" +(* -------------------------------------------------------------------- *) +(* [congr pat]: thin wrapper around [EcLowGoal.t_congr_pattern]. *) +let process_congr_pattern p tc = + let concl = FApi.tc1_goal tc in + if not (EcFol.is_eq_or_iff concl) then + tc_error !!tc "goal must be an equality or an equivalence"; + let (ps, ue), pat = TTC.tc1_process_pattern tc p in + let pvars = Mid.keys ps in + EcLowGoal.t_congr_pattern ~pat ~pvars ~ue tc + +(* -------------------------------------------------------------------- *) +(* [congr *]: thin wrapper around [EcLowGoal.t_congr_star]. *) +let process_congr_star tc = + let concl = FApi.tc1_goal tc in + if not (EcFol.is_eq_or_iff concl) then + tc_error !!tc "goal must be an equality or an equivalence"; + EcLowGoal.t_congr_star tc + +(* -------------------------------------------------------------------- *) +let process_congr (mode : pcongr_mode) tc = + match mode with + | PCongrDefault -> process_congr_default tc + | PCongrStar -> process_congr_star tc + | PCongrPattern p -> process_congr_pattern p tc + (* -------------------------------------------------------------------- *) let process_wlog ids wlog tc = let hyps, _ = FApi.tc1_flat tc in diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli index 78f61f3b00..04220db14a 100644 --- a/src/ecHiGoal.mli +++ b/src/ecHiGoal.mli @@ -92,7 +92,7 @@ val process_split_all : must:bool -> backward val process_elim : prevert * pqsymbol option -> backward val process_case : ?doeq:bool -> prevertv -> backward val process_exists : ppt_arg located list -> backward -val process_congr : backward +val process_congr : pcongr_mode -> backward val process_solve : ?bases:symbol list -> ?depth:int -> backward val process_trivial : backward val process_change : pformula -> backward diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 8a6576983b..0595c5d9e8 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -139,7 +139,7 @@ and process1_logic (ttenv : ttenv) (t : logtactic located) (tc : tcenv1) = | Pexists fs -> process_exists fs | Pleft -> process_left | Pright -> process_right - | Pcongr -> process_congr + | Pcongr mode -> process_congr mode | Ptrivial -> process_trivial | Pelim pe -> process_elim pe | Papply pe -> process_apply ~implicits:ttenv.tt_implicits pe diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 4a73fc517e..6117f7bcbc 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -2568,6 +2568,181 @@ let t_congr (f1, f2) (args, ty) tc = in doit (List.rev args) ty tc +(* -------------------------------------------------------------------- *) +(* Read the equality (or iff) at the head of the goal and return: + - the two sides [f1, f2]; + - [t_ensure_eq], a tactic that coerces an iff goal to an eq goal; + - [t_subgoal], the auto-discharge tactic for trivial side goals + (alpha-reflexivity and alpha-assumption). + It is the caller's responsibility to have checked that the goal is an + equality or an equivalence (e.g. via [EcFol.is_eq_or_iff]). *) +let congr_split_eq_or_iff tc = + let concl = FApi.tc1_goal tc in + assert (EcFol.is_eq_or_iff concl); + + let ((f1, f2), iseq) = + if EcFol.is_eq concl + then (EcFol.destr_eq concl, true ) + else (EcFol.destr_iff concl, false) in + + let t_ensure_eq = + if iseq then t_id + else + (fun tc -> + let hyps = FApi.tc1_hyps tc in + Apply.t_apply_bwd_r + (PT.pt_of_uglobal !!tc hyps LG.p_eq_iff) tc) in + + let t_subgoal = + FApi.t_ors [t_reflex ~mode:`Alpha; t_assumption `Alpha; t_id] in + + (f1, f2, t_ensure_eq, t_subgoal) + +(* -------------------------------------------------------------------- *) +(* Discharge an equality goal whose two sides are [skel[xi := Li]] and + [skel[xi := Ri]] (up to beta), by: + 1. coercing iff to eq if needed; + 2. changing the goal to [(\xi. skel) Li... = (\xi. skel) Ri...]; + 3. unfolding the congruence one step per hole with [t_congr]; + 4. auto-closing trivial side goals. + The goal type is read from [f1.f_ty]; [holes], [lvec] and [rvec] must + have the same length, and each [Li/Ri] must have the type of [xi]. *) +let t_congr_from_skeleton ~holes ~skel ~lvec ~rvec tc = + let (f1, _f2, t_ensure_eq, t_subgoal) = congr_split_eq_or_iff tc in + + if List.is_empty holes then + FApi.t_seq t_ensure_eq t_reflex tc + else + let ty = f1.f_ty in + let bds = List.map (fun (x, t) -> (x, GTty t)) holes in + let lam = f_lambda bds skel in + let app_lhs = f_app lam lvec ty in + let app_rhs = f_app lam rvec ty in + let newgoal = f_eq app_lhs app_rhs in + let pairs = List.combine lvec rvec in + let tcgr = t_congr (lam, lam) (pairs, ty) in + FApi.t_seqs + [t_ensure_eq; + (fun tc -> FApi.tcenv_of_tcenv1 (t_change1 newgoal tc)); + tcgr; + t_subgoal] + tc + +(* -------------------------------------------------------------------- *) +(* [congr pat]: pattern matches both sides of an equality/iff goal; one + subgoal per pattern variable (skipping syntactically-equal sides). + - [pat] is the elaborated pattern formula (containing free [f_local]s + for each pattern variable); + - [pvars] is the list of pattern-variable identifiers; + - [ue] is the unification environment from pattern elaboration. *) +let t_congr_pattern ~pat ~pvars ~ue tc = + let (env, hyps, _concl) = FApi.tc1_eflat tc in + let (f1, f2, _, _) = congr_split_eq_or_iff tc in + + let ev0 = MEV.of_idents pvars `Form in + + let match_side label side = + let ue' = EcUnify.UniEnv.copy ue in + try + let (ue'', _, ev'') = + f_match fmsearch hyps (ue', ev0) pat side + in (ue'', ev'') + with MatchFailure -> + tc_error !!tc "pattern does not match %s of the goal" label + in + + let (ueL, evL) = match_side "left-hand side" f1 in + let (ueR, evR) = match_side "right-hand side" f2 in + + let substL = MEV.assubst ueL evL env in + let substR = MEV.assubst ueR evR env in + + let holes_full = + List.map (fun x -> + let probe_ty = EcUnify.UniEnv.fresh ueL in + let probe = f_local x probe_ty in + let li = Fsubst.f_subst substL probe in + let ri = Fsubst.f_subst substR probe in + (x, li.f_ty, li, ri) + ) pvars + in + + let kept, dropped = + List.partition + (fun (_, _, li, ri) -> not (is_alpha_eq hyps li ri)) + holes_full + in + + let holes = List.map (fun (x, t, _, _) -> (x, t)) kept in + let lvec = List.map (fun (_, _, l, _) -> l) kept in + let rvec = List.map (fun (_, _, _, r) -> r) kept in + + let skel = + List.fold_left + (fun acc (x, _, li, _) -> Fsubst.f_subst_local x li acc) + pat dropped + in + + t_congr_from_skeleton ~holes ~skel ~lvec ~rvec tc + +(* -------------------------------------------------------------------- *) +(* [congr *]: walk LHS/RHS in lock-step without reduction; emit one + subgoal per pair of differing positions. Binders are opaque. *) +let t_congr_star tc = + let (env, hyps, _concl) = FApi.tc1_eflat tc in + let (f1, f2, _, _) = congr_split_eq_or_iff tc in + + let holes = ref [] in + let lvec = ref [] in + let rvec = ref [] in + + let mk_hole (l : form) (r : form) : form = + let x = EcIdent.create "_x" in + holes := (x, l.f_ty) :: !holes; + lvec := l :: !lvec; + rvec := r :: !rvec; + f_local x l.f_ty + in + + let rec walk (l : form) (r : form) : form = + if is_alpha_eq hyps l r then + l + else + match l.f_node, r.f_node with + | Fapp (hL, aL), Fapp (hR, aR) + when is_alpha_eq hyps hL hR + && List.length aL = List.length aR + && EqTest.for_type env l.f_ty r.f_ty -> + let args' = List.map2 walk aL aR in + f_app hL args' l.f_ty + + | Fif (cL, tL, eL), Fif (cR, tR, eR) -> + let c' = walk cL cR in + let t' = walk tL tR in + let e' = walk eL eR in + f_if c' t' e' + + | Ftuple xs, Ftuple ys when List.length xs = List.length ys -> + let zs = List.map2 walk xs ys in + f_tuple zs + + | Fproj (xL, iL), Fproj (xR, iR) + when iL = iR && EqTest.for_type env l.f_ty r.f_ty -> + f_proj (walk xL xR) iL l.f_ty + + | _, _ -> + if not (EqTest.for_type env l.f_ty r.f_ty) then + tc_error !!tc "congr*: cannot equate subterms of different types"; + mk_hole l r + in + + let skel = walk f1 f2 in + let holes = List.rev !holes in + let lvec = List.rev !lvec in + let rvec = List.rev !rvec in + + t_congr_from_skeleton ~holes ~skel ~lvec ~rvec tc + (* -------------------------------------------------------------------- *) type smtmode = [`Sloppy | `Strict | `Report of EcLocation.t option] diff --git a/src/ecLowGoal.mli b/src/ecLowGoal.mli index 2581c9bb04..e69da529d6 100644 --- a/src/ecLowGoal.mli +++ b/src/ecLowGoal.mli @@ -335,6 +335,21 @@ val t_crush_fwd : ?delta:bool -> int -> FApi.backward (* -------------------------------------------------------------------- *) val t_congr : form pair -> form pair list * ty -> FApi.backward +val t_congr_from_skeleton : + holes:(EcIdent.t * ty) list + -> skel:form + -> lvec:form list + -> rvec:form list + -> FApi.backward + +val t_congr_pattern : + pat:form + -> pvars:EcIdent.t list + -> ue:EcUnify.unienv + -> FApi.backward + +val t_congr_star : FApi.backward + (* -------------------------------------------------------------------- *) type smtmode = [`Sloppy | `Strict | `Report of EcLocation.t option] diff --git a/src/ecParser.mly b/src/ecParser.mly index 68121e583b..37c728e28e 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2802,7 +2802,13 @@ logtactic: { Pclear (`Include l) } | CONGR - { Pcongr } + { Pcongr PCongrDefault } + +| CONGR STAR + { Pcongr PCongrStar } + +| CONGR p=sform_h + { Pcongr (PCongrPattern p) } | TRIVIAL { Ptrivial } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 1dd721c69e..b9e71b8a3a 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -1039,6 +1039,12 @@ type clear_info = [ (* -------------------------------------------------------------------- *) type pgenhave = psymbol * intropattern option * psymbol list * pformula +(* -------------------------------------------------------------------- *) +type pcongr_mode = + | PCongrDefault + | PCongrStar + | PCongrPattern of pformula + (* -------------------------------------------------------------------- *) type logtactic = | Preflexivity @@ -1052,7 +1058,7 @@ type logtactic = | Pleft | Pright | Ptrivial - | Pcongr + | Pcongr of pcongr_mode | Pelim of (prevert * pqsymbol option) | Papply of (apply_info * prevert option) | Pcut of pcut diff --git a/src/phl/ecPhlDeno.ml b/src/phl/ecPhlDeno.ml index 544e6f3086..8b0a32851f 100644 --- a/src/phl/ecPhlDeno.ml +++ b/src/phl/ecPhlDeno.ml @@ -383,9 +383,9 @@ let t_equiv_deno_bad2 pre bad1 tc = t_intros_i [hcpre; hequiv] @! t_real_le_trans fabs' @+ [ t_apply_prept (`UG real_eq_le) @! - process_congr @! (* abs *) - process_congr @~ (* add *) - (t_last process_congr) @~+ (* opp *) + (process_congr PCongrDefault) @! (* abs *) + (process_congr PCongrDefault) @~ (* add *) + (t_last (process_congr PCongrDefault)) @~+ (* opp *) [ t_pr_rewrite_i ("mu_split", Some bad1) @! t_reflex; t_pr_rewrite_i ("mu_split", Some bad2) @! t_reflex ] ; t_apply_prept (`UG real_upto) @+ diff --git a/tests/congr-pattern.ec b/tests/congr-pattern.ec new file mode 100644 index 0000000000..6b200913d2 --- /dev/null +++ b/tests/congr-pattern.ec @@ -0,0 +1,86 @@ +(* Tests for the [congr], [congr *] and [congr pat] tactics. *) + +require import AllCore. + +(* The autodischarge tactic [t_subgoal] used by [congr] tries + [t_assumption] (alpha) on each generated subgoal. To check that the + correct subgoals are produced, we therefore avoid having matching + hypotheses in scope at the point [congr] runs. *) + +(* -- regression: bare [congr] still works on f a = f b ---------------- *) +lemma test_default_congr (f : int -> int) (a b : int) : + a = b => f a = f b. +proof. move=> ?; congr; assumption. qed. + +(* -- [congr pat]: one hole; produces exactly [a = c] ----------------- *) +lemma test_pat_one_hole (f : int -> int -> int) (a b c : int) : + (c = a) => f a b = f c b. +proof. +move=> h; congr (f _ b). +(* the produced subgoal is [a = c]; [h] is [c = a] so plain assumption + does not close it (no eq_sym auto-orientation). *) +by rewrite h. +qed. + +(* -- [congr pat]: two holes; produces [a = c] then [b = d] ----------- *) +lemma test_pat_two_holes (f : int -> int -> int) (a b c d : int) : + (c = a) /\ (d = b) => f a b = f c d. +proof. +case=> hac hbd. +congr (f _ _). +- by rewrite hac. +- by rewrite hbd. +qed. + +(* -- [congr pat]: nested; produces [a = b] --------------------------- *) +lemma test_pat_nested (f g : int -> int) (a b : int) : + b = a => f (g a) = f (g b). +proof. +move=> h. +congr (f (g _)). +by rewrite h. +qed. + +(* -- [congr *]: two diffs; produces [a = a'] then [c = c'] ------------ *) +lemma test_star_two_diffs (f : int -> int -> int -> int) (a a' b c c' : int) : + (a' = a) /\ (c' = c) => f a b c = f a' b c'. +proof. +case=> haa hcc. +congr *. +- by rewrite haa. +- by rewrite hcc. +qed. + +(* -- [congr *]: reflexivity closes when sides are already equal ------- *) +lemma test_star_reflex (f : int -> int) (a : int) : + f a = f a. +proof. congr *. qed. + +(* -- [congr *]: descends through [if] --------------------------------- *) +lemma test_star_if (b : bool) (x x' y y' : int) : + (x' = x) /\ (y' = y) => (if b then x else y) = (if b then x' else y'). +proof. +case=> hx hy. +congr *. +- by rewrite hx. +- by rewrite hy. +qed. + +(* -- [congr *]: does NOT descend under a binder ----------------------- *) +lemma test_star_no_binder_descent (P Q : int -> bool) (a : bool) : + (forall x, Q x) = (forall x, P x) => + ((forall x, P x) /\ a) = ((forall x, Q x) /\ a). +proof. +move=> h. +congr *. +by rewrite h. +qed. + +(* -- [congr *]: no beta reduction ------------------------------------- *) +(* The two sides have different head shape ([Flambda] applied vs raw + [Flocal]); since [congr *] never reduces, this leaves the whole + equality as a single subgoal. *) +lemma test_star_no_beta (a b : int) : + (b = (fun x => x) a) => + ((fun x => x) a = b). +proof. move=> h; congr *; by rewrite h. qed.