LeanPool.FormalizationOfBoundedArithmetic.DisplayedVariables

inductive FvName : Type

Names used for displayed free variables in formulas.

• x : FvName
• y : FvName
• z : FvName
• X : FvName

class HasVar (n : FvName) (α : Type u_1) : Type u_1

Typeclass selecting the displayed variable named n inside a variable type.

• fv : α

  The selected displayed variable.

inductive Vars0 : Type

No displayed variables.

inductive Vars1 : FvName → Type

A singleton displayed-variable context.

• fv1 {n1 : FvName} : Vars1 n1

inductive Vars2 : FvName → FvName → Type

A two-variable displayed context.

• fv1 {n1 n2 : FvName} : Vars2 n1 n2
• fv2 {n1 n2 : FvName} : Vars2 n1 n2

inductive Vars3 : FvName → FvName → FvName → Type

A three-variable displayed context.

• fv1 {n1 n2 n3 : FvName} : Vars3 n1 n2 n3
• fv2 {n1 n2 n3 : FvName} : Vars3 n1 n2 n3
• fv3 {n1 n2 n3 : FvName} : Vars3 n1 n2 n3

inductive Vars4 : FvName → FvName → FvName → FvName → Type

A four-variable displayed context.

• fv1 {n1 n2 n3 n4 : FvName} : Vars4 n1 n2 n3 n4
• fv2 {n1 n2 n3 n4 : FvName} : Vars4 n1 n2 n3 n4
• fv3 {n1 n2 n3 n4 : FvName} : Vars4 n1 n2 n3 n4
• fv4 {n1 n2 n3 n4 : FvName} : Vars4 n1 n2 n3 n4

@[implicit_reducible]

instance instHasVarVars1 (n1 : FvName) : HasVar n1 (Vars1 n1)

Equations

• instHasVarVars1 n1 = { fv := Vars1.fv1 }

@[implicit_reducible]

instance instHasVarVars2 (n1 n2 : FvName) : HasVar n1 (Vars2 n1 n2)

Equations

• instHasVarVars2 n1 n2 = { fv := Vars2.fv1 }

@[implicit_reducible]

instance instHasVarVars2_1 (n1 n2 : FvName) : HasVar n2 (Vars2 n1 n2)

Equations

• instHasVarVars2_1 n1 n2 = { fv := Vars2.fv2 }

@[implicit_reducible]

instance instHasVarVars3 (n1 n2 n3 : FvName) : HasVar n1 (Vars3 n1 n2 n3)

Equations

• instHasVarVars3 n1 n2 n3 = { fv := Vars3.fv1 }

@[implicit_reducible]

instance instHasVarVars3_1 (n1 n2 n3 : FvName) : HasVar n2 (Vars3 n1 n2 n3)

Equations

• instHasVarVars3_1 n1 n2 n3 = { fv := Vars3.fv2 }

@[implicit_reducible]

instance instHasVarVars3_2 (n1 n2 n3 : FvName) : HasVar n3 (Vars3 n1 n2 n3)

Equations

• instHasVarVars3_2 n1 n2 n3 = { fv := Vars3.fv3 }

@[implicit_reducible]

instance instHasVarVars4 (n1 n2 n3 n4 : FvName) : HasVar n1 (Vars4 n1 n2 n3 n4)

Equations

• instHasVarVars4 n1 n2 n3 n4 = { fv := Vars4.fv1 }

@[implicit_reducible]

instance instHasVarVars4_1 (n1 n2 n3 n4 : FvName) : HasVar n2 (Vars4 n1 n2 n3 n4)

Equations

• instHasVarVars4_1 n1 n2 n3 n4 = { fv := Vars4.fv2 }

@[implicit_reducible]

instance instHasVarVars4_2 (n1 n2 n3 n4 : FvName) : HasVar n3 (Vars4 n1 n2 n3 n4)

Equations

• instHasVarVars4_2 n1 n2 n3 n4 = { fv := Vars4.fv3 }

@[implicit_reducible]

instance instHasVarVars43 (n1 n2 n3 n4 : FvName) : HasVar n4 (Vars4 n1 n2 n3 n4)

Equations

• instHasVarVars43 n1 n2 n3 n4 = { fv := Vars4.fv4 }

@[implicit_reducible]

instance instIsEnumEmpty : IsEnum Empty

Equations

• instIsEnumEmpty = { size := 0, toIdx := Empty.elim, fromIdx := Fin.elim0, to_from_id := instIsEnumEmpty._proof_1, from_to_id := instIsEnumEmpty._proof_2 }

theorem IsEnum.size.Empty : size _root_.Empty = 0

@[implicit_reducible]

instance instIsEnumVars1 {n1 : FvName} : IsEnum (Vars1 n1)

Equations

• instIsEnumVars1 = { size := 1, toIdx := fun (x : Vars1 n1) => 0, fromIdx := fun (x : Fin 1) => Vars1.fv1, to_from_id := instIsEnumVars1._proof_2, from_to_id := ⋯ }

theorem IsEnum.size.Vars1 {n1 : FvName} : size (_root_.Vars1 n1) = 1

theorem IsEnum.toIdx.Vars1 {n1 : FvName} {x : _root_.Vars1 n1} : toIdx x = 0

@[implicit_reducible]

instance instIsEnumVars2 {n1 n2 : FvName} : IsEnum (Vars2 n1 n2)

Equations

• One or more equations did not get rendered due to their size.

theorem IsEnum.size.Vars2 {n1 n2 : FvName} : size (_root_.Vars2 n1 n2) = 2

theorem IsEnum.toIdx.Vars2 {n1 n2 : FvName} {x : _root_.Vars2 n1 n2} : toIdx x = match x with | Vars2.fv1 => 0 | Vars2.fv2 => 1

@[implicit_reducible]

instance instIsEnumVars3 {n1 n2 n3 : FvName} : IsEnum (Vars3 n1 n2 n3)

Equations

• One or more equations did not get rendered due to their size.

theorem IsEnum.size.Vars3 {n1 n2 n3 : FvName} : size (_root_.Vars3 n1 n2 n3) = 3

theorem IsEnum.toIdx.Vars3 {n1 n2 n3 : FvName} {x : _root_.Vars3 n1 n2 n3} : toIdx x = match x with | Vars3.fv1 => 0 | Vars3.fv2 => 1 | Vars3.fv3 => 2

@[implicit_reducible]

instance instIsEnumVars4 {n1 n2 n3 n4 : FvName} : IsEnum (Vars4 n1 n2 n3 n4)

Equations

• One or more equations did not get rendered due to their size.

theorem IsEnum.size.Vars4 {n1 n2 n3 n4 : FvName} : size (_root_.Vars4 n1 n2 n3 n4) = 4

theorem IsEnum.toIdx.Vars4 {n1 n2 n3 n4 : FvName} {x : _root_.Vars4 n1 n2 n3 n4} : toIdx x = match x with | Vars4.fv1 => 0 | Vars4.fv2 => 1 | Vars4.fv3 => 2 | Vars4.fv4 => 3

def x.name {α : Type u} [h : HasVar FvName.x α] : α

The selected variable named x.

Equations

• x.name = HasVar.fv FvName.x

def y.name {α : Type u} [h : HasVar FvName.y α] : α

The selected variable named y.

Equations

• y.name = HasVar.fv FvName.y

def z.name {α : Type u} [h : HasVar FvName.z α] : α

The selected variable named z.

Equations

• z.name = HasVar.fv FvName.z

def X.name {α : Type u} [h : HasVar FvName.X α] : α

The selected variable named X.

Equations

• X.name = HasVar.fv FvName.X

def x {α : Type u} {L : FirstOrder.Language} {k : ℕ} [h : HasVar FvName.x α] : L.Term (α ⊕ Fin k)

The first-order term for the displayed variable named x.

Equations

• x = FirstOrder.Language.var (Sum.inl (HasVar.fv FvName.x))

def y {α : Type u} {L : FirstOrder.Language} {k : ℕ} [h : HasVar FvName.y α] : L.Term (α ⊕ Fin k)

The first-order term for the displayed variable named y.

Equations

• y = FirstOrder.Language.var (Sum.inl (HasVar.fv FvName.y))

def z {α : Type u} {L : FirstOrder.Language} {k : ℕ} [h : HasVar FvName.z α] : L.Term (α ⊕ Fin k)

The first-order term for the displayed variable named z.

Equations

• z = FirstOrder.Language.var (Sum.inl (HasVar.fv FvName.z))

def X {α : Type u} {L : FirstOrder.Language} {k : ℕ} [h : HasVar FvName.X α] : L.Term (α ⊕ Fin k)

The first-order term for the displayed variable named X.

Equations

• X = FirstOrder.Language.var (Sum.inl (HasVar.fv FvName.X))

def FirstOrder.Language.Formula.display1 {L : Language} {n1 : FvName} (phi : L.Formula (Vars1 n1)) : L.Formula (Vars1 n1 ⊕ Empty)

Display a one-variable formula as a formula over an explicit sum context.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.Formula.display2 {L : Language} (name : FvName) {other : FvName} (phi : L.Formula (Vars2 name other)) : L.Formula (Vars1 name ⊕ Vars1 other)

Display a two-variable formula by isolating the named left variable.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.Formula.display3 {L : Language} (name : FvName) {other1 other2 : FvName} (phi : L.Formula (Vars3 name other1 other2)) : L.Formula (Vars1 name ⊕ Vars2 other1 other2)

Display a three-variable formula by isolating the named left variable.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.Formula.display4 {L : Language} (name : FvName) {o1 o2 o3 : FvName} (phi : L.Formula (Vars4 name o1 o2 o3)) : L.Formula (Vars1 name ⊕ Vars3 o1 o2 o3)

Display a four-variable formula by isolating the named left variable.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.Formula.displaySwapleft {L : Language} {n1 n2 n3 : FvName} (phi : L.Formula (Vars1 n1 ⊕ Vars2 n2 n3)) : L.Formula (Vars2 n1 n2 ⊕ Vars1 n3)

Reassociate displayed variables from x | (y,z) to (x,y) | z.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.Formula.displaySwapleft' {L : Language} {n1 n2 n3 : FvName} (phi : L.Formula (Vars1 n1 ⊕ Vars2 n2 n3)) : L.Formula ((Vars1 n1 ⊕ Vars1 n2) ⊕ Vars1 n3)

Reassociate displayed variables from x | (y,z) to (x | y) | z.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.Formula.rotate21 {L : Language} {n1 n2 : FvName} (phi : L.Formula (Vars2 n1 n2)) : L.Formula (Vars2 n2 n1)

Swap the two variables in a two-variable displayed formula.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.Formula.rotate213 {L : Language} (n1 n2 n3 : FvName) (phi : L.Formula (Vars3 n1 n2 n3)) : L.Formula (Vars3 n2 n1 n3)

Swap the first two variables in a three-variable displayed formula.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.Formula.rotate231 {L : Language} (n1 n2 n3 : FvName) (phi : L.Formula (Vars3 n1 n2 n3)) : L.Formula (Vars3 n3 n1 n2)

Rotate the variables in a three-variable displayed formula.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.BoundedFormula.flip {α : Type u} {L : Language} {β : Type u_3} {n : ℕ} (phi : L.BoundedFormula (α ⊕ β) n) : L.BoundedFormula (β ⊕ α) n

Flip the two sides of the free-variable sum in a bounded formula.

Equations

• phi.flip = (FirstOrder.Language.BoundedFormula.relabelEquiv { toFun := Sum.swap, invFun := Sum.swap, left_inv := ⋯, right_inv := ⋯ }) phi

def FirstOrder.Language.Formula.flip {α : Type u} {L : Language} {β : Type u_3} (phi : L.Formula (α ⊕ β)) : L.Formula (β ⊕ α)

Flip the two sides of the free-variable sum in a formula.

Equations

• phi.flip = (FirstOrder.Language.BoundedFormula.relabelEquiv { toFun := Sum.swap, invFun := Sum.swap, left_inv := ⋯, right_inv := ⋯ }) phi

def FirstOrder.Language.Formula.mkInl {α : Type u} {L : Language} (phi : L.Formula α) : L.Formula (α ⊕ Empty)

Embed a formula into a sum context by putting all variables on the left.

Equations

• phi.mkInl = (FirstOrder.Language.BoundedFormula.relabelEquiv { toFun := Sum.inl, invFun := Sum.elim id Empty.elim, left_inv := ⋯, right_inv := ⋯ }) phi