"Verbose" auto in Coq

Question

Sto imparando Coq e il libro da cui sto imparando, (CPDT) fa un uso intenso di auto nelle prove.

Dal momento che sto imparando penso che potrebbe essere utile per me vedere esattamente cosa auto sta facendo sotto il cofano (meno magia all'inizio, meglio è). C'è un modo per costringerlo a mostrare esattamente quali tattiche o tecniche sta usando per calcolare la dimostrazione?

In caso contrario, c'è un luogo che descrive esattamente cosa fa auto?

Answer 1

Ci sono diversi modi per dare un'occhiata a ciò che sta succedendo sotto il cofano.

TLDR: Inserisci info prima della tua tattica, oppure usa Show Proof. prima e dopo aver chiamato la tattica e individuare le differenze.

---

vedere ciò che un particolare chiamata tattica ha fatto, è possibile prefisso è con info, in modo da mostrare la prova particolare iniziative ha adottato.

(Questo potrebbe essere rotto con Coq 8.4, vedo che essi forniscono info_ versioni di alcune tattiche, leggere il messaggio di errore se è necessario.)

Questo è probabilmente ciò che si desidera a un livello principiante, può già essere piuttosto conciso.

---

Un altro modo di vedere ciò che sta accadendo all'interno di una prova è quello di utilizzare il comando Show Proof.. Ti mostrerà il termine attualmente costruito con buchi e ti mostrerà quale buca deve riempire ciascuno dei tuoi obiettivi attuali.

Questo è probabilmente più avanzata, soprattutto se si utilizza tattica come induction o inversion, come il termine in costruzione sta per essere abbastanza coinvolti, e si richiede di comprendere la natura di fondo dei sistemi di induzione o pattern-matching dipendente (quale CPDT dovrebbe insegnarti abbastanza presto).

---

Una volta terminata la prova con Qed. (o Defined.), si può anche chiedere di guardare il termine che è stato creato utilizzando Print term. dove term è il nome del teorema/termine.

Questo spesso è un termine grosso e brutto, e richiede una certa formazione per essere in grado di leggerli per i termini coinvolti. In particolare, se il termine è stato costruito tramite l'uso di potenti tattiche (come omega, crush, ecc.), Probabilmente sarà illeggibile. Fondamentalmente lo userai solo per scansionare in un punto particolare del termine a cui sei interessato. Se è lungo più di 10 righe, non preoccuparti di leggerlo in un formato così crudele! :)

---

Con tutti i precedenti, è possibile utilizzare Set Printing All. in anticipo, in modo che Coq stampa i non piegati, versioni esplicite di tutto. Inoltre è prolisso ma può aiutarti quando ti chiedi quali siano i valori dei parametri impliciti.

Questi sono tutti quelli che posso pensare in cima alla mia testa, potrebbe esserci di più però.

---

Quanto a ciò che una tattica fa, il solito migliore risposta si trova nella documentazione:

http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@tactic155

In sostanza, auto tenta di utilizzare tutti i suggerimenti forniti (a seconda del database utilizzato), e per risolvere il tuo obiettivo combinandoli fino ad una certa profondità (che puoi specificare). Per impostazione predefinita, il database è core e la profondità è 5.

Maggiori informazioni che si possono trovare qui:

http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#Hints-databases