Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit f6390a01 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix Coq scripts for examples/edit_distance.mlw.

parent 36507dad
......@@ -4,34 +4,15 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require list.List.
Require list.Length.
Require list.Mem.
Require map.Map.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive list
(a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Fixpoint length {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
a)), (0%Z <= (length l))%Z.
Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.
......@@ -41,108 +22,74 @@ Definition word := (list char).
(* Why3 assumption *)
Inductive dist : (list char) -> (list char) -> Z -> Prop :=
| dist_eps : (dist (Nil :(list char)) (Nil :(list char)) 0%Z)
| dist_eps : (dist nil nil 0%Z)
| dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist (Cons a w1) w2 (n + 1%Z)%Z)
w2 n) -> forall (a:char), (dist (cons a w1) w2 (n + 1%Z)%Z)
| dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist w1 (Cons a w2) (n + 1%Z)%Z)
w2 n) -> forall (a:char), (dist w1 (cons a w2) (n + 1%Z)%Z)
| dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist (Cons a w1) (Cons a w2) n).
w2 n) -> forall (a:char), (dist (cons a w1) (cons a w2) n).
(* Why3 assumption *)
Definition min_dist (w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z.
(* Why3 assumption *)
Fixpoint infix_plpl {a:Type} {a_WT:WhyType a} (l1:(list a)) (l2:(list
a)) {struct l1}: (list a) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl l (Nil :(list a))) = l).
Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), ((length (infix_plpl l1
l2)) = ((length l1) + (length l2))%Z).
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x
l2)).
Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
(l = (infix_plpl l1 (Cons x l2))).
(* Why3 assumption *)
Fixpoint last_char (a:char) (u:(list char)) {struct u}: char :=
match u with
| Nil => a
| (Cons c u') => (last_char c u')
| nil => a
| (cons c u') => (last_char c u')
end.
(* Why3 assumption *)
Fixpoint but_last (a:char) (u:(list char)) {struct u}: (list char) :=
match u with
| Nil => (Nil :(list char))
| (Cons c u') => (Cons a (but_last c u'))
| nil => nil
| (cons c u') => (cons a (but_last c u'))
end.
Axiom first_last_explicit : forall (u:(list char)) (a:char),
((infix_plpl (but_last a u) (Cons (last_char a u) (Nil :(list
char)))) = (Cons a u)).
((List.app (but_last a u) (cons (last_char a u) nil)) = (cons a u)).
Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char),
exists b:char, ((infix_plpl v (Cons b (Nil :(list char)))) = (Cons a u)) /\
((length v) = (length u)).
exists b:char, ((List.app v (cons b nil)) = (cons a u)) /\
((list.Length.length v) = (list.Length.length u)).
Axiom key_lemma_right : forall (w1:(list char)) (w'2:(list char)) (m:Z)
(a:char), (dist w1 w'2 m) -> forall (w2:(list char)), (w'2 = (Cons a
w2)) -> exists u1:(list char), exists v1:(list char), exists k:Z,
(w1 = (infix_plpl u1 v1)) /\ ((dist v1 w2 k) /\
((k + (length u1))%Z <= (m + 1%Z)%Z)%Z).
(a:char), (dist w1 w'2 m) -> forall (w2:(list char)),
(w'2 = (cons a w2)) -> exists u1:(list char), exists v1:(list char),
exists k:Z, (w1 = (List.app u1 v1)) /\ ((dist v1 w2 k) /\
((k + (list.Length.length u1))%Z <= (m + 1%Z)%Z)%Z).
Axiom dist_symetry : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> (dist w2 w1 n).
Axiom key_lemma_left : forall (w1:(list char)) (w2:(list char)) (m:Z)
(a:char), (dist (Cons a w1) w2 m) -> exists u2:(list char), exists v2:(list
char), exists k:Z, (w2 = (infix_plpl u2 v2)) /\ ((dist w1 v2 k) /\
((k + (length u2))%Z <= (m + 1%Z)%Z)%Z).
(a:char), (dist (cons a w1) w2 m) -> exists u2:(list char),
exists v2:(list char), exists k:Z, (w2 = (List.app u2 v2)) /\ ((dist w1 v2
k) /\ ((k + (list.Length.length u2))%Z <= (m + 1%Z)%Z)%Z).
Axiom dist_concat_left : forall (u:(list char)) (v:(list char)) (w:(list
char)) (n:Z), (dist v w n) -> (dist (infix_plpl u v) w ((length u) + n)%Z).
Axiom dist_concat_left : forall (u:(list char)) (v:(list char))
(w:(list char)) (n:Z), (dist v w n) -> (dist (List.app u v) w
((list.Length.length u) + n)%Z).
Axiom dist_concat_right : forall (u:(list char)) (v:(list char)) (w:(list
char)) (n:Z), (dist v w n) -> (dist v (infix_plpl u w) ((length u) + n)%Z).
Axiom dist_concat_right : forall (u:(list char)) (v:(list char))
(w:(list char)) (n:Z), (dist v w n) -> (dist v (List.app u w)
((list.Length.length u) + n)%Z).
Axiom min_dist_equal : forall (w1:(list char)) (w2:(list char)) (a:char)
(n:Z), (min_dist w1 w2 n) -> (min_dist (Cons a w1) (Cons a w2) n).
(n:Z), (min_dist w1 w2 n) -> (min_dist (cons a w1) (cons a w2) n).
Axiom min_dist_diff : forall (w1:(list char)) (w2:(list char)) (a:char)
(b:char) (m:Z) (p:Z), (~ (a = b)) -> ((min_dist (Cons a w1) w2 p) ->
((min_dist w1 (Cons b w2) m) -> (min_dist (Cons a w1) (Cons b w2)
(b:char) (m:Z) (p:Z), (~ (a = b)) -> ((min_dist (cons a w1) w2 p) ->
((min_dist w1 (cons b w2) m) -> (min_dist (cons a w1) (cons b w2)
((Zmin m p) + 1%Z)%Z))).
Axiom min_dist_eps : forall (w:(list char)) (a:char) (n:Z), (min_dist w
(Nil :(list char)) n) -> (min_dist (Cons a w) (Nil :(list char))
(n + 1%Z)%Z).
Axiom min_dist_eps : forall (w:(list char)) (a:char) (n:Z), (min_dist w nil
n) -> (min_dist (cons a w) nil (n + 1%Z)%Z).
Axiom min_dist_eps_length : forall (w:(list char)), (min_dist (Nil :(list
char)) w (length w)).
Axiom min_dist_eps_length : forall (w:(list char)), (min_dist nil w
(list.Length.length w)).
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
......@@ -152,7 +99,7 @@ Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
match v with
| (mk_ref x) => x
end.
......@@ -160,50 +107,53 @@ Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length1 {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length1 a1) (map.Map.set (elts a1) i v)).
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (array a) :=
(mk_array n (map.Map.const v:(map.Map.map Z a))).
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
(mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
Parameter suffix: (array char) -> Z -> (list char).
Parameter suffix: (@array char char_WhyType) -> Z -> (list char).
Axiom suffix_nil : forall (a:(array char)), ((suffix a
(length1 a)) = (Nil :(list char))).
Axiom suffix_nil : forall (a:(@array char char_WhyType)), ((suffix a
(length a)) = nil).
Axiom suffix_cons : forall (a:(array char)) (i:Z), ((0%Z <= i)%Z /\
(i < (length1 a))%Z) -> ((suffix a i) = (Cons (get a i) (suffix a
(i + 1%Z)%Z))).
Axiom suffix_cons : forall (a:(@array char char_WhyType)) (i:Z),
((0%Z <= i)%Z /\ (i < (length a))%Z) -> ((suffix a i) = (cons (get a
i) (suffix a (i + 1%Z)%Z))).
Axiom suffix_length : forall (a:(array char)) (i:Z), ((0%Z <= i)%Z /\
(i <= (length1 a))%Z) -> ((length (suffix a i)) = ((length1 a) - i)%Z).
Axiom suffix_length : forall (a:(@array char char_WhyType)) (i:Z),
((0%Z <= i)%Z /\ (i <= (length a))%Z) -> ((list.Length.length (suffix a
i)) = ((length a) - i)%Z).
(* Why3 assumption *)
Definition min_suffix (a1:(array char)) (a2:(array char)) (i:Z) (j:Z)
(n:Z): Prop := (min_dist (suffix a1 i) (suffix a2 j) n).
Definition min_suffix (a1:(@array char char_WhyType)) (a2:(@array
char char_WhyType)) (i:Z) (j:Z) (n:Z): Prop := (min_dist (suffix a1 i)
(suffix a2 j) n).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
......@@ -211,21 +161,22 @@ Open Scope Z_scope.
(* Why3 goal *)
Theorem WP_parameter_distance : forall (w1:Z) (w2:Z),
forall (w21:(map.Map.map Z char)) (w11:(map.Map.map Z char)), let w22 :=
(mk_array w2 w21) in let w12 := (mk_array w1 w11) in (((0%Z <= w1)%Z /\
(0%Z <= w2)%Z) -> let o := (w2 + 1%Z)%Z in ((0%Z <= o)%Z ->
((0%Z <= o)%Z -> ((0%Z <= w2)%Z -> forall (t:(map.Map.map Z Z)),
(forall (j:Z), ((0%Z <= j)%Z /\ (j < (w2 + 1%Z)%Z)%Z) -> ((map.Map.get t
j) = (w2 - j)%Z)) -> let o1 := (w1 - 1%Z)%Z in ((0%Z <= o1)%Z ->
forall (t1:(map.Map.map Z Z)), forall (i:Z), ((i <= o1)%Z /\
(0%Z <= i)%Z) -> ((forall (j:Z), ((0%Z <= j)%Z /\ (j <= w2)%Z) -> (min_dist
(suffix w12 (i + 1%Z)%Z) (suffix w22 j) (map.Map.get t1 j))) ->
(((0%Z <= o)%Z /\ ((0%Z <= w2)%Z /\ (w2 < o)%Z)) -> (((0%Z <= w2)%Z /\
(w2 < o)%Z) -> (((0%Z <= w2)%Z /\ (w2 < o)%Z) -> forall (t2:(map.Map.map Z
Z)), ((0%Z <= o)%Z /\ (t2 = (map.Map.set t1 w2 ((map.Map.get t1
w2) + 1%Z)%Z))) -> (((w2 - 1%Z)%Z < 0%Z)%Z -> forall (j:Z),
((0%Z <= j)%Z /\ (j <= w2)%Z) -> (min_dist (suffix w12
((i - 1%Z)%Z + 1%Z)%Z) (suffix w22 j) (map.Map.get t2 j)))))))))))).
forall (w21:(@map.Map.map Z _ char char_WhyType)) (w11:(@map.Map.map Z _
char char_WhyType)), let w22 := (mk_array w2 w21) in let w12 :=
(mk_array w1 w11) in (((0%Z <= w1)%Z /\ (0%Z <= w2)%Z) -> let o :=
(w2 + 1%Z)%Z in ((0%Z <= o)%Z -> ((0%Z <= o)%Z -> ((0%Z <= w2)%Z ->
forall (t:(@map.Map.map Z _ Z _)), (forall (j:Z), ((0%Z <= j)%Z /\
(j < (w2 + 1%Z)%Z)%Z) -> ((map.Map.get t j) = (w2 - j)%Z)) -> let o1 :=
(w1 - 1%Z)%Z in ((0%Z <= o1)%Z -> forall (t1:(@map.Map.map Z _ Z _)),
forall (i:Z), ((i <= o1)%Z /\ (0%Z <= i)%Z) -> ((forall (j:Z),
((0%Z <= j)%Z /\ (j <= w2)%Z) -> (min_dist (suffix w12 (i + 1%Z)%Z)
(suffix w22 j) (map.Map.get t1 j))) -> (((0%Z <= o)%Z /\ ((0%Z <= w2)%Z /\
(w2 < o)%Z)) -> (((0%Z <= w2)%Z /\ (w2 < o)%Z) -> (((0%Z <= w2)%Z /\
(w2 < o)%Z) -> forall (t2:(@map.Map.map Z _ Z _)), ((0%Z <= o)%Z /\
(t2 = (map.Map.set t1 w2 ((map.Map.get t1 w2) + 1%Z)%Z))) ->
(((w2 - 1%Z)%Z < 0%Z)%Z -> forall (j:Z), ((0%Z <= j)%Z /\ (j <= w2)%Z) ->
(min_dist (suffix w12 ((i - 1%Z)%Z + 1%Z)%Z) (suffix w22 j) (map.Map.get t2
j)))))))))))).
(* Why3 intros w1 w2 w21 w11 w22 w12 (h1,h2) o h3 h4 h5 t h6 o1 h7 t1 i
(h8,h9) h10 (h11,(h12,h13)) (h14,h15) (h16,h17) t2 (h18,h19) h20 j
(h21,h22). *)
......@@ -234,7 +185,7 @@ intros w1 w2 w21 w11 w22 w12 (h1,h2) o h3 h4 _ t h5 o1 h6 t1 i (h7,h8) h9 (h10,h
subst o o1.
replace (i-1+1) with i by omega.
rewrite suffix_cons.
assert (h : length1 w22 = j) by ae.
assert (h : length w22 = j) by ae.
ae.
ae.
Qed.
......
......@@ -4,144 +4,92 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require list.List.
Require list.Length.
Require list.Mem.
Require map.Map.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
a)), (0%Z <= (length l))%Z.
Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
Definition unit := unit.
Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.
(* Why3 assumption *)
Definition word := (list char).
Definition word := (list char).
(* Why3 assumption *)
Inductive dist : (list char) -> (list char) -> Z -> Prop :=
| dist_eps : (dist (Nil :(list char)) (Nil :(list char)) 0%Z)
| dist_eps : (dist nil nil 0%Z)
| dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist (Cons a w1) w2 (n + 1%Z)%Z)
w2 n) -> forall (a:char), (dist (cons a w1) w2 (n + 1%Z)%Z)
| dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist w1 (Cons a w2) (n + 1%Z)%Z)
w2 n) -> forall (a:char), (dist w1 (cons a w2) (n + 1%Z)%Z)
| dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist (Cons a w1) (Cons a w2) n).
w2 n) -> forall (a:char), (dist (cons a w1) (cons a w2) n).
(* Why3 assumption *)
Definition min_dist(w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
Definition min_dist (w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z.
(* Why3 assumption *)
Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list
a)) {struct l1}: (list a) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl l (Nil :(list a))) = l).
Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), ((length (infix_plpl l1
l2)) = ((length l1) + (length l2))%Z).
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x
l2)).
Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
(l = (infix_plpl l1 (Cons x l2))).
(* Why3 assumption *)
Fixpoint last_char(a:char) (u:(list char)) {struct u}: char :=
Fixpoint last_char (a:char) (u:(list char)) {struct u}: char :=
match u with
| Nil => a
| (Cons c u') => (last_char c u')
| nil => a
| (cons c u') => (last_char c u')
end.
(* Why3 assumption *)
Fixpoint but_last(a:char) (u:(list char)) {struct u}: (list char) :=
Fixpoint but_last (a:char) (u:(list char)) {struct u}: (list char) :=
match u with
| Nil => (Nil :(list char))
| (Cons c u') => (Cons a (but_last c u'))
| nil => nil
| (cons c u') => (cons a (but_last c u'))
end.
Axiom first_last_explicit : forall (u:(list char)) (a:char),
((infix_plpl (but_last a u) (Cons (last_char a u) (Nil :(list
char)))) = (Cons a u)).
((List.app (but_last a u) (cons (last_char a u) nil)) = (cons a u)).
Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char),
exists b:char, ((infix_plpl v (Cons b (Nil :(list char)))) = (Cons a u)) /\
((length v) = (length u)).
exists b:char, ((List.app v (cons b nil)) = (cons a u)) /\
((list.Length.length v) = (list.Length.length u)).
Axiom key_lemma_right : forall (w1:(list char)) (w'2:(list char)) (m:Z)
(a:char), (dist w1 w'2 m) -> forall (w2:(list char)), (w'2 = (Cons a
w2)) -> exists u1:(list char), exists v1:(list char), exists k:Z,
(w1 = (infix_plpl u1 v1)) /\ ((dist v1 w2 k) /\
((k + (length u1))%Z <= (m + 1%Z)%Z)%Z).
(a:char), (dist w1 w'2 m) -> forall (w2:(list char)),
(w'2 = (cons a w2)) -> exists u1:(list char), exists v1:(list char),
exists k:Z, (w1 = (List.app u1 v1)) /\ ((dist v1 w2 k) /\
((k + (list.Length.length u1))%Z <= (m + 1%Z)%Z)%Z).
Axiom dist_symetry : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> (dist w2 w1 n).
Axiom key_lemma_left : forall (w1:(list char)) (w2:(list char)) (m:Z)
(a:char), (dist (Cons a w1) w2 m) -> exists u2:(list char), exists v2:(list
char), exists k:Z, (w2 = (infix_plpl u2 v2)) /\ ((dist w1 v2 k) /\
((k + (length u2))%Z <= (m + 1%Z)%Z)%Z).
(a:char), (dist (cons a w1) w2 m) -> exists u2:(list char),
exists v2:(list char), exists k:Z, (w2 = (List.app u2 v2)) /\ ((dist w1 v2
k) /\ ((k + (list.Length.length u2))%Z <= (m + 1%Z)%Z)%Z).
Axiom dist_concat_left : forall (u:(list char)) (v:(list char)) (w:(list
char)) (n:Z), (dist v w n) -> (dist (infix_plpl u v) w ((length u) + n)%Z).
Axiom dist_concat_left : forall (u:(list char)) (v:(list char))
(w:(list char)) (n:Z), (dist v w n) -> (dist (List.app u v) w
((list.Length.length u) + n)%Z).
Axiom dist_concat_right : forall (u:(list char)) (v:(list char)) (w:(list
char)) (n:Z), (dist v w n) -> (dist v (infix_plpl u w) ((length u) + n)%Z).
Axiom dist_concat_right : forall (u:(list char)) (v:(list char))
(w:(list char)) (n:Z), (dist v w n) -> (dist v (List.app u w)
((list.Length.length u) + n)%Z).
Axiom min_dist_equal : forall (w1:(list char)) (w2:(list char)) (a:char)
(n:Z), (min_dist w1 w2 n) -> (min_dist (Cons a w1) (Cons a w2) n).
(n:Z), (min_dist w1 w2 n) -> (min_dist (cons a w1) (cons a w2) n).
Axiom min_dist_diff : forall (w1:(list char)) (w2:(list char)) (a:char)
(b:char) (m:Z) (p:Z), (~ (a = b)) -> ((min_dist (Cons a w1) w2 p) ->
((min_dist w1 (Cons b w2) m) -> (min_dist (Cons a w1) (Cons b w2)
(b:char) (m:Z) (p:Z), (~ (a = b)) -> ((min_dist (cons a w1) w2 p) ->
((min_dist w1 (cons b w2) m) -> (min_dist (cons a w1) (cons b w2)
((Zmin m p) + 1%Z)%Z))).
Axiom min_dist_eps : forall (w:(list char)) (a:char) (n:Z), (min_dist w
(Nil :(list char)) n) -> (min_dist (Cons a w) (Nil :(list char))
(n + 1%Z)%Z).
Axiom min_dist_eps : forall (w:(list char)) (a:char) (n:Z), (min_dist w nil
n) -> (min_dist (cons a w) nil (n + 1%Z)%Z).
Axiom min_dist_eps_length : forall (w:(list char)), (min_dist (Nil :(list
char)) w (length w)).
Axiom min_dist_eps_length : forall (w:(list char)), (min_dist nil w
(list.Length.length w)).
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
......@@ -151,91 +99,98 @@ Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
match v with
|</