[Proved rot-lemma. Nils Anders Danielsson **20080306231042] hunk ./MultiComposition.agda 15 +open import Relation.Binary.PropositionalEquality1 hunk ./MultiComposition.agda 18 +open import Algebra.Structures +open import Data.Nat.Properties hunk ./MultiComposition.agda 24 --- Difference lists. +-- I am using difference lists to get associativity "for free". This +-- makes it possible to state the right-assoc lemma below without +-- using any casts. hunk ./MultiComposition.agda 31 - _→_ : Set -> Set - map : forall {a b} -> (a -> b) -> _→_ a -> _→_ b - - -- Since extensionality is needed anyway we might as well state - -- functoriality in point-free form: - + _→_ : Set -> Set + map : forall {a b} -> (a -> b) -> _→_ a -> _→_ b hunk ./MultiComposition.agda 37 + -- (The map-id field is not used for anything, but it feels nice + -- to include it.) + hunk ./MultiComposition.agda 42 +-- The empty list. + hunk ./MultiComposition.agda 52 +-- Cons. + hunk ./MultiComposition.agda 66 +-- Append. + hunk ./MultiComposition.agda 90 +-- Replicate. + hunk ./MultiComposition.agda 109 +-- Congruence. + hunk ./MultiComposition.agda 117 +-- Right associativity. + hunk ./MultiComposition.agda 126 +------------------------------------------------------------------------ +-- Boring lemmas + +-- Lemmas about _^_. + +shift : forall {A B} n -> A ^ suc n → B ≡₁ A ^ n → (A -> B) +shift zero = ≡₁-refl +shift {A = A} (suc n) = ≡₁-cong (\t -> A -> t) (shift n) + +shift' : forall {A B} {C : Set} n -> + (C -> A ^ suc n → B) ≡₁ (C -> A ^ n → (A -> B)) +shift' {C = C} n = ≡₁-cong (\t -> C -> t) (shift n) + +merge : forall {A B} m n -> A ^ m → A ^ n → B ≡₁ A ^ (m + n) → B +merge zero n = ≡₁-refl +merge {A = A} (suc m) n = ≡₁-cong (\t -> A -> t) (merge m n) + +swap : forall {A B} m n -> A ^ (m + n) → B ≡₁ A ^ (n + m) → B +swap {A} {B} m n = ≡₀₁-cong (\i -> A ^ i → B) (+-comm m n) + where open IsCommutativeSemiring _ ℕ-isCommutativeSemiring + +-- Subst commutes with well-typed function applications. + +subst-commutes : forall {a b : Set1} x₁ x₂ y₁ y₂ + (F : a -> b -> Set) + (f : (x : a) -> F x y₁ -> F x y₂) + (g : F x₁ y₁) + (eq₁ : F x₁ y₁ ≡₁ F x₂ y₁) + (eq₂ : F x₁ y₂ ≡₁ F x₂ y₂) -> + f x₂ (≡₁-subst eq₁ g) ≡ ≡₁-subst eq₂ (f x₁ g) +subst-commutes ._ _ _ _ _ _ _ ≡₁-refl ≡₁-refl = ≡-refl + +-- A variant of the right associativity result. This lemma is used to +-- prove rot-lemma below. + +-- (Note that it is not possible to pattern match on an equality proof +-- unless the two sides can be unified. This is the reason for +-- formulating the lemma in this way.) + +right-assoc' : forall {a b k c ana anb amnc} m n + (f : k -> c) (g : k -> b) (h : ana) + (eq₀ : b ≡₁ a ^ m → k) + (eq₁ : ana ≡₁ a ^ n → k) + (eq₂ : a ^ n → b ≡₁ anb) + (eq₃ : anb ≡₁ a ^ (m + n) → k) + (eq₄ : a ^ (m + n) → c ≡₁ amnc) + (eq₅ : (k -> b) ≡₁ (k -> a ^ m → k)) + (eq₆ : ana ≡₁ a ^ n → k) + (eq₇ : a ^ n → a ^ m → c ≡₁ amnc) -> + ≡₁-subst eq₄ (f ⟪ a ^ (m + n) ⟫ + ≡₁-subst eq₃ (≡₁-subst eq₂ + (g ⟪ a ^ n ⟫ ≡₁-subst eq₁ h))) ≡ + ≡₁-subst eq₇ ((f ⟪ k ▻ a ^ m ⟫ ≡₁-subst eq₅ g) + ⟪ a ^ n ⟫ ≡₁-subst eq₆ h) +right-assoc' {a = a} {k = k} m n f g h + ≡₁-refl ≡₁-refl ≡₁-refl eq₃ ≡₁-refl ≡₁-refl ≡₁-refl eq₇ = + begin + f ⟪ a ^ (m + n) ⟫ ≡₁-subst eq₃ (g ⟪ a ^ n ⟫ h) + ≡⟨ subst-commutes (a ^ n ▻▻ a ^ m) (a ^ (m + n)) _ _ + _→_ (_⟪_⟫_ f) (g ⟪ a ^ n ⟫ h) eq₃ eq₇ ⟩ + ≡₁-subst eq₇ (f ⟪ a ^ n ▻▻ a ^ m ⟫ (g ⟪ a ^ n ⟫ h)) + ≡⟨ ≡-cong (≡₁-subst eq₇) + (≡-sym $ right-assoc (a ^ n) (a ^ m) f g h) ⟩ + ≡₁-subst eq₇ ((f ⟪ k ▻ a ^ m ⟫ g) ⟪ a ^ n ⟫ h) + ∎ + +------------------------------------------------------------------------ +-- Variants of _⟪_⟫_ + +-- Used to establish the correctness of the rotation function (see +-- Wand.agda). + +B′ : forall {v c} n -> let k = v -> c in + (k -> c) -> (k -> v ^ suc n → c) -> (k -> v ^ n → c) +B′ {v} {c} n f g = f ⟪ k ▻ v ^ n ⟫ cast g + where + k = v -> c + cast = ≡₁-subst (shift' n) + +B″ : forall {v c} m n -> + ((v -> c) -> v ^ m → c) -> v ^ suc n → c -> v ^ (m + n) → c +B″ {v} m n f g = cast₂ (f ⟪ v ^ n ⟫ cast₁ g) + where + cast₁ = ≡₁-subst (shift n) + cast₂ = ≡₁-subst (≡₁-trans (merge n m) (swap n m)) + +-- We still have a form of right associativity. + +rot-lemma : forall {v c} m n (f : (v -> c) -> c) g h -> + B″ 0 (m + n) f (B″ (suc m) n g h) ≡ B″ m n (B′ m f g) h +rot-lemma m n f g h = + right-assoc' m n f g h + (shift m) + (shift n) + (≡₁-trans (merge n (suc m)) (swap n (suc m))) + (shift (m + n)) + (≡₁-trans (merge (m + n) 0) (swap (m + n) 0)) + (shift' m) + (shift n) + (≡₁-trans (merge n m) (swap n m)) + hunk ./Wand.agda 23 -open import Relation.Binary.PropositionalEquality1 hunk ./Wand.agda 25 -open import Algebra.Structures -open import Data.Nat.Properties hunk ./Wand.agda 37 + -- Domains for values, stores, commands and continuations. + hunk ./Wand.agda 51 - -- The semantics, in continuation-passing style (I would have chosen - -- something more easily digestible, but monads weren't available to - -- CS people in the early eighties): + -- The semantics, in continuation-passing style. (I would have + -- chosen something more easily digestible, but monads weren't + -- available to CS people in the early eighties.) hunk ./Wand.agda 75 - -- The remaining continuations are named here. (Even though this + -- First the remaining continuations are named. (Even though this hunk ./Wand.agda 178 - -- so we have to write it out, and things start to look messy. - -- - -- See below: + -- so we have to write it out, and things start to look messy. See + -- below. hunk ./Wand.agda 297 -module Stack where - - open Language - - -- A bunch of lemmas about it. - - shift₀ : forall {A B} n -> - A ^ suc n → B ≡₁ - A ^ n → (A -> B) - shift₀ zero = ≡₁-refl - shift₀ {A = A} (suc n) = ≡₁-cong (\t -> A -> t) (shift₀ n) - - shift₀' : forall {A B} {C : Set} n -> - (C -> A ^ suc n → B) ≡₁ - (C -> A ^ n → (A -> B)) - shift₀' {C = C} n = ≡₁-cong (\t -> C -> t) (shift₀ n) - - merge : forall {A B} m n -> - A ^ m → A ^ n → B ≡₁ - A ^ (m + n) → B - merge zero n = ≡₁-refl - merge {A = A} (suc m) n = ≡₁-cong (\t -> A -> t) (merge m n) - - swap : forall {A B} m n -> - A ^ (m + n) → B ≡₁ - A ^ (n + m) → B - swap {A} {B} m n = ≡₀₁-cong (\i -> A ^ i → B) (+-comm m n) - where open IsCommutativeSemiring _ ℕ-isCommutativeSemiring - - -- Variants of _⟪_⟫_. - - B′ : forall n -> - (K -> C) -> (K -> V ^ suc n → C) -> (K -> V ^ n → C) - B′ n f g = f ⟪ K ▻ V ^ n ⟫ cast g - where cast = ≡₁-subst (shift₀' n) - - B″ : forall m n -> - (K -> V ^ m → C) -> (V ^ suc n → C) -> (V ^ (m + n) → C) - B″ m n f g = cast₂ (f ⟪ V ^ n ⟫ cast₁ g) - where - cast₁ = ≡₁-subst (shift₀ n) - cast₂ = ≡₁-subst (≡₁-trans (merge n m) (swap n m)) - - rot-lemma : forall m n f g h -> - B″ 0 (m + n) f (B″ (suc m) n g h) ≡ B″ m n (B′ m f g) h - rot-lemma m n f g h = {! !} - hunk ./Wand.agda 300 - -- the types, and to include a version of the top-level compiler - -- (P). + -- the types (in order to make some of Wand's invariants explicit, + -- and simplify the next step), and to include a version of the + -- top-level compiler (P). hunk ./Wand.agda 305 - open Stack hunk ./Wand.agda 345 - -- Let's implement Wand's rotation. - hunk ./Wand.agda 346 - open Stack + + -- Let's implement Wand's rotation. The goal is to take the + -- tree-like structure from step 2 and flatten it. hunk ./Wand.agda 361 - -- ensure that it is well-typed and structurally recursive. + -- ensure that it is well-typed and structurally recursive: hunk ./Wand.agda 370 - rot (Step₂″.B {m} {f} {g} e₁ e₂) {n} {h} = \k -> - cast (rot e₁ (rot e₂ k)) (rot-lemma m n f g h) + rot (Step₂″.B {m} {f} {g} e₁ e₂) {n} {h} = \k -> cast (rot e₁ (rot e₂ k)) hunk ./Wand.agda 372 - cast : forall {n f g} -> LinearExp n f -> f ≡ g -> LinearExp n g - cast e ≡-refl = e + cast = ≡-subst (LinearExp (m + n)) (rot-lemma m n f g h) hunk ./Wand.agda 377 + -- Check out MultiComposition.agda to see the proofs needed to + -- verify this step. The proofs look difficult, but the core result + -- (right-assoc) is very simple; the rest of the code is boring + -- impedance-matching (ensuring that functions and arguments have + -- matching types). +