# Tag Info

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 $... 13 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 ... 12 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 "... 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 The authors give the answer: The error is that we have not proved the exact form of the inductive hypothesis, that is, that$T(n) \leq cn$. Granted, that is hard to understand if you are not used to do inductions (right), because they do not do the induction explicitly/rigorously. In short: you need to have one constant$c$for all$n$, but this (un)... 7 You need to do a proof by induction on$n + r$. Let$P(m)$be the statement "for any$n,r \geq 1$satisfying$n+r = m$,$\mathrm{multiply}(n,r) = nr$. The proof by induction goes along the following lines. Base case:$m=2$, so$n=r=1$. By inspection,$\mathrm{multiply}(1,1)=1$. Induction step: suppose$P(m)$is true for some$m \geq 2$, and let$n,r\geq 1$... 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 No, but not for the reasons other people have given. The difference between recursion and induction is not that recursion is "top-down" and induction is "bottom-up." Induction is isomorphic to something called "primitve recursion," but, in general, recursion is strictly more powerful than induction. The distinction between top-down and bottom up is trivial -... 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 (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 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, ... 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 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 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 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 ...