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