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