loglangcoq.logique.semantique_avec_procedure
Sémantique avec procédures
Require Export GenEnv.CoreGenericEnv.
Require Export GenEnv.GenericEnv.
Require Export GenEnv.GenericEnvList.
Require Import Morphisms FunInd.
Require Import Setoid.
Require Export Gen_env_more.
Open Scope list_scope.
Reserved Notation "x ;; y" (at level 70, right associativity).
Inductive exp : Set :=
| TRUE: exp
| FALSE: exp
| CST: nat ⟶ exp
| VAR: nat ⟶ exp
| PLUS: exp ⟶ exp ⟶ exp
| MINUS: exp ⟶ exp ⟶ exp
| OPP: exp ⟶ exp ⟶ exp
| MULT: exp ⟶ exp ⟶ exp
| DIV: exp ⟶ exp ⟶ exp
| AND: exp ⟶ exp ⟶ exp
| OR: exp ⟶ exp ⟶ exp
| NOT: exp ⟶ exp.
Notation "A + B" := (PLUS A B) : Prog_scope.
Notation "A - B" := (MINUS A B) : Prog_scope.
Notation "A * B" := (MULT A B) : Prog_scope.
Notation "A / B" := (DIV A B) : Prog_scope.
Notation "A && B" := (AND A B) : Prog_scope.
Notation "A || B" := (OR A B) : Prog_scope.
Notation "! A" := (NOT A) (at level 45) : Prog_scope.
Notation "'X'" := (VAR 1): Prog_scope.
Notation "'Y'" := (VAR 2): Prog_scope.
Notation "'Z'" := (VAR 3): Prog_scope.
Notation "'T'" := (VAR 4): Prog_scope.
Open Scope Prog_scope.
Le domaine d'interprétation des expressions
La sémantique opérationnelle à grands pas des expressions
Notation "'__________________' P2" := (P2) (at level 90, P2 at level 200, right associativity, only parsing).
Notation "'____________________________________' P2" := (P2) (at level 90, P2 at level 200, right associativity, only parsing).
La relation d'interprétation des expressions. Aussi appelée la
sémantique des expressions.
Inductive eval_exp (σ:gen_env value): exp ⟶ value ⟶ Prop :=
| Eval_Var: forall i v,
Ext.binds i v σ ⟶
《 σ, VAR i 》↦ v
| Eval_TRUE:
《 σ, TRUE 》 ↦ Bool true
| Eval_FALSE:
《 σ, FALSE 》 ↦ Bool false
| Eval_CST: forall i,
《 σ, CST i 》 ↦ Int i
| Eval_NOT: forall e v v',
《 σ , e 》 ↦ (Bool v') ⟶
v = negb v' ⟶
《 σ , ! e 》 ↦ Bool v
| Eval_AND: forall e1 v1 e2 v2 v,
《 σ , e1 》 ↦ (Bool v1) ⟶
《 σ , e2 》 ↦ (Bool v2) ⟶
v = andb v1 v2 ⟶
《 σ , e1 && e2 》 ↦ Bool v
| Eval_OR: forall e1 v1 e2 v2 v,
《 σ , e1 》 ↦ (Bool v1) ⟶
《 σ , e2 》 ↦ (Bool v2) ⟶
v = orb v1 v2 ⟶
《 σ , e1 || e2 》 ↦ Bool v
| Eval_PLUS: forall e1 v1 e2 v2 v,
《 σ , e1 》 ↦ (Int v1) ⟶
《 σ , e2 》 ↦ (Int v2) ⟶
v = (v1 +v2)%nat ⟶
《 σ , e1 + e2 》 ↦ Int v
| Eval_MINUS: forall e1 v1 e2 v2 v,
《 σ , e1 》 ↦ (Int v1) ⟶
《 σ , e2 》 ↦ (Int v2) ⟶
v = (v1 - v2)%nat ⟶
《 σ , e1 - e2 》 ↦ Int v
| Eval_MULT: forall e1 v1 e2 v2 v,
《 σ , e1 》 ↦ (Int v1) ⟶
《 σ , e2 》 ↦ (Int v2) ⟶
v = (v1 × v2)%nat ⟶
《 σ , e1 × e2 》 ↦ Int v
where " '《' A ',' B '》' '↦' C " := (eval_exp A B C) : Prog_scope.
Function eval_exp_list (σ:gen_env value) (le:list exp) (lv:list value) {struct le} : Prop :=
match le with
| nil =>
match lv with
| cons v lv' => False
| nil => True
end
| cons e le' =>
match lv with
| cons v lv' => eval_exp σ e v ∧ eval_exp_list σ le' lv'
| nil => False
end
end.
Lemma eval_exp1 : 《(ENV.Core.empty _) , CST 1 + CST 2 》 ↦ Int 3.
Proof.
apply (Eval_PLUS _ _ 1 _ 2).
apply Eval_CST.
apply Eval_CST.
reflexivity.
Qed.
Print eval_exp1.
Preuve du déterminisme de la sémantique des expressions.
Lemma determinisme_exp :
forall σ e v, 《σ,e》 ↦ v ⟶ forall v', 《σ,e》 ↦ v' ⟶ v = v'.
Proof.
intros σ e x semv.
induction semv; intros x' semx';inversion semx';clear semx';subst.
- eapply Ext.binds_eq_inv;eauto.
- trivial.
- trivial.
- trivial.
- apply IHsemv in H1.
inversion H1.
auto.
- apply IHsemv1 in H2.
apply IHsemv2 in H3.
inversion H2.
inversion H3.
auto.
- apply IHsemv1 in H2.
apply IHsemv2 in H3.
inversion H2.
inversion H3.
auto.
- apply IHsemv1 in H2.
apply IHsemv2 in H3.
inversion H2.
inversion H3.
auto.
- apply IHsemv1 in H2.
apply IHsemv2 in H3.
inversion H2.
inversion H3.
auto.
- apply IHsemv1 in H2.
apply IHsemv2 in H3.
inversion H2.
inversion H3.
auto.
Qed.
Corollary deterministe_eval_exp_list: forall σ le lv lv',
eval_exp_list σ le lv
⟶ eval_exp_list σ le lv'
⟶ lv = lv'.
Proof.
intros σ le.
induction le;simpl;intros.
- destruct lv; destruct lv'; try contradiction;auto.
- destruct lv; destruct lv'; try contradiction;auto.
destruct H as [h h'].
destruct H0 as [h0 h0'].
rewrite (IHle lv lv').
+ rewrite (determinisme_exp _ _ _ h _ h0).
reflexivity.
+ assumption.
+ assumption.
Qed.
Inductive prog : Set :=
NOPE: prog
| AFF: nat ⟶ exp ⟶ prog
| SEQ: prog ⟶ prog ⟶ prog
| IFTE: exp ⟶ prog ⟶ prog ⟶ prog
| WHILE: exp ⟶ prog ⟶ prog
| CALL: nat ⟶ list exp ⟶ prog.
Quelques notations pour y voir plus clair.
Notation "A ;; B" := (SEQ A B): Prog_scope.
Notation "N ← B" := (AFF N B) (at level 65): Prog_scope.
Notation "'X' ← B" := (AFF 1 B) (at level 65): Prog_scope.
Notation "'Y' ← B" := (AFF 2 B) (at level 65): Prog_scope.
Notation "'Z' ← B" := (AFF 3 B) (at level 65): Prog_scope.
Notation "'T' ← B" := (AFF 4 B) (at level 65): Prog_scope.
Notation "'IF' A 'THEN' B 'ELSE' C" := (IFTE A B C) (at level 200): Prog_scope.
Notation "'WHILE' A 'DO' B 'DONE'" := (WHILE A B) (at level 71): Prog_scope.
Notation "'f(' L ')'" := (CALL 1 L) : Prog_scope.
Notation "'g(' L ')'" := (CALL 2 L) : Prog_scope.
Notation "'h(' L ')'" := (CALL 3 L) : Prog_scope.
Module Ex_prog.
Exemples de programme;
Definition prog1:prog :=
WHILE TRUE DO
NOPE ;;
X ← CST(2) + X;;
Y ← Y + Z;;
f( (X :: (CST(2) + Y)::nil) )
DONE.
End Ex_prog.
La sémantique (opérationnelle, à grands pas) des programmes
La relation d'interprétation des programmes, aussi appelée la
sémantique des programmes. Le domaine d'interprétation est
gen_env value c'est-à-dire qu'un programme est interprété comme
une fonction (partielle, certains programmes ne termine pas ou
n'ont pas de signification) des états (ou environnements) vers les
états.
À la différence des définitions précédentes (sémantiques sans
procédure), on n'utilise plus l'équivalence sur les environnement,
mais l'égalité stricte. Cela permet de simplifier les preuves sur
le pop.
Print Scopes.
Inductive eval_prog (π:gen_env (list nat×prog)) : prog ⟶ gen_env value ⟶ gen_env value ⟶ Prop :=
| Eval_NOPE: forall σ σ',
σ = σ' ⟶
《 σ, NOPE, π 》 ⟿ σ'
| Eval_Seq: forall σ p1 σ' p2 σ'',
《 σ, p1, π 》 ⟿ σ' ⟶
《 σ', p2, π 》 ⟿ σ'' ⟶
《 σ, p1;;p2, π 》 ⟿ σ''
| Eval_Aff: forall σ e i v σ',
《 σ, e 》 ↦ v ⟶
σ' = σ [ i <- v] ⟶
《 σ, i ← e, π 》 ⟿ σ'
| Eval_If_then: forall σ e p1 p2 σ',
《 σ, e 》 ↦ Bool true ⟶
《 σ, p1, π 》⟿ σ' ⟶
《 σ, (IF e THEN p1 ELSE p2), π 》 ⟿ σ'
| Eval_If_else: forall σ e p1 p2 σ',
《 σ, e 》 ↦ Bool false ⟶
《 σ, p2, π 》⟿ σ' ⟶
《 σ, (IF e THEN p1 ELSE p2), π 》 ⟿ σ'
| Eval_While_true: forall σ e p σ' σ'',
《 σ, e 》 ↦ Bool true ⟶
《 σ, p, π 》 ⟿ σ' ⟶
《 σ', WHILE e DO p DONE, π 》⟿ σ'' ⟶
《 σ, WHILE e DO p DONE, π 》 ⟿ σ''
| Eval_While_false: forall σ e p σ',
σ = σ' ⟶
《 σ, e 》 ↦ Bool false ⟶
《 σ, WHILE e DO p DONE, π 》 ⟿ σ'
| Eval_Proc: forall σ prc lid le lv σproc σ' σ'' pbody,
Ext.binds prc (lid,pbody) π ⟶
eval_exp_list σ le lv ⟶
pushl lid lv σ = Some σproc ⟶
《 σproc , pbody, π 》 ⟿ σ' ⟶
pop_forgetl (List.length lv) σ' = Some σ'' ⟶
《 σ, CALL prc le, π 》 ⟿ σ''
where " '《' A ',' B ',' C '》' '⟿' D " := (eval_prog C B A D) : Prog_scope.
Lemma determinisme_prog :
forall π σ p σ', 《σ,p,π》 ⟿ σ' ⟶ forall σ'', 《σ,p,π》 ⟿ σ'' ⟶ σ' = σ''.
Proof.
intros π σ p σ' Hσ'.
induction Hσ'; try (rename σ'' into σaux) ; intros σ'' Hσ''.
- inversion Hσ'';auto.
transitivity σ;auto.
- inversion Hσ'';subst;eauto.
inversion Hσ'';subst.
assert (σ' = σ'0).
+ eapply IHHσ'1;eauto.
+ eapply IHHσ'2;eauto.
rewrite H;auto.
- inversion Hσ'';subst.
assert (heq: v = v0 ).
eapply determinisme_exp;eauto.
rewrite heq in ×.
eauto.
- inversion Hσ'';subst.
apply IHHσ';auto.
absurd (Bool false = Bool true).
intro.
inversion H0.
eapply determinisme_exp;eauto.
- inversion Hσ'';subst.
absurd (Bool false = Bool true).
intro.
inversion H0.
eapply determinisme_exp;eauto.
apply IHHσ';auto.
- inversion Hσ'';subst.
+ assert (σ' = σ'0).
{ apply IHHσ'1;auto. }
eapply IHHσ'2;eauto.
rewrite H0;auto.
+ eapply IHHσ'2;eauto.
absurd (Bool false = Bool true).
intro.
inversion H0.
eapply determinisme_exp;eauto.
- inversion Hσ'';subst.
absurd (Bool false = Bool true).
intro.
inversion H.
eapply determinisme_exp;eauto.
eauto.
- inversion Hσ'';subst.
generalize (@Ext.binds_eq_inv _ prc _ _ π H H5).
intros heqbody.
inversion heqbody as [[heqbody1 heqbody2]]; clear heqbody;subst.
assert (lv = lv0).
{ eapply deterministe_eval_exp_list;eauto. }
subst.
assert (σ' = σ'0).
{ apply IHHσ';auto.
rewrite H1 in H7.
inversion H7. subst.
assumption.
}
subst. rewrite H2 in H11. inversion H11. reflexivity.
Qed.
This page has been generated by coqdoc