flag_WP_Flag_WP_parameter_dutch_flag_4.v 7.67 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 5
Require Import BuiltIn.
Require BuiltIn.
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 11
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
12
  | mk_ref : a -> ref a.
Andrei Paskevich's avatar
Andrei Paskevich committed
13 14 15 16 17 18 19 20
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 *)
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 49
(* Why3 assumption *)
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 54 55 56 57 58
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 *)
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 62 63 64
(* Why3 assumption *)
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 68 69
(* Why3 assumption *)
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 72 73
(* Why3 assumption *)
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 79 80 81
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) :=
  (mk_array n (const v:(map Z a))).

(* Why3 assumption *)
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
82 83
  i) = (get a2 i)).

Andrei Paskevich's avatar
Andrei Paskevich committed
84 85 86 87 88
(* Why3 assumption *)
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))).
89

Andrei Paskevich's avatar
Andrei Paskevich committed
90 91 92
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).
93

Andrei Paskevich's avatar
Andrei Paskevich committed
94 95 96
(* Why3 assumption *)
Inductive permut_sub{a:Type} {a_WT:WhyType a}  : (map Z a) -> (map Z a) -> Z
  -> Z -> Prop :=
97 98 99 100 101 102 103 104
  | 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
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
      (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))).

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)).

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)).

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)).

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

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

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

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)))).

Axiom permut_sym1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a))
  (a2:(array a)), (permut a1 a2) -> (permut a2 a1).

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)).

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

(* Why3 assumption *)
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
154 155
  (length a1)).

Andrei Paskevich's avatar
Andrei Paskevich committed
156 157 158
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).
159

Andrei Paskevich's avatar
Andrei Paskevich committed
160 161
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).
162

Andrei Paskevich's avatar
Andrei Paskevich committed
163
(* Why3 assumption *)
164 165 166 167
Inductive color  :=
  | Blue : color 
  | White : color 
  | Red : color .
Andrei Paskevich's avatar
Andrei Paskevich committed
168 169
Axiom color_WhyType : WhyType color.
Existing Instance color_WhyType.
170

Andrei Paskevich's avatar
Andrei Paskevich committed
171
(* Why3 assumption *)
172
Definition monochrome(a:(array color)) (i:Z) (j:Z) (c:color): Prop :=
Andrei Paskevich's avatar
Andrei Paskevich committed
173
  forall (k:Z), ((i <= k)%Z /\ (k < j)%Z) -> ((get1 a k) = c).
174 175 176



Andrei Paskevich's avatar
Andrei Paskevich committed
177 178 179 180 181 182 183 184
(* Why3 goal *)
Theorem WP_parameter_dutch_flag : forall (a:Z) (n:Z), forall (a1:(map Z
  color)), ((0%Z <= n)%Z /\ (a = n)) -> forall (r:Z) (i:Z) (b:Z) (a2:(map Z
  color)), let a3 := (mk_array a a2) in ((((((((((0%Z <= b)%Z /\
  (b <= i)%Z) /\ (i <= r)%Z) /\ (r <= n)%Z) /\ (monochrome a3 0%Z b Blue)) /\
  (monochrome a3 b i White)) /\ (monochrome a3 r n Red)) /\ (a = n)) /\
  (permut_sub a1 a2 0%Z n)) -> ((i < r)%Z -> (((0%Z <= i)%Z /\ (i < a)%Z) ->
  match (get a2
185
  i) with
Andrei Paskevich's avatar
Andrei Paskevich committed
186 187 188 189 190 191
  | Blue => (((0%Z <= b)%Z /\ (b < a)%Z) /\ ((0%Z <= i)%Z /\ (i < a)%Z)) ->
      forall (a4:(map Z color)), (exchange a2 a4 b i) -> forall (b1:Z),
      (b1 = (b + 1%Z)%Z) -> forall (i1:Z), (i1 = (i + 1%Z)%Z) ->
      (monochrome (mk_array a a4) b1 i1 White)
  | White => True
  | Red => True
192 193 194 195 196 197 198 199 200 201
  end))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intuition.
destruct (get a2 i); intuition.
red; intros.
subst b1 i1.
unfold get1; simpl.
assert (case: (k < i \/ k = i)%Z) by omega. destruct case.
replace (get a4 k) with (get a2 k).
Andrei Paskevich's avatar
Andrei Paskevich committed
202
apply H9; omega.
203 204 205 206
destruct H15 as (_,h). destruct h as (_,h).
apply h; omega.
subst k.
destruct H15 as (h,_). rewrite <- h.
Andrei Paskevich's avatar
Andrei Paskevich committed
207
apply H9; omega.
208 209 210
Qed.