new theories ArraySorted and ArrayPermut; new program example quicksort.mlw in...

new theories ArraySorted and ArrayPermut; new program example quicksort.mlw in progress (but triggers a bug in inductive elimination)
parent 8a0401df
......@@ -16,7 +16,7 @@ module M
exception Not_found (* raised to signal a search failure *)
let binary_search (a :array int) (v : int) =
{ (* forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] *) }
{ forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
try
let l = ref 0 in
let u = ref (length a - 1) in
......
module Quicksort
use import int.Int
use import module stdlib.Ref
use import module stdlib.Array
clone import array.ArraySorted with type elt = int, logic le = (<=)
use import array.ArrayPermut
let quicksort (t : array int) =
{}
() (*(quick_rec t 0 ((array_length_ t)-1))*)
{ sorted t and permutation t (old t) }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/quicksort.gui"
End:
*)
......@@ -66,6 +66,65 @@ theory ArrayLength "Theory of arrays with length"
end
theory ArraySorted
use import int.Int
use import ArrayLength
type elt
logic le elt elt
logic sorted (a : t int elt) =
forall i1 i2 : int. 0 <= i1 <= i2 < length a -> le a[i1] a[i2]
end
theory ArrayPermut
use import int.Int
use export ArrayLength
logic exchange (a1 a2 : t int 'a) (i j : int) =
length a1 = length a2 and
a1[i] = a2[j] and a2[i] = a1[j] and
forall k:int. (k <> i and k <> j) -> a1[k] = a2[k]
lemma exchange_set :
forall a : t int 'a. forall i j : int.
exchange a (set (set a i a[j]) j a[i]) i j
inductive permut (t int 'a) (t int 'a) int int =
| permut_refl :
forall a : t int 'a. forall l u : int. permut a a l u
| permut_sym :
forall a1 a2 : t int 'a. forall l u : int.
permut a1 a2 l u -> permut a2 a1 l u
| permut_trans :
forall a1 a2 a3 : t int 'a. forall l u : int.
permut a1 a2 l u -> permut a2 a3 l u -> permut a1 a3 l u
| permut_exchange :
forall a1 a2 : t int 'a. forall l u i j : int.
l <= i <= u -> l <= j <= u -> exchange a1 a2 i j -> permut a1 a2 l u
lemma permut_weakening :
forall a1 a2 : t int 'a. forall l1 r1 l2 r2 : int.
l1 <= l2 <= r2 <= r1 -> permut a1 a2 l2 r2 -> permut a1 a2 l1 r1
lemma permut_eq :
forall a1 a2 : t int 'a. forall l u : int.
l <= u -> permut a1 a2 l u ->
forall i:int. (i < l or u < i) -> a2[i] = a1[i]
lemma permut_length :
forall a1 a2 : t int 'a. forall l u : int.
permut a1 a2 l u -> length a1 = length a2
logic permutation (a1 a2 : t int 'a) =
permut a1 a2 0 (length a1 - 1)
end
theory ArrayRich
use import int.Int
......
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