1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
(** In general, one can require more elaborate loop invariants.
This [fast_length] function computes the length of a list using
tail recursion: *)
Equations fast_length {A} (l : list A) : nat :=
fast_length l := go 0 l
where go : nat -> list A -> nat :=
go n [] := n;
go n (_ :: l) := go (S n) l.
(** To prove its correctness, we show its pointwise equivalence to
regular [length l]. *)
Lemma fast_length_length : forall {A} (l : list A), length l = fast_length l.
Proof.
(** Applying the eliminator is a bit more tricky in this case:
we must the length
*)
apply (fast_length_elim (fun A l res => length l = res)
(fun A l res l' lenl => res + length l' = lenl));
intros l H; simpl in *; intuition auto with arith; lia.
Qed.
Equations list_init {A} (n : nat) (a : A) : list A :=
list_init 0 _ := [];
list_init (S n) x := x :: list_init n x.
Require Import NArith.
Equations pos_list_init {A} (n : positive) (a : A) : list A :=
pos_list_init xH x := [x];
pos_list_init (n~1) x := let l := pos_list_init n x in x :: l ++ l;
pos_list_init (n~0) x := let l := pos_list_init n x in x :: l ++ l.
(* Time Definition big_interval := Eval vm_compute in pos_list_init 20000 true. *)
(* Extraction length. *)
(* Extraction fast_length. *)
(* Time Definition slow := Eval vm_compute in length big_interval. *)
(* Time Definition fast := Eval vm_compute in fast_length big_interval. *)
|
