Coercion Confusion

Stream: new members

[Patrick O'Melveny]

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!

[Alex J. Best]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Patrick O'Melveny]

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

[Reid Barton]

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

[Scott Morrison]

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

[Reid Barton]

anyways, in this situation cases h will work

[Scott Morrison]

(but: what Reid said)

[Patrick O'Melveny]

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

[Jalex Stark]

bool is for computation

[Patrick O'Melveny]

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