Zulip Chat Archive

Stream: general

Topic: newbie: proof from assumption of inductively defined prop


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Andrew Ashworth (Oct 17 2018 at 18:15):

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

view this post on Zulip 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

view this post on Zulip 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)
-/

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Oct 17 2018 at 18:43):

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

view this post on Zulip Chris Hughes (Oct 17 2018 at 18:43):

I'm guessing dec_trivial failed because you didn't make decidable an instance.

view this post on Zulip Kevin Buzzard (Oct 17 2018 at 18:44):

My rw proof doesn't work for some reason

view this post on Zulip Scott Olson (Oct 17 2018 at 18:45):

I think the problem is rewriting with an iff invokes propext which then cannot reduce?

view this post on Zulip 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) _)

view this post on Zulip 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>)

view this post on Zulip Kevin Buzzard (Oct 17 2018 at 18:47):

Nice!

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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