Les lignes suivante donnent la description du petit langage que nous avons utilisé dans le cours.
The following commands are the description of the small language we have used since the beginning of the course.
Require Import ZArith List Zwf. Open Scope Z_scope. Inductive aexpr : Set := avar : Z -> aexpr | aint : Z -> aexpr | aplus : aexpr -> aexpr -> aexpr. Inductive bexpr : Set := blt : aexpr -> aexpr -> bexpr. Inductive instr : Set := skip : instr | assign : Z -> aexpr -> instr | sequence : instr -> instr -> instr | while : bexpr -> instr -> instr.
Voici maintenant la définition des jugements sémantiques.
Here are the definition of the semantic judgments.
Inductive a_eval : list(Z*Z) -> aexpr -> Z -> Prop :=
ae_int : forall r n, a_eval r (aint n) n
| ae_var1 : forall r x v, a_eval ((x,v)::r) (avar x) v
| ae_var2 : forall r x y v v' ,
x <> y -> a_eval r (avar x) v' ->
a_eval ((y,v)::r) (avar x) v'
| ae_plus : forall r e1 e2 v1 v2,
a_eval r e1 v1 -> a_eval r e2 v2 ->
a_eval r (aplus e1 e2) (v1 + v2).
Inductive b_eval : list(Z*Z) -> bexpr -> bool -> Prop :=
| be_lt1 : forall r e1 e2 v1 v2,
a_eval r e1 v1 -> a_eval r e2 v2 ->
v1 < v2 -> b_eval r (blt e1 e2) true
| be_lt2 : forall r e1 e2 v1 v2,
a_eval r e1 v1 -> a_eval r e2 v2 ->
v2 <= v1 -> b_eval r (blt e1 e2) false.
Hint Resolve ae_int ae_var1 ae_var2 ae_plus.
Inductive s_update : list(Z*Z)->Z->Z->list(Z*Z)->Prop :=
| s_up1 :
forall r x v v', s_update ((x,v)::r) x v' ((x,v')::r)
| s_up2 :
forall r r' x y v v', s_update r x v' r' -> x <> y ->
s_update ((y,v)::r) x v' ((y,v)::r').
Inductive s_exec : list(Z*Z)->instr->list(Z*Z)->Prop :=
| SN1 : forall r, s_exec r skip r
| SN2 : forall r r' x e v,
a_eval r e v -> s_update r x v r' ->
s_exec r (assign x e) r'
| SN3 : forall r r' r'' i1 i2,
s_exec r i1 r' -> s_exec r' i2 r'' ->
s_exec r (sequence i1 i2) r''
| SN4 : forall r r' r'' b i,
b_eval r b true -> s_exec r i r' ->
s_exec r' (while b i) r'' ->
s_exec r (while b i) r''
| SN5 : forall r b i,
b_eval r b false -> s_exec r (while b i) r.
Hint Resolve
be_lt1 be_lt2 s_up1 s_up2 SN1 SN2 SN3 SN4 SN5.
Dans nos exercices nous utiliserons la convention que le nom de la variable "x" est représenté par l'entier 1 et le nom de la variable "y" est représenté par l'entier 2.
In our exercices, we use the convention that the name of the variable "x"is représented by the integer 1 and the name of the variable "y"is représented by the integer 2.
Definition x_name := 1. Definition y_name := 2. Lemma x_diff_y : x_name <> y_name. Proof. unfold x_name, y_name; discriminate. Qed. Lemma y_diff_x : y_name <> x_name. Proof. unfold x_name, y_name; discriminate. Qed.
voici un exemple de définition d'une expression arithmétique, exp0 représente l'expression "5 + y".
Here is an example of definition of an arithmetic expression, exp0 represents the expression "5 + y".
Definition exp0 := aplus (aint 5) (avar y_name).
Votre premier exercice est de définir deux constantes exp1 et inst1 dont la première représente l'expression arithmétique "x + (y + 4)" et la deuxième représente l'instruction "y := x + (y + 4); x := 3".
Your first exercise: define two constants exp1 and inst1, which should represent respectively the arithmetic expression "x + (y + 4)" and the second represents the instruction "y := x + (y + 4); x := 3"
Prouvez le fait ev_exp1 qui décrit l'évaluation de exp1 dans le même environnement.
Second exercise: define the fact ev_exp1 that describes the evaluation of exp1 in the same environment.
Fact ev_exp1 : a_eval ((x_name,1)::(y_name,3)::nil) exp1 .....
Prouvez le fait ex_inst1 qui décrit l'exécution de inst1 à partir du même environment (réutilisez le fait ev_exp1 comme lemme. Define the fact ex_inst1 that describes the execution of inst1 in the same environment (re-use the fact ev_exp1 as a lemma.
Fact ex_inst1 : s_exec ((x_name,1)::(y_name,3)::nil) inst1 .....
il s'agit de démontrer que l'instruction "while b do x := e; y := n done" et l'instruction "while b do x := e done" se comportent de la même manière dans tout environment r tel que "a_eval r (avar y) n" soit satisfait. Il faut démontrer deux lemmes avant le résultat principal.
fourth exercise : you have to prove that the instruction "while b do x :=e ; y := n done" and the instruction "while b do x := e done" behave similarly in any environment r such that "a_eval r (avar y) n" is satisfied. You need to prove two lemmas before the main result.
Lemma update_unchanged :
forall r v n, a_eval r v n ->
forall id r', s_update r id n r' -> v = avar id -> r = r'.
Lemma update_diff :
forall r x n r', s_update r x n r' ->
forall y n', x<>y ->
a_eval r (avar y) n' -> a_eval r' (avar y) n'.
Fact simplify_loop :
forall r i r',
s_exec r i r' ->
forall b e n,
i = while b
(sequence (assign x_name e)(assign y_name (aint n))) ->
a_eval r (avar y_name) n ->
s_exec r (while b (assign x_name e)) r'.
On pourra conclure en démontrant que les deux instructions "y := n ; while b do x:= e done" et "while b do x:=e; y:= n done" sont équivalentes.
You can conclude by proving that the two instructions "y := n ; while b do x:= e done" and "while b do x:=e; y:= n done" are equivalent.
Les preuves qui ne seront pas terminées pendant les travaux dirigées seront terminées à la maison par les étudiants et rendues par courrier électronique.
The proofs that are not finished during the time of the laboratory session will be finished at home by the students and sent back by e-mail.
Indication, les tactiques à utiliser sont:
Hint, the tactics you need to use are the following ones:
induction, intros, inversion, apply, elim, discriminate, injection, assert, rewrite