forall congr

Stream: general

[Violeta Hernández]

I have not once gotten forall_congr to fire with congr

[Violeta Hernández]

Anyone knows what's up with that?

[Violeta Hernández]

It really stifles the tactic

[Eric Wieser]

Does congr even work on iffs?

[Violeta Hernández]

Wait, it doesn't?

[Violeta Hernández]

I thought I was just unlucky at getting it to fire

[Violeta Hernández]

Are you supposed to do propext, congr then?

[Eric Wieser]

import tactic

example {a b c : ℕ} : a = b ↔ a = c :=
begin
  congr',  --  only the primed version works
  sorry
end

[Eric Wieser]

You could change docs#tactic.congr_core' to support this

[Eric Wieser]

I assume you want it to do intros too?

[Eric Wieser]

What should it do if the variables have different names on each side?

[Eric Wieser]

That is, what do you want the goal state to be here?

example {b d : ℕ} : (∀a, a = b) ↔ (∀ c, c = d) :=
begin
  my_congr,
  -- ???
end

[Violeta Hernández]

I'd expect it to use either of the possible names

[Violeta Hernández]

Wouldn't matter too much which one

[Damiano Testa]

According to congrm, this is what you get:

import tactic.congrm

example {b d : ℕ} : (∀a, a = b) ↔ (∀ c, c = d) :=
begin
  congrm ∀a, _ = _,
  -- ⊢ b = d
end

[Violeta Hernández]

By the way, am I doing something wrong? congr' isn't doing anything here:

import order.order_iso_nat

example {α : Type*} [partial_order α] :
  (∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬a n < a m) ↔
  ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → a n = a m :=
by { congr', sorry }

[Eric Wieser]

congr' doesn't know about forall either, but we can trivially modify it so that it does

[Damiano Testa]

Again, congrm, though with some help:

example {α : Type*} [partial_order α] :
  (∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬a n < a m) ↔
  ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → a n = a m :=
by { congrm (∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → (_ : Prop)),
  -- ⊢ ¬⇑a n < ⇑a m ↔ ⇑a n = ⇑a m
 sorry }

[Violeta Hernández]

Thanks! This is precisely what I was looking for

[Damiano Testa]

Great to hear this! Heather wanted this "congr extension" and I think that it is a very good idea. It works on the assumption that the lhs and rhs have a similar pattern and it gives you the possibility of putting underscores on the "differing" parts, to create side-goals.

Since it works mostly up to defeq, being "the same" can be stronger or weaker than you pretty-print.

[Eric Wieser]

I think it would stil
Damiano Testa said:

According to congrm, this is what you get:

This nicely sidesteps the problem of coming up with names due to the pattern containing the names in the first place

[Kyle Miller]

Violeta Hernández said:

I have not once gotten forall_congr to fire with congr

The short answer to this is that congr does not use user @[congr] lemmas. It only uses congr lemmas generated by docs#tactic.mk_congr_lemma and friends -- these are the automatically synthesized lemmas that simp uses to navigate equalities and heterogeneous equalities.

[Kyle Miller]

User @[congr] lemmas are only used in the inner workings of simp, so they're not useless. (I was surprised they weren't used by congr -- I'd spent a good amount of time trying to figure out what I was doing wrong to get them to fire before I realized this).

[Damiano Testa]

While I do not understand how the mk_congr_lemmas are generated, the same is also true of congrm. Except, that since the user provides a canvas to congrm for how to snake through the congruences, it can reach where congr does not.

[Kyle Miller]

I had started modifying congr' to make use of user congruence lemmas, but it had far-reaching effects since it's used in many places and I didn't want to go through mathlib to fix everything at the time.

[Kyle Miller]

mk_congr_lemma lemmas are generated in the C++ side. Roughly, it looks at a function application, sees what kinds of arguments it has, then generates a custom congruence lemma for the situation. It takes into account things like decidable being a subsingleton.

[Damiano Testa]

Kyle, thanks, this helps a bit! I had explored those C++ generated congr_lemmas via traceing them, but it was somewhat inefficient and left several doubts. In particular, I had completely missed decidable issues.

[Kyle Miller]

Here's a description of each of the argument kinds: https://github.com/leanprover-community/lean/blob/master/src/library/congr_lemma.h#L13

Here's the same thing on the Lean side (though the docstring is a bit out of date): docs#congr_arg_kind

[Damiano Testa]

Thanks! Honestly, I still find it cryptic, but having seen them in action, made me accept them "a little"! :upside_down: