Skip to main content
5 votes
Accepted

My Inductive function over a pair of lists gives "Cannot guess decreasing argument of fix."

You need to change your equal definition to the following to let Coq know that your definition is indeed syntactically decreasing. ...
Hiroki Chen's user avatar
4 votes

My Inductive function over a pair of lists gives "Cannot guess decreasing argument of fix."

It is a limitation of mutual fixpoints. The guard checker requires that the structural arguments are on mutually defined inductive types. The solution is to replace with nested fixpoints as the ...
Dominique Larchey-Wendling's user avatar
3 votes
Accepted

Error `Abstracting over the term leads to a term which is ill-typed` when doing a destruct

Admittedly, the error is quite obscure, but the issue is that, while you do not see it, nth_safe_obligation_1 … uses ...
Meven Lennon-Bertrand's user avatar
3 votes

How do I define an induction principle for a type with a nested list of tuples?

The question of recursors for types nested with lists, aka rose trees, is popping up quite often these days. I did develop a Coq library specifically for the purpose of dealing with these data ...
Dominique Larchey-Wendling's user avatar
2 votes

How do I define an induction principle for a type with a nested list of tuples?

...
Li-yao Xia's user avatar
  • 1,757
2 votes
Accepted

Rewriting/Applying unidirectional morphisms in Coq

Morphisms only affect rewrite, not apply. The following does work, and makes use of the ...
djao's user avatar
  • 434
2 votes
Accepted

Book on Coq that helps me write proofs regarding integral equations

Unfortunately, Coq is maybe not your tool of choice. Real analysis in Coq is still work in progress, and not much has been formalized yet. The state of the art, to the best of my knowledge, is ...
xuq01's user avatar
  • 136
2 votes
Accepted

Inductive from CoInductive?

You should not expect to be able to pull a similar trick with inductives as you have with coinductives. Inductives are initial algebras of strictly positive polynomial endofunctors, while coinductives ...
Jason Gross's user avatar
  • 1,537
1 vote

How do I properly interact with CertiCoq's garbage collector when calling library functions from C++?

Thanks all for the help! After getting some offline help from Andrew Appel, I wanted to follow up with the solution in case it's useful to anyone else. The problem was in the use of LIVEPOINTERS. ...
Jennifer Paykin's user avatar
1 vote

How do I properly interact with CertiCoq's garbage collector when calling library functions from C++?

normally, the GC should not lead to a segmentation fault. In my experience, those rather arise from deep recursion when using non-tail recursive functions. I looked into your code examples and ...
Mario Frank's user avatar
1 vote
Accepted

What's the idiomatic way to instantiate a tuple of evars in Ltac2?

I think you are looking for something like this: ...
Jason Gross's user avatar
  • 1,537
1 vote
Accepted

How do I define an induction principle for a type with a nested list of tuples?

Concerning your question in a comment about Equal : _ -> _ -> Prop, this is how I would proceed, using an inductive predicate: ...
Dominique Larchey-Wendling's user avatar
1 vote

How do I define an induction principle for a type with a nested list of tuples?

Allow me to give a “these are not the droids you're looking for” answer. A record is a mapping from field labels to corresponding values. A list of pairs, such as the one you are using, is not a ...
Andrej Bauer's user avatar
  • 9,104
1 vote
Accepted

What does `induction ... in ...` do in Coq?

Since you have added a follow-up question, I think wrapping all the comments in this answer might be clearer. What does the part in e'' in ...
Hiroki Chen's user avatar
1 vote

My Inductive function over a pair of lists gives "Cannot guess decreasing argument of fix."

Let me give a more complete answer. It recollects some code that you can find in the library Kruskal-Trees that I specifically designed to deal with various kinds ...
Dominique Larchey-Wendling's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible