On devra travailler avec les définitions suivantes:
Require Export ZArith String.
Require Export List.
Open Scope Z_scope.
Open Scope string_scope.
Inductive aexpr : Type :=
avar (s:string) | anum (x:Z) | aplus (e1 e2 : aexpr).
Inductive bexpr : Set :=
blt (e1 e2 : aexpr).
Inductive instr : Type:=
skip | assign (s:string) (e:aexpr)
| sequence (i1 i2 : instr) | while (b : bexpr) (i:instr).
Definition env := list (string * Z).
Inductive aeval : env -> aexpr -> Z -> Prop :=
ae_num : forall r n, aeval r (anum n) n
| ae_var1 : forall r x v, aeval ((x,v)::r) (avar x) v
| ae_var2 : forall r x y v v' , x <> y -> aeval r (avar x) v' ->
aeval ((y,v)::r) (avar x) v'
| ae_plus : forall r e1 e2 v1 v2,
aeval r e1 v1 -> aeval r e2 v2 ->
aeval r (aplus e1 e2) (v1 + v2).
Inductive beval : env -> bexpr -> bool -> Prop :=
| be_lt1 : forall r e1 e2 v1 v2,
aeval r e1 v1 -> aeval r e2 v2 ->
v1 < v2 -> beval r (blt e1 e2) true
| be_lt2 : forall r e1 e2 v1 v2,
aeval r e1 v1 -> aeval r e2 v2 ->
v2 <= v1 -> beval r (blt e1 e2) false.
Inductive update : env->string->Z->env->Prop :=
| s_up1 : forall r x v v', update ((x,v)::r) x v' ((x,v')::r)
| s_up2 : forall r r' x y v v', update r x v' r' ->
x <> y -> update ((y,v)::r) x v' ((y,v)::r').
Inductive exec : env->instr->env->Prop :=
| SN1 : forall r, exec r skip r
| SN2 : forall r r' x e v,
aeval r e v -> update r x v r' -> exec r (assign x e) r'
| SN3 : forall r r' r'' i1 i2,
exec r i1 r' -> exec r' i2 r'' ->
exec r (sequence i1 i2) r''
| SN4 : forall r r' r'' b i,
beval r b true -> exec r i r' ->
exec r' (while b i) r'' ->
exec r (while b i) r''
| SN5 : forall r b i,
beval r b false -> exec r (while b i) r.
Fixpoint lku e s : option Z :=
match e with
nil => None
| (x,v)::tl => if string_dec s x then Some v else lku tl s
end.
Fixpoint up e s v : option env :=
match e with
nil => None
| (x,v')::tl =>
if string_dec x s then
Some ((x, v)::tl)
else
match up tl s v with
None => None
| Some tl' => Some((x,v')::tl')
end
end.
Fixpoint evf e a : option Z :=
match a with
avar s => lku e s
| anum n => Some n
| aplus a1 a2 =>
match evf e a1 with
None => None
| Some v1 =>
match evf e a2 with
None => None
| Some v2 => Some (v1 + v2)
end
end
end.
Definition evbf e b : option bool :=
match b with
blt a1 a2 =>
match evf e a1 with
None => None
| Some v1 =>
match evf e a2 with
None => None
| Some v2 =>
if Z_lt_dec v1 v2 then
Some true
else
Some false
end
end
end.
Fixpoint run e i n : option env :=
match n with
S p =>
match i with
sequence i1 i2 =>
match run e i1 p with
Some r1 => run r1 i2 p
| None => None
end
| skip => Some e
| while be i' =>
match evbf e be with
None => None
| Some b =>
if b then
match run e i' p with
None => None
| Some r1 => run r1 (while be i') p
end
else
Some e
end
| assign x a =>
match evf e a with
None => None
| Some v => up e x v
end
end
| 0%nat => None
end.
On voudrait prouver les lemmes suivants
Lemma up_correct : forall e x v e', up e x v = Some e' -> update e x v e'. Lemma evf_correct : forall e a n, evf e a = Some n -> aeval e a n. Lemma evbf_correct : forall e be b, evbf e be = Some b -> beval e be b. Lemma run_correct : forall n e i e', run e i n = Some e' -> exec e i e'.