Discriminazione dei costruttori e sotto tipi

  • definiamo il tipo dei numeri naturali positivi
  • usiamolo per programmare la funzione pred

Dobbiamo dimostrare che, per sempio, ~ 3 = 0, per applciare pred a 3

Adesso generalizziamo not_3_0 a not_Sx_0 perchè ci servirà dopo

Concetti:

  • sig rappresenta un sotto tipo
  • eixists (il costruttore di sig) è come pair, raggruppa due termini e possiamo usarlo per scrivere programmi
  • change tipo per cambiare la forma del goal corrente con una convertibile
  • dimostrare che 2 costruttori sono diversi

Lezione 3

  • Induzione
    • programmiamo il principio per nat
    • prove per induzione su nat
    • accumulatori e generalizzazione
    • prove per induzione su liste

  • Esercizi

Dimostriamo (hem programmiamo) il principio di induzione per nat

Se le prove sono programmi, allora abitiamo questo tipo, senza troppo riflettere a cosa significhi.

Abbiamo ottenuto il principio di induzione!

Beh, anche Coq lo sa fare... Infatti non appena uno definisce il tipo nat Coq genera questo programma in modo automatico:

Concetti:

  • I principi di induzione non sono altro che funzioni ricorsive

La prima prova per induzione

Concetti:

  • elim: n per iniziare l'induzione
  • rewrite /= per calcolare all'avanti
  • ... => nomi
  • ... => /=
  • by ... per terminare un comando di prova

Accumulatori e generalizzazione

Concetti:

  • => //= per semplificare e eliminare goal triviali
  • elim: main gens per generalizzare prima di fare l'induzione

Indici e inversione

Concetti:

  • move: (term) per generare una equazione
  • case: {occs}_ / h per scegliere le occorrenze degli indici di h da sostituire
  • inversion H genera l'equazione e fa il case: ../.. al volo

Link utili:

Esercizi 

by elim: a => //= p -> .
Note: se si da il nome -> a una ipotesi equazionale, allora la si sostituisce al volo. 

by elim: l1 => //= x xs ->.


by elim: l => //= x xs ->.


by elim: l => //= y ys ->.


elim: l1.
  by rewrite /= append_nil.
move=> x xs /= ->.
by rewrite appendA.


elim: l => //= x xs IH .
by rewrite rev_append /= IH.

In questo esercizio, prima di iniziare la prova bisogna capire quale invariante serve dimostrare. In partcolare l'accumulatore nil (da generalizzare come ben sapete) non compare a destra. E questo è il problema che dovere risolvere... E la soluzione è uno dei lemmi che avete dimostrato prima! 

rewrite -(append_nil A (rev l)).
elim: l nil => //= x xs IH acc.
by rewrite IH append_cons.