loglangcoq.logique.semantique_avec_routine

Sémantique avec routines

Ce module formalise la sémantique d'un petit langage impératif.

Require Export GenEnv.CoreGenericEnv.
Require Export GenEnv.GenericEnv.
Require Export GenEnv.GenericEnvList.
Require Import Morphisms.
Require Import Setoid.
Require Export Gen_env_more.

Open Scope gen_env_scope.

Les expressions

Le type des expressions entière et booléennes

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

Inductive value : Set :=
Bool: bool ⟶ value
| Int: nat ⟶ value.

La sémantique opérationnelle à grands pas des expressions

Afin de présenter la sémantique sous la forme de règles d'inférences, on introduit la barre horizontal comme une notation qui ne fait rien.

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.

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';subst.
    eapply Ext.binds_eq_inv;eauto.
  - inversion semx';subst. trivial.
  - inversion semx';subst. trivial.
  - inversion semx';subst. trivial.
  - inversion semx';subst.
    apply IHsemv in H1.
    inversion H1.
    auto.
  - inversion semx';subst.
    apply IHsemv1 in H2.
    apply IHsemv2 in H3.
    inversion H2.
    inversion H3.
    auto.
  - inversion semx';subst.
    apply IHsemv1 in H2.
    apply IHsemv2 in H3.
    inversion H2.
    inversion H3.
    auto.
  - inversion semx';subst.
    apply IHsemv1 in H2.
    apply IHsemv2 in H3.
    inversion H2.
    inversion H3.
    auto.
  - inversion semx';subst.
    apply IHsemv1 in H2.
    apply IHsemv2 in H3.
    inversion H2.
    inversion H3.
    auto.
  - inversion semx';subst.
    apply IHsemv1 in H2.
    apply IHsemv2 in H3.
    inversion H2.
    inversion H3.
    auto.
Qed.

Les programmes

Le type des programmes

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()'" := (CALL 1) : Prog_scope.
Notation "'g()'" := (CALL 2) : Prog_scope.
Notation "'h()'" := (CALL 3) : Prog_scope.

Module Ex_prog.

Exemples de programme;

  Definition prog1:prog :=
    WHILE TRUE DO
      NOPE ;;
      X ← CST(2) + X ;;
      Y ← Y + Z ;;
      f ()
    DONE.

End Ex_prog.

La sémantique (opérationnelle, à grands pas) des programmes

On note E ≡ F lorsque E et F sont deux environnements (deux états) équivalents (les variables ont les mêmes valeurs).

Notation "E '≡' F" := (Ext.eq E F) (at level 68) : gen_env_scope.

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) des états (ou environnements) vers les états.

Inductive eval_prog (π:gen_env 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 σ' pbody,
                                     Ext.binds prc pbody π ⟶
                                     《 σ , pbody , π 》 ⟿ σ' ⟶

                                     《 σ , CALL prc , π 》 ⟿ σ'


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).
    + apply IHHσ'1;auto.
    + 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 H1.
    eapply determinisme_exp;eauto.
    eauto.

  - apply IHHσ'.
    inversion Hσ'';subst.
    rewrite (@Ext.binds_eq_inv _ prc pbody pbody0 π);auto.
Qed.

This page has been generated by coqdoc