Skip to main content

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
2 votes
1 answer
85 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: ...
Jay Lee's user avatar
  • 123
3 votes
3 answers
217 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 ...
Glyn Webster's user avatar
0 votes
0 answers
26 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. ...
Mark Pock's user avatar
1 vote
0 answers
125 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: ...
camsterwheel's user avatar
3 votes
1 answer
381 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): ...
tinlyx's user avatar
  • 2,034
3 votes
1 answer
99 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: ...
Dave's user avatar
  • 175
2 votes
1 answer
64 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 ...
Thanasis's user avatar
1 vote
1 answer
122 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 ...
noCrayCray's user avatar
2 votes
1 answer
172 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: ...
Circuit Craft's user avatar
-2 votes
2 answers
114 views

Help with strong induction

I have the following definition of divisibility by 3. ...
deleted_user0972's user avatar
0 votes
1 answer
163 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? ...
deleted_user0972's user avatar
-5 votes
1 answer
249 views

How do I prove this theorem with induction in COQ

...
HELLOBIRD 892's user avatar
2 votes
1 answer
89 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 ...
asha soroushpoor's user avatar
1 vote
3 answers
151 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 ...
matteo_c's user avatar
  • 131
1 vote
3 answers
222 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: ...
Charles Averill's user avatar
1 vote
1 answer
620 views

Strong induction for nat in Coq

I'm doing some exercises on Coq and trying to prove the strong induction principle for nat: ...
Pavel Snopov's user avatar
5 votes
1 answer
176 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. ...
Joey Eremondi's user avatar
3 votes
4 answers
743 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 ...
Nova Sczerin's user avatar
12 votes
1 answer
475 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 ...
Ms. Molly Stewart-Gallus's user avatar
2 votes
1 answer
174 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, ...
Wno-all's user avatar
  • 1,108
5 votes
1 answer
89 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 ...
Wno-all's user avatar
  • 1,108