foveoos11_challenge3_WP_TwoEqualElements_WP_parameter_two_equal_elements_3.v 4.86 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
Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
Andrei Paskevich's avatar
Andrei Paskevich committed
19 20
  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
Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map Z a) :=
Andrei Paskevich's avatar
Andrei Paskevich committed
57 58
  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
Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): Z :=
Andrei Paskevich's avatar
Andrei Paskevich committed
63 64
  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 appear_twice(a:(array Z)) (v:Z) (u:Z): Prop := exists i:Z,
Andrei Paskevich's avatar
Andrei Paskevich committed
81 82
  ((0%Z <= i)%Z /\ (i < u)%Z) /\ (((get1 a i) = v) /\ exists j:Z,
  ((0%Z <= j)%Z /\ (j < u)%Z) /\ ((~ (j = i)) /\ ((get1 a j) = v))).
83 84


Andrei Paskevich's avatar
Andrei Paskevich committed
85 86
(* Why3 goal *)
Theorem WP_parameter_two_equal_elements : forall (a:Z) (n:Z), forall (a1:(map
Andrei Paskevich's avatar
Andrei Paskevich committed
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107
  Z Z)), let a2 := (mk_array a a1) in (((((a = (n + 2%Z)%Z) /\
  (2%Z <= n)%Z) /\ forall (i:Z), ((0%Z <= i)%Z /\ (i < a)%Z) ->
  ((0%Z <= (get a1 i))%Z /\ ((get a1 i) < n)%Z)) /\ exists v1:Z,
  (appear_twice a2 v1 (n + 2%Z)%Z) /\ exists v2:Z, (appear_twice a2 v2
  (n + 2%Z)%Z) /\ ~ (v2 = v1)) -> ((0%Z <= n)%Z -> ((0%Z <= (n + 1%Z)%Z)%Z ->
  forall (v2:Z) (v1:Z) (deja_vu:(map Z bool)), forall (i:Z), ((0%Z <= i)%Z /\
  (i <= (n + 1%Z)%Z)%Z) -> ((((((((v1 = (-1%Z)%Z) -> (v2 = (-1%Z)%Z)) /\
  ((~ (v1 = (-1%Z)%Z)) -> (appear_twice a2 v1 i))) /\ ((~ (v2 = (-1%Z)%Z)) ->
  ((appear_twice a2 v2 i) /\ ~ (v2 = v1)))) /\ forall (v:Z), ((0%Z <= v)%Z /\
  (v < n)%Z) -> ((((get deja_vu v) = true) /\ exists j:Z, ((0%Z <= j)%Z /\
  (j < i)%Z) /\ ((get a1 j) = v)) \/ ((~ ((get deja_vu v) = true)) /\
  forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((get a1 j) = v)))) /\
  ((v1 = (-1%Z)%Z) -> forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) ->
  ~ (appear_twice a2 v i))) /\ ((v2 = (-1%Z)%Z) -> forall (v:Z),
  ((0%Z <= v)%Z /\ (v < n)%Z) -> ((~ (v = v1)) -> ~ (appear_twice a2 v
  i)))) -> (((0%Z <= i)%Z /\ (i < a)%Z) -> let v := (get a1 i) in
  (((0%Z <= v)%Z /\ (v < n)%Z) -> ((~ ((get deja_vu v) = true)) ->
  (((0%Z <= v)%Z /\ (v < n)%Z) -> forall (deja_vu1:(map Z bool)),
  (deja_vu1 = (set deja_vu v true)) -> ((v1 = (-1%Z)%Z) -> forall (v3:Z),
  ((0%Z <= v3)%Z /\ (v3 < n)%Z) -> ~ (appear_twice a2 v3
  (i + 1%Z)%Z)))))))))).
108 109 110
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intuition.
Andrei Paskevich's avatar
Andrei Paskevich committed
111
destruct (H18 (get a1 i)); intuition.
112 113
red in H23.
destruct H23 as (i0, (h0, (h1, (j, (h2, (h3, h4)))))).
Andrei Paskevich's avatar
Andrei Paskevich committed
114
assert (v3 <> get a1 i).
115 116 117
assert (case: (i0 < i \/ j < i)%Z) by omega. destruct case.
red; intro; apply (H27 i0). omega. unfold get1 in h1; simpl in h1. omega.
red; intro; apply (H27 j). omega. unfold get1 in h4; simpl in h4. omega.
Andrei Paskevich's avatar
Andrei Paskevich committed
118
apply (H22 v3); auto.
119 120 121 122 123 124 125 126 127 128 129 130 131 132 133
red; exists i0; intuition.
assert (case: (i0 < i \/ i0 = i)%Z) by omega. destruct case.
auto.
subst i0.
unfold get1 in h1; simpl in h1.
omega.
exists j; intuition.
assert (case: (j < i \/ j = i)%Z) by omega. destruct case.
auto.
subst j.
unfold get1 in h4; simpl in h4.
omega.
Qed.