Questions tagged [induction]
Tag for questions about induction such as mathematical induction, structural induction or well-founded induction (Noetherian).
14
questions
1
vote
1
answer
56
views
İnduction/inversion and others in coq
I'm trying to learn Coq using the software foundations. I somehow made it to the 2nd volume but I'm struggling writing proofs on my own. Especially whether I should be using inversion or induction.
I ...
- 51
2
votes
1
answer
128
views
Induction scheme on two arguments for custom type in Coq
I've been working on formalizing a Hilbert deductive system within Coq. I have the following definition for a term in first-order logic:
...
- 195
-2
votes
2
answers
78
views
Help with strong induction
I have the following definition of divisibility by 3.
...
0
votes
1
answer
131
views
Induction COQ Question
Just practicing some induction proofs and was wondering what would be the fastest and most effective way to solve this proof and proofs similar to this?
...
-4
votes
1
answer
183
views
1
vote
1
answer
68
views
Coq Induction on Hypothesis destroys the Hypothesis
I'm trying to prove something in coq
I have and Inductive prop type named in_order_merge which is a relation between three lists that shows third one is in_order merge of first two, here is the ...
1
vote
3
answers
89
views
Two-step induction of inductive predicate on Streams
If I want to have an induction principle for nats from n to n+2, I can define and prove this ...
- 131
1
vote
3
answers
135
views
How do I approach the final inductive step in `plus_leb_compat_l` from Software Foundations?
I'm provided with this theorem from the Software Foundations textbook:
...
- 155
1
vote
1
answer
411
views
Strong induction for nat in Coq
I'm doing some exercises on Coq and trying to prove the strong induction principle for nat:
...
- 195
5
votes
1
answer
160
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.
...
- 773
3
votes
4
answers
633
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
...
- 41
12
votes
1
answer
394
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,768
2
votes
1
answer
145
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, ...
- 1,088
5
votes
1
answer
77
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 ...
- 1,088