mathlib3 documentation

mathlib-archive / examples.prop_encodable

W types #

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

The file data/W.lean shows that if α is an an encodable fintype and for every a : α, β a is encodable, then W β is encodable.

As an example of how this can be used, we show that the type of propositional formulas with variables labeled from an encodable type is encodable.

The strategy is to define a type of labels corresponding to the constructors. From the definition (using sum, unit, and an encodable type), Lean can infer that it is encodable. We then define a map from propositional formulas to the corresponding Wfin type, and show that map has a left inverse.

We mark the auxiliary constructions private, since their only purpose is to show encodability.

inductive prop_encodable.prop_form (α : Type u_1) :
Type u_1

Propositional formulas with labels from α.

Instances for prop_encodable.prop_form

The next three functions make it easier to construct functions from a small fin.

@[simp]
def prop_encodable.mk_fn0 {α : Type u_1} :
fin 0 α

the trivial function out of fin 0.

Equations
@[simp]
def prop_encodable.mk_fn1 {α : Type u_1} (t : α) :
fin 1 α

defines a function out of fin 1

Equations
@[simp]
def prop_encodable.mk_fn2 {α : Type u_1} (s t : α) :
fin 2 α

defines a function out of fin 2

Equations
@[protected, instance]
Equations