Advent of proof submissions.HEADmaster

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

1 files changed, 56 insertions, 0 deletions

diff --git a/src/Problem3.agda b/src/Problem3.agda
new file mode 100644
index 0000000..b340df9
--- /dev/null
+++ b/src/Problem3.agda
@@ -0,0 +1,56 @@
+{-# OPTIONS --safe #-}
+
+module Problem3 where
+
+open import Data.List
+open import Relation.Binary.PropositionalEquality
+open import Data.Nat
+open import Data.Empty
+open import Data.Nat.Properties using (≤-step; n<1+n; <⇒≢; module ≤-Reasoning)
+
+data _⊑_ {A : Set} : List A → List A → Set where
+  ⊑-nil  : [] ⊑ []
+  ⊑-cons : ∀{x}{xs ys} → xs ⊑ ys → (x ∷ xs) ⊑ (x ∷ ys)
+  ⊑-skip : ∀{x}{xs ys} → xs ⊑ ys → xs ⊑ (x ∷ ys)
+
+⊑-refl : ∀{A : Set}(xs : List A) → xs ⊑ xs
+⊑-refl []       = ⊑-nil
+⊑-refl (x ∷ xs) = ⊑-cons (⊑-refl xs)
+
+-- Induct on the second relation, then the first.
+⊑-trans : ∀{A : Set}{xs ys zs : List A} → xs ⊑ ys → ys ⊑ zs → xs ⊑ zs
+⊑-trans xs⊑ys          (⊑-skip ys⊑zs) = ⊑-skip (⊑-trans xs⊑ys ys⊑zs)
+⊑-trans ⊑-nil          ⊑-nil          = ⊑-nil
+⊑-trans (⊑-cons xs⊑ys) (⊑-cons ys⊑zs) = ⊑-cons (⊑-trans xs⊑ys ys⊑zs)
+⊑-trans (⊑-skip xs⊑ys) (⊑-cons ys⊑zs) = ⊑-skip (⊑-trans xs⊑ys ys⊑zs)
+
+⊑-len : ∀{A : Set}{xs ys : List A} → xs ⊑ ys → length xs ≤ length ys
+⊑-len ⊑-nil          = z≤n
+⊑-len (⊑-cons xs⊑ys) = s≤s (⊑-len xs⊑ys)
+⊑-len (⊑-skip xs⊑ys) = ≤-step (⊑-len xs⊑ys)
+
+∷-injectiveᵣ : {A : Set} {x y : A} {xs ys : List A} → x ∷ xs ≡ y ∷ ys → xs ≡ ys
+∷-injectiveᵣ refl = refl
+
+private
+  lemma : {A : Set} {w : A} {xs ys zs ws : List A} → xs ≡ w ∷ ws → xs ⊑ ys → ys ≡ zs → zs ⊑ ws → ⊥
+  lemma {w = w} {xs} {ys} {zs} {ws} xs≡w∷ws xs⊑ys ys≡zs zs⊑ws = <⇒≢ prf (cong length (xs≡w∷ws))
+    where
+    open ≤-Reasoning
+    prf : length xs < length (w ∷ ws)
+    prf = begin-strict
+      length xs       ≤⟨ ⊑-len xs⊑ys ⟩
+      length ys       ≡⟨ cong length ys≡zs ⟩
+      length zs       ≤⟨ ⊑-len zs⊑ws ⟩
+      length ws       <⟨ n<1+n (length ws) ⟩
+      length (w ∷ ws) ∎
+
+⊑-antisym-no-K :
+  ∀{A : Set}{xs ys zs ws : List A} → xs ⊑ zs → ws ⊑ ys → xs ≡ ys → zs ≡ ws → xs ≡ zs
+⊑-antisym-no-K ⊑-nil          ⊑-nil          []≡[]     []≡[]′    = refl
+⊑-antisym-no-K (⊑-cons xs⊑zs) (⊑-cons ws⊑ys) x∷xs≡y∷ys x∷zs≡y∷ws = cong (_ ∷_) (⊑-antisym-no-K xs⊑zs ws⊑ys (∷-injectiveᵣ x∷xs≡y∷ys) (∷-injectiveᵣ x∷zs≡y∷ws))
+⊑-antisym-no-K (⊑-skip xs⊑zs) ws⊑ys          xs≡ys     z∷zs≡ws   = ⊥-elim (lemma (sym z∷zs≡ws) ws⊑ys (sym xs≡ys) xs⊑zs)
+⊑-antisym-no-K xs⊑zs          (⊑-skip ws⊑ys) xs≡y∷ys   zs≡ws     = ⊥-elim (lemma xs≡y∷ys       xs⊑zs zs≡ws       ws⊑ys)
+
+⊑-antisym : ∀{A : Set}{xs ys : List A} → xs ⊑ ys → ys ⊑ xs → xs ≡ ys
+⊑-antisym xs⊑ys ys⊑xs = ⊑-antisym-no-K xs⊑ys ys⊑xs refl refl