Library coq8_SN_props



Require Import Bool Arith List.
Import List.ListNotations.

On choisit de définir ici un état comme une liste d'entiers naturels.

On utilise ici le type list de la bibliothèque standard de Coq. Ce type est polymorphe. On le spécialise pour des éléments de type nat.

On reprend ici les AST définis aux séances précédentes

Syntaxe des expressions arithmétiques


Inductive aexp :=
| Aco : nat → aexp
constantes
| Ava : nat → aexp
variables
| Apl : aexp → aexp → aexp
| Amu : aexp → aexp → aexp
| Amo : aexp → aexp → aexp
.

Syntaxe des expressions booléennes


Inductive bexp :=
| Btrue : bexp
| Bfalse : bexp
| Bnot : bexp → bexp
| Band : bexp → bexp → bexp
| Bor : bexp → bexp → bexp
| Beq : bexp → bexp → bexp
| Beqnat : aexp → aexp → bexp
.

Syntaxe du langage impératif WHILE


Inductive winstr :=
| : winstr
| Assign : nat → aexp → winstr
| Seq : winstr → winstr → winstr
| If : bexp → winstr → winstr → winstr
| While : bexp → winstr → winstr
.

Quelques listes/états pour faire des tests

S1 est un état dans lequel la variable '0' vaut 1 et la variable '1' vaut 2 et toutes les autres '0' (valeur par défaut) Une variable (Ava i) étant représentée par un entier naturel i, sa valeur dans l'état est la valeur de la ieme position de la liste

Definition state := list nat.

Definition S1 := [1; 2].
Definition S2 := [0; 3].
Definition S3 := [0; 7; 5; 41].

Sémantique

On reprend les sémantiques fonctionnelles des expressions artihmétiques et booléennes
La fonction get x s rend la valeur de x dans s. Elle rend 0 par défaut, par exemple si la variable n'est pas définie/initialisée

Fixpoint get (x:nat) (s:state) : nat :=
match x,s with
| 0 , v::_ ⇒ v
| S x1, _::l1 ⇒ get x1 l1
| _ , _ ⇒ 0
end.

Exemples

Compute (get 0 S3).
Compute (get 1 S3).
Compute (get 2 S3).
Compute (get 3 S3).
Compute (get 4 S3).

La mise à jour d'une variable v par un nouvel entier n dans un état s s'écrit 'update s v n' Cette fonction n'échoue jamais et écrit la valeur à sa place même si elle n'est pas encore définie dans l'état

Fixpoint update (s:state) (v:nat) (n:nat): state :=
match v,s with
| 0 , a :: l1 ⇒ n :: l1
| 0 , nil ⇒ n :: nil
| S v1, a :: l1 ⇒ a :: (update l1 v1 n)
| S v1, nil ⇒ 0 :: (update nil v1 n) end.

Definition S4 := update (update (update (update (update S1 4 1) 3 2) 2 3) 1 4) 0 5.

Compute S1.
Compute S4.

Sémantique fonctionnelle de aexp

Fixpoint evalA (a: aexp) (s: state) : nat :=
  match a with
  | Aco n ⇒ n
  | Ava x ⇒ get x s
  | Apl a1 a2 ⇒ evalA a1 s + evalA a2 s
  | Amu a1 a2 ⇒ evalA a1 s × evalA a2 s
  | Amo a1 a2 ⇒ evalA a1 s - evalA a2 s
  end.

Sémantique fonctionnelle de bexp


Definition eqboolb b1 b2 : bool :=
  match b1, b2 with
  | true , true ⇒ true
  | false, false ⇒ true
  | _ , _ ⇒ false
  end.

Fixpoint eqnatb n1 n2 : bool :=
  match n1, n2 with
  | O , O ⇒ true
  | S n1', S n2' ⇒ eqnatb n1' n2'
  | _ , _ ⇒ false
  end.

Fixpoint evalB (b : bexp) (s : state) : bool :=
  match b with
  | Btrue ⇒ true
  | Bfalse ⇒ false
  | Bnot b ⇒ negb (evalB b s)
  | Band e1 e2 ⇒ (evalB e1 s) && (evalB e2 s)
  | Bor e1 e2 ⇒ (evalB e1 s) || (evalB e2 s)
  | Beq e1 e2 ⇒ eqboolb (evalB e1 s) (evalB e2 s)
  | Beqnat n1 n2 ⇒ eqnatb (evalA n1 s) (evalA n2 s)
  end.

Pour définir plus facilement des expressions de test on prédéfinit des constantes entières ...

Definition N0 := Aco 0.
Definition N1 := Aco 1.
Definition N2 := Aco 2.
Definition N3 := Aco 3.
Definition N4 := Aco 4.

... et des variables

Definition X := Ava 1.
Definition Y := Ava 2.
Definition Z := Ava 3.

Quelques expressions arithmétiques pour tester
exp1 = x + 3
Definition E1 := Apl X N3.

exp2 = y - 1
Definition E2 := Amo Y N1.

exp3 = (x + y) * 2
Definition E3 := Amu (Apl X Y) N2.

Compute (evalA E1 S1).
Compute (evalA E1 S2).
Compute (evalA E2 S1).
Compute (evalA E2 S2).
Compute (evalA E3 S1).
Compute (evalA E3 S2).

Quelques expressions booléennes pour tester
B1 := exp1 = 4
Definition B1 := Beqnat E1 N4.

B2 := not ( bexp1 /\ (exp1 = 7)
Definition B2 := Bnot (Band B1 (Beqnat X N2)).

Compute (evalB B1 S1).
Compute (evalB B1 S2).
Compute (evalB B2 S1).
Compute (evalB B2 S2).

Version relationnelle, appelée "sémantique naturelle"

Vu dans le CM précédent. La sémantique naturelle (ou sémantique opérationnelle à grands pas) du langage WHILE est donnée sous la forme d'un prédicat inductif.

Inductive SN : winstr → state → state → Prop :=
| SN_Skip : ∀ s,
                   SN Skip s s
| SN_Assign : ∀ x a s,
                   SN (Assign x a) s (update s x (evalA a s))
| SN_Seq : ∀ i1 i2 s s1 s2,
                   SN i1 s s1 → SN i2 s1 s2 → SN (Seq i1 i2) s s2
| SN_If_true : ∀ b i1 i2 s s1,
                   (evalB b s = true) → SN i1 s s1 → SN (If b i1 i2) s s1
| SN_If_false : ∀ b i1 i2 s s2,
                   (evalB b s = false) → SN i2 s s2 → SN (If b i1 i2) s s2
| SN_While_false : ∀ b i s,
                   (evalB b s = false) → SN (While b i) s s
| SN_While_true : ∀ b i s s1 s2,
                   (evalB b s = true) → SN i s s1 → SN (While b i) s1 s2 →
                   SN (While b i) s s2
.

On code dans WHILE un programme P1 correspondant à while not (i=0) do {i:=i-1;x:=1+x}
Definition Il := 0.
Definition Ir := Ava Il.
Definition Xl := 1.
Definition Xr := Ava Xl.

Definition corps_boucle := Seq (Assign Il (Amo Ir N1)) (Assign Xl (Apl N1 Xr)).
Definition P1 := While (Bnot (Beqnat Ir N0)) corps_boucle.

On montre que P1 transforme l'état S1 en l'état S2

Theorem reduction1 : SN P1 S1 S2.
Regarder les états courants tout au long de la preuve
Proof.
  cbv [P1]. cbv [S1]. cbv [S2].
Ou de façon équivalente : unfold P1. unfold S1. unfold S2.
Ce but devrait être prouvé par l'une des deux dernières règles de SN, qui portent sur le cas While. On peut deviner laquelle de tête, ou demander de l'aide ainsi :
  Compute (evalB (Bnot (Beqnat Ir N0)) [1; 2]).
Ce sera donc avec SN_While_true. On peut essayer d'avancer avec 'apply SN_While_true.' ... mais ça échoue. Ici Coq ne peut pas deviner ce que sera l'état intermédiaire s1.
  Fail apply SN_While_true.
Une stratégie possible serait d'indiquer directement l'état intermédiaire avec la variante 'apply ... with (s1:= ...)'. Il faut deviner les paramètres corrects ce qui n'est pas toujours facile. Dans notre cas cela serait :
  apply SN_While_true with (s1:=[0;3]).
On va donc proposer une autre stratégie·
  Undo 1.
Une première possibilité est avec refine, déjà connu : ici on indique un joker '_' pour chacun des HUIT arguments ; b, i, s et s2 se trouvent déterminés par la forme du but, s1 sera déterminé par la preuve de SN s i s s1 et ne donne donc pas lieu à un sous-but. Il restera à prouver : evalB b s = true, SN i s s1 et SN (While b i) s1 s2.
  refine (SN_While_true _ _ _ _ _ _ _ _).
On obtient le même effet avec la tactique eapply, plus commode.
  Undo 1.
  eapply SN_While_true.
  - reflexivity.
  - cbv [corps_boucle].
Un nouvel état intermédiaire est à deviner
    eapply SN_Seq.
    + apply SN_Assign.
    +
      cbn [evalA Ir Il N1 get minus update].
Ou, plus rapidement
      Undo 1.
      cbn.
      apply SN_Assign.
  - cbn.
SN_While_true ou SN_While_false ?
    Compute (evalB (Bnot (Beqnat Ir N0)) [0; 3]).
    apply SN_While_false.
    cbn.
    reflexivity.
Qed.

ICI 1 : présenter reduction1 sous forme d'arbre


Une autre présentation de ce script, structurée par accolades. Cela permet de gérer l'indentation autrement (surtout utile quand le corps de boucle s'exécute plusieurs fois.
Theorem reduction1_accolades : SN P1 S1 S2.
Proof.
  cbv [P1]. cbv [S1]. cbv [S2].
  eapply SN_While_true.
  { cbn. reflexivity. }
  { cbv [corps_boucle].
    eapply SN_Seq.
    + apply SN_Assign.
    + cbn. apply SN_Assign. }
  cbn.
  Compute (evalB (Bnot (Beqnat Ir N0)) [0; 3]).
  apply SN_While_false.
  cbn. reflexivity.
Qed.

Preuve par récurrence structurelle dans un prédicat inductif

Transformation simple de programme :
  • if true then X else Y ---> X
  • if false then X else Y ---> Y
Fixpoint simpl_test_Btrue_Bfalse (i: winstr) : winstr :=
  match i with
  | Skip ⇒ Skip
  | Assign v a ⇒ i
  | Seq w1 w2 ⇒ Seq (simpl_test_Btrue_Bfalse w1)
                     (simpl_test_Btrue_Bfalse w2)
  | If Btrue i1 i2 ⇒ simpl_test_Btrue_Bfalse i1
  | If Bfalse i1 i2 ⇒
     simpl_test_Btrue_Bfalse i2
  | If b i1 i2 ⇒ If b (simpl_test_Btrue_Bfalse i1)
                       (simpl_test_Btrue_Bfalse i2)
  | While b i ⇒ While b (simpl_test_Btrue_Bfalse i)
  end.

Lemma discrim_bool :
  ∀ {X: Set}, ∀ x y: X, false = true → x = y.
Proof.
  intros X x y e.
  pose (f (b:bool) := if b then y else x).
  change (f false = f true). f_equal. apply e.
Qed.

ICI 2 - Combinaisons de tactiques
Theorem simpl_test_Btrue_Bfalse_correct :
  ∀ i s s', SN i s s' → SN (simpl_test_Btrue_Bfalse i) s s'.
Proof.
  intros i s s' sn.
  induction sn as [ s
                   | x s a
                   | i1 i2 s1 s2 s' sn1 hrec_sn1 sn2 hrec_sn2
                   | cond i1 i2 s s' e sn hrec_sn
                   | cond i1 i2 s s' e sn hrec_sn
                   | cond i s e
                   |
                     cond i s0 s1 s' e sn hrec_sn sni hrec_sni
                   ]; cbn [simpl_test_Btrue_Bfalse].

  - apply SN_Skip.
  - apply SN_Assign.
  - apply SN_Seq with s2.
    + apply hrec_sn1.
    + apply hrec_sn2.
  - destruct cond as [ | | | | | | ].
    + apply hrec_sn.
    + cbn in e. Check (discrim_bool i2 i1 e).
      rewrite (discrim_bool i2 i1 e). apply hrec_sn.
    + apply SN_If_true.
      × apply e.
      × apply hrec_sn.
Même chose pour ce cas "+" en un coup.
      Undo 6.
    + apply SN_If_true; [apply e | apply hrec_sn].
Résolution de la plupart des sous-buts créés par "- destruct cond"
    Undo 10.
  - destruct cond as [ | | | | | | ];
      try (apply SN_If_true; [apply e | apply hrec_sn]).
Il reste les deux sous-buts les plus intéressants.
    + apply hrec_sn.
    + rewrite (discrim_bool i2 i1 e). apply hrec_sn.
   - destruct cond as [ | | | | | | ];
      try (apply SN_If_false; [apply e | apply hrec_sn]).
     + rewrite (discrim_bool i1 i2).
       × apply hrec_sn.
       × symmetry. apply e.
    + apply hrec_sn.
  - apply SN_While_false. apply e.
  - apply SN_While_true with s1.
    + apply e.
    + apply hrec_sn.
    + apply hrec_sni.
Qed.

Interlude sur l'inversion

Il convient de lire d'abord l'introduction dans coq9_inversion.v
Dans l'exercice qui suit, on aura un but comprenant une hypothèse de la forme SN i s s2, où i est lui-même de la forme Seq i1 i2 (1). Sans la condition (1), il serait naturel de procéder par cas sur i, ce qui donnerait lieu aux 7 cas ; mais avec la condition (1), on voit que seul un cas est pertinent, correpondant à SN_Seq. Cette technique de preuve est dite "par inversion". On va se rameer à une situation plus simple au moyen du prédicat ad-hoc suivant, qui isole le cas intéressant de SN.

Inductive SN1_Skip: state → state → Prop :=
| SN_Skip' : ∀ s,
                    SN1_Skip s s
.
Inductive SN1_Assign (v: nat) (a: aexp) : state → state → Prop :=
| SN_Assign' : ∀ s,
                    SN1_Assign v a s (update s v (evalA a s))
.
Inductive SN1_Seq i1 i2 : state → state → Prop :=
| SN_Seq' : ∀ s s1 s2,
                    SN i1 s s1 → SN i2 s1 s2 → SN1_Seq i1 i2 s s2
.
Inductive SN1_If (b: bexp) (i1 i2: winstr): state → state → Prop :=
| SN_If_true' : ∀ s s1,
                    (evalB b s = true) → SN i1 s s1 → SN1_If b i1 i2 s s1
| SN_If_false' : ∀ s s2,
                    (evalB b s = false) → SN i2 s s2 → SN1_If b i1 i2 s s2
.
Inductive SN1_While (b: bexp) (i: winstr): state → state → Prop :=
| SN_While_false' : ∀ s,
                    (evalB b s = false) → SN1_While b i s s
| SN_While_true' : ∀ s s1 s2,
                    (evalB b s = true) → SN i s s1 → SN (While b i) s1 s2 →
                    SN1_While b i s s2.

Definition dispatch (i: winstr) : state → state → Prop :=
  match i with
  | Skip ⇒ SN1_Skip
  | Assign v a ⇒ SN1_Assign v a
  | Seq i1 i2 ⇒ SN1_Seq i1 i2
  | If b i1 i2 ⇒ SN1_If b i1 i2
  | While b i ⇒ SN1_While b i
  end.

Definition SN_inv {i s s2} (sn : SN i s s2) : dispatch i s s2 :=
  match sn with
  | SN_Skip s ⇒ SN_Skip' s
  | SN_Assign v a s ⇒ SN_Assign' v a s
  | SN_Seq i1 i2 s s1 s2 sn1 sn2 ⇒ SN_Seq' i1 i2 s s1 s2 sn1 sn2
  | SN_If_true b i1 i2 s s1 btr sn ⇒ SN_If_true' b i1 i2 s s1 btr sn
  | SN_If_false b i1 i2 s s1 bfa sn ⇒ SN_If_false' b i1 i2 s s1 bfa sn
  | SN_While_false b i s bfa ⇒ SN_While_false' b i s bfa
  | SN_While_true b i s s1 s2 btr sn1 sn2 ⇒ SN_While_true' b i s s1 s2 btr sn1 sn2
  end.

Definition SN_inv' {i s s2} (sn : SN i s s2) : dispatch i s s2.
  destruct sn; econstructor; eassumption.
Defined.

Illustration

Une autre manière d'exprimer la sémantique de WHILE ; on prouvera que SN et SN' sont équivalentes.
Inductive SN': winstr → state → state → Prop :=
| SN'_Skip : ∀ s,
                    SN' Skip s s
| SN'_Assign : ∀ x a s,
                    SN' (Assign x a) s (update s x (evalA a s))
| SN'_Seq : ∀ i1 i2 s s1 s2,
                    SN' i1 s s1 → SN' i2 s1 s2 → SN' (Seq i1 i2) s s2
| SN'_If_true : ∀ b i1 i2 s s1,
                    (evalB b s = true) → SN' i1 s s1 → SN' (If b i1 i2) s s1
| SN'_If_false : ∀ b i1 i2 s s2,
                    (evalB b s = false) → SN' i2 s s2 → SN' (If b i1 i2) s s2
| SN'_While_false : ∀ b i s,
                    (evalB b s = false) → SN' (While b i) s s
| SN'_While_true : ∀ b i s s1,
                    (evalB b s = true) → SN' (Seq i (While b i)) s s1 →
                    SN' (While b i) s s1
.

La direction suivante ne pose pas de nouvelle difficulté
Lemma SN_SN' : ∀ i s s1, SN i s s1 → SN' i s s1.
Proof.
  intros i s s1 sn.
  induction sn as [ s
                   | x s a
                   | i1 i2 s1 s2 s' sn1 hrec_sn1 sn2 hrec_sn2
                   | cond i1 i2 s s' e sn hrec_sn
                   | cond i1 i2 s s' e sn hrec_sn
                   | cond i s e
                   |
                     cond i s0 s1 s' e sn hrec_sn sni hrec_sni
                   ].
  - apply SN'_Skip.
  - apply SN'_Assign.
  - apply (SN'_Seq _ _ _ _ _ hrec_sn1 hrec_sn2).
  - apply SN'_If_true.
    + apply e.
    + apply hrec_sn.
  - apply (SN'_If_false _ _ _ _ _ e hrec_sn).
  - apply SN'_While_false. apply e.
  - apply SN'_While_true.
    + apply e.
    + eapply SN'_Seq.
      -- apply hrec_sn.
      -- apply hrec_sni.
Qed.

Pour la réciproque le script est semblable SAUF au dernier sous-but, qui précisément demande une inversion.
Lemma SN'_SN : ∀ i s s1, SN' i s s1 → SN i s s1.
Proof.
  intros i s s1 sn'.
  induction sn' as [ s
                   | x s a
                   | i1 i2 s1 s2 s' sn1 hrec_sn1 sn2 hrec_sn2
                   | cond i1 i2 s s' e sn hrec_sn
                   | cond i1 i2 s s' e sn hrec_sn
                   | cond i s e
                   |
                     cond i s0 s2 e sn hrec_sn
                   ].
  - apply SN_Skip.
  - apply SN_Assign.
  - apply (SN_Seq _ _ _ _ _ hrec_sn1 hrec_sn2).
  - apply SN_If_true.
    + apply e.
    + apply hrec_sn.
  - apply (SN_If_false _ _ _ _ _ e hrec_sn).
  - apply SN_While_false. apply e.
  -
Ici il faut exploiter l'hypothèse hrec_sn : SN (Seq i (While cond i)) s0 s2 On observe que cette hypothèse est de la forme SN (Seq i1 i2) s0 s2 qui est un cas particulier de SN i s0 s2 ; cependant un destruct de hrec_sn oublierait que l'on est dans ce cas particulier
    destruct hrec_sn as [ | | | | | | ].
    +
Le but obtenu ici correspond au cas où Seq i (While cond i) serait en même temps Skip un cas qui est hors propos.
      Undo 1.
    Undo 1.
Cela est résolu en utilisant conséquence de hrec_sn indiquée par inv_Seq. Voir le mode d'emploi indiqué ci-dessus.
    destruct (SN_inv hrec_sn) as [s0 s1 s2 sn1 sn2].
On termine en utilisant ici SN_While_true
    + eapply SN_While_true.
      -- apply e.
      -- apply sn1.
      -- apply sn2.
Qed.

Le langage REPEAT

On considère maintenant un langage impératif sans la commande While, mais comportant une autre instruction de boucle 'repeat i until b qui exécute i puis sort si b est vrai, et sinon recommence.
Voici la syntaxe du langage REPEAT (on redéfinit un nouveau type avec de nouveaux constructeurs.

Inductive rinstr :=
| RSkip : rinstr
| RAssign : nat → aexp → rinstr
| RSeq : rinstr → rinstr → rinstr
| RIf : bexp → rinstr → rinstr → rinstr
| Repeat : rinstr → bexp → rinstr.

Définir la sémantique naturelle du REPEAT

Inductive SNr: rinstr → state → state → Prop :=
| SNr_Skip : ∀ s,
                    SNr RSkip s s
| SNr_Assign : ∀ x e s,
                    SNr (RAssign x e) s (update s x (evalA e s))
| SNr_Seq : ∀ i1 i2 s s1 s2,
                    SNr i1 s s1 → SNr i2 s1 s2 → SNr (RSeq i1 i2) s s2
| SNr_If_true : ∀ b i1 i2 s s1,
                    evalB b s = true → SNr i1 s s1 → SNr (RIf b i1 i2) s s1
| SNr_If_false : ∀ b i1 i2 s s2,
                    evalB b s = false → SNr i2 s s2 → SNr (RIf b i1 i2) s s2
| SNr_Repeat_true : ∀ i b s s1,
                    SNr i s s1 → evalB b s1 = true → SNr (Repeat i b) s s1
| SNr_Repeat_false: ∀ i b s s1 s2,
                    SNr i s s1 → evalB b s1 = false → SNr (Repeat i b) s1 s2 →
                    SNr (Repeat i b) s s2
.

On code dans REPEAT un programme P2 correspondant à repeat {i:=i-1;x:=1+x} until i=0

Definition corps_boucleR : rinstr :=
  RSeq (RAssign Il (Amo Ir N1)) (RAssign Xl (Apl N1 Xr)).
Definition P2 := Repeat corps_boucleR (Beqnat Ir N0).