coq6_While_SN.v

P1 = "while not (i=0) do {i := i-1; x := 1+x}".

Theorem reduction1 : SN P1 S1 S2.

On utilise les conversions :

• update [0; 2] "x" (evalA "1+x" [0; 2]) = [0; 3]

          ------------------------- SN:=    ------------------------- SN:= "x" "1+x" [0, 2]
          SN "i:=i-1" [1; 2] [0; 2]         SN "x:=1+x" [0; 2] [0; 3]
          ----------------------------------------------------------- SN_Seq
                            SN corps [1; 2] [0; 3]
                                          \
                                           \
                                            \                   --------------------------- =refl
                                             \                  evalB "i<>0" [0; 3] = false
-------------------------- =refl    ......................      --------------------------- SN_While_false
evalB "i<>0" [1; 2] = true          SN corps [1; 2] [0; 3]         SN P1 [0; 3] [0; 3]
-------------------------------------------------------------------------------------- SN_While_true _ _ _ _ _
                                    SN P1 [1; 2] [0; 3]

Theorem simpl_test_Btrue_Bfalse_correct :
  forall i s s', SN i s s' -> SN (simpl_test_Btrue_Bfalse i) s s'.

  intros i s s' sn.
  induction sn as  [ (* SN_Skip *) s
                   | (* SN_Assign *) x s a
                   | (* SN_Seq *) i1 i2 s1 s2 s' sn1 hrec_sn1 sn2 hrec_sn2
                   | (* SN_If_true *) cond i1 i2 s s' e sn hrec_sn
                   | (* SN_If_false *) cond i1 i2 s s' e sn hrec_sn
                   | (* SN_While_false *)  cond i s e
                   | (* SN_While_true *)
                     cond i s0 s1 s' e sn hrec_sn sni hrec_sni

coq8_SN_props.v

coq8_SN_props_debut.v coq8_SN_props.v

Il s'agit d'exploiter une égalité en hypothèse, entre deux expressions formées par des constructeurs différents cons1 et cons2.

e : cons1 ... = cons2 ...
...
-------------------------
conclusion

On a vu une technique pour résoudre un tel but, sous le nom "d'égalités contagieuses" ou "super-contagieuses" : quelle que soit la conclusion, elle peut être prouvée à partir de e.

Cette technique demande un peu de préparation. Pour plus de facilité, la tactique discriminate de Coq fait ce travail automatiquement.

coq9_inversion.v

Soit rel une relation définie inductivement

(Inductive rel ... : Prop := ... )

ayant par exemple 3 paramètres.

Si un but comporte une hypothèse pour rel

hyp : rel x y z
...
---------------
conclusion

on a souvent deux situations typiques :

1. celle où tous les paramètres x y z sont des variables
2. celle où au moins un paramètre est formé par un constructeur (s'il est de type nat, ce sera par exemple 0 ou (S …))

Dans la situation 1), le raisonnement par cas (destruct) ou par récurrence (induction) sur hyp est efficace.

Dans la situation 2), l'information indiquant qu'à une position donnée le paramètre a telle forme est perdue. Pour plus d'explications, voir cours07_inversion.v. Il faut alors une utilisation plus subtile de destruct, qui peut être invoquée au moyen de la tactique inversion de Coq.

Pour une compréhension plus fine, et notamment obtenir un résultat équivalent, plus satisfaisant mais qui demande un travail préparatoire, voir les fichiers Coq associés à ce cours.

coq9_inversion.v et coq8_SN_props_debut.v puis coq8_SN_props.v

Les informations procurées par l'exploitation d'une hypothèse (c'est notamment les cas d'un inversion) doivent être mises dans le contexte et partagées AVANT la création de sous-buts par eapply.