I have a question about chapter 11.3 of the ATS introduction. Why is and subtraction able to compile successfully, but not max(n1, n2) and n1 * n2?

[prehonor]

prfun mul_distribute {m,n1,n2:int}{p1,p2:int} (MUL(m, n1, p1), MUL(m, n2, p2)): MUL(m, max(n1,n2), max(p1,p2)) // + and - are right but max and * primplement mul_distribute {m,n1,n2}{p1,p2} (pf1, pf2) = let // prfun auxnat {m:nat}{p1,p2:int} .<m>. ( pf1: MUL(m, n1, p1), pf2: MUL(m, n2, p2) ) : MUL(m, max(n1,n2), max(p1,p2)) = ( case+ (pf1, pf2) of | (MULbas(), MULbas()) => MULbas() | (MULind(pf1), MULind pf2) => MULind(auxnat (pf1, pf2)) ) (* end of [auxnat] *) // in // sif m >= 0 then ( auxnat (pf1, pf2) ) // end of [then] else let prval MULneg(pf1) = pf1 prval MULneg(pf2) = pf2 in MULneg(auxnat (pf1, pf2)) end // end of [else] // end // end of [mul_distribute]

[githwxi]

Note that m*max(n1,n2) = max(m*n1, m*n2) is true only when m >= 0 holds.

The constraint-solver in ATS can only handle linear constraints; using * is restricted.

[prehonor]

Note that m*max(n1,n2) = max(m*n1, m*n2) is true only when m >= 0 holds.

The constraint-solver in ATS can only handle linear constraints; using * is restricted.

Thank you for your response. I have redefined MUL, but I am still getting some sort of error. `dataprop MUL1(int, int, int) = // I want set the first int to nat ，but The compiler does not allow me to do this. | {n:int} MULbas1(0, n, 0) of () | {m:nat}{n,p:int} MULind1(m+1, n, p+n) of MUL1(m, n, p) prfun mul_distribute1 {m:nat}{n1,n2:int}{p1,p2:int} (MUL1(m, n1, p1), MUL1(m, n2, p2)): MUL1(m, max(n1,n2), max(p1,p2))

primplement mul_distribute1 {m,n1,n2}{p1,p2} // static arity mismatch: fewer arguments are expected. (pf1, pf2) = let // prfun auxnat {m:nat| m >= 0}{p1,p2:int} .. ( pf1: MUL1(m, n1, p1), pf2: MUL1(m, n2, p2) // the static identifier [n1] is unrecognized. ) : MUL1(m, max(n1,n2), max(p1,p2)) = ( case+ (pf1, pf2) of | (MULbas1(), MULbas1()) => MULbas1() | (MULind1(pf1), MULind1 pf2) => MULind1(auxnat (pf1, pf2)) ) ( end of [auxnat] ) // in auxnat (pf1, pf2)

// end // end of [mul_distribute] `

[githwxi]

I studied this one a bit.

Your proof does not work because the proof makes use of the following identity:

max(x1, x2) + max(y1, y2) = max(x1+y1, x2+y2)

where is NOT true.

(Also, Your proof has a syntax error: {m,n1,n2} should be {m}{n1,n2})

However, one can give a non-inductive proof as follows. BTW, a proof for mul_increasing is not given here (it can be given based on induction).

dataprop
MUL1(int, int, int) = // I want set the first int to nat ，but The compiler does not allow me to do this.                                             
| {n:int} MULbas1(0, n, 0) of ()
| {m:nat}{n,p:int}
MULind1(m+1, n, p+n) of MUL1(m, n, p)

extern
prfun
mul_increasing
{m:nat}{n1,n2:int | n1 >= n2}{p1,p2:int}
(MUL1(m, n1, p1), MUL1(m, n2, p2)): [p1 >= p2] void
extern
prfun
mul_distribute1
{m:nat}{n1,n2:int}{p1,p2:int}
(MUL1(m, n1, p1), MUL1(m, n2, p2)): MUL1(m, max(n1,n2), max(p1,p2))

primplement
mul_distribute1
{m}{n1,n2}{p1,p2} // static arity mismatch: fewer arguments are expected.                                                                             
(pf1, pf2) =
sif n1 >= n2
then
let prval () = mul_increasing(pf1, pf2) in pf1 end
else
let prval () = mul_increasing(pf2, pf1) in pf2 end

[githwxi]

Here is a proof of mul_increasing:

prfun
mul_increasing
{m:nat}
{n1,n2:int | n1 >= n2}{p1,p2:int}.<m>.
(pf1:MUL1(m, n1, p1)
,pf2:MUL1(m, n2, p2)): [p1 >= p2] void =
sif m == 0
then
let
prval MULbas1() = pf1
prval MULbas1() = pf2 in () end
else
let
prval MULind1(pf1) = pf1
prval MULind1(pf2) = pf2 in mul_increasing(pf1, pf2) end

[prehonor]

Here is a proof of mul_increasing:

prfun
mul_increasing
{m:nat}
{n1,n2:int | n1 >= n2}{p1,p2:int}.<m>.
(pf1:MUL1(m, n1, p1)
,pf2:MUL1(m, n2, p2)): [p1 >= p2] void =
sif m == 0
then
let
prval MULbas1() = pf1
prval MULbas1() = pf2 in () end
else
let
prval MULind1(pf1) = pf1
prval MULind1(pf2) = pf2 in mul_increasing(pf1, pf2) end

I made an error in interpreting the program, but I don’t know where I went wrong. Below is my process of interpreting the program:

(MULind1 pf1, MULind1 pf2) represents Max(MULind1 pf1, MULind1 pf2)… (1)

MULind1(auxnat(pf1, pf2)) represents m*max(n1, n2) = (m-1)max(n1, n2) + max(n1, n2) (according to the MULind1 rule)… (2)

Let’s assume n1 > n2. Based on the induction hypothesis, when m-1 is true, (m-1)max(n1, n2) = (m-1)n1 and max(n1, n2) = n1.

Therefore, according to (2), we have MULind1(auxnat(pf1, pf2)) = (m-1)*n1 + n1.

Then, according to (1), Max(MULind1 pf1, MULind1 pf2) = max(mn1, mn2).

Based on the definition of MULind1, we have max(mn1, mn2) = max((m-1)n1+n1, (m-1)n2+n2).

Therefore, we conclude that max((m-1)n1+n1, (m-1)n2+n2) = (m-1)*n1 + n1, that is (MULind1 pf1, MULind1 pf2) => MULind1(auxnat(pf1, pf2)).

Then, according to (1), Max(MULind1 pf1, MULind1 pf2) = max(mn1, mn2).

Based on the definition of MULind1, we have max(mn1, mn2) = max((m-1)n1+n1, (m-1)n2+n2).

Therefore, we conclude that max((m-1)n1+n1, (m-1)n2+n2) = (m-1)*n1 + n1, that is (MULind1 pf1, MULind1 pf2) => MULind1(auxnat(pf1, pf2)).

[githwxi]

Therefore, we conclude that max((m-1)*n1+n1, (m-1)*n2+n2) = (m-1)*n1 + n1, that is (MULind1 pf1, MULind1 pf2) => MULind1(auxnat(pf1, pf2)).

The above step does not work. You made an implicit assumption (m-1)n1 >= (m-1)n2, which the type-checker does not know.

[prehonor]

Therefore, we conclude that max((m-1)*n1+n1, (m-1)*n2+n2) = (m-1)*n1 + n1, that is (MULind1 pf1, MULind1 pf2) => MULind1(auxnat(pf1, pf2)).

The above step does not work. You made an implicit assumption (m-1)n1 >= (m-1)n2, which the type-checker does not know. I would like to modify my previous reasoning and make corrections in two places:

1. Addition: prfun mul_distribute1 {m:nat}{n1,n2:int}{p1,p2:int} (MUL1(m, n1, p1), MUL1(m, n2, p2)): MUL1(m, max(n1,n2), max(p1,p2)) This function represents the desired conclusion that needs to be proven, which is max(mn1,mn2) = m*max(n1,n2).

   2. In order to prove the above conclusion, we need to show that (MULind1 pf1, MULind1 pf2) => MULind1(auxnat(pf1, pf2)) holds true. First, (MULind1 pf1, MULind1 pf2) = max((m-1)n1+n1, (m-1)n2+n2), which is true. Secondly, based on the induction hypothesis that assumes (m-1) holds true, we have MULind1(auxnat(pf1, pf2)) = (m-1)n1 + n2, which is also true. Therefore, (MULind1 pf1, MULind1 pf2) => MULind1(auxnat(pf1, pf2)) is true. This implies that max((m-1)n1+n, (m-1)n2+n2) = (m1)n1 + n2.

[githwxi]

This implies that max((m-1)n1+n, (m-1)n2+n2) = (m1)*n1 + n2.

You need (m-1)n1 >= (m-1)n2 here, but it is not yet proven. This is basically what mul_increasing is needed for.

[prehonor]

This implies that max((m-1)n1+n, (m-1)n2+n2) = (m1)*n1 + n2.

You need (m-1)n1 >= (m-1)n2 here, but it is not yet proven. This is basically what mul_increasing is needed for.

Your meaning is => This is an equal sign, which means that the expansion on the left side must equal the expansion on the right side, rather than an implication. It is not about the left side being true and the right side being true. Introducing an implication formula as true in this way is incorrect.

[githwxi]

I just want to stress that doing theorem-proving in ATS is not "natural"; it requires the user to "translate" a natural proof into a functional program. ATS was not designed for theorem-proving.There are many theorem-proving systems out there that do much better than ATS in this regard.

The "philosophical" point behind ATS is that programs are brittle but proofs are robust. By merely stating (not proving) theorems, one can use them to type-check programs; through type-checking, one can potentially flush out many potential bugs (e.g., out-of-bounds array subscripting).

[githwxi]

I am sorry. I have to stop here. Too busy with many other things at this moment.

[prehonor]

I am sorry. I have to stop here. Too busy with many other things at this moment.

Thank you very much for your response. I’m just worried that if I don’t understand the principles behind ATS proofs, it might affect my understanding of the subsequent chapters. I don’t quite understand the principles of ATS proof system, so I need some time to think. There might be more questions to consult you later.