variant syntax for `congr'`

Stream: metaprogramming / tactics

[Heather Macbeth]

The tactic congr' is supposed to be a more precise version of congr. You can specify the number of levels you want congr to break down an equality on, if you don't want it to go all the way. But sometimes a single level number is not precise enough, if there's a "tree" of matching with different desired levels on different branches.

import tactic

variables {X : Type*} [has_add X] {a b c d : X} (f : X → X)

example (H : true → a = b) (H' : true → f c = f d) : f a + f c = f b + f d :=
begin
  congr' 1,
  { congr,
    exact H trivial },
  { exact H' trivial }
end

example (H : true → a = b) (H' : true → c + (f a) = c + (f d)) (H'' : true → f d = f b) :
  f (f a) + (f d + (c + f a)) = f (f b) + (f b + (c + f d)) :=
begin
  congr' 1,
  { congr,
    exact H trivial },
  { congr' 1,
    { exact H'' trivial },
    { exact H' trivial } }
end

[Heather Macbeth]

What would people think of a more precise syntax for congr', modelled on change?

-- desired syntax
example (H : true → a = b) (H' : true → f c = f d) : f a + f c = f b + f d :=
begin
  congr' f _ + _,
  { exact H trivial }
  { exact H' trivial }
end

-- desired syntax
example (H : true → a = b) (H' : true → c + (f a) = c + (f d)) (H'' : true → f d = f b) :
  f (f a) + (f d + (c + f a)) = f (f b) + (f b + (c + f d)) :=
begin
  congr' f (f _) + (f _ + _),
  { exact H trivial },
  { exact H'' trivial },
  { exact H' trivial }
end

(I used these true → a = b hypotheses to mimic examples where each individual equality would be closed by some tactic, since congr' automatically picks up and applies equality hypotheses.).

[Eric Wieser]

This sounds a lot like the suggested congr macro from another thread

[Eric Wieser]

Namely, this one: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2313979.20arbitrary.20proof.20terms.20in.20.60linear_combination.60/near/281627870

[Eric Wieser]

(which is to say; I like this suggestion but wonder if we can combine the two somehow)

[Mario Carneiro]

I was aware of this issue when I first designed the syntax; my reasoning was that if you want an asymmetric descent you can use congr' 1 and then congr' n again in the subgoals

[Mario Carneiro]

By the way you can compress this into one line using congr' 1; [congr, skip] and congr' 1; [congr, congr' 1] in your examples respectively

[Gabriel Ebner]

congr f _ = _ is a lot more intuitive though.

[Eric Wieser]

It might make sense to use a different marker to _, so that we can distinguish "create a goal out of this hole" and "this bit is constant, work it out from the goal"

[Eric Wieser]

I guess to match pattern matching ._/ .(_) could be "don't make a goal out of this"

[Mario Carneiro]

yeah that part will be easier in lean 4 with _/?_

[Mario Carneiro]

I agree _ is a bad notation here, especially since in non-contrived examples writing the type of the goal can be really complicated and you want to omit anything you can to avoid spurious type errors

[Heather Macbeth]

Eric Wieser said:

It might make sense to use a different marker to _, so that we can distinguish "create a goal out of this hole" and "this bit is constant, work it out from the goal"

Yes, I agree this would be useful, although ideally both markers could be only one character long.

[Heather Macbeth]

Eric Wieser said:

This sounds a lot like the suggested congr macro from another thread

Namely, this one: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2313979.20arbitrary.20proof.20terms.20in.20.60linear_combination.60/near/281627870

@Kyle Miller's idea is for a tactic which acts on hypotheses: given the equality hypotheses H : a = b, H' : c + (f a) = c + (f d), H'' : f d = f b, it would create a hypothesis

f (f a) + (f d + (c + f a)) = f (f b) + (f b + (c + f d))

by writing

have := exact_congr f (f %!H) + (f %!H'' + %!H'),

whereas my idea is for a tactic which acts on goals: given the goal

f (f a) + (f d + (c + f a)) = f (f b) + (f b + (c + f d))

it would reduce this to goals a = b c + (f a) = c + (f d), f d = f b by writing

congr' f (f _) + (f _ + _)

I agree that there is some relationship (a bit subtle) and I think they would both be very useful!

[Heather Macbeth]

Maybe my idea amounts to

refine exact_congr f (f %!_) + (f %!_ + %!_)

if that will be permitted (although I think it's still nice to have this callable under the tactic name congr').

[Damiano Testa]

Heather, what you would like is to unify the input that you give with the target, returning the provided metavariables as side goals, right?

[Damiano Testa]

Maybe, trying congr on each side goal, would also make the _ that were in place to avoid rewriting some part of the expression deal with the "different" interpretations that _ might have.

[Heather Macbeth]

Sorry @Damiano Testa, I don't follow, can you explain?

[Heather Macbeth]

Damiano Testa said:

Heather, what you would like is to unify the input that you give with the target, returning the provided metavariables as side goals, right?

I'm not sure this is the same as what I'm asking -- the input f (f _) + (f _ + _) I'm suggesting is the "shared LHS/RHS pattern" of the target, not the target itself.

[Damiano Testa]

If I understood correctly, you would like something like

do t ← target,
 unify t (expr corresponding that what you provide),
return (all metavariable goals)

Is this clearer? Close to what you wanted?

[Heather Macbeth]

I think it's more like

do t ← target,
  e ← mk_app eq [(expr corresponding that what you provide), (expr corresponding that what you provide)]
 unify t e,

but I'm not very experienced at metaprogramming, so this is certainly incorrect in a literal sense!

[Damiano Testa]

Ah, I see! You are right. I had understood what you asked, but then messed up. Yes, in my pseudo-code above, I was thinking of providing

f (f _) + (f _ + _) = f (f _) + (f _ + _)

which, if I interpreted your version correctly, if what you wanted!

[Heather Macbeth]

But I want more than just the unification, right? I want to reduce the goal to a series of subgoals, one for each matching LHS/RHS pair of underscores.

[Damiano Testa]

Yes, I think that you would want each metavariable to be returned as a goal, possibly passed through a congr before that, in case it works.

[Damiano Testa]

something like match (your expr = your expr) with target, return metavariables as side-goals. Let me try!

[Damiano Testa]

(I am very new to meta-programming, so I am not very confident that I will get anywhere, but I like the challenge!)

[Heather Macbeth]

Please go ahead, I'd love to have this tactic!

As I said in the initial post, I imagine it as a variant of congr' and reusing most of the internals of that tactic. But it's true that my proposed input syntax provides more information than congr' 3 would (it provides the names of the functions, not just the number of function applications), so maybe this unification-based trick you're describing would work too.

[Damiano Testa]

I think that it will be some combination of match, unify, congr('). Maybe!

[Damiano Testa]

This does not work yet, but seems to go somewhere along the way. It made me realize that there might be a typo in your first desired syntax: an f for a g.

import tactic

namespace tactic.interactive
open tactic interactive
setup_tactic_parser

meta def mc_arg (prec : nat) : parser pexpr :=
parser.pexpr prec

meta def mca (arg : parse (mc_arg tac_rbp)) : tactic unit :=
do tgt ← target,
  (lhs, rhs) ← match_eq tgt,
  gl ← to_expr arg,
  e ← mk_app `eq [gl, gl],
  e1 ← mk_app `eq [tgt, e],
  n ← get_unused_name,
  assert n e1,
  congr
end tactic.interactive

variables {X : Type*} [has_add X] {a b c d : X} (f g : X → X)

-- desired syntax
example (H : true → a = b) (H' : true → g c = f d) : f a + g c = f b + f d := -- I changed an `f` to a `g`
begin
  mca f _ + _,  -- produces the "right" goals, but also an unwanted one
  { exact (H trivial).symm }, -- works
  { exact (H' trivial).symm }, -- works
-- the original goal persists
end

[Damiano Testa]

Ok, maybe it was not a typo in your first example, I think that I might have implemented congr in a less efficient way! :face_palm:

Maybe, instead of the last congr, I should use congr' 1 in some way.

Or maybe, I should try to unify the lhs and then congr the rhs.

[Mario Carneiro]

Actually, it's an interesting observation that unification does most of the work here. The way I imagine it, you take the expression with holes and elaborate it to an expr with metavariables. Then unify it with the LHS, producing an assignment of the metavariables. Then undo that unification to unassign the metavariables and unify it with the RHS, producing another assignment. Finally, for every metavariable generated by the original expression we take the two assignments to it and equate them, and those are the desired subgoals. (Filter out the ones that are defeq or other trivialities.)

[Damiano Testa]

Yes, I was now trying to parse two exprs simultaneously, matching on whether they were both has_add.add or both expr.app and if so, trying to unify the arguments (failing otherwise). But it would be useful to maybe have a type of "repeated exprs", so that it applies to expr = expr where you want do treat the two expr as equal...

[Damiano Testa]

(I'm not sure if what I said was comprehensible, I am still struggling with matches...)

[Damiano Testa]

What I had in mind is a function that takes to expr and returns a tactic (list expr). The first expr is the one assumed to have metavariables (eventually arising from the user input), the second one is the "full pattern" (eventually arising from the target).

[Damiano Testa]

Now you scan the two exprs, assuming that, where they differ, it is because there is a metavariable on the left. When you find a metavariable, you produce a goal between the "mirror images" of the actual terms arising from the second expr.

[Damiano Testa]

It might be simpler to match 3 exprs, assuming that they are "built in the same way, except that the first one might have mvars instead of actual info". Then, you look for places where the first has mvar, and you create a goal of the equality of the corresponding locations in the remaining two.

[Damiano Testa]

I'm going to have to take a break now, but this is roughly what I had in mind:

meta def mc : expr →expr →expr →tactic unit
| (expr.mvar n1 n2 e) f g := (make equation f=g)
| (expr.??? args) same same := make sure args match and descend
| _ _ _ := fail "sorry, no match"

This would be applied to (to_expr user_input) target_lhs target_rhs.

[Damiano Testa]

This is what I have, but does not enter enough into the expressions.

meta def mc_m : expr → expr → expr → tactic unit
| (expr.mvar n1 n2 e) f g := do trace "mvar", trace f, trace g,n ← get_unused_name,
                              fg ← mk_app `eq [f, g],
                              assert n fg, target >>= trace,
                              skip
| (expr.app f a) (expr.app g b) (expr.app h c) := do
  unify f g,
  mc_m a b c
| _ _ _ := fail "sorry, no match"

meta def ca (arg : parse (mc_arg tac_rbp)) : tactic unit :=
do tgt ← target,
  (lhs, rhs) ← match_eq tgt,
  gl ← to_expr arg,
  mc_m gl lhs rhs

I leave it here, but I won't be able to work on this further for a few hours.

mc should probably recurse into lam or pi, as well, possibly both?

After that, it will be a matter of rewriting the correct hypotheses and leave the leftover goals.

[Damiano Testa]

I almost have it!

I think that what is missing below is getting Lean to keep working on the "main" goal, instead of one of the side goals. The first "desired syntax" works with some permutation (and, once I learn how to choose on which goal to work, the rewrites should be automatable). The second one fails, but I think that the reason is that Lean starts working on a side-goal, instead of on the main one.

import tactic

namespace tactic.interactive
open tactic interactive
setup_tactic_parser

meta def mc_arg (prec : nat) : parser pexpr :=
parser.pexpr prec

meta def decomp : expr → expr → expr → tactic unit
| (expr.app f e) (expr.app f0 e0) (expr.app f1 e1) := do
  match e.is_mvar with
  | ff := decomp e e0 e1
  | tt := do el ← mk_app `eq [e0, e1],
             n ← get_unused_name "h",
             assert n el,
             rotate, -- instead of rotate, I would like to always work on the "original" goal
             decomp f f0 f1
             end
| _ _ _ := trace "nothing"

meta def dap (arg : parse (mc_arg tac_rbp)) : tactic unit :=
do ta ← to_expr arg tt ff,
  tgt ← target,
  (lhs, rhs) ← match_eq tgt,
  decomp ta lhs rhs,
  try refl

end tactic.interactive

variables {X : Type*} [has_add X] {a b c d : X} (f : X → X)


-- desired syntax
example (H : true → a = b) (H' : true → f c = f d) : f a + f c = f b + f d :=
begin
  dap f _ + _,
  rw [h, h_1],
  { exact H' trivial },
  { exact H trivial },

end

-- desired syntax
example (H : true → a = b) (H' : true → c + (f a) = c + (f d)) (H'' : true → f d = f b) :
  f (f a) + (f d + (c + f a)) = f (f b) + (f b + (c + f d)) :=
begin
  dap f (f _) + (f _ + _),
  { exact H trivial },
  { exact H'' trivial },
  { exact H' trivial },
end

[Damiano Testa]

EDIT: The above code should work!

[Damiano Testa]

Ok, I think that I got it!

It needs a lot of testing, but the code above works in the two given examples!

Note that I have a weird permutation of the goal showing up.

[Damiano Testa]

Btw, Heather, here:

example (H : true → a = b) (H' : true → c + (f a) = c + (f d)) (H'' : true → f d = f b) :
  f (f a) + (f d + (c + f a)) = f (f b) + (f b + (c + f d)) :=
begin
  congr' f (f _) + (f _ + _),
  ...
end

did you mean

H'': true → d = b  <--- removed `f`-application

?

[Damiano Testa]

(This is what Lean wants when I run the code above...)

[Heather Macbeth]

Maybe I stated my own desired syntax wrong, does it work with

example (H : true → a = b) (H' : true → c + (f a) = c + (f d)) (H'' : true → f d = f b) :
  f (f a) + (f d + (c + f a)) = f (f b) + (f b + (c + f d)) :=
begin
  congr' f (f _) + (_ + _),
  ...
end

[Damiano Testa]

Yes, this works:

example (H : true → a = b) (H' : true → c + (f a) = c + (f d)) (H'' : true → f d = f b) :
  f (f a) + (f d + (c + f a)) = f (f b) + (f b + (c + f d)) :=
begin
  dap f (f _) + (_ + _),
  { exact H' trivial },
  { exact H trivial },
  { exact H'' trivial },
end

[Damiano Testa]

(The permutation thing is still a little iffy.)

[Damiano Testa]

Ok, having found a typo in the proposed syntax test is a good check!

[Damiano Testa]

Obviously, this means that the tactic will always work... :upside_down:

[Heather Macbeth]

It's very cool, congrats! One thing that I don't immediately understand: why does your code also work for functions with multiple inputs like +?

[Damiano Testa]

Because expr.app plays well with curry!

[Damiano Testa]

+ is twice expr.app.

[Damiano Testa]

It has some test with unary and binary. Should work with n-ary, but I really would want to test it before making a bold statement.

[Heather Macbeth]

And what about Eric's idea to allow for holes in the function names, too? Does it work with

example (H : true → a = b) (H' : true → c + (f a) = c + (f d)) (H'' : true → f d = f b) :
  f (f a) + (f d + (c + f a)) = f (f b) + (f b + (c + f d)) :=
begin
  dap f (_ _) + (_ + _),
  { exact H' trivial },
  { exact H trivial },
  { exact H'' trivial },
end

[Damiano Testa]

Not sure about this, I'm skeptical for the code as is...

[Damiano Testa]

placeholders '_' cannot be used where a function is expected

sadly...

[Damiano Testa]

There is some room for getting the two "different" _, one where you want to create a goal and one where you want to unify since you know it works.

[Damiano Testa]

I have not played with that, but it should be doable, especially if I learn better how the parser works to distinguish the two.

[Damiano Testa]

Note that you can be sloppy with your pattern matching. Giving a multiplication to X, this still works:

example (H : true → a = b) (H' : true → c + (f a) = c + (f d)) (H'' : true → f d = f b) :
  f (f a) * (f d + (c + f a)) = f (f b) * (f b + (c + f d)) :=
begin
  dap f (f _) + (_ + _),  <--- note the `+` instead of `*`!!
  { exact H' trivial },
  { exact H trivial },
  { exact H'' trivial },
end

[Damiano Testa]

The pattern that you provide, is really just a canvas. Since you use function application, you mostly need the right arity and it might work.

[Damiano Testa]

I'm going to do some non-Lean stuff now, but would love to hear more comments!

[Heather Macbeth]

That's funny! Initially I was actually thinking of suggesting an input syntax as some kind of spelled-out tree, like

congr' (((x))(xx)))

which technically speaking is providing less information to Lean, but which is also much less human-parseable. I guess what you're saying is that your tactic would also work for that syntax.

[Damiano Testa]

I think that it might. When I'm back at a computer, I'll try with a unary and a binary function from a different type and will see how the matching goes!

[Damiano Testa]

I just tried it: this works.

example {A : Type*} (j₂ : A → A → A) (j₁ : A → A)
  (H : true → a = b) (H' : true → c + (f a) = c + (f d)) (H'' : true → f d = f b) :
  f (f a) * (f d + (c + f a)) = f (f b) * (f b + (c + f d)) :=
begin
  dap j₂ (j₁ (j₁ _)) (j₂ _ _),
  { exact H' trivial },
  { exact H trivial },
  { exact H'' trivial },
end

example {A : Type*} (j₂ : A → A → A) (j₁ : A → A) (w : A)
  (H : true → a = b) (H' : true → c + (f a) = c + (f d)) (H'' : true → f d = f b) :
  f (f a) * (f d + (c + f a)) = f (f a) * (f b + (c + f d)) :=
begin
  dap j₂ (j₁ (j₁ w)) (j₂ _ _),
  { exact H'' trivial },
  { exact H' trivial },
end

[Damiano Testa]

In fact, I had initially placed some test that there was a compatibility between the pattern in the user-provided input and the one found in the lhs/rhs, but eventually decided against.

Still, I am amazed at how well Lean understands this very hard to parse statement!

[Damiano Testa]

Looking back at the code above, I think that replacing rotate_right 1 with swap will generate the side goals in reverse order, with respect to the "obvious" one. However, I switched off the computer for the day and am not able to check it.

If it is a desirable feature, I can try to produce code with "natural ordering" of the side-goals.

[Damiano Testa]

Also, currently the code only descends into function applications. It will stop with everything else. It is probably easy to make the matching extend much deeper into the expression, if needed.

[Damiano Testa]

Just to get some further comments:
#14153

[Damiano Testa]

Btw, Gabriel, I am trying to get the apply_eq_congr_core to work, but with little success for now. I am thinking of extracting the wanted goals and using simp only [extracted equalities] to simplify the initial goal, leaving side-goals to prove the extracted equalities. Would this be suitable?

[Gabriel Ebner]

simp only [h] could loop in some cases.

[Damiano Testa]

I could do a single_pass... Although, I feel that I am trying to avoid using the apply_eq_congr_core, mostly because I do not understand it and am unable to get it to work...

[Gabriel Ebner]

Another issue. Say you have the pattern f _ _ and the equation f a (a + b) = f b b. First you rewrite with a = b, this turns the goal into f b (b + b) = f b b. But now you can no longer rewrite with a + b = b (from the second underscore).

[Damiano Testa]

Yes, this is what I was hoping to cure by letting simp do its magic... :upside_down:

[Damiano Testa]

And also the reason for extracting all the goals upfront, so that they don't get messed up by the intermediate rw.

[Damiano Testa]

I will keep trying with apply_eq_congr_core: I agree that it feels more robust, but I do not understand it.

[Gabriel Ebner]

Yeah, the API is a bit tricky because you manually need to juggle the arguments and proof terms. This should work though:

private meta def extract_subgoals : list expr → list congr_arg_kind → list expr →
  tactic (list (expr × expr))
| (_ :: _ :: g :: prf_args) (congr_arg_kind.eq :: kinds) (pat :: pat_args) :=
  (λ rest, (g, pat) :: rest) <$> extract_subgoals prf_args kinds pat_args
| (_ :: prf_args) (congr_arg_kind.fixed :: kinds) (_ :: pat_args) :=
  extract_subgoals prf_args kinds pat_args
| prf_args (congr_arg_kind.fixed_no_param :: kinds) (_ :: pat_args) :=
  extract_subgoals prf_args kinds pat_args
| (_ :: _ :: prf_args) (congr_arg_kind.cast :: kinds) (_ :: pat_args) :=
  extract_subgoals prf_args kinds pat_args
| _ _ [] := pure []
| _ _ _ := fail "unsupported congr lemma"

meta def equate_with_pattern_core : expr → tactic (list expr) | pat :=
(applyc ``subsingleton.elim >> pure []) <|>
(applyc ``rfl >> pure []) <|>
if pat.is_mvar || pat.get_delayed_abstraction_locals.is_some then
  get_goals <* set_goals []
else if pat.is_app && pat.get_app_fn.is_constant then do
  cl ← mk_specialized_congr_lemma pat,
  [prf] ← get_goals,
  tactic.apply cl.proof,
  prf ← instantiate_mvars prf,
  set_goals [],
  subgoals ← extract_subgoals prf.get_app_args cl.arg_kinds pat.get_app_args,
  subgoals ← subgoals.mmap (λ ⟨subgoal, subpat⟩, do
    set_goals [subgoal],
    equate_with_pattern_core subpat),
  pure subgoals.join
else if pat.is_lambda then do
  applyc ``_root_.funext,
  x ← tactic.intro pat.binding_name,
  equate_with_pattern_core $ pat.lambda_body.instantiate_var x
else do
  pat ← pp pat,
  fail $ to_fmt "unsupported pattern:\n" ++ pat

meta def equate_with_pattern (pat : expr) : tactic unit := do
congr_subgoals ← tactic.solve1 (equate_with_pattern_core pat),
gs ← get_goals,
set_goals $ congr_subgoals ++ gs

[Damiano Testa]

Gabriel, thank you so much for the code! I will try to understand this a little and will PR it with some tests, adding you as a coauthor, if that is ok with you. Or feel free to push to the branch directly, if you prefer. :namaste:

[Gabriel Ebner]

Great! I've added some tests and docstrings.

[FR]

import tactic.congrm

example {f g : ℕ → ℕ → ℕ} (h : f = g) : (λ i j, f i j) = (λ i j, g i j) :=
begin
  congrm λ i j, _,
  sorry,
end

Is it possible to support multiple arguments in lambda expressions?

[Gabriel Ebner]

Oh, it returns (λ j, f i j) = λ j, g i j. That's a bug.

[Gabriel Ebner]

#14753

[Damiano Testa]

Dear All,

#14532 introduces "function underscores" for use with congrm. This is to implement one of Heather's suggestions further up in this thread (I'm on mobile and cannot post the exact link).

The PR introduces notation _ᵢ for an unspecified function with arity i. Does anyone have any opinion on the matter?

Thanks!

[Heather Macbeth]

@Damiano Testa I noticed that the parsing for congrm seems to interpret the ; as part of the expression, at least in the following example:

import tactic.congrm
import tactic.norm_num

-- fails with `unknown identifier 'norm_num'`
example {f : ℕ → Prop} :
  (∃ k, f (3 + 2 + k) ∨ f (8 + 1 + k)) ↔ ∃ k, f (1 + 4 + k) ∨ f (2 + 7 + k) :=
by congrm ∃ k, f (_ + k) ∨ f (_ + k); norm_num

-- works
example {f : ℕ → Prop} :
  (∃ k, f (3 + 2 + k) ∨ f (8 + 1 + k)) ↔ ∃ k, f (1 + 4 + k) ∨ f (2 + 7 + k) :=
by congrm (∃ k, f (_ + k) ∨ f (_ + k)); norm_num

Is there any way to prevent this behaviour?

[Damiano Testa]

Heather, thanks for reporting this! I will take a look and will try to fix it. It probably has to do with changing the binding power of some parsed argument. I hope to have time either today or tomorrow to look at this.

[Damiano Testa]

@Heather Macbeth , I have investigated this a bit and I do not know how to fix it. I think that I have minimized further your example:

import tactic.congrm

--  unknown identifier 'assumption'
example {p q r s : Prop} (pr : p ↔ r) (qs : q ↔ s) :
  p ∧ q ↔ r ∧ s :=
by congrm _ ∧ _; assumption

--  works
example {p q r s : Prop} (pr : p ↔ r) (qs : q ↔ s) :
  p ∧ q ↔ r ∧ s :=
by congrm (_ ∧ _); assumption

If I had to guess, I think that the priority of ∧ (as well as ∨) interacts badly with the "right-binding strength" of the argument to congrm. Still, I do not know how to fix this.

Maybe @Gabriel Ebner can help?

[Damiano Testa]

In fact, I am unable to find where the notation for docs#and is defined.

[Heather Macbeth]

Thanks Damiano, this already taught me something!

[Damiano Testa]

Glad to hear!

Although, I would like to get to the bottom of this: after all, the argument to congrm is already a parse texpr which is supposed to terminate with ;. See the docstring to docs#interactive.types.texpr. I'm not sure why it does not work.

[Damiano Testa]

#15074 is a partial fix to this issue: the minimized version that I have above is resolved, but Heather's first bug stays.

Any help is appreciated! :smile:

[Damiano Testa]

Actually, here is something that I had not realized:

import tactic.congrm

-- works
example {f : ℕ → Prop} :
  (∃ k, f (3 + 2 + k) ∨ f (8 + 1 + k)) ↔ ∃ k, f (1 + 4 + k) ∨ f (2 + 7 + k) :=
by congrm ∃ k, f (_ + k) ∨ f (_ + k)

Note: no parentheses and side-goals solved by reflexivity. I do not know why the ; norm_num could not be tagged along, but this already "works".

[Heather Macbeth]

I guess because equalities between natural numbers are true by definition, if very slowly. I should have come up with a test case where you truly did need the tactic, sorry!

[Damiano Testa]

I still think that it is interesting that with the parentheses it does work, while without it does not.

[Damiano Testa]

Notice that congrm attempts rfl, so I think that it should be congrm closing those nat goals, not norm_num in both cases. The ; should simply be informing Lean to apply the following tactic to all, non-existent, remaining goals.

I do not know why it fails in one case and succeeds in the other.

[Damiano Testa]

It seems that and does not have much to do with this issue.

import tactic.congrm

--  works
example {a : Prop} :
  (∃ k : Prop, a) ↔ ∃ k : Prop, a :=
by congrm (∃ k, _); refl

--  fails
example {a : Prop} :
  (∃ k : Prop, a) ↔ ∃ k : Prop, a :=
by congrm ∃ k, _; refl
/-
type mismatch at application
  ?m_4; refl
term
  refl
has type
  ∀ (a : ?m_1), ?m_2 a a : Prop
but is expected to have type
  ?m_1 : Type ?
-/

[Gabriel Ebner]

Both of the examples for ∧ work for me. But the ∃ requires parentheses even with other tactics like have so I don't think we can do much there.

import logic.basic
example : 1 = 1 := by have : ∃ x : nat, true; simp -- unknown identifier 'simp'
example : 1 = 1 := by have : (∃ x : nat, true); simp

[Damiano Testa]

Gabriel, thanks for the confirmation!

I am not sure where I got the issue with ∧, maybe some weird problem with old oleans. They do work now. I will close the PR then, since this is not really an issue with congrm, then!

[Damiano Testa]

The ∃ issue might have to do with the fact that , is allowed "inside" the ∃ syntax, and then it might get tricky to allow ; but not ,.

Anyway, I'm satisfied with the current state!