coq

14calore

2risposta

Che cosa significa V sta per nell'estensione di file Coq?

È .v per la verifica? convalida? vamanos? Perché non utilizzare l'estensione .coq?

5calore

1risposta

Controllo dell'esportazione di costruttori nel codice estratto da Coq

Sto guardando il codice di scrittura in Coq ed estraendo questo codice per l'utilizzo in un grande progetto Haskell. Voglio costruire un singolo modulo in Coq, provare le proprietà, quindi utilizzare

6calore

1risposta

come nominare l'assunto quando si ricorda un'espressione?

La documentazione per Coq reca l'ammonizione generale non per fare affidamento sul meccanismo di denominazione incorporato, ma selezionare i propri nomi, per evitare che le modifiche nel meccanismo di

9calore

1risposta

inverti ricorsivamente le ipotesi in coq

Ho difficoltà a definire una tattica per invertire ricorsivamente le ipotesi in un contesto di prova. Per esempio, supponiamo di avere un contesto prova contenente un'ipotesi simile: H1 : search_tree

6calore

3risposta

Come convinco coq che (A/\ B)/\ C == A/\ B/\ C?

Nella mia prova mi imbatto in problemi in cui c'è un nelle mie ipotesi, e ho bisogno di dimostrare (A /\ B) /\ C. Questi sono logicamente esattamente gli stessi, ma coq non li risolverà con assumption

9calore

1risposta

Glifi Unicode per parole chiave e operatori in Coq/Proof General in Emacs

Questa domanda ha a che fare con la configurazione della modalità Coq in Proof General, in Emacs. Sto cercando di fare in modo che Emacs sostituisca automaticamente le parole chiave e la notazione in

10calore

1risposta

Per tutti l'introduzione in coq?

Sto cercando di (classicamente) dimostrare ~ (forall t : U, phi) -> exists t: U, ~phi in Coq. Quello che sto cercando di fare è dimostrarlo contrapositively: 1. Assume there is no such t (so ~(exist

16calore

2risposta

LTAC-ticamente astraendo per un sottotermine del tipo di obiettivo

Come uno sfondo ruvido e ignorante, in HoTT, si deduce il heck fuori di tipo induttivo definito Inductive paths {X : Type } : X -> X -> Type := | idpath : forall x: X, paths x x. che permette la co

6calore

2risposta

Individuazione della definizione di una tattica nelle prove Coq

Nello studio delle prove di Coq di altri autori, incontro spesso una tattica, diciamo "inv eq Heq" o "intro_b". Voglio capire queste tattiche. Come posso trovare se è una tattica Coq o una notazione t

6calore

1risposta

Come utilizzare la riscrittura su una sottoespressione dell'obiettivo corrente

In coq, è in qualche modo possibile applicare un lemma o un'ipotesi a una sottoespressione dell'obiettivo corrente? Per esempio vorrei applicare il fatto che plus è commutativo per scambiare 3 e 4 in