# Tag Info

42

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 have to invent a new technique to solve a given problem. A professional mathematician could spend their entire life attempting to prove a given statement and ...

16

It is an illusion that the computation rules "define" or "construct" the objects they speak about. You correctly observed that the equation for $\mathrm{ind}_{=_A}$ does not "define" it, but failed to observe that the same is true in other cases as well. Let us consider the induction principle for the unit type $1$, which seems particularly obviously "...

16

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 explanations in the Forsberg & Setzer's paper A finite axiomatisation of inductive-inductive definitions illuminating. Induction-recursion An inductive-recursive ...

13

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 principle of strong mathematical induction and has the form Suppose that $P(n)$ is a predicate defined on $n\in \{1, 2, \dotsc\}$. If we can show that $... 12 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. Rather, most proofs are written out of a kind of obligation, as a sort of run-away argument; not presenting proofs at all is considered unacceptable, but writing ... 11 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 Processes by Daniel Solow that may be more accessible. In any event doing proofs is entirely Unnatural for humans. It is a discipline that requires careful ... 10 Short answer: Proof by induction is correct because we define the natural integers as the set for which proof by induction works. On your interpretations and examples Your understanding seems broadly correct, though there are a few places where your statements are not fully rigorous. Given that we're talking about logic, getting things precisely right is ... 8 A language is infinite if it can generate infinitely many words. In order to prove that a language generated by a grammar is infinite, you need come up with some infinite list of words generated by the grammar. Proving that the language is finite is slightly more messy—you need to make a list of all possible derivations, and show that all of the ... 7 I'm no HoTT person, but I'll throw in my two-cents. Suppose we are wanting to make a function $$f_A : \prod_{x,y : A}\prod_{p : x =_A y} C(x,y,p)$$ How would we do this? Well, suppose we're given any$x,y : A$and a proof of their equality$p : x =_A y$. Since I know nothing about the arbitrary type$A$, I know nothing about the `structure' of$x,y$. ... 7 it looks like we are assuming l2 doesn't change in the induction case. But when we later apply it with l2:=l1, we are breaking this assumption. No. If we regard l1 to be a value which is repeatedly decreased in the induction proof, note that we let l2 to be equal to the initial value of l1 -- such value will not change in the induction steps. In other ... 7 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. Then$P(n)$holds for all$n \geq 1$. You can prove this principle using the usual induction principle by considering the property $$Q(m) \... 6 The only way a finite system (grammar) can generate an infinite set of words is by repeating stuff: you start at S and keep expanding until you hit a non-terminal that you've already expanded. So now you can just copy the sub-tree corresponding to that symbol and paste it. You can do this forever so it must be that the grammar generates infinitely many ... 6 Let me try to clarify a point that seems to be confusing you: you seem to be conflating 2 related, but different concepts. The first is the concept of a proof system, which allows you to specify and prove theorems about mathematics or computer science. Dependent types are one elegant way to do this, where the types are the specification language and the ... 6 (1) We are just using this general theorem to prove a special case, we don't change anything here. When we use this coq construction apply app_length_cons' with (l1:=l1) (l2:=l1). we just in some sense instantiate this universally quantified formula$$ \forall l_1, l_2. \mid l_1 \cdot (x :: l_2) \mid~=~succ \mid l_1 \cdot l_2 \mid $$with l_2 = l_1: ... 5 Claim: The algorithm, Fibonacci(n) is correct (Proof by Strong Induction) Base Case: for inputs 0 and 1, the algorithm returns 0 and 1 respectively. So this is Correct. Induction Hypothesis: Fibonacci(k) is correct for all values of k \leq n, where n,k\in \mathbb{N} Inductive Step: let Fibonacci(k) be true for all values until n From IH, ... 5 (Seems like it may be a duplicate, but the "Related" questions don't seem to be too close, with the possible exception of "this one) The proof is by induction on n. Consider the cases n = 0 and n = 1. In these cases, the algorithm presented returns 0 and 1, which may as well be the 0th and 1st Fibonacci numbers (assuming a reasonable definition of ... 5 There are two basic induction patterns for (non-empty) full binary trees: A tree is either a leaf or consists of a root and two full binary subtrees. A tree is either a leaf or can be obtained from a smaller full binary tree by adding two children to a leaf. Your first question can be proved in both ways. In both cases, the base case is clear: if a tree is ... 5 "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 forget for a moment it should be free) with a term, which may very well be an abstraction or application, but not a variable. Let me illustrate this by example. ... 5 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 L_1L_2, iff there exists 0\le k\le n such that a_n\cdots a_k\in L_1 and a_{k-1}\cdots a_1\in L_2, iff there exists 0\le k\le n such that a_k\cdots a_n\... 5 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 not exposed to mathematical logic. They do not know, for instance, how to define the set of real numbers. Or even the set of natural numbers. Numeric sets are ... 5 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 imagine defining naturals as the free semiring on one generator which would give you many of the "axiomatic" facts for "free". (Well, you'd have to prove them ... 4 The language is infinite iff its grammar can generate an infinite number of words, or equivalently iff a recognizing automaton can recognize an infinite number of words. This is something that you have to prove. For that purpose you can rely on some facts. a language is infinite if and only if contains words of unbounded length, i.e. longer than any size ... 4 There is no induction needed. There is only one transition reaching the final state q_2, namely q_1 \xrightarrow{b} q_2. Furthermore, every transition reaching q_1 is labelled by a. It follows that every word accepted by the automaton has to end by ab. It remains to prove that, conversely, any word of the form uab is accepted. After reading u ... 4 Part of your intuition is correct: "terms" really means "the collection of terms generated thus far". I think you will also find in Pierce a definition that makes this explicit on the next page (Definition 3.2.3). What Pierce is actually doing is giving three equivalent and common ways of presenting syntax. In fact, the first one (page 24) is what you often ... 4 Well, we don't really need induction here. We want to prove that for any language L holds the statement$$\left( L^R \right)^R = L.$$(1) Let$s \in \left( L^R \right)^R$. Then there exists a (unique) string$t \in L^R$, such that$s = t^R$. The situation is analogous with$t$: there exists a (unique) string$u \in L$such that$t = u^R$. From that we ... 4 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$[(xx)/y](\lambda y.\ y)$since$\lambda$wants a variable, not a term. (As Anton Trunov points out above) It is true however that the$\lambda$rules in the ... 4 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], A[j] be elements of the array post-sort, where i < j. Then A[i] < A[j] follows from one of the following placement cases (and there are no other cases)... 4 You'll want a helper lemma to make this endeavor more digestible. Notations for map and subs: I'm going to condense the map notation a bit so that we can express it as the binary operator$f \diamond l = \mathrm{map} ~ f ~ l$. Similarly, we will express the subs as a unary operation$\lfloor\!\!\lfloor l \rfloor\!\!\rfloor = \mathrm{subs} ~ l$. This might ... 4 Here's a fully formal articulation in the language of Agda. First, inductive rules correspond to indexed families. data Star {A : Set}(R : A → A → Set) : A → A → Set where Refl : {a : A} → Star R a a Trans : {a b c : A} → Star R a b → R b c → Star R a c Here the Refl data constructor corresponds to your first rule, and the Trans data constructor ... 4 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 binary tree, which cannot be composed further. Show that one has the Property. The induction step argues that the Property is true for any tree$T\$ assuming the ...

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