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.

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.

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.

Download Files
### Definitions File

### Template File

### Check 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

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

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

### Template File

### Check 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

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

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

### Template 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.

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

### Template File

### Check 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

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

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

### Template File

### Check 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

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

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

Terms and Conditions