Questions tagged [coq-mathcomp]

Mathematical Components are libraries of formalized mathematics developed using the Coq proof assistant.

Filter by
Sorted by
Tagged with
2 votes
0 answers
46 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....
user avatar
8 votes
2 answers
650 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 ...
user avatar
  • 2,676
4 votes
1 answer
95 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? ...
user avatar
  • 157
5 votes
2 answers
64 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 ...
user avatar
  • 157
7 votes
2 answers
137 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 ...
user avatar
  • 273