Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

[Proof Ground 2019] Fold

It is well known that many functions operating on lists can be rewritten in terms of fold (right).

But how strong is fold really? It turns out that it is actually the unique solution to this sort of recursive definition:

g []      = v             <-> g = fold f v
g (x::xs) = f x (g xs)

Prove it.

Using the universal property, prove that filter and fold_left can be rewritten as a fold.

Fibonacci numbers with fold

Natural integers being isomorphic with list of units, fold corresponds to function exponentiation. Can we discover interesting properties using the universal property? Your second task is to take a look at the Fibonacci sequence in that regard.

Many thanks to Alix Trieu for stating the problem. Thanks to Armaël Guéneau and Maximilian Haslbeck for translating.

Resources

Download Files

Definitions File

theory Defs
imports Main
begin

fun fib_list :: "unit list ⇒ nat" where
  "fib_list [] = 1"
| "fib_list (_#n') = (case n' of [] ⇒ 1 | (_#n'') ⇒ fib_list n' + fib_list n'')"


fun fib_list_tail' :: "unit list ⇒ nat ⇒ nat ⇒ nat" where
  "fib_list_tail' [] a b = b"
| "fib_list_tail' (x#xs) a b = fib_list_tail' xs (a+b) a"

definition fib_list_tail :: "unit list ⇒ nat" where
  "fib_list_tail n = fib_list_tail' n 1 1"


fun fib_induct where
  "fib_induct [] = 0"
| "fib_induct [x] = 0"
| "fib_induct (x # y # xs) = fib_induct xs + fib_induct (y # xs)"


end

Template File

theory Submission
imports Defs
begin

(***
It is well known that many functions operating on lists can be rewritten in terms of fold (right).
For instance, length = fold (λ x n → n + 1) 0 and map f = fold (λ x xs → f x :: xs) [].
Can you prove it ?
***)

lemma length_is_fold:
  "length xs = foldr (λx n. n +1) xs 0"
  by (induct xs) auto

lemma map_is_fold:
  "map f xs = foldr (λx ys. f x # ys) xs []"
  by (induct xs) auto

(***
But how strong fold actually is ?
It turns out that it is actually the unique solution to this sort of recursive definition:
  g []      = v             <-> g = fold f v
  g (x::xs) = f x (g xs)
Prove it.
***)


theorem universal_property_fold:
  fixes g :: "'a list ⇒ 'b" and f :: "'a ⇒ 'b ⇒ 'b"
  shows "(∀x xs. g (x#xs) = f x (g xs)) ⟷ (∀l. g l = foldr f l (g []))"
  sorry

lemma universal_property_foldI: 
    "(∀x xs. g (x#xs) = f x (g xs)) ⟹ g l = foldr f l (g [])"
  unfolding universal_property_fold by blast

lemma universal_property_foldI2: 
    "(∀x xs. g (x#xs) = f x (g xs)) ⟹ (g []) = n ⟹ g l = foldr f l n"
  unfolding universal_property_fold by blast

(***
Using the universal property, prove that filter and fold_left can be rewritten as a fold.
***)

lemma filter_with_fold:
  fixes p :: "'a ⇒ bool"
  shows            "∃a g. (∀xs. filter p xs = foldr g xs a)"
  sorry
 


lemma foldl_with_fold:
  fixes f :: "'a ⇒ 'b ⇒ 'a"
  shows            
  "∃a g. (∀b xs. foldl f b xs = foldr g xs a b)"
  sorry

(***
Natural integers being isomorphic with list of units, fold corresponds to function exponentiation.
Can we discover interesting properties using the universal property ?
Let's look at the Fibonacci sequence.
Unfortunately, the standard definition does not fit the requirement of the universal property.
***)

term fib_list

value "fib_list [(),(),(),()]"


(***
However, the tail recursive version does fit into the universal property theorem.
***)

term fib_list_tail'

term fib_list_tail

 
 
lemma fib_list_tail'_is_fold:
  "∃f c. fib_list_tail' xs = foldr f xs c"
  sorry
  
(***
Remarkably, this corresponds to a (convoluted) matrix exponentiation version of the Fibonacci sequence.
 ***)

thm fib_list_tail'_is_fold

(***
Now, prove that fib_list can be rewritten as a fold.    
***)

term fib_induct

thm fib_induct.induct

lemma fib_list_is_fib_list_tail:
  "fib_list n = fib_list_tail n"
  sorry
 
theorem fib_list_is_fold:
  "∃f a. fib_list n = foldr f n a (Suc 0) (Suc 0)"
  sorry

thm fib_list_is_fold

end

Check File

theory Check
imports Submission
begin


theorem universal_GOAL1: 
  "(∀x xs. (g::'a list ⇒ 'b) (x#xs) = (f::'a ⇒ 'b ⇒ 'b) x (g xs)) ⟷ (∀l. g l = foldr f l (g []))"
  by(rule Submission.universal_property_fold)

lemma universal_GOAL2: 
  "∃a g. (∀xs. filter (p::'a ⇒ bool) xs = foldr g xs a)"
  by (rule Submission.filter_with_fold)

lemma universal_GOAL3: 
  "∃a g. (∀b xs. foldl (f::'a ⇒ 'b ⇒ 'a) b xs = foldr g xs a b)"
  by (rule Submission.foldl_with_fold)

lemma universal_GOAL4:
  "∃f c. fib_list_tail' xs = foldr f xs c"
  by (rule Submission.fib_list_tail'_is_fold) 

lemma universal_GOAL5:
  "fib_list n = fib_list_tail n"
  by (rule Submission.fib_list_is_fib_list_tail) 
 
theorem universal_GOAL6:
  "∃f a. fib_list n = foldr f n a (Suc 0) (Suc 0)"
  by (rule Submission.fib_list_is_fold) 

end
Download Files

Definitions File

-- Lean version: 3.4.2
-- Mathlib version: 2019-09-11

import tactic.ext
import tactic.library_search



def fib_list : list unit → nat 
| [] := 1
| [_] := 1
| (_::e::n') := (fib_list (e::n')) + (fib_list n')

def fib_list_tail' : list unit → nat → nat → nat 
| [] a b := b
| (x::xs) a b := fib_list_tail' xs (a+b) a

def fib_list_tail : list unit → nat :=
  λ n, fib_list_tail' n 1 1

Template File

import .defs
variables {α : Type*} {β : Type*}
 


/-
It is well known that many functions operating on lists can be rewritten in terms of fold (right).
For instance, length = fold (λ x n → n + 1) 0 and map f = fold (λ x xs → f x :: xs) [].
Here are some easy proofs:
-/

lemma length_is_fold (xs : list nat ) :
  list.length xs = list.foldr (λx n, n + 1) 0 xs :=
begin
  induction xs,
  case list.nil { by refl },
  case list.cons { rw list.foldr, rw list.length, rw xs_ih  }
end

lemma map_is_fold (f : nat → nat) (xs : list nat ) :
  list.map f xs = list.foldr (λx ys, f x :: ys) [] xs :=
begin
  induction xs,
  case list.nil { by refl },
  case list.cons { rw list.foldr, rw list.map, rw xs_ih  }
end

/-
But how strong fold actually is ?
It turns out that it is actually the unique solution to this sort of recursive definition:
  g []      = v             <-> g = fold f v
  g (x::xs) = f x (g xs)
Prove it.
-/
 
theorem universal_property_fold (g : list α → β)  (f: α → β → β) :
  (∀ x xs, g (x::xs) = f x (g xs)) ↔ (∀ l, g l = list.foldr f (g []) l) :=
sorry

lemma universal_property_foldI (g : list α → β)  (f: α → β → β) (l : list α)  :
  (∀ x xs, g (x::xs) = f x (g xs)) → g l = list.foldr f (g []) l :=
begin 
  sorry
end


lemma universal_property_foldI2 (g : list α → β)  (f: α → β → β) (l : list α) (n:β)  :
  (∀ x xs, g (x::xs) = f x (g xs)) → (g []) = n → g l = list.foldr f n l :=
begin 
  sorry
end



/-
Using the universal property, prove that filter and fold_left can be rewritten as a fold.
-/

lemma filter_with_fold (p : α → Prop) [decidable_pred p]  :
  (∃(a : list α) (g : α → list α → list α), ∀ (xs : list α), list.filter p xs = list.foldr g a xs) :=
  sorry

lemma foldl_with_fold (f : α → β → α) :
  (∃ (a : α → α) g, ∀b xs, list.foldl f b xs = list.foldr g a xs b) :=
sorry

/-
Natural integers being isomorphic with list of units, fold corresponds to function exponentiation.
Can we discover interesting properties using the universal property ?
Let's look at the Fibonacci sequence.
Unfortunately, the standard definition does not fit the requirement of the universal property.
-/
 

#check fib_list

#eval fib_list [(),(),(),()]


/-
However, the tail recursive version does fit into the universal property theorem.
-/


lemma fib_list_tail'_is_fold ( xs : list unit ) :
  ∃f c, fib_list_tail' xs = list.foldr f c xs :=
sorry
  

/-
Remarkably, this corresponds to a (convoluted) matrix exponentiation version of the Fibonacci sequence.

Now, prove that fib_list can be rewritten as a fold.    
-/

lemma fib_list_is_fib_list_tail (n : list unit ):
  fib_list n = fib_list_tail n :=
  sorry


theorem fib_list_is_fold ( n : list unit )  :
  ∃ f (a : (nat → nat → nat)), fib_list n = list.foldr f a n 1 1 :=
  sorry

Check File

import .defs
import .submission
variables {α : Type*} {β : Type*}
  
theorem GOAL1 (g : list α → β)  (f: α → β → β) :
  (∀ x xs, g (x::xs) = f x (g xs)) ↔ (∀ l, g l = list.foldr f (g []) l) :=
  universal_property_fold g f


lemma GOAL2 (p : α → Prop) [decidable_pred p] :
  (∃(a : list α) (g : α → list α → list α), ∀ (xs : list α), list.filter p xs = list.foldr g a xs) :=
  filter_with_fold p


lemma GOAL3 (f : α → β → α) :
  (∃ (a : α → α) g, ∀b xs, list.foldl f b xs = list.foldr g a xs b) :=
  foldl_with_fold f


lemma GOAL4 ( xs : list unit ) :
  ∃f c, fib_list_tail' xs = list.foldr f c xs :=
   fib_list_tail'_is_fold xs
  
 
lemma GOAL5 (n : list unit ):
  fib_list n = fib_list_tail n :=
  fib_list_is_fib_list_tail n


theorem GOAL6 ( n : list unit )  :
  ∃ f (a : (nat → nat → nat)), fib_list n = list.foldr f a n 1 1 :=
  fib_list_is_fold n
Download Files

Definitions File

Require Export List Arith Psatz.
Export ListNotations.

Fixpoint fib_list (n: list unit): nat :=
  match n with
  | nil => 1
  | _::n' => match n' with
            | nil => 1
            | _::n'' => fib_list n' + fib_list n''
            end
  end.

Fixpoint fib_list_tail' (n: list unit) a b: nat :=
  match n with
  | nil => b
  | _::n' => fib_list_tail' n' (a + b) a
  end.

Definition fib_list_tail n := fib_list_tail' n 1 1.

Template File

Require Import Defs.

(***
It is well known that many functions operating on lists can be rewritten in terms of fold (right).
For instance, length = fold (λ x n → n + 1) 0 and map f = fold (λ x xs → f x :: xs) [].
Can you prove it ?
***)

Axiom funext: forall A B (f g: A -> B), (forall a, f a = g a) -> f = g.

Lemma length_is_fold:
  forall A,
    @length A = fold_right (fun x n => n + 1) 0.
Proof.
  intros; eapply funext.
  induction a; intros; try reflexivity.
  simpl. rewrite <- IHa. rewrite Nat.add_1_r. reflexivity.
Qed.

Lemma map_is_fold:
  forall A B (f: A -> B),
    map f = fold_right (fun x xs => f x :: xs) [].
Proof.
  intros; apply funext.
  induction a; intros; reflexivity.
Qed.

(***
But how strong fold actually is ?
It turns out that it is actually the unique solution to this sort of recursive definition:
  g []      = v             <-> g = fold f v
  g (x::xs) = f x (g xs)
Prove it.
***)

Theorem universal_property_fold:
  forall A B (g: list A -> B) (f: A -> B -> B),
    (forall x xs, g (x::xs) = f x (g xs)) <-> (g = fold_right f (g [])).
Admitted.

(***
Using the universal property, prove that filter and fold_left can be rewritten as a fold.
***)

Theorem filter_with_fold : forall A (p: A -> bool),
  exists a g, filter p = fold_right g a.
Admitted.

Theorem fold_left_with_fold : forall A B (f: A -> B -> A),
  exists a g, fold_left f = fold_right g a.
Admitted.

(***
Natural integers being isomorphic with list of units, fold corresponds to function exponentiation.
Can we discover interesting properties using the universal property ?
Let's look at the Fibonacci sequence.
Unfortunately, the standard definition does not fit the requirement of the universal property.
***)

Check fib_list.

Eval compute in (fib_list [tt;tt;tt;tt]).

(***
However, the tail recursive version does fit into the universal property theorem.
***)

Check fib_list_tail'.
Check fib_list_tail.

Theorem fib_list_tail'_is_fold:
  exists f a, fib_list_tail' = fold_right f a.
Admitted.

(***
Remarkably, this corresponds to a (convoluted) matrix exponentiation
version of the Fibonacci sequence.
***)

(***
Now, prove that fib_list can be rewritten as a fold.
***)

Lemma fib_list_is_fib_list_tail: forall n,
  fib_list n = fib_list_tail n.
Admitted.

Theorem fib_list_is_fold :
  exists f a,
  forall n, fib_list n = fold_right f a n 1 1.
Admitted.
Download Files

Definitions File

theory Defs
imports Main
begin

fun fib_list :: "unit list ⇒ nat" where
  "fib_list [] = 1"
| "fib_list (_#n') = (case n' of [] ⇒ 1 | (_#n'') ⇒ fib_list n' + fib_list n'')"


fun fib_list_tail' :: "unit list ⇒ nat ⇒ nat ⇒ nat" where
  "fib_list_tail' [] a b = b"
| "fib_list_tail' (x#xs) a b = fib_list_tail' xs (a+b) a"

definition fib_list_tail :: "unit list ⇒ nat" where
  "fib_list_tail n = fib_list_tail' n 1 1"


fun fib_induct where
  "fib_induct [] = 0"
| "fib_induct [x] = 0"
| "fib_induct (x # y # xs) = fib_induct xs + fib_induct (y # xs)"


end

Template File

theory Submission
imports Defs
begin

(***
It is well known that many functions operating on lists can be rewritten in terms of fold (right).
For instance, length = fold (λ x n → n + 1) 0 and map f = fold (λ x xs → f x :: xs) [].
Can you prove it ?
***)

lemma length_is_fold:
  "length xs = foldr (λx n. n +1) xs 0"
  by (induct xs) auto

lemma map_is_fold:
  "map f xs = foldr (λx ys. f x # ys) xs []"
  by (induct xs) auto

(***
But how strong fold actually is ?
It turns out that it is actually the unique solution to this sort of recursive definition:
  g []      = v             <-> g = fold f v
  g (x::xs) = f x (g xs)
Prove it.
***)


theorem universal_property_fold:
  fixes g :: "'a list ⇒ 'b" and f :: "'a ⇒ 'b ⇒ 'b"
  shows "(∀x xs. g (x#xs) = f x (g xs)) ⟷ (∀l. g l = foldr f l (g []))"
  sorry

lemma universal_property_foldI: 
    "(∀x xs. g (x#xs) = f x (g xs)) ⟹ g l = foldr f l (g [])"
  unfolding universal_property_fold by blast

lemma universal_property_foldI2: 
    "(∀x xs. g (x#xs) = f x (g xs)) ⟹ (g []) = n ⟹ g l = foldr f l n"
  unfolding universal_property_fold by blast

(***
Using the universal property, prove that filter and fold_left can be rewritten as a fold.
***)

lemma filter_with_fold:
  fixes p :: "'a ⇒ bool"
  shows            "∃a g. (∀xs. filter p xs = foldr g xs a)"
  sorry
 


lemma foldl_with_fold:
  fixes f :: "'a ⇒ 'b ⇒ 'a"
  shows            
  "∃a g. (∀b xs. foldl f b xs = foldr g xs a b)"
  sorry

(***
Natural integers being isomorphic with list of units, fold corresponds to function exponentiation.
Can we discover interesting properties using the universal property ?
Let's look at the Fibonacci sequence.
Unfortunately, the standard definition does not fit the requirement of the universal property.
***)

term fib_list

value "fib_list [(),(),(),()]"


(***
However, the tail recursive version does fit into the universal property theorem.
***)

term fib_list_tail'

term fib_list_tail

 
 
lemma fib_list_tail'_is_fold:
  "∃f c. fib_list_tail' xs = foldr f xs c"
  sorry
  
(***
Remarkably, this corresponds to a (convoluted) matrix exponentiation version of the Fibonacci sequence.
 ***)

thm fib_list_tail'_is_fold

(***
Now, prove that fib_list can be rewritten as a fold.    
***)

term fib_induct

thm fib_induct.induct

lemma fib_list_is_fib_list_tail:
  "fib_list n = fib_list_tail n"
  sorry
 
theorem fib_list_is_fold:
  "∃f a. fib_list n = foldr f n a (Suc 0) (Suc 0)"
  sorry

thm fib_list_is_fold

end

Check File

theory Check
imports Submission
begin


theorem universal_GOAL1: 
  "(∀x xs. (g::'a list ⇒ 'b) (x#xs) = (f::'a ⇒ 'b ⇒ 'b) x (g xs)) ⟷ (∀l. g l = foldr f l (g []))"
  by(rule Submission.universal_property_fold)

lemma universal_GOAL2: 
  "∃a g. (∀xs. filter (p::'a ⇒ bool) xs = foldr g xs a)"
  by (rule Submission.filter_with_fold)

lemma universal_GOAL3: 
  "∃a g. (∀b xs. foldl (f::'a ⇒ 'b ⇒ 'a) b xs = foldr g xs a b)"
  by (rule Submission.foldl_with_fold)

lemma universal_GOAL4:
  "∃f c. fib_list_tail' xs = foldr f xs c"
  by (rule Submission.fib_list_tail'_is_fold) 

lemma universal_GOAL5:
  "fib_list n = fib_list_tail n"
  by (rule Submission.fib_list_is_fib_list_tail) 
 
theorem universal_GOAL6:
  "∃f a. fib_list n = foldr f n a (Suc 0) (Suc 0)"
  by (rule Submission.fib_list_is_fold) 

end
Download Files

Definitions File

-- Lean version: 3.16.2
-- Mathlib version: eb5b7fb7f406385cd1f2efaa15d9c0923541b955

import tactic.basic

def fib_list : list unit → nat
| [] := 1
| [_] := 1
| (_::e::n') := (fib_list (e::n')) + (fib_list n')

def fib_list_tail' : list unit → nat → nat → nat
| [] a b := b
| (x::xs) a b := fib_list_tail' xs (a+b) a

def fib_list_tail : list unit → nat :=
  λ n, fib_list_tail' n 1 1

notation `GOAL1` := λ α β,
∀ (g : list α → β)  (f: α → β → β),
  (∀ x xs, g (x::xs) = f x (g xs)) ↔ (∀ l, g l = list.foldr f (g []) l)

notation `GOAL2` := λ α (p : α → Prop) (h : decidable_pred p),
  (∃(a : list α) (g : α → list α → list α), ∀ (xs : list α), @list.filter α p h xs = list.foldr g a xs)

notation `GOAL3` := λ α β,
∀ (f : α → β → α),
  (∃ (a : α → α) g, ∀b xs, list.foldl f b xs = list.foldr g a xs b)

notation `GOAL4` :=
∀ (xs : list unit), ∃f c, fib_list_tail' xs = list.foldr f c xs

notation `GOAL5` :=
∀ (n : list unit ), fib_list n = fib_list_tail n

notation `GOAL6` :=
∀ ( n : list unit ), ∃ f (a : (nat → nat → nat)), fib_list n = list.foldr f a n 1 1

Template File

import .defs
variables {α : Type*} {β : Type*}
 


/-
It is well known that many functions operating on lists can be rewritten in terms of fold (right).
For instance, length = fold (λ x n → n + 1) 0 and map f = fold (λ x xs → f x :: xs) [].
Here are some easy proofs:
-/

lemma length_is_fold (xs : list nat ) :
  list.length xs = list.foldr (λx n, n + 1) 0 xs :=
begin
  induction xs,
  case list.nil { by refl },
  case list.cons { rw list.foldr, rw list.length, rw xs_ih  }
end

lemma map_is_fold (f : nat → nat) (xs : list nat ) :
  list.map f xs = list.foldr (λx ys, f x :: ys) [] xs :=
begin
  induction xs,
  case list.nil { by refl },
  case list.cons { rw list.foldr, rw list.map, rw xs_ih  }
end

/-
But how strong fold actually is ?
It turns out that it is actually the unique solution to this sort of recursive definition:
  g []      = v             <-> g = fold f v
  g (x::xs) = f x (g xs)
Prove it.
-/
 
theorem universal_property_fold (g : list α → β)  (f: α → β → β) :
  (∀ x xs, g (x::xs) = f x (g xs)) ↔ (∀ l, g l = list.foldr f (g []) l) :=
sorry

lemma universal_property_foldI (g : list α → β)  (f: α → β → β) (l : list α)  :
  (∀ x xs, g (x::xs) = f x (g xs)) → g l = list.foldr f (g []) l :=
begin 
  sorry
end


lemma universal_property_foldI2 (g : list α → β)  (f: α → β → β) (l : list α) (n:β)  :
  (∀ x xs, g (x::xs) = f x (g xs)) → (g []) = n → g l = list.foldr f n l :=
begin 
  sorry
end



/-
Using the universal property, prove that filter and fold_left can be rewritten as a fold.
-/

lemma filter_with_fold (p : α → Prop) [decidable_pred p]  :
  (∃(a : list α) (g : α → list α → list α), ∀ (xs : list α), list.filter p xs = list.foldr g a xs) :=
  sorry

lemma foldl_with_fold (f : α → β → α) :
  (∃ (a : α → α) g, ∀b xs, list.foldl f b xs = list.foldr g a xs b) :=
sorry

/-
Natural integers being isomorphic with list of units, fold corresponds to function exponentiation.
Can we discover interesting properties using the universal property ?
Let's look at the Fibonacci sequence.
Unfortunately, the standard definition does not fit the requirement of the universal property.
-/
 

#check fib_list

#eval fib_list [(),(),(),()]


/-
However, the tail recursive version does fit into the universal property theorem.
-/


lemma fib_list_tail'_is_fold ( xs : list unit ) :
  ∃f c, fib_list_tail' xs = list.foldr f c xs :=
sorry
  

/-
Remarkably, this corresponds to a (convoluted) matrix exponentiation version of the Fibonacci sequence.

Now, prove that fib_list can be rewritten as a fold.    
-/

lemma fib_list_is_fib_list_tail (n : list unit ):
  fib_list n = fib_list_tail n :=
  sorry


theorem fib_list_is_fold ( n : list unit )  :
  ∃ f (a : (nat → nat → nat)), fib_list n = list.foldr f a n 1 1 :=
  sorry

Check File

import .defs
import .submission
variables {α : Type*} {β : Type*}

theorem goal1 : GOAL1 α β :=
  universal_property_fold

lemma goal2 (p : α → Prop) [h : decidable_pred p] : GOAL2 α p h :=
  filter_with_fold p

lemma goal3 : GOAL3 α β :=
  foldl_with_fold

lemma goal4 : GOAL4 :=
   fib_list_tail'_is_fold

lemma goal5 : GOAL5 :=
  fib_list_is_fib_list_tail

theorem goal6 : GOAL6 :=
  fib_list_is_fold
Download Files

Definitions File

theory Defs
imports Main
begin

fun fib_list :: "unit list ⇒ nat" where
  "fib_list [] = 1"
| "fib_list (_#n') = (case n' of [] ⇒ 1 | (_#n'') ⇒ fib_list n' + fib_list n'')"


fun fib_list_tail' :: "unit list ⇒ nat ⇒ nat ⇒ nat" where
  "fib_list_tail' [] a b = b"
| "fib_list_tail' (x#xs) a b = fib_list_tail' xs (a+b) a"

definition fib_list_tail :: "unit list ⇒ nat" where
  "fib_list_tail n = fib_list_tail' n 1 1"


fun fib_induct where
  "fib_induct [] = 0"
| "fib_induct [x] = 0"
| "fib_induct (x # y # xs) = fib_induct xs + fib_induct (y # xs)"


end

Template File

theory Submission
imports Defs
begin

(***
It is well known that many functions operating on lists can be rewritten in terms of fold (right).
For instance, length = fold (λ x n → n + 1) 0 and map f = fold (λ x xs → f x :: xs) [].
Can you prove it ?
***)

lemma length_is_fold:
  "length xs = foldr (λx n. n +1) xs 0"
  by (induct xs) auto

lemma map_is_fold:
  "map f xs = foldr (λx ys. f x # ys) xs []"
  by (induct xs) auto

(***
But how strong fold actually is ?
It turns out that it is actually the unique solution to this sort of recursive definition:
  g []      = v             <-> g = fold f v
  g (x::xs) = f x (g xs)
Prove it.
***)


theorem universal_property_fold:
  fixes g :: "'a list ⇒ 'b" and f :: "'a ⇒ 'b ⇒ 'b"
  shows "(∀x xs. g (x#xs) = f x (g xs)) ⟷ (∀l. g l = foldr f l (g []))"
  sorry

lemma universal_property_foldI: 
    "(∀x xs. g (x#xs) = f x (g xs)) ⟹ g l = foldr f l (g [])"
  unfolding universal_property_fold by blast

lemma universal_property_foldI2: 
    "(∀x xs. g (x#xs) = f x (g xs)) ⟹ (g []) = n ⟹ g l = foldr f l n"
  unfolding universal_property_fold by blast

(***
Using the universal property, prove that filter and fold_left can be rewritten as a fold.
***)

lemma filter_with_fold:
  fixes p :: "'a ⇒ bool"
  shows            "∃a g. (∀xs. filter p xs = foldr g xs a)"
  sorry
 


lemma foldl_with_fold:
  fixes f :: "'a ⇒ 'b ⇒ 'a"
  shows            
  "∃a g. (∀b xs. foldl f b xs = foldr g xs a b)"
  sorry

(***
Natural integers being isomorphic with list of units, fold corresponds to function exponentiation.
Can we discover interesting properties using the universal property ?
Let's look at the Fibonacci sequence.
Unfortunately, the standard definition does not fit the requirement of the universal property.
***)

term fib_list

value "fib_list [(),(),(),()]"


(***
However, the tail recursive version does fit into the universal property theorem.
***)

term fib_list_tail'

term fib_list_tail

 
 
lemma fib_list_tail'_is_fold:
  "∃f c. fib_list_tail' xs = foldr f xs c"
  sorry
  
(***
Remarkably, this corresponds to a (convoluted) matrix exponentiation version of the Fibonacci sequence.
 ***)

thm fib_list_tail'_is_fold

(***
Now, prove that fib_list can be rewritten as a fold.    
***)

term fib_induct

thm fib_induct.induct

lemma fib_list_is_fib_list_tail:
  "fib_list n = fib_list_tail n"
  sorry
 
theorem fib_list_is_fold:
  "∃f a. fib_list n = foldr f n a (Suc 0) (Suc 0)"
  sorry

thm fib_list_is_fold

end

Check File

theory Check
imports Submission
begin


theorem universal_GOAL1: 
  "(∀x xs. (g::'a list ⇒ 'b) (x#xs) = (f::'a ⇒ 'b ⇒ 'b) x (g xs)) ⟷ (∀l. g l = foldr f l (g []))"
  by(rule Submission.universal_property_fold)

lemma universal_GOAL2: 
  "∃a g. (∀xs. filter (p::'a ⇒ bool) xs = foldr g xs a)"
  by (rule Submission.filter_with_fold)

lemma universal_GOAL3: 
  "∃a g. (∀b xs. foldl (f::'a ⇒ 'b ⇒ 'a) b xs = foldr g xs a b)"
  by (rule Submission.foldl_with_fold)

lemma universal_GOAL4:
  "∃f c. fib_list_tail' xs = foldr f xs c"
  by (rule Submission.fib_list_tail'_is_fold) 

lemma universal_GOAL5:
  "fib_list n = fib_list_tail n"
  by (rule Submission.fib_list_is_fib_list_tail) 
 
theorem universal_GOAL6:
  "∃f a. fib_list n = foldr f n a (Suc 0) (Suc 0)"
  by (rule Submission.fib_list_is_fold) 

end

Terms and Conditions