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

Love podcasts or audiobooks? Learn on the go with our new app.

Recommended from Medium

Basics of Computer Vision - Part 1

How we use Convolutional Neural Networks to estimate the layout of a room

Multi-Class Classification? Yes.

Designing a Deep Learning App

Tackling common Neural Network problems

Brief Introduction of Reinforcement Learning (1)

Using Optuna to Optimize PyTorch Hyperparameters

Generative Adversarial Networks

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Takanori Ishibashi

Takanori Ishibashi

Software engineer

More from Medium

Clean Code in SIPASCA

The Evolution of the programming language

Visual Studio Code, The Ninja Way

6 common website bugs and their fixes