Zulip Chat Archive

Stream: general

Topic: Simple question about online tutorial example


view this post on Zulip M. Andrew Moshier (May 20 2018 at 04:36):

The following from the online Lean tutorial (Lean 2) doesn't work as is in Lean 3. I figured out that I needed to change underscores in the tutorial into inaccessibles in the mutual theorem. Fine. But I still don't see how to prove not_odd_zero.

mutual inductive even, odd
with even : ℕ → Prop
| even_zero : even 0
| even_succ : ∀ n, odd n → even (n + 1)
with odd : ℕ → Prop
| odd_succ : ∀ n, even n → odd (n + 1)

open even odd

theorem not_odd_zero : ¬ (odd 0).

mutual theorem even_of_odd_succ, odd_of_even_succ
with even_of_odd_succ : ∀ n, odd (n + 1) → even n
| .(n) (odd_succ n h) := h
with odd_of_even_succ : ∀ n, even (n + 1) → odd n
| .(n) (even_succ n h) := h

view this post on Zulip Mario Carneiro (May 20 2018 at 04:37):

that works for me in 3.4.1

view this post on Zulip Mario Carneiro (May 20 2018 at 04:40):

There is also no need for the mutual theorem, since the proof is non-recursive. This works too:

theorem even_of_odd_succ : ∀ n, odd (n + 1) → even n
| .(n) (odd_succ n h) := h

theorem odd_of_even_succ : ∀ n, even (n + 1) → odd n
| .(n) (even_succ n h) := h

view this post on Zulip M. Andrew Moshier (May 20 2018 at 16:22):

I know it doesn't need to be mutual. This is lifted as is (except the change to inaccessibles) from the tutorial. My vscode is using 3.2.x; Emacs is using 3.4.x. I'll fix that. Thanks.


Last updated: May 09 2021 at 18:17 UTC