[Coq-Club] formalisation de la logique propositionnelle / introduction to conversational Martian

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 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 implicatif 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.

Interpretation 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 propositionnel 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 fonctions 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 systeme 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