Questions tagged [coq-mathcomp]
Mathematical Components are libraries of formalized mathematics developed using the Coq proof assistant.
6
questions
5
votes
2
answers
112
views
Basics of real numbers in mathcomp (Coq)
I'm trying to play around with the Mathematical Components library in Coq but am having trouble writing basic, concrete statements about real numbers. E.g., I'd like to define
...
- 153
3
votes
0
answers
54
views
SSReflect tuple constructor: why not use phantom?
I was reading the mathcomp book learning about canonical structures and following along with the mathcomp source to compare how things were done in practice. Specifically I was looking at sections 6....
- 31
8
votes
2
answers
685
views
Explanation of Coq math-comp repositories
How are the Coq math-comp account and repositories related?
Details
One of my side goals is to try to keep the tags on this site meaningful and useful.
Today I ran into this question:
How to prove ...
- 2,786
4
votes
1
answer
104
views
How can I prove has_esp when using mathcomp.analysis?
How can I prove the following goal (which I believe to be true) using mathcomp.analysis?
...
- 157
5
votes
2
answers
68
views
How to provide a countType when using mathcomp?
The following snippet can't pass type checking.
From mathcomp Require Import choice.
Definition exfn (A:countType) := false.
(* Fail *) Check exfn nat.
Failed with ...
- 157
8
votes
2
answers
151
views
How to prove `forall m n : nat, m == n -> m = n`?
I am learning Coq with ssreflect. Just to understand things, I've proved forall a b : bool, a == b -> a = b but I can't figure out how to prove ...
- 317