The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Bonjour

J'espère que vous êtes conscient que l'enseignant qui vous a donné ce
projet a toutes les chances de lire cette mailing liste, et qu'il
n'est pas évident qu'il considère que faire corriger/compléter votre
réponse soit exactement le travail qu'il attendait de vous.

J'espère aussi que vous penserez, avant de rendre votre projet, à
supprimer le nom de votre camarade Samuel Besset, et à le remplacer
par le votre. Cela risquerait de d'éveiller des soupçons de triche. Ce
serait malheureux.

Cordialement,

Alexandre Pilkiewicz

Le 21 avril 2011 11:46, aymen bouslama 
<aymen.bouslama AT googlemail.com>
 a écrit :
> bonjour,
> est ce que vous pouvez me dire si c'est juste ce que j'ai fais pour résoudre
> le problème suivant?
> Construire un type inductif a deux constructeurs permettant de mod eliser le
> fragment im-
> plicatif de la logique propositionnelle. Les termes seront soit des
> variables, not ees a, b, c, etc.
> (prises dans un ensemble V ), soit une implication entre deux termes.
> On pourra utiliser la biblioth eque String de Coq pour g erer les noms des
> propositions.
> Interpr etation On propose de repr esenter une valuation par une liste de
> paires (variable,bool een).
> Definition valuation := list (string * bool).
> Ecrire une fonction list assoc qui, etant donn ee une variable
> propositionnelle et une valuation
> V donne la valeur de la variable dans la valuation. Ex : si
> V=[("x",true);("y", false)]  list_assoc V y=false.
>  Ecrire une fonction d'interpr etation qui, etant donn e une formule F et
> une valuation I, calcule si I satisfait F , i.e. I(F ) = true.
> Tables de v erit e Programmer une fonction qui prend en argument un terme du
> calcul propo-sitionnel et calcule s'il s'agit d'une tautologie ou non en
> utilisant
> une table de v erit e.
> Indication : on pourra enum erer toutes les valuations possibles. Il su ra
> ensuite de tester
> que la formule est satisfaite pour toutes ces valuations. On pourra pour
> cela utiliser les fonc-
> tions d'ordre sup erieurs sur les listes (par exemple forallb). Pour
> l'implication (2 variables), le
> nombre de cas a etudier pour d eterminer si on a a faire a une tautologie
> est 4.
> Utiliser votre fonction pour v eri er que les termes suivants sont bien des
> tautologies.
> { Pierce : ((A -> B) ->A) ->A
> { S : F ->(G -> F )
> { K : (F -> (G -> H)) -> ((F -> G) -> (F -> H))
> -------------------------------
>
>
> (*---------------------------------------------------------------------------------*)
> (*------------------------------ PROJET COQ M1 ILC
> --------------------------------*)
> (*------------------------------ BESSET SAMUEL
> --------------------------------*)
> (*---------------------------------------------------------------------------------*)
> Require Export List.
> Require Export String.
> Require Export Bool.
> Open Local Scope char_scope.
> (*---------------------------------------------------------------------------------*)
> (* Formaliser la syntaxe et sémantique et modéliser un système de déduction
>        *)
> (*---------------------------------------------------------------------------------*)
>
>
> (*---------------------------------------------------------------------------------*)
> (*
> SYNTAXE *)
> (*---------------------------------------------------------------------------------*)
>
> (* Définition inductive du type : form *)
> Inductive form : Set :=
>  | p : string -> form           (* proposition *)
>  | i : form -> form -> form     (* implication *)
>  | e : form -> form -> form     (* ET logique  *)
>  | o : form -> form -> form     (* OU logique  *)
>  .
>
> (*---------------------------------------------------------------------------------*)
> (*
>  SEMANTIQUE *)
> (*---------------------------------------------------------------------------------*)
>
> (* Définition de la valuation *)
> Definition valuation := list (string * bool).
>
> (* Définition de la fonction : list_assoc *)
> Fixpoint list_assoc a (v:valuation) : bool :=
>  match v with
>  | nil        => false
>  | (x,b) :: l =>
>                  if    string_dec x a then b
>                  else                      list_assoc a l
>  end.
>
>
> (* Définition de la fonction : interpretation *)
> Fixpoint interpretation form (v:valuation) : bool :=
>  match form with
>  | p s1           => list_assoc s1 v
>  | i form1 form2  => (orb (negb (interpretation form1 v)) (interpretation
> form2 v))
>  | e form1 form2  => (andb (interpretation form1 v) (interpretation form2
> v))
>  | o form1 form2  => (orb (interpretation form1 v) (interpretation form2 v))
>  end.
>
> (*---------------------------------------------------------------------------------*)
> (*                                                               TEST -
> SEMANTIQUE *)
> (*---------------------------------------------------------------------------------*)
>
> (* Tests des définitions précédentes : *)
> Definition a      := (String "A" EmptyString).
> Definition b      := (String "B" EmptyString).
> Definition val    := (a,true)::(b,false)::nil.
>
> Eval compute in (interpretation (p a) val). (* doit rendre : true *)
> Eval compute in (interpretation (p b) val). (* doit rendre : false *)
> après avez vous une idée pour la suite?
> Syst eme formel
> On rappelle les r egles de la d eduction naturelle : comme elim et intro
> On d eclare un contexte (comme ) comme une liste de formules.
> Definition context := list formule.
> 1. Mod eliser le syst eme formel pr ec edent a travers un type inductif de
> la forme :
> Inductive prouvable : context -> formule -> Prop := ...
> 2. Prouver ensuite le th eor eme A -> A dans ce syst eme.
> 3. Faire de m^eme avec les th eor emes S et K de la section pr ec edente.
> 4. On va maintenant s'int eresser a la preuve de la correction de ce syst
> eme formel.
> (a) D e nir un pr edicat consequence_l qui prend en argument un contexte et
> une
> formule F et indique si F est cons equence s emantique de .
> (b) Prouver le th eor eme suivant :
> Lemma correctness : forall P G,
> provable G P ->
> consequence_l G P.
>
> merci
> Cordialement