How to prove n+0 = 0+n in ATS2

Hello,

I am trying to play with proofs(newbie) in ATS2 and I am unable to solve
the simple case of n+0 = 0+n.

I have dataprop PLUS defined as :

dataprop PLUS (int,int,int) =
| {n:nat} PLUS_base (0 , n , n) of ()
| {m,n,p:nat} PLUS_ind (m+1,n,p+1) of PLUS (m,n,p)

I can show that PLUS (0,n,n) = PLUS (n,0,n) like this :

extern prfun zero_plus_comm {n:nat} (pf : PLUS(0,n,n)) : PLUS (n,0,n)

primplement zero_plus_comm {n} (pf) =
let prfun zero_plus {n:nat} ..
(pf : PLUS(0,n,n)) : PLUS (n,0,n) =
case+ pf of
| PLUS_base () => sif n==0 then PLUS_base()
else PLUS_ind (zero_plus {n-1} (PLUS_base ()))

in
zero_plus {n} (pf)
end

But I am unable to show other way i.e PLUS (n,0,n) = PLUS (0,n,n) i.e for :

extern prfun zero_plus_comm2 {n:nat} (pf : PLUS(n,0,n)) : PLUS (0,n,n)

Base case is simple , but for inductive case if prev proof is of the form

PLUS(n-1,0,n-1) and PLUS(0,n-1,n-1) is also true , so how do I construct
PLUS(0,n,n) from these.

Thanks

Try:

extern
prfun lemma_plus_elim {m,n:nat}{s:int} (pf: PLUS(m,n,s)): [s==m+n] void

Also, the following function is not properly formulated:

extern prfun zero_plus_comm2 {n:nat} (pf : PLUS(n,0,n)) : PLUS (0,n,n)

You don’ t need any argument:

extern prfun zero_plus_comm2 {n:nat} () : PLUS (0,n,n)On Thursday, December 26, 2013 5:44:39 AM UTC-5, chota singh wrote:

Hello,

I am trying to play with proofs(newbie) in ATS2 and I am unable to solve
the simple case of n+0 = 0+n.

I have dataprop PLUS defined as :

dataprop PLUS (int,int,int) =
| {n:nat} PLUS_base (0 , n , n) of ()
| {m,n,p:nat} PLUS_ind (m+1,n,p+1) of PLUS (m,n,p)

I can show that PLUS (0,n,n) = PLUS (n,0,n) like this :

extern prfun zero_plus_comm {n:nat} (pf : PLUS(0,n,n)) : PLUS (n,0,n)

primplement zero_plus_comm {n} (pf) =
let prfun zero_plus {n:nat} ..
(pf : PLUS(0,n,n)) : PLUS (n,0,n) =
case+ pf of
| PLUS_base () => sif n==0 then PLUS_base()
else PLUS_ind (zero_plus {n-1} (PLUS_base ()))

in
zero_plus {n} (pf)
end

But I am unable to show other way i.e PLUS (n,0,n) = PLUS (0,n,n) i.e for
:

extern prfun zero_plus_comm2 {n:nat} (pf : PLUS(n,0,n)) : PLUS (0,n,n)

Base case is simple , but for inductive case if prev proof is of the form

PLUS(n-1,0,n-1) and PLUS(0,n-1,n-1) is also true , so how do I construct
PLUS(0,n,n) from these.

Thanks