## Stream: new members

### Topic: Coercion Confusion

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

#### Alex J. Best (Jul 20 2020 at 01:12):

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

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

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

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


#### Reid Barton (Jul 20 2020 at 01:37):

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

#### Scott Morrison (Jul 20 2020 at 01:37):

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

#### Reid Barton (Jul 20 2020 at 01:37):

anyways, in this situation cases h will work

#### Scott Morrison (Jul 20 2020 at 01:37):

(but: what Reid said)

#### Patrick O'Melveny (Jul 20 2020 at 01:38):

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

#### Jalex Stark (Jul 20 2020 at 01:46):

bool is for computation

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