Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

foveoos11_challenge3_WP_TwoEqualElements_WP_parameter_two_equal_elements_4.v 4.7 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
(* This file is generated by Why3's Coq 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

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

MARCHE Claude's avatar
MARCHE Claude committed
11 12 13 14
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.

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

Andrei Paskevich's avatar
Andrei Paskevich committed
22
(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
23
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
Andrei Paskevich's avatar
Andrei Paskevich committed
24 25
  match v with
  | (mk_ref x) => x
26 27
  end.

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
51
(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
52 53
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
  a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
Andrei Paskevich's avatar
Andrei Paskevich committed
54

MARCHE Claude's avatar
MARCHE Claude committed
55 56 57 58 59 60 61
Parameter make: forall {a:Type} {a_WT:WhyType a}, Z -> a -> (array a).

Axiom make_length : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (v:a),
  ((length (make n v)) = n).

Axiom make_elts : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (i:Z) (v:a),
  ((get (make n v) i) = v).
62

Andrei Paskevich's avatar
Andrei Paskevich committed
63
(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
64
Definition appear_twice (a:(array Z)) (v:Z) (u:Z): Prop := exists i:Z,
65 66
  ((0%Z <= i)%Z /\ (i < u)%Z) /\ (((get a i) = v) /\ exists j:Z,
  ((0%Z <= j)%Z /\ (j < u)%Z) /\ ((~ (j = i)) /\ ((get a j) = v))).
Andrei Paskevich's avatar
Andrei Paskevich committed
67 68

(* Why3 goal *)
MARCHE Claude's avatar
MARCHE Claude committed
69 70
Theorem WP_parameter_two_equal_elements : forall (a:Z) (a1:(map.Map.map Z Z))
  (n:Z), let a2 := (mk_array a a1) in (((0%Z <= a)%Z /\
Andrei Paskevich's avatar
Andrei Paskevich committed
71 72 73 74
  (((a = (n + 2%Z)%Z) /\ (2%Z <= n)%Z) /\ ((forall (i:Z), ((0%Z <= i)%Z /\
  (i < a)%Z) -> ((0%Z <= (map.Map.get a1 i))%Z /\ ((map.Map.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)))) ->
MARCHE Claude's avatar
MARCHE Claude committed
75 76 77 78 79 80
  ((0%Z <= n)%Z -> forall (deja_vu:Z) (deja_vu1:(map.Map.map Z bool)),
  ((0%Z <= deja_vu)%Z /\ ((deja_vu = n) /\ forall (i:Z),
  ((map.Map.get deja_vu1 i) = false))) -> let o := (n + 1%Z)%Z in
  ((0%Z <= o)%Z -> forall (v2:Z) (v1:Z) (deja_vu2:(map.Map.map Z bool)),
  forall (i:Z), ((0%Z <= i)%Z /\ (i <= o)%Z) -> ((((v1 = (-1%Z)%Z) ->
  (v2 = (-1%Z)%Z)) /\ (((~ (v1 = (-1%Z)%Z)) -> (appear_twice a2 v1 i)) /\
Andrei Paskevich's avatar
Andrei Paskevich committed
81
  (((~ (v2 = (-1%Z)%Z)) -> ((appear_twice a2 v2 i) /\ ~ (v2 = v1))) /\
MARCHE Claude's avatar
MARCHE Claude committed
82
  ((forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ((((map.Map.get deja_vu2
Andrei Paskevich's avatar
Andrei Paskevich committed
83
  v) = true) /\ exists j:Z, ((0%Z <= j)%Z /\ (j < i)%Z) /\ ((map.Map.get a1
MARCHE Claude's avatar
MARCHE Claude committed
84
  j) = v)) \/ ((~ ((map.Map.get deja_vu2 v) = true)) /\ forall (j:Z),
Andrei Paskevich's avatar
Andrei Paskevich committed
85 86 87 88 89
  ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((map.Map.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 := (map.Map.get a1 i) in
MARCHE Claude's avatar
MARCHE Claude committed
90 91 92 93 94 95 96 97 98 99
  (((0%Z <= deja_vu)%Z /\ ((0%Z <= v)%Z /\ (v < deja_vu)%Z)) ->
  ((~ ((map.Map.get deja_vu2 v) = true)) -> (((0%Z <= v)%Z /\
  (v < deja_vu)%Z) -> forall (deja_vu3:(map.Map.map Z bool)),
  ((0%Z <= deja_vu)%Z /\ (deja_vu3 = (map.Map.set deja_vu2 v true))) ->
  ((v2 = (-1%Z)%Z) -> forall (v3:Z), ((0%Z <= v3)%Z /\ (v3 < n)%Z) ->
  ((~ (v3 = v1)) -> ~ (appear_twice a2 v3 (i + 1%Z)%Z))))))))))).
intros a a1 n a2 (h1,((h2,h3),(h4,(v1,(h5,(v2,(h6,h7))))))) h8
        deja_vu deja_vu1 (h9,(h10,h11)) o h12 v3 v4 deja_vu2 i (h13,h14)
        (h15,(h16,(h17,(h18,(h19,h20))))) (h21,h22) v (h23,(h24,h25)) h26
        (h27,h28) deja_vu3 (h29,h30) h31 v5 (h32,h33) h34.
Andrei Paskevich's avatar
Andrei Paskevich committed
100
intros h0;
MARCHE Claude's avatar
MARCHE Claude committed
101 102
destruct (h18 (Map.get a1 i)); intuition.
subst v; omega.
Andrei Paskevich's avatar
Andrei Paskevich committed
103 104
red in h0.
destruct h0 as (i0,(h00,(h01,(j,(h02,(h03,h04)))))).
MARCHE Claude's avatar
MARCHE Claude committed
105
assert (v5 <> Map.get a1 i).
106
assert (case: (i0 < i \/ j < i)%Z) by omega. destruct case.
Andrei Paskevich's avatar
Andrei Paskevich committed
107 108
red; intro; apply (H1 i0). omega. unfold get in h01; simpl in h01. omega.
red; intro; apply (H1 j). omega. unfold get in h04; simpl in h04. omega.
MARCHE Claude's avatar
MARCHE Claude committed
109
apply (H v5); auto.
MARCHE Claude's avatar
MARCHE Claude committed
110 111
red; exists i0.
split.
112
assert (case: (i0 < i \/ i0 = i)%Z) by omega. destruct case.
MARCHE Claude's avatar
MARCHE Claude committed
113
auto with zarith.
114
subst i0.
Andrei Paskevich's avatar
Andrei Paskevich committed
115
unfold get in h01; simpl in h01.
116
omega.
MARCHE Claude's avatar
MARCHE Claude committed
117 118
split; auto.
exists j.
119
assert (case: (j < i \/ j = i)%Z) by omega. destruct case.
MARCHE Claude's avatar
MARCHE Claude committed
120
auto with zarith.
121
subst j.
Andrei Paskevich's avatar
Andrei Paskevich committed
122
unfold get in h04; simpl in h04.
123 124 125
omega.
Qed.