A type for VM-erased data

This file defines a type Erased α which is classically isomorphic to α, but erased in the VM. That is, at runtime every value of Erased α is represented as 0, just like types and proofs.

ink

def Erased (α : Sort u) : Sort (max1u)

Erased α is the same as α, except that the elements of Erased α are erased in the VM in the same way as types and proofs. This can be used to track data without storing it literally.

Equations

• Erased α = ((s : α → Prop) ×' ∃ a, (fun b => a = b) = s)

ink

@[inline]

def Erased.mk {α : Sort u_1} (a : α) : Erased α

Erase a value.

Equations

• Erased.mk a = { fst := fun b => a = b, snd := (_ : ∃ a, (fun b => a = b) = fun b => a = b) }

ink

noncomputable def Erased.out {α : Sort u_1} : Erased α → α

Extracts the erased value, noncomputably.

Equations

• Erased.out x = match x with | { fst := fst, snd := h } => Classical.choose h

ink

def Erased.OutType (a : Erased (Sort u)) : Sort u

Extracts the erased value, if it is a type.

Note: (mk a).OutType is not definitionally equal to a.

Equations

• Erased.OutType a = Erased.out a

ink

theorem Erased.out_proof {p : Prop} (a : Erased p) : p

Extracts the erased value, if it is a proof.

ink

@[simp]

theorem Erased.out_mk {α : Sort u_1} (a : α) : Erased.out (Erased.mk a) = a

ink

@[simp]

theorem Erased.mk_out {α : Sort u_1} (a : Erased α) : Erased.mk (Erased.out a) = a

ink

theorem Erased.out_inj {α : Sort u_1} (a : Erased α) (b : Erased α) (h : Erased.out a = Erased.out b) : a = b

ink

noncomputable def Erased.equiv (α : Sort u_1) : Erased α ≃ α

Equivalence between Erased α and α.

Equations

• Erased.equiv α = { toFun := Erased.out, invFun := Erased.mk, left_inv := (_ : ∀ (a : Erased α), Erased.mk (Erased.out a) = a), right_inv := (_ : ∀ (a : α), Erased.out (Erased.mk a) = a) }

ink

instance Erased.instReprErased (α : Type u) : Repr (Erased α)

Equations

• Erased.instReprErased α = { reprPrec := fun x x => Std.Format.text "Erased" }

ink

instance Erased.instToStringErased (α : Type u) : ToString (Erased α)

Equations

• Erased.instToStringErased α = { toString := fun x => "Erased" }

ink

def Erased.choice {α : Sort u_1} (h : Nonempty α) : Erased α

Computably produce an erased value from a proof of nonemptiness.

Equations

• Erased.choice h = Erased.mk (Classical.choice h)

ink

@[simp]

theorem Erased.nonempty_iff {α : Sort u_1} : Nonempty (Erased α) ↔ Nonempty α

ink

instance Erased.instInhabitedErased {α : Sort u_1} [h : Nonempty α] : Inhabited (Erased α)

Equations

• Erased.instInhabitedErased = { default := Erased.choice h }

ink

def Erased.bind {α : Sort u_1} {β : Sort u_2} (a : Erased α) (f : α → Erased β) : Erased β

(>>=) operation on Erased.

This is a separate definition because α and β can live in different universes (the universe is fixed in Monad).

Equations

• Erased.bind a f = { fst := fun b => PSigma.fst (f (Erased.out a)) b, snd := (_ : ∃ a, (fun b => a = b) = (f (Erased.out a)).fst) }

ink

@[simp]

theorem Erased.bind_eq_out {α : Sort u_1} {β : Sort u_2} (a : Erased α) (f : α → Erased β) : Erased.bind a f = f (Erased.out a)

ink

def Erased.join {α : Sort u_1} (a : Erased (Erased α)) : Erased α

Collapses two levels of erasure.

Equations

• Erased.join a = Erased.bind a id

ink

@[simp]

theorem Erased.join_eq_out {α : Sort u_1} (a : Erased (Erased α)) : Erased.join a = Erased.out a

ink

def Erased.map {α : Sort u_1} {β : Sort u_2} (f : α → β) (a : Erased α) : Erased β

(<$>) operation on Erased.

This is a separate definition because α and β can live in different universes (the universe is fixed in Functor).

Equations

• Erased.map f a = Erased.bind a (Erased.mk ∘ f)

ink

@[simp]

theorem Erased.map_out {α : Sort u_1} {β : Sort u_2} {f : α → β} (a : Erased α) : Erased.out (Erased.map f a) = f (Erased.out a)

ink

instance Erased.Monad : Monad Erased

Equations

• Erased.Monad = Monad.mk

ink

@[simp]

theorem Erased.pure_def {α : Type u_1} : pure = Erased.mk

ink

@[simp]

theorem Erased.bind_def {α : Type u_1} {β : Type u_1} : (fun x x_1 => x >>= x_1) = Erased.bind

ink

@[simp]

theorem Erased.map_def {α : Type u_1} {β : Type u_1} : (fun x x_1 => x <$> x_1) = Erased.map

ink

instance Erased.LawfulMonad : LawfulMonad Erased

Equations

• Erased.LawfulMonad = Erased.LawfulMonad.proof_1