Finally prove that e [ μ e / zero ] ≈ μ e.

Complete proof of generator.

1 files changed, 41 insertions, 0 deletions

diff --git a/src/Cfe/Vec/Relation/Binary/Pointwise/Inductive.agda b/src/Cfe/Vec/Relation/Binary/Pointwise/Inductive.agda
new file mode 100644
index 0000000..ba75606
--- /dev/null
+++ b/src/Cfe/Vec/Relation/Binary/Pointwise/Inductive.agda
@@ -0,0 +1,41 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Cfe.Vec.Relation.Binary.Pointwise.Inductive where
+
+open import Data.Fin using (toℕ; zero; suc)
+open import Data.Nat using (ℕ; suc; _≟_; pred)
+open import Data.Vec using (Vec; insert; remove)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)
+open import Function using (_|>_)
+open import Level using (Level)
+open import Relation.Binary using (REL; Antisym)
+open import Relation.Binary.PropositionalEquality using (cong)
+open import Relation.Nullary.Decidable using (True; toWitness; fromWitness)
+
+private
+  variable
+    a b ℓ : Level
+    A : Set a
+    B : Set b
+    _∼_ : REL A B ℓ
+    m n : ℕ
+
+antisym :
+  ∀ {P : REL A B ℓ} {Q : REL B A ℓ} {R : REL A B ℓ} →
+  Antisym P Q R → Antisym (Pointwise P {m} {n}) (Pointwise Q) (Pointwise R)
+antisym anti []       []       = []
+antisym anti (x ∷ xs) (y ∷ ys) = anti x y ∷ antisym anti xs ys
+
+Pointwise-insert :
+  ∀ {xs : Vec A m} {ys : Vec B n} → ∀ i j {i≡j : True (toℕ i ≟ toℕ j)} {x y} →
+  x ∼ y → Pointwise _∼_ xs ys → Pointwise _∼_ (insert xs i x) (insert ys j y)
+Pointwise-insert zero    zero          x xs       = x ∷ xs
+Pointwise-insert (suc i) (suc j) {i≡j} x (y ∷ xs) =
+  y ∷ Pointwise-insert i j {i≡j |> toWitness |> cong pred |> fromWitness} x xs
+
+Pointwise-remove :
+  ∀ {xs : Vec A (suc m)} {ys : Vec B (suc n)} → ∀ i j {i≡j : True (toℕ i ≟ toℕ j)} →
+  Pointwise _∼_ xs ys → Pointwise _∼_ (remove xs i) (remove ys j)
+Pointwise-remove zero zero (_ ∷ xs) = xs
+Pointwise-remove (suc i) (suc j) {i≡j} (x ∷ y ∷ xs) =
+  x ∷ Pointwise-remove i j {i≡j |> toWitness |> cong pred |> fromWitness} (y ∷ xs)