Seance 6 — Logique des Constructions

6.1 Types dependants et Logique des Constructions

6.1.1 Types dependants (Pi-types)

(* Vecteur de longueur connue (type dependant) *)
Inductive Vect (A : Type) : nat -> Type :=
  | VNil  : Vect A 0
  | VCons : forall n, A -> Vect A n -> Vect A (S n).

(* Vect A n = vecteur de n elements de type A *)
(* La longueur est dans le TYPE, pas dans les donnees ! *)

(* Exemple *)
Definition v2 := VCons nat 1 (VCons nat 2 (VNil nat)).
(* v2 : Vect nat 2 *)

(* Tentative de faux vecteur : *)
(* VCons nat 1 (VNil nat) : Vect nat 1 — on ne peut pas mentir sur la longueur ! *)

6.2 Regles de reecriture

(* Exemple : n = m -> n + 1 = m + 1 *)
Lemma eq_succ : forall n m : nat,
  n = m -> S n = S m.
Proof.
  intros n m H.
  rewrite H.
  reflexivity.
Qed.

6.3 Proprietes des programmes

Les proprietes verifiables :

• Correction fonctionnelle : le programme fait ce qu'il doit
• Terminaison : le programme s'arrete toujours
• Preservation de type : les types sont conserves
• Invariants : certaines proprietes restent vraies

6.4 Application — Verification des programmes

6.4.1 Verification de la factorielle

(* La factorielle de la Seance 1 *)
Fixpoint fact (n : nat) : nat :=
  match n with
  | O => 1
  | S p => S p * fact p
  end.

(* Equivalence avec Nat.factorial *)
Lemma fact_equivalence : forall n,
  fact n = Nat.factorial n.
Proof.
  intro n. induction n as [| n' IH].
  - simpl. reflexivity.
  - simpl. rewrite IH. reflexivity.
Qed.

(* La factorielle est toujours positive *)
Lemma fact_non_nul : forall n,
  fact n > 0.
Proof.
  intro n. induction n as [| n' IH].
  - simpl. lia.
  - simpl. lia.
Qed.

(* La factorielle est croissante *)
Lemma fact_croissant : forall n,
  fact (S n) >= fact n.
Proof.
  intro n. induction n as [| n' IH].
  - simpl. lia.
  - simpl. lia.
Qed.

6.4.2 Verification des listes

(* map preserve la longueur *)
Lemma map_length : forall (A B : Type) (f : A -> B) (l : list A),
  length (map f l) = length l.
Proof.
  intros A B f l. induction l as [| a l' IH].
  - simpl. reflexivity.
  - simpl. rewrite IH. reflexivity.
Qed.

(* filter n'augmente pas la longueur *)
Lemma filter_length : forall (A : Type) (p : A -> bool) (l : list A),
  length (filter p l) <= length l.
Proof.
  intros A p l. induction l as [| a l' IH].
  - simpl. lia.
  - simpl. destruct (p a).
    + simpl. lia.
    + lia.
Qed.

6.4.3 Verification de l'interpreteur d'AST

(* Type des expressions *)
Inductive expr : Type :=
  | Cst : nat -> expr
  | Add : expr -> expr -> expr.

(* Interpreteur *)
Fixpoint eval (e : expr) : nat :=
  match e with
  | Cst n => n
  | Add e1 e2 => eval e1 + eval e2
  end.

(* Instructions de la machine a pile *)
Inductive instruction : Type :=
  | PUSH : nat -> instruction
  | ADD  : instruction.

(* Compilateur *)
Fixpoint compile (e : expr) : list instruction :=
  match e with
  | Cst n => PUSH n :: nil
  | Add e1 e2 => compile e1 ++ compile e2 ++ ADD :: nil
  end.

(* Executeur *)
Fixpoint exec (code : list instruction) (pile : list nat)
  : option nat :=
  match code with
  | nil =>
    match pile with
    | cons a nil => Some a
    | _ => None
    end
  | PUSH n :: rest => exec rest (n :: pile)
  | ADD :: rest =>
    match pile with
    | cons a (cons b rest') => exec rest ((a + b) :: rest')
    | _ => None
    end
  end.

(* Theoreme de correction (partiellement admis) *)
Lemma compiler_correct : forall e,
  exec (compile e) nil = Some (eval e).
Proof.
  intro e. induction e as [n | e1 IH1 e2 IH2].
  - simpl. reflexivity.
  - simpl. rewrite IH1. rewrite IH2.
    (* A completer : cas de la pile *)
    Admitted.