-- ==========================================================
--> CafeOBJ codes for lecture01 of i613-0912
-- ==========================================================

--> 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) .
}

-- "mod! PNAT {" indicates start of definition of module
-- named "PNAT". The definition ends at "}".  "!" in "mod!"
-- indicats that this module has tight semantics.

-- "[ Nat ]" is a declaration of a sort (i.e. set of
-- objects) named "Nat".

-- "op 0 : -> Nat {constr} ." is a declaration of operator
-- named "0" with no argument and return value of sort
-- "Nat".  That is, "0" is a constant of sort "Nat".  "0"
-- has an attribute of constructor indicated by
-- "{constr}". The last "." can be omitted.

-- "op s_ : Nat -> Nat {constr} ." is a declaration of
-- constructor operator named "s_" with an argument of sort
-- "Nat" and return value of sort "Nat".  "_" in "s_"
-- indicts the position where the argument placed.

-- "{comm}" indicates that the operator "_=_" is
-- commutative.

-- Notice that the first "=" of "eq (X:Nat = X) = true ." is
-- an equality operator on the sort "Nat", but the second
-- "=" is for declaring an equation in CafeOBJ language.

-- "eq (X:Nat = X) = true ." is a declaration of an
--  equation.  This equation means that for any object "X"
--  of sort Nat, "X = X" is equal to "true".  "X:Nat" is an
--  in line declaration of variable "X" and the scope of
--  this variable ends at the end of this equation.  "." at
--  the end and a space before it are must.

--> 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) .
}

-- "pr(PNAT)" indicates the importation of module "PNAT"
-- into this module with the importation mode of "pr"
-- (i.e. protecting).  There are three importation modes of
-- pr (protecting), ex (extending), and us (using) in
-- CafeOBJ.

-- "{r-assoc}" indicates that the operator "_+_" associate
-- to right.  This is just for parsing terms.

-- "vars X Y : Nat ." is a declaration of variables "X" and
-- "Y" of sort "Nat".  The scope of these variables ends at
-- the end of the module.  "." at the end can be omitted.

-- ==========================================================
--> special charactors of CafeOBJ
-- ==========================================================

-- Seven charactors of "(" ")" "," "[" "]" "{" "}" are
-- self-terminating characters of CafeOBJ.  A
-- self-terminating charactor is a printable ASCII character
-- which by itself constitutes a token.  You do not need to
-- put spaces before and after these characters.

-- Two charactors of "(" ")" are meta-charactors of CafeOBJ
-- system, and should be used only for grouping
-- terms/expressions.  These charactors can not be used in
-- any kind of identifiers. 

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

-- ==========================================================
--> Proof score for righ zero property: 
-->                     (N:Nat + 0 = N)
-- ==========================================================
-- opening module PNAT+ to make use of all its contents
open PNAT+
--> declare that n stands for any Nat value
op n : -> Nat .

**> Proof of (n + 0 = n) by induction on n
**> base case of n = 0:
red 0 + 0 = 0 .
**> induction hypothesis:
eq n + 0 = n .
**> induction step proof for (s n):
red s n + 0 = s n .
**> QED {end of proof}
close
-- ==========================================================

-- "ops n : -> Nat ." is an operator declaration inside
-- "open" and "close", and the last "." is a must.  This is
-- different from an operator declaration inside module
-- definition.

-- "red 0 + 0 = 0 ." is a reduction command, and returns the
-- most simplified expression of "0 + 0 = 0" by using all
-- avairable equations of the module "PNAT+" as rewrite
-- rules from left to write.

-- ==========================================================
--> Proof score for associativity of (_ + _)
-->    (N1:Nat + N2:Nat) + N3:Nat = N1 +(N2 + N3)
-- ==========================================================

-- opening module PNAT+ to make use of all its contents
open PNAT+
--> declaring constants for arbitrary values
ops n1 n2 n3 : -> Nat .

**> Proof of associativity: 
**>    (n1 + n2) + n3 = n1 +(n2 + n3)
**> by induction on n1
**> base case proof for 0:
red 0 + (n2 + n3) = (0 + n2) + n3 .
**> induction hypothesis:
eq (n1 + n2) + n3 = n1 + (n2 + n3) .
**> induction step proof for (s n1):
red ((s n1) + n2) + n3 = (s n1) + (n2 + n3) .
**> QED {end of proof}
close
-- ==========================================================

-- ==========================================================
--> comments in CafeOBJ codes
-- ==========================================================

-- line starts with "-- " or "** " is a comment line

--> line starts with "--> " and "**> " are comment lines with
--> echo backs from CafeOBJ system.  That is, the system
--> print out these lines if this file is inputed into the
--> system.

-- Text not containing charactore " and enclosed with " and
-- " is a comment.

-- ==========================================================
--> parsing term with precedences and {r-assoc} attribute
-- ==========================================================

-- selecting PNAT
select PNAT
parse  s s 0 .
reduce s s 0 .
-- "parse s s 0 ." is a command to parse the term "s s 0"

open PNAT+
set verbose on

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

describe op (s _)
describe op (_ + _)
describe op (_ = _)
sh ops
sh op (s _)
sh op (_ + _)
sh op (_ = _)

set verbose off
close

-- It is better to put enough parentheses and make the term
-- structure clear!  Do not play with parsing with
-- precedences too much!

-- ==========================================================
-- Order sorted Peano style natural numbers 
-- and error handling
-- ==========================================================

--> Order sorted Peano style natural numbers 
mod! PNATord {
  [Zero NzNat < Nat]
  op 0 : -> Zero {constr} .
  -- successor
  op s_ : Zero -> NzNat {constr} .
  op s_ : Nat -> NzNat {constr} .

  -- predecessor
  op p_ : NzNat -> Nat .
  eq p s N:Nat = N .

  op _=_ : Nat Nat -> Bool {comm} .
  eq (N:Nat = N) = true .
  eq (0 = s(N2:Nat)) = false .
  eq (s(N1:Nat) = s(N2:Nat)) = (N1 = N2) .
}

-- "[Zero NzNat < Nat]" indicates that the sort "Zero" and
-- "NzNat" are included in the sort "Nat".

--> error handling with ordered sorts 
open PNATord 

-- (p 0) is a term of error sort
parse p 0 .  
red p 0 .

parse p s 0 .
red p s 0 = 0 .

parse p p s 0 .

red p p s 0 = 0 .
-- this reduction shows an example of
-- error handling with ordered sorts

close

-- ==========================================================
--> Difference of _=_ and _==_
-- ==========================================================

-- opening PNAT
open PNAT
parse 0 = s 0 .
red 0 = s 0 .

op n : -> Nat .
red n = n .
red 0 = n .
red 0 == n .
close

-- NAT is built-in module of natural numbers.  The module
-- NAT contains (1) sort Nat which is a set of infinite
-- natural numbers, and (2) ordinary fundamental operations
-- over Nat.

-- EQL is built-in meta-module for making predicate _=_
-- available.  Inspect EQL by the command:
sh EQL

mod! GOOD-POS{
pr(NAT + EQL)
pred positive : Nat
var N : Nat
eq positive(N) = not(N = 0) .
}

mod! BAD-POS{
pr(NAT + EQL)
pred positive : Nat 
var N : Nat 
eq positive(N) = not(N == 0) .
}

-- Proof scores for "positive(n) for all Nat n" 
-- (This is not true) .
open BAD-POS
op n : -> Nat .
red positive(n) .
close

-- Proof scores for "positive(n) for all Nat n"  
-- (This is not true) .
open GOOD-POS
op n : -> Nat .
red positive(n) .
close

-- Proof scores for "positive(n) if ((n = 0) = false)  
-- (This is true) .
open GOOD-POS
op n : -> Nat .
eq (n = 0) = false .
red positive(n) .
close

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