Duality

@cite{barwise-cooper-1981}

Universal vs existential operators formalized as a Galois connection.

Main definitions

• DualityType: existential vs universal classification
• aggregate: aggregate list by duality type

For GQ-level duality operations (outer negation, inner negation, dual) see Core.Quantification.outerNeg / innerNeg / dualQ.

inductive Core.Duality.DualityType : Type

Existential vs universal classification.

• existential : DualityType
• universal : DualityType

def Core.Duality.instReprDualityType.repr : DualityType → ℕ → Std.Format

Equations

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

instance Core.Duality.instReprDualityType : Repr DualityType

Equations

• Core.Duality.instReprDualityType = { reprPrec := Core.Duality.instReprDualityType.repr }

instance Core.Duality.instDecidableEqDualityType : DecidableEq DualityType

Equations

• Core.Duality.instDecidableEqDualityType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Duality.instBEqDualityType.beq : DualityType → DualityType → Bool

Equations

• Core.Duality.instBEqDualityType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Duality.instBEqDualityType : BEq DualityType

Equations

• Core.Duality.instBEqDualityType = { beq := Core.Duality.instBEqDualityType.beq }

instance Core.Duality.instInhabitedDualityType : Inhabited DualityType

Equations

• Core.Duality.instInhabitedDualityType = { default := Core.Duality.instInhabitedDualityType.default }

def Core.Duality.instInhabitedDualityType.default : DualityType

Equations

• Core.Duality.instInhabitedDualityType.default = Core.Duality.DualityType.existential

def Core.Duality.DualityType.isRobust : DualityType → Bool

Existential is robust: one witness suffices.

Equations

• Core.Duality.DualityType.existential.isRobust = true
• Core.Duality.DualityType.universal.isRobust = false

def Core.Duality.DualityType.isFragile : DualityType → Bool

Universal is fragile: one counterexample breaks.

Equations

• Core.Duality.DualityType.existential.isFragile = false
• Core.Duality.DualityType.universal.isFragile = true

def Core.Duality.DualityType.dual : DualityType → DualityType

Swap existential and universal.

Equations

• Core.Duality.DualityType.existential.dual = Core.Duality.DualityType.universal
• Core.Duality.DualityType.universal.dual = Core.Duality.DualityType.existential

theorem Core.Duality.dual_involutive (d : DualityType) : d.dual.dual = d

def Core.Duality.aggregate (d : DualityType) (l : List Truth3) : Truth3

Aggregate a list according to duality type.

Equations

• Core.Duality.aggregate Core.Duality.DualityType.existential l = List.foldl (fun (x1 x2 : Core.Duality.Truth3) => x1 ⊔ x2) ⊥ l
• Core.Duality.aggregate Core.Duality.DualityType.universal l = List.foldl (fun (x1 x2 : Core.Duality.Truth3) => x1 ⊓ x2) ⊤ l

def Core.Duality.existsAny (l : List Truth3) : Truth3

Existential aggregation: true if ANY true.

Equations

• Core.Duality.existsAny l = Core.Duality.aggregate Core.Duality.DualityType.existential l

def Core.Duality.forallAll (l : List Truth3) : Truth3

Universal aggregation: true only if ALL true.

Equations

• Core.Duality.forallAll l = Core.Duality.aggregate Core.Duality.DualityType.universal l

theorem Core.Duality.foldl_sup_of_true (l : List Truth3) : List.foldl (fun (x1 x2 : Truth3) => x1 ⊔ x2) Truth3.true l = Truth3.true

theorem Core.Duality.foldl_inf_of_false (l : List Truth3) : List.foldl (fun (x1 x2 : Truth3) => x1 ⊓ x2) Truth3.false l = Truth3.false

theorem Core.Duality.foldl_sup_mem_true (l : List Truth3) (acc : Truth3) (h : Truth3.true ∈ l) : List.foldl (fun (x1 x2 : Truth3) => x1 ⊔ x2) acc l = Truth3.true

theorem Core.Duality.foldl_inf_mem_false (l : List Truth3) (acc : Truth3) (h : Truth3.false ∈ l) : List.foldl (fun (x1 x2 : Truth3) => x1 ⊓ x2) acc l = Truth3.false

theorem Core.Duality.existential_robust (l : List Truth3) (h : (l.any fun (x : Truth3) => x == Truth3.true) = true) : existsAny l = Truth3.true

theorem Core.Duality.universal_fragile (l : List Truth3) (h : (l.any fun (x : Truth3) => x == Truth3.false) = true) : forallAll l = Truth3.false

def Core.Duality.const {α : Type u_1} (t : Truth3) : α → Truth3

Equations

• Core.Duality.const t x✝ = t

def Core.Duality.exists' {α : Type u_1} (P : α → Truth3) (l : List α) : Truth3

Equations

• Core.Duality.exists' P l = Core.Duality.existsAny (List.map P l)

def Core.Duality.forall' {α : Type u_1} (P : α → Truth3) (l : List α) : Truth3

Equations

• Core.Duality.forall' P l = Core.Duality.forallAll (List.map P l)