Tag Info

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
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 ...
• 982

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: <...
• 982
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. ...
• 420
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,316

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 ...
Accepted

Strong induction for nat in Coq

A classic solution is to define a stronger property, which you prove by induction. ...
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 ...
Accepted

Coq Induction on Hypothesis destroys the Hypothesis

The induction tactic tends to forget about the values of concrete arguments (e.g., nil on ...
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! ...
• 5,530

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

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,547
Accepted

How can I prove this theorem with induction in Coq?

The beginning of the proof looks as follows: ...
• 2,320

...

How can I prove this theorem with induction in Coq?

It comes out quite concisely with the use of ArithRing. ...
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). ...

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 ...
• 476
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 ...
• 9,842

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 ...
• 420
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 ...
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,316
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 ...
1 vote

Two-step induction of inductive predicate on Streams

Do you mean the induction principle generated by the following definition ? ...
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 ...
1 vote

How do I approach the final inductive step in plus_leb_compat_l from Software Foundations?

You could try to do the induction on p instead of n.

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