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.
287
questions
44
votes
2
answers
5k
views
Difference between type parameters and indices?
I am new to dependent types and am confused about the difference between the two. It seems people usually say a type is parameterized by another type and indexed by some value. But isn't there no ...
- 1,234
16
votes
1
answer
3k
views
Why are logical connectives and booleans separate in Coq?
I come from a JavaScript/Ruby programming background and am used to this being how true/false works (in JS):
!true
// false
!false
// true
Then you can use those true/false values with && ...
- 77.9k
22
votes
4
answers
12k
views
coqide - can't load modules from same folder
I can't load modules that are in same folder in CoqIde.
I'm trying to load sources from Software Foundations, I'm running coqide in folder that contains SF sources with coqide or coqide ./, then ...
- 7,029
8
votes
1
answer
1k
views
How or is that possible to prove or falsify `forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.` in Coq?
I want to prove or falsify forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q. in Coq. Here is my approach.
Inductive True2 : Prop :=
| One : True2
| Two : True2.
Lemma True_has_one : ...
- 1,712
8
votes
3
answers
3k
views
How to prove False from obviously contradictory assumptions
Suppose I want to prove following Theorem:
Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.
This one is trivial since m cannot be both successor and zero, as assumed. ...
- 363
21
votes
2
answers
5k
views
What exactly is a Set in Coq
I'm still puzzled what the sort Set means in Coq. When do I use Set and when do I use Type?
In Hott a Set is defined as a type, where identity proofs are unique.
But I think in Coq it has a different ...
- 1,216
14
votes
1
answer
2k
views
Coq simpl for Program Fixpoint
is there anything like the tactic simpl for Program Fixpoints?
In particular, how can one proof the following trivial statement?
Program Fixpoint bla (n:nat) {measure n} :=
match n with
| 0 => ...
- 143
12
votes
2
answers
2k
views
Step by step simplification in coq?
Is there a way to simplify one step at a time?
Say you have f1 (f2 x) both of which can be simplified in turn via a single simpl, is it possible to simplify f2 x as a first step, examine the ...
- 1,051
12
votes
2
answers
2k
views
How to install SSReflect and MathComp in Linux?
I have successfully installed Coq 8.6 and CoqIDE in Linux (Ubuntu 17.04). However, I don't know to proceed in order to add SSReflect and MathComp to this installation. All the references that I have ...
- 469
7
votes
2
answers
357
views
Proofs' role in Coq extractions
I'm trying to understand what is the role of proofs in Coq extractions.
I have the following example of floor integer division by two taken from here. For my first try I used the Admitted keyword:
(**...
- 6,760
6
votes
2
answers
2k
views
Decomposing equality of constructors coq
Often in Coq I find myself doing the following: I have the proof goal, for example:
some_constructor a c d = some_constructor b c d
And I really only need to prove a = b because everything else is ...
- 4,444
5
votes
2
answers
2k
views
How do we know all Coq constructors are injective and disjoint?
According to this course, all constructors (for inductive types) are injective and disjoint:
...Similar principles apply to all inductively defined types: all
constructors are injective, and the ...
- 22.1k
3
votes
1
answer
585
views
Structural recursion on a dependent parameter
I'm trying to write the sieve of Eratosthenes in Coq. I have a function crossout : forall {n:nat}, vector bool n -> nat -> vector bool n. When the sieve finds a number that is prime, it uses ...
user2457874
2
votes
1
answer
713
views
Writing well-founded programs in Coq using Fix or Program Fixpoint
Following the example given in the chapter GeneralRec of Chlipala book, I'm trying to write the mergesort algorithm.
Here is my code
Require Import Nat.
Fixpoint insert (x:nat) (l: list nat) : ...
- 619
98
votes
3
answers
18k
views
What are the strengths and weaknesses of the Isabelle proof assistant compared to Coq?
Does Isabelle/HOL proof assistant have any weaknesses and strengths compared to Coq?
- 1,013