edit_distance_EditDistance_WP_parameter_distance_1.v 7.01 KB
Newer Older
1 2 3 4 5 6
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
7 8 9
Require list.List.
Require list.Length.
Require list.Mem.
Andrei Paskevich's avatar
Andrei Paskevich committed
10
Require map.Map.
11
Require list.Append.
12 13

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
14
Definition unit := unit.
15 16 17 18 19 20

Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
21
Definition word := (list char).
22 23 24

(* Why3 assumption *)
Inductive dist : (list char) -> (list char) -> Z -> Prop :=
25
  | dist_eps : (dist nil nil 0%Z)
26
  | dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
27
      w2 n) -> forall (a:char), (dist (cons a w1) w2 (n + 1%Z)%Z)
28
  | dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
29
      w2 n) -> forall (a:char), (dist w1 (cons a w2) (n + 1%Z)%Z)
30
  | dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
31
      w2 n) -> forall (a:char), (dist (cons a w1) (cons a w2) n).
32 33

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
34
Definition min_dist (w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
35 36 37
  w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z.

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
38
Fixpoint last_char (a:char) (u:(list char)) {struct u}: char :=
39
  match u with
40 41
  | nil => a
  | (cons c u') => (last_char c u')
42 43 44
  end.

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
45
Fixpoint but_last (a:char) (u:(list char)) {struct u}: (list char) :=
46
  match u with
47 48
  | nil => nil
  | (cons c u') => (cons a (but_last c u'))
49 50 51
  end.

Axiom first_last_explicit : forall (u:(list char)) (a:char),
52
  ((List.app (but_last a u) (cons (last_char a u) nil)) = (cons a u)).
53 54

Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char),
55 56
  exists b:char, ((List.app v (cons b nil)) = (cons a u)) /\
  ((list.Length.length v) = (list.Length.length u)).
57 58

Axiom key_lemma_right : forall (w1:(list char)) (w'2:(list char)) (m:Z)
59 60 61 62
  (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).
63 64 65 66 67

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)
68 69 70
  (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).
71

72 73 74
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).
75

76 77 78
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).
79 80

Axiom min_dist_equal : forall (w1:(list char)) (w2:(list char)) (a:char)
81
  (n:Z), (min_dist w1 w2 n) -> (min_dist (cons a w1) (cons a w2) n).
82 83

Axiom min_dist_diff : forall (w1:(list char)) (w2:(list char)) (a:char)
84 85
  (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)
86 87
  ((Zmin m p) + 1%Z)%Z))).

88 89
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).
90

91 92
Axiom min_dist_eps_length : forall (w:(list char)), (min_dist nil w
  (list.Length.length w)).
93 94 95 96 97 98 99 100 101

(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
  | mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].

(* Why3 assumption *)
102
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
103 104 105 106 107
  match v with
  | (mk_ref x) => x
  end.

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
108 109
Inductive array
  (a:Type) {a_WT:WhyType a} :=
110
  | mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
111 112 113 114 115
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 *)
116 117
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
  Z _ a a_WT) := match v with
118 119 120 121
  | (mk_array x x1) => x1
  end.

(* Why3 assumption *)
122
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
123 124 125 126 127
  match v with
  | (mk_array x x1) => x
  end.

(* Why3 assumption *)
128
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
Andrei Paskevich's avatar
Andrei Paskevich committed
129
  (map.Map.get (elts a1) i).
130 131

(* Why3 assumption *)
132 133 134
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)).
135 136

(* Why3 assumption *)
137 138
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))).
139

140
Parameter suffix: (@array char char_WhyType) -> Z -> (list char).
141

142 143
Axiom suffix_nil : forall (a:(@array char char_WhyType)), ((suffix a
  (length a)) = nil).
144

145 146 147
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))).
148

149 150 151
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).
152 153

(* Why3 assumption *)
154 155 156
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).
157 158 159 160 161 162

Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
Open Scope Z_scope.

(* Why3 goal *)
Andrei Paskevich's avatar
Andrei Paskevich committed
163
Theorem WP_parameter_distance : forall (w1:Z) (w2:Z),
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
  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)))))))))))).
Andrei Paskevich's avatar
Andrei Paskevich committed
180 181 182 183
(* 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). *)
intros w1 w2 w21 w11 w22 w12 (h1,h2) o h3 h4 _ t h5 o1 h6 t1 i (h7,h8) h9 (h10,h11)
184
(h12,h13) (h14,h15) t2 h16 h17 j (h18,h19).
Andrei Paskevich's avatar
Andrei Paskevich committed
185
subst o o1.
186 187
replace (i-1+1) with i by omega.
rewrite suffix_cons.
188
assert (h : length w22 = j) by ae.
189 190 191 192 193
ae.
ae.
Qed.