Esiste un insieme minimo di tattiche in Coq?

Ho visto molte tattiche di Coq che si sovrappongono in funzione.Esiste un insieme minimo di tattiche in Coq?

Ad esempio, quando si ha la conclusione precisa nell'ipotesi, è possibile utilizzare assumption, apply, exact, trivial, e forse altri. Altri esempi includono destruct e induction per tipi non induttivi (??).

La mia domanda è:

Esiste un minimo serie di base tattiche (che esclude auto, e la sua simili) che è completo, nel senso che questo set può essere utilizzato per dimostrare qualsiasi Coq -progetti teorici sulle funzioni dei numeri naturali?

Le tattiche in questo insieme minimo essenziale sarebbero idealmente di base, in modo che ciascuna eseguisse una (o due) sola funzione e si potesse facilmente capire cosa fa.

fonte

2015-09-20 tinlyx

A causa dell'isomorfismo di Curry-Howard, ogni prova che è possibile costruire con una tattica corrisponde a un termine. Quindi, la tattica 'esatta' è sufficiente per dimostrare qualsiasi obiettivo. Se non vuoi costruire il termine tutto in una volta, puoi usare 'refine' invece. –

Una prova in Coq è solo un termine del tipo corretto. Le tattiche ti aiutano a costruire questi termini combinando sottotemi più piccoli in termini più complessi. Pertanto, l'insieme minimo di tattiche di base conterrebbe solo la tattica exact, come menzionato da Konstantin.

La tattica refine consente di fornire direttamente termini di prova, ma con buchi che genereranno sotto-obiettivi. Fondamentalmente ogni tattica è solo un'istanza della tattica refine.

Tuttavia, se si desidera esaminare in primo luogo solo un insieme minimo di tattiche, vorrei prendere in considerazione intro{s}, exists, reflexivity, symmetry, apply, rewrite, revert, destruct e induction. inversion potrebbe tornare utile anche troppo rapidamente.

fonte

2015-09-21 09:28:37 Vinz

'reflexivity' è semplicemente' applica eq_refl' se non si utilizzano i setoid e anche la simmetria è un'applicazione; esiste "costruttore", che a sua volta è anche "applica". Utilizzi spesso 'ripristina'? D'altra parte, 'rewrite' e' simpl' sarebbero probabilmente delle belle aggiunte a questa lista. –

Si potrebbe dire il concetto di "riscrittura", è solo l'applicazione di un lemma con la forma corretta. Come ho detto, tutto si riduce a "raffinare" (scrivendo direttamente il termine di prova). Ma ammetto, 'riscrivi' dovrebbe essere nella lista. Uso spesso il revert, perché faccio molta induzione con tipi dipendenti, dove aiuta molto. – Vinz

Ah, i tipi dipendenti utilizzerebbero molto 'revert'ing, infatti :)' rewrite' è in effetti spesso solo un'applicazione di un principio induttivo, ma praticamente non lo uso mai. –

Esiste un insieme minimo di tattiche in Coq?

risposta

Problemi correlati