UP | HOME

TP 1 - Définitions inductives, principes inductifs, logique

Table of Contents

(Correction partielle dans le dépôt Git : fichier src/corrections/tp1.v.)

Quelques définitions inductives

  • On placera les définitions qui suivent dans un module pour en limiter la portée.

    Module SystemeInference.
      ...
    End SystemeInference.
    
  • Définir avec Coq les définitions inductives présentées dans le cours.

    Formules

    		   p : Formule  q : Formule
    ----------------   -------------------------  
      V : Formule          p ∨ q : Formule
    

    Listes

    			  (t : T)    (r : Liste T) 
    ------------------       --------------------------
     vide T : Liste T          cons T t r : Liste T
    

    Calcul des séquents exprimant leur validité (extrait)

    ------------ [Id]
       p ⊢ p
    
       Γ ⊢ Δ           
    ------------ [V-G]           ----- [V-D]   
      V, Γ ⊢ Δ                    ⊢ V
    
    				Γ ⊢ p, Δ
    			    ---------------- [∨-Dg]   
    p, Γ ⊢ Δ   q, Γ ⊢ Δ          Γ ⊢ (p ∨ q), Δ
    ------------------- [∨-G]
      (p ∨ q), Γ ⊢ Δ                Γ ⊢ q, Δ
    			    ---------------- [∨-Dd]   
    			     Γ ⊢ (p ∨ q), Δ
    
  • Lesquelles sont paramétrées ? indexées ?
  • Introduire les notations suivantes.
    • ou logique (∨) : \/
    • liste vide : []
    • liste construite : t::r
    • liste singleton : [e]
    • liste comme énumération : [ x ; y ; .. ; z ] (on utilise deux points .. pour marquer l'énumération
    • déduction ⊢ : |-
  • Donner les principes inductifs et récursifs des listes. Comparer avec les types Liste_ind et Liste_rec.
  • Prouver le lemme d'affaiblissement suivant : pour toutes formules p et q, on a : *p ⊢ p ∨ q.

    Lemma affaiblissement : forall p q, [p] |- [p \/ q].
    Proof.
      intros p q. (* Destruction du forall, ajout des hypothèses (p : nat) et (q : nat) *)
      (* Appliquer les bonnes règles en utilisant les tactiques 
         - apply constructeur.
      *)
    Qed. (* Quid est demonstratum. *)
    

Logique

Le but de cette seconde partie est de ré-implémenter des opérateurs logiques existants en utilisant des définitions inductives. En Coq, les propositions logiques, qui correspondent à des types, appartiennent elles-mêmes à un type, la sorte Prop. Préalable : lire le cours dédié à la logique et décrivant différents systèmes d'inférence utilisés pour démontrer. Dans la suite du TP, c'est le calcul des séquents qui est utilisé. On utilisera aussi uniquement des définitions inductives paramétrées et non indexées.

  • Comme précédemment, on placera les définitions qui suivent dans un module.

    Module Logique.
      ...
    End Logique.
    
  • Définir la proposition Faux : Prop. Elle est définie inductivement par un système d'inférence vide.
  • Définir la proposition Vrai : Prop ainsi.

    -------- [vrai] 
      Vrai
    
  • Définir l'alternative logique ainsi.

         P                   Q
    ----------- [ouG]   ----------- [ouD]  
     (Ou P Q)            (Ou P Q)
    

    On utilisera un système d'inférence paramétré, définissant inductivement la proposition Ou(P Q : Prop) : Prop.

  • Définir la conjonction logique ainsi.

      P     Q
    --------- [et]
     (Et P Q)
    

    On utilisera un système d'inférence paramétré, définissant inductivement la proposition Et(P Q : Prop) : Prop.

  • Définir la négation Non P par P -> Faux. Il s'agit d'une simple définition, non inductive.
  • Introduire les notations habituelles pour ces opérateurs. Pour éviter la confusion avec les notations standards, rajouter : type_scope à la fin de la définition.
    • Ou : \/
    • Et : /\
    • Non : ~
  • Définir un prédicat sur les entiers naturels, qui est toujours vrai.
  • Montrer qu'effectivement pour tout entier naturel, ce prédicat est vrai.
  • Montrer la distributivité de la conjonction sur la disjonction.

    ∀ P Q R, ((P ∧ (Q ∨ R) -> (P ∧ Q) ∨ (P ∧ R))
           ∧ ((P ∧ Q) ∨ (P ∧ R) -> P ∧ (Q ∨ R)))
    
    • Faire d'abord la démonstration sur papier en utilisant les règles du calcul des séquents (étant données trois propositions p, q et r).
    • Coder en Coq la démonstration.

      Lemma distributivite : forall P Q R,
        ((P /\ (Q \/ R) -> (P /\ Q) \/ (P /\ R))
        /\
        ((P /\ Q) \/ (P /\ R) -> P /\ (Q \/ R))).
      Proof.
        intros P Q R.
        (*
         * Pour appliquer la règle droite de l'implication, 
           - intro H. (H est le nom choisi pour l'hypothèse)
         * Pour appliquer une règle droite décomposant l'opérateur logique C (ou/et) : 
           - apply C.
         * Pour appliquer une règle gauche décomposant l'opérateur logique C (ou/et): 
           - case C as [premisses].
         * On indique dans [premisses] pour chaque règle les noms des variables associées 
         * à chaque prémisse de la règle. Le séparateur est |.
         * Exemples : 
           - Ou -> [p | q] (deux règles, chaque règle ayant une prémisse).
           - Et -> [p q] (une règle, avec deux prémisses).
         *)
      Qed.
      

Tutoriel - session 1 (fichier session1_progFcntl.v)

  • Reprendre toutes les définitions en adoptant le point de vue et le style logiques et non plus fonctionnels.
    • S'inspirer de l'exemple suivant (qui est le premier donné).

      Definition negb (b:bool) : bool :=
      match b with
        | true => false
        | false => true
      end.
      Definition negb' (b:bool) : bool.
      Proof.
      Show Match bool. (* commande permettant de voir les constructeurs de bool. *)
      case b.
      {
        apply false. (* ou : exact false. *)
      }
      {
        apply true.
      }
      Defined.
      Print neqb'. (* Code identique à celui de negb ! *)
      

Author: Hervé Grall
Version history: v1: 2020-01-07; v2: 2020-01-14[+intro/implication].
Comments or questions: Send a mail.
The webpage content is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.