All Questions
Tagged with coq or rocq-prover
3,009 questions
Advice
1
vote
6
replies
227
views
Can we prove equal subcases have equal induction hypotheses in recursion principle?
When performing recursion, it seems reasonable to assume that if two subcases f b1 and f b2 are equal, they will produce equal results IH b1 = IH b2: after all, we only expect to call the inductive ...
- 496
Advice
1
vote
1
replies
84
views
Coq (Rocq) standard library function for converting nat to string?
I'm looking for a Coq function that converts a natural number (of type nat) to a string. I've found some code here that works, but I'd really prefer if there was a function in a standard library that ...
- 199
0
votes
3
answers
119
views
Equality of type with equal indices do not typecheck
I have two discrete systems. The first one (B1) is composed of sequences
starting with 0 and where steps are either +2 or "no-op". For instance :
0 → 2 → 4 → 6...
0 → 0 → 2 → 4 → 4 → 4 → 6......
- 23
0
votes
3
answers
87
views
How to prove manually (using calc) a Dafny lemma with an existential variable?
I would like to have a following Dafny lemma to be proved. The automatic proof fails, so I have to use Dafny calc feature for guided proofs, but I don't see a way how to apply it in lemma with an ...
1
vote
2
answers
103
views
Kind of issue with two-steps recursion
Trying to get some basic results about Fibonnaci sequence, I faced a rocq behavior
that is daunting for my understanding of recursion. The following code shows that
the two-step Fibonacci function is ...
2
votes
1
answer
99
views
How to scrutinize a `match` term with return type `a=b -> c`
In the development below, I arrive at the goal, and I don't know how to proceed.
A: Type
a: list (list A)
b: list A
i,j: nat
Hi: i < length a
Hj: j < length (nth i a [])
-------------------------...
- 5,933
1
vote
1
answer
67
views
How to deal with potentially-aliased arguments in VST?
Consider the following code:
void incr(int *a, int *b) {
(*a)++;
(*b)++;
}
void f(int *a, int *b) {
incr(a, b);
incr(a, a);
}
The incr function admits two specifications:
{a ↦ n * b ↦ m}...
- 500
0
votes
2
answers
188
views
How can one handle dependent-type equality proofs (sigma types) in Coq?
I've been trying to prove this lemma (an abstract version of what I need), but I seem to be stuck with dependent-type errors. I tried to provide a first proof attempt (see below), but I fail to see ...
- 935
0
votes
2
answers
117
views
How can one handle by case analysis a boolP expression in Coq/ssreflect?
I'm puzzled by this simple lemma (a simplified version of what I'm trying to do).
From mathcomp Require Import all_ssreflect.
Lemma foo (bar : bool) : match boolP bar with
| @AltTrue _ _ baz => (...
- 935
3
votes
2
answers
165
views
Unexpected message about "decreasing argument of fix"
Trying to follow the course material in the Mathematical Components book
(see here, I tried to mimic the type of
the nat. The code is the followoing:
From HB Require Import structures.
From mathcomp ...
1
vote
1
answer
64
views
How to understand `(elimTF andP top)`?
Section 5.1.3 "Using views in intro patterns" of the book "Mathematical Components" explain how the view intro-pattern works as follows.
First, we have a lemma andP which relates (...
- 2,011
0
votes
1
answer
161
views
Providing and using proofs as arguments to a function in Rocq
I am having trouble with a piece of Rocq code that I think has to do with providing a proof argument to a function, but I am not sure.
Here's the relevant code. The code below typechecks:
Require ...
- 361
1
vote
2
answers
187
views
Deducing equality from existT equality
I'm doing inversion H on an Inductive definition that uses dependent types, and I obtain some assumptions of the form existT ... n = existT ... n' from which I want to deduce n = n' (this is done ...
- 4,540
0
votes
2
answers
134
views
Prove that an element of fin 1 is exactly 0
I have an inductive type
Inductive fin : nat -> Set :=
| First : forall n, fin (S n)
| Next : forall n, fin n -> fin (S n).
Coq cannot deduce that if something is of type fin 1 then it must be ...
- 311
1
vote
3
answers
96
views
In Coq (or Rocq), can't a lemma with a universal conclusion be applied to other premises?
When I prove with Coq (or Rocq), I find that sometimes if a hypothesis is "P" and another is "P -> forall x, Q x", I cannot make "forall x, Q x" a new premise by modus ...
