Writing an exctracting function

Stream: general

[jthulhu]

I'm trying to write a function that has the following signature {α : Type} → (x : α) → (∃ β, α = (Bool × β)) → Bool which extracts the first component of x
Ideally, it should also have the following properties:

• it shouldn't rely on classical lemmas
• it should be computable
  I can't eliminate the proof that α is of the form Bool × _ in a contexte where I'm not in a proof, but since the result of the computation doesn't actually depend on that β, there might be a trick.

For instance, I've tried the following

def extract {α : Type} (x : α) (h : ∃ β, α = (Bool × β)) : Bool :=
  let β := Classical.choose h
  have : α = (Bool × β) := Classical.choose_spec h
  (this ▸ x).fst

which relies on classical logic, but is still computable because I only use the axiom of choice to get a type. However, this fails with

invalid projection
  x.1

The following versions do work

def extract (x : (A : Type _) × A) (h : ∃ B : Type _, x.fst = (Bool × B)) : Bool := by
    obtain ⟨A, a⟩ := x
    rcases Classical.indefiniteDescription _ h with ⟨B, rfl⟩
    exact a.fst

and

def extract {α : Type} (x : α) (h : ∃ β, α = (Bool × β)) : Bool :=
  have ⟨_, α_eq_Bβ⟩ := Classical.indefiniteDescription _ h
  match α_eq_Bβ.symm, x with
    | .refl _, x => x.fst

So my questions are:

• why do some of these versions work, but not the first one?
• is there a way to do so without relying on classical axioms?

[Aaron Liu]

This should probably be impossible I think

[Vasilii Nesterov]

This is impossible because there are models of Lean type theory where (A : Type) = B ↔ A ≃ B. And if there is a bijection f between α and Bool × β there is also another bijection g a := (not (f a).1, (f a).2) and you can't naturally choose which one to use, so Classical.choice is unaviodable.

[Aaron Liu]

I don't think that's how it works

[Aaron Liu]

where's the contradiction here

[Aaron Liu]

saying A = B is the same as saying you have a canonical isomorphism between A and B called casting, where canonical means that it's coherent and commutes with everything

[Aaron Liu]

So in the cardinality model we've picked out these canonical isomorphisms for every pair of isomorphic types, so there's an easy way to choose which one to use - just pick the canonical one