Proving a Property of Map in OBJ3
obj NAT is
sorts Nat Pos .
subsort Pos < Nat .
op 0 : -> Nat .
op 1 : -> Pos .
op s_ : Nat -> Pos .
eq 1 = s 0 .
op _<=_ : Nat Nat -> Bool .
vars M N : Nat .
eq M <= M = true .
eq s M <= 0 = false .
eq 0 <= M = true .
eq s M <= s N = M <= N .
endo
obj LIST[E :: TRIV] is
sorts List NeList .
subsort NeList < List .
op nil : -> List .
op cons : Elt List -> NeList .
op car_ : NeList -> Elt .
op cdr_: NeList -> List .
var E : Elt .
var L : List .
eq car cons(E,L) = E .
eq cdr cons(E,L) = L .
endo
obj NTH[E :: TRIV] is
protecting LIST[E] + NAT .
sort ErrElt .
subsort Elt < ErrElt .
op length_ : List -> Nat .
op nth : Pos List -> Elt .
op toolong : -> ErrElt .
var E : Elt .
var L : List .
eq length nil = 0 .
eq length cons(E,L) = s length L .
var P : Pos .
eq nth(P,nil) = toolong .
eq nth(s 0,cons(E,L)) = E .
eq nth(s P,cons(E,L)) = nth(P,L) .
endo
th FN is
sort Elt .
op f : Elt -> Elt .
endth
obj MAP[F :: FN] is
protecting NTH[F] .
op map_ : List -> List .
var E : Elt .
var L : List .
eq map nil = nil .
eq map cons(E,L) = cons(f(E),map L) .
endo
obj SETUPFN is
sort Elt .
op f : Elt -> Elt .
endo
obj SETUP is
extending MAP[SETUPFN] .
op e : -> Elt .
op l : -> List .
op p : -> Pos .
var P : Pos .
ceq nth(P,map l) = f(nth(P,l)) if P <= length l .
eq p <= length l = true .
endo
***> base case
reduce nth(1,map cons(e,nil)) == f(nth(1,cons(e,nil))) .
***> induction step, by case analysis on P: Pos
reduce nth(1,map cons(e,l)) == f(nth(1,cons(e,l))) .
reduce nth(s p,map cons(e,l)) == f(nth(s p,cons(e,l))) .
***> thus we can assert:
obj MAP-FACT[F :: FN] is
protecting MAP[F] .
var L : List .
var P : Pos .
ceq nth(P, map L) = f(nth(P,L)) if P <= length L .
endo