congr: add congr pat and congr * variants

src/ecHiGoal.ml

@@ -2258,8 +2258,11 @@ let process_exists args (tc : tcenv1) =
   EcLowGoal.t_exists_intro_s args tc
 
 (* -------------------------------------------------------------------- *)
-let process_congr tc =
-  let (env, hyps, concl) = FApi.tc1_eflat tc in
+(* Common scaffolding for [congr], [congr *] and [congr /pat]: setup the
+   [t_ensure_eq] coercion (iff -> eq when needed) and the auto-discharge
+   tactic for trivial subgoals. *)
+let process_congr_setup tc =
+  let (_env, _hyps, concl) = FApi.tc1_eflat tc in
 
   if not (EcFol.is_eq_or_iff concl) then
     tc_error !!tc "goal must be an equality or an equivalence";
@@ -2279,6 +2282,15 @@ let process_congr tc =
 
   let t_subgoal = t_ors [t_reflex ~mode:`Alpha; t_assumption `Alpha; t_id] in
 
+  (f1, f2, iseq, t_ensure_eq, t_subgoal)
+
+(* -------------------------------------------------------------------- *)
+(* 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
+  let (f1, f2, iseq, t_ensure_eq, t_subgoal) = process_congr_setup tc in
+  let _ = concl in
+
   match f1.f_node, f2.f_node with
   | _, _ when EcReduction.is_alpha_eq hyps f1 f2 ->
       FApi.t_seq t_ensure_eq EcLowGoal.t_reflex tc
@@ -2306,6 +2318,173 @@ let process_congr tc =
 
   | _, _ -> tacuerror "not a congruence"
 
+(* -------------------------------------------------------------------- *)
+(* Given a skeleton [skel] containing free locals [holes = (xi, tyi)],
+   a left vector [lvec] and a right vector [rvec] of the same length and
+   types, discharge an equality goal [f1 = f2] where
+     skel[xi := Li] is convertible to f1
+   and
+     skel[xi := Ri] is convertible to f2.
+
+   The discharge proceeds by:
+     1. ensuring the goal is an equality (vs iff);
+     2. changing it to [(\xi. skel) Li... = (\xi. skel) Ri...] (beta);
+     3. unfolding the congruence one step per hole with [t_congr];
+     4. auto-closing trivial side goals (reflexivity / assumption). *)
+let process_congr_from_skeleton ~holes ~skel ~lvec ~rvec tc =
+  let (f1, _f2, _iseq, t_ensure_eq, t_subgoal) = process_congr_setup tc in
+
+  if List.is_empty holes then
+    FApi.t_seq t_ensure_eq EcLowGoal.t_reflex tc
+  else
+    let ty = f1.f_ty in
+    let bds = List.map (fun (x, t) -> (x, EcAst.GTty t)) holes in
+    let lam = EcFol.f_lambda bds skel in
+    let app_lhs = EcFol.f_app lam lvec ty in
+    let app_rhs = EcFol.f_app lam rvec ty in
+    let newgoal = EcFol.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 (EcLowGoal.t_change1 newgoal tc));
+       tcgr;
+       t_subgoal]
+      tc
+
+(* -------------------------------------------------------------------- *)
+(* [congr /pat]: pattern matches both sides; one subgoal per pattern
+   variable (skipping syntactically-equal sides). *)
+let process_congr_pattern p tc =
+  let (_env, hyps, _concl) = FApi.tc1_eflat tc in
+  let (f1, f2, _iseq, _t_ensure_eq, _t_subgoal) = process_congr_setup tc in
+
+  let (ps, ue), pat_f = TTC.tc1_process_pattern tc p in
+  let pvars = Mid.keys ps in
+  let ev0 = EcMatching.MEV.of_idents pvars `Form in
+
+  let match_side label side =
+    let ue' = EcUnify.UniEnv.copy ue in
+    let ev' = ev0 in
+    try
+      let (ue'', _, ev'') =
+        EcMatching.f_match EcMatching.fmsearch hyps (ue', ev') pat_f side
+      in (ue'', ev'')
+    with EcMatching.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 env = FApi.tc1_env tc in
+  let substL = EcMatching.MEV.assubst ueL evL env in
+  let substR = EcMatching.MEV.assubst ueR evR env in
+
+  (* For each pattern variable [x], get its binding on both sides by
+     substituting [f_local x] (with a fresh unification type that the
+     subst will refine to the matched term's type). *)
+  let holes_full =
+    List.map (fun x ->
+      let probe_ty = EcUnify.UniEnv.fresh ueL in
+      let probe    = EcFol.f_local x probe_ty in
+      let li = EcCoreSubst.Fsubst.f_subst substL probe in
+      let ri = EcCoreSubst.Fsubst.f_subst substR probe in
+      (x, li.EcAst.f_ty, li, ri)
+    ) pvars
+  in
+
+  (* Drop holes whose two sides are alpha-equal: they do not generate a
+     subgoal (and including them in the skeleton would be harmless but
+     noisy). *)
+  let kept =
+    List.filter (fun (_, _, li, ri) -> not (EcReduction.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
+
+  (* Rebuild the skeleton from the original pattern, substituting away the
+     dropped pattern variables with their (alpha-equal) bound form. *)
+  let dropped =
+    List.filter (fun (_, _, li, ri) -> EcReduction.is_alpha_eq hyps li ri)
+      holes_full
+  in
+  let skel =
+    List.fold_left (fun acc (x, _, li, _) ->
+      EcCoreSubst.Fsubst.f_subst_local x li acc) pat_f dropped
+  in
+
+  process_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 process_congr_star tc =
+  let (env, hyps, _concl) = FApi.tc1_eflat tc in
+  let (f1, f2, _iseq, _t_ensure_eq, _t_subgoal) = process_congr_setup 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.EcAst.f_ty) :: !holes;
+    lvec  := l :: !lvec;
+    rvec  := r :: !rvec;
+    EcFol.f_local x l.EcAst.f_ty
+  in
+
+  let rec walk (l : form) (r : form) : form =
+    if EcReduction.is_alpha_eq hyps l r then
+      l
+    else
+      match l.EcAst.f_node, r.EcAst.f_node with
+      | Fapp (hL, aL), Fapp (hR, aR)
+          when    EcReduction.is_alpha_eq hyps hL hR
+               && List.length aL = List.length aR
+               && EcReduction.EqTest.for_type env l.EcAst.f_ty r.EcAst.f_ty ->
+          let args' = List.map2 walk aL aR in
+          EcFol.f_app hL args' l.EcAst.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
+          EcFol.f_if c' t' e'
+
+      | Ftuple xs, Ftuple ys when List.length xs = List.length ys ->
+          let zs = List.map2 walk xs ys in
+          EcFol.f_tuple zs
+
+      | Fproj (xL, iL), Fproj (xR, iR)
+          when iL = iR
+            && EcReduction.EqTest.for_type env l.EcAst.f_ty r.EcAst.f_ty ->
+          EcFol.f_proj (walk xL xR) iL l.EcAst.f_ty
+
+      | _, _ ->
+          if not (EcReduction.EqTest.for_type env l.EcAst.f_ty r.EcAst.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
+
+  process_congr_from_skeleton ~holes ~skel ~lvec ~rvec 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

src/ecHiGoal.mli

@@ -91,7 +91,7 @@ val process_split       : ?i:int -> 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

src/ecHiTacticals.ml

@@ -137,7 +137,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

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 }

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

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) @+

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.