Skip to main content
Share Your Experience: Take the 2024 Developer Survey
42 votes
Accepted

Why are mathematical proofs so hard?

I feel like i am memorizing the proofs rather than learn how to prove You can't learn "how to prove". "Proving" is not a mechanical process, but rather a creative one where you ...
Tom van der Zanden's user avatar
18 votes
Accepted

What is induction-induction?

Supplemental 2016-10-03: I mixed up induction-induction and induction-recursion (not the first time I did that!). My apologies for the mess. I updated the answer to cover both. I find the ...
Andrej Bauer's user avatar
  • 30.8k
14 votes
Accepted

Trying to understand this Quicksort Correctness proof

We are indeed assuming $P(k)$ holds for all $k < n$. This is a generalization of the "From $P(n-1)$, we prove $P(n)$" style of proof you're familiar with. The proof you describe is known as the ...
Rick Decker's user avatar
  • 14.8k
12 votes

Why are mathematical proofs so hard?

As other authors have mentioned, partly because proofs are inherently hard, but also partly because of the cold fact that proofs are not written for the purpose of teaching, even in most textbooks. ...
apen's user avatar
  • 369
11 votes

Why are mathematical proofs so hard?

I can certainly recommend the book of G. Polya's, How to Solve It. It is a standard classic, not to be missed. There is a newer book How to Read and Do Proofs: An Introduction to Mathematical Thought ...
Elliot's user avatar
  • 211
7 votes

Trying to understand this Quicksort Correctness proof

This proof uses the principle of complete induction: Suppose that: Base case: $P(1)$ Step: For every $n > 1$, if $P(1),\ldots,P(n-1)$ hold (induction hypothesis) then $P(n)$ also holds....
Yuval Filmus's user avatar
6 votes

How does one know what statements in Coq require Induction?

Coq allows one to prove mathematical theorems in a completely formal way. At first, this copes with our experience of doing maths, which is far more informal. Most of the time, people doing maths are ...
chi's user avatar
  • 14.6k
5 votes

How to prove that the reversal of the concatenation of two strings is the concatenation of the reversals?

Well, consider the following "proof" (I'll explain afterwords why the quotation marks): Let $w=a_1\cdots a_n$ be a word, then we have that $w\in (L_1L_2)^{\mathrm{rev}}$ iff $a_n\cdots a_1\in ...
Shaull's user avatar
  • 17.2k
5 votes
Accepted

Lambda Calculus inductive substitution definition

"If one deletes $(\mathrm{d})$ and allows bound variables to be substituted..." The problem here is that substitution of a bound variable makes little sense, since one substitutes a variable (let's ...
Anton Trunov's user avatar
  • 3,479
5 votes

How does one know what statements in Coq require Induction?

As the others have mentioned, in Coq's standard library (or typical presentations of naturals in Coq), naturals are defined inductively, usually a la Peano. We could make other choices, e.g. one could ...
Derek Elkins left SE's user avatar
4 votes

Trying to understand this Quicksort Correctness proof

The missing part of the argument is transitivity of '<' - i.e the property that if a < b and b < c, then a < c. The proof that the final array is sorted goes something like this: Let A[i]...
PMar's user avatar
  • 41
4 votes

Lambda Calculus inductive substitution definition

First of all, you can't always define a substitution for bound variables. Having $[x/y](\lambda y.\ y) = \lambda x.\ x$ may look appealing, but there's no real way to replace the bound variable in $[(...
chi's user avatar
  • 14.6k
4 votes

Proving property of a term using Induction

A term is defined recursively. You can do induction on recursive types, using structural induction. For instance, suppose we say that a term is something of the form $c$ (a constant), or $t_1+t_2$, ...
D.W.'s user avatar
  • 161k
4 votes
Accepted

How to use structural induction to prove law on lists

You'll want a helper lemma to make this endeavor more digestible. Notations for map and subs: I'm going to condense the ...
Lee's user avatar
  • 1,097
4 votes
Accepted

Induction rules for reflexive, transitive closure

Here's a fully formal articulation in the language of Agda. First, inductive rules correspond to indexed families. ...
Derek Elkins left SE's user avatar
4 votes
Accepted

Prove that the number of full nodes plus one is qual to the number of leaves in a nonempty binary tree

Well, an induction proof consists of a base case and an induction step. For trees that is usually structural induction, based on inductive ways trees are built. The base case considers the smallest ...
Hendrik Jan's user avatar
  • 30.8k
4 votes

Why does the denotational semantics for a while loop have a existence quantifier?

The existential quantifier is misplaced. This is due to lack of reasonable notation for what needs to be expressed, namely: "if there is $i$ safisfying condition $C$, then use that $i$", where we make ...
Andrej Bauer's user avatar
  • 30.8k
4 votes
Accepted

Induction to prove equivalence of a recursive and iterative algorithm for Towers of Hanoi

Let's start with reformulating the two solutions, following Wikipedia. We use A for the source peg, B for the auxiliary peg, and C for the destination peg. Recursive algorithm If $n > 1$, ...
Yuval Filmus's user avatar
4 votes
Accepted

Which inductive schemes can encode the following Agda definition?

No scheme that I know of directly encodes that type. Sometimes it's called a "nested" inductive definition. The complication here is that Maybe and ...
András Kovács's user avatar
4 votes

Why are mathematical proofs so hard?

I like Tom's answer: there's no magic bullet but you just need to continue doing exercises and gradually you will develop a better intuition and know how to attack a problem. As for resources, you ...
Juho's user avatar
  • 22.6k
4 votes

Why are mathematical proofs so hard?

Why are mathematical proofs so hard?... I have to learn data structures and algorithms, My guess is you'll also want to learn about algorithms' space and time complexity, as quantified in big O ...
J.G.'s user avatar
  • 237
4 votes
Accepted

Is this graph Hamiltonian?

The complete digraph of $n$ nodes, $K_n$ has $n(n-1)$ edges. Describe a digraph of $n$ nodes with $n(n-1)-\delta$ edges as a digraph "with $\delta$ edges removed". A proof by induction The ...
John L.'s user avatar
  • 39k
3 votes

Can you apply the induction hypothesis to its outcome?

As stated, the reasoning does not make much sense to me. You claim that, in your specific case, you have $a < b \wedge P(a) \Longrightarrow \exists c < b$ $P(a) \wedge P(b) \Longrightarrow P(b)...
chi's user avatar
  • 14.6k
3 votes
Accepted

Proof of correctness of algorithms (induction)

how do I include the if else statement in the proof? In this example, the if statement describes the basic case and the ...
hengxin's user avatar
  • 9,561
3 votes

How to find whether a grammar's language is finite or infinite?

I recall from the 1960's a technique for at least some classes of formal grammars for finding cycles (loops generating an infinite language ) in a grammar. A Boolean matrix is created for all ...
I recall from the 1960's's user avatar
3 votes
Accepted

Why do I need a base case for n=3 when solving a d&c recurrence?

They do not want $T(1)$ to occur as a base case as it causes troubles. $T(3)$ depends on $T(1)$, so if they didn't take $T(3)$ as a base case in addition to taking $T(2)$ as one, they'd run into ...
Tom van der Zanden's user avatar
3 votes

Is structural induction on terms applicable when a function is involved?

You probably shouldn't write $\cfrac{\phi(t)\Downarrow \phi(u)}{t\Downarrow u}$ for "For any terms $t,u$, $\phi(t)\Downarrow \phi(u)$ implies $t\Downarrow u$". I'll take a concrete example: Terms are ...
xavierm02's user avatar
  • 1,255
3 votes
Accepted

How do I approach inductive design problems with no information or context given?

It seems to me that your teacher wants a induction proof where the induction is on the length of the array. It seems weird that your teacher does not provide a sorting algorithm . If the task is to ...
Gabriel Tigerström's user avatar
3 votes

Induction rules for reflexive, transitive closure

No. Induction rules for this case look like this: Let $P$ be some property of relations on $A$ (you already know some examples of such properties: symmetry, transitivity, etc.). To show that $P(\...
Alexey Romanov's user avatar
3 votes
Accepted

Induction on typing derivation in refinement types system

It's a form of structural induction. As we see on page 12 of the text, the typing relation is defined inductively by four rules. For example, the rule abs says that given a deduction $\Gamma, x:r \...
Daniel Mroz's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible