from some equality to is_some

Stream: general

[Bernd Losert]

I have a proposition p that requires an is_some x, but I only have an equality x = some y. How do I convert it?

[Bernd Losert]

This seems to work:

have : is_some x, simp [h], -- h : x = some y

[Patrick Johnson]

A #mwe would be helpful. But in general, you can rewrite the assumption and use docs#option.is_some_some

import tactic
open option

example {α : Type*} {x : option α} {y : α}
  (h : x = some y) : is_some x = tt :=
by rw [h, is_some_some]

[Bernd Losert]

But is_some_some gives you an equality. What I want is a value of type is_some x.

[Patrick Johnson]

is_some x is not a type. It is a term. Note that is_some returns a bool, not a Prop. What you've done in have : is_some x, simp [h] is an implicit coercion.

[Bernd Losert]

Oh boy. So the type that I actually what then is is_some x = tt?

[Patrick Johnson]

It depends on your use case. It's impossible to tell without a mwe.

[Bernd Losert]

In your example, do I have to write is_some x = tt or could I just write is_some x?

[Yaël Dillies]

is_some x : Prop is defined as is_some x = tt

[Bernd Losert]

In the example given you need the = tt. Otherwise, it complains. Looks like lean doesn't realize it could coerce it to a Prop.

[Yaël Dillies]

This is unexpected. Give us a MWE.

[Bernd Losert]

import tactic
open option

example {α : Type*} {x : option α} {y : α}
  (h : x = some y) : is_some x :=
by rw [h, is_some_some]

[Bernd Losert]

It says: error: tactic failed, there are unsolved goals.

[Yaël Dillies]

This works:

import data.option.basic

open option

example {α : Type*} {x : option α} {y : α} (h : x = some y) : is_some x :=
by { rw h, exact is_some_some }

[Yaël Dillies]

This too:

example {α : Type*} {x : option α} {y : α} (h : x = some y) : is_some x :=
by { rw [h, is_some_some], exact rfl }

[Bernd Losert]

Ah, so you need exact rfl to do the coercion? OK.

[Yaël Dillies]

It's just that the goal at the end is tt, which is defeq to tt = tt, but rw doesn't see it so it doesn't automatically close the goal.

[Bernd Losert]

The goal for me looks like ⊢ ↥tt.

[Yaël Dillies]

Yes, which is defeq to tt = tt, as I just said.

[Bernd Losert]

I see. Thanks for explaining.

[Eric Rodriguez]

Subst may be a nice tactic too

[Stuart Presnell]

Why does is_some return a bool? I thought it was more common to define a property by a map into Prop.

[Kevin Buzzard]

It's a computer science function

[Kevin Buzzard]

It'll be used in tactics probably. You probably wouldn't use it in proofs

[Adam Topaz]

In proofs you would usually do a case match on a term of type option X