Commit b11896fb authored by Martin Clochard's avatar Martin Clochard

sequence: minor

parent 17ff099b
......@@ -136,7 +136,7 @@ theory FreeMonoid
(* Monoidal properties/simplification. *)
let lemma associative (s1 s2 s3:seq 'a)
ensures { (s1 ++ s2) ++ s3 = s1 ++ (s2 ++ s3) }
ensures { s1 ++ (s2 ++ s3) = (s1 ++ s2) ++ s3 }
= if not (s1 ++ s2) ++ s3 == s1 ++ (s2 ++ s3) then absurd
meta rewrite axiom associative
......@@ -160,6 +160,12 @@ theory FreeMonoid
= if not snoc s x == s ++ singleton x then absurd
meta rewrite axiom snoc_def
let lemma double_sub_sequence (s:seq 'a) (i j k l:int)
requires { 0 <= i <= j <= length s }
requires { 0 <= k <= l <= j - i }
ensures { s[i .. j][k .. l] = s[k+i .. l+i] }
= if not s[i .. j][k .. l] == s[k+i .. l+i] then absurd
(* Inverting cons/snoc/catenation *)
let lemma cons_back (x:'a) (s:seq 'a)
......
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