Advent of proof submissions.HEADmaster

Completed all problems save 12, where I had to postulate two lemma.

1 files changed, 55 insertions, 0 deletions

diff --git a/src/Problem2.agda b/src/Problem2.agda
new file mode 100644
index 0000000..aaf35bc
--- /dev/null
+++ b/src/Problem2.agda
@@ -0,0 +1,55 @@
+{-# OPTIONS --safe #-}
+
+module Problem2 (T : Set) where
+open import Data.List
+open import Data.Nat
+open import Data.Product
+
+Relation = T → T → Set
+
+Commutes : Relation → Relation → Set
+Commutes R1 R2 = ∀{x y z} → R1 x y →  R2 x z → ∃[ t ] (R2 y t × R1 z t)
+
+Diamond : Relation → Set
+Diamond R = Commutes R R
+
+data Star (R : Relation) : Relation where
+  rule  : ∀{x y} → R x y → Star R x y
+  refl  : ∀{x} → Star R x x
+  trans : ∀{x y z} → Star R x y → Star R y z → Star R x z
+
+-- We prove by induction on the transitive closure proof rs. The three cases
+-- are given diagrammatically:
+--
+-- rs = rule r′
+-- We have the following diagram by assumption.
+-- x - r′ → y
+-- |        |
+-- r        s
+-- ↓        ↓
+-- z - s′ → t
+--
+-- rs = refl
+-- The diagram commutes.
+-- x == x
+-- |    |
+-- r    r
+-- ↓    ↓
+-- z == z
+--
+-- rs = trans rs₁ rs₂
+-- The diagram commutes, with each square derived by induction.
+-- x - rs₁ → y₁ - rs₂ → y₂
+-- |         |          |
+-- r         s₁         s₂
+-- ↓         ↓          ↓
+-- z - ss₁ → t₁ - ss₂ → t₂
+strip : ∀{R} → Diamond R → Commutes (Star R) R
+strip commutes (rule r′) r =
+  let (t , s , s′) = commutes r′ r in
+  t , s , rule s′
+strip commutes refl r = -, r , refl
+strip commutes (trans rs₁ rs₂) r =
+  let (t₁ , s₁ , ss₁) = strip commutes rs₁ r in
+  let (t₂ , s₂ , ss₂) = strip commutes rs₂ s₁ in
+  t₂ , s₂ , trans ss₁ ss₂