insertion_sort_WP_InsertionSort_WP_parameter_insertion_sort_1.v 8.04 KB
Newer Older
1
(* This file is generated by Why3's Coq 8.4 driver *)
2
(* Beware! Only edit allowed sections below    *)
Andrei Paskevich's avatar
Andrei Paskevich committed
3 4
Require Import BuiltIn.
Require BuiltIn.
Andrei Paskevich's avatar
Andrei Paskevich committed
5
Require int.Int.
6
Require map.Map.
7
Require map.MapPermut.
8

Andrei Paskevich's avatar
Andrei Paskevich committed
9
(* Why3 assumption *)
10
Definition unit := unit.
11

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

Andrei Paskevich's avatar
Andrei Paskevich committed
19
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
20
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
Andrei Paskevich's avatar
Andrei Paskevich committed
21 22
  match v with
  | (mk_ref x) => x
23 24
  end.

Andrei Paskevich's avatar
Andrei Paskevich committed
25
(* Why3 assumption *)
26 27
Inductive array
  (a:Type) {a_WT:WhyType a} :=
Andrei Paskevich's avatar
Andrei Paskevich committed
28
  | mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Andrei Paskevich's avatar
Andrei Paskevich committed
29 30 31
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
32

Andrei Paskevich's avatar
Andrei Paskevich committed
33
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
34 35
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
  Z _ a a_WT) := match v with
Andrei Paskevich's avatar
Andrei Paskevich committed
36
  | (mk_array x x1) => x1
37 38
  end.

Andrei Paskevich's avatar
Andrei Paskevich committed
39
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
40
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
Andrei Paskevich's avatar
Andrei Paskevich committed
41 42
  match v with
  | (mk_array x x1) => x
43 44
  end.

Andrei Paskevich's avatar
Andrei Paskevich committed
45
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
46
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
47
  (map.Map.get (elts a1) i).
48

Andrei Paskevich's avatar
Andrei Paskevich committed
49
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
50 51 52
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)).
Andrei Paskevich's avatar
Andrei Paskevich committed
53 54

(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
55 56
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))).
57

Andrei Paskevich's avatar
Andrei Paskevich committed
58
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
59 60
Definition sorted_sub (a:(@map.Map.map Z _ Z _)) (l:Z) (u:Z): Prop :=
  forall (i1:Z) (i2:Z), ((l <= i1)%Z /\ ((i1 <= i2)%Z /\ (i2 < u)%Z)) ->
61
  ((map.Map.get a i1) <= (map.Map.get a i2))%Z.
62

Andrei Paskevich's avatar
Andrei Paskevich committed
63
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
64
Definition sorted_sub1 (a:(@array Z _)) (l:Z) (u:Z): Prop := (sorted_sub
65
  (elts a) l u).
66

Andrei Paskevich's avatar
Andrei Paskevich committed
67
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
68
Definition sorted (a:(@array Z _)): Prop := (sorted_sub (elts a) 0%Z
69
  (length a)).
70

71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86
(* Why3 assumption *)
Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _
  a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z): Prop := forall (i:Z),
  ((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)).

(* Why3 assumption *)
Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
  (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\
  (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\
  (u <= (length a1))%Z) /\ (map_eq_sub (elts a1) (elts a2) l u))).

(* Why3 assumption *)
Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
  (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map_eq_sub
  (elts a1) (elts a2) 0%Z (length a1)).

Andrei Paskevich's avatar
Andrei Paskevich committed
87
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
88
Definition exchange {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
89
  (a2:(@array a a_WT)) (i:Z) (j:Z): Prop := ((length a1) = (length a2)) /\
90
  (map.MapPermut.exchange (elts a1) (elts a2) 0%Z (length a1) i j).
91 92

(* Why3 assumption *)
93 94
Definition permut {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array
  a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\
95
  (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\
96
  (u <= (length a1))%Z) /\ (map.MapPermut.permut (elts a1) (elts a2) l u))).
97

Andrei Paskevich's avatar
Andrei Paskevich committed
98
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
99
Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
100 101 102
  (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2)
  0%Z l) /\ ((permut a1 a2 l u) /\ (map_eq_sub (elts a1) (elts a2) u
  (length a1))).
103

Andrei Paskevich's avatar
Andrei Paskevich committed
104
(* Why3 assumption *)
105 106 107
Definition permut_all {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
  (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\
  (map.MapPermut.permut (elts a1) (elts a2) 0%Z (length a1)).
108

109 110 111
Axiom permut_sub_refl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
  a a_WT)) (l:Z) (u:Z), ((0%Z <= l)%Z /\ ((l <= u)%Z /\
  (u <= (length a1))%Z)) -> (permut_sub a1 a1 l u).
112

113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131
Axiom permut_sub_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
  a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT)) (l:Z) (u:Z), (permut_sub
  a1 a2 l u) -> ((permut_sub a2 a3 l u) -> (permut_sub a1 a3 l u)).

Axiom exchange_permut_sub : forall {a:Type} {a_WT:WhyType a},
  forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z) (l:Z) (u:Z),
  (exchange a1 a2 i j) -> (((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\
  (j < u)%Z) -> ((0%Z <= l)%Z -> ((u <= (length a1))%Z -> (permut_sub a1 a2 l
  u))))).

Axiom permut_sub_unmodified : forall {a:Type} {a_WT:WhyType a},
  forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z), (permut_sub
  a1 a2 l u) -> forall (i:Z), (((0%Z <= i)%Z /\ (i < l)%Z) \/ ((u <= i)%Z /\
  (i < (length a1))%Z)) -> ((get a2 i) = (get a1 i)).

Axiom permut_sub_weakening : forall {a:Type} {a_WT:WhyType a},
  forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l1:Z) (u1:Z) (l2:Z)
  (u2:Z), (permut_sub a1 a2 l1 u1) -> (((0%Z <= l2)%Z /\ (l2 <= l1)%Z) ->
  (((u1 <= u2)%Z /\ (u2 <= (length a1))%Z) -> (permut_sub a1 a2 l2 u2))).
132

133 134 135 136 137 138 139
Axiom permut_sub_compose : forall {a:Type} {a_WT:WhyType a},
  forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT))
  (l1:Z) (u1:Z) (l2:Z) (u2:Z), (u1 <= l2)%Z -> ((permut_sub a1 a2 l1 u1) ->
  ((permut_sub a2 a3 l2 u2) -> (permut_sub a1 a3 l1 u2))).

Axiom permut_all_refl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
  a a_WT)), (permut_all a1 a1).
140

141 142 143
Axiom permut_all_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
  a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT)), (permut_all a1 a2) ->
  ((permut_all a2 a3) -> (permut_all a1 a3)).
144

145 146 147 148
Axiom exchange_permut_all : forall {a:Type} {a_WT:WhyType a},
  forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z), (exchange a1
  a2 i j) -> (permut_all a1 a2).

149 150 151
Axiom array_eq_permut_all : forall {a:Type} {a_WT:WhyType a},
  forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (array_eq a1 a2) ->
  (permut_all a1 a2).
152

153
Axiom permut_sub_permut_all : forall {a:Type} {a_WT:WhyType a},
154
  forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z), (permut_sub
155
  a1 a2 l u) -> (permut_all a1 a2).
156

Andrei Paskevich's avatar
Andrei Paskevich committed
157
(* Why3 goal *)
Andrei Paskevich's avatar
Andrei Paskevich committed
158 159 160 161
Theorem WP_parameter_insertion_sort : forall (a:Z) (a1:(@map.Map.map Z _
  Z _)), let a2 := (mk_array a a1) in ((0%Z <= a)%Z -> let o :=
  (a - 1%Z)%Z in ((1%Z <= o)%Z -> forall (a3:(@map.Map.map Z _ Z _)),
  forall (i:Z), ((1%Z <= i)%Z /\ (i <= o)%Z) -> (((sorted_sub a3 0%Z i) /\
162
  (permut_all a2 (mk_array a a3))) -> (((0%Z <= a)%Z /\ ((0%Z <= i)%Z /\
Andrei Paskevich's avatar
Andrei Paskevich committed
163
  (i < a)%Z)) -> let v := (map.Map.get a3 i) in forall (j:Z)
164 165
  (a4:(@map.Map.map Z _ Z _)), (((0%Z <= j)%Z /\ (j <= i)%Z) /\ ((permut_all
  a2 (mk_array a (map.Map.set a4 j v))) /\ ((forall (k1:Z) (k2:Z),
Andrei Paskevich's avatar
Andrei Paskevich committed
166 167 168 169 170 171 172
  ((0%Z <= k1)%Z /\ ((k1 <= k2)%Z /\ (k2 <= i)%Z)) -> ((~ (k1 = j)) ->
  ((~ (k2 = j)) -> ((map.Map.get a4 k1) <= (map.Map.get a4 k2))%Z))) /\
  forall (k:Z), (((j + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (v < (map.Map.get a4
  k))%Z))) -> ((0%Z < j)%Z -> let o1 := (j - 1%Z)%Z in (((0%Z <= a)%Z /\
  ((0%Z <= o1)%Z /\ (o1 < a)%Z)) -> ((v < (map.Map.get a4 o1))%Z -> let o2 :=
  (j - 1%Z)%Z in (((0%Z <= o2)%Z /\ (o2 < a)%Z) -> (((0%Z <= j)%Z /\
  (j < a)%Z) -> forall (a5:(@map.Map.map Z _ Z _)), ((0%Z <= a)%Z /\
173 174
  (a5 = (map.Map.set a4 j (map.Map.get a4 o2)))) -> ((exchange (mk_array a
  (map.Map.set a4 j v)) (mk_array a (map.Map.set a5 (j - 1%Z)%Z v))
175
  (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut_all a2
176 177 178 179
  (mk_array a (map.Map.set a5 j1 v))))))))))))).
(* Why3 intros a a1 a2 h1 o h2 a3 i (h3,h4) (h5,h6) (h7,(h8,h9)) v j a4
        ((h10,h11),(h12,(h13,h14))) h15 o1 (h16,(h17,h18)) h19 o2 (h20,h21)
        (h22,h23) a5 (h24,h25) h26 j1 h27. *)
Andrei Paskevich's avatar
Andrei Paskevich committed
180 181 182
intros a a1 a2 h1 o h2 a3 i (h3,h4) (h5,h6) (h7,(h8,h9)) v j a4
        ((h10,h11),(h12,(h13,h14))) h15 o1 (h16,(h17,h18)) h19 o2 (h20,h21)
        (h22,h23) a5 (h24,h25) h26 j1 h27.
183
intuition.
184
unfold permut_all.
185 186 187
split.
simpl.
auto.
Andrei Paskevich's avatar
Andrei Paskevich committed
188
subst a5.
189
simpl.
190
apply MapPermut.permut_trans with (elts (set (mk_array a a4) j (Map.get a3 i))); auto.
191
subst j1.
192
unfold permut_all in h12.
193
intuition.
194 195
generalize (exchange_permut_all _ _ _ _ h26).
unfold permut_all; simpl; intuition.
196
subst j1; assumption.
197 198
Qed.