Commit 015baaec by Jean-Christophe Filliâtre

### programs: more examples with algebraic datatypes

parent 6e72c531
 { use import list.Length use import list.Sorted use import list.Permut (* FIXME *) lemma Nil_not_Cons : forall x:int, l:list int. Nil <> Cons x l } let rec insert x l variant { length l } = { sorted l } match l with | Nil -> Cons x Nil | Cons y r -> if x <= y then Cons x l else Cons y (insert x r) end { sorted result and permut (Cons x l) result } let rec insertion_sort l variant { length l } = { } match l with | Nil -> Nil | Cons x r -> insert x (insertion_sort r) end { sorted result and permut l result } (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/insertion_sort_list" End: *)
 (* find a value in a sorted list *) { use import list.Mem use import list.Sorted inductive sorted (l : list int) = | Sorted_Nil : sorted Nil | Sorted_One : forall x:int. sorted (Cons x Nil) | Sorted_Two : forall x y : int, l : list int. x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) lemma Sorted_inversion : forall y : int, l : list int. sorted (Cons y l) -> sorted l (* FIXME *) lemma Nil_not_Cons : forall x:int, l:list int. Nil <> Cons x l lemma Sorted_not_mem: forall x y : int, l : list int. ... ...
 ... ... @@ -113,10 +113,13 @@ let build_maze (n:int) = } let x = rand n in let y = rand n in (*let d = rand 2 in*) let w = x+1 (* select d (x+1) x *) (*if d = 0 then x+1 else x *) in let z = y (* select d y (y+1) *) (*if d = 0 then y else y+1*) in if andb (w < n) (z < n) then (* TODO && *) begin let d = rand 2 in let w = if d = 0 then x+1 else x in let z = if d = 0 then y else y+1 in (* let (w, z) = if d = 0 then (x+1, y) else (x, y+1) in *) if w < n && z < n then begin let a = y * n + x in assert { 0 <= a < n*n }; let b = w * n + z in ... ...
 ... ... @@ -138,6 +138,7 @@ parameter set : *) let set a i v = { 0 <= i < sa_sz !a and invariant !a } (* let SA val idx back sz n = !a in *) let val = sa_val !a in let idx = sa_idx !a in let back = sa_back !a in ... ...
 ... ... @@ -9,8 +9,8 @@ type uf = UF (link : array int) (dist : array int) (* distance to representative *) (size : int) (num : int) (size : int) (* elements are 0..size-1 *) (num : int) (* number of classes *) logic inv (u : uf) = let (UF l d s n) = u in ... ... @@ -43,7 +43,6 @@ let create (n:int) = forall j:int. 0 <= j < !i -> !l#j = j } variant { n - !i } l := A.store !l !i !i; i := !i + 1 done; ref (UF !l (A.const_length 0 n) n n) ... ... @@ -51,16 +50,17 @@ let create (n:int) = num !result = n and size !result = n and forall x:int. 0 <= x < n -> repr !result x = x } let find (u:ref uf) (x:int) = let rec find (u:ref uf) (x:int) variant { dist !u # x } = { inv !u and 0 <= x < size !u } let l = link !u in let y = ref x in while A.select l !y <> !y do invariant { 0 <= !y < size !u and same !u x !y } variant { dist(!u) # !y } y := A.select l !y done; !y let y = A.select (link !u) x in if y <> x then begin let r = find u y in let l = A.store (link !u) x r in let d = A.store (dist !u) x 1 in u := UF l d (size !u) (num !u); r end else x { inv !u and result = repr !u x and size !u = size (old !u) and num !u = num (old !u) and ... ...
 ... ... @@ -29,19 +29,92 @@ theory Mem end theory Sorted use export List use import int.Int inductive sorted (l : list int) = | Sorted_Nil : sorted Nil | Sorted_One : forall x:int. sorted (Cons x Nil) | Sorted_Two : forall x y : int, l : list int. x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) use import Mem lemma Sorted_mem : forall x : int, l : list int. (forall y : int. mem y l -> x <= y) and sorted l <-> sorted (Cons x l) end theory NumOcc use import int.Int use import List (* number of occurence of x in l *) logic num_occ (x : 'a) (l : list 'a) : int = match l with | Nil -> 0 | Cons y r -> (if x = y then 1 else 0) + num_occ x r end use import Mem lemma Mem_Num_Occ : forall x:'a, l:list 'a. mem x l <-> num_occ x l > 0 end theory Permut (* TODO *) use import NumOcc use import List logic permut (l1 : list 'a) (l2 : list 'a) = forall x : 'a. num_occ x l1 = num_occ x l2 lemma Permut_refl : forall l : list 'a. permut l l lemma Permut_sym : forall l1 l2 : list 'a. permut l1 l2 -> permut l2 l1 lemma Permut_trans : forall l1 l2 l3 : list 'a. permut l1 l2 -> permut l2 l3 -> permut l1 l3 lemma Permut_cons : forall x : 'a, l1 l2 : list 'a. permut l1 l2 -> permut (Cons x l1) (Cons x l2) lemma Permut_swap : forall x y : 'a, l : list 'a. permut (Cons x (Cons y l)) (Cons y (Cons x l)) use import Mem lemma Permut_mem : forall x : 'a, l1 l2 : list 'a. permut l1 l2 -> mem x l1 -> mem x l2 use import Length lemma Permut_length : forall l1 l2 : list 'a. permut l1 l2 -> length l1 = length l2 end theory Induction use import List logic p (list 'a) type elt logic p (list elt) axiom Induction : p (Nil : list 'a) -> (forall x:'a. forall l:list 'a. p l -> p (Cons x l)) -> forall l:list 'a. p l p (Nil : list elt) -> (forall x:elt. forall l:list elt. p l -> p (Cons x l)) -> forall l:list elt. p l end ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!