9
votes
How can I prove this theorem with induction in Coq?
There have been several good answers to this question, so I'm not trying to compete with them, but rather offer a peculiar angle on this problem as food for thought and potential for a useful library ...
- 771
8
votes
Accepted
Is induction over mutually inductive coinductive types possible?
It makes sense to want something like this, but Agda's termination/productivity checker does not actually validate this interpretation of the types. The reasoning behind your induction principle is ...
- 1,002
7
votes
Accepted
6
votes
Strictly-monotone "max" operation for constructive Brouwer-trees?
You can define a max that will be better behaved by induction on x and y. Something like:
<...
- 1,002
6
votes
Accepted
How to provide proof for termination in Agda?
There are three possible approaches:
Use a different algorithm, like division in stdlib, see div-helper.
Use the well-founded induction library. There are many ...
- 6,532
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.
...
- 430
4
votes
Accepted
Strong induction for nat in Coq
A classic solution is to define a stronger property, which you prove by induction.
...
- 683
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 ...
3
votes
Accepted
Stuck in a proof about sum types and nonempty lists
I don't have Coq installed to check, but I believe cons (inr (inl 1)) (sngl (inl 2)) should be a counterexample as ...
- 146
3
votes
Accepted
Coq Induction on Hypothesis destroys the Hypothesis
The induction tactic tends to forget about the values of concrete arguments (e.g., nil on ...
3
votes
Accepted
Induction scheme on two arguments for custom type in Coq
Coq complains with reason: there is a priori no reason why the number of arguments of the two functions you are comparing have to be the same. And, indeed, you lemma is false!
...
- 6,028
3
votes
Defining Lists and Prove Associativity of Append
Here's a little list module written in Adga. To do this we are going to need cong -rule, and it resides in PropositionalEquality -module.
...
- 731
3
votes
General Guidelines and Tips for using Induction
The best guideline is: If you don't know how to do the proof on pen-and-paper, you probably will get lost doing it in a proof assistant. If you don't know what your induction hypothesis is supposed ...
- 1,607
2
votes
Accepted
How can I prove this theorem with induction in Coq?
The beginning of the proof looks as follows:
...
- 2,330
2
votes
How can I prove this theorem with induction in Coq?
It comes out quite concisely with the use of ArithRing.
...
2
votes
Accepted
How do I approach the final inductive step in `plus_leb_compat_l` from Software Foundations?
Induction on p, as Pierre Jouvelot suggests, makes this proof much easier (the challenge is recognising it but it will come with experience).
...
- 268
2
votes
How do I prove this theorem with induction in COQ
You can take advantage of the ring tactic that can prove equality modulo associativity and commutativity
...
- 486
2
votes
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 ...
2
votes
Accepted
Is the validity of induction in Coq axiomatic?
The answer is "no, Coq does not introduce an axiom", but this is not the whole story, because type theory does not operate by postulating axioms. Instead, Coq has some primitive building ...
- 11.1k
2
votes
Is the validity of induction in Coq axiomatic?
You could say that induction is a logical consequence of the fact that the inhabitants of an inductive type are fully defined by the list of the constructors.
It would be better to say that the ...
- 121
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 ...
- 430
1
vote
Accepted
Inductive Hypothesis is wrongly generated
Coq will not touch the context surrounding the thing you do the induction on. If your g' changes during the induction (here you want it to become ...
- 191
1
vote
How to target an introduced value set with the set tactic for induction in Coq?
Here is a proof that directly uses well-founded induction:
...
- 6,028
1
vote
How to target an introduced value set with the set tactic for induction in Coq?
Conceptually, when we prove something by induction on $x$, we lose any hypotheses we had on the particular value of $x$ that we wanted to apply this to.
Otherwise here is the kind of nonsensical ...
- 497
1
vote
Accepted
How to target an introduced value set with the set tactic for induction in Coq?
I couldn't figure out any way to do it other than making an assert.
...
- 650
1
vote
Accepted
Inductively proving that a number is either even or odd in Lean
Here's a completed proof, which should be inserted at the place of your sorry:
...
- 6,532
1
vote
İnduction/inversion and others in coq
Intuitively induction is for reasoning about all possible values of an inductive type. Inversion is reasoning about a particular « shape » of a term of an inductive type.
For instance if you have a ...
- 381
1
vote
Two-step induction of inductive predicate on Streams
Do you mean the induction principle generated by the following definition ?
...
- 683
1
vote
How do I approach the final inductive step in `plus_leb_compat_l` from Software Foundations?
Indeed, there is no need to use explicit rewriting. The reductions of
leb (S n) (S m)to leb n m and ...
- 683
Only top scored, non community-wiki answers of a minimum length are eligible