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.
- var : Π {α : Type u_1}, α → prop_encodable.prop_form α
- not : Π {α : Type u_1}, prop_encodable.prop_form α → prop_encodable.prop_form α
- and : Π {α : Type u_1}, prop_encodable.prop_form α → prop_encodable.prop_form α → prop_encodable.prop_form α
- or : Π {α : Type u_1}, prop_encodable.prop_form α → prop_encodable.prop_form α → prop_encodable.prop_form α
Propositional formulas with labels from α.
Instances for prop_encodable.prop_form
- prop_encodable.prop_form.has_sizeof_inst
- prop_encodable.prop_form.encodable
The next three functions make it easier to construct functions from a small
fin.
defines a function out of fin 1
Equations
- prop_encodable.mk_fn1 t ⟨n + 1, h⟩ = absurd h _
- prop_encodable.mk_fn1 t ⟨0, _x⟩ = t
defines a function out of fin 2
Equations
- prop_encodable.mk_fn2 s t ⟨n + 2, h⟩ = absurd h _
- prop_encodable.mk_fn2 s t ⟨1, _x⟩ = t
- prop_encodable.mk_fn2 s t ⟨0, _x⟩ = s
Equations
- prop_encodable.prop_form.encodable = encodable.of_left_inverse f finv prop_encodable.prop_form.encodable._proof_2