pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-19 19:57:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

FirstClassFunctions compiles again

Browse source
This commit is contained in:
Adam Chlipala 2020-02-12 13:53:55 -05:00
parent fbf211bad2
commit 6f17daa2df
1 changed files with 7 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
FirstClassFunctions.v
View file

@ -732,8 +732,6 @@ Fixpoint allSublists {A} (ls : list A) : list (list A) :=
Compute allSublists [1; 2; 3]. Compute allSublists [1; 2; 3].
Definition sum ls := fold_left plus ls 0.
(* This is the main function we want to define. It looks for a sublist whose (* This is the main function we want to define. It looks for a sublist whose
* sum matches some target. *) * sum matches some target. *)
Fixpoint sublistSummingTo (ns : list nat) (target : nat) : option (list nat) := Fixpoint sublistSummingTo (ns : list nat) (target : nat) : option (list nat) :=
@ -1075,16 +1073,16 @@ Fixpoint flattenKD {A} (fuel : nat) (t : tree A) (acc : list A)
(* A somewhat peculiar notion of size for trees. Why that 2 instead of 1? (* A somewhat peculiar notion of size for trees. Why that 2 instead of 1?
* Because it lets the proof below work out! *) * Because it lets the proof below work out! *)
Fixpoint size {A} (t : tree A) : nat := Fixpoint tree_size {A} (t : tree A) : nat :=
match t with match t with
| Leaf => 0 | Leaf => 0
| Node l _ r => 2 + size l + size r | Node l _ r => 2 + tree_size l + tree_size r
end. end.
Fixpoint continuation_size {A} (k : flatten_continuation A) : nat := Fixpoint continuation_size {A} (k : flatten_continuation A) : nat :=
match k with match k with
| KDone => 0 | KDone => 0
| KMore l d k' => 1 + size l + continuation_size k' | KMore l d k' => 1 + tree_size l + continuation_size k'
end. end.
(* A continuation encodes a flattening call, waiting to be run. (* A continuation encodes a flattening call, waiting to be run.
@ -1100,7 +1098,7 @@ Fixpoint flatten_cont {A} (k : flatten_continuation A) : list A :=
* *strong induction* via the parameter [fuel], which bounds the actual fuel * *strong induction* via the parameter [fuel], which bounds the actual fuel
* amount [fuel']. *) * amount [fuel']. *)
Lemma flattenKD_ok' : forall {A} fuel fuel' (t : tree A) acc k, Lemma flattenKD_ok' : forall {A} fuel fuel' (t : tree A) acc k,
size t + continuation_size k < fuel' < fuel tree_size t + continuation_size k < fuel' < fuel
-> flattenKD fuel' t acc k -> flattenKD fuel' t acc k
= flatten_cont k ++ flatten t ++ acc. = flatten_cont k ++ flatten t ++ acc.
Proof. Proof.
@ -1126,10 +1124,10 @@ Qed.
(* A nice, simple final theorem can be stated, when we initialize fuel in the (* A nice, simple final theorem can be stated, when we initialize fuel in the
* right way. *) * right way. *)
Theorem flattenKD_ok : forall {A} (t : tree A), Theorem flattenKD_ok : forall {A} (t : tree A),
flattenKD (size t + 1) t [] KDone = flatten t. flattenKD (tree_size t + 1) t [] KDone = flatten t.
Proof. Proof.
simplify. simplify.
rewrite flattenKD_ok' with (fuel := size t + 2). rewrite flattenKD_ok' with (fuel := tree_size t + 2).
simplify. simplify.
apply app_nil_r. apply app_nil_r.
simplify. simplify.
@ -1191,7 +1189,7 @@ Proof.
Qed. Qed.
Theorem flattenS_ok : forall {A} (t : tree A), Theorem flattenS_ok : forall {A} (t : tree A),
flattenS (size t + 1) t [] [] = flatten t. flattenS (tree_size t + 1) t [] [] = flatten t.
Proof. Proof.
simplify. simplify.
rewrite flattenS_flattenKD. rewrite flattenS_flattenKD.