-- ==========================================================
--> An example answer for exercises of lecture1
-->  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
  op _=_ : Nat Nat -> Bool {comm} .
  eq (X:Nat = X) = true .
  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} .
  vars X Y : Nat .
  eq 0 + Y = Y .
  eq (s X) + Y = s(X + Y) .
}

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

  -- declaration of CafeOBJ variables
  vars X Y Z  : Nat .

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

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

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

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

-- "mod PRED-PNAT+ (X :: PNAT+)" indicates that this module
-- "PRED-PNAT+" has a parameter "X" which satisfies the
-- constrains defined by the module "PNAT+".

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

-- ==========================================================
--> Property of PRED-PNAT+
-->        \forall 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
-- either (1) or (2) works
-- (1)
open PRED-PNAT+
-- arbitrary value
  op x : -> Nat .
-- induction hypothesis
  eq x + 0 = x .
-- check
  red +rz(s(x)) .
close
-- (2)
open PRED-PNAT+
-- arbitrary value
  op x : -> Nat .
-- check
  red +rz(x) implies +rz(s(x)) .
close
--
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-PNAT+
-->  \forall 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
-- (1) and (2) are same in CafeOBJ
-- (1)
open PRED-PNAT+
-- check
  red +assoc(0,Y:Nat,Z:Nat) .
close
-- (2)
open PRED-PNAT+
-- arbitrary values
  ops y z : -> Nat .
-- check
  red +assoc(0,y,z) .
close
--> II Induction case
-- either (1) or (2) works
-- (1)
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,X:Nat) .
close
-- (2)
open PRED-PNAT+
  ops x y z : -> Nat .
-- check
  red +assoc(x,y,z) implies +assoc(s(x),y,z) .
  -- notice that +assoc(x,y,z) is an instance of 
  -- the induction hypothesis:
  -- \forall Y,Z:Nat.+assoc(x,Y,Z).
  -- i.e. eq (x + Y:Nat) + Z:Nat = x + (Y + Z) .
close
--
--> QED
-- ==========================================================

-- ==========================================================
--> Property \forall 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+
-- arbitrary values
  op y : -> Nat .
-- check
  red +rs(0,y) .
close
--> II Induction case
open PRED-PNAT+
-- arbitrary values
  ops x y : -> Nat .
-- induction hypothesis
  eq x + s(Y:Nat) = s(x + Y) .
-- check
  red +rs(s(x),y) .
close
--
--> QED
-- ==========================================================

-- ==========================================================
--> Property \forall X,Y:Nat.(X + Y = Y + X)
-- Proof: By induction on X
--> I Base case 
-- This case uses +rz(y) as a lemma.
open PRED-PNAT+
-- arbitrary values
  op y : -> Nat .
-- check
  -- +rz(Y:Nat) is already proved
  red +rz(y) implies +comm(0,y) .
close
--> II Induction case 
open PRED-PNAT+
-- arbitrary values
  op x : -> Nat .
-- assumptions 
  -- +rs(X:Nat,Y:Nat) is already proved
  eq X:Nat + (s Y:Nat) = s(X + Y) .
-- induction hypothesis
  eq x + Y:Nat = Y + x .
-- check
  red +comm(s(x),Y:Nat) .
close  
--
--> QED
-- ==========================================================

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

  vars X Y : Nat .

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

  -- _*_ connects stronger than _+_ 
  -- because it has smaller precedence (prec:)
  op _*_ : Nat Nat -> Nat {prec: 29 r-assoc}
  eq 0 * Y = 0 .
  eq s(X) * Y = Y + (X * Y) .
}

-- "{assoc comm prec: 30}" declares that the operator "_+_"
-- is associative and commutative and parsing precedence 30.

-- inspect the precedences of operators "_+_", "_*_", and
-- "_=_" by running the following commands

select PNAT+*
show op (_ + _)
show op (_ * _)

show op (_ = _)  
describe op (_ = _)

--> test of PNAT+*
open PNAT+*
  red s s s 0 + s s s s 0 .
  red s s s 0 * s s s s 0 .

  parse s s 0 = s 0 + s 0 .
  red s 0 + s s 0 * s s s 0 .

  parse s s 0 = s 0 + s 0 .
  red s s 0 = s 0 + s 0 .

  parse 0 + s 0 + s s 0 = s s 0 * s 0 * 0 .
  red 0 + s 0 + s s 0 = s s 0 * s 0 * 0 .
close

--> fundamental predicates of PNAT+*
mod! PRED-PNAT+* (Y :: PNAT+*) {
  inc(PRED-PNAT+(Y))

  -- CafeOBJ variables
  vars X Y Z  : Nat

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

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

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

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

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

-- "PRED-PNAT+(Y)" in "pr(PRED-PNAT+(Y))" indicates the
-- module obtained by replacing "X" of "PRED-PNAT+ (X ::
-- PNAT+)" with "Y" having constrain of "(Y :: PNAT+*)"
-- which is declared in "PRED-PNAT+* (Y :: PNAT+*)".
-- "PNAT+*" is obtained by refining "PNAT+", and it is clear
-- that "Y" satisfies the all the constrains required by "(X
-- :: PNAT+)".

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

-- ==========================================================
--> Property 
-->    \forall X,Y,Z:Nat.((X + Y) * Z = X * Z + Y * Z)
--    (i.e. *disr(X:Nat,Y:nat,Z:Nat) = true)
-- Proof: By induction on X.
--> I Base case 
open PRED-PNAT+*
-- arbitrary values
  ops y z : -> Nat .
-- check
  red *disr(0,y,z) .
close
--> II Induction case 
open PRED-PNAT+*
-- arbitrary values
  ops x y z : -> Nat .
-- induction hypothesis
  eq (x + Y:Nat) * Z:Nat = (x * Z) + (Y * Z) .
-- check
  red *disr(s(x),y,z) .
close
--
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-PNAT+*
-->    \forall 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+*
-- arbitrary values
  ops y z : -> Nat .
-- check
  red *assoc(0,y,z) .
close
--> II Induction case
open PRED-PNAT+*
-- arbitrary values
  ops x y z : -> Nat .
-- assumption
  -- *disr(X:Nat,Y:Nat,Z:Nat) is already proved
  eq (X:Nat + Y:Nat) * Z:Nat = (X * Z) + (Y * Z) .
-- induction hypothesis
  eq (x * Y:Nat) * Z:Nat = x * (Y * Z) .
-- check
  red *assoc(s(x),y,z) .
close
--
--> QED
-- ==========================================================

-- ==========================================================
--> Property \forall X:Nat.(X * 0 = 0)
--     (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 .
-- check
  red *rz(x) implies *rz(s(x)) .
close
--
--> QED
-- ==========================================================

-- ==========================================================
--> Property \forall 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+*
-- arbitrary values
  op y : -> Nat .
-- check
  red *rs(0,y) .
close
--> II Induction case
open PRED-PNAT+*
-- arbitrary values
  ops x y : -> Nat .
-- induction hypothesis
  eq x * s(Y:Nat) = x + (x * Y) .
-- check
  red *rs(s(x),y) .
close
--
--> QED
-- ==========================================================

-- ==========================================================
--> Property \forall 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+*
-- arbitrary value
  op y : -> Nat .
-- check
  -- notice *rz(Y:Nat) is already proved
  red *rz(y) implies *comm(0,y) .
close
--> II Induction case
open PRED-PNAT+*
-- arbitrary values
  ops x y : -> Nat .
-- assumptions
  -- notice that *rs(X:Nat,Y:Nat) is already proved
  eq X:Nat * (s Y:Nat) = X + (X * Y) .
-- induction hypothesis
  eq x * Y:Nat = Y:Nat * x .
-- check
  red *comm(s(x),y) .
close
--
--> QED
-- ==========================================================

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