insertion_sort_WP_InsertionSort_WP_parameter_insertion_sort_1.v 7.96 KB
Newer Older
1 2
(* This file is generated by Why3's Coq driver *)
(* 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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
10
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
11
Inductive ref (a:Type) {a_WT:WhyType a} :=
12
  | mk_ref : a -> ref a.
Andrei Paskevich's avatar
Andrei Paskevich committed
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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
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

Andrei Paskevich's avatar
Andrei Paskevich committed
28 29
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  (map a b) -> a -> b.
30

Andrei Paskevich's avatar
Andrei Paskevich committed
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

Andrei Paskevich's avatar
Andrei Paskevich committed
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

Andrei Paskevich's avatar
Andrei Paskevich committed
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

Andrei Paskevich's avatar
Andrei Paskevich committed
42 43
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  b -> (map a b).
44

Andrei Paskevich's avatar
Andrei Paskevich committed
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

Andrei Paskevich's avatar
Andrei Paskevich committed
48
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
49
Inductive array (a:Type) {a_WT:WhyType a} :=
50
  | mk_array : Z -> (map Z a) -> array a.
Andrei Paskevich's avatar
Andrei Paskevich committed
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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
67
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
68 69
Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a :=
  (get (elts a1) i).
70

Andrei Paskevich's avatar
Andrei Paskevich committed
71
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
72 73 74 75 76 77
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)).

(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) :=
  (mk_array n (const v:(map Z a))).
78

Andrei Paskevich's avatar
Andrei Paskevich committed
79
(* Why3 assumption *)
80
Definition sorted_sub(a:(map Z Z)) (l:Z) (u:Z): Prop := forall (i1:Z) (i2:Z),
Andrei Paskevich's avatar
Andrei Paskevich committed
81
  (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> ((get a i1) <= (get a
82 83
  i2))%Z.

Andrei Paskevich's avatar
Andrei Paskevich committed
84
(* Why3 assumption *)
85 86 87
Definition sorted_sub1(a:(array Z)) (l:Z) (u:Z): Prop := (sorted_sub (elts a)
  l u).

Andrei Paskevich's avatar
Andrei Paskevich committed
88
(* Why3 assumption *)
89 90
Definition sorted(a:(array Z)): Prop := (sorted_sub (elts a) 0%Z (length a)).

Andrei Paskevich's avatar
Andrei Paskevich committed
91
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
92 93
Definition map_eq_sub {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a))
  (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1
94 95
  i) = (get a2 i)).

Andrei Paskevich's avatar
Andrei Paskevich committed
96
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
97 98 99 100
Definition exchange {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a))
  (i:Z) (j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1
  j)) /\ forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2
  k))).
101

Andrei Paskevich's avatar
Andrei Paskevich committed
102 103 104
Axiom exchange_set : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a)),
  forall (i:Z) (j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i
  j).
105

Andrei Paskevich's avatar
Andrei Paskevich committed
106
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
107 108
Inductive permut_sub{a:Type} {a_WT:WhyType a}  : (map Z a) -> (map Z a) -> Z
  -> Z -> Prop :=
109 110 111 112 113 114 115 116
  | permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
      (map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u)
  | permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
      (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u)
  | permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)),
      forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l
      u) -> (permut_sub a1 a3 l u))
  | permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z)
Andrei Paskevich's avatar
Andrei Paskevich committed
117 118
      (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\
      (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))).
119

Andrei Paskevich's avatar
Andrei Paskevich committed
120 121 122 123
Axiom permut_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z
  a)) (a2:(map Z a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\
  (l2 <= r2)%Z) /\ (r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) ->
  (permut_sub a1 a2 l1 r1)).
124

Andrei Paskevich's avatar
Andrei Paskevich committed
125 126 127
Axiom permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a))
  (a2:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z),
  ((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i)).
128

Andrei Paskevich's avatar
Andrei Paskevich committed
129 130 131 132
Axiom permut_exists : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a))
  (a2:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z),
  ((l <= i)%Z /\ (i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\
  ((get a2 i) = (get a1 j)).
133

Andrei Paskevich's avatar
Andrei Paskevich committed
134
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
135 136
Definition exchange1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a))
  (i:Z) (j:Z): Prop := (exchange (elts a1) (elts a2) i j).
137

Andrei Paskevich's avatar
Andrei Paskevich committed
138
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
139 140
Definition permut_sub1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a))
  (l:Z) (u:Z): Prop := (permut_sub (elts a1) (elts a2) l u).
141

Andrei Paskevich's avatar
Andrei Paskevich committed
142
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
143 144 145
Definition permut {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
  a)): Prop := ((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2)
  0%Z (length a1)).
146

Andrei Paskevich's avatar
Andrei Paskevich committed
147 148 149 150
Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array
  a)) (a2:(array a)) (i:Z) (j:Z), (exchange1 a1 a2 i j) ->
  (((length a1) = (length a2)) -> (((0%Z <= i)%Z /\ (i < (length a1))%Z) ->
  (((0%Z <= j)%Z /\ (j < (length a1))%Z) -> (permut a1 a2)))).
151

Andrei Paskevich's avatar
Andrei Paskevich committed
152 153
Axiom permut_sym1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
  (a2:(array a)), (permut a1 a2) -> (permut a2 a1).
154

Andrei Paskevich's avatar
Andrei Paskevich committed
155 156 157
Axiom permut_trans1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
  (a2:(array a)) (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) ->
  (permut a1 a3)).
158

Andrei Paskevich's avatar
Andrei Paskevich committed
159
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
160 161
Definition array_eq_sub {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
  a)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u).
162

Andrei Paskevich's avatar
Andrei Paskevich committed
163
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
164 165 166
Definition array_eq {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array
  a)): Prop := ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z
  (length a1)).
167

Andrei Paskevich's avatar
Andrei Paskevich committed
168 169 170
Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a},
  forall (a1:(array a)) (a2:(array a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l
  u) -> (permut_sub1 a1 a2 l u).
171

Andrei Paskevich's avatar
Andrei Paskevich committed
172 173
Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array
  a)) (a2:(array a)), (array_eq a1 a2) -> (permut a1 a2).
174

Andrei Paskevich's avatar
Andrei Paskevich committed
175
(* Why3 goal *)
176 177
Theorem WP_parameter_insertion_sort : forall (a:Z), forall (a1:(map Z Z)),
  let a2 := (mk_array a a1) in ((1%Z <= (a - 1%Z)%Z)%Z -> forall (a3:(map Z
178
  Z)), forall (i:Z), ((1%Z <= i)%Z /\ (i <= (a - 1%Z)%Z)%Z) ->
179
  (((sorted_sub a3 0%Z i) /\ (permut a2 (mk_array a a3))) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
180 181 182 183 184 185 186 187 188 189 190 191
  (((0%Z <= i)%Z /\ (i < a)%Z) -> let v := (get a3 i) in forall (j:Z)
  (a4:(map Z Z)), (((((0%Z <= j)%Z /\ (j <= i)%Z) /\ (permut a2 (mk_array a
  (set a4 j v)))) /\ forall (k1:Z) (k2:Z), (((0%Z <= k1)%Z /\
  (k1 <= k2)%Z) /\ (k2 <= i)%Z) -> ((~ (k1 = j)) -> ((~ (k2 = j)) -> ((get a4
  k1) <= (get a4 k2))%Z))) /\ forall (k:Z), (((j + 1%Z)%Z <= k)%Z /\
  (k <= i)%Z) -> (v < (get a4 k))%Z) -> ((0%Z < j)%Z ->
  (((0%Z <= (j - 1%Z)%Z)%Z /\ ((j - 1%Z)%Z < a)%Z) -> ((v < (get a4
  (j - 1%Z)%Z))%Z -> (((0%Z <= (j - 1%Z)%Z)%Z /\ ((j - 1%Z)%Z < a)%Z) ->
  (((0%Z <= j)%Z /\ (j < a)%Z) -> forall (a5:(map Z Z)), (a5 = (set a4 j
  (get a4 (j - 1%Z)%Z))) -> ((exchange (set a4 j v) (set a5 (j - 1%Z)%Z v)
  (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut a2
  (mk_array a (set a5 j1 v)))))))))))).
192 193 194 195 196 197
intuition.
intuition.
unfold permut.
split.
simpl.
auto.
Andrei Paskevich's avatar
Andrei Paskevich committed
198
subst a5.
199 200
simpl.
apply permut_trans with (elts (set1 (mk_array a a4) j (get a3 i))); auto.
201
subst j1.
Andrei Paskevich's avatar
Andrei Paskevich committed
202
unfold permut in H18.
203
intuition.
204 205 206
apply permut_exchange with (j-1)%Z j.
simpl; omega.
simpl; omega.
207
subst j1; assumption.
208 209 210
Qed.