Questions tagged [coq]
Coq is a formal proof management system, semi-interactive theorem prover and functional programming language. Coq is used for software verification, the formalization of programming languages, the formalization of mathematical theorems, teaching, and more. Due to the interactive nature of Coq, we recommend questions to link to executable examples at https://x80.org/collacoq/ if deemed appropriate.
322
questions with no upvoted or accepted answers
31
votes
0
answers
401
views
Compatibility of impredicative Set and function extensionality
The Coq FAQ says that function extensionality is consistent with predicative Set. It's not fully clear to me from this whether it's consistent with impredicative Set (or maybe the consistency is ...
- 30k
17
votes
0
answers
643
views
What is the Parigot Mendler encoding?
The following encoding of Nats is used in some Cedille sources:
cNat : ★
cNat = ∀ X : ★ . X ➔ (∀ R : ★ . (R ➔ X) ➔ R ➔ X) ➔ X
cZ : cNat
cZ = Λ X . λ z . λ s . z
cS : ∀ A : ★ . (A ➔ cNat) ➔ A ➔ cNat
...
- 52.4k
9
votes
0
answers
377
views
How to extract the second element of Sigma on the Calculus of Constructions?
I'm attempting to do that as follows:
λ (A : *) ->
λ (B : (A -> *)) ->
λ (t : (∀ (r : *) -> (∀ (x : a) -> (B x) -> r)) -> r) ->
(t (B (t A (λ (x : A) -> λ (y : (B x)) -> ...
- 52.4k
9
votes
0
answers
332
views
Idris type system properties
Is it theoretically possible to convert any Coq proof to Idris or there are any limitations? More abstract question: Where does Idris type system fall on the lambda cube?
The reason for these ...
- 308
8
votes
0
answers
1k
views
Which axioms may be safely added to Coq?
This question is a request for references or explanation.
The main idea is: What if I add every axiom from standard library of Coq?
Will it raise a contradiction or they are well-adjusted to each ...
- 697
8
votes
0
answers
280
views
Definitional vs propositional equality in Coq lemma statements
When writing highly automated proofs in Coq (CPDT-style) proofs, building on extensive use of eauto N, I must often modify my lemma statements to allow eauto to use them easily. In particular, I must ...
- 6,478
8
votes
0
answers
470
views
Is it possible to normalize affine λ-calculus terms using PHOAS in Agda?
In Agda, one can conveniently represent λ-terms using PHOAS:
data Term (V : Set) : Set where
var : V → Term V
abs : (V → Term V) → Term V
app : Term V → Term V → Term V
That approach has ...
- 52.4k
7
votes
0
answers
942
views
proof general cannot find library or its source file even with coq-load-path-include-current and coq-compile-before-require
I'm on windows 8.1 with proof general 4.2 and emacs 24.2.1. I have set coq-compile-before-require and coq-load-path-include-current to on, but when I try to require a library whose source file is in ...
- 331
6
votes
0
answers
160
views
How does one automatically make a `COQ_PROJ.opam` install script automatically from a Coq Project/Package?
I have a very long list of coq projects I want to automatically install with opam pin/install. I'd like to install them with opam because I am using this python tool (PyCoq) that uses opam pin/install....
- 5,961
6
votes
0
answers
3k
views
How to resolve coq suffix import error (physical path bound to logical path)
Probably a coq newbie question, but I could not find a ready solution so I'll ask here for reference. The cocq version is 8.5pl2
I tried to build
coqfj. The first make attempt has failed with some ...
- 1,001
6
votes
0
answers
476
views
Extract functor in Coq to OCaml using Extraction mechanism of Coq
I have a function PolyInterpretation (http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt.html)
Definition PolyInterpretation := forall f : Sig, poly (arity f).
and a module signature TPolyInt(http://...
- 1,373
5
votes
0
answers
306
views
What is the origin of the names of I and tt?
The Coq standard library has two unit type. One True is typed in Prop, and has a single constructor I : True. The other unit is typed in Set, and has a single constructor tt : unit. I wonder what is ...
- 410
5
votes
1
answer
734
views
How to look at multiple goals at the same time?
I am considering writing tactics which will look at multiple goals and make decision based on that. However, when I use match goal with and stare at a goal, how do I say "please find another goal that ...
- 6,317
5
votes
0
answers
1k
views
Coq: Defining a subtype
I have a type, say
Inductive Tt := a | b | c.
What's the easiest and/or best way to define a subtype of it? Suppose I want the subtype to contain only constructors a and b. A way would be to ...
- 930
5
votes
0
answers
145
views
MSets of different types interact badly
I wanted to use sets, and for that tried to use the MSets library. But I need to write functions from one type of set to another type of set, and it interacts badly with Coq's module system.
Here is ...
- 3,102