Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.

Sign up to join this community
Anybody can ask a question
Anybody can answer
The best answers are voted up and rise to the top

Explore our questions

3 votes
0 answers
20 views

.CoqMakefile.d required by CoqMakefile but not generated

0 votes
0 answers
47 views

If I make some new structure like Q, then can I use 'rewrite' tactic for my new structure in Coq?

1 vote
1 answer
111 views

Can I unfold not all things but only one thing in Coq?

8 votes
3 answers
254 views

Has anyone accidentally "proven" a false theorem using what was later found to be a critical bug?

0 votes
1 answer
40 views

How can I correspond a hypothesis to a decidable axiom in match (in Coq)?

1 vote
1 answer
79 views

How do I prove this property in Coq?

1 vote
1 answer
49 views

How can I use a (three terms) decidable axiom in a case analysis?

2 votes
1 answer
92 views

Natural deduction with coq assistant prover

4 votes
1 answer
75 views

How can I search only all of the lemmas in a different module (in Coq)?

1 vote
2 answers
324 views

What is the remaining goals on the shelf?

3 votes
2 answers
106 views

Coq: can `tauto` be used to prove classical tautologies?

5 votes
0 answers
119 views

How does one systematically traverse OCaml representations of Coq ASTs terms?

0 votes
2 answers
80 views

How to define two mutually recursive functions in Coq?

5 votes
1 answer
83 views

Unexpected eta expansion in constant definition

Browse more Questions