# Zulip Chat Archive

## Stream: general

### Topic: newbie: proof from assumption of inductively defined prop

#### Kevin Sullivan (Oct 17 2018 at 17:41):

Given a typical definition of an evenness property ...

inductive ev: ℕ → Prop | ev_0 : ev 0 | ev_SS : ∀ n, ev n → ev (n + 2)

Here's a script that proves that 7 isn't even:

example : ¬ ev 7 := begin assume ev7, cases ev7 with ev5, cases ev7_a, cases ev7_a_a, cases ev7_a_a_a, end

To prove that 8 is even, I can use repeat { apply ev_SS }.

What is a stylistically nicer way to prove that 7 isn't even.

#### Kevin Buzzard (Oct 17 2018 at 18:04):

You could move this thread into the `new members`

stream. And if you're posting code you can triple quote it: write ` ```lean `

at the beginning and ` ``` `

at the end. For your question: you could prove `ev n`

was decidable, and then `dec_trivial`

would decide it.

#### Andrew Ashworth (Oct 17 2018 at 18:13):

I think this is something that can be improved in Lean 4, when reflection runs a bit faster. https://people.csail.mit.edu/jgross/personal-website/papers/2018-reification-by-parametricity-itp-camera-ready.pdf

#### Andrew Ashworth (Oct 17 2018 at 18:15):

the paper's first few sections go through several ways of implementing an evenness checker

#### Kevin Buzzard (Oct 17 2018 at 18:41):

got it:

instance decidable_ev : ∀ n, decidable (ev n) | 0 := is_true ev_0 | 1 := is_false (λ ev1, by cases ev1) | (n + 2) := decidable_of_decidable_of_iff (decidable_ev n) $ (ev_SS_iff n).symm example : ¬ ev 7 := dec_trivial

#### Kevin Buzzard (Oct 17 2018 at 18:41):

dammit I failed:

inductive ev : ℕ → Prop | ev_0 : ev 0 | ev_SS : ∀ n, ev n → ev (n + 2) open ev lemma ev_SS_iff (n : ℕ) : ev (n + 2) ↔ ev n := begin split, { -- cases way intro evSS, cases evSS, assumption }, { -- easy way exact ev_SS n } end open ev instance decidable_ev : ∀ n, decidable (ev n) | 0 := is_true ev_0 | 1 := is_false (λ ev1, by cases ev1) | (n + 2) := begin rw ev_SS_iff n, exact decidable_ev n end example : decidable (ev 2) := by apply_instance example : ev 2 := dec_trivial -- fails /- exact tactic failed, type mismatch, given expression has type true but is expected to have type as_true (ev 2) state: ⊢ as_true (ev 2) -/

#### Kevin Buzzard (Oct 17 2018 at 18:41):

example : ¬ (ev 7) := begin repeat {rw ev_SS_iff}, intro ev1,cases ev1 end

is an answer (using the lemma I proved in the previous post).

#### Kevin Buzzard (Oct 17 2018 at 18:43):

Sorry, had dodgy internet and posts have appeared in random order

#### Chris Hughes (Oct 17 2018 at 18:43):

I'm guessing `dec_trivial`

failed because you didn't make decidable an instance.

#### Kevin Buzzard (Oct 17 2018 at 18:44):

My rw proof doesn't work for some reason

#### Scott Olson (Oct 17 2018 at 18:45):

I think the problem is rewriting with an `iff`

invokes propext which then cannot reduce?

#### Scott Olson (Oct 17 2018 at 18:45):

#eval (ev 2 : bool) -- tt #reduce (ev 2 : bool) -- decidable.rec (λ (h : ev 2 → false), ff) (λ (h : ev 2), tt) (eq.rec (is_true ev_0) _)

#### Scott Olson (Oct 17 2018 at 18:46):

If you `set_option pp.proofs true`

the innocent little `_`

there is `(propext <large iff structure expression>)`

#### Kevin Buzzard (Oct 17 2018 at 18:47):

Nice!

#### Kenny Lau (Oct 17 2018 at 18:50):

inductive ev : ℕ → Prop | ev_0 : ev 0 | ev_SS : ∀ n, ev n → ev (n + 2) instance : decidable_pred ev | 0 := is_true ev.ev_0 | 1 := is_false $ λ H, by cases H | (n+2) := match ev.decidable_pred n with | is_true H := is_true (ev.ev_SS n H) | is_false H := is_false (λ h, by cases h with h h; exact H h) end

#### Chris Hughes (Oct 17 2018 at 18:53):

@Kenny Lau now that we've established that "computable" functions aren't really computable unless you avoid `propext`

and `quot.sound`

, are you going to start avoiding those axioms as well?

#### Kenny Lau (Oct 17 2018 at 18:54):

inductive ev : ℕ → Prop | ev_0 : ev 0 | ev_SS : ∀ n, ev n → ev (n + 2) theorem ev_iff (n : ℕ) : ev n ↔ ev (n + 2) := ⟨ev.ev_SS n, λ H, by cases H with h h; exact h⟩ instance decidable_ev : ∀ n, decidable (ev n) | 0 := is_true ev.ev_0 | 1 := is_false (λ ev1, by cases ev1) | (n + 2) := decidable_of_decidable_of_iff (decidable_ev n) (ev_iff n)

#### Kenny Lau (Oct 17 2018 at 18:59):

inductive ev : ℕ → Prop | ev_0 : ev 0 | ev_SS : ∀ n, ev n → ev (n + 2) def ev_b : ℕ → bool | 0 := tt | 1 := ff | (n+2) := ev_b n theorem ev_iff : ∀ n, ev_b n ↔ ev n | 0 := ⟨λ _, ev.ev_0, λ _, rfl⟩ | 1 := ⟨λ ev1, by cases ev1, λ ev1, by cases ev1⟩ | (n+2) := ⟨λ evss, ev.ev_SS n ((ev_iff n).1 evss), λ evss, by cases evss with _ evss; exact (ev_iff n).2 evss⟩ instance : decidable_pred ev := λ n, decidable_of_decidable_of_iff infer_instance (ev_iff n)

#### Mario Carneiro (Oct 17 2018 at 20:20):

You should use `bodd`

instead, it has an efficient implementation in VM and a not stupid implementation in kernel

Last updated: May 11 2021 at 12:15 UTC