===== Rappels Coq =====

==== Prédicats inductifs ====


  ?? Prédicat :: une fonction dans bool. En Coq on a ''bool'' et ''Prop''. 

__Exemple : parité__
  Inductive even:nat -> Prop:=
  | even_0: even 0
  | even_SS: forall m:nat, even m -> even(S(Sm))
  
  Definition even n:= div2 n = div2(Sn)

!!

Une autre façon de définir ''even'' (croisée avec odd):

  Inductive even:nat -> Prop:=
  | even_0 : even 0
  | even_S : forall n, odd n -> even(Sn).
  with odd:nat -> Prop:=
  | odd_S : forall n, even n -> odd(Sn)
  | odd_1 : odd S0.


=== La Relation "≤" ===

  Definition le (n m:nat) Prop:= exists p:nat, m=n+p.
  
  Inductive le (n:nat) :nat->Prop:=
  | le_n: le n n   (* n ≤ n *)
  | le_S: forall m:nat, le n m -> le n (Sm).
  
==== De la sémantique des langages de programmation aux obligations de preuve. ====

> Pour prouver les programmes, il faut définir la sémantique du langage.

=== Références Bibliographiques ===
  * Glynn Winskel, //"The formal semantics of programming languages,"// The MIT Press, 1993. ISBN-13: 978-0262731034.
  * Tobias Nipkow, //"[[http://www4.informatik.tu-muenchen.de/~nipkow/pubs/fac98.html|Winskel is (almost) Right: Toward a Mechanized Semantics Textbook]]."//
    * @article{Nipkow-FAC98,author={Tobias Nipkow}, title={Winskel is (almost) Right: Towards a Mechanized Semantics Textbook}, journal={Formal Aspects of Computing},volume=10,pages={171--186},year=1998}
  * Yves Bertot, //"[[http://arxiv.org/abs/0707.0926|Theorem poving support in programming language semantics]]."//

=== Types de sémantique ===

  ?? opérationnelle :: un programme est vu et décrit comme une succession d'états !!
  ?? dénotationnelle  :: un programme est vu et décrit comme un fonction, c'est à dire une transformation d'une entrée en un résultat !!
  ?? axiomatique  :: un programme est vu et décrit comme un transformateur de propriété(s) !!

=== Quelques propriétés des langages de programmation ===

  * déterminisme : fait toujours la même chose sur la même entrée.
  * préservation du typage : le calcul ne change pas le type \\   P:T  \\ <jsm>P \sim\!\!> P'  \quad \rightarrow P':T</jsm>

=== Notre cadre : mini-langage ===

|  e  |  ::=  | n %%|%%  x  %%|%% e + e | (* expressions arithmétiques  *) |
|  b  |  ::=  | e < e  | (* expressions booléennes  *)  |
|  i  |  ::=  | skip %%|%%  x:= e  %%|%%  i;i  %%|%% ''while b do i done''  | (* instructions, dont affectation, séquence, boucle *) |

  Inductive aexpr:Type :=
  | Avar: string -> aexpr
  | Anum: Z -> aexpr
  | Aplus: aexpr -> aexpr -> aexpr.
  
Sémantique opérationnelle
  * à grands pas (sémantique naturelle)
  * à petits pas (sémantique opérationnelle standard, ou SOS)

  ?? Environnement :: modèle théorique de la mémoire. => liste de paires associant à chaque variable sa valeur. En Coq, ''Definition env:= list(string*Z).'' !!
  ?? Jugements  :: pour les expressions, les jugements sont de la forme <jsm>E \vdash e \rightarrow v </jsm> !!



==== Règles pour jugements ====

^ Hyp. |  //rien en haut : axiome // |
^ Déduction |  <jsm>E \vdash n \rightarrow n </jsm> |

^ Hyp. |  |
^ Déd. |  |

^ Hyp. |  |
^ Déd. |  |

^ Hyp. |  |
^ Déd. |  |

^ Hyp. |  |
^ Déd. |  |








==== Jugements en coq ====

  Definition env := list (string * Z).
  
  Inductive aeval: env -> aexpr -> Z -> Prop :=
  | Aeint: forall E n, aeval E (Anum n) n
  | Aeplus: forall E e1 e2 n1 n2, aeval E e1 n1 -> aeval E e2 n2 -> aeval E (Aplus e1 e2) (n1 +n2)
  | Aevar1: forall E x n, aeval((x,n)::E) (Avar x) n
  | Aevar2: forall E x y n m, aeval E (Avar x) n -> x<>y -> aeval((y, n)::E) (Avar x) m.
  


==== Jugements pour les instructions ====
 
<jsm>E \vdash i \tilde \rightarrow E' </jsm>


FIXME à completer

  * suite : [[coq_3|]] 
  * projet [[coq_projet|]]
  * TP [[coq_tp|]]