congr and subsingleton.elim

Stream: mathlib4

[Johan Commelin]

In some proof, after congr I'm left with the goal inst✝ = Fintype.subtype s H.
Does congr in Lean 4 not know about Subsingleton.elim?

[Johan Commelin]

Should we have a congr! that knows about Subsingleton.elim? And then mathport can translate congr to congr!.

[Kyle Miller]

congr doesn't seem to know about iffs either, and I ported some instances of it as apply iff_of_eq; congr. This was part of mathlib's congr' (implemented here)

[Kyle Miller]

Maybe it would be nice if a congr! would try doing "rfl lifting," where it synthesizes and applies a theorem a = b -> R a b if the target R is reflexive.

[Kyle Miller]

Though that could be considered to be be too aggressive (it'd apply even to a <= b). Maybe applying to just reflexive & symmetric relations is a better default.

[Kyle Miller]

Or alternatively there could be an attribute for congr! lemmas in general. Then both Subsingleton.elim and rfl lifting lemmas could plug into this.

[Eric Wieser]

Kyle Miller said:

Though that could be considered to be be too aggressive (it'd apply even to a <= b).

I think this is fine for the congr' n version where the depth can be specified

[Moritz Doll]

Another shortcoming of congr is that it does not know about pi_congr

[Kyle Miller]

Here's a prototype:

prototype of congr!

/-
Copyright (c) 2023 Kyle Miller. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kyle Miller
-/
import Lean
import Mathlib.Tactic.Relation.Rfl

import Mathlib.Tactic.RunCmd
import Mathlib.Data.Multiset.Basic
import Mathlib.Data.Fintype.Basic

/-!
# The `congr!` tactic

This is a more powerful version of the `congr` tactic.
-/

open Lean Meta Elab Tactic

/--
Asserts the given congruence theorem as fresh hypothesis, and then applies it.
Return the `fvarId` for the new hypothesis and the new subgoals.
-/
private def applyCongrThm? (mvarId : MVarId) (congrThmType congrThmProof : Expr) :
    MetaM (List MVarId) := do
  let mvarId ← mvarId.assert (← mkFreshUserName `h_congr_thm) congrThmType congrThmProof
  let (fvarId, mvarId) ← mvarId.intro1P
  let mvarIds ← mvarId.apply (mkFVar fvarId) { synthAssignedInstances := false }
  mvarIds.mapM fun mvarId => mvarId.tryClear fvarId

/--
Try applying user-provided congruence lemmas. If any are applicable,
returns a list of new goals.
-/
def Lean.MVarId.userCongr? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
  mvarId.withContext do
    mvarId.checkNotAssigned `userCongr?
    let some (lhs, _) := (← mvarId.getType').eqOrIff? | return none
    let some name := lhs.getAppFn.cleanupAnnotations.constName? | return none
    let congrTheorems := (← getSimpCongrTheorems).get name
    -- Note: congruence theorems are in provided in decreasing order of priority.
    for congrTheorem in congrTheorems do
      let res ← observing? do
        let cinfo ← getConstInfo congrTheorem.theoremName
        let us ← cinfo.levelParams.mapM fun _ => mkFreshLevelMVar
        let proof := mkConst congrTheorem.theoremName us
        let ptype ← instantiateTypeLevelParams cinfo us
        applyCongrThm? mvarId ptype proof
      if let some mvars := res then
        return mvars
    return none

/--
Try to convert an `Iff` into an `Eq` by applying `iff_of_eq`.
If successful, returns the new goal, and otherwise returns the original `MVarId`.
-/
def Lean.MVarId.iffOfEq (mvarId : MVarId) : MetaM MVarId :=
  mvarId.withContext do
    let some [mvarId] ← observing? do mvarId.apply (mkConst ``iff_of_eq []) | return mvarId
    return mvarId

/--
Try to convert an `Eq` into an `Iff` by applying `propext`.
If successful, then returns then new goal, otherwise returns the original `MVarId`.
-/
def Lean.MVarId.propext (mvarId : MVarId) : MetaM MVarId :=
  mvarId.withContext do
    let some [mvarId] ← observing? do mvarId.apply (mkConst ``propext []) | return mvarId
    return mvarId

/-- Helper theorem for `LEan.MVar.liftReflToEq`. -/
theorem Lean.MVarId.rel_of_eq_and_refl {R : α → α → Prop} (hxy : x = y) (h : R x x) :
    R x y := hxy ▸ h

/--
Use a `refl`-tagged lemma to convert the goal into an `Eq`. If this can't be done, returns
the original `MVarId`.
-/
def Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do
  mvarId.checkNotAssigned `liftReflToEq
  let tgt ← withReducible <| mvarId.getType'
  let .app (.app rel _) _ := tgt | return mvarId
  if rel.isAppOf `Eq then
    -- No need to lift Eq to Eq
    return mvarId
  let reflLemmas ← (Mathlib.Tactic.reflExt.getState (← getEnv)).getMatch rel
  for lem in reflLemmas do
    let res ← observing? do
      -- First create an equality relating the LHS and RHS
      -- and reduce the goal to proving that LHS is related to LHS.
      let [mvarIdEq, mvarIdR] ←
            mvarId.apply (← mkConstWithFreshMVarLevels ``Lean.MVarId.rel_of_eq_and_refl)
        | failure
      -- Then fill in the proof of the latter by reflexivity.
      let [] ← mvarIdR.apply (← mkConstWithFreshMVarLevels lem) | failure
      return mvarIdEq
    if let some mvarId := res then
      return mvarId
  return mvarId

/--
Try to close the goal using `Subsingleton.elim`. Returns whether or not it succeeds.
-/
def Lean.MVarId.subsingletonElim (mvarId : MVarId) : MetaM Bool := do
  let some [] ← observing? do mvarId.apply (mkConst ``Subsingleton.elim [← mkFreshLevelMVar])
    | return false
  return true

def Lean.MVarId.proofIrrelHeq (mvarId : MVarId) : MetaM Bool := do
  let some [] ← observing? do mvarId.apply (mkConst ``proof_irrel_heq [])
    | return false
  return true

/--
Try to apply `pi_congr`. This is similar to `Lean.MVar.congrImplies?`.
-/
def Lean.MVarId.congrPi? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
  observing? do mvarId.apply (← mkConstWithFreshMVarLevels ``pi_congr)

/--
Try to apply `funext`, but only if it is obviously an equality of two functions
(we do not want this to apply to equalities of sets).
"Obvious" means that the type of the terms being equated is a pi type.
-/
def Lean.MVarId.obviousFunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
  observing? do
    let tgt ← mvarId.getType'
    let some (ty, _, _) := tgt.eq? | failure
    let .forallE .. ← Lean.instantiateMVars ty | failure
    mvarId.apply (← mkConstWithFreshMVarLevels ``funext)

/--
Try to apply `Function.hfunext`, returning the new goals if it succeeds.
Like `Lean.MVarId.obviousFunext?`, we only do so if both sides of the `HEq` are terms
of pi types. This is to prevent unfolding of things like `Set`.
-/
def Lean.MVarId.obviousHfunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
  observing? do
    let tgt ← mvarId.getType'
    let some (ty1, ty2, _, _) := tgt.heq? | failure
    let .forallE .. ← Lean.instantiateMVars ty1 | failure
    let .forallE .. ← Lean.instantiateMVars ty2 | failure
    mvarId.apply (← mkConstWithFreshMVarLevels ``Function.hfunext)

/-- The list of passes used by `Lean.MVarId.congrCore!`. -/
def Lean.MVarId.congrPasses! : List (MVarId → MetaM (Option (List MVarId))) :=
  [userCongr?, congr?, hcongr?, obviousFunext?, obviousHfunext?, congrImplies?, congrPi?]

/-- Convert a goal into an `Eq` goal if possible (since we have a better shot at those).
Also try to dispatch the goal using an assumption, `Subsingleton.Elim`, or definitional equality. -/
def Lean.MVarId.preCongr! (mvarId : MVarId) : MetaM (Option MVarId) := do
  -- User congr lemmas might have created additional hypotheses.
  let (_, mvarId) ← mvarId.intros
  -- Next, turn `HEq` and `Iff` into `Eq`
  let mvarId ← mvarId.heqOfEq
  -- This is a good time to check whether we have a relevant hypothesis.
  if ← mvarId.assumptionCore then return none
  let mvarId ← mvarId.iffOfEq
  -- Now try definitional equality. No need to try `mvarId.hrefl` since we already did  `heqOfEq`.
  try withReducible mvarId.refl; return none catch _ => pure ()
  -- Now we go for (heterogenous) equality via subsingleton considerations
  if ← mvarId.subsingletonElim then return none
  if ← mvarId.proofIrrelHeq then return none
  return some mvarId

def Lean.MVarId.congrCore! (mvarId : MVarId) : MetaM (List MVarId) := do
  /- We do `liftReflToEq` here rather than in `preCongr!` since we don't want it to stick
     if there are no relevant congr lemmas. -/
  let mvarId ← mvarId.liftReflToEq
  for pass in congrPasses! do
    if let some mvarIds ← pass mvarId then
      return mvarIds
  throwTacticEx `congr! mvarId "failed to apply congruence"

/-- A pass to clean up after `Lean.MVarId.preCongr!` and `Lean.MVarId.congrCore!`. -/
def Lean.MVarId.postCongr! (mvarId : MVarId) : MetaM (Option MVarId) := do
  let some mvarId ← mvarId.preCongr! | return none
  -- Convert `p = q` to `p ↔ q`, which is likely the more useful form:
  let mvarId ← mvarId.propext
  if ← mvarId.assumptionCore then return none
  return some mvarId

/-- A more insistent version of `Lean.MVarId.congrN`. -/
def Lean.MVarId.congrN! (mvarId : MVarId) (depth : Nat := 1000000) : MetaM (List MVarId) := do
  let (_, s) ← go depth mvarId |>.run #[]
  return s.toList
where
  post (mvarId : MVarId) : StateRefT (Array MVarId) MetaM Unit := do
    let some mvarId ← mvarId.postCongr! | return
    modify (·.push mvarId)
  go (n : Nat) (mvarId : MVarId) : StateRefT (Array MVarId) MetaM Unit := do
    let some mvarId ← mvarId.preCongr! | return
    match n with
      | 0 => post mvarId
      | n + 1 =>
        let some mvarIds ← observing? (m := MetaM) mvarId.congrCore!
          | post mvarId
        mvarIds.forM (go n)

syntax (name := congr!) "congr! " (num)? : tactic

elab_rules : tactic
| `(tactic| congr! $[$n]?) =>
  let hugeDepth := 1000000
  let depth := n.map (·.getNat) |>.getD hugeDepth
  liftMetaTactic fun g ↦ g.congrN! depth

example (inst1 inst2 : Fintype α) : inst1 = inst2 := by
  congr!

example : ((n : Nat) → Fin (1 + n)) = ((n : Nat) → Fin (n + 1)) := by
  congr! 2
  -- ⊢ 1 + n = n + 1
  rw [add_comm]

@[congr]
lemma List.map_congr' (xs ys : List α) (f g : α → β) (hfg : ∀ x, x ∈ xs → f x = g x) (h : xs = ys) :
    List.map f xs = List.map g ys := by
  cases h
  exact List.map_congr hfg

example (xs ys : List α) (f g : α → β) (h : xs = ys) (h : ∀ x, x ∈ ys → f x = g x) :
    List.map f xs = List.map g ys := by
  congr!
  -- given x : α and x ∈ xs then ⊢ f x = g x
  subst_vars
  rwa [h]

example (x y : Nat) (h : x = y) : 1 + x ≤ 1 + y := by
  congr!

example (p q r : Prop) (h : q → r) : p ∧ q ↔ p ∧ q ∧ r := by
  congr!
  -- ⊢ q ↔ q ∧ r
  constructor
  · intro hq
    exact ⟨hq, h hq⟩
  · rintro ⟨hq, _⟩
    assumption

example (x y : Nat) (h : x = y) : HEq x y := by
  congr!

example : (fun n : Nat => n + n) = (fun n : Nat => 2 * n) := by
  congr!
  rw [two_mul]

example (p q : Prop) (hp : p) (hq : q) : HEq hp hq := by
  congr!

[Kyle Miller]

Along with some examples:

example (inst1 inst2 : Fintype α) : inst1 = inst2 := by
  congr!

example : ((n : Nat) → Fin (1 + n)) = ((n : Nat) → Fin (n + 1)) := by
  congr! using 2
  -- ⊢ 1 + n = n + 1
  rw [add_comm]

@[congr]
lemma List.map_congr' (xs ys : List α) (f g : α → β) (hfg : ∀ x, x ∈ xs → f x = g x) (h : xs = ys) :
    List.map f xs = List.map g ys := by
  cases h
  exact List.map_congr hfg

example (xs ys : List α) (f g : α → β) (h : xs = ys) (h : ∀ x, x ∈ ys → f x = g x) :
    List.map f xs = List.map g ys := by
  congr!
  -- given x : α and x ∈ xs then ⊢ f x = g x
  subst_vars
  rwa [h]

example (x y : Nat) (h : x = y) : 1 + x ≤ 1 + y := by
  congr!

example (p q r : Prop) (h : q → r) : p ∧ q ↔ p ∧ q ∧ r := by
  congr!
  -- ⊢ q ↔ q ∧ r
  constructor
  · intro hq
    exact ⟨hq, h hq⟩
  · rintro ⟨hq, _⟩
    assumption

example (x y : Nat) (h : x = y) : HEq x y := by
  congr!

example : (fun n : Nat => n + n) = (fun n : Nat => 2 * n) := by
  congr!
  rw [two_mul]

[Kyle Miller]

Features:

• It can apply user congr lemmas
• It can use refl lemmas to lift goals to proving an Eq
• It knows about funext, propext, and congr_pi
• It knows about Subsingleton
• Rather than leaving a goal as p = q, it will turn it back to p <-> q

[Kyle Miller]

There's a bug if you use it on expressions involving Set at the moment, but congr has the same issue (see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mkCongrSimp.3F.20error.20for.20Set/near/338881269)

[Kyle Miller]

One feature I didn't mention is that, to support being able to apply user congr lemmas recursively, it does intros for you. For example, List.map_congr' in the examples has an extra membership hypothesis.

If you need to name the extra hypotheses, I think a reasonable interface is that you can follow it up with rename_i.

[Johan Commelin]

Could you also take a list of names via a with clause?

[Kyle Miller]

That would make it a lot more complex, since it would need to thread that list of available names through everything.

I was sort of thinking about how with clauses were a solution to the problem that Lean 3 had no concept of inaccessible names.

[Yuyang Zhao]

I remember that in lean3 congr (or congr') also knows docs#proof_irrel_heq and ext knows docs#function.hfunext. But in lean4 they do not know.

[Kyle Miller]

@Yuyang Zhao Thanks, I added proof_irrel_heq.

I why docs4#Function.hfunext isn't tagged with @[ext]. Is this a limitation with ext or due to some other reason?

[Yuyang Zhao]

ext lemmas in Lean4 are required to output an Eq iirc.

[Eric Wieser]

(deleted)

[Kyle Miller]

There's a PR for congr!: mathlib4#2566

Part of it is changing convert to use it instead of congr, since that's closer to how convert worked in mathlib3, and this is also a good test to see how whether congr! is an improvement.

[Kyle Miller]

Maybe now's a good time for a request for comment about congr! before I get too much deeper into getting mathlib4 to compile.

[Kyle Miller]

I've been able to compile mathlib4 locally with the new congr!-powered convert in mathlib4#2566

[Kyle Miller]

It seems to me that there were no regressions (other than needing to be explicit with some universe variables, since otherwise Subsingleton.elim is overly eager to turn Sort _ into Prop).

[Kyle Miller]

Of course, since it's able to dig deeper into expressions sometimes a given convert might now need a using nn to limit it from going too far.

[Johan Commelin]

Great news!

[Johan Commelin]

PLMC = Paris Lean Meta Club

you guys are our life line :life_preserver: :rofl:

[Kyle Miller]

I'm excited that congr! knows about user congruence lemmas. I'd tried changing congr' to do this in mathlib3, but getting it to work with with-variables in a robust way, and then figuring out how to get mathlib to compile after these changes, it was too much work.

[Kyle Miller]

Here's an example of what user congruence lemmas give us:

import Mathlib

open BigOperators

example : ∑ n in Finset.Icc 0 5, (n - 5) = ∑ n in Finset.Icc 0 5, 0 := by
  congr! -- automatically applies Finset.sum_congr
  rename_i n h
  -- h : n ∈ Finset.Icc 0 5
  -- ⊢ n - 5 = 0
  apply tsub_eq_zero_of_le
  simpa using h

[Kyle Miller]

Kyle Miller said:

It seems to me that there were no regressions (other than needing to be explicit with some universe variables, since otherwise Subsingleton.elim is overly eager to turn Sort _ into Prop).

This ended up being straightforward to implement a fix. Rather than using Lean.MVarId.apply to apply the Subsingleton.elim lemma, the trick was to take the goal lhs = rhs and use mkAppM ``Subsingleton.elim #[lhs, rhs] and assign the resulting proof directly.

The key is that mkAppM uses withNewMCtxDepth so it doesn't unify any metavariables. (That way docs4#instSubsingleton doesn't give Lean any bright ideas that things would be much easier if that Sort _ were just Prop.)

[Kyle Miller]

I thought I'd mention that I've been working on further improvements to congr! in mathlib4#2606.

Something I noticed is that docs4#Lean.Meta.mkCongrSimp? can generate lemmas that are more specialized than you might like. For example, in f x = g y it can only generate lemmas like forall a b, a = b -> f a = f b, where f is the same on both sides. Also, when there are dependent types it can make certain arguments to an application fixed. This is all fine for congr lemmas for simp, but if our aim is to be able to equate every part of the two sides of anything and everything, this isn't sufficient.

Internally, congr! is happy working with HEq, so in this PR there's a congruence lemma generator that's similar to docs4#Lean.Meta.mkHCongrWithArity, but it has a couple extra features.

1. It can make use of Subsingleton instances to omit hypotheses immediately.
2. For each successive hypothesis, it includes all the previous equalities between variables this particular argument depends on (so for example, if you want to prove the equality ⟨a, x⟩ = ⟨b, y⟩ by congr!, the second goal will end up with a = b in the context).
3. You can request that the function and/or certain arguments be fixed (we can look at the arguments of the functions we're doing congr! on to see which ones are defeq), which can help produce HEq-free goals.

This last feature also helps to_additive since the resulting congruence lemma is more amenable to being to-additivized, otherwise you get bare algebraic functions that aren't applied to anything amidst a mess of Eq/HEq recursors.

[Kyle Miller]

Sometimes, though, this new congruence generator is too good at finding a way to make two sides of something equal, so the PR also needs to pepper mathlib with using clauses to limit it. I'm also limiting congr!'s ability to unfold definitions by only permitting reducible transparency by default; there are some places where convert was being used to deliberately unfold definitions, in a questionably reliable way, so either these have been rewritten or convert has been given a configuration option to use default transparency.

[Kyle Miller]

To give an example of it being too good and doing congruence is the following:

example (prime : Nat → Prop) (n : Nat) (h : prime (2 * n + 1)) :
    prime (n + n + 1) := by
  convert h
  -- goal 1: ⊢ HAdd.hAdd = HMul.hMul -- specialized to `Nat -> Nat -> Nat`
  -- goal 2: ⊢ n = 2

There are two solutions. One is to use using 2 to get ⊢ n + n = 2 * n. The other is to use a pre-defined collection of configuration options that keep convert/congr! from equating different functions.

example (prime : Nat → Prop) (n : Nat) (h : prime (2 * n + 1)) :
    prime (n + n + 1) := by
  convert (config := .unfoldSameFun) h
  -- goal: ⊢ n + n = 2 * n

These options allow definition unfolding at default transparency and also disallow congruence between partially-applied functions, and it makes it behave sort of like congr but with extra bells and whistles. This .unfoldSameFun config is not necessarily better or worse than the default congr! settings, but you can get different results with them, some worse some better.

[Kyle Miller]

Something I don't fully understand is a certain pattern I've seen a number of times, where convert is used for Funlike in a seemingly trivial way, for example closing a goal with by convert FunLike.ext_iff.1 hfg using 0.

In every case, using 0 works for these (which means the goal is just closed by Iff.rfl!). I think this is all being used as a fancy way to elaborate without an expected type, but I couldn't get other tricks for this to work in these cases. If anyone is interested, you can look for using 0 in the PR.