neg-id

Data/List/Properties.agda

@@ -10,7 +10,6 @@ open import Strict.Properties
 reverse : List A → List A
 reverse = foldl (flip _∷_) []
 
-
 foldl-by-r : (B → A → B) → B → List A → B
 foldl-by-r f b xs = foldr (λ x k xs → k (f xs x)) id xs b
 
@@ -90,6 +89,21 @@ module _ {A : Type a} {B : Type b} where
     foldr (λ x k b → k (f b x)) (flip (foldl f) ys) xs b ≡˘⟨ cong′ {A = B → B} (_$ b) (foldr-universal (λ xs b → foldl f (foldl f b xs) ys) (λ x k b → k (f b x)) (flip (foldl f) ys) refl (λ _ _ → refl) xs ) ⟩
     foldl f (foldl f b xs) ys ∎
 
+foldl-by-r-cons : (A → B → B) → A → (B → B) → B → B
+foldl-by-r-cons f x k xs = k (f x xs)
+
+foldr-reverse : (f : A → B → B) (b : B) (xs : List A)
+              → foldr f b (reverse xs) ≡ foldl (flip f) b xs
+foldr-reverse f b = foldl-fusion (foldr f b) [] (λ _ _ → refl)
+
+module _ {A : Type a} where
+  reverse-reverse : (xs : List A) → reverse (reverse xs) ≡ xs
+  reverse-reverse xs = foldl-is-foldr (flip _∷_) [] (reverse xs)
+                     ; cong (_$ []) (foldr-reverse (foldl-by-r-cons _∷_) id xs)
+                     ; cong (_$ []) (foldl-is-foldr (flip (foldl-by-r-cons _∷_)) id xs)
+                     ; cong (λ k → k id [] ) (sym (foldr-universal (λ xs k a → k (foldr _∷_ a xs)) (foldl-by-r-cons (foldl-by-r-cons _∷_)) id refl (λ x xs → funExt λ k → funExt λ a → refl) xs))
+                     ; sym (foldr-id xs)
+
 ++-assoc : (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
 ++-assoc xs ys zs = foldr-fusion (_++ zs) ys (λ _ _ → refl) xs
 

Data/Permutation/NonNorm.agda

@@ -64,15 +64,32 @@ open import Data.List.Properties
 neg : Swaps → Swaps
 neg = reverse
 
+
+
 open import Path.Reasoning
 
--- neg-id : ∀ xs n → xs ∙ neg xs · n ≡ n
--- neg-id xs n =
---   xs ∙ neg xs · n ≡⟨⟩
---   neg xs ++ xs · n ≡⟨ foldl-++ (flip (uncurry _↔_·_)) n (neg xs) xs ⟩
---   foldl (flip (uncurry _↔_·_)) (neg xs · n) xs ≡⟨⟩
---   foldl (flip (uncurry _↔_·_)) (foldl (flip (uncurry _↔_·_)) n (neg xs)) xs ≡⟨⟩
---   foldl (flip (uncurry _↔_·_)) (foldl (flip (uncurry _↔_·_)) n (foldl _∘⟨_⟩ ⟨⟩ xs)) xs ≡⟨ {!!} ⟩
---   foldl (flip (uncurry _↔_·_)) (foldr (uncurry _↔_·_) n xs) xs ≡⟨ {!!} ⟩
---   n ∎
+neg-id-lemma : ∀ xs n → foldl (flip (uncurry _↔_·_)) (foldr (uncurry _↔_·_) n xs) xs ≡ n
+neg-id-lemma ⟨⟩ n = refl
+neg-id-lemma (xs ∘⟨ x , y ⟩) n =
+  foldl (flip (uncurry _↔_·_)) (x ↔ y · x ↔ y · foldr (uncurry _↔_·_) n xs) xs ≡⟨ cong (flip (foldl (flip (uncurry _↔_·_))) xs) (swap-dup x y (foldr (uncurry _↔_·_) n xs)) ⟩
+  foldl (flip (uncurry _↔_·_)) (foldr (uncurry _↔_·_) n xs) xs ≡⟨ neg-id-lemma xs n ⟩
+  n ∎
+
+neg-id-lemma₂ : ∀ xs n → foldl (flip (uncurry _↔_·_)) n (foldl _∘⟨_⟩ ⟨⟩ xs) ≡ foldr (uncurry _↔_·_) n xs
+neg-id-lemma₂ xs n =
+  foldl (flip (uncurry _↔_·_)) n (reverse xs) ≡˘⟨ foldr-reverse _ _ (reverse xs) ⟩
+  foldr (uncurry _↔_·_) n (reverse (reverse xs)) ≡⟨ cong (foldr (uncurry _↔_·_) n) (reverse-reverse xs) ⟩
+  foldr (uncurry _↔_·_) n xs ∎
+
+neg-id : ∀ xs n → xs ∙ neg xs · n ≡ n
+neg-id xs n =
+  xs ∙ neg xs · n ≡⟨⟩
+  neg xs ++ xs · n ≡⟨ foldl-++ (flip (uncurry _↔_·_)) n (neg xs) xs ⟩
+  foldl (flip (uncurry _↔_·_)) (neg xs · n) xs ≡⟨⟩
+  foldl (flip (uncurry _↔_·_)) (foldl (flip (uncurry _↔_·_)) n (neg xs)) xs ≡⟨⟩
+  foldl (flip (uncurry _↔_·_)) (foldl (flip (uncurry _↔_·_)) n (foldl _∘⟨_⟩ ⟨⟩ xs)) xs
+    ≡⟨ cong (flip (foldl (flip (uncurry _↔_·_))) xs) (neg-id-lemma₂ xs n) ⟩
+  foldl (flip (uncurry _↔_·_)) (foldr (uncurry _↔_·_) n xs) xs
+    ≡⟨ neg-id-lemma xs n ⟩
+  n ∎