The Coq mailing list

[aymen bouslama <aymen.bouslama AT googlemail.com>]

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 modeliser le fragment im-

plicatif de la logique propositionnelle. Les termes seront soit des variables, notees a, b, c, etc.

(prises dans un ensemble V ), soit une implication entre deux termes.

On pourra utiliser la bibliotheque String de Coq pour gerer les noms des propositions.

Interpretation On propose de representer une valuation par une liste de paires (variable,booleen).

Definition valuation := list (string * bool).

Ecrire une fonction list assoc qui, etant donnee 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'interpretation qui, etant donne une formule F et

une valuation I, calcule si I satisfait F , i.e. I(F ) = true.

Tables de verite 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 verite.

Indication : on pourra enumerer toutes les valuations possibles. Il sura ensuite de tester

que la formule est satisfaite pour toutes ces valuations. On pourra pour cela utiliser les fonc-

tions d'ordre superieurs sur les listes (par exemple forallb). Pour l'implication (2 variables), le

nombre de cas a etudier pour determiner si on a a faire a une tautologie est 4.

Utiliser votre fonction pour veri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