-- ========================================================== --> An example answer for exercise of lecture02 --> Proof scores for verifications of properties of --> \forall L:List.(rev1(L) = rev2(L)) --> \forall L:List.(rev1(rev1(L)) = L) . --> and others about generic list. -- ========================================================== --> elements with equality predicate mod* TRIV= { [Elt] op _=_ : Elt Elt -> Bool {comm} . eq (E:Elt = E) = true . } --> parametrized list mod! LIST(X :: TRIV=) { [List] op nil : -> List {constr} . op _|_ : Elt.X List -> List {constr} . -- -- variables declaration vars L L1 L2 : List . vars E1 E2 : Elt . -- equality on the sort List op _=_ : List List -> Bool {comm} . eq (L = L) = true . eq (nil = (E2 | L2)) = false . eq ((E1 | L1) = (E2 | L2)) = (E1 =.X E2) and (L1 = L2) . } --> append _@_ over List mod! LIST@(X :: TRIV=) { pr(LIST(X)) -- append operation over List op _@_ : List List -> List . var E : Elt . vars L1 L2 : List . eq [@1]: nil @ L2 = L2 . eq [@2]: (E | L1) @ L2 = E | (L1 @ L2) . } --> predicates about _@_ mod PRED-LIST@(X :: TRIV=) { pr(LIST@(X)) -- CafeOBJ variables vars L1 L2 L3 : List . -- nil is right identity of _@_ pred @ri : List . eq @ri(L1) = ((L1 @ nil) = L1) . -- _@_ is associative pred @assoc : List List List . eq @assoc(L1,L2,L3) = ((L1 @ L2) @ L3 = L1 @ (L2 @ L3)) . } -- ========================================================== --> Property of PRED-LIST@ --> \forall L1:List.((L1 @ nil) = L1) --> (i.e. @ri(L:Nat) = true) -- Proof: By induction on L1. -- I. Base case. open PRED-LIST@ -- check red @ri(nil) . close -- II Induction case open PRED-LIST@ -- arbitrary values op e : -> Elt.X . op l1 : -> List . -- check red @ri(l1) implies @ri(e | l1) . close -- --> QED -- ========================================================== -- ========================================================== --> Property of PRED-LIST@ --> \forall L1,L2,L3:List. --> ((L1 @ L2) @ L3 = L1 @ (L2 @ L3)) --> (i.e. @assoc(L1:List,L2:List,L3:List) = true) -- Proof: By induction on L1. -- I Base case open PRED-LIST@ -- arbitrary values ops l2 l3 : -> List . -- check red @assoc(nil,l2,l3) . close -- II Induction case open PRED-LIST@ -- arbitrary values op e : -> Elt.X . ops l1 l2 l3 : -> List . -- check red @assoc(l1,l2,l3) implies @assoc(e | l1,l2,l3) . close -- --> QED -- ========================================================== --> LIST with associative append _@_ mod! LIST@a(X :: TRIV=) { pr(LIST(X)) -- notice that associativity {assoc} -- and right identity [@3] is already proved op _@_ : List List -> List {assoc} . vars L1 L2 : List var E : Elt.X eq [@1]: nil @ L2 = L2 . eq [@2]: (E | L1) @ L2 = E | (L1 @ L2) . eq [@3]: L1 @ nil = L1 . } --> LIST with reverse operations mod! LISTrev(X :: TRIV=) { pr(LIST@a(X)) vars L L1 L2 : List var E : Elt.X -- one argument reverse operation op rev1 : List -> List . eq rev1(nil) = nil . eq rev1(E | L) = rev1(L) @ (E | nil) . -- two arguments reverse operation op rev2 : List -> List . -- auxiliary function for rev2 op sr2 : List List -> List . eq rev2(L) = sr2(L,nil) . eq sr2(nil,L2) = L2 . eq sr2(E | L1,L2) = sr2(L1,E | L2) . } --> predicates about LISTrev mod PRED-LISTrev(X :: TRIV=) { pr(LISTrev(X)) -- CafeOBJ variables vars L L1 L2 L3 : List -- rev1 distributes over _@_ reversely pred rev1@ : List List . eq rev1@(L1,L2) = (rev1(L1 @ L2) = rev1(L2) @ rev1(L1)) . -- rev1rev1 is identity function pred rev1rev1 : List . eq rev1rev1(L) = (rev1(rev1(L)) = L) . -- sr2 with _@_ pred sr2@ : List List List . eq sr2@(L1,L2,L3) = (sr2(L1,L2) @ L3 = sr2(L1,L2 @ L3)) . -- left hand of _=_ is better to be canonical -- rev1=rev2 pred rev1=rev2 : List . eq rev1=rev2(L) = (rev1(L) = rev2(L)) . } -- ========================================================== --> Property of PRED-LISTrev --> \forall L1,L2:List. --> (rev1(L1 @ L2) = rev1(L2) @ rev1(L1)) -- (i.e. rev1(L1:List,L2:List) = true) -- Proof: By induction on L1. -- I Base case open PRED-LISTrev -- arbitrary values op l2 : -> List . -- check red rev1@(nil,l2) . close -- II Induction case open PRED-LISTrev -- arbitrary values op e : -> Elt.X . ops l1 l2 : -> List . -- induction hypothesis eq rev1(l1 @ L2:List) = rev1(L2) @ rev1(l1) . -- check red rev1@(e | l1,l2) . close -- --> QED -- ========================================================== -- ========================================================== --> Property of PRED-LISTrev --> \forall L:List.(rev1(rev1(L)) = L) . --> (i.e. rev1rev1(L:List) = true) -- Proof: By induction on L. -- I Base case open PRED-LISTrev -- check red rev1rev1(nil) . close -- II Induction case -- either (1) or (2) works -- (1) open PRED-LISTrev -- arbitrary values op e : -> Elt.X . op l : -> List . -- assumption -- rev1@(L1:List,L2:List) is already proved eq rev1(L1:List @ L2:List) = rev1(L2) @ rev1(L1) . -- induction hypothesis eq rev1(rev1(l)) = l . -- check red rev1rev1(e | l) . close -- (2) open PRED-LISTrev op e : -> Elt.X . op l : -> List . -- induction hypothesis eq rev1(rev1(l)) = l . -- check -- notice that rev1@(rev1(l),(e | nil)) is -- an instance of rev1@(L1:List,L2:List) red rev1@(rev1(l),(e | nil)) implies rev1rev1(e | l) . close -- --> QED -- ========================================================== -- ========================================================== --> Property of PRED-LISTrev --> \forall L:List.(sr2(L1,L2) @ L3 = sr2(L1,L2 @ L3)) --> (i.e. sr2@(L1:List,L2:List,L3:List) = true) -- Proof: By induction on L1. -- I Base case open PRED-LISTrev -- arbitrary values ops l2 l3 : -> List . -- check red sr2@(nil,l2,l3) . close -- II Induction case -- either (1) or (2) works -- (1) open PRED-LISTrev -- arbitrary values op e : -> Elt.X . ops l1 l2 l3 : -> List . -- induction hypothesis sr2@(l1,L2:List,L3:List) eq sr2(l1,L2:List) @ L3:List = sr2(l1,L2 @ L3) . -- check red sr2@(e | l1,l2,l3) . close -- (2) open PRED-LISTrev -- arbitrary values op e : -> Elt.X . ops l1 l2 l3 : -> List . -- check -- notice that sr2@(l1,e | l2,l3) is -- an instance of IH: sr2@(l1,L2:List,L3:List) red sr2@(l1,e | l2,l3) implies sr2@(e | l1,l2,l3) . close -- --> QED -- ========================================================== -- ========================================================== --> Property of PRED-LISTrev --> \forall L:List.(rev1(L) = rev2(L)) --> (i.e. rev1=rev2(L:List) = true) -- Proof: By induction on L. --> I Base case open PRED-LISTrev -- check red rev1=rev2(nil) . close --> II Induction case --> ~(rev1(l)=sr2(l,nil)) open PRED-LISTrev -- arbitrary values op e : -> Elt.X . op l : -> List . -- assumptions eq (rev1(l) = sr2(l,nil)) = false . -- check red rev1=rev2(l) implies rev1=rev2(e | l) . close -- either (1) or (2) works --> (1) (rev1(l)=sr2(l,nil)) open PRED-LISTrev -- arbitrary values op e : -> Elt.X . op l : -> List . -- assumptions eq rev1(l) = sr2(l,nil) . -- check red (rev1=rev2(l) and sr2@(l,nil,e | nil)) implies rev1=rev2(e | l) . close --> (2) (rev1(l)=sr2(l,nil)) open PRED-LISTrev -- arbitrary values op e : -> Elt.X . op l : -> List . -- assumptions eq rev1(l) = sr2(l,nil) . -- sr2@(L1:List,L2:List,L3:List) is alreaday proved eq sr2(L1:List,L2:List) @ L3:List = sr2(L1,L2 @ L3) . -- check red rev1=rev2(l) implies rev1=rev2(e | l) . close -- --> QED -- ========================================================== -- ========================================================== --> end end end -- ==========================================================