congr tactic: first steps

Stream: mathlib4

[Siddhartha Gadgil]

I have made my first attempts at congr tactic. It does cover the two examples at https://leanprover-community.github.io/mathlib_docs/tactics.html#congr (including the congr' example). It is verbose however, and does not cover the rcasesPat part. I am sharing below for comments.

Also, can someone point me to docs/examples for the rcasesPat part (I have no idea what that is).

def congrStep? (closeOnly : Bool)(mvar: MVarId) : MetaM (Option (List MVarId)) := do
  let u ← mkFreshLevelMVar
  let v ← mkFreshLevelMVar
  try
    let res ←  Meta.apply mvar (mkConst ``Eq.refl [u])
    if res.isEmpty then return some [] else pure none
  catch _ =>
  try
    let res ←  Meta.apply mvar (mkConst ``Subsingleton.intro [u])
    if res.isEmpty then return some [] else pure none
  catch _ =>
  if !closeOnly then
    try
      let res ←  Meta.apply mvar (mkConst ``congr [u, v])
      return some res
    catch e =>
      pure none
  else
    pure none

partial def recCongr(maxDepth? : Option Nat)(mvar: MVarId) : MetaM (List MVarId) := do
  let closeOnly : Bool := (maxDepth?.map (fun n => decide (n ≤  1))).getD false
  let res ← congrStep? closeOnly mvar
  match res with
  | some [] => return []
  | some xs => do
    let depth? := maxDepth?.map (fun n => n - 1)
    let groups ← xs.mapM (recCongr depth?)
    return groups.bind fun x => x
  | none => return [mvar]

def Meta.congr(maxDepth? : Option Nat)(mvar : MVarId) : MetaM (List MVarId) := do
  try
    let u ← mkFreshLevelMVar
    let v ← mkFreshLevelMVar
    let xs ← Meta.apply mvar (mkConst ``congr [u, v])
    let groups ← xs.mapM (recCongr maxDepth?)
    return groups.bind fun x => x
  catch e =>
    throwTacticEx `congr mvar m!"congr tactic failed"

open Lean.Elab.Tactic

syntax (name := congrTactic) "congr" (ppSpace (colGt num))? : tactic
@[tactic congrTactic] def congrTacticImpl : Tactic := fun stx =>
match stx with
| `(tactic|congr $(x?)?) =>
  withMainContext do
    let x? := x?.map <| fun card => (Syntax.isNatLit? card).get!
    liftMetaTactic (Meta.congr x?)
| _ => throwIllFormedSyntax

example (x y w: Nat)(f g: Nat → Nat): x * f y = g w * f z := by
  congr
  repeat (exact sorry)

example (x y : Nat)(f g: Nat → Nat): f (g (x + y)) = f (g (y + x)) := by
  congr 2 -- goal remaining : x + y = y + x
  skip
  repeat (exact sorry)

[Arthur Paulino]

rcasesPat is declared (and expanded) here

[Siddhartha Gadgil]

Thanks. What would it mean to have such a pattern in the congr tactic?

[Arthur Paulino]

I don't know :D
But I think Mario or Gabriel will be able to explain

[Siddhartha Gadgil]

@Gabriel Ebner Can I ask what it means to say congr with (x, y) or some other such pattern? Should one try to match both sides of an equality to the pattern, or the full proposition? Is it done before, after, or instead of function application?
Or is it something entirely different?

[Floris van Doorn]

In lean 3 it's just that rcases is being applied to the introduced variable(s) with that pattern (or rintro)

[Siddhartha Gadgil]

I see.
Does this mean that after each iteration of apply congr I should call rcases on the returned variables? With a failure not being an error, but just not decomposing further?

[Mario Carneiro]

src#tactic.interactive.congr'

[Mario Carneiro]

the two parts are not intermingled, and you can probably just write it as a macro tactic. It does (congr n with pats) := focus (congr n <;> ext pats)

[Mario Carneiro]

(For this kind of tactic implementation I do recommend reading the source of the original tactic to get the control flow right)

[Siddhartha Gadgil]

Thanks. Indeed I should look at lean 3 mathlib and the already implemented tactics more.
In this case:

• there is non congr (yet?) in lean 4, and the syntax seems to be for a single congr tactic covering various cases; so stuff does not directly translate.
• I see at https://github.com/leanprover-community/mathlib4/blob/226f899cb18cb76990f480dd8b79b6d341e44797/Mathlib/Tactic/Ext.lean#L145 that the case of ext that must be called is not ready yet (and when ready it seems easy enough to call).

So it seems the best I can do now is do what congr and congr' did in mathlib for lean 3. I will try to streamline my code, and any suggestions to improve it are very welcome.

[Siddhartha Gadgil]

Apologies @Mario Carneiro : I see that lean 3 docs clearly say ext is used with given pattern. I will read these with care in the future.

[Mario Carneiro]

I mean the source specifically, not just the docs. Sometimes the docs are vague about what happens in such and such edge case, but you can find out by reading the source and/or doing some unit testing of the tactic

[Mario Carneiro]

I believe that congr should exist in lean 4 for the same reason it existed in lean 3: it was originally written as an internal mechanism for simp to be able to traverse inside terms, and it was later exposed as a standalone tactic

[Siddhartha Gadgil]

I realized that, but it is more egregious to miss something in the docs. As I started using lean 4 without using lean 3 more than a tiny amount, I have not gotten the habit of looking at the lean 3 sources (while learning most things by trawling the lean 4 source).

I see meanwhile that ext now supports the rintro syntax. I will try to cover that case too.

[Siddhartha Gadgil]

Specific question: @Gabriel Ebner and @Mario Carneiro : the (unimplemented) syntax of congr uses rcasesPat while the syntax of extuses rintroPat. On the other hand a TODO in ext mentioned rcasesPat as intended syntax.

My question: is this a result of everything being in a transient state, or is the intention that ext is called after relating the two types of patterns (I can see that they are related)?

[Mario Carneiro]

The lean 4 tactics are intended to be an exact match (or possibly a superset) for the corresponding lean 3 tactics. So the source of truth here is whatever is in mathlib

[Mario Carneiro]

For tactics that do a list of name introductions with pattern matching, rintroPat makes more sense. Note that rintroPat is a superset of rcasesPat, which supports binders like (a b c : Nat) that would not make sense as a cases/obtain pattern e.g. obtain (a b c: Nat) := foo

[Mario Carneiro]

So IMO both congr and ext should use rintroPat

[Siddhartha Gadgil]

I have made a pull request at https://github.com/leanprover-community/mathlib4/pull/247. As far as I can tell this is correct in the basic cases. I could not test the case with patterns.

If there is something I should change to fit in with the porting plans (or because it is wrong) please let me know. I plan to try implementing symm, trans and rfl' next (modeled on the ext implementation).

[Siddhartha Gadgil]

Incidentally, ext gives a confusing error message when the tactic fails, saying incorrect syntax and including a whole block (maybe it is trying to parse the whole block as a tactic).

[Mario Carneiro]

#mwe?

[Mario Carneiro]

That sounds like a bug in the parser or the input, so what does the input look like?

[Siddhartha Gadgil]

Modified from the test file:

example (a b : C n) : a = b := by
  ext x

[Siddhartha Gadgil]

Since ext x is perfectly valid syntax which works elsewhere, I would expect a failed tactic, but we get incorrect syntax.
I get a similar error elsewhere, but that could be my mistake.

[Siddhartha Gadgil]

I guess the above was not self-contained, so here is a fuller example (the above is ext.lean modified).

import Mathlib.Tactic.Ext
import Mathlib.Init.Logic

structure A (n : Nat) where
  a : Nat

structure B (n) extends A n where
  b : Nat
  h : b > 0
  i : Fin b

@[ext] structure C (n) extends B n where
  c : Nat

example (a b : C n) : a = b := by
  ext x

[Mario Carneiro]

The ext attribute before the example is throwing several index out of bounds errors

[Siddhartha Gadgil]

I see that too. Had not noticed.

[Mario Carneiro]

Note that one way tactics can "throw an error" is throwUnsupportedSyntax which is usually used to allow overlapping syntaxes to take a shot at interpreting the input. I guess this is what it looks like if nothing is found

[Siddhartha Gadgil]

I checked in mathlib4 and all cases I see of throwUnsupportedSyntax are the fallback case in a pattern match.

[Siddhartha Gadgil]

I am puzzled by this being triggered in a context dependent way, i.e., not just the syntactic context.

[Mario Carneiro]

it's also used by things like macro_rules and elab_rules as the implicit fallback

[Mario Carneiro]

I don't see evidence that this is not simply a syntactic issue

[Siddhartha Gadgil]

In the same file, the following is valid

example (f g : Nat × Nat → Nat) : f = g := by
  ext x

but the following is not

example (a b : C n) : a = b := by
  ext x

[Mario Carneiro]

I think rintro is throwing the exception

[Mario Carneiro]

because ext x expands to apply_ext_lemma; rintro x; skip

[Siddhartha Gadgil]

I see. My main concern is somewhere else where I have seemingly identical code which works if entered by hand but not by macros. I feel this may be related.

[Mario Carneiro]

I think it's a precedence issue in rintroPat

[Siddhartha Gadgil]

Here is the full code (the macro is based on what you said).

import Lean.Meta
import Mathlib.Mathport.Syntax
import Mathlib.Tactic.Ext

namespace Mathlib.Tactic.Congr
open Lean Meta Elab

/-- try to close goal using reflexivity and subsingletons -/
def tryCloseGoal (mvar: MVarId) : MetaM Bool := do
  try
    let res ←  Meta.apply mvar (← mkConstWithFreshMVarLevels ``Eq.refl)
    unless res.isEmpty do
      throwError "failed to close goal"
    pure true
  catch _ =>
  try
    let res ←  Meta.apply mvar (← mkConstWithFreshMVarLevels ``Subsingleton.intro)
    unless res.isEmpty do
      throwError "failed to close goal"
    pure true
  catch _ =>
    pure false

/-- apply `congr` after trying to close goal, optionally return result if successful -/
def congrStep? (mvar: MVarId) : MetaM (Option (List MVarId)) := do
  let closed  ← tryCloseGoal mvar
  if !closed then
    try
      let res ←  Meta.apply mvar (← mkConstWithFreshMVarLevels ``congr)
      return some res
    catch e =>
      pure none
  else
    pure none

/-- recursively apply congr and try to close goals, not an error if tactics fail -/
partial def recCongr(maxDepth? : Option Nat)(mvar: MVarId) : MetaM (List MVarId) := do
  let closeOnly : Bool := (maxDepth?.map (fun n => decide (n ≤  1))).getD false
  if closeOnly then
    let  chk ← tryCloseGoal mvar
    if chk then return [] else return [mvar]
  let res ← congrStep? mvar
  match res with
  | some [] => return []
  | some xs => do
    let depth? := maxDepth?.map (fun n => n - 1)
    let groups ← xs.mapM (recCongr depth?)
    return groups.bind id
  | none => return [mvar]

/-- apply `congr` and then continue recursively; error if first application fails -/
def Meta.congr(maxDepth? : Option Nat)(mvar : MVarId) : MetaM (List MVarId) := do
  try
    let u ← mkFreshLevelMVar
    let v ← mkFreshLevelMVar
    let xs ← Meta.apply mvar (mkConst ``congr [u, v])
    let groups ← xs.mapM (recCongr maxDepth?)
    return groups.bind id
  catch e =>
    throwTacticEx `congr mvar e.toMessageData

open Lean.Elab.Tactic

syntax (name := congrBase) "congr_base" (ppSpace (colGt num))? : tactic

/--
The `congr` tactic attempts to identify both sides of an equality goal `A = B`, leaving as new goals the subterms of `A` and `B` which are not definitionally equal. Example: suppose the goal is `x * f y = g w * f z`. Then congr will produce two goals: `x = g w` and `y = z`.

If `x y : t`, and an instance subsingleton t is in scope, then any goals of the form `x = y` are solved automatically.

The `congr` tactic, but takes an optional argument which gives
the depth of recursive applications.
* This is useful when `congr` without a depth bound is too aggressive in breaking down the goal.
* For example, given `⊢ f (g (x + y)) = f (g (y + x))`, `congr'` produces the goals `⊢ x = y`
  and `⊢ y = x`, while `congr' 2` produces the intended `⊢ x + y = y + x`.
* If, at any point, a subgoal matches a hypothesis then the subgoal will be closed.
-/
@[tactic congrBase] def congrTacticImpl : Tactic := fun stx =>
match stx with
| `(tactic|congr_base $(x?)?) =>
  withMainContext do
    let x? := x?.map <| fun card => (Syntax.isNatLit? card).get!
    liftMetaTactic (Meta.congr x?)
| _ => throwIllFormedSyntax

macro_rules
| `(tactic| congr $(x?)?) => do
    `(tactic|congr_base $(x?)?)
| `(tactic| congr $(x?)? with $xs) => do
    `(tactic| congr_base $(x?)?; ext $xs)

example (x y w: Nat)(f g: Nat → Nat): x * f y = g w * f z := by
  congr
  have : x = g w := sorry
  assumption
  have : y = z := sorry
  assumption

example (x y : Nat)(f g: Nat → Nat): f (g (x + y)) = f (g (y + x)) := by
  congr 2
  have : x + y = y + x := sorry
  assumption

example (x y : Nat)(f g: Nat → Nat): f (x + y) = (g (y + x)) := by
  -- congr 2 with x
  congr_base 2; ext x
  admit
  admit
  admit

[Siddhartha Gadgil]

If I uncomment the commented line close to the end and comment the next, I get the error unexpected syntax with the block just like that inserted by hand giving an error.
I don't understand macros well, so assumed it was my error. But I see the behaviour that I at least do not expect elsewhere, and suspect these are related.

[Mario Carneiro]

I minimized the issue to the following:

import Lean

elab "fails" : tactic => throwError "nope"

syntax "foo" (ppSpace ident)? : tactic
macro_rules | `(tactic| foo) => `(tactic| skip)
macro_rules | `(tactic| foo $x:ident) => `(tactic| fails; skip)

example : True := by foo x

[Mario Carneiro]

The problem seems to be that when a macro has multiple macro_rules definitions, if all of the definitions fail (in any way, not just by throwUnsupportedSyntax) then it throws a syntax error instead of the result of the (first? last?) tactic

[Mario Carneiro]

which makes me think that it is best not used as a control flow mechanism in nontrivial cases

[Mario Carneiro]

the macro in question is ext_or_simp btw

[Mario Carneiro]

and this syntax error is going to bubble up to ext and congr that call this tactic internally

[Siddhartha Gadgil]

A lot of the lean 4 tactics seem to be implemented at Meta/Elab level and chained that way.

[Siddhartha Gadgil]

Perhaps that is the most robust approach.

[Siddhartha Gadgil]

Call things as functions, rather than manipulate syntax.

[Siddhartha Gadgil]

I am very biased by being much more comfortable with the non-syntactic style.

[Mario Carneiro]

I also think that elab tactics are superior: you have more control, less overhead, and a reasonable programming language to work in

[Mario Carneiro]

I would only prefer macro tactics for trivial syntactic manipulations. Even something like repeat is a bit of a stretch to do as a recursive macro expansion

[Siddhartha Gadgil]

What has happened here is that I had to go to a syntactic level as the tactics to use are at macro level. Best may be to move to something else for now without this problem (e.g. an attempt at symm).

[Arthur Paulino]

Mario Carneiro said:

less overhead

Why do elab tactics have less overhead? I thought it was more expensive to lift a TacticM monad

[Mario Carneiro]

lifting is usually negative work: there is some small overhead to prepare the input and output but most of the execution is now happening in a smaller monad which means less things to pass around on every step

[Mario Carneiro]

the thing that makes macro tactics expensive is that you are constantly parsing and reinterpreting syntax into expressions

[Mario Carneiro]

if you use repeat to execute exact foo a bunch of times it has to parse and elaborate the syntax foo into an expression many times

[Mario Carneiro]

whereas if you have a MetaM tactic foo will usually be an Expr already

[Arthur Paulino]

Got it. And then calling evalTactic ⋯ inside TacticM is even more expensive I presume?

[Mario Carneiro]

it's about the same cost as a macro tactic

[Mario Carneiro]

probably a bit less since you aren't calling expandMacros too

[Mario Carneiro]

On the other hand, interactive tactics do a lot of things for you and when you take it into your own hands you have to make sure to do all the side stuff

[Mario Carneiro]

for example this is needed for getting go-to-definition on a binder to work

[Mario Carneiro]

eventually we will reimplement these things enough times that the common utilities will naturally be discovered

[Siddhartha Gadgil]

Some updates: now I cover the ext case as well at least in a basic example. I had to struggle a bit to pass around the syntax, and things worked when - as @Mario Carneiro said should be the case - I changed rcasesPat to rintroPatin the syntax for congr (otherwise when the syntax was passed around it was no longer recognized).

Can I request a review @Mario Carneiro @Gabriel Ebner ? This looks to me like a largely correct implementation, and before trying more implementations I want to understand how this matches with the maintainers expectations.

[Mario Carneiro]

I suspect that just calling apply congr isn't going to work in dependent situations. Did you take a look at how simp is currently doing congruence and whether you can reuse that backend?

[Mario Carneiro]

You should try porting the lean 3 tests for congr if there are any; you need more dependent function and subsingleton tests, for example congruence of if expressions

[Mario Carneiro]

I think you should look into src4#Lean.Meta.CongrTheorem and src#tactic.congr

[Siddhartha Gadgil]

Thanks @Mario Carneiro - I will read the sources you mention and look for tests.

[Mario Carneiro]

the main logic is in src4#Lean.Meta.Simp.simp which clearly has a congruence component, but it's not clear how extractable it is from the simp core

[Mario Carneiro]

I think you want to adapt tryAutoCongrTheorem? to do something similar but call congr instead of simp recursively

[Siddhartha Gadgil]

Yes, it does look like much of the work is done there. On the other hand, I believe simp will not resolve f x = g y to goals f = g and x = y, as congr should. I will digest the code and then get back to trying to implement a better congr.

I should also follow the same congr_core pattern as the lean implementation (with updated syntax).

[Mario Carneiro]

We aren't using simp directly here, so the question is closer to whether simp is capable of performing simplifications when they are available in both f and x. And it looks like it is:

example (h1 : (f : α → β) = g) (h2 : x = y) : f x = g y := by simp [h1, h2]

[Mario Carneiro]

congr uses the same steps as simp, it just does the subgoal management differently

[Siddhartha Gadgil]

Shouldn't congr break up f x = g y into f = g and x = y, as apply congr will? I agree with your point that most (perhaps all) of the non-trivial stuff done will overlap with simp, and indeed the code for simp shows this.

[Siddhartha Gadgil]

Okay, I see from the lean 3 code that one matches for a (heterogeneous) equality, then looks if the lhs is a function application and if it is uses the same stuff as in simplification.

[Siddhartha Gadgil]

In lean 4 there are methods Expr.eq? and Expr.heq? which do the matching (I have used the former a fair bit). So one can glue these with appropriately extracted code from simp (which I have to digest further to know what is the appropriate code).