Re: Syntax-hilighting for ATS code in docbook

[Kiwamu Okabe]

On Wed, Feb 24, 2016 at 4:38 PM, gmhwxi <gmh...@gmail.com> wrote:
> The texting functions for syntax-hilighting are sats2xhtml and dats2xhtml:
>
> https://github.com/githwxi/ATS-Postiats/tree/master/doc/BOOK/ATS2TUTORIAL/ATEXT/myatexting.dats

Today, I tried to build your document using the syntax-hilighting.
However I get the attached result.

How to use sats2xhtml and dats2xhtml?

Best regards,
-- 
Kiwamu Okabe at METASEPI DESIGN

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dnOEE0uxsAjqwRL3dXwScxSq7vcj%2BORAhyGLGdgZuB_mA%40mail.gmail.com.

Title: Programmer-Centric Theorem-Proving

Introduction to Programming in ATS: Prev Chapter 11. Theorem-Proving in ATS/LF Next Programmer-Centric Theorem-Proving I have so far presented several formal proofs in ATS. However, constructing such formal proofs is at most a secondary issue in ATS. If I compare ATS with theorem-proving systems such as Isabelle and Coq, I would like to state emphatically that the design for theorem-proving in ATS takes a fundamentally different view of theorem-proving. In particular, theorem-proving in ATS does not take a foundational approach that establishes the validity of a theorem by reducing it to the validity of a minimal set of axioms and rules. Instead, theorem-proving in ATS is mostly done in a semi-formal manner and its primary purpose is to greatly diminish the chance of a programmer making use of incorrect assumptions or claims. In this regard, theorem-proving in ATS is rather similar to contructing informal paper-and-pencil proofs (in mathematics and elsewhere). I refer to this style of theorem-proving in ATS as being programmer-centric. In order to allow the reader to obtain a more concrete feel as to what this style of theorem-proving is like, I present in the rest of this section a simple but telling example of programmer-centric theorem-proving. Suppose we are to prove that the square of any rational number cannot equal 2. Note that this statement is a bit weaker than the one stating that the square root of 2 is irrational as the latter assumes the very existence of the square root of 2. Let us first sketch an informal proof as follows. Suppose (m/n)2=2 for some positive numbers m and n. Clearly, this means (m)2=2(n)2, implying m being an even number. Let m=2m2. We have (2m2)2=2(n)2, implying (n/m2)2=2. Clearly, m > n > m2 holds. If we assume that m is the least positive number satisfying (m/n)2=2 for some n, then a contradiction is reached as n satisfies the same property. Therefore, there is no rational number whose square equals 2. Clearly, this proof still holds if the number 2 is replaced with another prime number. The primary argument in the above informal proof can be encoded in ATS as follows: ##dats2xhtml_docbook("""// extern prfun mylemma_main {m,n,p:int | m*m==p*n*n}(PRIME(p)): [m2:nat | n*n==p*m2*m2] void // primplmnt mylemma_main {m,n,p}(pfprm) = let prval pfeq_mm_pnn = eqint_make{m*m,p*n*n}() prval () = square_is_nat{m}() prval () = square_is_nat{n}() prval () = lemma_PRIME_param(pfprm) prval pfmod1 = lemma_MOD0_intr{m*m,p,n*n}() prval pfmod2 = mylemma1{m,p}(pfmod1, pfprm) prval [m2:int] EQINT() = lemma_MOD0_elim(pfmod2) prval EQINT() = pfeq_mm_pnn prval () = __assert{p}{p*m2*m2,n*n}() where { extern prfun __assert{p:pos}{x,y:int | p*x==p*y}(): [x==y] void } (* end of [where] *) // end of [prval] in #[m2 | ()] end // end of [mylemma_main] // """) The interface for mylemma_main states that (m)2=p(n)2 implies (n)2=p(m2)2 for some natural number m2. Given two integers m and p, MOD0(m,p) means that m equals the product of p and q for some natural number q. This meaning is encoded into the following two proof functions: ##sats2xhtml_docbook("""// prfun lemma_MOD0_intr{m,p,q:nat | m==p*q}(): MOD0(m, p) // prfun lemma_MOD0_elim{m,p:int}(MOD0(m, p)): [q:nat] EQINT(m, p*q) // """) where EQINT is a dataprop declared as follows: ##sats2xhtml_docbook("""dataprop EQINT(int, int) = {x:int} EQINT(x, x) """) Given two integers x and y, EQINT(x, y) simply means that x equals y. Also, the function eqint_make is assgined the interface below: ##sats2xhtml_docbook("""prfun eqint_make{x,y:int | x == y}((*void*)): EQINT (x, y) """) Given an integer p, PRIME(p) means that p is a prime number. The following two proof functions are called in the above implementation of mylemma_main: ##sats2xhtml_docbook("""// prfun lemma_PRIME_param{p:int}(PRIME(p)): [p >= 2] void // prfun mylemma1{n,p:int}(MOD0(n*n, p), PRIME(p)): MOD0(n, p) // """) The proof function mylemma1 encodes a proposition stating that p divides n if p divides the square of n and p is also a prime number. I give no implementation of mylemma1 as I see the encoded proposition to be obviously true. Certainly, this is a kind of programmer-centric judgment. One may find that the following declaration in the implementation of mylemma_main looks mysterious: prval EQINT() = pfeq_mm_pnn Note that pfeq_mm_pnn is of the prop EQINT(m*m, p*(n*n)). Also, m equaling p*m2 for some natural number m2 is available when the above declaration is typechecked. This means that the equality between (p*m2)2 and p*(n)2 is added into the current store of (static) assumptions after the above declaration is typechecked. Please find on-line the entirety of an encoded proof showing that there exists no rational number whose square equals 2. Prev Home Next Example: Establishing Properties on Braun Trees Up Programming with Theorem-Proving