Seance 5 — Logique des predicats

5.1 Logique des predicats

5.1.1 Quantificateurs en Coq

(* Universel : pour tout x, P(x) *)
Lemma forall_ex : forall n : nat, n + 0 = n.
Proof.
  intro n.
  induction n as [| n' IH].
  - simpl. reflexivity.
  - simpl. rewrite IH. reflexivity.
Qed.

(* Existentiel : il existe x tel que P(x) *)
Lemma exists_even : exists n : nat, n + n = 4.
Proof.
  exists 2.
  simpl. reflexivity.
Qed.

5.1.2 Regles des quantifyurs

Regle	En Coq	Condition
∀I	intro x	x ne doit pas apparaitre dans le contexte
∀E	specialize (H t)	Appliquer a un terme concret
&exists;I	exists t	Donner le temoin
&exists;E	destruct H as [x Hx]	Extraire le temoin et la propriete

5.2 Unification

type term =
  | TVar of string
  | TFun of string * term list

type subst = (string * term) list

let rec appliquer_subst subst t =
  match t with
  | TVar x       ->
    (try List.assoc x subst with Not_found -> t)
  | TFun (f, ts) ->
    TFun (f, List.map (appliquer_subst subst) ts)

let occurs_check x t =
  let rec aux = function
    | TVar y       -> x = y
    | TFun (_, ts) -> List.exists aux ts
  in aux t

let rec unifier t1 t2 =
  match t1, t2 with
  | TVar x, TVar y when x = y -> Some []
  | TVar x, _ when not (occurs_check x t2) ->
    Some [(x, t2)]
  | _, TVar x when not (occurs_check x t1) ->
    Some [(x, t1)]
  | TFun (f, ts1), TFun (g, ts2) when f = g &&
       List.length ts1 = List.length ts2 ->
    unifier_list ts1 ts2
  | _ -> None

and unifier_list ts1 ts2 =
  match ts1, ts2 with
  | [], [] -> Some []
  | t1 :: r1, t2 :: r2 ->
    match unifier t1 t2 with
    | None -> None
    | Some s1 ->
      match unifier_list
        (List.map (appliquer_subst s1) r1)
        (List.map (appliquer_subst s1) r2) with
      | None -> None
      | Some s2 -> Some (s1 @ s2)
    end
  | _ -> None

5.3 Raisonnement par induction

(* Associativite de l'addition *)
Lemma add_assoc : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
  intros n m p.
  induction n as [| n' IH].
  - simpl. reflexivity.
  - simpl. rewrite IH. reflexivity.
Qed.

(* Somme des n premiers entiers *)
Lemma somme_formule : forall n : nat,
  2 * somme n = n * (n + 1).
Proof.
  intro n. induction n as [| n' IH].
  - simpl. reflexivity.
  - simpl. lia.
Qed.

(* Longueur de append *)
Lemma append_length : forall (A : Type) (l1 l2 : list A),
  length (l1 ++ l2) = length l1 + length l2.
Proof.
  intros A l1 l2. induction l1 as [| a l1' IH].
  - simpl. reflexivity.
  - simpl. rewrite IH. reflexivity.
Qed.

5.4 Application — Mini Prolog

type fait = {
  pred : string;
  args : term list;
}

type base = {
  faits : fait list;
  regles : (fait * term list) list;  (* regle = fait + conditions *)
}

let ajouter_fait base f = { base with faits = f :: base.faits }

let ajouter_regle base (conclusion, conditions) =
  { base with regles = (conclusion, conditions) :: base.regles }

let rec rechercher base but subst =
  (* Essayer chaque fait de la base *)
  let resultats_faits =
    List.filter_map (fun f ->
      let but_subst = appliquer_subst subst but in
      unifier_fait but_subst f
    ) base.faits
  in
  (* Essayer chaque regle *)
  let resultats_regles =
    List.filter_map (fun (conclusion, conditions) ->
      let but_subst = appliquer_subst subst but in
      match unifier_fait but_subst conclusion with
      | None -> None
      | Some s ->
        (* Resoudre chaque condition recursivement *)
        Some (resoudre_conditions base conditions s)
    ) base.regles
  in
  resultats_faits @ List.concat resultats_regles