Chapter20: Add

Author: splintersuidman

Mockingbird/Problems/Chapter20.agda

@@ -0,0 +1,152 @@
+open import Mockingbird.Forest using (Forest)
+
+-- Craig’s Discovery
+module Mockingbird.Problems.Chapter20 {ℓb ℓ} (forest : Forest {ℓb} {ℓ}) where
+
+open import Data.Product using (_,_)
+open import Data.Vec using ([]; _∷_)
+open import Function using (_$_)
+open import Relation.Unary using (Pred; _∈_; _⊆_; _⊇_)
+
+open Forest forest
+open import Mockingbird.Forest.Birds forest
+open import Mockingbird.Forest.Combination.Vec forest
+open import Mockingbird.Forest.Combination.Vec.Properties forest
+open import Mockingbird.Forest.Extensionality forest
+import Mockingbird.Problems.Chapter11 forest as Chapter₁₁
+open import Mockingbird.Problems.Chapter19 forest using (_≐_)
+
+problem₁ : ⦃ _ : HasGoldfinch ⦄ ⦃ _ : HasIdentity ⦄ → HasQuirkyBird
+problem₁ = record
+  { Q₃ = G ∙ I
+  ; isQuirkyBird = λ x y z → begin
+      G ∙ I ∙ x ∙ y ∙ z  ≈⟨ isGoldfinch I x y z ⟩
+      I ∙ z ∙ (x ∙ y)    ≈⟨ congʳ $ isIdentity z ⟩
+      z ∙ (x ∙ y)        ∎
+  }
+
+problem₂′ : ⦃ _ : HasQuirkyBird ⦄ ⦃ _ : HasIdentity ⦄ → HasThrush
+problem₂′ = record
+  { T = Q₃ ∙ I
+  ; isThrush = λ x y → begin
+      Q₃ ∙ I ∙ x ∙ y  ≈⟨ isQuirkyBird I x y ⟩
+      y ∙ (I ∙ x)     ≈⟨ congˡ $ isIdentity x ⟩
+      y ∙ x           ∎
+  }
+
+problem₂ : ⦃ _ : HasGoldfinch ⦄ ⦃ _ : HasIdentity ⦄ → HasThrush
+problem₂ = record
+  { T = G ∙ I ∙ I
+  ; isThrush = isThrush ⦃ problem₂′ ⦄
+  } where
+  instance hasQuirkyBird = problem₁
+
+problem₃ : ⦃ _ : HasGoldfinch ⦄ ⦃ _ : HasIdentity ⦄ → HasCardinal
+problem₃ = record
+  { C = G ∙ G ∙ I ∙ I
+  ; isCardinal = λ x y z → begin
+      G ∙ G ∙ I ∙ I ∙ x ∙ y ∙ z  ≈⟨ congʳ $ congʳ $ isGoldfinch G I I x ⟩
+      G ∙ x ∙ (I ∙ I) ∙ y ∙ z    ≈⟨ isGoldfinch x (I ∙ I) y z ⟩
+      x ∙ z ∙ (I ∙ I ∙ y)        ≈⟨ congˡ $ congʳ $ isIdentity I ⟩
+      x ∙ z ∙ (I ∙ y)            ≈⟨ congˡ $ isIdentity y ⟩
+      x ∙ z ∙ y                  ∎
+  }
+
+problem₄-Q : ⦃ _ : HasGoldfinch ⦄ ⦃ _ : HasIdentity ⦄ → HasQueerBird
+problem₄-Q = record
+  { Q = G ∙ R ∙ Q₃
+  ; isQueerBird = λ x y z → begin
+      G ∙ R ∙ Q₃ ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isGoldfinch R Q₃ x y ⟩
+      R ∙ y ∙ (Q₃ ∙ x) ∙ z    ≈⟨ isRobin y (Q₃ ∙ x) z ⟩
+      Q₃ ∙ x ∙ z ∙ y          ≈⟨ isQuirkyBird x z y ⟩
+      y ∙ (x ∙ z)             ∎
+  } where
+  instance
+    hasQuirkyBird = problem₁
+    hasCardinal = problem₃
+    hasRobin = Chapter₁₁.problem₂₃
+
+problem₄-B : ⦃ _ : HasGoldfinch ⦄ ⦃ _ : HasIdentity ⦄ → HasBluebird
+problem₄-B = record
+  { B = C ∙ Q
+  ; isBluebird = λ x y z → begin
+      C ∙ Q ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isCardinal Q x y ⟩
+      Q ∙ y ∙ x ∙ z      ≈⟨ isQueerBird y x z ⟩
+      x ∙ (y ∙ z)        ∎
+  } where
+  instance
+    hasCardinal = problem₃
+    hasQueerBird = problem₄-Q
+
+module _ ⦃ _ : Extensional ⦄
+         ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄
+         ⦃ _ : HasIdentity ⦄ ⦃ _ : HasGoldfinch ⦄ where
+  ⟨B,T,I⟩ = ⟨ B ∷ T ∷ I ∷ [] ⟩
+  ⟨G,I⟩ = ⟨ G ∷ I ∷ [] ⟩
+
+  module _ where
+    private
+      instance
+        hasCardinal = Chapter₁₁.problem₂₁-bonus
+        hasDove = Chapter₁₁.problem₅
+
+      hasGoldfinch = Chapter₁₁.problem₄₇
+
+      b : B ∈ ⟨B,T,I⟩
+      b = [ here refl ]
+
+      t : T ∈ ⟨B,T,I⟩
+      t = [ there (here refl) ]
+
+      i : I ∈ ⟨B,T,I⟩
+      i = [ there (there (here refl)) ]
+
+      c : C ∈ ⟨B,T,I⟩
+      c = b ⟨∙⟩ (t ⟨∙⟩ (b ⟨∙⟩ b ⟨∙⟩ t)) ⟨∙⟩ (b ⟨∙⟩ b ⟨∙⟩ t)
+
+      d : D ∈ ⟨B,T,I⟩
+      d = b ⟨∙⟩ b
+
+      g : G ∈ ⟨B,T,I⟩
+      g = subst′
+        (ext′ $ ext′ $ ext′ $ ext′ $ trans
+          (isGoldfinch _ _ _ _)
+          (sym $ isGoldfinch ⦃ hasGoldfinch ⦄ _ _ _ _))
+        (d ⟨∙⟩ c)
+
+    ⟨G,I⟩⊆⟨B,T,I⟩ : ⟨G,I⟩ ⊆ ⟨B,T,I⟩
+    ⟨G,I⟩⊆⟨B,T,I⟩ [ here x≈G ] = subst′ x≈G g
+    ⟨G,I⟩⊆⟨B,T,I⟩ [ there (here x≈I) ] = [ there (there (here x≈I)) ]
+    ⟨G,I⟩⊆⟨B,T,I⟩ (x∈⟨G,I⟩ ⟨∙⟩ y∈⟨G,I⟩ ∣ xy≈z) =
+      ⟨G,I⟩⊆⟨B,T,I⟩ x∈⟨G,I⟩ ⟨∙⟩ ⟨G,I⟩⊆⟨B,T,I⟩ y∈⟨G,I⟩ ∣ xy≈z
+
+  module _ where
+    private
+      g : G ∈ ⟨G,I⟩
+      g = [ here refl ]
+
+      i : I ∈ ⟨G,I⟩
+      i = [ there (here refl) ]
+
+      t : T ∈ ⟨G,I⟩
+      t = subst′
+        (ext′ $ ext′ $ trans
+          (isThrush _ _)
+          (sym $ isThrush ⦃ problem₂ ⦄ _ _))
+        (g ⟨∙⟩ i ⟨∙⟩ i)
+
+      b : B ∈ ⟨G,I⟩
+      b = subst′
+        (ext′ $ ext′ $ ext′ $ trans
+          (isBluebird _ _ _)
+          (sym $ isBluebird ⦃ problem₄-B ⦄ _ _ _))
+        (g ⟨∙⟩ g ⟨∙⟩ i ⟨∙⟩ i ⟨∙⟩ (g ⟨∙⟩ (g ⟨∙⟩ g ⟨∙⟩ i ⟨∙⟩ i ⟨∙⟩ (g ⟨∙⟩ g ⟨∙⟩ i ⟨∙⟩ i)) ⟨∙⟩ (g ⟨∙⟩ i)))
+
+    ⟨G,I⟩⊇⟨B,T,I⟩ : ⟨G,I⟩ ⊇ ⟨B,T,I⟩
+    ⟨G,I⟩⊇⟨B,T,I⟩ [ here x≈B ] = subst′ x≈B b
+    ⟨G,I⟩⊇⟨B,T,I⟩ [ there (here x≈T) ] = subst′ x≈T t
+    ⟨G,I⟩⊇⟨B,T,I⟩ [ there (there (here x≈I)) ] = [ there (here x≈I) ]
+    ⟨G,I⟩⊇⟨B,T,I⟩ (x∈⟨B,T,I⟩ ⟨∙⟩ y∈⟨B,T,I⟩ ∣ xy≈z) = ⟨G,I⟩⊇⟨B,T,I⟩ x∈⟨B,T,I⟩ ⟨∙⟩ ⟨G,I⟩⊇⟨B,T,I⟩ y∈⟨B,T,I⟩ ∣ xy≈z
+
+  ⟨G,I⟩≐⟨B,T,I⟩ : ⟨ G ∷ I ∷ [] ⟩ ≐ ⟨ B ∷ T ∷ I ∷ [] ⟩
+  ⟨G,I⟩≐⟨B,T,I⟩ = (⟨G,I⟩⊆⟨B,T,I⟩ , ⟨G,I⟩⊇⟨B,T,I⟩)

index.agda

@@ -31,3 +31,4 @@ import Mockingbird.Problems.Chapter16
 import Mockingbird.Problems.Chapter17
 import Mockingbird.Problems.Chapter18
 import Mockingbird.Problems.Chapter19
+import Mockingbird.Problems.Chapter20