Commit e161e554 by Jean-Christophe Filliâtre

### removed random_access_list from in_progress/

parent d00b4a8b
 (* 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 option.Option use import list.List use import list.Append use import list.HdTl 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 lemma preorder_non_nil: forall t: tree 'a. preorder t <> Nil function flatten (l: list (int, tree 'a)) : list 'a = match l with | Nil -> Nil | Cons (_, t) r -> preorder t ++ flatten r end function height (t: tree 'a) : int = match t with | Leaf _ -> 1 | Node l _ _ -> 1 + height l end lemma size_pos: forall t: tree 'a. height t >= 1 (* perfect binary tree *) predicate perfect (t: tree 'a) = match t with | Leaf _ -> true | Node l _ r -> perfect l && perfect r && height l = height r end (* increasing list of trees, starting with height at least h *) predicate well_formed_aux (h: int) (l: list (int, tree 'a)) = match l with | Nil -> true | Cons (h, t) rest -> perfect t && height t = h && well_formed_aux (h + 1) rest end predicate well_formed (l: list (int, tree 'a)) = match l with | Nil -> true | Cons (h, t) rest -> perfect t && height t = h && well_formed_aux h l end lemma well_formed_tail: forall l: list (int, tree 'a), h: int, t: tree 'a. well_formed (Cons (h,t) l) -> well_formed l type t 'a = { trees: list (int, tree 'a) } invariant { well_formed self.trees } function listof (t: t 'a) : list 'a = flatten t.trees let empty () : t 'a ensures { listof result = Nil } = { trees = Nil } let is_empty (t: t 'a) : bool ensures { result = True <-> listof t = Nil } = t.trees = Nil let cons (x: 'a) (t: t 'a) : t 'a ensures { listof result = Cons x (listof t) } = match t.trees with | Cons (h1, t1) (Cons (h2, t2) rest) -> if h1 = h2 then { trees = Cons (1+h1, Node t1 x t2) rest } else { trees = Cons (1, Leaf x) t.trees } | _ -> { trees = Cons (1, Leaf x) t.trees } end let head (t: t 'a) : option 'a ensures { result = hd (listof t) } = 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 (listof t) = None | Some t' -> tl (listof t) = Some (listof t') end } = match t.trees with | Nil -> None | Cons (_, Leaf _) trees' -> Some { trees = trees' } | Cons (h, Node l x r) rest -> let h' = h - 1 in Some { trees = Cons (h', l) (Cons (h', r) rest) } end end
 (* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. 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. Axiom preorder_non_nil : forall {a:Type} {a_WT:WhyType a}, forall (t:(@tree a a_WT)), ~ ((preorder t) = nil). (* 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 height {a:Type} {a_WT:WhyType a} (t:(@tree a a_WT)) {struct t}: Z := match t with | (Leaf _) => 1%Z | (Node l _ _) => (1%Z + (height l))%Z end. Axiom size_pos : forall {a:Type} {a_WT:WhyType a}, forall (t:(@tree a a_WT)), (1%Z <= (height t))%Z. (* Why3 assumption *) Fixpoint perfect {a:Type} {a_WT:WhyType a} (t:(@tree a a_WT)) {struct t}: Prop := match t with | (Leaf _) => True | (Node l _ r) => (perfect l) /\ ((perfect r) /\ ((height l) = (height r))) end. (* Why3 assumption *) Fixpoint well_formed_aux {a:Type} {a_WT:WhyType a} (h:Z) (l:(list (Z* (@tree a a_WT))%type)) {struct l}: Prop := match l with | nil => True | (cons (h1, t) rest) => (perfect t) /\ (((height t) = h1) /\ (well_formed_aux (h1 + 1%Z)%Z rest)) end. (* Why3 assumption *) Definition well_formed {a:Type} {a_WT:WhyType a} (l:(list (Z* (@tree a a_WT))%type)): Prop := match l with | nil => True | (cons (h, t) rest) => (perfect t) /\ (((height t) = h) /\ (well_formed_aux h l)) end. Axiom well_formed_tail : forall {a:Type} {a_WT:WhyType a}, forall (l:(list (Z* (@tree a a_WT))%type)) (h:Z) (t:(@tree a a_WT)), (well_formed (cons (h, t) l)) -> (well_formed l). (* Why3 assumption *) Inductive t (a:Type) {a_WT:WhyType a} := | mk_t : (list (Z* (@tree a a_WT))%type) -> 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 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) => x end. (* Why3 assumption *) Definition listof {a:Type} {a_WT:WhyType a} (t1:(@t a a_WT)): (list a) := (flatten (trees t1)). (* Why3 goal *) Theorem WP_parameter_is_empty : forall {a:Type} {a_WT:WhyType a}, forall (t1:(list (Z* (@tree a a_WT))%type)), (well_formed t1) -> ((t1 = nil) <-> ((flatten t1) = nil)). (* Why3 intros a a_WT t1 h1. *) intros a a_WT t1 h1. destruct t1; simpl in *. intuition. destruct p; simpl in *. generalize (preorder_non_nil t0). destruct (preorder t0); intuition. discriminate H4. discriminate H4. Qed.
 (* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. 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. Axiom preorder_non_nil : forall {a:Type} {a_WT:WhyType a}, forall (t:(@tree a a_WT)), ~ ((preorder t) = nil). (* 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 height {a:Type} {a_WT:WhyType a} (t:(@tree a a_WT)) {struct t}: Z := match t with | (Leaf _) => 1%Z | (Node l _ _) => (1%Z + (height l))%Z end. Axiom size_pos : forall {a:Type} {a_WT:WhyType a}, forall (t:(@tree a a_WT)), (1%Z <= (height t))%Z. (* Why3 assumption *) Fixpoint perfect {a:Type} {a_WT:WhyType a} (t:(@tree a a_WT)) {struct t}: Prop := match t with | (Leaf _) => True | (Node l _ r) => (perfect l) /\ ((perfect r) /\ ((height l) = (height r))) end. (* Why3 assumption *) Fixpoint well_formed_aux {a:Type} {a_WT:WhyType a} (h:Z) (l:(list (Z* (@tree a a_WT))%type)) {struct l}: Prop := match l with | nil => True | (cons (h1, t) rest) => (perfect t) /\ (((height t) = h1) /\ (well_formed_aux (h1 + 1%Z)%Z rest)) end. (* Why3 assumption *) Definition well_formed {a:Type} {a_WT:WhyType a} (l:(list (Z* (@tree a a_WT))%type)): Prop := match l with | nil => True | (cons (h, _) _) => (well_formed_aux h l) end. (* Why3 goal *) Theorem well_formed_tail : forall {a:Type} {a_WT:WhyType a}, forall (l:(list (Z* (@tree a a_WT))%type)) (h:Z) (t:(@tree a a_WT)), (well_formed (cons (h, t) l)) -> (well_formed l). intros a a_WT l h t h1. Qed.
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!