## 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