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 ...
- 13.4k
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 ...
- 31.2k
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. ...
- 379
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 ...
- 211
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 ...
- 14.7k
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 ...
- 12.1k
5
votes
Is there a fully combinatorial version of MLTT without lambda abstraction?
You need a termination checker to translate recursive pattern-matching definitions into corresponding uses of eliminators (recursion/induction principles). This has nothing to do with $\lambda$-...
- 464
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 ...
- 1,097
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 ...
- 31.1k
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.♦
- 166k
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.
...
- 12.1k
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 ...
- 31.2k
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$, ...
- 279k
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 ...
- 948
4
votes
Accepted
When can the coinduction hypothesis be used?
First, let me recall least and greatest fixed points for $\subseteq$. We are working relative to some set $U$, the universe. In the case of (co)inductive definitions, $U$ is the set of all terms. A ...
- 2,328
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 ...
- 22.8k
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 ...
- 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 ...
- 39.1k
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(\...
- 3,192
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)...
- 14.7k
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 ...
- 1,255
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 ...
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 ...
- 9,631
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 \...
- 376
3
votes
Accepted
How to prove even with structural induction, for expression
To prove a property p by structural induction on your E, one has to prove
p(zero)
...
- 14.7k
3
votes
Why does the denotational semantics for a while loop have a existence quantifier?
The intuition is that the loop terminates at the $i$th iteration if the loop condition is false at that iteration but true at all earlier ones. If the loop condition is never false, then the loop ...
- 82.2k
3
votes
How does one know what statements in Coq require Induction?
To see how you can prove something about natural numbers, you must know what you know about natural numbers. Usually, we learn all sorts of 'basic facts' about numbers in high school that are pretty ...
- 8,332
3
votes
How does one know what statements in Coq require Induction?
I want to share my own experience of learning Coq and theorem proving in general.
Most of the time, the proof of a statement largely depends on the recursive structure of the function or operation at ...
- 508
3
votes
Accepted
Deriving recursive definition from function specification
Your notation and understanding are pretty good.
It is easier to consider (xs:x) as the inductive case instead of (x:xs)
\...
- 39.1k
3
votes
Accepted
on coq: Why is the proof complete after proving only for one induction when we have more than one variable?
You do not have to prove things by induction. For example, you can prove $\forall n : \mathbb{N} \,.\, n = n$ without induction by applying reflexivity. In your proof, we use induction on $a$, but ...
- 31.2k
Only top scored, non community-wiki answers of a minimum length are eligible