Prove rev (rev L) = L in CafeOBJ

Photo by Sebastian Schuppik on Unsplash

Let R@ be {(@1),(@2),(r1),(r2)} such that
    nil @ L2 = L2                   (@1)
    (E | L1) @ L2 = E | (L1 @ L2)   (@2)
    rev(nil) = nil                  (r1)
    rev(E | L) = rev(L) @ (E | nil) (r2)

Theorem1

rev(rev(L)) = L

Proof of Theorem1 by structural induction on L.
Let e be a fresh constant of Elt.E , l be a fresh constant of List.

I. Base case

What to show is rev(rev(nil)) = nil .

rev(rev(nil))
-> rev(nil)  by(r1)
-> nil       by(r1)

II. Induction case

What to show is rev(rev(e | l)) = e | l.
assuming the induction hypothesis
rev(rev(l) = l -- (1H)

rev(rev(e | l))
-> rev(rev(l) @ (e | nil))  by(r2)

Both rev(rev(l) @ (e | nil)) and e | l cannot be rewritten any more, and then we need a lemma. One possible candidate is as follows:
rev(rev(l) @ (e | nil)) = rev(e | nil) @ rev(rev(l))
However, this seems too specific. Therefore, we make it more generic:
rev(L1 @ L2) = rev(L2) @ rev(L1) -- (p-r)

rev(rev(e | l))
-> rev(rev(l) @ (e | nil))             by(r2)
-> rev(e | nil) @ rev(rev(l))          by(p-r)
-> rev(nil) @ (e | nil) @ rev(rev(l))  by(r2)
-> nil @ (e | nil) @ rev(rev(l))       by(r1)
-> (e | nil) @ rev(rev(l))             by(@1)
-> (e | nil) @ l                       by(1H)
-> e | (nil | l)                       by(@2)
-> e | l                               by(@1)

End of Proof of Theorem1.

Lemma1 [p-r]

rev(L1 @ L2) = rev(L2) @ rev(L1)

Proof of Lemma1 by structural induction on L1, L2.
Let e be a fresh constant of Elt.E , l1 , l2 be fresh constants of List.

I. Base case

What to show is rev(nil @ l1) = rev(l1) @ rev(nil) .

rev(nil @ l1)
-> rev(l1)  by (@1)
rev(l1) @ rev(nil)
-> rev(l1) @ nil  by(r1)

Both rev(l1) and rev(l1) @ nil cannot be rewritten any more, and then we need a lemma.
One possible candidate is as follows:
rev(l1) @ nil = rev(l1)
However, this seems too specific. Therefore, we make it more generic:
L @ nil = L -- (p-@)

rev(l1) @ rev(nil)
-> rev(l1) @ nil  by(r1) 
-> rev(l1)        by(p-@)

II. Induction case

What to show is rev(e | l1) @ l2 = rev(l2) @ rev(e | l1) .
assuming the induction hypothesis
rev(l1 @ l2) = rev(l2) @ rev(l1) -- (1H)

rev((e | l1) @ l2)
-> rev(e | (l1 @ l2))             by(@2)
-> rev(l1 @ l2) @ (e | nil)       by(r2)
-> rev(l2) @ rev(l1) @ (e | nil)  by(1H)
rev(l2) @ rev(e | l1)
-> rev(l2) @ rev(l1) @ (e | nil)  by(r2)

End of Proof of Lemma1.

Lemma2 [p-@]

L @ nil = L

Proof of Lemma2 by structural induction on L.
Let e be a fresh constant of Elt.E , l be fresh constants of List.

I. Base case

What to show is nil @ nil = nil .

nil @ nil
-> nil  by(@1)

II. Induction case

What to show is (e | l) @ nil = e | l .
assuming the induction hypothesis
(l @ nil) = l -- (1H)

(e | l) @ nil
-> e | (l @ nil)  by(@2)
-> e | l          by(1H)

End of Proof of Lemma2.

Proof scores in CafeOBJ

I use CafeOBJ 1.5.7 in this blog post. List is defined in CafeOBJ as follows:

mod! LIST (X :: TRIV) {
  [List]
  op nil : -> List {constr} .
  op _|_ : Elt List -> List {constr} .
}

Concatenation of list is defined as follows:

mod! LIST@ (X :: TRIV) {
  pr(LIST(X))
  op _@_ : List List -> List .
  eq nil @ L2:List = L2 .
  eq (E:Elt | L1:List) @ L2:List = E | (L1 @ L2) .
}

Lemma1 [p-@]

Proof of L @ nil = L by structural induction on L.

CafeOBJ> --> induction base
--> induction base
CafeOBJ> select LIST@ .
LIST@(X)> red (nil @ nil) = nil .
-- reduce in LIST@(X) : ((nil @ nil) = nil):Bool
(true):Bool
(0.0000 sec for parse, 0.0010 sec for 2 rewrites + 2 matches)
LIST@(X)> --> induction step
--> induction step
LIST@(X)> open LIST@ .
-- opening module LIST@(X) done.
%LIST@(X)> --> induction hypothesis
--> induction hypothesis
%LIST@(X)> op l : -> List .
%LIST@(X)> (l @ nil) = 1 .
%LIST@(X)> op e : -> Elt .
%LIST@(X)> red (e | l) @ nil = (e | l) .
-- reduce in %LIST@(X) : (((e | l) @ nil) = (e | l)):Bool
(true):Bool
(0.0000 sec for parse, 0.0000 sec for 3 rewrites + 5 matches)
%LIST@(X)> close

Lemma1 [p-r]

Concatenation of list is redefined as follow:

mod! LIST@ (X :: TRIV) {
  pr(LIST(X))
  op _@_ : List List -> List .
  eq nil @ L2:List = L2 .
  eq (E:Elt | L1:List) @ L2:List = E | (L1 @ L2) .
  -- Add p-@ 
  eq L1:List @ nil = L1 . 
}

Reverse of list is defined as follows:

mod! LIST-REV(X :: TRIV) {
  pr(LIST@(X))
  op rev : List -> List .
  eq rev(nil) = nil .
  eq rev(E:Elt | L:List) = rev(L) @ (E | nil) .
}

Proof of rev(L1 @ L2) = rev(L2) @ rev(L1) by structural induction on L1 and L2.

CafeOBJ> --> induction base
--> induction base
CafeOBJ> open LIST-REV .
-- opening module LIST-REV(X) done.
%LIST-REV(X)> op l2 : -> List .
%LIST-REV(X)> red rev(nil @ l2) = rev(l2) @ rev(nil) .
-- reduce in %LIST-REV(X) : (rev((nil @ l2)) = (rev(l2) @ rev(nil))):Bool
(true):Bool
(0.0000 sec for parse, 0.0000 sec for 4 rewrites + 12 matches)
%LIST-REV(X)> close
CafeOBJ> open LIST-REV .
-- opening module LIST-REV(X) done.
%LIST-REV(X)> --> induction hypothesis
--> induction hypothesis
%LIST-REV(X)> op l1 : -> List .
%LIST-REV(X)> eq rev(l1 @ L2:List) = rev(L2) @ rev(l1) .
%LIST-REV(X)> op e : -> Elt .
%LIST-REV(X)> op l2 : -> List .
%LIST-REV(X)> red rev((e | l1) @ l2) = rev(l2) @ rev(e | l1) .
-- reduce in %LIST-REV(X) : (rev(((e | l1) @ l2)) = (rev(l2) @ rev((e | l1)))):Bool
(((rev(l2) @ rev(l1)) @ (e | nil)) = (rev(l2) @ (rev(l1) @ (e | nil)))):Bool
(0.0000 sec for parse, 0.0000 sec for 4 rewrites + 41 matches)
%LIST-REV(X)> close

Theorem1

Reverse of list is redefined as follow:

mod! LIST-REV(X :: TRIV) {
  pr(LIST@(X))
  op rev : List -> List .
  eq rev(nil) = nil .
  eq rev(E:Elt | L:List) = rev(L) @ (E | nil) .
  -- Add p-r
  eq rev(L1:List @ L2:List) = rev(L2) @ rev(L1) .
}

Proof of rev(rev(L) = L by structural induction on L.

LIST-REV(X)> --> induction base
--> induction base 
LIST-REV(X)> select LIST-REV .
LIST-REV(X)> red rev(rev(nil)) = nil .
-- reduce in LIST-REV(X) : (rev(rev(nil)) = nil):Bool
(true):Bool
(0.0010 sec for parse, 0.0000 sec for 3 rewrites + 3 matches)
LIST-REV(X)> --> inducton step
--> inducton step
LIST-REV(X)> open LIST-REV .
-- opening module LIST-REV(X) done.
%LIST-REV(X)> --> induction hypothesis
--> induction hypothesis 
%LIST-REV(X)> op l : -> List .
%LIST-REV(X)> eq rev(rev(l)) = l .
%LIST-REV(X)> op e : -> Elt .
%LIST-REV(X)> red rev(rev(e | l)) = (e | l) .
-- reduce in %LIST-REV(X) : (rev(rev((e | l))) = (e | l)):Bool
(true):Bool
(0.0000 sec for parse, 0.0000 sec for 9 rewrites + 29 matches)
%LIST-REV(X)> close

Thanks for reading this blog post. You can connect with me on Twitter.