distance_Distance_WP_parameter_distance_1.v 4.9 KB
Newer Older
1 2
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
3 4
Require Import BuiltIn.
Require BuiltIn.
5 6 7 8 9 10
Require int.Int.

(* Why3 assumption *)
Definition unit  := unit.

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

(* Why3 assumption *)
18
Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
19 20 21 22
  match v with
  | (mk_ref x) => x
  end.

23 24 25 26
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
  (b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
27

28 29
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  (map a b) -> a -> b.
30

31 32
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  (map a b) -> a -> b -> (map a b).
33

34 35 36
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
  ((get (set m a1 b1) a2) = b1).
37

38 39 40
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
  {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
  forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
41

42 43
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  b -> (map a b).
44

45 46
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
47 48

(* Why3 assumption *)
49
Inductive array (a:Type) {a_WT:WhyType a} :=
50
  | mk_array : Z -> (map Z a) -> array a.
51 52 53
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
54 55

(* Why3 assumption *)
56
Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map Z a) :=
57 58 59 60 61
  match v with
  | (mk_array x x1) => x1
  end.

(* Why3 assumption *)
62
Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): Z :=
63 64 65 66 67
  match v with
  | (mk_array x x1) => x
  end.

(* Why3 assumption *)
68 69
Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a :=
  (get (elts a1) i).
70 71

(* Why3 assumption *)
72 73
Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array
  a) := (mk_array (length a1) (set (elts a1) i v)).
74

Andrei Paskevich's avatar
Andrei Paskevich committed
75 76 77 78
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) :=
  (mk_array n (const v:(map Z a))).

79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
Parameter n: Z.

Axiom n_nonneg : (0%Z < n)%Z.

Parameter f: Z -> Z.

Axiom f_prop : forall (k:Z), ((0%Z < k)%Z /\ (k < n)%Z) ->
  ((0%Z <= (f k))%Z /\ ((f k) < k)%Z).

(* Why3 assumption *)
Inductive path : Z -> Z -> Prop :=
  | path0 : (path 0%Z 0%Z)
  | paths : forall (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> forall (d:Z) (j:Z),
      (path d j) -> ((((f i) <= j)%Z /\ (j < i)%Z) -> (path (d + 1%Z)%Z i)).

(* Why3 assumption *)
Definition distance(d:Z) (i:Z): Prop := (path d i) /\ forall (d':Z), (path d'
  i) -> (d <= d')%Z.

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

(* Why3 goal *)
Theorem WP_parameter_distance : (0%Z <= n)%Z -> ((((0%Z < 0%Z)%Z \/
  (0%Z = 0%Z)) /\ (0%Z < n)%Z) -> forall (g:(map Z Z)),
  (g = (set (const 0%Z:(map Z Z)) 0%Z (-1%Z)%Z)) -> ((0%Z <= n)%Z ->
  (((1%Z < (n - 1%Z)%Z)%Z \/ (1%Z = (n - 1%Z)%Z)) -> forall (count:Z) (d:(map
Andrei Paskevich's avatar
Andrei Paskevich committed
106 107
  Z Z)) (g1:(map Z Z)), (((((get d 0%Z) = 0%Z) /\ (((get g1
  0%Z) = (-1%Z)%Z) /\ (((count + (get d
108 109
  (((n - 1%Z)%Z + 1%Z)%Z - 1%Z)%Z))%Z < (((n - 1%Z)%Z + 1%Z)%Z - 1%Z)%Z)%Z \/
  ((count + (get d
Andrei Paskevich's avatar
Andrei Paskevich committed
110 111 112 113 114 115 116 117 118 119 120
  (((n - 1%Z)%Z + 1%Z)%Z - 1%Z)%Z))%Z = (((n - 1%Z)%Z + 1%Z)%Z - 1%Z)%Z)))) /\
  forall (k:Z), ((0%Z < k)%Z /\ (k < ((n - 1%Z)%Z + 1%Z)%Z)%Z) -> (((((get g1
  (get g1 k)) < (f k))%Z /\ (((f k) < (get g1 k))%Z \/ ((f k) = (get g1
  k)))) /\ ((get g1 k) < k)%Z) /\ (((0%Z < (get d k))%Z /\ ((get d
  k) = ((get d (get g1 k)) + 1%Z)%Z)) /\ forall (k':Z), (((get g1
  k) < k')%Z /\ (k' < k)%Z) -> ((get d (get g1 k)) < (get d k'))%Z))) /\
  forall (k:Z), (((0%Z < k)%Z \/ (0%Z = k)) /\
  (k < ((n - 1%Z)%Z + 1%Z)%Z)%Z) -> (path (get d k) k)) -> ((count < n)%Z ->
  forall (k:Z), (((0%Z < k)%Z \/ (0%Z = k)) /\ (k < n)%Z) -> forall (d':Z),
  (path d' k) -> ((get d k) <= d')%Z)))).
intros h1 (h2,h3) g h4 h5 h6 count d g1 (((h7,(h8,h9)),h10),h11) h12 k
121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141
(h13,h14) d' h15.
clear h1 h2.
clear h5 h6.
replace (n-1+1)%Z with n in * by omega.
clear count h9 h12.
generalize h13 h14 d' h15.
pattern k.
apply Z_lt_induction; [clear k h13 h14 d' h15 | omega].
intros k IH hk1 hk2 d' hd'.
assert (case: (get d k <= d' \/ d' < get d k)%Z) by omega.
destruct case; auto.
destruct hk1.
(* 0 < k *)
inversion hd'.
omega.
subst i.
assert (h: (0 < k < n)%Z) by omega.
generalize (h10 k h). intros h10k.
assert (case: (j < get g1 k \/ j = get g1 k \/ j > get g1 k)%Z) by omega.
destruct case.
(* j < g[k] *)
142
why3 "z3" timelimit 5.
143 144 145 146
destruct H5.
(* j = g[k] *)
ae.
(* j > g[k] *)
147
why3 "z3" timelimit 3.
148 149 150 151 152
(* k = 0 *)
ae.
Qed.