Commit a734c3c8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remose some obsolete Coq proofs.

parent cfbcceb9
(* 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.
Require list.List.
Require list.Length.
Require list.Mem.
Require map.Map.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.
(* Why3 assumption *)
Definition word := (list char).
(* Why3 assumption *)
Inductive dist: (list char) -> (list char) -> Z -> Prop :=
| dist_eps : (dist Init.Datatypes.nil Init.Datatypes.nil 0%Z)
| dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist (Init.Datatypes.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 (Init.Datatypes.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 (Init.Datatypes.cons a w1)
(Init.Datatypes.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 last_char (a:char) (u:(list char)) {struct u}: char :=
match u with
| Init.Datatypes.nil => a
| (Init.Datatypes.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
| Init.Datatypes.nil => Init.Datatypes.nil
| (Init.Datatypes.cons c u') => (Init.Datatypes.cons a (but_last c u'))
end.
Axiom first_last_explicit : forall (u:(list char)) (a:char),
((Init.Datatypes.app (but_last a u) (Init.Datatypes.cons (last_char a
u) Init.Datatypes.nil)) = (Init.Datatypes.cons a u)).
Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char),
exists b:char,
((Init.Datatypes.app v (Init.Datatypes.cons b Init.Datatypes.nil)) = (Init.Datatypes.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 = (Init.Datatypes.cons a w2)) -> exists u1:(list char),
exists v1:(list char), exists k:Z, (w1 = (Init.Datatypes.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 (Init.Datatypes.cons a w1) w2 m) -> exists u2:(list char),
exists v2:(list char), exists k:Z, (w2 = (Init.Datatypes.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 (Init.Datatypes.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 (Init.Datatypes.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 (Init.Datatypes.cons a w1)
(Init.Datatypes.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 (Init.Datatypes.cons a w1)
w2 p) -> ((min_dist w1 (Init.Datatypes.cons b w2) m) -> (min_dist
(Init.Datatypes.cons a w1) (Init.Datatypes.cons b w2)
((ZArith.BinInt.Z.min m p) + 1%Z)%Z))).
Axiom min_dist_eps : forall (w:(list char)) (a:char) (n:Z), (min_dist w
Init.Datatypes.nil n) -> (min_dist (Init.Datatypes.cons a w)
Init.Datatypes.nil (n + 1%Z)%Z).
Axiom min_dist_eps_length : forall (w:(list char)), (min_dist
Init.Datatypes.nil w (list.Length.length w)).
(* Why3 assumption *)
Inductive ref (a:Type) :=
| 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]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
(* Why3 assumption *)
Inductive array (a:Type) :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): 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 :=
(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 (length a1) (map.Map.set (elts a1) i v)).
Parameter make: forall {a:Type} {a_WT:WhyType a}, Z -> a -> (array a).
Axiom make_length : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (v:a),
((length (make n v)) = n).
Axiom make_elts : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (i:Z) (v:a),
((get (make n v) i) = v).
Parameter suffix: (array char) -> Z -> (list char).
Axiom suffix_nil : forall (a:(array char)), ((suffix a
(length a)) = Init.Datatypes.nil).
Axiom suffix_cons : forall (a:(array char)) (i:Z), ((0%Z <= i)%Z /\
(i < (length a))%Z) -> ((suffix a i) = (Init.Datatypes.cons (get a
i) (suffix a (i + 1%Z)%Z))).
Axiom suffix_length : forall (a:(array char)) (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).
(* Why3 goal *)
Theorem WP_parameter_distance : forall (w1:Z) (w11:(map.Map.map Z char))
(w2:Z) (w21:(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 -> forall (t:Z) (t1:(map.Map.map Z
Z)), ((0%Z <= t)%Z /\ ((t = o) /\ forall (i:Z), ((map.Map.get t1
i) = 0%Z))) -> ((0%Z <= w2)%Z -> forall (t2:(map.Map.map Z Z)),
(forall (j:Z), ((0%Z <= j)%Z /\ (j < (w2 + 1%Z)%Z)%Z) -> ((map.Map.get t2
j) = (w2 - j)%Z)) -> let o1 := (w1 - 1%Z)%Z in ((0%Z <= o1)%Z ->
forall (t3:(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 t3 j))) ->
(((0%Z <= t)%Z /\ ((0%Z <= w2)%Z /\ (w2 < t)%Z)) -> (((0%Z <= w2)%Z /\
(w2 < t)%Z) -> (((0%Z <= w2)%Z /\ (w2 < t)%Z) -> forall (t4:(map.Map.map Z
Z)), ((0%Z <= t)%Z /\ (t4 = (map.Map.set t3 w2 ((map.Map.get t3
w2) + 1%Z)%Z))) -> let o2 := (w2 - 1%Z)%Z in ((0%Z <= o2)%Z ->
forall (oldt:Z) (t5:(map.Map.map Z Z)), forall (j:Z), ((j <= o2)%Z /\
(0%Z <= j)%Z) -> (((forall (k:Z), ((j < k)%Z /\ (k <= w2)%Z) -> (min_dist
(suffix w12 i) (suffix w22 k) (map.Map.get t5 k))) /\ ((forall (k:Z),
((0%Z <= k)%Z /\ (k <= j)%Z) -> (min_dist (suffix w12 (i + 1%Z)%Z)
(suffix w22 k) (map.Map.get t5 k))) /\ (min_dist (suffix w12 (i + 1%Z)%Z)
(suffix w22 (j + 1%Z)%Z) oldt))) -> (((0%Z <= t)%Z /\ ((0%Z <= j)%Z /\
(j < t)%Z)) -> forall (oldt1:Z), (oldt1 = (map.Map.get t5 j)) ->
(((0%Z <= j)%Z /\ (j < w2)%Z) -> (((0%Z <= i)%Z /\ (i < w1)%Z) ->
((~ ((map.Map.get w11 i) = (map.Map.get w21 j))) -> let o3 :=
(j + 1%Z)%Z in (((0%Z <= o3)%Z /\ (o3 < t)%Z) -> (((0%Z <= j)%Z /\
(j < t)%Z) -> (((0%Z <= j)%Z /\ (j < t)%Z) -> forall (t6:(map.Map.map Z
Z)), ((0%Z <= t)%Z /\ (t6 = (map.Map.set t5 j
((ZArith.BinInt.Z.min (map.Map.get t5 j) (map.Map.get t5
o3)) + 1%Z)%Z))) -> forall (k:Z), (((j - 1%Z)%Z < k)%Z /\ (k <= w2)%Z) ->
(min_dist (suffix w12 i) (suffix w22 k) (map.Map.get t6
k))))))))))))))))))).
intros w1 w11 w2 w21 w22 w12 (h1,h2) o h3 t t1 (h4,(h5,h6)) h7 t2 h8
o1 h9 t3 i (h10,h11) h12 (h13,(h14,h15)) (h16,h17) (h18,h19) t4
(h20,h21) o2 h22 oldt t5 j (h23,h24) (h25,(h26,h27)) (h28,(h29,h30))
oldt1 h31 (h32,h33) (h34,h35) h36 o3 (h37,h38) (h39,h40) (h41,h42) t6
(h43,h44) k (h45,h46).
(*
intros w1 w11 w2 w21 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) o2 h20
oldt t3 j (h21,h22) (h23,(h24,h25)) (h26,(h27,h28)) oldt1 h29
(h30,h31) (h32,h33) h34 o3 (h35,h36) (h37,h38) (h39,h40) t4 (h41,h42)
k (h43,h44).
*)
subst t4 t6 w12 w22 o o1 o2 o3.
unfold min_suffix.
assert (k=j \/ j<k)%Z by omega. intuition.
(* j=k *)
subst j.
rewrite (suffix_cons _ i).
2: unfold length; simpl; omega.
rewrite (suffix_cons _ k).
2: unfold length; simpl; omega.
rewrite Map.Select_eq; try omega.
apply min_dist_diff.
subst; auto.
rewrite <- (suffix_cons _ i).
2: unfold length; simpl; omega.
subst.
apply h25; omega.
rewrite <- (suffix_cons _ k).
subst.
apply h26. omega.
unfold length; simpl; omega.
(* j<k *)
subst.
rewrite Map.Select_neq; try omega.
apply h25. omega.
Qed.
(* 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.
Require list.List.
Require list.Length.
Require list.Mem.
Require map.Map.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.
(* Why3 assumption *)
Definition word := (list char).
(* Why3 assumption *)
Inductive dist: (list char) -> (list char) -> Z -> Prop :=
| dist_eps : (dist Init.Datatypes.nil Init.Datatypes.nil 0%Z)
| dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist (Init.Datatypes.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 (Init.Datatypes.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 (Init.Datatypes.cons a w1)
(Init.Datatypes.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 last_char (a:char) (u:(list char)) {struct u}: char :=
match u with
| Init.Datatypes.nil => a
| (Init.Datatypes.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
| Init.Datatypes.nil => Init.Datatypes.nil
| (Init.Datatypes.cons c u') => (Init.Datatypes.cons a (but_last c u'))
end.
Axiom first_last_explicit : forall (u:(list char)) (a:char),
((Init.Datatypes.app (but_last a u) (Init.Datatypes.cons (last_char a
u) Init.Datatypes.nil)) = (Init.Datatypes.cons a u)).
Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char),
exists b:char,
((Init.Datatypes.app v (Init.Datatypes.cons b Init.Datatypes.nil)) = (Init.Datatypes.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 = (Init.Datatypes.cons a w2)) -> exists u1:(list char),
exists v1:(list char), exists k:Z, (w1 = (Init.Datatypes.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 (Init.Datatypes.cons a w1) w2 m) -> exists u2:(list char),
exists v2:(list char), exists k:Z, (w2 = (Init.Datatypes.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 (Init.Datatypes.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 (Init.Datatypes.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 (Init.Datatypes.cons a w1)
(Init.Datatypes.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 (Init.Datatypes.cons a w1)
w2 p) -> ((min_dist w1 (Init.Datatypes.cons b w2) m) -> (min_dist
(Init.Datatypes.cons a w1) (Init.Datatypes.cons b w2)
((ZArith.BinInt.Z.min m p) + 1%Z)%Z))).
Axiom min_dist_eps : forall (w:(list char)) (a:char) (n:Z), (min_dist w
Init.Datatypes.nil n) -> (min_dist (Init.Datatypes.cons a w)
Init.Datatypes.nil (n + 1%Z)%Z).
Axiom min_dist_eps_length : forall (w:(list char)), (min_dist
Init.Datatypes.nil w (list.Length.length w)).
(* Why3 assumption *)
Inductive ref (a:Type) :=
| 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]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
(* Why3 assumption *)
Inductive array (a:Type) :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): 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 :=
(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 (length a1) (map.Map.set (elts a1) i v)).
Parameter make: forall {a:Type} {a_WT:WhyType a}, Z -> a -> (array a).
Axiom make_length : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (v:a),
((length (make n v)) = n).
Axiom make_elts : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (i:Z) (v:a),
((get (make n v) i) = v).
Parameter suffix: (array char) -> Z -> (list char).
Axiom suffix_nil : forall (a:(array char)), ((suffix a
(length a)) = Init.Datatypes.nil).
Axiom suffix_cons : forall (a:(array char)) (i:Z), ((0%Z <= i)%Z /\
(i < (length a))%Z) -> ((suffix a i) = (Init.Datatypes.cons (get a
i) (suffix a (i + 1%Z)%Z))).
Axiom suffix_length : forall (a:(array char)) (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).
(* Why3 goal *)
Theorem WP_parameter_distance : forall (w1:Z) (w11:(map.Map.map Z char))
(w2:Z) (w21:(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 -> forall (t:Z) (t1:(map.Map.map Z
Z)), ((0%Z <= t)%Z /\ ((t = o) /\ forall (i:Z), ((map.Map.get t1
i) = 0%Z))) -> ((0%Z <= w2)%Z -> forall (t2:(map.Map.map Z Z)),
(forall (j:Z), ((0%Z <= j)%Z /\ (j < (w2 + 1%Z)%Z)%Z) -> ((map.Map.get t2
j) = (w2 - j)%Z)) -> let o1 := (w1 - 1%Z)%Z in ((0%Z <= o1)%Z ->
forall (t3:(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 t3 j))) ->
(((0%Z <= t)%Z /\ ((0%Z <= w2)%Z /\ (w2 < t)%Z)) -> (((0%Z <= w2)%Z /\
(w2 < t)%Z) -> (((0%Z <= w2)%Z /\ (w2 < t)%Z) -> forall (t4:(map.Map.map Z
Z)), ((0%Z <= t)%Z /\ (t4 = (map.Map.set t3 w2 ((map.Map.get t3
w2) + 1%Z)%Z))) -> let o2 := (w2 - 1%Z)%Z in ((0%Z <= o2)%Z ->
forall (oldt:Z) (t5:(map.Map.map Z Z)), forall (j:Z), ((j <= o2)%Z /\
(0%Z <= j)%Z) -> (((forall (k:Z), ((j < k)%Z /\ (k <= w2)%Z) -> (min_dist
(suffix w12 i) (suffix w22 k) (map.Map.get t5 k))) /\ ((forall (k:Z),
((0%Z <= k)%Z /\ (k <= j)%Z) -> (min_dist (suffix w12 (i + 1%Z)%Z)
(suffix w22 k) (map.Map.get t5 k))) /\ (min_dist (suffix w12 (i + 1%Z)%Z)
(suffix w22 (j + 1%Z)%Z) oldt))) -> (((0%Z <= t)%Z /\ ((0%Z <= j)%Z /\
(j < t)%Z)) -> forall (oldt1:Z), (oldt1 = (map.Map.get t5 j)) ->
(((0%Z <= j)%Z /\ (j < w2)%Z) -> (((0%Z <= i)%Z /\ (i < w1)%Z) ->
(((map.Map.get w11 i) = (map.Map.get w21 j)) -> (((0%Z <= j)%Z /\
(j < t)%Z) -> forall (t6:(map.Map.map Z Z)), ((0%Z <= t)%Z /\
(t6 = (map.Map.set t5 j oldt))) -> forall (k:Z), (((j - 1%Z)%Z < k)%Z /\
(k <= w2)%Z) -> (min_dist (suffix w12 i) (suffix w22 k) (map.Map.get t6
k))))))))))))))))).
(* Why3 intros w1 w11 w2 w21 w22 w12 (h1,h2) o h3 t t1 (h4,(h5,h6)) h7 t2 h8
o1 h9 t3 i (h10,h11) h12 (h13,(h14,h15)) (h16,h17) (h18,h19) t4
(h20,h21) o2 h22 oldt t5 j (h23,h24) (h25,(h26,h27)) (h28,(h29,h30))
oldt1 h31 (h32,h33) (h34,h35) h36 (h37,h38) t6 (h39,h40) k (h41,h42). *)
Proof.
intuition.
intuition.
assert (j=k \/ j < k)%Z by omega.
intuition.
(* j=k *)
subst j.
rewrite (suffix_cons _ i).
2: unfold length; simpl; omega.
rewrite (suffix_cons _ k).
2: unfold length; simpl; omega.
subst.
unfold get; simpl.
replace (Map.get w11 i) with (Map.get w21 k).
apply min_dist_equal.
rewrite Map.Select_eq; auto.
(* j<k *)
subst.
rewrite Map.Select_neq; try omega.
apply H15.
omega.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
Require list.NumOcc.
Require list.Permut.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive t (a:Type) :=
| mk_t : (list a) -> t a.
Axiom t_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (t a).
Existing Instance t_WhyType.
Implicit Arguments mk_t [[a]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(t a)): (list a) :=
match v with
| (mk_t x) => x
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (q:(t a)): Z :=
(list.Length.length (elts q)).
Axiom elt : Type.
Parameter elt_WhyType : WhyType elt.
Existing Instance elt_WhyType.
Parameter le: elt -> elt -> Prop.
Axiom total_preorder1 : forall (x:elt) (y:elt), (le x y) \/ (le y x).
Axiom total_preorder2 : forall (x:elt) (y:elt) (z:elt), (le x y) -> ((le y
z) -> (le x z)).
(* Why3 assumption *)
Inductive sorted: (list elt) -> Prop :=
| Sorted_Nil : (sorted Init.Datatypes.nil)
| Sorted_One : forall (x:elt), (sorted
(Init.Datatypes.cons x Init.Datatypes.nil))
| Sorted_Two : forall (x:elt) (y:elt) (l:(list elt)), (le x y) -> ((sorted
(Init.Datatypes.cons y l)) -> (sorted
(Init.Datatypes.cons x (Init.Datatypes.cons y l)))).
Axiom sorted_mem : forall (x:elt) (l:(list elt)), ((forall (y:elt),
(list.Mem.mem y l) -> (le x y)) /\ (sorted l)) <-> (sorted
(Init.Datatypes.cons x l)).
Import Permut.
(* Why3 goal *)
Theorem WP_parameter_merge : forall (q1:(list elt)) (q2:(list elt))
(q:(list elt)), (q = Init.Datatypes.nil) -> forall (q3:(list elt))
(q21:(list elt)) (q11:(list elt)), (list.Permut.permut
(Init.Datatypes.app (Init.Datatypes.app q3 q11) q21)
(Init.Datatypes.app q1 q2)) -> ((0%Z < (list.Length.length q11))%Z ->
((~ ((list.Length.length q11) = 0%Z)) ->
((~ ((list.Length.length q21) = 0%Z)) -> ((~ (q11 = Init.Datatypes.nil)) ->
forall (x1:elt),
match q11 with
| Init.Datatypes.nil => False
| (Init.Datatypes.cons x _) => (x1 = x)
end -> ((~ (q21 = Init.Datatypes.nil)) -> forall (x2:elt),
match q21 with
| Init.Datatypes.nil => False
| (Init.Datatypes.cons x _) => (x2 = x)
end -> ((~ (le x1 x2)) -> ((~ (q21 = Init.Datatypes.nil)) ->
forall (q22:(list elt)), forall (o:elt),
match q21 with
| Init.Datatypes.nil => False
| (Init.Datatypes.cons x t1) => (o = x) /\ (q22 = t1)
end -> forall (q4:(list elt)),
(q4 = (Init.Datatypes.app q3 (Init.Datatypes.cons o Init.Datatypes.nil))) ->
(list.Permut.permut (Init.Datatypes.app (Init.Datatypes.app q4 q11) q22)
(Init.Datatypes.app q1 q2))))))))).
(* Why3 intros q1 q2 q h1 q3 q21 q11 h2 h3 h4 h5 h6 x1 h7 h8 x2 h9 h10 h11
q22 o h12 q4 h13. *)
Proof.
intros q q2 q1 h1 q3 q21 q11 h2 h3 h4 h5 h6 x1 h7 x2 h8 h9 q22 o h10
q4 h11.
destruct q21.
elim h9.
intuition; subst.
apply Permut_trans with (app (app q3 q11) (cons e q21)); auto.
repeat rewrite <- Append.Append_assoc.
eapply Permut_append; auto.
apply Permut_refl.
simpl.
apply (Permut_cons_append e).
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Nth.
Require option.Option.
Require