Prove rev (rev L) = L in CafeOBJ

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

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

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

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.

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.

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-@)

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.

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.

What to show is nil @ nil = nil .

nil @ nil
-> nil by(@1)

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

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

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 baseCafeOBJ> 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)> closeCafeOBJ> 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

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.

Software engineer