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

(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
9
10
11
Inductive datatype  :=
  | Tint : datatype 
  | Tbool : datatype .
12
13
Axiom datatype_WhyType : WhyType datatype.
Existing Instance datatype_WhyType.
MARCHE Claude's avatar
MARCHE Claude committed
14

15
(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
16
17
18
19
20
Inductive operator  :=
  | Oplus : operator 
  | Ominus : operator 
  | Omult : operator 
  | Ole : operator .
21
22
Axiom operator_WhyType : WhyType operator.
Existing Instance operator_WhyType.
MARCHE Claude's avatar
MARCHE Claude committed
23

24
(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
25
26
Definition ident  := Z.

27
(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
28
29
30
31
32
Inductive term  :=
  | Tconst : Z -> term 
  | Tvar : Z -> term 
  | Tderef : Z -> term 
  | Tbin : term -> operator -> term -> term .
33
34
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
MARCHE Claude's avatar
MARCHE Claude committed
35

36
(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
37
38
39
40
41
42
43
Inductive fmla  :=
  | Fterm : term -> fmla 
  | Fand : fmla -> fmla -> fmla 
  | Fnot : fmla -> fmla 
  | Fimplies : fmla -> fmla -> fmla 
  | Flet : Z -> term -> fmla -> fmla 
  | Fforall : Z -> datatype -> fmla -> fmla .
44
45
Axiom fmla_WhyType : WhyType fmla.
Existing Instance fmla_WhyType.
MARCHE Claude's avatar
MARCHE Claude committed
46

47
(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
48
49
50
Inductive value  :=
  | Vint : Z -> value 
  | Vbool : bool -> value .
51
52
Axiom value_WhyType : WhyType value.
Existing Instance value_WhyType.
MARCHE Claude's avatar
MARCHE Claude committed
53

54
55
(* Why3 assumption *)
Definition env  := (map.Map.map Z value).
MARCHE Claude's avatar
MARCHE Claude committed
56

57
58
(* Why3 assumption *)
Definition var_env  := (map.Map.map Z value).
MARCHE Claude's avatar
MARCHE Claude committed
59

60
61
(* Why3 assumption *)
Definition ref_env  := (map.Map.map Z value).
MARCHE Claude's avatar
MARCHE Claude committed
62

63
(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
64
Inductive state  :=
65
66
67
68
69
70
71
72
  | mk_state : (map.Map.map Z value) -> (map.Map.map Z value) -> state .
Axiom state_WhyType : WhyType state.
Existing Instance state_WhyType.

(* Why3 assumption *)
Definition ref_env1(v:state): (map.Map.map Z value) :=
  match v with
  | (mk_state x x1) => x1
MARCHE Claude's avatar
MARCHE Claude committed
73
74
  end.

75
76
77
78
(* Why3 assumption *)
Definition var_env1(v:state): (map.Map.map Z value) :=
  match v with
  | (mk_state x x1) => x
MARCHE Claude's avatar
MARCHE Claude committed
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
  end.

Parameter eval_bin: value -> operator -> value -> value.

Axiom eval_bin_def : forall (x:value) (op:operator) (y:value), match (x,
  y) with
  | ((Vint x1), (Vint y1)) =>
      match op with
      | Oplus => ((eval_bin x op y) = (Vint (x1 + y1)%Z))
      | Ominus => ((eval_bin x op y) = (Vint (x1 - y1)%Z))
      | Omult => ((eval_bin x op y) = (Vint (x1 * y1)%Z))
      | Ole => ((x1 <= y1)%Z -> ((eval_bin x op y) = (Vbool true))) /\
          ((~ (x1 <= y1)%Z) -> ((eval_bin x op y) = (Vbool false)))
      end
  | (_, _) => ((eval_bin x op y) = (Vbool false))
  end.

96
(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
97
98
99
Fixpoint eval_term(s:state) (t:term) {struct t}: value :=
  match t with
  | (Tconst n) => (Vint n)
100
101
  | (Tvar id) => (map.Map.get (var_env1 s) id)
  | (Tderef id) => (map.Map.get (ref_env1 s) id)
MARCHE Claude's avatar
MARCHE Claude committed
102
103
104
  | (Tbin t1 op t2) => (eval_bin (eval_term s t1) op (eval_term s t2))
  end.

105
(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
106
107
108
109
110
Fixpoint eval_fmla(s:state) (f:fmla) {struct f}: Prop :=
  match f with
  | (Fterm t) => ((eval_term s t) = (Vbool true))
  | (Fand f1 f2) => (eval_fmla s f1) /\ (eval_fmla s f2)
  | (Fnot f1) => ~ (eval_fmla s f1)
111
112
113
  | (Fimplies f1 f2) => (eval_fmla s f1) -> (eval_fmla s f2)
  | (Flet x t f1) => (eval_fmla (mk_state (map.Map.set (var_env1 s) x
      (eval_term s t)) (ref_env1 s)) f1)
MARCHE Claude's avatar
MARCHE Claude committed
114
  | (Fforall x Tint f1) => forall (n:Z),
115
116
      (eval_fmla (mk_state (map.Map.set (var_env1 s) x (Vint n))
      (ref_env1 s)) f1)
MARCHE Claude's avatar
MARCHE Claude committed
117
  | (Fforall x Tbool f1) => forall (b:bool),
118
119
      (eval_fmla (mk_state (map.Map.set (var_env1 s) x (Vbool b))
      (ref_env1 s)) f1)
MARCHE Claude's avatar
MARCHE Claude committed
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
  end.

Parameter subst_term: term -> Z -> term -> term.

Axiom subst_term_def : forall (e:term) (x:Z) (t:term),
  match e with
  | (Tconst _) => ((subst_term e x t) = e)
  | (Tvar _) => ((subst_term e x t) = e)
  | (Tderef y) => ((x = y) -> ((subst_term e x t) = t)) /\ ((~ (x = y)) ->
      ((subst_term e x t) = e))
  | (Tbin e1 op e2) => ((subst_term e x t) = (Tbin (subst_term e1 x t) op
      (subst_term e2 x t)))
  end.

Axiom eval_subst_term : forall (s:state) (e:term) (x:Z) (t:term),
  ((eval_term s (subst_term e x t)) = (eval_term (mk_state (var_env1 s)
136
  (map.Map.set (ref_env1 s) x (eval_term s t))) e)).
MARCHE Claude's avatar
MARCHE Claude committed
137

138
(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
139
140
141
142
143
144
Fixpoint subst(f:fmla) (x:Z) (t:term) {struct f}: fmla :=
  match f with
  | (Fterm e) => (Fterm (subst_term e x t))
  | (Fand f1 f2) => (Fand (subst f1 x t) (subst f2 x t))
  | (Fnot f1) => (Fnot (subst f1 x t))
  | (Fimplies f1 f2) => (Fimplies (subst f1 x t) (subst f2 x t))
145
  | (Flet y t' f1) => (Flet y t' (subst f1 x t))
MARCHE Claude's avatar
MARCHE Claude committed
146
147
148
  | (Fforall y ty f1) => (Fforall y ty (subst f1 x t))
  end.

149
150
151
Axiom eval_subst : forall (f:fmla) (s:state) (x:Z) (t:term), (eval_fmla s
  (subst f x t)) <-> (eval_fmla (mk_state (var_env1 s)
  (map.Map.set (ref_env1 s) x (eval_term s t))) f).
MARCHE Claude's avatar
MARCHE Claude committed
152

153
(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
154
155
156
157
158
Inductive stmt  :=
  | Sskip : stmt 
  | Sassign : Z -> term -> stmt 
  | Sseq : stmt -> stmt -> stmt 
  | Sif : term -> stmt -> stmt -> stmt 
159
  | Sassert : fmla -> stmt 
MARCHE Claude's avatar
MARCHE Claude committed
160
  | Swhile : term -> fmla -> stmt -> stmt .
161
162
Axiom stmt_WhyType : WhyType stmt.
Existing Instance stmt_WhyType.
MARCHE Claude's avatar
MARCHE Claude committed
163
164
165

Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).

166
(* Why3 assumption *)
MARCHE Claude's avatar
MARCHE Claude committed
167
168
Inductive one_step : state -> stmt -> state -> stmt -> Prop :=
  | one_step_assign : forall (s:state) (x:Z) (e:term), (one_step s (Sassign x
169
170
171
172
173
      e) (mk_state (var_env1 s) (map.Map.set (ref_env1 s) x (eval_term s e)))
      Sskip)
  | one_step_seq : forall (s:state) (s':state) (i1:stmt) (i1':stmt)
      (i2:stmt), (one_step s i1 s' i1') -> (one_step s (Sseq i1 i2) s'
      (Sseq i1' i2))
MARCHE Claude's avatar
MARCHE Claude committed
174
175
176
177
178
179
  | one_step_seq_skip : forall (s:state) (i:stmt), (one_step s (Sseq Sskip i)
      s i)
  | one_step_if_true : forall (s:state) (e:term) (i1:stmt) (i2:stmt),
      ((eval_term s e) = (Vbool true)) -> (one_step s (Sif e i1 i2) s i1)
  | one_step_if_false : forall (s:state) (e:term) (i1:stmt) (i2:stmt),
      ((eval_term s e) = (Vbool false)) -> (one_step s (Sif e i1 i2) s i2)
180
181
  | one_step_assert : forall (s:state) (f:fmla), (eval_fmla s f) ->
      (one_step s (Sassert f) s Sskip)
MARCHE Claude's avatar
MARCHE Claude committed
182
183
184
185
186
187
188
189
  | one_step_while_true : forall (s:state) (e:term) (inv:fmla) (i:stmt),
      (eval_fmla s inv) -> (((eval_term s e) = (Vbool true)) -> (one_step s
      (Swhile e inv i) s (Sseq i (Swhile e inv i))))
  | one_step_while_false : forall (s:state) (e:term) (inv:fmla) (i:stmt),
      (eval_fmla s inv) -> (((eval_term s e) = (Vbool false)) -> (one_step s
      (Swhile e inv i) s Sskip)).


190
(* Why3 goal *)
MARCHE Claude's avatar
MARCHE Claude committed
191
Theorem If42 : forall (s1:state) (s2:state) (i:stmt),
192
193
194
195
196
197
  (one_step (mk_state (map.Map.const (Vint 42%Z):(map.Map.map Z value))
  (map.Map.const (Vint 0%Z):(map.Map.map Z value))) (Sif (Tbin (Tderef 0%Z)
  Ole (Tconst 10%Z)) (Sassign 0%Z (Tconst 13%Z)) (Sassign 0%Z (Tconst 42%Z)))
  s1 i) -> ((one_step s1 i s2 Sskip) -> ((map.Map.get (ref_env1 s2)
  0%Z) = (Vint 13%Z))).
Proof.
MARCHE Claude's avatar
MARCHE Claude committed
198
199
200
201
intros s1 s2 i H1 H2.
inversion H1; subst; clear H1.
inversion H7; subst; clear H7.
inversion H2; subst; clear H2.
202
Opaque Map.const.
MARCHE Claude's avatar
MARCHE Claude committed
203
simpl.
204
rewrite Map.Select_eq; auto.
MARCHE Claude's avatar
MARCHE Claude committed
205
206
207

inversion H7; subst; clear H7.
clear H2.
208
rewrite Map.Const in H0.
MARCHE Claude's avatar
MARCHE Claude committed
209
210
211
212
213
214
215
216
217
generalize (eval_bin_def (Vint 0) Ole (Vint 10)).
rewrite H0; clear H0.
assert (h:((0 <= 10)%Z)) by omega.
intros (H1,_).
generalize (H1 h).
intro; discriminate.
Qed.