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

I. Base case

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

II. Induction case

rev(rev(e | l))
-> rev(rev(l) @ (e | nil)) by(r2)
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)

Lemma1 [p-r]

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

I. Base case

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

II. Induction case

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)

Lemma2 [p-@]

L @ nil = L

I. Base case

nil @ nil
-> nil by(@1)

II. Induction case

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

Proof scores in CafeOBJ

mod! LIST (X :: TRIV) {
[List]
op nil : -> List {constr} .
op _|_ : Elt List -> List {constr} .
}
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-@]

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]

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

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

Software engineer