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

Axiom ident : Type.
Parameter ident_WhyType : WhyType ident.
Existing Instance ident_WhyType.
11
12
13
14
15
16
17
18

Axiom ident_eq_dec : forall (i1:ident) (i2:ident), (i1 = i2) \/ ~ (i1 = i2).

Parameter mk_ident: Z -> ident.

Axiom mk_ident_inj : forall (i:Z) (j:Z), ((mk_ident i) = (mk_ident j)) ->
  (i = j).

19
(* Why3 assumption *)
20
21
22
23
Inductive operator  :=
  | Oplus : operator 
  | Ominus : operator 
  | Omult : operator .
24
25
Axiom operator_WhyType : WhyType operator.
Existing Instance operator_WhyType.
26

27
(* Why3 assumption *)
28
29
30
31
Inductive expr  :=
  | Econst : Z -> expr 
  | Evar : ident -> expr 
  | Ebin : expr -> operator -> expr -> expr .
32
33
Axiom expr_WhyType : WhyType expr.
Existing Instance expr_WhyType.
34

35
(* Why3 assumption *)
36
37
38
39
40
41
Inductive stmt  :=
  | Sskip : stmt 
  | Sassign : ident -> expr -> stmt 
  | Sseq : stmt -> stmt -> stmt 
  | Sif : expr -> stmt -> stmt -> stmt 
  | Swhile : expr -> stmt -> stmt .
42
43
Axiom stmt_WhyType : WhyType stmt.
Existing Instance stmt_WhyType.
44
45
46

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

47
48
(* Why3 assumption *)
Definition state  := (map.Map.map ident Z).
49

50
(* Why3 assumption *)
51
52
53
54
55
56
57
Definition eval_bin(x:Z) (op:operator) (y:Z): Z :=
  match op with
  | Oplus => (x + y)%Z
  | Ominus => (x - y)%Z
  | Omult => (x * y)%Z
  end.

58
59
(* Why3 assumption *)
Fixpoint eval_expr(s:(map.Map.map ident Z)) (e:expr) {struct e}: Z :=
60
61
  match e with
  | (Econst n) => n
62
  | (Evar x) => (map.Map.get s x)
63
64
65
  | (Ebin e1 op e2) => (eval_bin (eval_expr s e1) op (eval_expr s e2))
  end.

66
67
(* Why3 assumption *)
Inductive one_step : (map.Map.map ident Z) -> stmt -> (map.Map.map ident Z)
68
  -> stmt -> Prop :=
69
70
71
72
73
74
75
76
77
78
79
  | one_step_assign : forall (s:(map.Map.map ident Z)) (x:ident) (e:expr),
      (one_step s (Sassign x e) (map.Map.set s x (eval_expr s e)) Sskip)
  | one_step_seq : forall (s:(map.Map.map ident Z)) (s':(map.Map.map ident
      Z)) (i1:stmt) (i1':stmt) (i2:stmt), (one_step s i1 s' i1') ->
      (one_step s (Sseq i1 i2) s' (Sseq i1' i2))
  | one_step_seq_skip : forall (s:(map.Map.map ident Z)) (i:stmt),
      (one_step s (Sseq Sskip i) s i)
  | one_step_if_true : forall (s:(map.Map.map ident Z)) (e:expr) (i1:stmt)
      (i2:stmt), (~ ((eval_expr s e) = 0%Z)) -> (one_step s (Sif e i1 i2) s
      i1)
  | one_step_if_false : forall (s:(map.Map.map ident Z)) (e:expr) (i1:stmt)
80
      (i2:stmt), ((eval_expr s e) = 0%Z) -> (one_step s (Sif e i1 i2) s i2)
81
  | one_step_while_true : forall (s:(map.Map.map ident Z)) (e:expr) (i:stmt),
82
83
      (~ ((eval_expr s e) = 0%Z)) -> (one_step s (Swhile e i) s (Sseq i
      (Swhile e i)))
84
85
  | one_step_while_false : forall (s:(map.Map.map ident Z)) (e:expr)
      (i:stmt), ((eval_expr s e) = 0%Z) -> (one_step s (Swhile e i) s Sskip).
86

87
88
89
Axiom progress : forall (s:(map.Map.map ident Z)) (i:stmt),
  (~ (i = Sskip)) -> exists s':(map.Map.map ident Z), exists i':stmt,
  (one_step s i s' i').
90

91
92
(* Why3 assumption *)
Inductive many_steps : (map.Map.map ident Z) -> stmt -> (map.Map.map ident Z)
93
  -> stmt -> Prop :=
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
  | many_steps_refl : forall (s:(map.Map.map ident Z)) (i:stmt),
      (many_steps s i s i)
  | many_steps_trans : forall (s1:(map.Map.map ident Z)) (s2:(map.Map.map
      ident Z)) (s3:(map.Map.map ident Z)) (i1:stmt) (i2:stmt) (i3:stmt),
      (one_step s1 i1 s2 i2) -> ((many_steps s2 i2 s3 i3) -> (many_steps s1
      i1 s3 i3)).

Axiom many_steps_seq_rec : forall (s1:(map.Map.map ident Z)) (s3:(map.Map.map
  ident Z)) (i:stmt) (i3:stmt), (many_steps s1 i s3 i3) -> ((i3 = Sskip) ->
  forall (i1:stmt) (i2:stmt), (i = (Sseq i1 i2)) -> exists s2:(map.Map.map
  ident Z), (many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip)).

Axiom many_steps_seq : forall (s1:(map.Map.map ident Z)) (s3:(map.Map.map
  ident Z)) (i1:stmt) (i2:stmt), (many_steps s1 (Sseq i1 i2) s3 Sskip) ->
  exists s2:(map.Map.map ident Z), (many_steps s1 i1 s2 Sskip) /\
  (many_steps s2 i2 s3 Sskip).

(* Why3 assumption *)
112
Inductive fmla  :=
113
114
115
116
117
118
119
120
  | Fterm : expr -> fmla 
  | Fand : fmla -> fmla -> fmla 
  | Fnot : fmla -> fmla .
Axiom fmla_WhyType : WhyType fmla.
Existing Instance fmla_WhyType.

(* Why3 assumption *)
Fixpoint eval_fmla(s:(map.Map.map ident Z)) (f:fmla) {struct f}: Prop :=
121
122
  match f with
  | (Fterm e) => ~ ((eval_expr s e) = 0%Z)
123
124
  | (Fand f1 f2) => (eval_fmla s f1) /\ (eval_fmla s f2)
  | (Fnot f1) => ~ (eval_fmla s f1)
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
  end.

Parameter subst_expr: expr -> ident -> expr -> expr.

Axiom subst_expr_def : forall (e:expr) (x:ident) (t:expr),
  match e with
  | (Econst _) => ((subst_expr e x t) = e)
  | (Evar y) => ((x = y) -> ((subst_expr e x t) = t)) /\ ((~ (x = y)) ->
      ((subst_expr e x t) = e))
  | (Ebin e1 op e2) => ((subst_expr e x t) = (Ebin (subst_expr e1 x t) op
      (subst_expr e2 x t)))
  end.



140
141
142
(* Why3 goal *)
Theorem eval_subst_expr : forall (s:(map.Map.map ident Z)) (e:expr) (x:ident)
  (t:expr), ((eval_expr s (subst_expr e x t)) = (eval_expr (map.Map.set s x
143
  (eval_expr s t)) e)).
144
Proof.
145
146
147
148
149
150
151
152
153
154
155
intros s e x t.
induction e.
(* case Econst *)
rewrite (subst_expr_def (Econst z) x t).
now simpl.
(* case Evar *)
generalize (subst_expr_def (Evar i) x t).
intros (H1,H2).
case (ident_eq_dec x i).
(* subcase x=i *)
simpl; intro; subst x.
156
rewrite Map.Select_eq; auto.
157
158
159
now rewrite H1.
(* subcase x<>i *)
simpl; intro.
160
rewrite Map.Select_neq; auto.
161
162
163
164
165
166
167
168
169
now rewrite H2.
(* case Ebin *)
rewrite (subst_expr_def (Ebin e1 o e2) x t).
simpl.
rewrite IHe2.
now rewrite IHe1.
Qed.