Topic: congr tactic
Sean Leather (Mar 01 2018 at 13:28):
How do I know when to use the
congr tactic? It's not in the Lean reference. Are there any good examples? I should've learned already, but I'm slow. :simple_smile:
Gabriel Ebner (Mar 01 2018 at 13:29):
As a motivating example you could try it on
a + b + c = a + c + b and see what subgoals you get.
Sean Leather (Mar 01 2018 at 13:31):
state: 2 goals a b c : ℕ ⊢ b = c a b c : ℕ ⊢ c = b
Gabriel Ebner (Mar 01 2018 at 13:31):
With regards to the other thread: congr (and all other uses of congruence lemmas in lean such as
simp) skips all arguments that are have a
subsingleton instance. For
cc this means you don't need to explicitly show that they're equal. For
simp this means you can't rewrite there.
Gabriel Ebner (Mar 01 2018 at 13:34):
Looking back, this may have been a bad example. The point is: if you have an equality, then
congr stubbornly reduces it to equalities of subterms (the topmost positions where the two sides differ, that is).
Last updated: Aug 03 2023 at 10:10 UTC