wrap up advent of proof
This commit is contained in:
parent
d9faaaeeb1
commit
e61bbcbbbf
2 changed files with 257 additions and 0 deletions
|
|
@ -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
|
||||
|
|
|
|||
251
src/AOP/Tiling.agda
Normal file
251
src/AOP/Tiling.agda
Normal file
|
|
@ -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 (_≟_; _<?_)
|
||||
open import Data.Fin.Properties
|
||||
|
||||
-- pow2 k returns 2^k.
|
||||
pow2 : ℕ → ℕ
|
||||
pow2 0 = 1
|
||||
pow2 (suc n) = pow2 n + pow2 n
|
||||
|
||||
-- Use this instead of the constructor zero for the type Fin (pow2 m)
|
||||
-- as Agda has trouble seeing that pow2 m is always > 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 <? pow2n) (hy <? pow2n)
|
||||
where
|
||||
pow2n = fromℕ (pow2 n)
|
||||
2ⁿ-1' = ℕ.pred (pow2 n)
|
||||
-- 2ⁿ-1 : Fin (suc 2ⁿ-1')
|
||||
2ⁿ-1 : Fin (pow2 n)
|
||||
2ⁿ-1 = subst {! !} (suc-pred {! pow2 n !}) (fromℕ 2ⁿ-1')
|
||||
|
||||
defaultTopLeft = covering n {! 2ⁿ-1 !} {! !}
|
||||
|
||||
helper : ∀ {hx hy} (z1 : Dec (hx Fin.< pow2n)) (z2 : Dec (hy Fin.< pow2n)) → Σ (Board (pow2 n + pow2 n) (pow2 n + pow2 n)) (λ b → Covered ⟦ b ⟧ Except (hx , hy))
|
||||
-- Bottom right
|
||||
helper (no ¬a) (no ¬b) = {! !} , {! !}
|
||||
|
||||
-- Top right
|
||||
helper (no ¬a) (yes b) = {! !} , {! !}
|
||||
|
||||
-- Bottom left
|
||||
helper (yes a) (no ¬b) = {! !}
|
||||
|
||||
-- Top left
|
||||
helper (yes a) (yes b) = {! !}
|
||||
Loading…
Reference in a new issue