|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +------------------------------------------------------------------------ |
| 4 | +-- Vec-rotation infrastructure. |
| 5 | +-- |
| 6 | +-- One cyclic-rotation fact about the alternating (sign-flipping) |
| 7 | +-- vector, factored out of `examples/Transport.agda` where it blocked |
| 8 | +-- the `∀ n` generalisation of `nyquist-in-step-kernel`. Polymorphic |
| 9 | +-- over any carrier with an involutive "negation"; the ℚ Nyquist mode |
| 10 | +-- is the intended instance (`-_` is involutive via |
| 11 | +-- `Data.Rational.Properties.neg-involutive`). |
| 12 | +-- |
| 13 | +-- `rotL`/`rotR` are reproduced verbatim from `examples/Transport.agda` |
| 14 | +-- (stdlib carries no cyclic rotation), so the lemma is drop-in for the |
| 15 | +-- consumer. Scope is deliberately one lemma plus its `map` corollary; |
| 16 | +-- this is not a general rotation theory. |
| 17 | +-- |
| 18 | +-- Note on the statement. The minimally honest signature carries an |
| 19 | +-- explicit involution hypothesis `neg (neg x) ≡ x`: rotating an |
| 20 | +-- *even*-length alternating vector by one equals its pointwise |
| 21 | +-- negation, and the equality genuinely needs `neg² = id` (it fails |
| 22 | +-- pointwise otherwise). The `2 * n` length is what makes the |
| 23 | +-- alternation parity-stable; the builder mirrors Transport's |
| 24 | +-- `concat ∘ replicate` 2-block construction exactly. |
| 25 | +------------------------------------------------------------------------ |
| 26 | + |
| 27 | +module VecRotation where |
| 28 | + |
| 29 | +open import Data.Nat.Base using (ℕ; zero; suc; _*_) |
| 30 | +open import Data.Vec.Base |
| 31 | + using (Vec; []; _∷_; _++_; map; concat; replicate; _∷ʳ_; reverse) |
| 32 | +open import Data.Vec.Properties |
| 33 | + using (reverse-∷; reverse-involutive) |
| 34 | +open import Relation.Binary.PropositionalEquality |
| 35 | + using (_≡_; refl; sym; trans; cong) |
| 36 | + |
| 37 | +private |
| 38 | + variable |
| 39 | + A : Set |
| 40 | + |
| 41 | +-- Cyclic rotations (verbatim from examples/Transport.agda). |
| 42 | +rotL : ∀ {n} → Vec A n → Vec A n |
| 43 | +rotL [] = [] |
| 44 | +rotL (x ∷ xs) = xs ∷ʳ x |
| 45 | + |
| 46 | +rotR : ∀ {n} → Vec A n → Vec A n |
| 47 | +rotR xs = reverse (rotL (reverse xs)) |
| 48 | + |
| 49 | +-- The alternating vector [a, neg a, a, neg a, …] of length 2·n, |
| 50 | +-- built from n copies of the 2-block (the shape of Transport's |
| 51 | +-- `nyquist`, modulo its outer `*-comm` `vcast`). |
| 52 | +alternating : (A → A) → (n : ℕ) → A → Vec A (n * 2) |
| 53 | +alternating neg n a = concat (replicate n (a ∷ neg a ∷ [])) |
| 54 | + |
| 55 | +-- One-step unfolding. Definitional: the 2-block keeps `a` fixed, so |
| 56 | +-- there is no parity flip to track here. |
| 57 | +alt-cons : ∀ (neg : A → A) n a → |
| 58 | + alternating neg (suc n) a ≡ a ∷ neg a ∷ alternating neg n a |
| 59 | +alt-cons neg n a = refl |
| 60 | + |
| 61 | +-- `map neg` walks the alternation forward by one block. No involution |
| 62 | +-- needed; the consumer's homogeneity step uses this corollary. |
| 63 | +map-alternating : ∀ (neg : A → A) n a → |
| 64 | + map neg (alternating neg n a) ≡ alternating neg n (neg a) |
| 65 | +map-alternating neg zero a = refl |
| 66 | +map-alternating neg (suc n) a = |
| 67 | + cong (λ z → neg a ∷ neg (neg a) ∷ z) (map-alternating neg n a) |
| 68 | + |
| 69 | +-- Snoc/cons reshuffle: appending `a` at the tail of an alternating |
| 70 | +-- vector equals consing `a` onto its pointwise negation. This is the |
| 71 | +-- single inductive step the rotation lemma turns on; the involution |
| 72 | +-- enters here (and only here). |
| 73 | +alt-snoc : ∀ (neg : A → A) (inv : ∀ x → neg (neg x) ≡ x) n a → |
| 74 | + alternating neg n a ∷ʳ a ≡ a ∷ map neg (alternating neg n a) |
| 75 | +alt-snoc neg inv zero a = refl |
| 76 | +alt-snoc neg inv (suc n) a = |
| 77 | + cong (λ z → a ∷ neg a ∷ z) |
| 78 | + (trans (alt-snoc neg inv n a) |
| 79 | + (cong (_∷ map neg (alternating neg n a)) (sym (inv a)))) |
| 80 | + |
| 81 | +-- Headline: left-rotating the (even-length) alternating vector equals |
| 82 | +-- negating it. This is exactly the Vec-rotation fact stdlib does not |
| 83 | +-- provide and that `examples/Transport.agda` documents as the blocker |
| 84 | +-- for `∀ n → step (nyquist n) ≡ 0`. |
| 85 | +rotL-alternating : ∀ (neg : A → A) (inv : ∀ x → neg (neg x) ≡ x) n a → |
| 86 | + rotL (alternating neg n a) ≡ map neg (alternating neg n a) |
| 87 | +rotL-alternating neg inv zero a = refl |
| 88 | +rotL-alternating neg inv (suc n) a = |
| 89 | + cong (neg a ∷_) |
| 90 | + (trans (alt-snoc neg inv n a) |
| 91 | + (cong (_∷ map neg (alternating neg n a)) (sym (inv a)))) |
| 92 | + |
| 93 | +------------------------------------------------------------------------ |
| 94 | +-- rotR variant. |
| 95 | +-- |
| 96 | +-- `rotR` is `step`'s other rotation, so the consumer needs it too. |
| 97 | +-- Rather than re-run the inductive argument through `reverse`'s |
| 98 | +-- double-snoc (which has no clean stdlib support), `rotR` is recovered |
| 99 | +-- as the inverse of `rotL`: `rotR ∘ rotL ≡ id` reduces, via the |
| 100 | +-- one derived helper `reverse-∷ʳ` (dual of stdlib `reverse-∷`), to |
| 101 | +-- `reverse-involutive`. `rotR-alternating` then reuses the landed |
| 102 | +-- `rotL-alternating` with no new induction over the alternation. |
| 103 | + |
| 104 | +-- Dual of stdlib `reverse-∷`: snoc-then-reverse is reverse-then-cons. |
| 105 | +reverse-∷ʳ : ∀ x {n} (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs |
| 106 | +reverse-∷ʳ x xs = |
| 107 | + trans (cong reverse |
| 108 | + (sym (trans (reverse-∷ x (reverse xs)) |
| 109 | + (cong (_∷ʳ x) (reverse-involutive xs))))) |
| 110 | + (reverse-involutive (x ∷ reverse xs)) |
| 111 | + |
| 112 | +-- `rotR` undoes `rotL`. |
| 113 | +rotR-rotL : ∀ {n} (v : Vec A n) → rotR (rotL v) ≡ v |
| 114 | +rotR-rotL [] = refl |
| 115 | +rotR-rotL (x ∷ xs) = |
| 116 | + trans (cong (λ z → reverse (rotL z)) (reverse-∷ʳ x xs)) |
| 117 | + (trans (reverse-∷ʳ x (reverse xs)) |
| 118 | + (cong (x ∷_) (reverse-involutive xs))) |
| 119 | + |
| 120 | +-- One step of the rotation, the right-handed way: `rotR` of the |
| 121 | +-- block-shifted alternation recovers the original. |
| 122 | +rotR-alternating-shift : ∀ (neg : A → A) (inv : ∀ x → neg (neg x) ≡ x) |
| 123 | + n a → rotR (alternating neg n (neg a)) ≡ alternating neg n a |
| 124 | +rotR-alternating-shift neg inv n a = |
| 125 | + trans (cong rotR |
| 126 | + (sym (trans (rotL-alternating neg inv n a) |
| 127 | + (map-alternating neg n a)))) |
| 128 | + (rotR-rotL (alternating neg n a)) |
| 129 | + |
| 130 | +-- Headline (rotR twin of `rotL-alternating`). |
| 131 | +rotR-alternating : ∀ (neg : A → A) (inv : ∀ x → neg (neg x) ≡ x) n a → |
| 132 | + rotR (alternating neg n a) ≡ map neg (alternating neg n a) |
| 133 | +rotR-alternating neg inv n a = |
| 134 | + trans (cong rotR (cong (alternating neg n) (sym (inv a)))) |
| 135 | + (trans (rotR-alternating-shift neg inv n (neg a)) |
| 136 | + (sym (map-alternating neg n a))) |
0 commit comments