New answers tagged inductive-type
1
vote
Uniqueness of proofs for inductively defined predicates
Here is a proof that is somehow self-explaining. Jean François Monin and I reworked it about two years ago. Below is an Ltac style proof script. The keywork is of course dependent pattern matching for ...
5
votes
Accepted
-2
votes
Uniqueness of proofs for inductively defined predicates
The principle of proof irrelevance cannot be proved in Coq, but we can introduce axiom proof_irrelevance from https://coq.inria.fr/library/Coq.Logic....
1
vote
Accepted
Formalizing "finite or infinite" in Coq
The problem
Informally, we want a type of "finite or infinite sequences", henceforth "runs", with the following form:
The finite runs:
...
- 248
2
votes
Formalizing "finite or infinite" in Coq
Another way to approach the problem is to characterize isFinRun inductivelly and to define run_to_pos by structural induction on ...
4
votes
Formalizing "finite or infinite" in Coq
Since the error you encountered is that you can't deconstruct a proof term whose type's type is Prop to construct the value whose type's type is ...
- 2,032
2
votes
Formalizing "finite or infinite" in Coq
This is my second attempt to solve the problem, it is completely different from the first.
Would it be fix the problem to pass in an upper bound of the length and a proof that that length is correct?
<...
- 3,095
Top 50 recent answers are included