Questions tagged [induction]

Tag for questions about induction such as mathematical induction, structural induction or well-founded induction (Noetherian).

Filter by
Sorted by
Tagged with
1 vote
1 answer
89 views

Strong induction for nat in Coq

I'm doing some exercises on Coq and trying to prove the strong induction principle for nat: ...
6 votes
1 answer
139 views

Strictly-monotone "max" operation for constructive Brouwer-trees?

The Setting I'm trying to use Agda's well-founded ordering to prove that something is terminating using Brouwer Trees i.e. ...
3 votes
4 answers
498 views

How can I prove this theorem with induction in Coq?

Lemma sum_square_p : forall n, 6 * sum_n2 n = n * (n + 1) * (2 * n + 1). where sum_n2 is defined ...
11 votes
1 answer
256 views

Is induction over mutually inductive coinductive types possible?

You can encode ordinals in Coq as Inductive ord := O | S (n: ord) | Lim (s: nat -> ord). Suppose you use the following encoding instead ...
2 votes
1 answer
125 views

Defining Lists and Prove Associativity of Append [closed]

When I saw this question asking what is the "Hello, World!" for proof assistants I immediately thought of that exercise. Not a long time after this answer by Couchy was proposed. Therefore, ...
  • 998
5 votes
1 answer
61 views

General Guidelines and Tips for using Induction

There are many kinds of induction (induction over the natural numbers ⊂ structural induction ⊂ Noetherian induction), when do I use which flavour? And what should I keep in mind when doing proofs by ...
  • 998