Seance 4 -- Types et logique des propositions

4.1 Inference de types

En OCaml, le compilateur deduit automatiquement les types des expressions (type inference). En Coq, le mecanisme est similaire mais plus strict.

(* OCaml : le type est infere *)
let ident x = x            (* 'a -> 'a *)
let compose f g x = f (g x) (* ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c *)

(* Coq : meme principe *)
Check (fun x => x).
(* = ?A -> ?A : Type *)

4.2 Logique des propositions

Correspondance de Curry-Howard

La logique et les types sont la meme chose :

Logique	Types
Proposition	Type
Preuve	Programme
`P /\ Q`	Produit (`P * Q`)
`P \/ Q`	Somme ( `Either P Q`)
`P -> Q`	Fonction (`P -> Q`)
`forall x, P x`	Type dependant (Pi-type)
`exists x, P x`	Sigma-type
`True`	Unit
`False`	Empty

4.2.1 Connectives logiques en Coq

(* Conjonction (et) *)
Inductive and (P Q : Prop) : Prop :=
  | conj : P -> Q -> P /\ Q.

(* Disjonction (ou) *)
Inductive or (P Q : Prop) : Prop :=
  | or_introl  : P -> P \/ Q
  | or_intror  : Q -> P \/ Q.

(* Faux *)
Inductive False : Prop := .

(* Vrai *)
Inductive True : Prop :=  I : True.

4.2.2 Exemple : commutativite

(* Commutativite de la conjunction *)
Lemma and_comm : forall P Q : Prop,
  P /\ Q -> Q /\ P.
Proof.
  intros P Q H.
  destruct H as [HP HQ].
  split.
  - exact HQ.
  - exact HP.
Qed.

(* Commutativite de la disjonction *)
Lemma or_comm : forall P Q : Prop,
  P \/ Q -> Q \/ P.
Proof.
  intros P Q H.
  destruct H as [HP | HQ].
  - right. exact HP.
  - left. exact HQ.
Qed.

4.3 Sequents et regles d'introduction

Definition — Sequent

Un sequent est de la forme Γ |- P, ou Γ est le contexte (hypotheses) et P est la conclusion a prouver.

4.3.1 Regles d'introduction

Regle	En Coq	Description
Hyp	`exact H`	Utiliser une hypothese du contexte
→I	`intro H`	Introduire une hypothese
/\I	`split`	Prouver les deux parties d'une conjunction
\/I₁	`left`	Prouver la partie gauche d'une disjonction
\/I₂	`right`	Prouver la partie droite d'une disjonction
botE	`contradiction`	De `False`, tout est prouvable

4.3.2 Regles d'elimination

Regle	En Coq	Description
→E	`apply H`	Appliquer une implication
/\E₁	`destruct H`	Extraire la partie gauche
/\E₂	`destruct H`	Extraire la partie droite
\/E	`destruct H`	Cas par cas sur une disjonction

4.4 Arbres de preuves

Arbre de preuve pour (P /\ Q) -> (Q /\ P)

             [H : P /\ Q]
             --------------
             [HQ : Q]  [HP : P]
           ---------   ---------
           Q /\ P
    ---------  (->I, H)
    P /\ Q -> Q /\ P

Exemple Coq complet

Lemma imp_or : forall P Q : Prop,
  P -> P \/ Q.
Proof.
  intros P Q HP.
  left.
  exact HP.
Qed.

4.5 Application — Mini assistant de preuves

(* Representons les propositions comme des types *)
type prop =
  | Var of string
  | And of prop * prop
  | Or  of prop * prop
  | Imp of prop * prop
  | Bot

type sequent = {
  contexte : (string * prop) list;
  conclusion : prop;
}

let appliquer_tactique seq tac =
  match tac with
  | Intro (nom, hyp) ->
    match seq.conclusion with
    | Imp (p, q) ->
      Some { contexte = (nom, p) :: seq.contexte; conclusion = q }
    | _ -> None
    end
  | Split ->
    match seq.conclusion with
    | And (p, q) -> Some [ { seq with conclusion = p };
                           { seq with conclusion = q } ]
    | _ -> None
    end
  | Exact nom ->
    if List.assoc_opt nom seq.contexte = Some seq.conclusion
    then Some []
    else None
  | _ -> None

Exercices

Implementez la tactique Apply dans l'assistant.
Prouvez (P \/ Q) /\ R -> (P /\ R) \/ (Q /\ R) en Coq.
Implementez l'elimination du cut pour l'assistant.

Seance 4 — Types et logique des propositions