-- ==========================================================
--> Sample 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
  red rev1@(nil,`l2:List) .
close
--> II Induction case
open PRED-LISTrev .
-- arbitrary values
  op l1 : -> List .
-- induction hypothesis
  eq rev1(l1 @ `l2:List) = rev1(`l2) @ rev1(l1) .
-- check
  red rev1@(`e:Elt | l1,`l2:List) .
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
  red rev1rev1(nil) .
close
--> II Induction case
open PRED-LISTrev .
-- already proved lemma: rev1@(L1:List,L2:List) 
  eq rev1(L1:List @ L2:List) = rev1(L2) @ rev1(L1) .
-- arbitrary values
  op l : -> List .
-- induction hypothesis
  eq rev1(rev1(l)) = l .
-- check
  red rev1rev1(`e:Elt | l) .
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
  red sr2@(nil,`l2:List,`l3:List) .
close
--> II Induction case
open PRED-LISTrev .
-- arbitrary values
  op l1 : -> List .
-- induction hypothesis sr2@(l1,L2:List,L3:List) 
  eq sr2(l1,L2:List) @ L3:List = sr2(l1,L2 @ L3) .
-- check
  red sr2@(`e:Elt | l1,`l2:List,`l3:List) .
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
  red rev1=rev2(nil) .
close
--> II Induction case
open PRED-LISTrev .
-- already proved lemma: sr2@(L1:List,L2:List,L3:List)
eq (sr2(L1:List,L2:List) @ L3:List) = sr2(L1,L2 @ L3) .
-- arbitrary values
  op l : -> List .
-- induction hypothesis
eq rev1(l) = rev2(l) .
-- check
red rev1=rev2(`e:Elt | l) .
close
--> QED
-- ==========================================================

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