-- ==========================================================
--> An example answer for exercise of lecture02 
-->  Proof scores for verifications of properties of
-->      \forall L:List.(rev1(L) = rev2(L)) 
-->      \forall L:List.(rev1(rev1(L)) = L) .
-->  and others about generic list.
-- ==========================================================

--> elements with equality predicate
mod* TRIV= {
  [Elt]
  op _=_ : Elt Elt -> Bool {comm} .
  eq (E:Elt = E) = true .
}

--> parametrized list 
mod! LIST(X :: TRIV=) {
  [List]
  op nil : -> List {constr} .
  op _|_ : Elt.X List -> List {constr} .
  --
  
  -- variables declaration
  vars L L1 L2 : List .
  vars E1 E2 : Elt .
  -- equality on the sort List
  op _=_ : List List -> Bool {comm} .
  eq (L = L) = true .
  eq (nil = (E2 | L2)) = false .
  eq ((E1 | L1) = (E2 | L2))
      = (E1 =.X E2) and (L1 = L2) .
}

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

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

  -- CafeOBJ variables
  vars L1 L2 L3 : List .

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

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

-- ==========================================================
--> Property of PRED-LIST@
-->      \forall 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 e : -> Elt.X .
  op l1 : -> List .
-- check
  red @ri(l1) implies @ri(e | l1) .
close
--
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-LIST@ 
-->      \forall 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@
-- arbitrary values
  ops l2 l3 : -> List .
-- check
  red @assoc(nil,l2,l3) .
close
-- II Induction case
open PRED-LIST@
-- arbitrary values
  op e : -> Elt.X .
  ops l1 l2 l3 : -> List .
-- check
  red @assoc(l1,l2,l3) implies @assoc(e | l1,l2,l3) .
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} .
  vars L1 L2 : List
  var E : Elt.X
  eq [@1]: nil @ L2 = L2 .
  eq [@2]: (E | L1) @ L2 = E | (L1 @ L2) .
  eq [@3]: L1 @ nil = L1 .
}

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

  vars L L1 L2 : List
  var E : Elt.X

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

  -- two arguments reverse operation
  op rev2 : List -> List .
  -- auxiliary function for rev2
  op sr2 : List List -> List .
  eq rev2(L) = sr2(L,nil) .
  eq sr2(nil,L2) = L2 .
  eq sr2(E | L1,L2) = sr2(L1,E | L2) .
}

--> predicates about LISTrev
mod PRED-LISTrev(X :: TRIV=) {
  pr(LISTrev(X))

  -- CafeOBJ variables
  vars L L1 L2 L3 : List

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

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

  -- sr2 with _@_ 
  pred sr2@ : List List List .
  eq sr2@(L1,L2,L3)
     = (sr2(L1,L2) @ L3 = sr2(L1,L2 @ L3)) .
        -- left hand of _=_ is better to be canonical

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

-- ==========================================================
--> Property of PRED-LISTrev
-->      \forall 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
-- arbitrary values
  op l2 : -> List .
-- check
  red rev1@(nil,l2) .
close
-- II Induction case
open PRED-LISTrev
-- arbitrary values
  op e : -> Elt.X .
  ops l1 l2 : -> List .
-- induction hypothesis
  eq rev1(l1 @ L2:List) = rev1(L2) @ rev1(l1) .
-- check
  red rev1@(e | l1,l2) .
close
--
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-LISTrev
-->    \forall L:List.(rev1(rev1(L)) = L) .
-->    (i.e. rev1rev1(L:List) = true)
-- Proof: By induction on L.
-- I Base case
open PRED-LISTrev
-- check
  red rev1rev1(nil) .
close
-- II Induction case
-- either (1) or (2) works
-- (1)
open PRED-LISTrev
-- arbitrary values
  op e : -> Elt.X .
  op l : -> List .
-- assumption
  -- rev1@(L1:List,L2:List) is already proved
  eq rev1(L1:List @ L2:List) = rev1(L2) @ rev1(L1) .
-- induction hypothesis
  eq rev1(rev1(l)) = l .
-- check
  red rev1rev1(e | l) .
close
-- (2)
open PRED-LISTrev
  op e : -> Elt.X .
  op l : -> List .
-- induction hypothesis
  eq rev1(rev1(l)) = l .
-- check
  -- notice that rev1@(rev1(l),(e | nil)) is 
  -- an instance of rev1@(L1:List,L2:List)
  red rev1@(rev1(l),(e | nil)) implies rev1rev1(e | l) .
close
--
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-LISTrev
-->    \forall 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
-- arbitrary values
  ops l2 l3 : -> List .
-- check
  red sr2@(nil,l2,l3) .
close
-- II Induction case
-- either (1) or (2) works
-- (1)
open PRED-LISTrev
-- arbitrary values
  op e : -> Elt.X .
  ops l1 l2 l3 : -> List .
-- induction hypothesis sr2@(l1,L2:List,L3:List) 
  eq sr2(l1,L2:List) @ L3:List = sr2(l1,L2 @ L3) .
-- check
  red sr2@(e | l1,l2,l3) .
close
-- (2)
open PRED-LISTrev
-- arbitrary values
  op e : -> Elt.X .
  ops l1 l2 l3 : -> List .
-- check
  -- notice that sr2@(l1,e | l2,l3) is 
  -- an instance of IH: sr2@(l1,L2:List,L3:List) 
  red sr2@(l1,e | l2,l3) implies sr2@(e | l1,l2,l3) .
close
--
--> QED
-- ==========================================================

-- ==========================================================
--> Property of PRED-LISTrev
-->        \forall 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
  red rev1=rev2(nil) .
close
--> II Induction case
--> ~(rev1(l)=sr2(l,nil))
open PRED-LISTrev
-- arbitrary values
  op e : -> Elt.X .
  op l : -> List .
-- assumptions
  eq (rev1(l) = sr2(l,nil)) = false .
-- check
  red rev1=rev2(l) implies rev1=rev2(e | l) .
close
-- either (1) or (2) works
--> (1) (rev1(l)=sr2(l,nil)) 
open PRED-LISTrev
-- arbitrary values
  op e : -> Elt.X .
  op l : -> List .
-- assumptions
  eq rev1(l) = sr2(l,nil) .
-- check
  red (rev1=rev2(l) and sr2@(l,nil,e | nil)) 
                    implies rev1=rev2(e | l) .
close
--> (2) (rev1(l)=sr2(l,nil)) 
open PRED-LISTrev
-- arbitrary values
  op e : -> Elt.X .
  op l : -> List .
-- assumptions
  eq rev1(l) = sr2(l,nil) .
  -- sr2@(L1:List,L2:List,L3:List) is alreaday proved
  eq sr2(L1:List,L2:List) @ L3:List = sr2(L1,L2 @ L3) .
-- check
  red rev1=rev2(l) implies rev1=rev2(e | l) .
close
--
--> QED
-- ==========================================================

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