Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math
On 02/11/2019 19:10, Rob Arthan wrote: If I need to work with the rationals I just treat them as a subset of the reals. Though I think for these examples even that is an unnecessary complication, since the proof over the reals as a whole will be closest (apart from the actual types) to what a proof for the rationals would look like. And the original seems ambiguous about types. Roger PS: my 0 < r < 1 suggestion seems unnecessary. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math
Roger, David, > On 2 Nov 2019, at 18:45, Roger Bishop Jones wrote: > > Oops. > > On 02/11/2019 17:25, Roger Bishop Jones wrote: >> How about working in theory "ℚ"? > Great idea, apart from the fact that it doesn't exist! That's right: we don't provide a type ℚ of rationals. The approach I took to defining the type ℝ of reals doesn't construct the rationals first. A type of rationals could easily be provided as a subtype of the reals, but I have never felt the need for it: if I need to work with the rationals I just treat them as a subset of the reals. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math
Oops. On 02/11/2019 17:25, Roger Bishop Jones wrote: How about working in theory "ℚ"? Great idea, apart from the fact that it doesn't exist! Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math
David, Thanks for the reference to the text you are working from, it makes it much clearer what you are trying to do. In example 9.2 I think he should stipulate 0 < r < 1 not just r not= 1. I think strictly speaking if you work with real numbers you are not doing discrete maths, but I don't know how much that matters to you. ( /"Discrete mathematics/is the study of/mathematical/structures that are countable or otherwise distinct and separable." This seems the most popular definition.) However, the examples in 9.2 don't require real numbers, since he is only dealing with finite sums, not taking limits, so the numbers here could be the rational numbers ℚ, and the induction is over the natural numbers. How about working in theory "ℚ"? (that's still discrete by the above criterion). As to utf8, it is likely that the next release of ProofPower will work with utf8, and in the interim there is a ProofPower contrib which contains programs for converting between ProofPower ext character set and utf8. I can't see anywhere that pputf8 can be downloaded, so you might have to clone the github depository at: https://github.com/RobArthan/pp-contrib Then look for build instructions in src/pputf8. Alternatively, look here for Rob's previous advice: http://lemma-one.com/pipermail/proofpower_lemma-one.com/2016-August/002345.html Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math
David, Looking further at what you are trying to prove, its clear that, though you can have geometric sequences over the naturals, this kind of result will not be obtainable in that context. As soon as you thing of them as series, things go awry, since non but the absolutely trivial ones converge. So if you want to reason about these things then you will need real numbers and can best work from maths_egs. However the leap from the kind of reasoning you have been doing to formal proof in analysis is very great (also, if it matters to you, this is no longer discreet mathematics!) and I would have thought that carrying through some arithmetic proofs would be a more manageable advance for you. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Proofpower Digest, Vol 119, Issue 1
David, > On 1 Nov 2019, at 16:13, David Topham wrote: > > Ok, I can work within integers for awhile! I was trying to use the general > form of the geometric progression that may involve fractions, but I can > explore whole numbers more first. As an aside from what Roger has been trying to help with, you may also like to look at the treatment of sequences and series in the document wrk066.doc in the mathematical case studies that deals with some basic analysis. Sequences are modelled as functions ℕ → ℝ. The following function is defined to convert a sequence s into the series comprising the sequence of partial sums s_0 + s_1 + … + s_n. ⓈHOLCONST │ ⦏Sigma⦎ : (ℕ → ℝ) → (ℕ → ℝ) ├── │ (∀s⦁ Sigma s 0 = ℕℝ 0) │ ∧ (∀s n⦁ Sigma s (n+1) = Sigma s n + s n) ■ In a similar vein, a function that maps a sequence of coefficients to the corresponding power series is defined as follows: ⓈHOLCONST │ ⦏PowerSeries⦎ : (ℕ → ℝ) → (ℕ → ℝ → ℝ) ├── │ ∀s n⦁ PowerSeries s n = PolyEval (s To n) ■ where s To n is the list comprising the first n elements of the sequence s and PolyEval maps a list of coefficients to the corresponding polynomial function: ⓈHOLCONST │ ⦏PolyEval⦎ : ℝ LIST → (ℝ → ℝ) ├── │ (∀x⦁ PolyEval [] x = ℕℝ 0) │∧ (∀c l x⦁ PolyEval (Cons c l) x = c + x * PolyEval l x) ■ When you are reasoning about these things, you can do induction over the index of a sequence, because that’s a natural number. The theory includes the usual results on geometric series: :) geometric_sum_thm; val it = ⊢ ∀ n x⦁ ¬ x = 1. ⇒ Sigma (𝜆 m⦁ x ^ m) (n + 1) = (1. - x ^ (n + 1)) / (1. - x): THM :) geometric_series_thm; val it = ⊢ ∀ x⦁ ~ 1. < x ∧ x < 1. ⇒ (𝜆 n⦁ PowerSeries (𝜆 m⦁ 1.) n x) -> 1. / (1. - x): THM Regards, Rob ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math
David The ascii may not be readable, but it can be converted back to ext, or to utf8: ⓈHOLCONST │ sum:ℕ→ℕ ├── │ ∀n⦁ sum 0 = 0 ∧ sum (n) = n + (sum n-1) ■ ⓈHOLCONST │ pow:ℕ→ℕ→ℕ ├── │ ∀b e⦁ (pow b 0) = 1 ∧ (pow b e) = b * (pow b (e - 1)) ■ =SML val ex92 = ⌜λ n r⦁ sum (pow r n) = (1 - (pow r (n - 1)) Div (1 - r))⌝; val UI = ∀_elim ex92 induction_thm; val lemma1 = rewrite_rule [] UI; putting in utf8 would be better, but you probably wouldn't find that easy. (the next release of ProofPower will make it easier) To understand why your definitions don't work, consider what they say when you instantiate n or e to 0. You get conflicting and nonsensical assertions about sum 0 and pow b 0. When you use similar definitions in SML its OK because execution is sequential and the second reading is never reached (for the zero argument), but in logic you can reach the second clause and you can derive a contradiction. Also, it is now clear (even though you don't actually state your goal), that you are trying to reason about the sum of a segment of series, but the function "sum" you have (almost) defined gives the sum of an initial segment of the natural numbers, not of an arbitrary series. The "sum" you want takes a function as well as a number, so it has type: sum:(ℕ→ℕ) → ℕ → ℕ When it comes to doing induction, apart from the need to chose the proposition carefully which I mentioned earlier, you obtain the required property by eliminating only the outermost universal, so you would have: val ex92 = ⌜λ n⦁ ∀r⦁ sum (pow r n) = (1 - (pow r (n - 1)) Div (1 - r))⌝; Then you would have a term of the right type to instantiate induction thm. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
