# Questions tagged [induction]

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

23 questions
Filter by
Sorted by
Tagged with
41 views

### STLC substitution behaviour with lambda body normalisation

UPDATE 31/07/'24 12.57: It is false: Assume v, w, x, y, z all type variables. Take t = (\y. y) (x w) --> x w = t', then ...
124 views

### Is the validity of induction in Coq axiomatic?

When one defines an inductive type in Coq, for example, natural numbers, Inductive nat : Set := | O : nat | S : nat -> nat. Coq automatically creates an ...
• 33
105 views

### What does induction ... in ... do in Coq?

I'm self-studying the Semantics course, and met the following proof script in the warmup directory: ...
• 153
235 views

### My Inductive function over a pair of lists gives "Cannot guess decreasing argument of fix."

This is the smallest example that causes the problem. It should decrease, but I don't know how to reassure Coq that it will. I'm going to have to compare lots of lists of pairs for what I'm doing so ...
27 views

### Inductive assumption in inductive case

likely stupid question here, I'm sure, but I have been trying fruitlessly with little success to figure this problem out. Here is a toy example. Suppose we have this. ...
1 vote
127 views

### Trouble proving a theorem using induction in Coq

Theorem five_and_three: forall i, exists a b, i + 8 = 3 * a + 5 * b. I'm currently using these tactics: ...
396 views

### How to provide proof for termination in Agda?

I am trying to write an integer division function from scratch in agda2 (as of 2.6.3): ...
• 2,236
102 views

### Stuck in a proof about sum types and nonempty lists

I have a hard time proving an apparently simple property or finding a counterexample. It is about sum types and nonempty lists. I first define two basic functions about sum types: ...
• 175
83 views

### Inductively proving that a number is either even or odd in Lean

I have the following Lean definitions: def is_even (a : Nat) := ∃ m, a = 2 * m def is_odd (a: Nat) := ∃ m, a = 2 * m + 1 The following proof would be complete if I ...
• 23
1 vote
149 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 ...
184 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: ...
123 views

### Help with strong induction

I have the following definition of divisibility by 3. ...
200 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? ...
254 views

...
94 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
169 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
239 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: ...
1 vote
659 views

### Strong induction for nat in Coq

I'm doing some exercises on Coq and trying to prove the strong induction principle for nat: ...
• 205
178 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. ...
760 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 ...
494 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 ...
177 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,128