Commit af08d5c4 by Martin Clochard

### sequence theory: factor definitions/axioms as specs, add a algebraic theory

parent f954b8a6
 ... ... @@ -24,15 +24,7 @@ theory Seq axiom length_nonnegative: forall s: seq 'a. 0 <= length s (** empty sequence *) val constant empty : seq 'a axiom empty_length: length (empty: seq 'a) = 0 (** n-th element *) val function get (seq 'a) int : 'a (** [get s i] is the ([i]+1)-th element of sequence [s] (the first element has index 0) *) ... ... @@ -40,105 +32,176 @@ theory Seq let function ([]) (s: seq 'a) (i: int) : 'a = get s i (** update *) val function set (seq 'a) int 'a : seq 'a (** [set s i v] is a new sequence [u] such that [u[i] = v] and [u[j] = s[j]] otherwise *) axiom set_def1: forall s: seq 'a, i: int, v: 'a. 0 <= i < length s -> length (set s i v) = length s axiom set_def2: forall s: seq 'a, i: int, v: 'a. 0 <= i < length s -> get (set s i v) i = v axiom set_def3: forall s: seq 'a, i: int, v: 'a. 0 <= i < length s -> forall j: int. 0 <= j < length s -> j <> i -> get (set s i v) j = get s j let function ([<-]) (s: seq 'a) (i: int) (v: 'a) : seq 'a = set s i v (** equality *) (** equality is extensional *) val predicate (==) (s1 s2: seq 'a) ensures { result <-> length s1 = length s2 && forall i: int. 0 <= i < length s1 -> s1[i] = s2[i] } ensures { result -> s1 = s2 } axiom extensionality: forall s1 s2: seq 'a. s1 == s2 -> s1 = s2 (** insertion of elements on both sides *) val function cons 'a (seq 'a) : seq 'a axiom cons_length: forall x: 'a, s: seq 'a. length (cons x s) = 1 + length s (** sequence comprehension *) val function create (len: int) (f: int -> 'a) : seq 'a requires { 0 <= len } ensures { length result = len } ensures { forall i. 0 <= i < len -> result[i] = f i } axiom cons_get: forall x: 'a, s: seq 'a, i: int. 0 <= i <= length s -> (cons x s)[i] = if i = 0 then x else s[i-1] (** empty sequence *) (* FIXME: could be defined, but let constant does not accept spec. *) val constant empty : seq 'a ensures { length result = 0 } (* let constant empty : seq 'a ensures { length result = 0 } = while false do variant { 0 } () done; create 0 (fun _ requires { false } -> absurd) *) val function snoc (seq 'a) 'a : seq 'a (** update *) let function set (s:seq 'a) (i:int) (v:'a) : seq 'a requires { 0 <= i < length s } ensures { length result = length s } ensures { result[i] = v } ensures { forall j. 0 <= j < length s /\ j <> i -> result[j] = s[j] } (** [set s i v] is a new sequence [u] such that [u[i] = v] and [u[j] = s[j]] otherwise *) = while false do variant { 0 } () done; create s.length (fun j -> if j = i then v else s[j]) axiom snoc_length: forall s: seq 'a, x: 'a. length (snoc s x) = 1 + length s (* FIXME: not a real alias because of spec, but should be. *) let function ([<-]) (s: seq 'a) (i: int) (v: 'a) : seq 'a requires { 0 <= i < length s } = set s i v axiom snoc_get: forall s: seq 'a, x: 'a, i: int. 0 <= i <= length s -> (snoc s x)[i] = if i < length s then s[i] else x (** singleton sequence *) let function singleton (v:'a) : seq 'a ensures { length result = 1 } ensures { result[0] = v } = while false do variant { 0 } () done; create 1 (fun _ -> v) lemma snoc_last: forall s: seq 'a, x: 'a. (snoc s x)[length s] = x (** insertion of elements on both sides *) let function cons (x:'a) (s:seq 'a) : seq 'a ensures { length result = 1 + length s } ensures { result[0] = x } ensures { forall i. 0 < i <= length s -> result[i] = s[i-1] } = while false do variant { 0 } () done; create (1 + length s) (fun i -> if i = 0 then x else s[i-1]) let function snoc (s:seq 'a) (x:'a) : seq 'a ensures { length result = 1 + length s } ensures { result[length s] = x } ensures { forall i. 0 <= i < length s -> result[i] = s[i] } = while false do variant { 0 } () done; create (1 + length s) (fun i -> if i = length s then x else s[i]) (** sub-sequence *) val function ([_.._]) (seq 'a) int int : seq 'a let function ([_.._]) (s:seq 'a) (i:int) (j:int) : seq 'a requires { 0 <= i <= j <= length s } ensures { length result = j - i } ensures { forall k. 0 <= k < j - i -> result[k] = s[i + k] } (** [s[i..j]] is the sub-sequence of [s] from element [i] included to element [j] excluded *) = while false do variant { 0 } () done; create (j-i) (fun k -> s[i+k]) axiom sub_length: forall s: seq 'a, i j: int. 0 <= i <= j <= length s -> length s[i..j] = j - i axiom sub_get: forall s: seq 'a, i j: int. 0 <= i <= j <= length s -> forall k: int. 0 <= k < j - i -> s[i..j][k] = s[i + k] (* FIXME: spec/alias *) let function ([_..]) (s: seq 'a) (i: int) : seq 'a requires { 0 <= i <= length s } = s[i .. length s] let function ([_..]) (s: seq 'a) (i: int) : seq 'a = s[i .. length s] let function ([.._]) (s: seq 'a) (j: int) : seq 'a = s[0 .. j] (* FIXME: spec/alias *) let function ([.._]) (s: seq 'a) (j: int) : seq 'a requires { 0 <= j <= length s } = s[0 .. j] (** concatenation *) let function (++) (s1:seq 'a) (s2:seq 'a) : seq 'a ensures { length result = length s1 + length s2 } ensures { forall i. 0 <= i < length s1 -> result[i] = s1[i] } ensures { forall i. length s1 <= i < length result -> result[i] = s2[i - length s1] } = while false do variant { 0 } () done; let l = length s1 in create (l + length s2) (fun i -> if i < l then s1[i] else s2[i-l]) val function (++) (seq 'a) (seq 'a) : seq 'a axiom concat_length: forall s1 s2: seq 'a. length (s1 ++ s2) = length s1 + length s2 axiom concat_get1: forall s1 s2: seq 'a, i: int. 0 <= i < length s1 -> (s1 ++ s2)[i] = s1[i] axiom concat_get2: forall s1 s2: seq 'a, i: int. length s1 <= i < length s1 + length s2 -> (s1 ++ s2)[i] = s2[i - length s1] (** sequence comprehension *) end val function create (len: int) (f: int -> 'a) : seq 'a (** {2 lemma library about algebraic interactions between empty/singleton/cons/snoc/++/[ .. ]} *) theory FreeMonoid axiom create_length: forall len: int, f: int -> 'a. 0 <= len -> length (create len f) = len use import int.Int use import Seq axiom create_get: forall len: int, f: int -> 'a, i: int. 0 <= i < len -> (create len f)[i] = f i (* Monoidal properties/simplification. *) let lemma associative (s1 s2 s3:seq 'a) ensures { (s1 ++ s2) ++ s3 = s1 ++ (s2 ++ s3) } = if not (s1 ++ s2) ++ s3 == s1 ++ (s2 ++ s3) then absurd meta rewrite axiom associative let lemma left_neutral (s:seq 'a) ensures { empty ++ s = s } = if not empty ++ s == s then absurd meta rewrite axiom left_neutral let lemma right_neutral (s:seq 'a) ensures { s ++ empty = s } = if not s ++ empty == s then absurd meta rewrite axiom right_neutral let lemma cons_def (x:'a) (s:seq 'a) ensures { cons x s = singleton x ++ s } = if not cons x s == singleton x ++ s then absurd meta rewrite axiom cons_def let lemma snoc_def (s:seq 'a) (x:'a) ensures { snoc s x = s ++ singleton x } = if not snoc s x == s ++ singleton x then absurd meta rewrite axiom snoc_def (* Inverting cons/snoc/catenation *) let lemma cons_back (x:'a) (s:seq 'a) ensures { (cons x s)[1 ..] = s } = if not (cons x s)[1 ..] == s then absurd let lemma snoc_back (s:seq 'a) (x:'a) ensures { (snoc s x)[.. length s] = s } = if not (snoc s x)[.. length s] == s then absurd let lemma cat_back (s1 s2:seq 'a) ensures { (s1 ++ s2)[.. length s1] = s1 } ensures { (s1 ++ s2)[length s1 ..] = s2 } = let c = s1 ++ s2 in let l = length s1 in if not (c[.. l] == s1 || c[l ..] == s2) then absurd (* Decomposing sequences as cons/snoc/catenation/empty/singleton *) let lemma cons_dec (s:seq 'a) requires { length s >= 1 } ensures { s = cons s[0] s[1 ..] } = if not s == cons s[0] s[1 ..] then absurd let lemma snoc_dec (s:seq 'a) requires { length s >= 1 } ensures { s = snoc s[.. length s - 1] s[length s - 1] } = if not s == snoc s[.. length s - 1] s[length s - 1] then absurd let lemma cat_dec (s:seq 'a) (i:int) requires { 0 <= i <= length s } ensures { s = s[.. i] ++ s[i ..] } = if not s == s[.. i] ++ s[i ..] then absurd let lemma empty_dec (s:seq 'a) requires { length s = 0 } ensures { s = empty } = if not s == empty then absurd let lemma singleton_dec (s:seq 'a) requires { length s = 1 } ensures { s = singleton s[0] } = if not s == singleton s[0] then absurd end ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!