From e61bbcbbbff9bb024942d6c5e9f0a6ee6b76333a Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Tue, 24 Dec 2024 12:21:29 -0500 Subject: [PATCH] wrap up advent of proof --- src/AOP/NBE.agda | 6 ++ src/AOP/Tiling.agda | 251 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 257 insertions(+) create mode 100644 src/AOP/Tiling.agda diff --git a/src/AOP/NBE.agda b/src/AOP/NBE.agda index 982c6ec..1accc45 100644 --- a/src/AOP/NBE.agda +++ b/src/AOP/NBE.agda @@ -60,6 +60,12 @@ optimise : SNat → SNat optimise x = reify (eval x) -- phase 3: correctness +reify-hom : ∀ m n → reify (m + n) ≈ add (reify m) (reify n) +reify-hom zero n = ≈-sym add-zero +reify-hom (suc m) n = + let IH = reify-hom m n in + {! !} + correct : ∀ x → optimise x ≈ x correct zero = ≈-refl correct one = ≈-refl diff --git a/src/AOP/Tiling.agda b/src/AOP/Tiling.agda new file mode 100644 index 0000000..965f58a --- /dev/null +++ b/src/AOP/Tiling.agda @@ -0,0 +1,251 @@ +open import Data.Fin.Base as Fin hiding (_+_) +open import Data.Nat.Properties using (+-assoc; +-identityʳ; suc-pred) +open import Relation.Binary.PropositionalEquality +open import Data.Empty +open import Relation.Nullary +open import Data.Sum +open import Data.Bool using (true;false) +open import Data.Product +open import Data.Nat as ℕ hiding (_≟_; _ 0. +zero′ : ∀{m} → Fin (pow2 m) +zero′ {zero} = zero +zero′ {suc m} = raise (pow2 m) (zero′ {m}) + +-- splitAt is injective +splitAt-inj : ∀ j k → (x y : Fin (k + j)) → splitAt k x ≡ splitAt k y → x ≡ y +splitAt-inj j zero x .x refl = refl +splitAt-inj j (suc k) zero zero e = refl +splitAt-inj j (suc k) zero (suc y) e with splitAt k y +splitAt-inj j (suc k) zero (suc y) () | inj₁ x +splitAt-inj j (suc k) zero (suc y) () | inj₂ y₁ +splitAt-inj j (suc k) (suc x) zero e with splitAt k x +splitAt-inj j (suc k) (suc x) zero () | inj₁ x₁ +splitAt-inj j (suc k) (suc x) zero () | inj₂ y +splitAt-inj j (suc k) (suc x) (suc y) e = cong suc (splitAt-inj j k x y (lemma e)) + where + lemma : ∀{j k}{x y : Fin k ⊎ Fin j} → Data.Sum.map₁ Fin.suc x ≡ Data.Sum.map₁ Fin.suc y → x ≡ y + lemma {x = inj₁ x} {y = inj₁ _} refl = refl + lemma {x = inj₁ x} {y = inj₂ y} () + lemma {x = inj₂ y} {y = inj₁ x} () + lemma {x = inj₂ y} {y = inj₂ _} refl = refl + + +-- There are four types of Trionimoes +data TriType : Set where + L : TriType -- #. + -- ## + + rL : TriType -- ## + -- #. + + rrL : TriType -- ## + -- .# + + rrrL : TriType -- .# + -- ## + + +data Board : ℕ → ℕ → Set where + -- A board may be empty (of any size) + Empty : ∀ w h → Board w h + -- A board may consist of a single trionimo in the center. + -- For convenience, the single-trionimo board may be any square with side length 2^k for k ≥ 1 + Triomino : ∀ w → TriType → Board (pow2 (suc w)) (pow2 (suc w)) + -- We may stack two boards (of the same size) on top of each other + Stack : ∀{w}{h} → Board w h → Board w h → Board w h + -- We may widen a board, leaving all tiles at the same place. + Widen : ∀{w} w′ {h} → Board w h → Board (w + w′) h + -- Similarly we may heighten a board, leaving all tiles at the same place. + Heighten : ∀{w}{h} h′ → Board w h → Board w (h + h′) + -- We may also widen a board, moving all tiles to the right. + MoveRight : ∀{w} w′ {h} → Board w h → Board (w′ + w) h + -- We may also heighten a board, moving all tiles downwards. + MoveDown : ∀{w}{h} h′ → Board w h → Board w (h′ + h) + +variable w h : ℕ + +-- The meaning of a board is a footprint: a function from x and y coordinates to the number of +-- tiles stacked at that location. +-- N.B: I am too used to old school graphics programming so I assumed y = 0 was at the top, not the bottom. +-- Not sure it actually matters though. +Footprint : ℕ → ℕ → Set +Footprint w h = Fin w → Fin h → ℕ + +-- The meaning of each trionimo. We split the board into four quadrants, and place a single tile +-- in the inner corners of three out of the four quadrants. +l-fp : ∀ m → Footprint (pow2 (suc m)) (pow2 (suc m)) +l-fp m rx ry with splitAt (pow2 m) rx | splitAt (pow2 m) ry +l-fp m rx ry | inj₁ x | inj₁ y with x ≟ opposite (zero′ {m}) | y ≟ opposite (zero′ {m}) +... | yes _ | yes _ = 1 +... | _ | _ = 0 +l-fp m rx ry | inj₁ x | inj₂ y with x ≟ opposite (zero′ {m}) | y ≟ zero′ {m} +... | yes _ | yes _ = 1 +... | _ | _ = 0 +l-fp m rx ry | inj₂ x | inj₁ y = 0 +l-fp m rx ry | inj₂ x | inj₂ y with x ≟ zero′ {m} | y ≟ zero′ {m} +... | yes _ | yes _ = 1 +... | _ | _ = 0 + + +rl-fp : ∀ m → Footprint (pow2 (suc m)) (pow2 (suc m)) +rl-fp m rx ry with splitAt (pow2 m) rx | splitAt (pow2 m) ry +rl-fp m rx ry | inj₁ x | inj₁ y with x ≟ opposite (zero′ {m}) | y ≟ opposite (zero′ {m}) +... | yes _ | yes _ = 1 +... | _ | _ = 0 +rl-fp m rx ry | inj₁ x | inj₂ y with x ≟ opposite (zero′ {m}) | y ≟ zero′ {m} +... | yes _ | yes _ = 1 +... | _ | _ = 0 +rl-fp m rx ry | inj₂ x | inj₁ y with x ≟ zero′ {m} | y ≟ opposite (zero′ {m}) +... | yes _ | yes _ = 1 +... | _ | _ = 0 +rl-fp m rx ry | inj₂ x | inj₂ y = 0 + +rrl-fp : ∀ m → Footprint (pow2 (suc m)) (pow2 (suc m)) +rrl-fp m rx ry with splitAt (pow2 m) rx | splitAt (pow2 m) ry +rrl-fp m rx ry | inj₁ x | inj₁ y with x ≟ opposite (zero′ {m}) | y ≟ opposite (zero′ {m}) +... | yes _ | yes _ = 1 +... | _ | _ = 0 +rrl-fp m rx ry | inj₁ x | inj₂ y = 0 +rrl-fp m rx ry | inj₂ x | inj₁ y with x ≟ zero′ {m} | y ≟ opposite (zero′ {m}) +... | yes _ | yes _ = 1 +... | _ | _ = 0 +rrl-fp m rx ry | inj₂ x | inj₂ y with x ≟ zero′ {m} | y ≟ zero′ {m} +... | yes _ | yes _ = 1 +... | _ | _ = 0 + +rrrl-fp : ∀ m → Footprint (pow2 (suc m)) (pow2 (suc m)) +rrrl-fp m rx ry with splitAt (pow2 m) rx | splitAt (pow2 m) ry +rrrl-fp m rx ry | inj₁ x | inj₁ y = 0 +rrrl-fp m rx ry | inj₁ x | inj₂ y with x ≟ opposite (zero′ {m}) | y ≟ zero′ {m} +... | yes _ | yes _ = 1 +... | _ | _ = 0 +rrrl-fp m rx ry | inj₂ x | inj₁ y with x ≟ zero′ {m} | y ≟ opposite (zero′ {m}) +... | yes _ | yes _ = 1 +... | _ | _ = 0 +rrrl-fp m rx ry | inj₂ x | inj₂ y with x ≟ zero′ {m} | y ≟ zero′ {m} +... | yes _ | yes _ = 1 +... | _ | _ = 0 + +-- The meaning assignment for boards in terms of footprints +⟦_⟧ : Board w h → Footprint w h +⟦ Empty w h ⟧ x y = 0 +⟦ Triomino m L ⟧ x y = l-fp m x y +⟦ Triomino m rL ⟧ x y = rl-fp m x y +⟦ Triomino m rrL ⟧ x y = rrl-fp m x y +⟦ Triomino m rrrL ⟧ x y = rrrl-fp m x y +⟦ Stack b b₁ ⟧ x y = ⟦ b ⟧ x y + ⟦ b₁ ⟧ x y +⟦ Widen {w} o₁ b ⟧ x y = [ (λ p → ⟦ b ⟧ p y) , (λ _ → 0) ]′ (splitAt w x) +⟦ Heighten {_}{h} o₁ b ⟧ x y = [ (λ p → ⟦ b ⟧ x p) , (λ _ → 0) ]′ (splitAt h y) +⟦ MoveRight o b ⟧ x y = [ (λ _ → 0) , (λ x₁ → ⟦ b ⟧ x₁ y) ]′ (splitAt o x) +⟦ MoveDown o b ⟧ x y = [ (λ _ → 0) , (λ y₁ → ⟦ b ⟧ x y₁) ]′ (splitAt o y) + +-- A utility function to place four boards of size (pow2 m) into the four quadrants giving a board of size (pow2 (suc m)) +-- +-- four_boards m a b c d +-- <-2*2^m-> +-- |-----------| +-- | a | b | ^ +-- |-----|-----| 2*2^m +-- | c | d | v +-- |-----------| +four-boards : ∀ m → (a b c d : Board (pow2 m) (pow2 m)) → Board (pow2 (suc m)) (pow2 (suc m)) +four-boards m a b c d = Stack (Widen (pow2 m) (Heighten (pow2 m) a)) + (Stack (MoveRight (pow2 m) (Heighten (pow2 m) b)) + (Stack (Widen (pow2 m) (MoveDown (pow2 m) c)) + (MoveRight (pow2 m) (MoveDown (pow2 m) d)))) + +-- These lemmas about four_boards +-- are useful if you already know which quadrant your coordinates are in +fb-lemma₁ : ∀ m (a b c d : Board (pow2 m) (pow2 m)){hx hy}{x y} + → splitAt (pow2 m) hx ≡ inj₁ x → splitAt (pow2 m) hy ≡ inj₁ y + → ⟦ four-boards m a b c d ⟧ hx hy ≡ ⟦ a ⟧ x y +fb-lemma₁ m a b c d {hx = hx}{hy} e₁ e₂ with splitAt (pow2 m) hx | splitAt (pow2 m) hy +fb-lemma₁ m a b c d {hx = hx}{hy} refl refl | ._ | ._ = +-identityʳ _ + +fb-lemma₂ : ∀ m (a b c d : Board (pow2 m) (pow2 m)){hx hy}{x y} + → splitAt (pow2 m) hx ≡ inj₂ x → splitAt (pow2 m) hy ≡ inj₁ y + → ⟦ four-boards m a b c d ⟧ hx hy ≡ ⟦ b ⟧ x y +fb-lemma₂ m a b c d {hx = hx}{hy} e₁ e₂ with splitAt (pow2 m) hx | splitAt (pow2 m) hy +fb-lemma₂ m a b c d {hx = hx}{hy} refl refl | ._ | ._ = +-identityʳ _ + +fb-lemma₃ : ∀ m (a b c d : Board (pow2 m) (pow2 m)){hx hy}{x y} + → splitAt (pow2 m) hx ≡ inj₁ x → splitAt (pow2 m) hy ≡ inj₂ y + → ⟦ four-boards m a b c d ⟧ hx hy ≡ ⟦ c ⟧ x y +fb-lemma₃ m a b c d {hx = hx}{hy} e₁ e₂ with splitAt (pow2 m) hx | splitAt (pow2 m) hy +fb-lemma₃ m a b c d {hx = hx}{hy} refl refl | ._ | ._ = +-identityʳ _ + +fb-lemma₄ : ∀ m (a b c d : Board (pow2 m) (pow2 m)){hx hy}{x y} + → splitAt (pow2 m) hx ≡ inj₂ x → splitAt (pow2 m) hy ≡ inj₂ y + → ⟦ four-boards m a b c d ⟧ hx hy ≡ ⟦ d ⟧ x y +fb-lemma₄ m a b c d {hx = hx}{hy} e₁ e₂ with splitAt (pow2 m) hx | splitAt (pow2 m) hy +fb-lemma₄ m a b c d {hx = hx}{hy} refl refl | ._ | ._ = refl + + +-- These lemmas about each triomino +-- show that each triomino has one quadrant that is totally empty. +l-lemma : ∀ m {hx hy}{x y} + → splitAt (pow2 m) hx ≡ inj₂ x → splitAt (pow2 m) hy ≡ inj₁ y + → l-fp m hx hy ≡ 0 +l-lemma m {hx = hx}{hy} e₁ e₂ with splitAt (pow2 m) hx | splitAt (pow2 m) hy +l-lemma m {hx = hx}{hy} refl refl | ._ | ._ = refl + +rl-lemma : ∀ m {hx hy}{x y} + → splitAt (pow2 m) hx ≡ inj₂ x → splitAt (pow2 m) hy ≡ inj₂ y + → rl-fp m hx hy ≡ 0 +rl-lemma m {hx = hx}{hy} e₁ e₂ with splitAt (pow2 m) hx | splitAt (pow2 m) hy +rl-lemma m {hx = hx}{hy} refl refl | ._ | ._ = refl + +rrl-lemma : ∀ m {hx hy}{x y} + → splitAt (pow2 m) hx ≡ inj₁ x → splitAt (pow2 m) hy ≡ inj₂ y + → rrl-fp m hx hy ≡ 0 +rrl-lemma m {hx = hx}{hy} e₁ e₂ with splitAt (pow2 m) hx | splitAt (pow2 m) hy +rrl-lemma m {hx = hx}{hy} refl refl | ._ | ._ = refl + +rrrl-lemma : ∀ m {hx hy}{x y} + → splitAt (pow2 m) hx ≡ inj₁ x → splitAt (pow2 m) hy ≡ inj₁ y + → rrrl-fp m hx hy ≡ 0 +rrrl-lemma m {hx = hx}{hy} e₁ e₂ with splitAt (pow2 m) hx | splitAt (pow2 m) hy +rrrl-lemma m {hx = hx}{hy} refl refl | ._ | ._ = refl + +-- The main theorem: +-- Given a number m and a coordinate (hx,hy), we can produce a +-- board of size 2^m x 2^m, where every space is covered by exactly +-- one triomino except for the space (hx,hy) which is left empty. +Covered_Except_ : Footprint w h → Fin w × Fin h → Set +Covered f Except (hx , hy) = (f hx hy ≡ 0) × (∀ x y → ( x , y) ≢ ( hx , hy ) → f x y ≡ 1) + +covering : ∀ n hx hy → Σ (Board (pow2 n) (pow2 n)) (λ b → Covered ⟦ b ⟧ Except (hx , hy)) +covering zero zero zero = (Empty 1 1) , refl , helper where + helper : (x y : Fin 1) → (x , y) ≢ (zero , zero) → 0 ≡ 1 + helper zero zero p = ⊥-elim (p refl) +covering (suc n) hx hy = helper (hx