All Questions
80
questions
0
votes
0
answers
14
views
Try to understand SSReflect's "have" and square bracket
I tried to understand square braket patterns I have seen in different proofs. So I followed the SSReflect example, and tried serveral patterns:
Lemma test : True.
Proof.
have : exists v : nat, v > ...
- 1
1
vote
1
answer
52
views
Showing polynomial equality in coq/ssreflect
I am trying to prove equality of polynomials by explicit computation in coq. Here's an example showing where I get stuck:
From mathcomp Require Import all_ssreflect all_algebra.
Set Implicit ...
- 201
1
vote
2
answers
145
views
How to prove the goals in more elegant way using ssreflect?
It seems my coq proofs are longer and uglier than expected and I can't achieve ssreflect advantages in them despite my attempts. I think I missed some key points. Or maybe I just need to know more ...
- 13
0
votes
1
answer
37
views
Coerce rat to realType im math-comp/analysis
Is there a way to coerce a rat into a realType (from the math-comp/analysis library)? For example, the notation for coercing a nat is %:R.
- 370
0
votes
2
answers
58
views
Understanding \is a unit in ssreflect
I'm really annoyed by the following goal:
a%:R \is a unit
where a is a nat. The only lemma that seems to help is unitrE, but then it seems impossible to simplify further. This goal should be solvable....
- 370
0
votes
1
answer
32
views
using addf_div for rat_numDomainType
I am trying to apply the addf_div theorem from math-comp's ssralg to the following:
1 / a%:R + 1 / a%:R. I want to show that this is 2 / a%:R, but addf_div is over fieldTypes and can't be applied. Is ...
- 370
1
vote
2
answers
147
views
Coq - prove that there exists a maximal element in a non empty sequence
As an exercise I want to prove that there is always exists a maximum element in a non-empty sequence.
Theorem largest_el_in_list (s: seq rat) x : x \in s -> exists y, y \in s /\ forall z, z \in s -&...
- 370
1
vote
1
answer
66
views
Case analysis on max - ssreflect
I have the following in my goal:
maxr x0 x
I would like to do a case analysis, to consider what happens in the case that x0 is greatest, and the case the x is greatest. Is this possible in ssreflect?
...
- 370
2
votes
2
answers
103
views
rewriting hypothesis to false with a contradictory theorem
I want to show that
[seq q x t | x <- iota 0 (t + 1)] != [::]
I decided to destruct iota 0 (t + 1) because I have a lemma that says:
iota 0 (t + 1) != [::]
So the first case of destruct should ...
- 370
1
vote
1
answer
118
views
What does `apply.` tactic on it's own do in Coq -- i.e. without specifying a rule or hypothesis to unify the goal's conclusion with?
I think I understand the main idea of the apply tactic but I can't figure out what it does in this case:
Lemma HilbertS :
forall A B C : Prop,
(A -> B -> C) -> (A -> B) -> A -&...
- 5,961
3
votes
1
answer
144
views
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,...
- 6,068
2
votes
2
answers
132
views
ssreflect inversion, I need two equations instead of one
I have next definitions (code can be compiled):
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Set Asymmetric Patterns.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
...
- 740
1
vote
0
answers
96
views
Proof irrelevance of decidable *inequality* in coq
While trying to prove some equality in ssreflect, I got to the following:
WTS: forall (a b: ~ false), a = b
which is basically
WTS: forall (a b: false <> true), a = b.
Knowing that the following ...
- 73
0
votes
1
answer
100
views
Alternative tactic for `ssreflect`'s `move=>`
I like using the move=> tactic from the ssreflect library in cases when the goal is an implication (e.g. A -> B), to make the premise a hypothesis, and make the conclusion the new goal. However, ...
- 263
1
vote
1
answer
133
views
Why unable to perform case analysis in rather simple case
Well, the code
From mathcomp Require Import ssreflect ssrnat ssrbool eqtype.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Inductive nat_rels m n : bool -> bool -> bool -> Set :=
...
- 740