mathlib3 documentation

data.erased

A type for VM-erased data #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

def erased (α : Sort u) :

Sort (max 1 u)

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 : α), (λ (b : α), a = b) = s

Instances for erased

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

Erase a value.

Equations

erased.mk a = ⟨λ (b : α), a = b, _⟩

noncomputable def erased.out {α : Sort u_1} :

erased α → α

Extracts the erased value, noncomputably.

Equations

erased.out ⟨s, h⟩ = classical.some h

@[reducible]

def erased.out_type (a : erased (Sort u)) :

Extracts the erased value, if it is a type.

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

Equations

a.out_type = a.out

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

p

Extracts the erased value, if it is a proof.

@[simp]

theorem erased.out_mk {α : Sort u_1} (a : α) :

(erased.mk a).out = a

@[simp]

theorem erased.mk_out {α : Sort u_1} (a : erased α) :

erased.mk a.out = a

@[ext]

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

a = b

noncomputable def erased.equiv (α : Sort u_1) :

erased α ≃ α

Equivalence between erased α and α.

Equations

erased.equiv α = {to_fun := erased.out α, inv_fun := erased.mk α, left_inv := _, right_inv := _}

@[protected, instance]

def erased.has_repr (α : Type u) :

has_repr (erased α)

Equations

erased.has_repr α = {repr := λ (_x : erased α), "erased"}

@[protected, instance]

def erased.has_to_string (α : Type u) :

has_to_string (erased α)

Equations

erased.has_to_string α = {to_string := λ (_x : erased α), "erased"}

@[protected, instance]

meta def erased.has_to_format (α : Type u) :

has_to_format (erased α)

def erased.choice {α : Sort u_1} (h : nonempty α) :

Computably produce an erased value from a proof of nonemptiness.

Equations

erased.choice h = erased.mk (classical.choice h)

@[simp]

theorem erased.nonempty_iff {α : Sort u_1} :

nonempty (erased α) ↔ nonempty α

@[protected, instance]

def erased.inhabited {α : Sort u_1} [h : nonempty α] :

inhabited (erased α)

Equations

erased.inhabited = {default := erased.choice h}

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

(>>=) operation on erased.

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

Equations

a.bind f = ⟨λ (b : β), (f a.out).fst b, _⟩

@[simp]

theorem erased.bind_eq_out {α : Sort u_1} {β : Sort u_2} (a : erased α) (f : α → erased β) :

a.bind f = f a.out

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

Collapses two levels of erasure.

Equations

a.join = a.bind id

@[simp]

theorem erased.join_eq_out {α : Sort u_1} (a : erased (erased α)) :

def erased.map {α : Sort u_1} {β : Sort u_2} (f : α → β) (a : 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 = a.bind (erased.mk ∘ f)

@[simp]

theorem erased.map_out {α : Sort u_1} {β : Sort u_2} {f : α → β} (a : erased α) :

(erased.map f a).out = f a.out

@[protected, instance]

def erased.monad :

Equations

erased.monad = monad.mk

@[simp]

theorem erased.pure_def {α : Type u_1} :

has_pure.pure = erased.mk

@[simp]

theorem erased.bind_def {α β : Type u_1} :

has_bind.bind = erased.bind

@[simp]

theorem erased.map_def {α β : Type u_1} :

functor.map = erased.map

@[protected, instance]

def erased.is_lawful_monad :

is_lawful_monad erased