Commit 9c6979c1 by Jean-Christophe Filliâtre

### random access lists (new example in progress)

parent 44aa9329
 (* Purely Functional Random-Access Lists Chris Okasaki, FPCA, 1995. (thanks to Simon Cruanes for suggesting this example) *) module RandomAccessList use import int.Int use import int.ComputerDivision use import list.Append use import list.HdTl use import list.Nth type tree 'a = | Leaf 'a | Node (tree 'a) 'a (tree 'a) function preorder (t: tree 'a) : list 'a = match t with | Leaf x -> Cons x Nil | Node l x r -> Cons x (preorder l ++ preorder r) end function flatten (l: list (int, tree 'a)) : list 'a = match l with | Nil -> Nil | Cons (_, t) r -> preorder t ++ flatten r end function size (t: tree 'a) : int = match t with | Leaf _ -> 1 | Node l _ r -> size l + 1 + size r end lemma size_pos: forall t: tree 'a. size t >= 1 (* perfect binary tree of size s *) inductive perfect (s: int) (t: tree 'a) = | perfect_leaf: forall x: 'a. perfect 1 (Leaf x) | perfect_node: forall x: 'a, l r: tree 'a, s: int. perfect s l -> perfect s r -> perfect (1 + 2*s) (Node l x r) lemma perfect_size: forall s: int, t: tree 'a. perfect s t -> s = size t predicate well_formed (l: list (int, tree 'a)) = match l with | Nil -> true | Cons (s, t) Nil -> perfect s t | Cons (s1, t1) ((Cons (s2, t2) _) as rest) -> perfect s1 t1 && s1 < s2 && well_formed rest end predicate well_formed0 (l: list (int, tree 'a)) = match l with | Nil -> true | Cons (s, t) Nil -> perfect s t | Cons (s1, t1) ((Cons (s2, t2) _) as rest) -> perfect s1 t1 && s1 <= s2 && well_formed rest end type t 'a = { trees: list (int, tree 'a); ghost contents: list 'a; } invariant { well_formed0 self.trees } invariant { self.contents = flatten self.trees } let empty () : t 'a = { trees = Nil : list (int, tree 'a); contents = Nil } let is_empty (t: t 'a) : bool ensures { result = True <-> t.contents = Nil } = t.trees = Nil let cons (x: 'a) (t: t 'a) : t 'a ensures { result.contents = Cons x t.contents } = match t.trees with | Cons (s1, t1) (Cons (s2, t2) rest) -> if s1 = s2 then { trees = Cons (1+s1+s2, Node t1 x t2) rest; contents = Cons x t.contents } else { trees = Cons (1, Leaf x) t.trees; contents = Cons x t.contents } | _ -> { trees = Cons (1, Leaf x) t.trees; contents = Cons x t.contents } end let head (t: t 'a) : option 'a ensures { result = hd t.contents } = match t.trees with | Nil -> None | Cons (_, Leaf x) _ -> Some x | Cons (_, Node _ x _) _ -> Some x end let safe_hd (l: list 'a) : list 'a requires { l <> Nil } ensures { Some result = tl l } = match l with Nil -> absurd | Cons _ rest -> rest end let tail (t: t 'a) : option (t 'a) ensures { match result with None -> tl t.contents = None | Some t' -> tl t.contents = Some t'.contents end } = match t.trees with | Nil -> None | Cons (_, Leaf _) trees' -> Some { trees = trees'; contents = safe_hd t.contents } | Cons (size, Node l x r) rest -> let size' = div size 2 in Some { trees = Cons (size', l) (Cons (size', r) rest); contents = safe_hd t.contents } end end
 (* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require Import ZOdiv. Require BuiltIn. Require int.Int. Require int.Abs. Require int.ComputerDivision. Require list.List. Require list.Length. Require list.Mem. Require list.Nth. Require option.Option. Require list.HdTl. Require list.Append. (* Why3 assumption *) Definition unit := unit. (* Why3 assumption *) Inductive tree (a:Type) {a_WT:WhyType a} := | Leaf : a -> tree a | Node : (@tree a a_WT) -> a -> (@tree a a_WT) -> tree a. Axiom tree_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (tree a). Existing Instance tree_WhyType. Implicit Arguments Leaf [[a] [a_WT]]. Implicit Arguments Node [[a] [a_WT]]. (* Why3 assumption *) Fixpoint preorder {a:Type} {a_WT:WhyType a} (t:(@tree a a_WT)) {struct t}: (list a) := match t with | (Leaf x) => (cons x nil) | (Node l x r) => (cons x (List.app (preorder l) (preorder r))) end. (* Why3 assumption *) Fixpoint flatten {a:Type} {a_WT:WhyType a} (l:(list (Z* (@tree a a_WT))%type)) {struct l}: (list a) := match l with | nil => nil | (cons (_, t) r) => (List.app (preorder t) (flatten r)) end. (* Why3 assumption *) Fixpoint size {a:Type} {a_WT:WhyType a} (t:(@tree a a_WT)) {struct t}: Z := match t with | (Leaf _) => 1%Z | (Node l _ r) => (((size l) + 1%Z)%Z + (size r))%Z end. Axiom size_pos : forall {a:Type} {a_WT:WhyType a}, forall (t:(@tree a a_WT)), (1%Z <= (size t))%Z. (* Why3 assumption *) Inductive perfect {a:Type} {a_WT:WhyType a} : Z -> (@tree a a_WT) -> Prop := | perfect_leaf : forall (x:a), ((@perfect _ _) 1%Z (Leaf x)) | perfect_node : forall (x:a) (l:(@tree a a_WT)) (r:(@tree a a_WT)) (s:Z), ((@perfect _ _) s l) -> (((@perfect _ _) s r) -> ((@perfect _ _) (1%Z + (2%Z * s)%Z)%Z (Node l x r))). Axiom perfect_size : forall {a:Type} {a_WT:WhyType a}, forall (s:Z) (t:(@tree a a_WT)), (perfect s t) -> (s = (size t)). (* Why3 assumption *) Fixpoint well_formed {a:Type} {a_WT:WhyType a} (l:(list (Z* (@tree a a_WT))%type)) {struct l}: Prop := match l with | nil => True | (cons (s, t) nil) => (perfect s t) | (cons (s1, t1) ((cons (s2, t2) _) as rest)) => (perfect s1 t1) /\ ((s1 < s2)%Z /\ (well_formed rest)) end. (* Why3 assumption *) Definition well_formed0 {a:Type} {a_WT:WhyType a} (l:(list (Z* (@tree a a_WT))%type)): Prop := match l with | nil => True | (cons (s, t) nil) => (perfect s t) | (cons (s1, t1) ((cons (s2, t2) _) as rest)) => (perfect s1 t1) /\ ((s1 <= s2)%Z /\ (well_formed rest)) end. (* Why3 assumption *) Inductive t (a:Type) {a_WT:WhyType a} := | mk_t : (list (Z* (@tree a a_WT))%type) -> (list a) -> t a. Axiom t_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (t a). Existing Instance t_WhyType. Implicit Arguments mk_t [[a] [a_WT]]. (* Why3 assumption *) Definition contents {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): (list a) := match v with | (mk_t x x1) => x1 end. (* Why3 assumption *) Definition trees {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): (list (Z* (@tree a a_WT))%type) := match v with | (mk_t x x1) => x end. (* Why3 goal *) Theorem WP_parameter_is_empty : forall {a:Type} {a_WT:WhyType a}, forall (t1:(list (Z* (@tree a a_WT))%type)) (t2:(list a)), ((well_formed0 t1) /\ (t2 = (flatten t1))) -> ((t1 = nil) <-> (t2 = nil)). intros a a_WT t1 t2 (h1,h2). destruct t1; simpl in h2. intuition. simpl in h1. destruct p; simpl in *. intuition. discriminate H. destruct t1; simpl in h1. inversion h1; intuition. subst t0; simpl in h2. subst t2. discriminate h2. subst t0; simpl in h2. subst t2. discriminate h2. destruct t0; simpl in h2. subst t2. discriminate H. subst t2. discriminate H. Qed.