Prove interattive

Introduzione

Per il momento abbiamo visto che, seguendo l'isomorfismo di Curry-Howard, per costruire una prova di una formula il procedimento consiste nel dare un oggetto il cui tipo è la formula. Costruire tale oggetto da capo può essere difficile, specialmente per le prove un po' complicate. In Coq è comunque possibile costruire tale oggetto in modo interattivo.

La costruzione interattiva è basata sulla nozione di tattica. Una tattica è un'operazione che prende un obiettivo (un goal) e restituisce una lista di sotto-obiettivi (subgoals). L'idea è che se i sotto-obiettivi possono essere provati, allora vuol dire che l'obiettivo iniziale è valido.

Per esempio, consideriamo la seguente prova: F D E B G C A Si può vedere la sua costruzione interattiva come il processo seguente. A partire dall'obiettivo iniziale A:

Applicando la prima tattica si creano due sotto-obiettivi B e C. Adesso è sufficiente trovare una prova per B e per C.
Sull'obiettivo B si applica un'altra tattica che a sua volta crea due nuovi obiettivi D e E. Per finire la prova, bisogna adesso trovare una prova per D, E e C.
Applicando una tattica su D si crea un nuovo obiettivo F.
Su F si applica un'altra tattica che non restituisce alcun obiettivo. Sono rimasti da provare solo E e C.
Su E si applica una tattica che termina la prova.
Su C si applica una tattica che genera G.
Si prova G applicando una tattica che non restituisce alcun obiettivo. La prova è finita.

In Coq, lo stato di una prova è implementato come una pila. Quando si applica una tattica, la tattica toglie l'obiettivo in testa alla pila e aggiunge i suoi sotto-obiettivi. Quindi, i movimenti sulla pila per l'esempio precedente sono i seguenti. Si parte con [A]:

[B;C]
[D;E;C]
[F;E;C]
[E;C]
[C]
[G]
[]

Quando la pila è vuota, la prova è finita.

Un obiettivo è composto dalla formula da provare (conclusione) e dall'ambiente (contesto) dentro il quale si deve provare la formula, costituito dalla lista delle ipotesi che si possono usare per provare la formula. In Coq un obiettivo è presentato cosí:

     Ambiente
  ============================
     Formula

Il comando Theorem permette di fare una prova in modo interattivo:
Theorem <NAME>: <TYPE>.

Si entra in modo interattivo. Adesso si può usare le tattiche o i comandi Undo e Abort per cancellare l'ultima tattica e uscire dal modo interattivo, rispettivamente. Quando la prova è finita (non ci sono piú obiettivi), si può registrarla usando il comando Qed.

Tattiche di base

Exact

La tattica di base exact permette di dare direttamente l'espressione che ha come tipo l'obiettivo che vogliamo provare. Dunque,

Definition A : T : = P.

è equivalente a:

Theorem A : T.
exact P.
Qed.

Logica

La tabella delle tattiche di base:

intro elim

⇒ intro <NAME> apply <NAME>

∧ split case <NAME>

∨ left
right case <NAME>

False case <NAME>

¬ red red in <NAME>

∀ intro <NAME> apply <NAME>

∃ exists <EXP> case <NAME>

Elim

Se l'oggetto n ha un tipo induttivo T, facendo elim n, si inizia una prova per ricorsione. Per esempio, per fare una prova per ricorsione sui numeri naturali, si fa:

Theorem Odd_or_Even: forall n: nat, (Even n) \/ (Odd n).
intro n.
elim n.
....

Esempio

Vediamo come si fa l'interazione per provare il teorema ∀A: Prop. ∀B: Prop. A∧B ⇒ B∧A.

Theorem and_com: forall A: Prop, forall B: Prop, A/\B -> B/\A.
1 subgoal
  
  ============================
   forall A: Prop, forall B: Prop, A/\B -> B/\A

Introduciamo A:

intro A.
1 subgoal
  
  A : Prop
  ============================
   forall B: Prop, A/\B -> B/\A

Introduciamo B:

intro B.
1 subgoal
  
  A : Prop
  B : Prop
  ============================
   A/\B -> B/\A

Introduciamo la prova di A/\B con il nome H:

intro H.
1 subgoal
  
  A : Prop
  B : Prop
  H : A/\B
  ============================
   B/\A

Per provare B/\A bisogna provare B e A:

split.
2 subgoals
  
  A : Prop
  B : Prop
  H : A/\B
  ============================
   B

subgoal 2 is: 
 A

Facciamo una discussione su H:

case H.
2 subgoals
  
  A : Prop
  B : Prop
  H : A/\B
  ============================
   A -> B -> B

subgoal 2 is: 
 A

Invece di mettere le nuove ipotesi nel contesto, Coq le ha messe dentro l'obiettivo, cosí l'utente può decidere quale nome dare alle due ipotesi. Per esempio, supponiamo di dare il nome H1 alla prima ipotesi:

intro H1.
2 subgoals
  
  A : Prop
  B : Prop
  H : A/\B
  H1 : A
  ============================
   B -> B

subgoal 2 is: 
 A

e di chiamare la seconda ipotesi H2:

intro H2.
2 subgoals
  
  A : Prop
  B : Prop
  H : A/\B
  H1 : A
  H2 : B
  ============================
   B

subgoal 2 is: 
 A

Adesso l'obiettivo è una prova di B, ma abbiamo H2 che è una prova di B, dunque:

exact H2.
1 subgoal
  
  A : Prop
  B : Prop
  H : A/\B
  ============================
   A

È rimasto solo un obiettivo, che viene provato nella stessa maniera:

case H.
1 subgoal
  
  A : Prop
  B : Prop
  H : A/\B
  ============================
   A -> B -> A


intro H1.
1 subgoal
  
  A : Prop
  B : Prop
  H : A/\B
  H1 : A
  ============================
   B -> A


intro H2.
1 subgoal
  
  A : Prop
  B : Prop
  H : A/\B
  H1 : A
  H2 : B
  ============================
   A


exact H1.
Subtree proved!

La prova è finita. Si può salvare:

Qed.
and_com is defined

Check and_com.
and_com
     : forall A: Prop, forall B: Prop, A/\B -> B/\A

Esercizi

K1. Dare la sequenza di tattiche che corrisponde alla prova di:

Theorem trivial: forall A: Prop, A -> A.

K2. Dare la sequenza di tattiche che corrisponde alla prova di:

Theorem or_commutative: forall A: Prop, forall B: Prop, A \/ B -> B \/ A.

K3. Dare la sequenza di tattiche che corrisponde alla prova di:

Theorem mp: forall A: Prop, forall B: Prop, A -> (A -> B) -> B.

K4. Dare la sequenza di tattiche che corrisponde alla prova di:

Theorem S: forall A: Prop, forall B: Prop, forall C: Prop, (A -> B ->C) -> (A ->B) -> A -> C.

K5. Dare la sequenza di tattiche che corrisponde alla prova di:

Theorem Praeclarum: forall x: Prop, forall y: Prop, forall  z: Prop, forall t: Prop, (x -> z) /\ (y -> t) -> x /\ y -> z /\ t.

K6. Dare la sequenza di tattiche che corrisponde alla prova di:

Theorem resol: 
  forall p: Type -> Prop, forall q: Type -> Prop, forall a: Type,
 (p a) -> (forall x: Type, (p x) -> (q x)) -> (q a).

K7. Dare la sequenza di tattiche che corrisponde alla prova di:

Theorem S: 
  forall A: Set,
  forall R: A -> A -> Prop,
  (forall x: A, forall y: A, forall z: A, (R x y) /\ (R y z) -> (R x z)) -> (forall x: A, forall y: A, (R x y) -> (R y x)) -> 
  forall x: A, (exists y: A, (R x y)) -> (R x x).

K8. Dare la sequenza di tattiche che corrisponde alla prova di:

Theorem not_not: forall a: Prop, a -> ~ (~ a).

K9. Dare la sequenza di tattiche che corrisponde alla prova di:

Theorem mini_cases: forall x: Prop, forall y: Prop, (x \/ ~ y) /\ y -> x.

K10. Dare la sequenza di tattiche che corrisponde alla prova di:

Theorem not_quite_classic: forall a: Prop, ~ (~ (a \/ ~ a)).

Laurent Théry

	intro	elim
⇒	`intro <NAME>`	`apply <NAME>`
∧	`split`	`case <NAME>`
∨	`left` `right`	`case <NAME>`
False		`case <NAME>`
¬	`red`	`red in <NAME>`
∀	`intro <NAME>`	`apply <NAME>`
∃	`exists <EXP>`	`case <NAME>`