Random access co-inductive stacks.

RACStack.coq

(** Infinite stacks with fast lookups. *)
 
(** Using co-inductive tries over binary positive integers, it is
remarkably easy to write infinite stack operations. While
maintaining an access in log(n) to the n-th element of the
stack. Of course [push] and [pull] are not constant time. I'm not
sure what the exact (amortised) complexity is. But both operation
are fairly elegant, and both their definitions and proof of
correctness are remarkably short and easy. *)
 
Require Import Coq.PArith.PArith.
 
Local Open Scope positive_scope.
 
 
(** Stacks are implemented as a co-inductive trie over binary positive
integers. Co-inductive (generalised) tries have been explored in
the context of Haskell to provide some kind of memoisation: [Stack
A] is isomorphic to [Pos.t->A] (up to extensional equality), but
thanks to sharing, previously computed values are memoised. I
don't explore these properties here. The semantics of stacks is
given by the [lookup] function below. *)
CoInductive Stack {A:Type} := {
one : A ;
twice : Stack A ;
twiceplusone : Stack A
}.
Arguments Stack A : clear implicits.
 
(** Lookup *)
 
(** Lookup is (by design) structural over the index. It is, hence,
logarithmic in the index. *)
Fixpoint lookup {A} (i:Pos.t) (s:Stack A) : A :=
match i with
| 1 => s.(one)
| j~0 => lookup j s.(twice)
| j~1 => lookup j s.(twiceplusone)
end
.
 
(** Stack Operations *)
 
(** These operations are very terse, their correctness is explicited
by the proofs that they meet their specification, below. *)
 
Definition peek {A} (s:Stack A) : A := lookup 1 s.
 
CoFixpoint pop {A} (s:Stack A) : Stack A := {|
twice := s.(twiceplusone) ;
one := peek s.(twice) ;
twiceplusone := pop s.(twice)
|}.
 
CoFixpoint push {A} (x:A) (s:Stack A) : Stack A := {|
one := x ;
twiceplusone := s.(twice) ;
twice := push s.(one) s.(twiceplusone)
|}.
 
 
(** Correctness *)
 
Lemma pop_spec A (s:Stack A) : forall i, lookup i (pop s) = lookup (i+1) s.
Proof.
intros i. revert s.
induction i as [ j h | j _ | ]; intros s.
+ (** Case [i=2j+1].
 
In that case, [i+1=2j+2 = 2(j+1)]. By induction hypothesis,
the appropriate way to look for [i] is indeed [pop
s.(twice)]. *)
rewrite !Pos.add_1_r in *.
rewrite Pos.xI_succ_xO at 2. rewrite <- Pos.double_succ.
simpl.
apply h.
+ (** Case [i=2j]
 
This case does not need the recursion hypothesis since,
obviously, [i+1=2j+1=j~1]. We, indeed, need to lookup in
[s.(twiceplusone]. *)
rewrite Pos.add_1_r, <- Pos.xI_succ_xO.
simpl.
reflexivity.
+ easy.
Qed.
 
(** Conversely for [push]. The proof is similar. *)
Lemma push_spec A x (s:Stack A) :
forall i, peek (push x s) = x /\ lookup (i+1) (push x s) = lookup i s.
Proof.
intros i.
split.
+ easy.
+ revert x s.
induction i as [ j h | j _ | ]; intros x s.
* rewrite !Pos.add_1_r in *.
rewrite Pos.xI_succ_xO, <- Pos.double_succ.
simpl.
apply h.
* rewrite !Pos.add_1_r.
rewrite <- Pos.xI_succ_xO.
simpl.
reflexivity.
* easy.
Qed.