feat(library/data/list): add foldr/foldl equality theorems for permutations

library/data/list/basic.lean

@@ -422,15 +422,23 @@ definition foldl (f : A → B → A) : A → list B → A
 | a []       := a
 | a (b :: l) := foldl (f a b) l
 
+theorem foldl_nil (f : A → B → A) (a : A) : foldl f a [] = a
+
+theorem foldl_cons (f : A → B → A) (a : A) (b : B) (l : list B) : foldl f a (b::l) = foldl f (f a b) l
+
 definition foldr (f : A → B → B) : B → list A → B
 | b []       := b
 | b (a :: l) := f a (foldr b l)
 
+theorem foldr_nil (f : A → B → B) (b : B) : foldr f b [] = b
+
+theorem foldr_cons (f : A → B → B) (b : B) (a : A) (l : list A) : foldr f b (a::l) = f a (foldr f b l)
+
 section foldl_eq_foldr
   -- foldl and foldr coincide when f is commutative and associative
   parameters {α : Type} {f : α → α → α}
   hypothesis (Hcomm  : ∀ a b, f a b = f b a)
-  hypothesis (Hassoc : ∀ a b c, f a (f b c) = f (f a b) c)
+  hypothesis (Hassoc : ∀ a b c, f (f a b) c = f a (f b c))
   include Hcomm Hassoc
 
   theorem foldl_eq_of_comm_of_assoc : ∀ a b l, foldl f a (b::l) = f b (foldl f a l)
@@ -440,7 +448,7 @@ section foldl_eq_foldr
       change (foldl f (f (f a b) c) l = f b (foldl f (f a c) l)),
       rewrite -foldl_eq_of_comm_of_assoc,
       change (foldl f (f (f a b) c) l = foldl f (f (f a c) b) l),
-      have H₁ : f (f a b) c = f (f a c) b, by rewrite [-Hassoc, -Hassoc, Hcomm b c],
+      have H₁ : f (f a b) c = f (f a c) b, by rewrite [Hassoc, Hassoc, Hcomm b c],
       rewrite H₁
     end
 

library/data/list/perm.lean

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 List permutations
 -/
 import data.list.basic
-open list setoid nat
+open list setoid nat binary
 
 variables {A B : Type}
 
@@ -461,4 +461,30 @@ assume p : l₁++(a::l₂) ~ l₃++(a::l₄),
           ...   ~ l₃++(a::l₄) : p
           ...   ~ a::(l₃++l₄) : symm (!perm_middle),
   perm_cons_inv p'
+
+section fold_thms
+  variables {f : A → A → A} {l₁ l₂ : list A} (fcomm : commutative f) (fassoc : associative f)
+  include fcomm
+  include fassoc
+
+  theorem foldl_eq_of_perm : l₁ ~ l₂ → ∀ a, foldl f a l₁ = foldl f a l₂ :=
+  assume p, perm_induction_on p
+    (λ a, by rewrite *foldl_nil)
+    (λ x t₁ t₂ p r a, calc
+       foldl f a (x::t₁) = foldl f (f a x) t₁ : foldl_cons
+               ...       = foldl f (f a x) t₂ : r (f a x)
+               ...       = foldl f a (x::t₂)  : foldl_cons)
+    (λ x y t₁ t₂ p r a, calc
+       foldl f a (y :: x :: t₁) = foldl f (f (f a y) x) t₁ : by rewrite foldl_cons
+                     ...        = foldl f (f (f a x) y) t₁ : by rewrite [right_comm fcomm fassoc]
+                     ...        = foldl f (f (f a x) y) t₂ : r (f (f a x) y)
+                     ...        = foldl f a (x :: y :: t₂) : by rewrite foldl_cons)
+    (λ t₁ t₂ t₃ p₁ p₂ r₁ r₂ a, eq.trans (r₁ a) (r₂ a))
+
+  theorem foldr_eq_of_perm : l₁ ~ l₂ → ∀ a, foldr f a l₁ = foldr f a l₂ :=
+  assume p, take a, calc
+    foldr f a l₁ = foldl f a l₁ : by rewrite [foldl_eq_foldr fcomm fassoc]
+         ...     = foldl f a l₂ : foldl_eq_of_perm fcomm fassoc p
+         ...     = foldr f a l₂ : by rewrite [foldl_eq_foldr fcomm fassoc]
+end fold_thms
 end perm