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
3 votes
3 answers

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 ...
user avatar
10 votes
1 answer

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 ...
user avatar
2 votes
1 answer

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, ...
user avatar
  • 898
5 votes
1 answer

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 ...
user avatar
  • 898