Note sulla lezione 1

  • match .. with .. end è un termine e può essere usato dovunque, non solo alla radice

E le chiamae ricorsive sono accettate anche su sotto-sotto-termini

  • I tipi induttivi ammetteno un principio di induzione/ ricorsione standard

Tipi di dato indiciati e i casi impossibili

Lezione 2

  • Curry Howard: la logica di Coq e le prime dimostrazioni
    • Programma : Tipo = Dimostrazione : Enunciato
    • connettivi
    • vero e falso
    • prove di logica proposizionale
    • uguaglianza
    • prove equazionali
    • quantificatori
    • prove in logica del primo ordine

  • Esercizi

Fare una dimostrazione è come abitare un tipo

Però lo facciamo in modo interattivo, usando dei comandi (tattiche) che costruiscono termini per noi.

I tipi (di dato) che abbiamo visto nella prima lezione non sono adatti a esprimere proprietà o enunciare veri e propri teoremi.

Ne definiamo quindi altri...

Concetti:

  • dimostrare = costruire termini passo passo
  • Lemma nome : tipo. Proof. ...prova... Qed.
  • apply: t usa t per dimostrare il goal corrente, ovvero t è un termine che abita il tipo del goal

Connettivi

$$P \to Q$$

dimostrare una implicazione (introduzione)

Usare una implicazione (MP)

$$P \land Q$$

Ricordate l'esercizio 8bis?

$$P \lor Q$$

Concetti:

  • congiunzione /\
  • disgiunzione \/
  • move=> nome
  • case: termine

Vero e falso

$$\top$$

$$\bot$$

$$\neg$$

Note: questo lemma è uguale all'esempio 4

Concetti:

  • vero e falso: True, False
  • negazione: ~
  • sostituire il nome con il corpo: unfold name in hyp (passo non strettamente necessario)

Uguaglianza

Ora ci siamo stufati della logica proposizionale e passiamo a quella del primo ordine.

Ci serve un predicato, e partiamo dal più difficle ;-)

Il tipo Id (che in Coq si chiama eq)

forall lega un termine

eq (Id) descrive una uguaglianza computazionale

Concetti:

  • uguaglianza = (Id nelle note del corso)
  • Usare un'uguaglianza: rewrite
  • erefl dimostra eq per termini uguali una volta nomalizzati
  • tipare un match (la clausola return e il tipo da fuori e da dentro

Quantificatori

Piccolo ripasso:

Il forall è primitivo, è stato usato

  • per legare tipi forall A : Type, list A -> nat
  • per legare termini forall x : A, eq A x x
  • per legare.. niente A -> B = forall dummy : A, B
Il dominio di forall

  • il tipo dei tipi forall A : Type, ..
  • un tipo di dato forall x : nat, ...
  • il tipo delle funzioni forall f : nat -> nat, ...

Ora usiamo $$\forall x:A, P x$$ che può essere dimostrato fornendo un funzione che data una prova di A (chiamata x) produce una prova di P x

Nota: del tutto simile alla prova di P -> P fatta nella slide 2

Nota: anche in questo caso il comportamento di XXX\forallXXX è molto simile a quello di XXX\toXXX

Ora definiamo $$\exists x:A, P x$$ che può essere dimostrato fornendo un testimone t : A e una prova p : P t

Nota: è molto simile alla coppia, ma il tipo della seconda componente dipende val valore della prima

forall lega un predicato/funzione

Dimostrazioni per casi

Concetti:

  • case: funziona anche su termini che rappresentano dati, come bool e nat
  • ; per combinare 2 comandi di prova (funziona solo con il browser Chrome)

Esercizi

Abitare i seguenti tipi (in un colpo solo o con dei comandi di prova) 

apply: (fun x =>
match x with
| conj (conj a b) c => conj (conj c a) b
end).


apply: (fun f q => f (right q)).


move=> npnq. case: npnq => np nq.
move=> poq. case: poq. apply: np. apply: nq.

La formula di Peirce

  • Suggerimento: scegliere per Q una formula falsa! 

move=> cc P.
apply: (cc False).
move=> truth.
apply: right.
move=> p.
apply: truth.
apply: left.
apply: p.

Dimostrare che orb è commutativo 

case: b1; case: b2; apply: erefl.

Dimostrare che orb è associativo 

case: b1; case: b2; case: b3; apply: erefl.

Dimostrare il seguente lemma 

case: b; apply: erefl.

Dimostra la seguente formula

XXX m ^ 2 - n ^ 2 = (m - n) * (m + n) XXX

Usare solo la riscrittura rewrite e i seguenti simboli e lemmi che sono forniti

Traccia della prova 

(m - n) * (m + n) =
          .. = m * (m + n) - n * (m + n)
          .. = m * m + m * n - n * (m + n)
          .. = m * m + m * n - (n * m + n * n)
          .. = m * n + m * m - (n * m + n * n)
          .. = n * m + m * m - (n * m + n * n)
          .. = m * m - n * n
          .. = m ^ 2 - n * n
          .. = m ^ 2 - n ^ 2


rewrite mulnBl.
rewrite mulnDr.
rewrite mulnDr.
rewrite addnC.
rewrite mulnC.
rewrite subnDl.
rewrite mulnn.
rewrite mulnn.
apply: erefl.