Skip to main content

Questions tagged [coq-mathcomp]

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

Filter by
Sorted by
Tagged with
1 vote
1 answer
51 views

I want to prove Lemma leq_exp2lp n1 n2 : 0 < n1 -> n1 <= n2 -> x ^ n1 and Theorem Argand : (x^2 + x + 1) * (x^2 - x + 1) = x^4 + x^2 + 1. in Coq

As I say in title, I want to prove two Lemmata in math-comp. At first, ======code====== From mathcomp Require Import all_ssreflect. Section Argand. Variable x : nat. Lemma leq_exp2lp n1 n2 : 0 < n1 ...
k k's user avatar
  • 11
2 votes
1 answer
80 views

About the use of command Canonical in Coq for mantaining Record Type information

Inside the MathComp book https://zenodo.org/records/7118596 there is the following example of use for the Canonical command: ...
Bruno Rafael's user avatar
2 votes
0 answers
34 views

Problem working with FMapWeakList and Parametrized Records

Consider the following definition of a record R, parametrized over an arbitrary eqType: ...
Felipe's user avatar
  • 63
2 votes
1 answer
85 views

Converting Lean formulations of Lemmas to Coq formulation

I want to contribute to the repository MiniF2F (https://github.com/facebookresearch/miniF2F/tree/main) which has formal formulation of problems asked in Math Olympiads in different languages like Lean,...
amit9oct's user avatar
1 vote
1 answer
82 views

Coq ssreflect - rewrite inside \big

I'm trying to prove the following lemma : ...
op325's user avatar
  • 13
5 votes
2 answers
370 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 ...
BallBoy's user avatar
  • 153
3 votes
0 answers
69 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....
wdeweijer's user avatar
8 votes
2 answers
839 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 ...
Guy Coder's user avatar
  • 2,846
4 votes
1 answer
127 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? ...
lyfeng's user avatar
  • 167
5 votes
2 answers
98 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 ...
lyfeng's user avatar
  • 167
8 votes
2 answers
228 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 ...
CrabMan's user avatar
  • 317