Lezione 4

  • Applicazioni di Coq
    • un compilatore C verificato
    • un libreria di matematica organizzata come una libreria di programmi

  • Riflessione computazionale
    • idea
    • normalizzazione nella segnatura di un monoide

  • Esercizio


Applicazione: Compilatore certificato CompCert

CompCert è un vero e proprio compilatore C. Il compilatore è scritto in OCaml. Il codice OCaml è extratto da programmi/prove Coq.

Sito del compilatore

Tecniche:

  • estrazione di programmi da termini Coq
  • verifica correttezza traccia esterna per riflessione computazionale

Ora proviamo il programma estratto in OCaml


Applicazione: Verfica di prove di matematica

La libreria Mathematical Components e il Libro (draft) sulla formalizzazione in Coq di tale libreria.

Tecniche utilizzate:

  • riflessione booleana (predicati decidibili = programmi)
  • programmazione logica (inferenza di tipo à la type-classes)



Riflessione computazionale

Bello:

  • nella teoria dei tipi dimostrare 2+3=3+2 è facile, o meglio, la dimostrazione è molto corta apply: erefl
  • tale dimostrazione non dipende dalla taglia delle espressioni coinvolte, ie rimane triviale anche per 2+3+4+5=5+2+3+4
Meno bello:

  • il calcollo è completo su termini chiusi, se sono presenti variabili dobbiamo ragionare per induzione o riutilizzare lemmi dimostrati in precendenza, eg x + 0 = x
  • la taglia della dimostrazione dipende però dal numero di passi da fare, eg (x + 0) + 0 = x richiede 2 riscritture
Osservazione:

  • l'esecuzione di un programma p non richiede una prova p x = y
  • e non importa quanti passi di esecuzione p faccia la prova di p x = y è sempre erefl
Idea: potremmo scrivere un programma che fa la dimostrazione (quando questa è ripetitiva).

Per empio p potrebbe prendere una expressione in un monoide e metterla in forma normale, e.g.

x + 0 + (y + 0) ----> x + y

Iniziamo col dare una rappresentazione concreta (un dato induttivo) alle espressioni nel monoide.


Intepretazione

Il termine x + (0 + y) è di tipo nat ed è un termine che potremmo trovare in un goal. La sua rappresentazione sintattica Op (Value x) .. non ha tipo nat, anche se rappresenta un termine di tale tipo.

Scriviamo una funziona che interpreta una espressione sintattica in un monoide


Normalizzazione

Op Identity x --> x

Op x Identity --> x

Op x (Op y z) --> Op (Op x y) z


Correttezza dell'algoritmo di normalizzazione


Reificazione

Non è una funzione delle teoria dei tipi:

  • la teoria quozienta i termini wrt il calcolo
  • 1 + 1 e 2 sono indistinguibili
  • ma Op (Value 1) (Value 1) e Value 2 sono ben diversi!
  • quello che è preservato è il significato (interpretazione)
Soluzione: la funzione di reificazione la scriviamo un linguaggio che non è la teoria dei tipi ;-)

Fortuna: non ci interessa dimostrarla corretta, basta che lo sia in pratica.

Esercizio:

aggiungere un elemento assorbente al monoide (sintassi, interpretazione, normalizzazione, prova di correttezza, codice quote e codice monoid)



Inductive Syntax A :=
  | Identity
  | Annihilator
  | Value (a : A)
  | Op (m1 : Syntax A) (m2 : Syntax A).

Arguments Value {_} a.
Arguments Op {_} m1 m2.
Arguments Identity {_}.
Arguments Annihilator {_}.

Fixpoint interp {A} op id abs (m : Syntax A) :=
  match m with
  | Identity => id
  | Annihilator => abs
  | Value x => x
  | Op l r => op (interp op id abs l) (interp op id abs r)
  end.

Fixpoint norm {A} (m : Syntax A) :=
  match m with
  | Identity => Identity
  | Annihilator => Annihilator
  | Value x => Value x
  | Op l r =>
      let l := norm l in
      let r := norm r in
      match l, r with
      | Annihilator, _ => Annihilator
      | _, Annihilator => Annihilator
      | Identity, _ => r
      | _, Identity => l
      | _, Op a b => Op (Op l a) b
      | _, _ => Op l r
      end
   end.

Lemma norm_ok {A op id abs} :
  (forall a b c, op a (op b c) = op (op a b) c) ->
  (forall a, op id a = a) ->
  (forall a, op a id = a) ->
  (forall a, op abs a = abs) ->
  (forall a, op a abs = abs) ->
  forall (m : Syntax A), 
    interp op id abs m = interp op id abs (norm m).
Proof.
move=> opA idL idR abdL absR m.
elim: m => //= e1 -> e2 ->.
case: (norm e1); case: (norm e2) => //=.
Qed.

Ltac quote op id abs t :=
  match t with
  | (op ?a ?b) =>
        let x := quote op id abs a in
        let y := quote op id abs b in
        uconstr:(Op x y)
  | id => uconstr:(Identity)
  | abs => uconstr:(Annihilator)
  | ?x => uconstr:(Value x)
  end.

Ltac monoid op id abs opA idL idR absL absR :=
  match goal with
  |- ?a = ?b =>
      let x := quote op id abs a in
      let y := quote op id abs b in 
      change (interp op id abs x = interp op id abs y);
      rewrite [interp op id abs x](norm_ok opA idL idR absL absR);
      rewrite [interp op id abs y](norm_ok opA idL idR absL absR);
      compute -[op]
  end.