The SSReflect proof language is a set of Coq tactics which allows for small scale reflection. It is the core language used in the Mathematical Components project and has been integrated into vanilla Coq starting from version 8.7.
Questions tagged [ssreflect]
78 questions
11
votes
2 answers
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 checked seemed to be very confusing to me. Does…
Marcus
- 437
- 2
- 11
7
votes
1 answer
Canonical structures in ssreflect
I'm trying to deal with canonical structures in ssreflect. There are 2 pieces of code that I took from here.
I will bring pieces for the bool and the option types.
Section BoolFinType.
Lemma bool_enumP : Finite.axiom [:: true; false]. Proof. by…
Sergey Bozhko
- 158
- 5
5
votes
2 answers
Does ssreflect assume excluded middle?
I am reading the ssreflect tutorial, which reads:
Below, we prove the ... by translating the propositional statement
into its boolean counterpart, which is easily proved using brute
force. This proof technique is called reflection. Ssreflect’s…
thor
- 21,418
- 31
- 87
- 173
4
votes
3 answers
Distributing subtraction over bigop
What is the best way to rewrite \sum_(i...) (F i - G i) as (\sum_(i...) F i - \sum_(i...) G i) on ordinals with bigop, assuming that underflows are properly managed?
More precisely, regarding these underflows, I'm interested in the following…
Pierre Jouvelot
- 901
- 3
- 13
4
votes
1 answer
How should a user-defined enumerated type be made `finType`?
I want to make an inductively-defined enumerated type in Coq/SSReflect like
Inductive E: Type := A | B | C.
be finType because it is apparently a finite type.
I have three solutions to do it but all are involved than I expected and never be…
Teirflegne
- 87
- 3
4
votes
1 answer
Proving isomorphism between Martin-Lof's equality and Path Induction in Coq
I am studying Coq and trying to prove the isomorphism between Martin-Lof's equality and the Path Induction's one.
I defined the two equalities as follows.
Module MartinLof.
Axiom eq : forall A, A -> A -> Prop.
Axiom refl : forall A, forall x : A,…
madipi
- 355
- 2
- 11
3
votes
1 answer
Coq/SSReflect: standard way to case on (x < y) + (x == y) + (y < x)?
In vanilla Coq, I'd write
Require Import Coq.Arith.Arith.
Goal nat -> nat -> False.
intros n m.
destruct (lt_eq_lt_dec n m) as [[?|?]|?].
to get three goals, one for n < m, one for n = m, and one for m < n.
In ssreflect, I'd start with
From…
Jason Gross
- 5,928
- 1
- 26
- 53
3
votes
1 answer
string comparison in ssreflect
I'm trying to make an ssreflect OrdType out of a custom type which involves strings. I assume that there is some inbuilt order type for strings in ssreflect, but I can't find it anywhere. I see one in Coq's standard library, but I can't figure out…
push33n
- 398
- 4
- 12
3
votes
1 answer
Is there any support in mathcomp/ssreflect for classical logic
For example, coq has in its standard library a Classical package with lemmas in classical logic such as ones that relate forall and exists (https://coq.inria.fr/library/Coq.Logic.Classical_Pred_Type.html).
My question is if there is any support like…
Christian Altamirano
- 31
- 2
3
votes
1 answer
polymorphic equality in coq
I cannot find a standard library == function which is overloaded and returns a boolean (or a sumbool, or something I can compute with). I would like to be able to do
3==5
and
"hello" == "hello"
without having to specify the type of the arguments.…
push33n
- 398
- 4
- 12
3
votes
1 answer
Instantiating a commutative ring of Zn with mathcomp
I was able to create a ComRingMixin, but when I try to declare this type as a canonical ring, Coq complains:
x : phantom (GRing.Zmodule.class_of ?bT) (GRing.Zmodule.class ?bT)
The term "x" has type "phantom (GRing.Zmodule.class_of ?bT)…
gtaumaturgo
- 33
- 3
3
votes
2 answers
Coq/SSReflect: How to do case analysis when reflecting && and /\
I have the following reflect predicate:
Require Import mathcomp.ssreflect.all_ssreflect.
Inductive reflect (P : Prop) (b : bool) : Prop :=
| ReflectT (p : P) (e : b = true)
| ReflectF (np : ~ P) (e : b = false).
And I am trying to relate the…
Atharva Shukla
- 2,098
- 8
- 21
3
votes
1 answer
Derive a ssreflect finType from a seq over a finType with uniq
I have a structure consisting of a sequence over a finite type and a proof of uniq of this sequence. This should describe a type that is obviously finite, but I do not see how to show that.
I thought I could use UniqFinMixin, however it requires -…
Pierre-Léo Bégay
- 57
- 5
3
votes
1 answer
Deriving a cannonical structure for a record in coq (ssreflect)
Given the following assumptions:
Variable A : finType.
Variable B : finType.
Variable C : finType.
and a record defined as:
Record example := Example {
example_A : A;
example_B : B;
example_C : C;
}.
Intuitively, it would…
Kiran Gopinathan
- 73
- 7
3
votes
1 answer
Coq Reals and Ssreflect GRings
I'd like to use ssreflect's lemmas on the Reals defined in Coq.Reals.Raxioms.
How do I do that?
For example, I'd like to be able to use the add, mul, etc. operations defined for ssralg.GRing.Ring directly on variables of type Rdefintions.R and apply…
larsr
- 5,447
- 19
- 38