Given (A : Set α) and (a ∈ A) conclude that (a : α)

Stream: new members

[JoXn S Costello]

I have a situation where I have (A : Set α) and (a ∈ A) by construction, so Lean concludes that (a : ↑A). I would like to coerce a to type α, but I can't find anything that would help me do that.

A is defined as

let A : Set α := { x : α | p x }

So clearly a ∈ A implies a : α, it's right there in the definition. But I can't find any way to extract that information. Any help would be appreciated here.

[Weiyi Wang]

Could you provide #mwe? What you described doesn't immediately makes sense. To be able to write a ∈ A legally, you will need to have (a : α) in the first place. That's not something that can be or needs to be extracted because it should be there already

[Weiyi Wang]

(in other words, x : y is not a proposition in Lean / type theory)

[Matt Diamond]

No, it makes sense... they have a value whose type is the coerced set. I think @JoXn S Costello just needs an explanation of exactly what happens when Lean coerces a Set to a type. Once they understand that, the solution should (hopefully) be obvious.

Though I do think more context (or even better, a #mwe) couldn't hurt.

[Aaron Liu]

might you be looking for (a : A)?

[Matt Diamond]

@Aaron Liu what I think he's looking for is a.val

[Matt Diamond]

when Lean coerces a Set to a type, it creates a docs#Subtype via docs#Set.Elem

[Matt Diamond]

@JoXn S Costello so if you have (a : ↑A) and you want a value of type α, you can just use a.val to extract the value from the Subtype, as a is just a combination of a value and a proof that the value is a member of the set

[Aaron Liu]

Aaron Liu said:

might you be looking for (a : A)?

typo, meant to write (a : α)

[Matt Diamond]

yeah you could just coerce it too

[Matt Diamond]

also this might be an #xy problem which is why a #mwe would be nice

[JoXn S Costello]

I'm trying, for fun and to learn something, to formalize Diaconescu's theorem, so I start out with

  let A : Set Bool := { x : Bool | (x = true) ∨ p }
  let B : Set Bool := { x : Bool | (x = false) ∨ p}

Classical.choice will "construct" me an a ∈ A, but I couldn't do anything useful like compare it to true in a match etc. a.val is exactly what I needed to lift a back up to Bool. Thank you!

(To make Classical.choice run at all you need to provide a proof of Nonempty A, but once you have done that choice quite reasonably produces values of type ↑A. Even figuring out how to construct Nonempty A has been instructive.)

I don't think there is any way I would have figured out that the Subtype info was what I needed, since I'm mostly relying on tutorial-level documents like "Theorem Proving in Lean 4" which don't even mention that this could be an issue. Don't get me wrong, that's a fantastic resource. But it's also got a whole section on "Propositions as Types" that doesn't dig into the differences between propositions and types, and it has a section on typeclass coercion that gives lots of advanced tips but it doesn't seem to mention subtypes...

[JoXn S Costello]

I should mention that I know that Lean uses Diaconescu's theorem to prove Classical.em but I am not going to let that spoil my fun!

[Aaron Liu]

By the way, you can match on a too

[JoXn S Costello]

When I type

match choice_A with
| true =>

Lean helpfully tells me Type mismatch ⏎true⏎ has type⏎Bool⏎but is expected to have type ⏎↑A⏎, and that's what started the adventure that led me here.

[Aaron Liu]

match choice_A with
| Subtype.mk true hA =>

[Aaron Liu]

or more commonly,

match choice_A with
| ⟨true, hA⟩ =>

[suhr]

open Classical in
  def eq_choose {U V: α → Prop}(uv: U = V)
  : (eu: ∃x, U x) → (ev: ∃x, V x) → choose eu = choose ev :=
    uv ▸ (λ_ _ ↦ rfl)

open Classical in
  example (P: Prop) : P ∨ ¬P :=
    let U := λx ↦ (x = true) ∨ P
    let V := λx ↦ (x = false) ∨ P
    let eu: ∃x, U x := ⟨true, Or.inl rfl⟩
    let ev: ∃x, V x := ⟨false, Or.inl rfl⟩
    let u := choose eu;  let v := choose ev
    let p_uv: P → u = v :=
      λp ↦
        let uv: U = V :=
          funext $ λ_ ↦ propext ⟨λ_ ↦ Or.inr p, λ_ ↦ Or.inr p⟩
        eq_choose uv eu ev
    match (choose_spec eu), (choose_spec ev) with
    | Or.inr p, _        => Or.inl p
    | _,        Or.inr p => Or.inl p
    | Or.inl (ut: u = true),
      Or.inl (vf: v = false) => Or.inr $ (ut ▸ vf ▸ Bool.noConfusion) ∘ p_uv

[suhr]

I just happen to have a readable proof of Diaconescu's theorem in Lean.

[Eric Rodriguez]

there's a proof in core lean (docs#Classical.em) but I think JoXn is trying to prove it themselves