Commit 4b9ec76c authored by MARCHE Claude's avatar MARCHE Claude

LCP: only one lemma left: antisymmetry of le

parent 5774a161
......@@ -119,7 +119,14 @@ axiom lcp_spec:
*)
predicate is_longest_common_prefix (a:array int) (x y:int) (l:int) =
is_common_prefix a x y l /\ not (is_common_prefix a x y (l+1))
is_common_prefix a x y l /\
forall m:int. l < m -> not (is_common_prefix a x y m)
(* for proving lcp_sym and le_trans lemmas, and compare function in the absurd case *)
lemma longest_common_prefix_succ:
forall a:array int, x y l:int.
is_common_prefix a x y l /\ not (is_common_prefix a x y (l+1)) ->
is_longest_common_prefix a x y l
use import ref.Refint
......@@ -190,12 +197,13 @@ let test1 () =
check {x = 1}
predicate le (a : array int) (x y:int) =
predicate lt (a : array int) (x y:int) =
let n = a.length in
0 <= x <= n /\ 0 <= y <= n /\
exists l:int. is_common_prefix a x y l /\
(x+l = n \/
(x+l < n /\ y+l < n /\ a[x+l] <= a[y+l]))
(y+l < n /\ (x+l = n \/ a[x+l] < a[y+l]))
predicate le (a : array int) (x y:int) = x = y \/ lt a x y
lemma le_refl :
forall a:array int, x :int.
......
This source diff could not be displayed because it is too large. You can view the blob instead.
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