Re: [ProofPower] Existential Elimination
Roger, Thank for once again trying to clarify Existential Elimination. Sorry for being to thick-headed, but I still don't get it. What is confusing is the 3 parameters. e.g. In this partial proof, there is only one premise, but you mention 2? > > Message: 2 > Date: Tue, 31 Mar 2020 21:35:59 +0100 > From: Roger Bishop Jones > To: proofpower@lemma-one.com > Subject: Re: [ProofPower] ?_elim > > David, > > The existential rule most closely analogous to universal instantiation > is existential introduction. > The ?_elim rule is more complex, and the name perhaps misleading. > The conclusion is always exactly the conclusion of the second premise. > The existential "eliminated" is the conclusion of the first premise. > But its probably clearer to think of the first premise being used to > eliminate an assumption in the second premise which is a witness to the > existential in the first premise. > > In your proof, the effect realised is to introduce an existential in the > assumptions (in both cases). > > Roger > I think I need a simpler example perhaps. How about this one? Prove ∀x(W(x)⇒R(x)),∃xW(x) ⊢ ∃xR(x) Starting out like this: "Existential Elimination"; val L1 = asm_rule ⌜∃x⦁W(x)⌝; val L2 = asm_rule ⌜W(b):BOOL⌝; val L3 = ∃_elim ⌜x⌝ L1 L2; =GFT val it = "Existential Elimination": string :) val L1 = ∃ x⦁ W x ⊢ ∃ x⦁ W x: THM :) val L2 = W b ⊢ W b: THM :) val L3 = ∃ x⦁ W x, W b ⊢ W b: THM It does seem to be close, but it introduced a new premise W b It I don't do that, what is the third parameter to ∃_elim? It seems I need 2 THMs but only have 1! Thank you in advance for all your wonderful contributions to this software and explanations of how to use it! -Dave ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Law of Cases
I was hoping this would work for applying the Law of Cases to a proof, but it adds q to the list of premises. What could I do to remove that? =SML fun law_of_cases th1 th2 = let val D⇒ (tm,_) = dest_term (concl th1) in asm_elim tm (undisch_rule th1)(undisch_rule th2) end; val L0 = asm_rule ⌜p ∨ q⌝; val L1 = asm_rule ⌜p⇒r⌝; val L2 = asm_rule ⌜q⇒r⌝; law_of_cases L1 L2; =GFT :) val L0 = p ∨ q ⊢ p ∨ q: THM :) val L1 = p ⇒ r ⊢ p ⇒ r: THM :) val L2 = q ⇒ r ⊢ q ⇒ r: THM :) val it = p ⇒ r, q ⇒ r, q ⊢ r: THM ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] ∃_elim
I was restudying this proof suggested by Rob a few years ago and still have a nagging question I am trying to resolve: Here is the complete proof with the output you should see in the comments. val L1 = asm_rule ⌜p(x,y):BOOL⌝; (* val L1 = p (x, y) ⊢ p (x, y): THM *) val L2 = ⌜∃x:'a⦁p(x,y)⌝; (* val L2 = ⌜∃ x⦁ p (x, y)⌝: TERM *) val L3 = ∃_intro L2 L1; (* val L3 = p (x, y) ⊢ ∃ x⦁ p (x, y): THM *) val L4 = ⌜∃y:'b⦁∃x:'a⦁p(x,y)⌝; (* val L4 = ⌜∃ y x⦁ p (x, y)⌝: TERM *) val L5 = ∃_intro L4 L3; (* val L5 = p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *) val L6 = asm_rule ⌜∃y:'b⦁p(x,y)⌝; (* val L6 = ∃ y⦁ p (x, y) ⊢ ∃ y⦁ p (x, y): THM *) val L7 = ∃_elim ⌜y:'b⌝ L6 L5; (* val L7 = ∃ y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *) val L8 = asm_rule ⌜∃x:'a⦁ ∃y:'b⦁p(x,y)⌝; (* val L8 = ∃ x y⦁ p (x, y) ⊢ ∃ x y⦁ p (x, y): THM *) val L9 = ∃_elim ⌜x:'a⌝ L8 L7; (* val L9 = ∃ x y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *) val L10 = ⇒_intro ⌜∃x:'a⦁ ∃y:'b⦁p(x,y)⌝ L9; (* val L10 = ⊢ (∃ x y⦁ p (x, y)) ⇒ (∃ y x⦁ p (x, y)): THM *) I know when we do Universal elimination the quantifier is no longer there, but here for Existential elimination the quantifier remains. Is there a reason for that? e.g. Why is val L7 = ∃_elim ⌜y:'b⌝ L6 L5; (* val L7 = ∃ y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *) not val L7 = ∃_elim ⌜y:'b⌝ L6 L5; (* val L7 = ∃ y⦁ p (x, y) ⊢ p (x, y): THM *) Aren't we selecting y to be witness or example of a y that satisfies p? Like (∃y)Py Py ∃_elim Need to make assumption based on the existentially quantified proposition ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] HOLCONST
I have been able to get the length sample for HOLCONST from user013 to work, but when I try my own function, I get an error. Can anyone see what my problem is? I suspect it may be setting the correct proof context since I needed to add set_pc "hol2" to get the length function to work. I have tried several contexts such as "lin_arith", "R", "misc", but I have not seen how to find the correct one (if that is even the problem). This one OK: :) force_delete_theory "cs113" handle Fail _ => (); val it = (): unit :) open_theory "hol"; new_theory "cs113"; val it = (): unit val it = (): unit :) set_pc "hol2"; val it = (): unit :) ⓈHOLCONST :# │ length:'a LIST→ℕ :# ├── :# │ length [] = 0 :# │ ∧ ∀ h t⦁ length (Cons h t) = length t + 1 :# │ :# ■ val it = ⊢ length [] = 0 ∧ (∀ h t⦁ length (Cons h t) = length t + 1): THM :) get_spec⌜length⌝; val it = ⊢ length [] = 0 ∧ (∀ h t⦁ length (Cons h t) = length t + 1): THM :) rewrite_conv[get_spec⌜length⌝] ⌜length [1;2;3;4]⌝; val it = ⊢ length [1; 2; 3; 4] = 4: THM But not this one: :) ⓈHOLCONST :# │ summ:ℕ→ℕ :# ├── :# │ summ 0 = 0 :# │ ∧ ∀n⦁ summ (n + 1) = (summ n) + (n + 1) :# │ :# ■ val it = ⊢ summ 0 = 0 ∧ (∀ n⦁ summ (n + 1) = summ n + n + 1): THM :# get_spec⌜summ⌝; val it = ⊢ summ 0 = 0 ∧ (∀ n⦁ summ (n + 1) = summ n + n + 1): THM :) rewrite_conv[get_spec⌜summ⌝] ⌜summ 2⌝; Exception Fail * no rewriting occurred [rewrite_conv.26001] * raised ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Proofpower Digest, Vol 120, Issue 1
Rob, I got this, but I had 3 previous posts to mailing list that didn't make it. Were they inappropriate? Or lost? -Dave On Wed, Mar 25, 2020 at 9:00 AM wrote: > Send Proofpower mailing list submissions to > proofpower@lemma-one.com > > To subscribe or unsubscribe via the World Wide Web, visit > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > or, via email, send a message with subject or body 'help' to > proofpower-requ...@lemma-one.com > > You can reach the person managing the list at > proofpower-ow...@lemma-one.com > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Proofpower digest..." > > > Today's Topics: > >1. Testing, testing (Rob Arthan) > > > -- > > Message: 1 > Date: Wed, 25 Mar 2020 15:10:15 + > From: Rob Arthan > To: ProofPower List > Subject: [ProofPower] Testing, testing > Message-ID: > Content-Type: text/plain; charset=us-ascii > > This is a test. If you receive it, please ignore it. > > Regards, > > Rob. > > > > -- > > Subject: Digest Footer > > ___ > Proofpower mailing list > Proofpower@lemma-one.com > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > > > -- > > End of Proofpower Digest, Vol 120, Issue 1 > ** > ___ 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
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. I see the "induction_thm" won't work with R anyway since it has the base case as 0 and SML would expect 0.0 there for domain R (at least that is what I am seeing so far in trying to open_theory R and apply the thm). I am trying wrk074 however open_theory "fincomb" fails so I need to find out how to load that as pre-requisite. On Fri, Nov 1, 2019 at 9:00 AM wrote: > Send Proofpower mailing list submissions to > proofpower@lemma-one.com > > To subscribe or unsubscribe via the World Wide Web, visit > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > or, via email, send a message with subject or body 'help' to > proofpower-requ...@lemma-one.com > > You can reach the person managing the list at > proofpower-ow...@lemma-one.com > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Proofpower digest..." > > > Today's Topics: > >1. Re: (EXTERNAL) Re: ProofPower and Discrete Math > (Roger Bishop Jones) > > > ------ > > Message: 1 > Date: Thu, 31 Oct 2019 22:25:43 + > From: Roger Bishop Jones > To: David Topham , proofpower@lemma-one.com > Subject: Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math > Message-ID: > Content-Type: text/plain; charset="utf-8"; Format="flowed" > > David, > > On 31/10/2019 19:14, David Topham wrote: > > Thank you Roger, that is very helpful.? I found I had to add this line > > to make it work: > > > > (open_theory "cs113" handle _ => (open_theory "hol"; new_theory > "cs113")); > > > > But then my next problem is to work on geometric progressions which > > require real numbers > > > > When I use R->R > > > > I get error message > > > > "type constructor or abbreviation for R not in scope." > > > > I wonder if hol is enough for using R? Or will I need to change or add > > to the ancestor theory I am inheriting from? > You could try the theory "?", which is not an ancestor of HOL. > You are making quite a big leap in complexity, going from arithmetic to > analysis, so things will get harder. > > You can have geometric progressions over the natural numbers, so if the > result you? are looking for actually works in that context, you might be > best to try it there first. > > If not you might benefit from working in one of the theories in > maths_egs, depending on how much analysis you need. > You would need to look at what is available (you can see the listings at > lemma-one.com if you want to check before installing maths_egs) and > decide what is the best context for your work. > see: http://www.lemma-one.com/ProofPower/examples/examples.html > > Even if you stick to the natural numbers, maths_egs has something for > you, the theory "numbers" in wrk074. > > Roger > > -- next part -- > An HTML attachment was scrubbed... > URL: < > http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20191031/826466b6/attachment-0001.html > > > > -- > > Subject: Digest Footer > > ___ > Proofpower mailing list > Proofpower@lemma-one.com > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > > > -- > > End of Proofpower Digest, Vol 119, Issue 1 > ** > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] ProofPower output
Got it, thanks! On Fri, Feb 15, 2019 at 10:39 AM Rob Arthan wrote: > Dave, > > It's done using: > > =GFT ProofPower output > > "=GFT" stands for something like "General Formal Text". The text on the > GFT line is used for the label and the lines coming after a GFT directive > are > just formatted like formal text in theLaTeX document, but not included by > docsml. > I would typically copy text out of the journal window and paste it into > the script > window while writing the document and processing the SML that produces > the output interactively. > > Regards, > > Rob. > > > On 15 Feb 2019, at 18:17, David Topham wrote: > > > > I was reading an article by Rob Arthan about ProofPower Z and notice > that the document shows SML input followed by ProofPower output. I have not > seen how to automatically create that using xpp. e.g. I know that > > =SML > > produces the first label using doctex, but what produces the "ProofPower > output" label in the tex file? > > > > So far, I have been using screenshot images of what I see in xpp and > using \includegraphics under =TEX > > -- > > -Dave > > ___ > > Proofpower mailing list > > Proofpower@lemma-one.com > > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > > -- -Dave ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] ProofPower output
I was reading an article by Rob Arthan about ProofPower Z and notice that the document shows SML input followed by ProofPower output. I have not seen how to automatically create that using xpp. e.g. I know that =SML produces the first label using doctex, but what produces the "ProofPower output" label in the tex file? So far, I have been using screenshot images of what I see in xpp and using \includegraphics under =TEX -- -Dave ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] ProofPower and Discrete Math
Roger, Thank you so much! I had not come across rewrite_rule in my reading. It works exactly as I need. -Dave On Tue, Feb 7, 2017 at 5:01 AM, Roger Bishop Jones wrote: > David, > > Of course, how to make a rule depends on what rule you are trying to make. > > ¬_∨_thm is an equivalence, i.e. a boolean equation, and the most common > way of using equations is by rewriting. > If you are doing forward proof then you can rewrite using rewrite_rule, so > to use this theorem you might rewrite with it as follows: > > val new_thm = rewrite_rule [¬_∨_thm] old_thm; > > The effect would be to push in negation over any disjunctions to which it > is applied in the old_thm and return the resulting theorem, > > If you wanted a special rule to achieve that effect then: > > val ¬_∨_rule = rewrite_rule [¬_∨_thm]; > > which you would use thus: > > val new_thm = ¬_∨_rule old_thm; > > Roger > > On 07/02/2017 05:29, David Topham wrote: > > I have made some more progress in applying ProofPower to forward proofs in > discrete math. e.g. I can prove DeMorgan's theorem successful > (propositional calculus). I would like to use the newly proved theorem in > other proofs now. What is the best strategy to do that? Is it to create > an SML function that takes an argument of type TERM and returns a THM? > Could you give an example of a proved THM intended to be used as a new rule > of inference? > > I also discovered the not_or_thm in the zed theory, which is DeMorgan's > Law, but that does not seem to be a function, so I am not sure how to apply > it in a forward proof. > > I appreciate any pointers in the right direction (or reference to which > manual might enlighten me). Thanks, Dave > > On Wed, Aug 17, 2016 at 11:06 AM, David Topham wrote: > >> Thank you both (Rob and Roger) for your "above and beyond the call of >> duty" help in getting me through my attempts to approach using ProofPower >> to teach Discrete Math. I understand your comments that backward proof is >> more economical than forward proof. Yet, I don't think the students will >> learn how to formulate proof thinking skills if ProofPower does it for >> them! True, that learning how to use the mechanized assistance is >> practical, but we (students) need to understand what constitutes valid >> reasoning so have to see the tedious steps one-at-a-time. (e.g. I tried "a >> (prove_tac[]);" and it works perfectly, but does not show me all the steps >> that were used (is there a way for it to do that?)) >> >> I believe the majority of courses teaching DM don't even try to go beyond >> the paper and pencil proofs--maybe that is good enough, but I can't help >> but think that exposure to professional tools (i.e. ProofPower) that force >> us to think carefully about what we are doing and to have the computer not >> allow us to proceed on shaky grounds is beneficial. >> >> Even though ProofPower is designed for math pros and is difficult to >> approach as beginning math novices, it is very well designed in its >> interface and ease of use. I am drawn to it by integration of "literate" >> approaches to documentation, ability to enter math notation, support for >> SML, and Z too (which is my next goal once basic Prop/Pred Calc is under >> our belts). Overall we should be able to derive correct programs and/or >> prove algorithms. >> >> My idea is that application of proofs to software design is the main goal >> of a Discrete Math course (recently changed to Discrete Structures by the >> powers that be). I do recognize the value of your time, and will resist >> asking each time I get stuck unless I am unable to continue. >> -Dave >> >> >> On Wed, Aug 17, 2016 at 3:02 AM, Rob Arthan wrote: >> >>> David, >>> >>> I endorse what Roger said about forward v. backwards proof. >>> There is definitely a tension between teaching proof theory >>> and teaching practical mechanised proof. >>> >>> For the record, the problem was that you had the two theorem >>> arguments of ∃_elim the wrong way round and you seemed >>> to have misunderstood the role of the term argument: it is >>> the variable that is free in the assumption of the second theorem >>> that is going to be discharged by the first theorem (the one >>> with the existential conclusion). Here is the complete proof >>> with the output you should see in the comments. >>> >>> val L1 = asm_rule ⌜p(x,y):BOOL⌝; >>> (* val L1 = p (x, y) ⊢ p (x, y): THM *) >>> val L2 = ⌜∃x:'a⦁p(x,y)⌝; >>&g
Re: [ProofPower] ProofPower and Discrete Math
I have made some more progress in applying ProofPower to forward proofs in discrete math. e.g. I can prove DeMorgan's theorem successful (propositional calculus). I would like to use the newly proved theorem in other proofs now. What is the best strategy to do that? Is it to create an SML function that takes an argument of type TERM and returns a THM? Could you give an example of a proved THM intended to be used as a new rule of inference? I also discovered the not_or_thm in the zed theory, which is DeMorgan's Law, but that does not seem to be a function, so I am not sure how to apply it in a forward proof. I appreciate any pointers in the right direction (or reference to which manual might enlighten me). Thanks, Dave On Wed, Aug 17, 2016 at 11:06 AM, David Topham wrote: > Thank you both (Rob and Roger) for your "above and beyond the call of > duty" help in getting me through my attempts to approach using ProofPower > to teach Discrete Math. I understand your comments that backward proof is > more economical than forward proof. Yet, I don't think the students will > learn how to formulate proof thinking skills if ProofPower does it for > them! True, that learning how to use the mechanized assistance is > practical, but we (students) need to understand what constitutes valid > reasoning so have to see the tedious steps one-at-a-time. (e.g. I tried "a > (prove_tac[]);" and it works perfectly, but does not show me all the steps > that were used (is there a way for it to do that?)) > > I believe the majority of courses teaching DM don't even try to go beyond > the paper and pencil proofs--maybe that is good enough, but I can't help > but think that exposure to professional tools (i.e. ProofPower) that force > us to think carefully about what we are doing and to have the computer not > allow us to proceed on shaky grounds is beneficial. > > Even though ProofPower is designed for math pros and is difficult to > approach as beginning math novices, it is very well designed in its > interface and ease of use. I am drawn to it by integration of "literate" > approaches to documentation, ability to enter math notation, support for > SML, and Z too (which is my next goal once basic Prop/Pred Calc is under > our belts). Overall we should be able to derive correct programs and/or > prove algorithms. > > My idea is that application of proofs to software design is the main goal > of a Discrete Math course (recently changed to Discrete Structures by the > powers that be). I do recognize the value of your time, and will resist > asking each time I get stuck unless I am unable to continue. > -Dave > > > On Wed, Aug 17, 2016 at 3:02 AM, Rob Arthan wrote: > >> David, >> >> I endorse what Roger said about forward v. backwards proof. >> There is definitely a tension between teaching proof theory >> and teaching practical mechanised proof. >> >> For the record, the problem was that you had the two theorem >> arguments of ∃_elim the wrong way round and you seemed >> to have misunderstood the role of the term argument: it is >> the variable that is free in the assumption of the second theorem >> that is going to be discharged by the first theorem (the one >> with the existential conclusion). Here is the complete proof >> with the output you should see in the comments. >> >> val L1 = asm_rule ⌜p(x,y):BOOL⌝; >> (* val L1 = p (x, y) ⊢ p (x, y): THM *) >> val L2 = ⌜∃x:'a⦁p(x,y)⌝; >> (* val L2 = ⌜∃ x⦁ p (x, y)⌝: TERM *) >> val L3 = ∃_intro L2 L1; >> (* val L3 = p (x, y) ⊢ ∃ x⦁ p (x, y): THM *) >> val L4 = ⌜∃y:'b⦁∃x:'a⦁p(x,y)⌝; >> (* val L4 = ⌜∃ y x⦁ p (x, y)⌝: TERM *) >> val L5 = ∃_intro L4 L3; >> (* val L5 = p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *) >> val L6 = asm_rule ⌜∃y:'b⦁p(x,y)⌝; >> (* val L6 = ∃ y⦁ p (x, y) ⊢ ∃ y⦁ p (x, y): THM *) >> val L7 = ∃_elim ⌜y:'b⌝ L6 L5; >> (* val L7 = ∃ y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *) >> val L8 = asm_rule ⌜∃x:'a⦁ ∃y:'b⦁p(x,y)⌝; >> (* val L8 = ∃ x y⦁ p (x, y) ⊢ ∃ x y⦁ p (x, y): THM *) >> val L9 = ∃_elim ⌜x:'a⌝ L8 L7; >> (* val L9 = ∃ x y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *) >> val L10 = ⇒_intro ⌜∃x:'a⦁ ∃y:'b⦁p(x,y)⌝ L9; >> (* val L10 = ⊢ (∃ x y⦁ p (x, y)) ⇒ (∃ y x⦁ p (x, y)): THM *) >> >> The documentation and the error messages talk about varstructs >> meaning either variables or things formed from variables using pairing >> (like ∃_elim will work on theorems with conclusions like ∃(x, y)⦁ p (x, >> y)). >> You can just read “variable” for “varstruct” in simple examples. >> >> Regards, >> >> Rob. >> >> On 16 Aug 20
Re: [ProofPower] Font for SML
Rob,
The author of the Latex class ffslides (Mark Wolters) suggested I try
putting \obeyspaces right at top line of \begin{document} and that works!
Great! All the SML is now spaced correctly. That means I don't have to
post-process the tex file. It remains
to be seen if that breaks anything else, but so far it is fine.
Thanks for the tip! -Dave
On Wed, Oct 5, 2016 at 10:42 PM, David Topham wrote:
> Rob, That idea does work: when I replace all spaces with ~ I get good
> output. I would need to post-process each tex file though. Maybe I can
> work out a script to do that and integrate it with docdvi (as Roger
> suggested)? First I will try to see if/how ffslides may be interfering with
> obeyspaces. I did read in the ffslides documentation that we can't use
> verbatim directly since pstricks (postscript) has some problem with that.
> Maybe a related issue.
> Thanks for the tip; that is a good work-around for now. -Dave
>
> On Wed, Oct 5, 2016 at 1:05 PM, Rob Arthan wrote:
>
>> David,
>>
>> The ProofPower environments use \obeyspaces to persuade LaTeX to honour
>> the spaces
>> in ML code etc. The ffslides package is doing something that is stopping
>> \obeyspaces
>> working properly. A quick fix would be to edit the .tex file (lab.tex in
>> your example) to replace
>> spaces between \begin{GFT} and \end{GFT} with tildes.
>>
>> Regards,
>>
>> Rob.
>>
>> On 5 Oct 2016, at 20:55, David Topham wrote:
>>
>> ...forgot to mention...need to go through postscript, so
>> latex lab.tex
>> dvipdf lab.dvi
>>
>> On Wed, Oct 5, 2016 at 12:28 PM, David Topham wrote:
>>
>>> Thanks Roger, In case you wish to see the problem more exactly attached
>>> is the doc file and the ffslides.cls (which you could also get at CTAN).
>>> It seems that for SML, the spaces are all removed! I will look into GFT to
>>> see how spaces are inserted. One issue might be if verbatim environment is
>>> used? -Dave
>>>
>>>
>>> On Wed, Oct 5, 2016 at 8:35 AM, Roger Bishop Jones
>>> wrote:
>>>
>>>> David,
>>>>
>>>> Doctex doesn't chose a font, it just generates LaTeX commands for the
>>>> formal text and any font changing is up to the rest of the document (that
>>>> you provide in the =TEX sections of the .doc file).
>>>>
>>>> It does generate tex for the HOL and ZED paragraphs which is intended
>>>> to force the layout in the printed version to follow the layout in the
>>>> source, which tex would not normally do, so I guess the ffslides package is
>>>> interfering with the way that works.
>>>> The formal text is translated into tex using an environment GFT which
>>>> is defined in ProofPower.sty, but its beyond my tex expertise to understand
>>>> how it works or why ffslides is interfering.
>>>>
>>>> It is possible to get slides made with ProofPower formal text in them,
>>>> the tutorial slides in the ProofPower distribution are examples of how this
>>>> can be done, though the method used for them is probably rather ancient by
>>>> now.
>>>>
>>>> Roger
>>>>
>>>>
>>>> On 04/10/2016 20:14, David Topham wrote:
>>>>
>>>> I am exploring a not often used but nice Latex package named ffslides.
>>>> It has several advantages in exact control of where things are placed on
>>>> the page using postscript (actually pstricks) behind the scenes. But, one
>>>> problem is that the SML in my doc file is getting scrunched together like
>>>> this:
>>>>
>>>> *funsubset([],[])=true*
>>>>
>>>> Is there a way for me to choose a different font when doctex extracts
>>>> the SML?
>>>> Maybe I could find an alternative that would not squash?
>>>>
>>>> -Dave
>>>>
>>>> ,
>>>> [])=
>>>> true
>>>>
>>>>
>>>> ___
>>>> Proofpower mailing
>>>> listProofpower@lemma-one.comhttp://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>>>>
>>>>
>>>>
>>>>
>>>> --
>>>> This message did not originate from Ohlone College and must be viewed
>>>> with caution. Viruses and phishing attempts can be transmitted via email.
>>>> E-mail transmission cannot be guaranteed to be secure or error-free as
>>>> information could be intercepted, corrupted, lost, destroyed, arrive late
>>>> or incomplete, or contain viruses. If you have any concerns, please contact
>>>> the Ohlone College IT Service Desk at itserviced...@ohlone.edu or (510)
>>>> 659-7333.
>>>>
>>>
>>>
>> ___
>> Proofpower mailing list
>> Proofpower@lemma-one.com
>> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>>
>>
>>
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Font for SML
Rob, That idea does work: when I replace all spaces with ~ I get good
output. I would need to post-process each tex file though. Maybe I can
work out a script to do that and integrate it with docdvi (as Roger
suggested)? First I will try to see if/how ffslides may be interfering with
obeyspaces. I did read in the ffslides documentation that we can't use
verbatim directly since pstricks (postscript) has some problem with that.
Maybe a related issue.
Thanks for the tip; that is a good work-around for now. -Dave
On Wed, Oct 5, 2016 at 1:05 PM, Rob Arthan wrote:
> David,
>
> The ProofPower environments use \obeyspaces to persuade LaTeX to honour
> the spaces
> in ML code etc. The ffslides package is doing something that is stopping
> \obeyspaces
> working properly. A quick fix would be to edit the .tex file (lab.tex in
> your example) to replace
> spaces between \begin{GFT} and \end{GFT} with tildes.
>
> Regards,
>
> Rob.
>
> On 5 Oct 2016, at 20:55, David Topham wrote:
>
> ...forgot to mention...need to go through postscript, so
> latex lab.tex
> dvipdf lab.dvi
>
> On Wed, Oct 5, 2016 at 12:28 PM, David Topham wrote:
>
>> Thanks Roger, In case you wish to see the problem more exactly attached
>> is the doc file and the ffslides.cls (which you could also get at CTAN).
>> It seems that for SML, the spaces are all removed! I will look into GFT to
>> see how spaces are inserted. One issue might be if verbatim environment is
>> used? -Dave
>>
>>
>> On Wed, Oct 5, 2016 at 8:35 AM, Roger Bishop Jones
>> wrote:
>>
>>> David,
>>>
>>> Doctex doesn't chose a font, it just generates LaTeX commands for the
>>> formal text and any font changing is up to the rest of the document (that
>>> you provide in the =TEX sections of the .doc file).
>>>
>>> It does generate tex for the HOL and ZED paragraphs which is intended to
>>> force the layout in the printed version to follow the layout in the source,
>>> which tex would not normally do, so I guess the ffslides package is
>>> interfering with the way that works.
>>> The formal text is translated into tex using an environment GFT which is
>>> defined in ProofPower.sty, but its beyond my tex expertise to understand
>>> how it works or why ffslides is interfering.
>>>
>>> It is possible to get slides made with ProofPower formal text in them,
>>> the tutorial slides in the ProofPower distribution are examples of how this
>>> can be done, though the method used for them is probably rather ancient by
>>> now.
>>>
>>> Roger
>>>
>>>
>>> On 04/10/2016 20:14, David Topham wrote:
>>>
>>> I am exploring a not often used but nice Latex package named ffslides.
>>> It has several advantages in exact control of where things are placed on
>>> the page using postscript (actually pstricks) behind the scenes. But, one
>>> problem is that the SML in my doc file is getting scrunched together like
>>> this:
>>>
>>> *funsubset([],[])=true*
>>>
>>> Is there a way for me to choose a different font when doctex extracts
>>> the SML?
>>> Maybe I could find an alternative that would not squash?
>>>
>>> -Dave
>>>
>>> ,
>>> [])=
>>> true
>>>
>>>
>>> ___
>>> Proofpower mailing
>>> listProofpower@lemma-one.comhttp://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>>>
>>>
>>>
>>>
>>> --
>>> This message did not originate from Ohlone College and must be viewed
>>> with caution. Viruses and phishing attempts can be transmitted via email.
>>> E-mail transmission cannot be guaranteed to be secure or error-free as
>>> information could be intercepted, corrupted, lost, destroyed, arrive late
>>> or incomplete, or contain viruses. If you have any concerns, please contact
>>> the Ohlone College IT Service Desk at itserviced...@ohlone.edu or (510)
>>> 659-7333.
>>>
>>
>>
> ___
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>
>
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Font for SML
...forgot to mention...need to go through postscript, so latex lab.tex dvipdf lab.dvi On Wed, Oct 5, 2016 at 12:28 PM, David Topham wrote: > Thanks Roger, In case you wish to see the problem more exactly attached is > the doc file and the ffslides.cls (which you could also get at CTAN). It > seems that for SML, the spaces are all removed! I will look into GFT to > see how spaces are inserted. One issue might be if verbatim environment is > used? -Dave > > > On Wed, Oct 5, 2016 at 8:35 AM, Roger Bishop Jones > wrote: > >> David, >> >> Doctex doesn't chose a font, it just generates LaTeX commands for the >> formal text and any font changing is up to the rest of the document (that >> you provide in the =TEX sections of the .doc file). >> >> It does generate tex for the HOL and ZED paragraphs which is intended to >> force the layout in the printed version to follow the layout in the source, >> which tex would not normally do, so I guess the ffslides package is >> interfering with the way that works. >> The formal text is translated into tex using an environment GFT which is >> defined in ProofPower.sty, but its beyond my tex expertise to understand >> how it works or why ffslides is interfering. >> >> It is possible to get slides made with ProofPower formal text in them, >> the tutorial slides in the ProofPower distribution are examples of how this >> can be done, though the method used for them is probably rather ancient by >> now. >> >> Roger >> >> >> On 04/10/2016 20:14, David Topham wrote: >> >> I am exploring a not often used but nice Latex package named ffslides. It >> has several advantages in exact control of where things are placed on the >> page using postscript (actually pstricks) behind the scenes. But, one >> problem is that the SML in my doc file is getting scrunched together like >> this: >> >> *funsubset([],[])=true* >> >> Is there a way for me to choose a different font when doctex extracts the >> SML? >> Maybe I could find an alternative that would not squash? >> >> -Dave >> >> , >> [])= >> true >> >> >> ___ >> Proofpower mailing >> listProofpower@lemma-one.comhttp://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com >> >> >> >> >> -- >> This message did not originate from Ohlone College and must be viewed >> with caution. Viruses and phishing attempts can be transmitted via email. >> E-mail transmission cannot be guaranteed to be secure or error-free as >> information could be intercepted, corrupted, lost, destroyed, arrive late >> or incomplete, or contain viruses. If you have any concerns, please contact >> the Ohlone College IT Service Desk at itserviced...@ohlone.edu or (510) >> 659-7333. >> > > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Font for SML
Thanks Roger, In case you wish to see the problem more exactly attached is the doc file and the ffslides.cls (which you could also get at CTAN). It seems that for SML, the spaces are all removed! I will look into GFT to see how spaces are inserted. One issue might be if verbatim environment is used? -Dave On Wed, Oct 5, 2016 at 8:35 AM, Roger Bishop Jones wrote: > David, > > Doctex doesn't chose a font, it just generates LaTeX commands for the > formal text and any font changing is up to the rest of the document (that > you provide in the =TEX sections of the .doc file). > > It does generate tex for the HOL and ZED paragraphs which is intended to > force the layout in the printed version to follow the layout in the source, > which tex would not normally do, so I guess the ffslides package is > interfering with the way that works. > The formal text is translated into tex using an environment GFT which is > defined in ProofPower.sty, but its beyond my tex expertise to understand > how it works or why ffslides is interfering. > > It is possible to get slides made with ProofPower formal text in them, the > tutorial slides in the ProofPower distribution are examples of how this can > be done, though the method used for them is probably rather ancient by now. > > Roger > > > On 04/10/2016 20:14, David Topham wrote: > > I am exploring a not often used but nice Latex package named ffslides. It > has several advantages in exact control of where things are placed on the > page using postscript (actually pstricks) behind the scenes. But, one > problem is that the SML in my doc file is getting scrunched together like > this: > > *funsubset([],[])=true* > > Is there a way for me to choose a different font when doctex extracts the > SML? > Maybe I could find an alternative that would not squash? > > -Dave > > , > [])= > true > > > ___ > Proofpower mailing > listProofpower@lemma-one.comhttp://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > > > > > -- > This message did not originate from Ohlone College and must be viewed with > caution. Viruses and phishing attempts can be transmitted via email. E-mail > transmission cannot be guaranteed to be secure or error-free as information > could be intercepted, corrupted, lost, destroyed, arrive late or > incomplete, or contain viruses. If you have any concerns, please contact > the Ohlone College IT Service Desk at itserviced...@ohlone.edu or (510) > 659-7333. > lab.doc Description: MS-Word document ffslides.cls Description: Binary data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Font for SML
I am exploring a not often used but nice Latex package named ffslides. It has several advantages in exact control of where things are placed on the page using postscript (actually pstricks) behind the scenes. But, one problem is that the SML in my doc file is getting scrunched together like this: *funsubset([],[])=true* Is there a way for me to choose a different font when doctex extracts the SML? Maybe I could find an alternative that would not squash? -Dave , [])= true ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] ProofPower and Discrete Math
Thank you both (Rob and Roger) for your "above and beyond the call of duty" help in getting me through my attempts to approach using ProofPower to teach Discrete Math. I understand your comments that backward proof is more economical than forward proof. Yet, I don't think the students will learn how to formulate proof thinking skills if ProofPower does it for them! True, that learning how to use the mechanized assistance is practical, but we (students) need to understand what constitutes valid reasoning so have to see the tedious steps one-at-a-time. (e.g. I tried "a (prove_tac[]);" and it works perfectly, but does not show me all the steps that were used (is there a way for it to do that?)) I believe the majority of courses teaching DM don't even try to go beyond the paper and pencil proofs--maybe that is good enough, but I can't help but think that exposure to professional tools (i.e. ProofPower) that force us to think carefully about what we are doing and to have the computer not allow us to proceed on shaky grounds is beneficial. Even though ProofPower is designed for math pros and is difficult to approach as beginning math novices, it is very well designed in its interface and ease of use. I am drawn to it by integration of "literate" approaches to documentation, ability to enter math notation, support for SML, and Z too (which is my next goal once basic Prop/Pred Calc is under our belts). Overall we should be able to derive correct programs and/or prove algorithms. My idea is that application of proofs to software design is the main goal of a Discrete Math course (recently changed to Discrete Structures by the powers that be). I do recognize the value of your time, and will resist asking each time I get stuck unless I am unable to continue. -Dave On Wed, Aug 17, 2016 at 3:02 AM, Rob Arthan wrote: > David, > > I endorse what Roger said about forward v. backwards proof. > There is definitely a tension between teaching proof theory > and teaching practical mechanised proof. > > For the record, the problem was that you had the two theorem > arguments of ∃_elim the wrong way round and you seemed > to have misunderstood the role of the term argument: it is > the variable that is free in the assumption of the second theorem > that is going to be discharged by the first theorem (the one > with the existential conclusion). Here is the complete proof > with the output you should see in the comments. > > val L1 = asm_rule ⌜p(x,y):BOOL⌝; > (* val L1 = p (x, y) ⊢ p (x, y): THM *) > val L2 = ⌜∃x:'a⦁p(x,y)⌝; > (* val L2 = ⌜∃ x⦁ p (x, y)⌝: TERM *) > val L3 = ∃_intro L2 L1; > (* val L3 = p (x, y) ⊢ ∃ x⦁ p (x, y): THM *) > val L4 = ⌜∃y:'b⦁∃x:'a⦁p(x,y)⌝; > (* val L4 = ⌜∃ y x⦁ p (x, y)⌝: TERM *) > val L5 = ∃_intro L4 L3; > (* val L5 = p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *) > val L6 = asm_rule ⌜∃y:'b⦁p(x,y)⌝; > (* val L6 = ∃ y⦁ p (x, y) ⊢ ∃ y⦁ p (x, y): THM *) > val L7 = ∃_elim ⌜y:'b⌝ L6 L5; > (* val L7 = ∃ y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *) > val L8 = asm_rule ⌜∃x:'a⦁ ∃y:'b⦁p(x,y)⌝; > (* val L8 = ∃ x y⦁ p (x, y) ⊢ ∃ x y⦁ p (x, y): THM *) > val L9 = ∃_elim ⌜x:'a⌝ L8 L7; > (* val L9 = ∃ x y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *) > val L10 = ⇒_intro ⌜∃x:'a⦁ ∃y:'b⦁p(x,y)⌝ L9; > (* val L10 = ⊢ (∃ x y⦁ p (x, y)) ⇒ (∃ y x⦁ p (x, y)): THM *) > > The documentation and the error messages talk about varstructs > meaning either variables or things formed from variables using pairing > (like ∃_elim will work on theorems with conclusions like ∃(x, y)⦁ p (x, > y)). > You can just read “variable” for “varstruct” in simple examples. > > Regards, > > Rob. > > On 16 Aug 2016, at 21:24, David Topham wrote: > > Since the slides for this book use slightly different notation, I am back > to trying to implement the proofs in the main book: UsingZ from > www.usingz.com (in text link, it is zedbook) > > On page 42, the proof is using nested existentials, and I am trying > to get past my lack of understanding in applying E-elim > (Roger already helped me with E-intro) > > Here are two of my attempts (using ASCII since I can't attach pdf here) > val L1 = asm_rule %<%p(x,y):BOOL%>%; > val L2 = %<%%exists%x:'a%spot%p(x,y)%>%; > val L3 = %exists%_intro L2 L1; > val L4 = %<%%exists%y:'b%spot%%exists%x:'a%spot%p(x,y)%>%; > val L5 = %exists%_intro L4 L3; > val L6 = asm_rule %<%%exists%y:'b%spot%p(x,y)%>%; > val L7 = %exists%_elim L4 L5 L6; > > val L1 = asm_rule %<%p:BOOL%>%; > val L2 = %<%%exists%x:'a%spot%p%>%; > val L3 = %exists%_intro L2 L1; > val L4 = %<%%exists%y:'b%spot%%exists%x:'a%spot%p%>%; > val L5 = %exists%_intro L4 L3; > val L6 = asm_rule %<%%exis
Re: [ProofPower] ProofPower and Discrete Math
Since the slides for this book use slightly different notation, I am back to trying to implement the proofs in the main book: UsingZ from www.usingz.com (in text link, it is zedbook) On page 42, the proof is using nested existentials, and I am trying to get past my lack of understanding in applying E-elim (Roger already helped me with E-intro) Here are two of my attempts (using ASCII since I can't attach pdf here) val L1 = asm_rule %<%p(x,y):BOOL%>%; val L2 = %<%%exists%x:'a%spot%p(x,y)%>%; val L3 = %exists%_intro L2 L1; val L4 = %<%%exists%y:'b%spot%%exists%x:'a%spot%p(x,y)%>%; val L5 = %exists%_intro L4 L3; val L6 = asm_rule %<%%exists%y:'b%spot%p(x,y)%>%; val L7 = %exists%_elim L4 L5 L6; val L1 = asm_rule %<%p:BOOL%>%; val L2 = %<%%exists%x:'a%spot%p%>%; val L3 = %exists%_intro L2 L1; val L4 = %<%%exists%y:'b%spot%%exists%x:'a%spot%p%>%; val L5 = %exists%_intro L4 L3; val L6 = asm_rule %<%%exists%y:'b%spot%p%>%; val L7 = %exists%_elim L4 L5 L6; The error I get is "does not match the bound varstruct" Does anyone have a suggestion to get me past this roadblock? -Dave On Sun, Aug 14, 2016 at 2:21 AM, Roger Bishop Jones wrote: > > On 14/08/2016 08:44, David Topham wrote: > >> Thanks Roger, I am using slides he distributes. He has false >> introduction rules starting on page 24 (attached). >> Sorry about my poor example, please ignore that since is a confused use >> of this technique anyway! -Dave >> >> Looks like he changed the name. > > In fact the original name (the one he uses in the book) is good in > ProofPower. > ¬_elim is available in ProofPower and does what you want (though it is > sligftly more general, it proves anything from a contradiction so you have > to tell it what result you are after). > Details in reference manual. > > Roger > > > This message did not originate from Ohlone College and must be viewed > with caution. Viruses and phishing attempts can be transmitted via email. > E-mail transmission cannot be guaranteed to be secure or error-free as > information could be intercepted, corrupted, lost, destroyed, arrive late > or incomplete, or contain viruses. > > If you have any concerns, please contact the Ohlone College IT Service > Desk at itserviced...@ohlone.edu or (510) 659-7333. > > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] V_cancel_rule alpha-conversion error
Thank you Mark. I appreciate you taking the time to help me out--that worked perfectly. -Dave On Fri, Mar 11, 2016 at 9:00 AM, wrote: > Send Proofpower mailing list submissions to > proofpower@lemma-one.com > > To subscribe or unsubscribe via the World Wide Web, visit > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > or, via email, send a message with subject or body 'help' to > proofpower-requ...@lemma-one.com > > You can reach the person managing the list at > proofpower-ow...@lemma-one.com > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Proofpower digest..." > > > Today's Topics: > >1. V_cancel_rule alpha-conversion error (David Topham) >2. Re: V_cancel_rule alpha-conversion error > (m...@proof-technologies.com) > > > ------ > > Message: 1 > Date: Fri, 11 Mar 2016 00:53:45 -0800 > From: David Topham > To: ProofPower List > Subject: [ProofPower] V_cancel_rule alpha-conversion error > Message-ID: > zjo+9_jydpo...@mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > I am trying to do a forward proof using hypothetical syllogism > (V_cancel_Rule) > of this form: ~q v r, q |- r > but get an alpha-conversion error. > (sorry for the hard to read format here, but I know I can't post images or > pdf files here, so what other way is there to show the extended chars of > ProofPower? I did > ascii-conv to get this format) > > val L1 = p %thm% p: THM > val L2 = p %implies% q %thm% p %implies% q: THM > val L3 = p %implies% q, p %thm% q: THM > val L4 = %not% q %or% r %thm% %not% q %or% r: THM > > Exception Fail * ? q ? r ? ? q ? r and p ? q, p ? q are not of the form: > `?1 ? > t1 ? t2' and `?2 ? ?t3' where ?t3? is ?-convertible to ?t1? or ?t2? > [?_cancel_rule.7050] * raised > -- next part -- > An HTML attachment was scrubbed... > URL: < > http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20160311/2ddae95b/attachment-0001.html > > > > -- > > Message: 2 > Date: Fri, 11 Mar 2016 14:06:27 + > From: m...@proof-technologies.com > To: ProofPower List > Subject: Re: [ProofPower] V_cancel_rule alpha-conversion error > Message-ID: > <7245278f69970a6c1211f108a9c92...@webmail-next.names.co.uk> > Content-Type: text/plain; charset="utf-8" > > Hi Dave, > > With this rule, the theorems need to precisely match up with how they > are described in the manual, so you need to have the conclusion of the > 2nd theorem as the logical negation of the LHS of the "or" in the 1st > thm (not vice versa). So just use the double logical negation > introduction rule on the 2nd theorem, and then it works. > > Perhaps using good old ASCII versions of the logical symbols a good > idea. This is what the HOL4 and HOL Light use. So there's: > disjunction: \/ > conjuntion: /\ > logical negation: ~ > implication: ==> > logical equivalence: <=> > universal quantification: ! > existential quantification: ? > unique existential quantification: ?! > > Mark. > > On 11/03/2016 08:53, David Topham wrote: > > > I am trying to do a forward proof using hypothetical syllogism > (V_cancel_Rule) > > of this form: ~q v r, q |- r > > but get an alpha-conversion error. > > (sorry for the hard to read format here, but I know I can't post images > or pdf files here, so what other way is there to show the extended chars of > ProofPower? I did > > ascii-conv to get this format) > > > > val L1 = p %thm% p: THM > > val L2 = p %implies% q %thm% p %implies% q: THM > > val L3 = p %implies% q, p %thm% q: THM > > val L4 = %not% q %or% r %thm% %not% q %or% r: THM > > > > Exception Fail * ? q ? r ? ? q ? r and p ? q, p ? q are not of the form: > `?1 ? > > t1 ? t2' and `?2 ? ?t3' where ?t3(R) is ?-convertible to ?t1(R) or ?t2(R) > > [?_cancel_rule.7050] * raised > > ___ > > Proofpower mailing list > > Proofpower@lemma-one.com > > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > > -- next part -- > An HTML attachment was scrubbed... > URL: < > http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20160311/300dfdc9/attachment-0001.html > > > > -- > > Subject: Digest Footer > > ___ > Proofpower mailing list > Proofpower@lemma-one.com > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > > > -- > > End of Proofpower Digest, Vol 101, Issue 1 > ** > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] V_cancel_rule alpha-conversion error
I am trying to do a forward proof using hypothetical syllogism (V_cancel_Rule) of this form: ~q v r, q |- r but get an alpha-conversion error. (sorry for the hard to read format here, but I know I can't post images or pdf files here, so what other way is there to show the extended chars of ProofPower? I did ascii-conv to get this format) val L1 = p %thm% p: THM val L2 = p %implies% q %thm% p %implies% q: THM val L3 = p %implies% q, p %thm% q: THM val L4 = %not% q %or% r %thm% %not% q %or% r: THM Exception Fail * ³ q ² r ô ³ q ² r and p ´ q, p ô q are not of the form: `‡1 ô t1 ² t2' and `‡2 ô ³t3' where ¬t3® is Á-convertible to ¬t1® or ¬t2® [²_cancel_rule.7050] * raised ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] xpp color highlighting
As I have mentioned in the past, I use xpp (and ProofPower) to teach programming in a literate way. We can easily combine several languages into one document (sml, c++, latex, etc) and then use docsml/doctex to extract the separate pieces to be compiled. The biggest resistance I get to adoption of this way of programming is that the editor does not help us "see" the different languages very well. i.e. There is no color-coding of language keywords. Has anyone investigated a way to integrate that feature into the xpp editor? I am used to all one color, but have enough experience that seeing the difference between latex and c++ is relatively easy -- not so for beginners learning both languages at the same time. Many have already had some exposure to IDEs such as Code::Blocks that highlight the keywords. -Dave *How 'Ya Gonna Keep 'Em Down on the Farm? (After They've Seen Paree)* ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Literate Programming
I love using ProofPower! Especially xpp has helped me to development literate programs mixing Latex with SML, and C++, and even assembly language. There is one thing missing that would be an improvement. The idea of literate programming as presented by Donald Knuth is to allow the order of program fragments be controlled. This means we could put more important or interesting pieces of code first in the document and less important pieces later. I don't see a way to rearrange pieces in xpp (sieveview) so far, but wonder if there is some possibility. For example, could =DUMPMORE prg.cpp have a parameter which represents an order? Maybe number them? =DUMPMORE 2 prg.cpp =DUMPMORE 1 prg.cpp would extract piece 1 before 2 in prg.cpp? -Dave ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Installation - location of Latex?
Thank you Roger, Since you said the tgz file is compressed, I re-downloaded it, and the original problem went away! I guess it had been slightly corrupted somehow during transfer. Next I found that Debian (Jessie) installs an older version of PolyML (5.2) and does not include polyc, so ProofPower fails installation. (I could see the problem in the build.log.) I got the source for PolyML 5.5 and built it. Also missing in Debian are some of the libx* libraries, but you clearly list those in the installation instructions (thank you for that!). Now ProofPower installs and I am a happy camper again! I really appreciate the support you provide. -Dave On Sun, Jul 5, 2015 at 12:11 AM, Roger Bishop Jones wrote: > David, > > On 05/07/15 06:02, David Topham wrote: > > I am installing the latest version of OpenProofPower in Debian. > > > > When I run ./configure, I get a message saying that tex and latex is > > not found. > > > > I know latex is installed (although not in the normal directory). I > > put the location > > of latex in PATH, but still no dice. I can run latex from the command > > line with no problems. > > > What does "which latex" say? > The configure script is checking with its own version of "which" to get > around > problems with which in some contexts. > > > Is there a requirement that latex be in a certain directory? > No. > > Or any environment variables other > > than PATH that should be updated? > > > No. I have TEXINPUTS BIBINPUTS BSTINPUTS and INDEXSTYLE but none of > those is required, > See section 4 of the README file for further advice on environment > variables. > > > > > > One other minor comment: when trying to extract the tgz file, I get > > message saying the file is not in a valid > > zip format! If I use tar without the z option, it works ok. > > > That doesn't sound right. > The latest release file will unpack with tar whether or not z is > specified but if > the file you have is not compressed then its not the right file. > > I suggest you go back to square 1(ish) download the latest tar file, > unpack it and try again, > Then if you still have the problem, report back in greater detail, > (though there isn't a lot more detail to be had!). > i.e. exactly what you did and what the response was and the output > from "which latex". > > Roger > > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Installation - location of Latex?
I am installing the latest version of OpenProofPower in Debian. When I run ./configure, I get a message saying that tex and latex is not found. I know latex is installed (although not in the normal directory). I put the location of latex in PATH, but still no dice. I can run latex from the command line with no problems. Is there a requirement that latex be in a certain directory? Or any environment variables other than PATH that should be updated? One other minor comment: when trying to extract the tgz file, I get message saying the file is not in a valid zip format! If I use tar without the z option, it works ok. -Dave ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Equational logic
Thank you Roger for those additional suggestions. I am still trying to wrap my head around how to apply them, and I have looked at USR013 but don't quite see an example that shows me how to do this kind of equational derivation (yet). I have an attempt in the attached link, but I know that (similar to earlier attempts), I have trouble turning my TERMs into THMs, which is what I need in order to use the deduction theorem. I don't think my L3 through L8 are in the right format...somehow they should be THMs, not TERMS. But what format would that be? Is it some sort of substitution of equals? -Dave https://www.dropbox.com/s/ifxxtsp8tpp1f6j/induction.PNG?dl=0 On Fri, Apr 3, 2015 at 6:37 AM, Roger Bishop Jones wrote: > On 31/03/15 22:39, David Topham wrote: > > I have been studying the idea of "equational logic" as described in this > link by Gries and wonder if anyone has used ProofPower in this way. If so, > I would love to see a sample. > >> One reason for my interest in this approach is because it seems more in >> line with proof by induction (which is a major topic of Discrete Math). >> For example, to prove that 2^n > n^2 for n >= 4 using induction seems >> like it would be clearest using equational logic. >> -Dave >> >> I looked closer at the rules specified by Gries and came up with > some > further suggestions as follows. > > Substitution: > > Provided x is not free in the assumptions then > you can use ∀_intro followed by ∀_elim. > > Leibniz: > > You could start with refl_conv to get |- E[P] = E[P] > then use subst_rule to substitute the Q for some instance of P. > > Alternatively use app_fun_rule, something like: > > fun leibniz_rule t = ((conv_rule (TRY_C(TOP_MAP_C β_conv o > (app_fun_rule t); > > leibniz_rule (λx.E) (asm_rule (P ⇔ Q)); > > Transitivity: - see eq_trans_rule > > Equanimity: ⇔_mp_rule > > You will find as you get into things more complex than the propositional > calculus that the penalty for using forward proof increases and things > can get quite cumbersome. > Typically in a goal oriented proof sight of the goal will allow the > tactics to work out details themselves which in a forward proof > you may have to specify in detail yourself, e.g. exactly which occurrences > of some expression need to be substituted for. > > Roger Jones > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Equational logic
...somehow my last post got garbled...maybe because of the html link? So instead, here is link to just the Equational Logic "rules of inference" (Gries): https://www.dropbox.com/s/t5kmsfufgqo4ciy/equ_logic.PNG?dl=0 And a sample of the proof I would like to encode in ProofPower: https://www.dropbox.com/s/la0wrk66cu8tviu/proof_by_induction.PNG?dl=0 I have been studying the idea of "equational logic" as described in this > link by Gries and wonder if anyone has used ProofPower in this way. If so, > I would love to see a sample. > One reason for my interest in this approach is because it seems more in > line with proof by induction (which is a major topic of Discrete Math). > For example, to prove that 2^n > n^2 for n >= 4 using induction seems like > it would be clearest using equational logic. > -Dave > > > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] ProofPower (and xpp) is a great program!
I know I am preaching to the choir here, but I was so impressed by the behavior of ProofPower today I thought I would go ahead and express my appreciation anyway! I have been using xpp to prepare notes and exercises for my discrete math course this semester, and today after spending a couple of hours working on a doc with some recursive functions in SML and inductive proofs in Latex, my xpp froze up! I don't know why, but I thought I was doomed. Then, magically, as I gave up and killed the process I saw the wonderful message: xpp-panic-problem_3_1_10.doc-Dq6T0c was being saved! Thank you, thank you, whoever added in that code to automatically save before dying! ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Predicate Calculus
Ah! Of course! Thank you again! I think I got it now. For completeness sake, in case anyone else is pursuing this line of learning ProofPower, I have a link here to the working version with those pieces in place. I do think there is a lot of potential for using this tool to teach Discrete Math. Sample predicate calculus proof <https://www.dropbox.com/s/7kd7dsd2erg0hi1/pred_calc.png?dl=0> On Tue, Mar 17, 2015 at 1:45 PM, Rob Arthan wrote: > David, > > The proof isn’t complete, as you will see if you look at the output when > you execute the lines that bind L6 and L7. You have just bound L6 to a term > not a theorem. You have bound L7 to the the applicatio of %forall%_intro to > L6, which does not give you a theorem (but rather a function from theorems > that will always fail, because %forall%_intro requires its first argument > to be (something akin to) a variable). The last line of your proof should > be something like: > > val L6 = %forall%_intro %<%x%>% L5; > > Regards, > > Rob. > > > On 17 Mar 2015, at 13:45, David Topham wrote: > > > > That makes sense, but the "proof" is completed, so what can I apply it > to? i > > .e. The goal of the proof is just to derive L7. Perhaps put it the form > of a conditional? ...conjunction of premises model the conclusion? > > > > On Mar 17, 2015 5:02 AM, "Rob Arthan" wrote: > > David, > > > > Your value L7 is a function (type THM -> THM) not a theorem (type THM). > > You need to apply it to another theorem to get a new theorem. > > ] > > Regards, > > > > Rob. > > > > On Tue, March 17, 2015 12:59 am, David Topham wrote: > > > Thank you so much Rob! That works! If you don't mind another > question: > > > I > > > had gotten format_thm to work without quantifiers, but with the > quantifier > > > I get an exception. (attached). I don't see anything about format_thm > in > > > user029.pdf (the main HOL reference). -Dave > > > > > > On Mon, Mar 16, 2015 at 2:51 PM, Rob Arthan wrote: > > > > > > > > >> David, > > >> > > >> > > >>> On 16 Mar 2015, at 04:22, David Topham wrote: > > >>> > > >>> > > >>> With my recent success learning to encode Propositional Calculus > > >>> using > > >> ProofPower (for my Discrete Math course), I have pressed on to > > >> Predicate > > >> Calculus. > > >> > > >>> > > >>> So far, I have figured out the basics, but stuck on quantifiers from > > >>> > > >> what I intuitively thought might work. Attached is my error message > > >> trying to quantify a negation. > > >> > > >> ProofPower syntax needs a bullet between the bound variables and the > > >> predicate in a quantification. You have to write: > > >> > > >> ∀ xâ¦? ¬ P(x) > > >> > > >> rather than: > > >> > > >> ∀ x ¬ P(x) > > >> > > >> This follows what is now common practice in logical languages used in > > >> CS > > >> and reflects a decision to make quantifiers have lower precedence than > > >> the propositional operators, so that the scope of a quantifier extends > > >> as far to the right as possible (as opposed to traditional > mathematical > > >> logic practice which requires brackets around the matrix of a > > >> quantification if the matrix is not a literal). So the brackets > around > > >> the implication in: > > >> > > >> ∀ xâ¦? (¬ P(x) ⇒ Q(x)) > > >> > > >> are unnecessary. (I think of the bullet as being like a big version of > > >> Russell & Whitehead’s convention of using a dot to adjust the > > >> precedence of a connective.) Unfortunately, this is probably at odds > > >> with the conventions you have been using in your course. > > >> > > >> Regards, > > >> > > >> > > >> Rob. > > >> > > >> > > >> > > > > > > > > > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Predicate Calculus
With my recent success learning to encode Propositional Calculus using ProofPower (for my Discrete Math course), I have pressed on to Predicate Calculus. So far, I have figured out the basics, but stuck on quantifiers from what I intuitively thought might work. Attached is my error message trying to quantify a negation. Any suggestions? Thank you, Dave ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] ProofPower and Discrete Math
My first successful results of the mapping from Discrete Math rules of inference to ProofPower are attached in case they are useful to anyone else working on a similar project. a mapping from discrete math "rules of inference" to ProofPower <https://www.dropbox.com/s/mtdejdpgzziz6g5/mapping_rules_of_inference.pdf?dl=0> On Sat, Feb 28, 2015 at 11:47 PM, David Topham wrote: > The first successful results of the mapping from Discrete Math rules of > inference to ProofPower are attached in case they are useful to anyone else > working on a similar project. > > On Thu, Feb 5, 2015 at 9:00 AM, wrote: > >> Send Proofpower mailing list submissions to >> proofpower@lemma-one.com >> >> To subscribe or unsubscribe via the World Wide Web, visit >> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com >> or, via email, send a message with subject or body 'help' to >> proofpower-requ...@lemma-one.com >> >> You can reach the person managing the list at >> proofpower-ow...@lemma-one.com >> >> When replying, please edit your Subject line so it is more specific >> than "Re: Contents of Proofpower digest..." >> >> >> Today's Topics: >> >>1. Re: ProofPower and Discrete Math (David Topham) >>2. Re: ProofPower and Discrete Math (Rob Arthan) >> >> >> -- >> >> Message: 1 >> Date: Wed, 4 Feb 2015 12:49:47 -0800 >> From: David Topham >> To: Roger Bishop Jones >> Cc: ProofPower List >> Subject: Re: [ProofPower] ProofPower and Discrete Math >> Message-ID: >> < >> cad034bgcumtxj3nkvjjpcxdspsd5s_7ipw+tli0mfu6htwo...@mail.gmail.com> >> Content-Type: text/plain; charset="utf-8" >> >> Roger, Thank you very much! This example got me past my mental block and I >> see how to work with these proofs much better now. I appreciate your time >> in helping me. Now I see one of my tasks is to map the names I use (such >> as >> hypothetical syllogism) to the names used within ProofPower (such as >> =>_trans_rule). I will work on that mapping... -Dave >> >> On Tue, Feb 3, 2015 at 7:29 AM, Roger Bishop Jones < >> postmas...@rbjones.com> >> wrote: >> >> > On 03/02/15 13:55, David Topham wrote: >> > > >> > > >> > > I am interested in using ProofPower to aid in the teaching of Discrete >> > > Math. I would like to assist the students in developing proofs using >> > > specific rules of inference. e.g. in the attached proof from our >> > > textbook the proof uses Hypothetical Syllogism to prove a >> > > Propositional expression. I don't quite see yet from the tutorials how >> > > to direct ProofPower in this way. Is it possible? Does anyone have >> > > experience using ProofPower like this? If so, I would appreciate some >> > > guidance. It seems so far in my observations, that pp is used by >> > > selecting some "tactics" which then guide pp to find a proof, but we >> > > would need to direct each step as part of the learning process. >> > > Thanks, Dave >> > > >> > The proof you exhibit is what we would call a "forward proof". >> > The subgoal package is used for what we call "backward" (or goal >> > oriented) proofs. >> > >> > A forward proof for the result you require runs like this: >> > >> > val L1 = asm_rule ?P ? Q?; >> > val L2 = asm_rule ?Q ? R?; >> > val L3 = ?_trans_rule L1 L2; >> > val L4 = asm_rule ?R ? P?; >> > val L5 = ?_intro L3 L4; >> > >> > Except that the characters are a mess because I just copied >> > and pasted from the xpp window which doesn't work. >> > >> > The value of L5 will be the desired result/ >> > >> > I attach a proofpower document containing the proof. >> > >> > The documentation for the inference rules is in the reference manual >> > USR029 section 8.1. >> > >> > The HOL Tutorial Notes USR013 has perhaps more accessible descriptions >> of >> > a selection of rules in Chapter 5. >> > >> > Roger Jones >> > >> > >> > >> > >> > >> -- next part -- >> An HTML attachment was scrubbed... >> URL: < >> http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20150204/341a13e6/attachmen
Re: [ProofPower] ProofPower PrettyPrinter
Rob, That works great! Thanks so much, Dave On Sun, Feb 22, 2015 at 9:08 AM, Rob Arthan wrote: > David, > > On 22 Feb 2015, at 16:47, David Topham wrote: > > I am trying to get a proof listing (of hypothetical syllogism) for > teaching purposes. > > Thanks to help from Roger, I have the proof working, but would like to use > PrettyPrinter to put each step of proof on different line. I almost have > it, but ran into a snag with the special character Q (which means something > special to ProofPower). > > I attached the screen capture where you can see the Q has become . > > > There is a function translate_for_output which undoes the encoding. > > Even easier in your example, there is a function diag_line which > translates a > string for output and prints it on standard output followed by a newline > character. > If you change your definition of printList > > val printList = app diag_line; > > it should do what you want. > > Regards, > > Rob. > > > My goal is something approximating a Fitch-style proof (but I don't need > the lines for the subproof) > > I appreciate any suggestions... > > -Dave Topham > ___ > Proofpower mailing list > Proofpower@lemma-one.com > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > > > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] ProofPower and Discrete Math
Roger, Thank you very much! This example got me past my mental block and I see how to work with these proofs much better now. I appreciate your time in helping me. Now I see one of my tasks is to map the names I use (such as hypothetical syllogism) to the names used within ProofPower (such as =>_trans_rule). I will work on that mapping... -Dave On Tue, Feb 3, 2015 at 7:29 AM, Roger Bishop Jones wrote: > On 03/02/15 13:55, David Topham wrote: > > > > > > I am interested in using ProofPower to aid in the teaching of Discrete > > Math. I would like to assist the students in developing proofs using > > specific rules of inference. e.g. in the attached proof from our > > textbook the proof uses Hypothetical Syllogism to prove a > > Propositional expression. I don't quite see yet from the tutorials how > > to direct ProofPower in this way. Is it possible? Does anyone have > > experience using ProofPower like this? If so, I would appreciate some > > guidance. It seems so far in my observations, that pp is used by > > selecting some "tactics" which then guide pp to find a proof, but we > > would need to direct each step as part of the learning process. > > Thanks, Dave > > > The proof you exhibit is what we would call a "forward proof". > The subgoal package is used for what we call "backward" (or goal > oriented) proofs. > > A forward proof for the result you require runs like this: > > val L1 = asm_rule ¬P ´ Q®; > val L2 = asm_rule ¬Q ´ R®; > val L3 = ´_trans_rule L1 L2; > val L4 = asm_rule ¬R ´ P®; > val L5 = ¤_intro L3 L4; > > Except that the characters are a mess because I just copied > and pasted from the xpp window which doesn't work. > > The value of L5 will be the desired result/ > > I attach a proofpower document containing the proof. > > The documentation for the inference rules is in the reference manual > USR029 section 8.1. > > The HOL Tutorial Notes USR013 has perhaps more accessible descriptions of > a selection of rules in Chapter 5. > > Roger Jones > > > > > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] ProofPower and Discrete Math
I am interested in using ProofPower to aid in the teaching of Discrete Math. I would like to assist the students in developing proofs using specific rules of inference. e.g. in the attached proof from our textbook the proof uses Hypothetical Syllogism to prove a Propositional expression. I don't quite see yet from the tutorials how to direct ProofPower in this way. Is it possible? Does anyone have experience using ProofPower like this? If so, I would appreciate some guidance. It seems so far in my observations, that pp is used by selecting some "tactics" which then guide pp to find a proof, but we would need to direct each step as part of the learning process. Thanks, Dave ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Proofpower Digest, Vol 88, Issue 8
Thank you Rob, I just tried this and it works perfectly! It is a testament to the quality of the design of ProofPower that it is so versatile and adaptable. I see you got QCheck to work too; It looks very promising to create unit tests easily. I hadn't known that you could choose to run different interpreters in xpp! Great program; I will use it this next semester in my computer science classes. I am not sure how far I can get with "proofs" for the beginning intro to cs classes, but at the very least, I can use it to introduce literate, functional programming. I used Object-Z in my OOP classes last semester using this tool: quote from Kenny Hunt (http://charity.cs.uwlax.edu): Toze: The Object Z EditorI have worked with Kasi Periyasamy and Tim Parker to develop a graphical editor for Object Z specifications. The application is rolled into a single executable jar file. Download the toze-2.0.2.jar file and then double-click on it once you've got it on your desktop. It was fairly successful for most students, and demonstrated the value of unambiguous specifications. I am hoping to use zed within ProofPower for similar reasons if I can get up to speed on it soon enough. -Dave Topham (http://dev2.ohlone.edu/people/dtopham/) On Mon, Dec 29, 2014 at 9:00 AM, wrote: > Send Proofpower mailing list submissions to > proofpower@lemma-one.com > > To subscribe or unsubscribe via the World Wide Web, visit > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > or, via email, send a message with subject or body 'help' to > proofpower-requ...@lemma-one.com > > You can reach the person managing the list at > proofpower-ow...@lemma-one.com > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Proofpower digest..." > > > Today's Topics: > >1. Re: Can QCheck work in xpp? (Rob Arthan) >2. Re: Can QCheck work in xpp? (Rob Arthan) > > > -- > > Message: 1 > Date: Mon, 29 Dec 2014 15:16:53 + > From: Rob Arthan > To: ProofPower List > Cc: David Topham > Subject: Re: [ProofPower] Can QCheck work in xpp? > Message-ID: <51b6efb9-323d-442e-800e-d0b4ef267...@lemma-one.com> > Content-Type: text/plain; charset="windows-1252" > > David, > > On 28 Dec 2014, at 05:08, David Topham wrote: > > > I am not sure if this is a bug in xpp or if it is a user (me!) error, > but I am trying to use a unit test framework named QCheck within xpp and it > fails. I have attached the doc file and the sml and pdf file produced via > docsml. In the files, I have shown where the error occurs. Since it works > ok in poly, then I expected it to also work within xpp so I am asking if > anyone has tried this; or sees why it may not work as I expect. > > > > The problem is not with xpp but with the extensions to Standard ML that > ProofPower uses > to provide object language quotations and support an extended character > set for use in forming > ML names (so we can use mathematical symbols to form ML names). The > extended language is > called ProofPower-ML. When you run xpp with a command line something like: > > xpp -d hol > or > xpp UT.doc -d zed > > xpp just spawns a process running the command ?pp -d hol? or ?pp -d zed? > which invokes > a session on the hol or zed database and communicates with that process > via a > UN*X pseudo-terminal. Unless you do something special, ?pp -d XYZ? will > run the ProofPower-ML read-eval-print loop. ProofPower-ML is implemented by > a pre-processor that encodes it into ASCII Standard ML and a > post-processor > that converts the ASCII output from the ML compiler?s eval-print function > into the extended character set. > > Your problem is then occurring because we use ?Q? to encode > non-ASCII characters, ?Q? itself being encoded as ??. So somewhat > bizarrely, you will find that: > > size ?QCheck? > > evaluates to 9 in ProofPower-ML. PolyML.make expects a Standard ML > string, rather than a ProofPower-ML string, so it can?t find the file and > raises an error. > > If you just want to use xpp as a user interface to Poly/ML and you don?t > want > the ProofPower specification and theorem-proving tools, then you can > ask xpp to run a different command line. E.g., > > xpp -c poly > > or > > xpp -f UT.doc -c poly > > will bring up xpp talking to a poly session (and editing a new empty file > in the first case and the file UT.doc in the second). (Note that for > not very good reasons, the command line requires -f before
[ProofPower] Can QCheck work in xpp?
I am not sure if this is a bug in xpp or if it is a user (me!) error, but I am trying to use a unit test framework named QCheck within xpp and it fails. I have attached the doc file and the sml and pdf file produced via docsml. In the files, I have shown where the error occurs. Since it works ok in poly, then I expected it to also work within xpp so I am asking if anyone has tried this; or sees why it may not work as I expect. -Thanks, Dave Topham UT.doc Description: MS-Word document UT.sml Description: Binary data UT.pdf Description: Adobe PDF document ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] ProofPower build problems
Rob, I am really enjoying learning about ProofPower and so impressed at the
amount of documentation and extra facilities that I didn't even know were
part of this program. e.g. I have long been interested in "literate
programming" and find your approach using =SML and =TEX to be very
efficient. I read in the usr001.pdf that it is possible to add other
languages such as =C but don't quite see what I have to do to make that
work. I tried just putting =C followed by the some C code, but got errors
from docsml that say =C is not defined.
The example is from page 56 in the section about sieve so I imagine the
info is there somewhere, but I find that section a bit difficult for me at
this early stage of learning about ProofPower. I found I can use =DUMP to
get a similar effect, however in the document =C would certainly be more
descriptive.
-Dave
p.s. I am cc'ing the literate programming group to this discussion because
I think there may be others that do not know about ProofPower
<http://www.lemma-one.com/ProofPower/index/> and its support for literate
programming.
On Fri, Dec 19, 2014 at 2:50 PM, David Topham wrote:
> Rob, Fantastic! That was the key! I reinstalled PolyML just to be sure
> and checked that poly and polyc worked OK, but still got same error
> building ProofPower. But I made the changes to the mkf (just xpp and hol,
> not zed) as you suggested and now it completed successfully. I had to
> install the standard Linux utilities to override BusyBox to get nroff, ed,
> and nl which are needed too. Anyway, now I can (finally) concentrate on
> learning ProofPower by looking at the tutorials on your site. If all goes
> well, I intend on using it as a supplement to teaching Discrete Math. I am
> excited to see some references to zed since I am also trying to learn to
> use Z for specifications. I appreciate your help getting me over these
> first hurdles. I use this less common distribution of Linux (TinyCore)
> since it is small enough to run within a virtual machine (I use Qemu) so
> can be carried around on a USB flash drive and run from within any
> computer! Makes it easier for students that can't install software on their
> own machines or school machines.
> -Dave
>
> On Thu, Dec 18, 2014 at 8:04 AM, Rob Arthan wrote:
>>
>> David,
>>
>> > On 17 Dec 2014, at 00:19, David Topham wrote:
>> >
>> > Maybe another non-Posix issue? Attached is latest build attempt. This
>> time it fails
>> > trying to build processes.cpp because pthread functions are undefined...
>> > (setting OS=linux made progress, then I had to install mkfontdir
>> utility and load the Xp libraries as well before getting to the current
>> error)
>> >
>>
>> What has actually happened is that it is failing to link the slrp-ml
>> executable,
>> almost certainly because the c++ command line it is using to do this does
>> not
>> identify the location of the pthreads and various XWindows libraries that
>> are
>> used by the Poly/ML runtime library. The error message talk about
>> processes.cpp
>> and xwindows.cpp because these are the Poly/ML source files that depend on
>> these libraries. You can now use a script polyc that is supplied with
>> Poly/ML to
>> link standalone executables created with Poly/ML and it should take care
>> of locating all the libraries that are needed. If you change src/dev.mkf
>> to
>> use polyc as shown in the following diff output, then it may work.
>>
>> --- dev.mkf-2013-08-04 15:22:21.0 +0100
>> +++ dev.mkf 2014-12-18 15:49:48.0 +
>> @@ -65,9 +65,7 @@
>> PPBuild.pp'save ();
>> SLRPSTARTCMD= \
>> { { echo "$(SLRPSTARTMLCMD)" | poly ; } && \
>> - LD_RUN_PATH=$(LD_RUN_PATH) \
>> - c++ $(POLYLINKFLAGS) -o slrp-ml pp-ml.o \
>> - -L$(POLYLIBDIR) -lpolymain -lpolyml && \
>> + polyc -o slrp-ml pp-ml.o && \
>> { echo "$(SLRPMAKEDBCMD)" | slrp-ml ; } }
>>
>>
>> If that does work, then you will either need to make the same changes
>> to src/hol.mkf and src/zed.mkf, or you may just be better off downloading
>> the latest development version of ProofPower (which will become the
>> next stable release very shortly). You can find this here:
>>
>>
>> http://www.lemma-one.com/ProofPower/getting/snapshots/OpenProofPower-3.1w2.tgz
>>
>> If it does not work, then we need to look into how you managed to build
>> Poly/ML
>> since the compiler managed to link itself and it will have the same
>>
[ProofPower] ProofPower build problems
Rob, Fantastic! That was the key! I reinstalled PolyML just to be sure
and checked that poly and polyc worked OK, but still got same error
building ProofPower. But I made the changes to the mkf (just xpp and hol,
not zed) as you suggested and now it completed successfully. I had to
install the standard Linux utilities to override BusyBox to get nroff, ed,
and nl which are needed too. Anyway, now I can (finally) concentrate on
learning ProofPower by looking at the tutorials on your site. If all goes
well, I intend on using it as a supplement to teaching Discrete Math. I am
excited to see some references to zed since I am also trying to learn to
use Z for specifications. I appreciate your help getting me over these
first hurdles. I use this less common distribution of Linux (TinyCore)
since it is small enough to run within a virtual machine (I use Qemu) so
can be carried around on a USB flash drive and run from within any
computer! Makes it easier for students that can't install software on their
own machines or school machines.
-Dave
On Thu, Dec 18, 2014 at 8:04 AM, Rob Arthan wrote:
>
> David,
>
> > On 17 Dec 2014, at 00:19, David Topham wrote:
> >
> > Maybe another non-Posix issue? Attached is latest build attempt. This
> time it fails
> > trying to build processes.cpp because pthread functions are undefined...
> > (setting OS=linux made progress, then I had to install mkfontdir utility
> and load the Xp libraries as well before getting to the current error)
> >
>
> What has actually happened is that it is failing to link the slrp-ml
> executable,
> almost certainly because the c++ command line it is using to do this does
> not
> identify the location of the pthreads and various XWindows libraries that
> are
> used by the Poly/ML runtime library. The error message talk about
> processes.cpp
> and xwindows.cpp because these are the Poly/ML source files that depend on
> these libraries. You can now use a script polyc that is supplied with
> Poly/ML to
> link standalone executables created with Poly/ML and it should take care
> of locating all the libraries that are needed. If you change src/dev.mkf to
> use polyc as shown in the following diff output, then it may work.
>
> --- dev.mkf-2013-08-04 15:22:21.0 +0100
> +++ dev.mkf 2014-12-18 15:49:48.0 +
> @@ -65,9 +65,7 @@
> PPBuild.pp'save ();
> SLRPSTARTCMD= \
> { { echo "$(SLRPSTARTMLCMD)" | poly ; } && \
> - LD_RUN_PATH=$(LD_RUN_PATH) \
> - c++ $(POLYLINKFLAGS) -o slrp-ml pp-ml.o \
> - -L$(POLYLIBDIR) -lpolymain -lpolyml && \
> + polyc -o slrp-ml pp-ml.o && \
> { echo "$(SLRPMAKEDBCMD)" | slrp-ml ; } }
>
>
> If that does work, then you will either need to make the same changes
> to src/hol.mkf and src/zed.mkf, or you may just be better off downloading
> the latest development version of ProofPower (which will become the
> next stable release very shortly). You can find this here:
>
>
> http://www.lemma-one.com/ProofPower/getting/snapshots/OpenProofPower-3.1w2.tgz
>
> If it does not work, then we need to look into how you managed to build
> Poly/ML
> since the compiler managed to link itself and it will have the same library
> dependencies.
>
> Regards,
>
> Rob.
>
>
> > On Tue, Dec 16, 2014 at 1:19 PM, Rob Arthan wrote:
> > David,
> >
> > On 16 Dec 2014, at 16:25, David Topham wrote:
> >
> >> Thanks for helping Rob, TinyCore does have uname, and that command
> returns "Linux".
> >>
> >> It uses BusyBox for shell commands and a subset of dd is supported
> which does not have the lcase option!
> >>
> >
> > Ah! I try to make the ProofPower build process only use POSIX features
> > of the usual UN*X utilities. BusyBox’s dd is not POSIX-compliant if it
> doesn’t
> > support conv=lcase.
> >
> > xpp.mkf is the only ProofPower make file that needs this trick, so if
> you just edit it to say
> >
> > OS=linux
> >
> > you should be able to make more progress. I will be interested to hear
> how you get on.
> >
> > Regards,
> >
> > Rob.
> >
> >> (see attached)
> >>
> >> -Dave
> >>
> >> On Tue, Dec 16, 2014 at 2:02 AM, Rob Arthan wrote:
> >> David,
> >>
> >> > On 15 Dec 2014, at 23:43, David Topham wrote:
> >> >
> >> > It is version 2.9.1w8... and here is the latest attempt (attached).
> >> >
> >> >
> >> > I notice that SOLARIS is on the compile line
Re: [ProofPower] ProofPower build problems (was, Re: GUI Interface (Motif))
Maybe another non-Posix issue? Attached is latest build attempt. This time
it fails
trying to build processes.cpp because pthread functions are undefined...
(setting OS=linux made progress, then I had to install mkfontdir utility
and load the Xp libraries as well before getting to the current error)
On Tue, Dec 16, 2014 at 1:19 PM, Rob Arthan wrote:
>
> David,
>
> On 16 Dec 2014, at 16:25, David Topham wrote:
>
> Thanks for helping Rob, TinyCore does have uname, and that command
> returns "Linux".
>
> It uses BusyBox for shell commands and a subset of dd is supported which
> does not have the lcase option!
>
>
> Ah! I try to make the ProofPower build process only use POSIX features
> of the usual UN*X utilities. BusyBox’s dd is not POSIX-compliant if it
> doesn’t
> support conv=lcase.
>
> xpp.mkf is the only ProofPower make file that needs this trick, so if you
> just edit it to say
>
> OS=linux
>
> you should be able to make more progress. I will be interested to hear how
> you get on.
>
> Regards,
>
> Rob.
>
> (see attached)
>
> -Dave
>
> On Tue, Dec 16, 2014 at 2:02 AM, Rob Arthan wrote:
>>
>> David,
>>
>> > On 15 Dec 2014, at 23:43, David Topham wrote:
>> >
>> > It is version 2.9.1w8... and here is the latest attempt (attached).
>> >
>> >
>> > I notice that SOLARIS is on the compile line which is not true..should
>> be LINUX perhaps?
>> > but how do I influence that?
>>
>> The relevant makefile (src/xpp.mkf) uses the following command to
>> determine the OS:
>>
>> uname -s | dd conv=lcase 2>/dev/null
>>
>> Is your TinyLinux installation missing uname or dd?
>>
>> By the way, at the point that this has failed, it hasn’t started trying
>> to compile any ML.
>>
>> Regards,
>>
>> Rob.
>>
>>
>> >
>> > On Mon, Dec 15, 2014 at 2:40 PM, Rob Arthan wrote:
>> > David,
>> >
>> >
>> >> On 15 Dec 2014, at 22:24, David Topham wrote:
>> >>
>> >> Rob, Yes I was following the instructions in the README file and did
>> ./configure, then ./install but it failed on the line in the Makefile that
>> invoked PolyML.commit();
>> >>
>> >> I replaced that in the Makefile with:
>> >> PolyML.export("mypoly",PolyML.rootFunction);
>> >>
>> >> ...and it ran further, but still I have been unable to compile it
>> successfully all the way with other errors I haven't tracked down yet. If
>> you have time, I could keep trying, and report to you what I can't figure
>> out on my own.
>> >
>> > I have copied this over to the ProofPower mailing list where we should
>> be able to answer it for you. What version have you downloaded? In version
>> 2.9.1w8, there is a spurious occurrence of PolyML.commit in src/dev.mkf,
>> but it is in a variable that is no longer used and shouldn’t stop anything
>> building.
>> >
>> > Regards,
>> >
>> > Rob.
>> >
>>
>> ___
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>
>
>
build.log
Description: Binary data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] ProofPower build problems (was, Re: GUI Interface (Motif))
Thanks for helping Rob, TinyCore does have uname, and that command returns
"Linux".
It uses BusyBox for shell commands and a subset of dd is supported which
does not have the lcase option!
(see attached)
-Dave
On Tue, Dec 16, 2014 at 2:02 AM, Rob Arthan wrote:
>
> David,
>
> > On 15 Dec 2014, at 23:43, David Topham wrote:
> >
> > It is version 2.9.1w8... and here is the latest attempt (attached).
> >
> >
> > I notice that SOLARIS is on the compile line which is not true..should
> be LINUX perhaps?
> > but how do I influence that?
>
> The relevant makefile (src/xpp.mkf) uses the following command to
> determine the OS:
>
> uname -s | dd conv=lcase 2>/dev/null
>
> Is your TinyLinux installation missing uname or dd?
>
> By the way, at the point that this has failed, it hasn’t started trying to
> compile any ML.
>
> Regards,
>
> Rob.
>
>
> >
> > On Mon, Dec 15, 2014 at 2:40 PM, Rob Arthan wrote:
> > David,
> >
> >
> >> On 15 Dec 2014, at 22:24, David Topham wrote:
> >>
> >> Rob, Yes I was following the instructions in the README file and did
> ./configure, then ./install but it failed on the line in the Makefile that
> invoked PolyML.commit();
> >>
> >> I replaced that in the Makefile with:
> >> PolyML.export("mypoly",PolyML.rootFunction);
> >>
> >> ...and it ran further, but still I have been unable to compile it
> successfully all the way with other errors I haven't tracked down yet. If
> you have time, I could keep trying, and report to you what I can't figure
> out on my own.
> >
> > I have copied this over to the ProofPower mailing list where we should
> be able to answer it for you. What version have you downloaded? In version
> 2.9.1w8, there is a spurious occurrence of PolyML.commit in src/dev.mkf,
> but it is in a variable that is no longer used and shouldn’t stop anything
> building.
> >
> > Regards,
> >
> > Rob.
> >
>
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
