Tactic to no tactic

Stream: general

[Nima]

Is there an easy way to re-write the last function without using tactic?

section
parameters (p : Prop) [decidable p]
def cnd₁ : Prop := sorry
def cnd₂ : Prop := sorry
def check : Prop := if p then cnd₁ else cnd₂
def f₁ (c:cnd₁) : nat := sorry
def f₂ (c:cnd₂) : nat := sorry
def f  (c:check): nat := -- if p then f₁ cnd₁ else f₂ cnd₂
begin
  by_cases p ; simp [check,h] at c,
  exact f₁ c,
  exact f₂ c,
end
end

[Mario Carneiro]

theorem check_of_p (h : p) : check ↔ cnd₁ := iff_of_eq (if_pos h)
theorem check_of_not_p (h : ¬ p) : check ↔ cnd₂ := iff_of_eq (if_neg h)

def f (c:check) : nat :=
if h : p then
  f₁ ((check_of_p h).1 c)
else
  f₂ ((check_of_not_p h).1 c)

[Nima]

Thank you, if_pos and if_neg are what I was looking for.

def f' (c:check): nat :=
  if h:p then f₁ (eq.mp (if_pos h) c)
  else        f₁ (eq.mp (if_neg h) c)

[Kenny Lau]

Nima beats Mario

[Mario Carneiro]

I wrote it that way for a reason. You should not rely on definitional expansion in this way as it is brittle. The point of the lemma is to isolate the unfolding of check so that this isn't happening in an ambiguous context

[Mario Carneiro]

The usage of iff is by convention since these are propositions