Commit b5d67fb3 authored by Martin Clochard's avatar Martin Clochard

examples: fixed proof for random_access_list

parent 6603e0f3
......@@ -193,6 +193,14 @@ module RandomAccessListWithSeq
(fun i -> let (x0, x1) = s[div i 2] in
if mod i 2 = 0 then x0 else x1)
lemma cons_flatten : forall x y :'a,s:seq ('a,'a).
let a = flatten (cons (x,y) s) in
let b = cons x (cons y (flatten s)) in
a = b by a == b by forall i. 0 <= i < a.length -> a[i] = b[i]
by (i <= 1 so (cons (x,y) s)[div i 2] = (x,y))
\/ (i >= 2 so (cons (x,y) s)[div i 2] = s[div (i-2) 2]
)
function elements (l: ral 'a) : seq 'a =
match l with
| Empty -> empty
......@@ -240,7 +248,10 @@ module RandomAccessListWithSeq
match l with
| Empty -> absurd
| One _ l1 -> Zero l1
| Zero l1 -> let (_, x1) = lookup 0 l1 in One x1 (tail l1)
| Zero l1 -> let (_, x1) as p = lookup 0 l1 in
let tl = tail l1 in
assert { elements l1 == cons p (elements tl) };
One x1 tl
end
(** update in O(log n)
......@@ -255,14 +266,22 @@ module RandomAccessListWithSeq
let rec fupdate (f: 'a -> 'a) (i: int) (l: ral 'a) : ral 'a
requires { 0 <= i < length (elements l) }
variant { i, l}
ensures { elements result == setf (elements l) i f}
variant { i, l }
ensures { elements result == setf (elements l) i f }
=
match l with
| Empty -> absurd
| One x l1 -> if i = 0 then One (f x) l1 else
cons x (fupdate f (i-1) (Zero l1))
| Zero l1 -> Zero (fupdate (aux i f) (div i 2) l1)
| Zero l1 ->
let ul1 = fupdate (aux i f) (div i 2) l1 in
let res = Zero ul1 in
assert { forall j. 0 <= j < length (elements res) ->
(elements res)[j] = (setf (elements l) i f)[j]
by div j 2 <> div i 2 ->
(elements ul1)[div j 2] = (elements l1)[div j 2]
};
res
end
let function f (y: 'a) : 'a -> 'a = fun _ -> y
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Require list.List.
Require list.Length.
Require list.Nth.
Require option.Option.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive ral
(a:Type) :=
| Empty : ral a
| Zero : (ral (a* a)%type) -> ral a
| One : a -> (ral (a* a)%type) -> ral a.
Axiom ral_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ral a).
Existing Instance ral_WhyType.
Implicit Arguments Empty [[a]].
Implicit Arguments Zero [[a]].
Implicit Arguments One [[a]].
(* Why3 assumption *)
Fixpoint flatten {a:Type} {a_WT:WhyType a} (l:(list (a*
a)%type)) {struct l}: (list a) :=
match l with
| Init.Datatypes.nil => Init.Datatypes.nil
| (Init.Datatypes.cons (x, y) l1) =>
(Init.Datatypes.cons x (Init.Datatypes.cons y (flatten l1)))
end.
(* Why3 goal *)
Theorem length_flatten : forall {a:Type} {a_WT:WhyType a},
forall (l:(list (a* a)%type)),
((list.Length.length (flatten l)) = (2%Z * (list.Length.length l))%Z).
intros l.
induction l.
auto.
simpl (flatten (a0::l)).
destruct a0.
replace (Length.length ((a0,a1)::l))
with (1 + (Length.length l))%Z by auto.
unfold Length.length at 1; fold Length.length.
rewrite IHl.
ring.
Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment