not_or_not in TBA course

Stream: lean4

[Kevin Buzzard]

Idle thoughts, nothing important. I was trying the exercises in @Sebastian Ullrich 's course, and I was proving not_or_not. With match it's fine:

theorem not_or_not : (¬p ∨ ¬q) → ¬(p ∧ q) := λ h ⟨hp, hq⟩ =>
match h with
| Or.inl h1 => h1 hp
| Or.inr h2 => h2 hq

But without it I tried

theorem not_or_not : (¬p ∨ ¬q) → ¬(p ∧ q) := λ h ⟨hp, hq⟩ => h.rec _ _

and instead of both underscores being underlined in red so I can fill them in, the entire h.rec _ _ is underlined in red with a type mismatch error. I'm assuming this is some unification issue (I don't really know what higher order unification is but this is usually what people say is the problem when this sort of thing happens), so I fix it with the funky new @-free trick

theorem not_or_not : (¬p ∨ ¬q) → ¬(p ∧ q) := λ h ⟨hp, hq⟩ =>
h.rec (motive := (λ x => False)) _ _

and now I do get the underscores, but the goals are annoyingly ∀ (h : ¬p), (fun (x : ¬p ∨ ¬q) => False) (Or.inl h) i.e. non-beta-reduced. I beta-reduced them in my head and made it home, but I couldn't figure out a neat way of getting Lean to do it: for example

theorem not_or_not : (¬p ∨ ¬q) → ¬(p ∧ q) := λ h ⟨hp, hq⟩ =>
h.rec (motive := (λ x => False)) (λ h => by simp; exact (λ h => _)) _

still gives me an error on all of exact (λ h => _) whereas I was really hoping to just see False. The match approach doesn't have this problem at all. I guess I am not entirely sure how to do this in Lean 3 either. How come match is doing better than this motive := trick?

PS I am quite surprised that

theorem not_or_not : (¬p ∨ ¬q) → ¬(p ∧ q) := λ h ⟨hp, hq⟩ =>
h.rec (λ h1 => h1 hp) (λ h2 => h2 hq)

doesn't work. If you feed it the motive it's fine.

[Mario Carneiro]

The reason the direct h.rec doesn't work is because @[elab_as_eliminator] was removed in lean 4

[Mario Carneiro]

the recommended workaround is "use match instead"

[Mario Carneiro]

Your exact (λ h => _) doesn't make sense because the goal is (defeq to) False, not a function type

[Mario Carneiro]

unfortunately exact error spans leave much to be desired. refine acts more like lean 3 exact

[Eric Wieser]

Where does that leave us with custom induction principles, if tagging with elab_as_eliminator is no longer an option?

[Mario Carneiro]

You can use induction using

[Eric Wieser]

Does that work for Kevin's example?

[Mario Carneiro]

I think so, it should act like the match

[Mario Carneiro]

def custom_induction := @Or.rec

theorem not_or_not : (¬p ∨ ¬q) → ¬(p ∧ q) := λ h ⟨hp, hq⟩ => by
  induction h using custom_induction with
  | inl h1 => exact h1 hp
  | inr h2 => exact h2 hq