W types

The file Mathlib/Data/W/Basic.lean shows that if α is 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 PropEncodable.PropForm (α : Type u_1) : Type u_1

Propositional formulas with labels from α.

• var: {α : Type u_1} → α → PropEncodable.PropForm α
• not: {α : Type u_1} → PropEncodable.PropForm α → PropEncodable.PropForm α
• and: {α : Type u_1} → PropEncodable.PropForm α → PropEncodable.PropForm α → PropEncodable.PropForm α
• or: {α : Type u_1} → PropEncodable.PropForm α → PropEncodable.PropForm α → PropEncodable.PropForm α

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

instance PropEncodable.PropForm.instNeZeroNatArityInrSumUnit {α : Type u_1} (c : Unit ⊕ Unit ⊕ Unit) : NeZero (PropEncodable.PropForm.arity α (Sum.inr c))

Equations

• ⋯ = ⋯

instance PropEncodable.PropForm.instEncodable {α : Type u_1} [Encodable α] : Encodable (PropEncodable.PropForm α)

Equations

• PropEncodable.PropForm.instEncodable = Encodable.ofLeftInverse PropEncodable.PropForm.f PropEncodable.PropForm.finv ⋯