# 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)`

## 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 baseCafeOBJ> 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 stepLIST@(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 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`

## 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 stepLIST-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.