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))

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

Equations

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