Zulip Chat Archive

Stream: new members

Topic: Coercion Confusion


view this post on Zulip Patrick O'Melveny (Jul 20 2020 at 01:07):

If have the state

h : (to_bool false)
 false

is there some step to finish off this proof?

I'm somewhat unclear what the type of h is exactly. All I really know is it has to do with coercions, but what I've read hasn't provided an obvious answer and I'm still a bit unclear on the topic.

I can try and work out a minimal example of how I ended up in this state if that would help (or if it seems like I've done something disastrous to wind up here, I can reformulate this to ask more generally about the problem I'm working on) . Sorry, still very new to this.

Thanks!

view this post on Zulip Alex J. Best (Jul 20 2020 at 01:12):

A minimal example would help for sure. You can try unfold_coes at h also

view this post on Zulip Jalex Stark (Jul 20 2020 at 01:16):

assumption_mod_cast may do it, norm_cast at h may be interesting for the same reason

view this post on Zulip Jalex Stark (Jul 20 2020 at 01:17):

Your example doesn't have to be super minimal in order to be helpful; it's not much harder to execute and read the error state in 50 lines of code than 10

view this post on Zulip Patrick O'Melveny (Jul 20 2020 at 01:35):

Sorry, it was actually pretty easy to get a mwe, please see:

inductive peano
    | zero : peano
    | succ (n : peano) : peano

open peano

def is_positive : peano  bool
    | zero := false
    | _    := true

lemma zero_is_not_positive : is_positive(zero)  false :=
begin
    intro h,
    rw is_positive at h,
    sorry,
end

view this post on Zulip Reid Barton (Jul 20 2020 at 01:37):

You probably want Prop rather than bool, or at least tt/ff rather than true/false

view this post on Zulip Scott Morrison (Jul 20 2020 at 01:37):

and simpa using h (or simp at h, exact h) will finish from there.

view this post on Zulip Reid Barton (Jul 20 2020 at 01:37):

anyways, in this situation cases h will work

view this post on Zulip Scott Morrison (Jul 20 2020 at 01:37):

(but: what Reid said)

view this post on Zulip Patrick O'Melveny (Jul 20 2020 at 01:38):

Oh yeah, I see Prop was the way to go. Thank you!

view this post on Zulip Jalex Stark (Jul 20 2020 at 01:46):

bool is for computation

view this post on Zulip Patrick O'Melveny (Jul 20 2020 at 02:01):

I do tend to forget I'm not actually doing computation sometimes :) hopefully with some more practice


Last updated: May 13 2021 at 22:15 UTC