171 lines
3.9 KiB
Coq
171 lines
3.9 KiB
Coq
Require Import List.
|
|
Import ListNotations.
|
|
(* Print fold_left. *)
|
|
(* Print fold_right. *)
|
|
|
|
Definition compose {A B C: Type}
|
|
(g: B -> C) (f: A -> B): A -> C := fun a =>
|
|
g (f a).
|
|
Infix "∘" := compose (at level 45, right associativity).
|
|
|
|
Section Folds.
|
|
Context {A B: Type}.
|
|
Variable (f: A -> B -> B).
|
|
|
|
Fixpoint foldr (acc: B) (l: list A): B :=
|
|
match l with
|
|
| [] => acc
|
|
| x::xs => f x (foldr acc xs)
|
|
end.
|
|
End Folds.
|
|
|
|
Section Folds.
|
|
Context {A B: Type}.
|
|
Variable (f: A -> B -> B).
|
|
Variable (g: list A -> B).
|
|
Variable (acc: B).
|
|
|
|
Theorem univFold:
|
|
g [] = acc /\
|
|
(forall (x:A) (xs:list A),
|
|
g (x::xs) = f x (g xs))
|
|
<-> forall (l:list A),
|
|
g l = foldr f acc l.
|
|
Proof.
|
|
split.
|
|
- intros [HNil HCons] l.
|
|
induction l.
|
|
+ simpl; trivial.
|
|
+ simpl.
|
|
rewrite <- IHl.
|
|
rewrite (HCons a l).
|
|
reflexivity.
|
|
- intros H.
|
|
split.
|
|
+ apply H.
|
|
+ intros x xs.
|
|
rewrite (H (x::xs)).
|
|
simpl.
|
|
rewrite (H xs).
|
|
reflexivity.
|
|
Qed.
|
|
|
|
(* Theorem univFold: *)
|
|
(* g [] = acc *)
|
|
(* -> (forall (x:A) (xs:list A), *)
|
|
(* g (x::xs) = f x (g xs)) *)
|
|
(* -> forall (l:list A), *)
|
|
(* g l = foldr f acc l. *)
|
|
(* Proof. *)
|
|
(* intros HNil HCons l. *)
|
|
(* induction l. *)
|
|
(* - simpl; trivial. *)
|
|
(* - simpl. *)
|
|
(* rewrite <- IHl. *)
|
|
(* rewrite (HCons a l). *)
|
|
(* reflexivity. *)
|
|
(* Qed. *)
|
|
End Folds.
|
|
|
|
Section Folds.
|
|
Context {A B: Type}.
|
|
Variable (f g: A -> B -> B).
|
|
Variable (h: B -> B).
|
|
Variable (acc acc': B).
|
|
|
|
Theorem fusionFold:
|
|
h acc' = acc
|
|
-> (forall (a:A) (b:B),
|
|
h (g a b) = f a (h b))
|
|
-> forall l:list A,
|
|
(h ∘ (foldr g acc')) l = (foldr f acc) l.
|
|
Proof.
|
|
intros HNil HCons l.
|
|
unfold compose.
|
|
induction l.
|
|
- simpl; apply HNil.
|
|
- simpl.
|
|
rewrite HCons.
|
|
rewrite IHl.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
(* Theorem fusionFold': *)
|
|
(* h acc' = acc *)
|
|
(* /\ (forall (a:A) (b:B), *)
|
|
(* h (g a b) = f a (h b)) *)
|
|
(* <-> forall l:list A, *)
|
|
(* (h ∘ (foldr g acc')) l = (foldr f acc) l. *)
|
|
(* Proof. *)
|
|
(* unfold compose. *)
|
|
(* split. *)
|
|
(* - intros [HNil HCons] l. *)
|
|
(* induction l. *)
|
|
(* + simpl; apply HNil. *)
|
|
(* + simpl. *)
|
|
(* rewrite HCons. *)
|
|
(* rewrite IHl. *)
|
|
(* reflexivity. *)
|
|
(* - intros H. *)
|
|
(* split. *)
|
|
(* + assert (foldr g acc' [] = acc') as H1; try reflexivity. *)
|
|
(* rewrite <- H1. *)
|
|
(* assert ((h (foldr g acc' [])) = (h ∘ foldr g acc') []) as H2; try reflexivity. *)
|
|
(* rewrite H2. *)
|
|
(* assert (((foldr f acc) []) = (h ∘ foldr g acc') []) as H3; try reflexivity. *)
|
|
(* * simpl. *)
|
|
(* unfold compose. *)
|
|
(* rewrite (H []). *)
|
|
(* simpl; reflexivity. *)
|
|
(* * unfold compose. *)
|
|
(* rewrite (H []). *)
|
|
(* simpl; reflexivity. *)
|
|
(* + intros a b. *)
|
|
(* Qed. *)
|
|
End Folds.
|
|
|
|
Section UnivEg.
|
|
Fixpoint sumlist (l: list nat): nat :=
|
|
match l with
|
|
| x::l' => x + sumlist l'
|
|
| [] => 0
|
|
end.
|
|
Compute sumlist [1;2;3;4;5].
|
|
(* = 15 : nat *)
|
|
Compute ((Nat.add 1) ∘ sumlist) [1;2;3;4;5].
|
|
(* = 16 : nat *)
|
|
|
|
|
|
Lemma sumlistLemma: forall (x:nat) (xs:list nat),
|
|
S (x + sumlist xs) = x + S (sumlist xs).
|
|
Proof.
|
|
intros x xs.
|
|
induction x.
|
|
- simpl; trivial.
|
|
- simpl.
|
|
rewrite IHx.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Example sumfold: forall l:list nat,
|
|
((Nat.add 1) ∘ sumlist) l = foldr Nat.add 1 l.
|
|
Proof.
|
|
intros l.
|
|
apply univFold.
|
|
- unfold compose.
|
|
simpl; reflexivity.
|
|
- intros x xs.
|
|
unfold compose.
|
|
simpl.
|
|
(* [ring] could also be used at this stage *)
|
|
(* Require Import Arith. *)
|
|
(* ring. *)
|
|
apply sumlistLemma.
|
|
Qed. (* No induction was needed! *)
|
|
End UnivEg.
|
|
|
|
Section FusionEg.
|
|
End FusionEg.
|
|
|
|
Compute foldr Nat.add 0 [1;2;3;4;5]. (* = 15 : nat *)
|