Looking for a tactic

Stream: new members

[Henrik Rueping]

Is there a tactic that simplifies a goal of the form

if P(x) then 1 else 0 =0

to P(x).
P(x) is a rather complicated expression. I think I could do it with have :P(x):=by ... and then use simp[this]. But it would be simpler if there was a tactic that simplifies the if away.

[Kyle Miller]

You could try using the split tactic. It's not exactly what you suggest, but it might help you avoid writing P(x).

[Kevin Buzzard]

Or you could prove that if a \ne b and if if P then a else b = a then P separately (for an abstract P) as a preliminary lemma (with split), and then just apply that.

[Kevin Buzzard]

(right now what you posted simplifies to \not P by the way) (and the backticks you want are ``` not ´´´ )

[Henrik Rueping]

With a usual simp? Hm strange. I did not write out what P is, because I hoped that this would not have an effect, it is just a rather complicated expression.

[Kevin Buzzard]

import Mathlib

lemma foo {P : Prop} [Decidable P] {X : Sort*} {a b : X} (h : a ≠ b)
    (h2 : (if P then a else b) = a) : P := by
  revert h2
  split <;> aesop

example (verylongproposition : Prop) [Decidable verylongproposition]
    (h : (if verylongproposition then 1 else 0) = 1) :
    verylongproposition := by
  -- note that the proof never mentions `verylongproposition`
  apply foo _ h
  simp

[Mauricio Collares]

I'm surprised a lemma like (c : Prop) [d : Decidable c] {α : Sort u} {t e : α} (h : e ≠ t) : @ite c d t e = t ↔ c doesn't already exist, though.

[Ruben Van de Velde]

I think I saw something similar recently, but where...

[Ruben Van de Velde]

Can't find it, though. This is an alternative proof:

lemma foo {P : Prop} [Decidable P] {X : Sort*} {a b : X} (h : a ≠ b)
    (h2 : (if P then a else b) = a) : P := by
  rw [ite_eq_left_iff] at h2
  exact of_not_not <| mt h2 h.symm

[Yaël Dillies]

docs#Ne.ite_eq_left_iff