[Proof Ground 2019] Fold

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

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.

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

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

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