Metatheorem about duals

blueprint/src/chapter/general_implications.tex

@@ -43,7 +43,7 @@ \chapter{General implications}
 
 The pre-ordering on laws has a duality symmetry:
 
-\begin{lemma}[Duality of laws]\label{duality}\uses{pre-order}  If $w  \formaleq  w'$ implies $w''  \formaleq  w'''$, then $w^{\mathrm{op}}  \formaleq  (w')^{\mathrm{op}}$ implies $w''^{\mathrm{op}}  \formaleq  (w''')^{\mathrm{op}}$.
+\begin{lemma}[Duality of laws]\lean{Law.MagmaLaw.implies_op}\leanok\label{duality}\uses{pre-order}  If $w  \formaleq  w'$ implies $w''  \formaleq  w'''$, then $w^{\mathrm{op}}  \formaleq  (w')^{\mathrm{op}}$ implies $w''^{\mathrm{op}}  \formaleq  (w''')^{\mathrm{op}}$.
 \end{lemma}
 
 \begin{proof} This follows from the fact that a magma $G$ satisfies a law $w  \formaleq  w'$ if and only if $G^{\mathrm{op}}$ satisfies $w^{\mathrm{op}}  \formaleq  (w')^{\mathrm{op}}$.

equational_theories/MagmaLaw.lean

@@ -94,3 +94,44 @@ infix:50 " ⊧ " => (models)
 infix:50 " ⊢ " => (derive)
 
 infix:50 " ⊢' " => (derive')
+
+namespace Law
+
+def MagmaLaw.symm {α : Type} (l : MagmaLaw α) : MagmaLaw α := {lhs := l.rhs, rhs:=l.lhs}
+
+@[simp]
+theorem MagmaLaw.symm_symm {α : Type} (l : MagmaLaw α) : l.symm.symm = l := by
+  simp [symm]
+
+theorem satisfiesPhi_symm_law {α G : Type} [Magma G] (φ : α → G) (E : MagmaLaw α)
+  (h : satisfiesPhi φ E) : satisfiesPhi φ E.symm := by
+  simp [Law.MagmaLaw.symm, satisfiesPhi]
+  exact h.symm
+
+theorem satisfiesPhi_symm {α G : Type} [Magma G] (φ : α → G) (w₁ w₂ : FreeMagma α)
+  (h : satisfiesPhi φ (w₁ ≃ w₂)) : satisfiesPhi φ (w₂ ≃ w₁) := Law.satisfiesPhi_symm_law φ (w₁ ≃ w₂) h
+
+theorem satisfies_symm_law {α : Type} (G : Type) [Magma G] (E : MagmaLaw α)
+  (h : G ⊧ E) :  G ⊧ E.symm := fun φ ↦ satisfiesPhi_symm_law φ E (h φ)
+
+theorem satisfies_symm {α : Type} (G : Type) [Magma G] (w₁ w₂ : FreeMagma α)
+  (h : G ⊧ w₁ ≃ w₂) :  G ⊧ w₂ ≃ w₁ := satisfies_symm_law G (w₁ ≃ w₂) h
+
+def set_symm {α} (Γ : Set (MagmaLaw α)) : Set (MagmaLaw α) := { (γ.symm) | γ ∈ Γ}
+
+theorem satisfiesSet_symm {α : Type} (G : Type) [Magma G] (Γ : Set (MagmaLaw α))
+  (h :  G ⊧ Γ) : G ⊧ (set_symm Γ) := by
+  simp [set_symm]
+  intro E ⟨Esymm, ⟨hEsymm,hEsymmE⟩⟩
+  rw [← hEsymmE]
+  apply Law.satisfies_symm
+  apply h
+  exact hEsymm
+
+theorem models_symm_law {α} (Γ : Ctx α) (E : MagmaLaw α) (h : Γ ⊧ E) : Γ   ⊧ E.symm :=
+ fun G [Magma G] hsatisfiesSet ↦ satisfies_symm_law G E (h G hsatisfiesSet)
+
+theorem models_symm {α} (Γ : Ctx α) (w₁ w₂ : FreeMagma α) (h : Γ ⊧ w₁ ≃ w₂) : Γ ⊧ w₂ ≃ w₁ :=
+   Law.models_symm_law Γ (w₁ ≃ w₂) h
+
+end Law

equational_theories/MagmaOp.lean

@@ -5,6 +5,7 @@
 
 import equational_theories.FreeMagma
 import equational_theories.MagmaLaw
+import equational_theories.Preorder
 
 open FreeMagma
 open Law
@@ -14,12 +15,20 @@ match w with
 | .Leaf x => .Leaf x
 | .Fork w₁ w₂ => .Fork w₂.op w₁.op
 
+/--
+The dual is indeed dual (an involution).
+-/
+@[simp]
+theorem FreeMagma.op_op {α} (w : FreeMagma α) : w.op.op = w := by
+ induction w <;> simp [op, *]
+
 @[simp]
 def Op (G : Type) : Type := G
 
 @[simp]
 instance opMagma {G : Type} [Magma G] : Magma (Op G) := { op := λ (x y : G) ↦ (y ◇ x : G) }
 
+def Magma.opHom {G} [Magma G] : G → Op G := fun x => x
 
 theorem evalInMagmaOp {α G} [Magma G] (φ : α → G) (w : FreeMagma α):
   evalInMagma (G := Op G) φ w.op = evalInMagma (G := G) φ w :=
@@ -36,3 +45,38 @@ by
   simp [satisfies, satisfiesPhi]
   repeat rw [@evalInMagmaOp]
   apply h
+
+namespace Law.MagmaLaw
+
+def op {α} (l : MagmaLaw α) : MagmaLaw α := { lhs := l.lhs.op, rhs := l.rhs.op}
+
+theorem law_op_op {α} (l : MagmaLaw α) : l.op.op = l := by simp [op]
+
+theorem satisfiesPhi_op {α G} [Magma G] {l : MagmaLaw α} {φ : α → G}
+  (h : satisfiesPhi (Magma.opHom ∘ φ) l) : satisfiesPhi φ l.op := by
+  simp [satisfiesPhi, evalInMagma, op] at *
+  rw [← evalInMagmaOp φ l.lhs.op, ← evalInMagmaOp φ l.rhs.op]
+  simp
+  exact h
+
+theorem satisfies_op_op {α G} [Magma G] {l : MagmaLaw α} (h : (Op G) ⊧ l) : G ⊧ l.op := by
+  intro φ
+  simp [op, satisfies]
+  apply satisfiesPhi_op
+  apply h
+
+theorem implies_op {α} {l₁ l₂ : MagmaLaw α} (h : l₁.implies l₂) : l₁.op.implies l₂.op := by
+  simp [op, implies] at *
+  intro G inst hsat
+  apply satisfies_op_op
+  apply h
+  rw [← law_op_op l₁]
+  apply satisfies_op_op
+  exact hsat
+
+theorem le_op {α} {l₁ l₂ : MagmaLaw α} (h : l₁ ≤ l₂) : l₁.op ≤ l₂.op := by
+  simp [LE.le]
+  apply implies_op
+  exact h
+
+end Law.MagmaLaw