ite term golf

Stream: general

[Andrew Ashworth]

Suppose I need to prove ite (x = y) tt ff = tt → x = y and x = y → ite (x = y) tt ff = tt. Is there a succint way to do this in term mode? (I know simp and split_ifs is amazing here, but I'd like to do inversion by hand if possible)

[Nicholas Scheel]

this should take care of the second part: https://github.com/leanprover/lean/blob/master/library/init/logic.lean#L839

[Nicholas Scheel]

for the first part I wonder if something like the following would work (untested):

λ h,
if p : (x = y) then p else
  bool.no_confusion (eq.trans (eq.symm h) (if_neg p))

basically you decide the proposition (equivalent to the by_cases tactic) and then return the true case, or prove the false case is absurd

[Nicholas Scheel]

maybe this is easier than no_confusion: https://github.com/leanprover/lean/blob/master/library/init/logic.lean

[Nicholas Scheel]

absurd (eq.symm (eq.trans .....)) bool.ff_ne_tt

[Nicholas Scheel]

btw I think this is just if p then tt else ff: https://github.com/leanprover/lean/blob/master/library/init/logic.lean#L590

[Mario Carneiro]

use to_bool, it has lots of lemmas for this

[Andrew Ashworth]

thanks Nicholas / Mario for the pointers