-- assignment1template.cafe file for i613-1312

-- **********************************************************
-- Problem 1: Complete the following proof scors about 
--              Peano style natural numbers
-- **********************************************************

-- ==========================================================
--> Template for answers to exercises of lecture01 
-->  Proof scores for verifications of properties (including
-->  associativity and commutativity of _+_ and _*_) about
-->  Peano Style natural numbers
-- ==========================================================

--> Peano style natural numbers
mod! PNAT {
  [ Nat ]
  op 0 : -> Nat {constr} .
  op s_ : Nat -> Nat {constr} .

  -- equality over the natural numbers
  eq (0 = s(Y:Nat)) = false .
  eq (s(X:Nat) = s(Y:Nat)) = (X = Y) .
}

--> PNAT with plus _+_ operation
mod! PNAT+ {
  pr(PNAT)
  op _+_ : Nat Nat -> Nat {r-assoc} .
  eq 0 + Y:Nat = Y .
  eq (s X:Nat) + Y:Nat = s(X + Y) .
}

--> fundamental predicates of PNAT+
mod! PRED-PNAT+ {pr(PNAT+)

  -- 0 is right zero of _+_
  op +rz : Nat -> Bool .
  eq +rz(X:Nat) = (X + 0 = X) .

  -- associativity of _+_
  op +assoc : Nat Nat Nat -> Bool
  eq +assoc(X:Nat,Y:Nat,Z:Nat) = ((X + Y) + Z = X + (Y + Z)) .

  -- right successor of _+_
  op +rs : Nat Nat -> Bool
  eq +rs(X:Nat,Y:Nat) = (X + s(Y) = s(X + Y)) .

  -- commutativity of _+_
  op +comm : Nat Nat -> Bool
  eq +comm(X:Nat,Y:Nat) = (X + Y = Y + X) .
}

-- ==========================================================
-->  verification of the properties about _+_
-- ==========================================================

-- ==========================================================
--> Property of PRED-PNAT+
-->  (for-all X:Nat).(X + 0 = X)
-->  (i.e.  +rz(X:Nat) = true)
-- Proof: By induction on X.
--> I Base case
open PRED-PNAT+ .
-- check
  red +rz(0) .
close
--> II Induction case
open PRED-PNAT+ .
-- arbitrary value
  op x : -> Nat .
-- induction hypothesis
  eq x + 0 = x .
-- check
  red +rz(s(x)) .
close
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-PNAT+
-->  (for-all X,Y,Z:Nat).((X + Y) + Z = X + (Y + Z))
-->  (i.e. +assoc(X:Nat,Y:Nat,Z:Nat) = true)
-- Proof: By induction on X.
--> I Base case
open PRED-PNAT+ .
-- check
  red +assoc(0,`y:Nat,`z:Nat) .
close
--> II Induction case
open PRED-PNAT+ .
-- arbitrary values
  op x : -> Nat .
-- induction hypothesis
  eq (x + Y:Nat) + Z:Nat = x + (Y + Z) .
-- check
  red +assoc(s(x),`y:Nat,`z:Nat) .
close
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-PNAT+
-->   (for-all X,Y:Nat).(X + s(Y) = s(X + Y))
-->   (i.e. +rs(X:Nat,Y:Nat) = true)
-- Proof: By induction on X
--> I Base case
open PRED-PNAT+ .
-- check
...
close
--> II Induction case
open PRED-PNAT+ .
-- arbitrary values
... 
-- induction hypothesis
... 
-- check
... 
close
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-PNAT+
-->    (for-all X,Y:Nat).(X + Y = Y + X)
-->    (i.e. +comm(X:Nat,Y:Nat) = true)
-- Proof: By induction on X
--> I Base case 
open PRED-PNAT+ .
-- already proved lemma: +rz(Y:Nat)
... 
-- check
... 
close
--> II Induction case 
open PRED-PNAT+ .
-- already proved lemma: +rs(X:Nat,Y:Nat)
... 
-- arbitrary values
... 
-- induction hypothesis
... 
-- check
... 
close  
--> QED
-- ==========================================================

-- ==========================================================
--> PNAT with _+_ and _*_ operations
-- ==========================================================
mod! PNAT+* {
  pr(PNAT)  

  -- notice that assoc and comm of _+_ are already proved
  op _+_ : Nat Nat -> Nat {assoc comm prec: 30}
  eq 0 + Y:Nat = Y .
  eq s(X:Nat) + Y:Nat = s(X + Y) .

  -- _*_ connects stronger than _+_ 
  -- because it has smaller precedence (prec:)
  op _*_ : Nat Nat -> Nat {prec: 29 r-assoc}
  eq 0 * Y:Nat = 0 .
  eq s(X:Nat) * Y:Nat = Y + (X * Y) .
}
-- "{assoc comm prec: 30}" declares that the operator "_+_"
-- is associative and commutative and parsing precedence 30.

--> fundamental predicates of PNAT+*
mod! PRED-PNAT+* {
pr(PRED-PNAT+)
pr(PNAT+*)

  -- _*_ distributes over _+_ from right
  op *distr : Nat Nat Nat -> Bool
  eq *distr(X:Nat,Y:Nat,Z:Nat) = ((X + Y) * Z = X * Z + Y * Z) .

  -- associativity of _*_
  op *assoc : Nat Nat Nat -> Bool
  eq *assoc(X:Nat,Y:Nat,Z:Nat) = ((X * Y) * Z = X * (Y * Z)) .

  -- 0 is right zero of _*_
  op *rz : Nat -> Bool
  eq *rz(X:Nat) = (X * 0 = 0) .

  -- right successor of _*_
  op *rs : Nat Nat -> Bool
  eq *rs(X:Nat,Y:Nat) = (X * s(Y) = X + (X * Y)) .

  -- commutativity of _*_
  op *comm : Nat Nat -> Bool
  eq *comm(X:Nat,Y:Nat) = (X * Y = Y * X) .
}

** ==========================================================
-->  verification of properties about _*_
** ==========================================================

-- ==========================================================
--> Property of PRED-PNAT+*
-->    \forall X,Y,Z:Nat.((X + Y) * Z = X * Z + Y * Z)
--    (i.e. *distr(X:Nat,Y:nat,Z:Nat) = true)
-- Proof: By induction on X.
--> I Base case 
open PRED-PNAT+* .
-- check
... 
close
--> II Induction case 
open PRED-PNAT+* .
-- arbitrary value
... 
-- induction hypothesis
... 
-- check
... 
close
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-PNAT+*
-->   (for-all X,Y,Z:Nat).((X * Y) * Z = X * (Y * Z))
-->   (i.e. *assoc(X:Nat,Y:Nat,Z:Nat) = true)
-- Proof: By induction on X
--> I Base case
open PRED-PNAT+* .
-- check
... 
close
--> II Induction case
open PRED-PNAT+* .
-- already proved lemma:
... 
-- arbitrary values
... 
-- induction hypothesis
... 
-- check
... 
close
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-PNAT+*
-->   (for-all X:Nat).(X * 0 = 0)
-->   (i.e. *rz(X:Nat) = true)
-- Proof: By induction on X
--> I Base case
open PRED-PNAT+* .
-- check
... 
close
--> II Induction case
open PRED-PNAT+* .
-- arbitrary value
... 
-- induction hypothesis
... 
-- check
... 
close
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-PNAT+*
-->   (for-all X,Y:Nat).(X * s(Y) = X + (X * Y))
-->   (i.e. *rs(X:Nat,Y:Nat) = true)
-- Proof: By induction on X
--> I Base case
open PRED-PNAT+* .
-- check
... 
close
--> II Induction case
open PRED-PNAT+* .
-- arbitrary value
... 
-- induction hypothesis
... 
-- check
... 
close
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-PNAT+*
-->   (for-all X,Y:Nat).(X * Y = Y * X)
-->   (i.e. *comm(X:Nat,Y:Nat) = true)
-- Proof: By induction on X
--> I Base case
open PRED-PNAT+* .
-- already proved lemma:
... 
-- check
... 
close
--> II Induction case
open PRED-PNAT+* .
-- already proved lemma:
... 
-- arbitrary values
... 
-- induction hypothesis
... 
-- check
... 
close
--> QED
-- ==========================================================

-- ==========================================================
--> end
-- ==========================================================


-- **********************************************************
-- Problem 2: Complete the following proof scors about
                 generic list
-- **********************************************************

-- ==========================================================
--> Template for example answers to exercises of lecture02 
-->  Proof scores for verifications of properties of
-->      (for-all L:List).(rev1(rev1(L)) = L) .
-->      (for-all L:List).(rev1(L) = rev2(L)) 
-->  and others about generic list.
-- ==========================================================

--> for defining LIST
mod! LISTi (X :: TRIV) {
  [List]
  op nil : -> List {constr} .
  op _|_ : Elt.X List -> List {constr} .
}
--> parametrized list (i.e. generic list)
mod* LIST (X :: TRIV) {
  pr(LISTi(X))
  -- equality on the sort List
  eq (nil = (E2:Elt | L2:List)) = false .
  eq ((E1:Elt | L1:List) = (E2:Elt | L2:List))
      = (E1 = E2) and (L1 = L2) .
}

--> append _@_ over List
mod! LIST@(X :: TRIV) {
  pr(LIST(X))
  -- append operation over List
  op _@_ : List List -> List .
  eq [@1]: nil @ L2:List = L2 .                   
  eq [@2]: (E:Elt | L1:List) @ L2:List = E | (L1 @ L2) .   
}

--> predicates about _@_
mod PRED-LIST@(X :: TRIV) {
  pr(LIST@(X))

  -- nil is right identity of _@_
  pred @ri : List .
  eq @ri(L1:List) = ((L1 @ nil) = L1) .

  -- _@_ is associative
  pred @assoc : List List List .
  eq @assoc(L1:List,L2:List,L3:List) 
     = ((L1 @ L2) @ L3 = L1 @ (L2 @ L3)) .
}

-- ==========================================================
--> Property of PRED-LIST@
-->   (for-all L1:List).((L1 @ nil) = L1) 
-->   (i.e. @ri(L:Nat) = true)
-- Proof: By induction on L1.
-- I Base case
open PRED-LIST@ .
-- check
  red @ri(nil) .
close
-- II Induction case
open PRED-LIST@ .
-- arbitrary values
  op l : -> List .
-- induction hypothesis
  eq (l @ nil) = l .
-- check
  red @ri(`e:Elt | l) .
close
--> QED
-- ==========================================================

-- ==========================================================
-- Property of PRED-LIST@
-->  (for-all L1,L2,L3:List).((L1 @ L2) @ L3 = L1 @ (L2 @ L3)) 
-->   (i.e.  @assoc(L1:List,L2:List,L3:List) = true)
-- Proof: By induction on L1.
-- I Base case
open PRED-LIST@ .
-- check
  red @assoc(nil,`l2:List,`l3:List) .
close
-- II Induction case
open PRED-LIST@ .
-- arbitrary values
  op l1 : -> List .
-- induction hypothesis
   eq ((l1 @ L2:List) @ L3:List) = (l1 @ (L2 @ L3)) .
-- check
  red @assoc(`e:Elt | l1,`l2:List,`l3:List) .
close
--
--> QED
-- ==========================================================

-- ==========================================================
--> LIST with associative append _@_
-- ==========================================================
mod! LIST@a(X :: TRIV) {
  pr(LIST(X))

  -- notice that associativity {assoc} 
  -- and right identity [@3] is already proved
  op _@_ : List List -> List {assoc} .
  eq [@1]: nil @ L2:List = L2 .
  eq [@2]: (E:Elt | L1:List) @ L2:List = E | (L1 @ L2) .
  eq [@3]: L1:List @ nil = L1 .
}

--> LIST with reverse operations
mod! LISTrev(X :: TRIV) {
  pr(LIST@a(X))

  -- one argument reverse operation
  op rev1 : List -> List .
  eq rev1(nil) = nil .
  eq rev1(E:Elt | L:List) = rev1(L) @ (E | nil) .

  -- two arguments reverse operation
  op rev2 : List -> List .
  -- auxiliary function for rev2
  op sr2 : List List -> List .
  eq rev2(L:List) = sr2(L,nil) .
  eq sr2(nil,L2:List) = L2 .
  eq sr2(E:Elt | L1:List,L2:List) = sr2(L1,E | L2) .
}
-- ==========================================================
--> predicates about LISTrev
mod PRED-LISTrev(X :: TRIV) {
  pr(LISTrev(X))

  -- rev1 distributes over _@_ reversely
  pred rev1@ : List List .
  eq rev1@(L1:List,L2:List) = 
             (rev1(L1 @ L2) = rev1(L2) @ rev1(L1)) .

  -- rev1rev1 is identity function
  pred rev1rev1 : List .
  eq rev1rev1(L:List) = (rev1(rev1(L)) = L) .

  -- sr2 with _@_ 
  pred sr2@ : List List List .
  eq sr2@(L1:List,L2:List,L3:List)
     = (sr2(L1,L2) @ L3 = sr2(L1,L2 @ L3)) .

  -- rev1=rev2
  pred rev1=rev2 : List .
  eq rev1=rev2(L:List) = (rev1(L) = rev2(L)) .
}

-- ==========================================================
-->  verification of the properties about rev1 and rev2
-- ==========================================================

-- ==========================================================
--> Property of PRED-LISTrev
-->   (for-all L1,L2:List).
-->          (rev1@(L1 @ L2) = rev1(L2) @ rev1(L1))
-->   (i.e. rev1(L1:List,L2:List) = true)
-- Proof: By induction on L1.
--> I Base case
open PRED-LISTrev .
-- check
... 
close
--> II Induction case
open PRED-LISTrev .
-- arbitrary values
... 
-- induction hypothesis
... 
-- check
... 
close
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-LISTrev
-->   (for-all L:List).(rev1(rev1(L)) = L) .
-->   (i.e. rev1rev1(L:List) = true)
-- Proof: By induction on L.
--> I Base case
open PRED-LISTrev .
-- check
... 
close
--> II Induction case
open PRED-LISTrev .
-- already proved lemma:
... 
-- arbitrary values
... 
-- induction hypothesis
... 
-- check
... 
close
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-LISTrev
-->   (for-all L:List).(sr2(L1,L2) @ L3 = sr2(L1,L2 @ L3))
-->   (i.e. sr2@(L1:List,L2:List,L3:List) = true)
-- Proof: By induction on L1.
--> I Base case
open PRED-LISTrev .
-- check
... 
close
--> II Induction case
open PRED-LISTrev .
-- arbitrary values
... 
-- induction hypothesis
... 
-- check
... 
close
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-LISTrev
-->   (for-all L:List).(rev1(L) = rev2(L)) 
-->   (i.e. rev1=rev2(L:List) = true)
-- Proof: By induction on L.
--> I Base case
open PRED-LISTrev .
-- check
... 
close
--> II Induction case
open PRED-LISTrev .
-- already proved lemma:
... 
-- arbitrary values
... 
-- induction hypothesis
... 
-- check
... 
close
--> QED
-- ==========================================================

-- ==========================================================
--> end
-- ==========================================================