Zulip Chat Archive

Stream: general

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):

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 cc and simp) skips all arguments that are have a subsingleton instance. For congr and 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: Dec 20 2023 at 11:08 UTC