-- ========================================================== --> An example answer for exercise of lecture6 -- ========================================================== -- loading lecture6.cafe in lecture6 -- module with lem1 definition mod* COMPILER-LEMMA { pr(INTERPRETER) pr(VM) pr(COMPILER) -- lemma op lem1 : Exp CList Stack -> Bool eq lem1(E:Exp,L:CList,S:Stack) = (exec(compile(E) @ L,S) = exec(L,vm(compile(E)) | S)) . } -- ============================================================== --> Lemma (\forall E:Exp,L:CList,S:Stack) --> (exec(compile(E) @ L,S) = exec(L,vm(compile(E)) | S)) -- that is lem1(E:Exp,L:CList,S:Stack) -- ============================================================== --> Proof: By induction on the structure of E. --> I. Base case --> 0. m open COMPILER-LEMMA op m : -> Nat&Err . -- check red lem1(m,L:CList,S:Stack) . close --> II. Induction case --> 1. e1 ++ e2 open COMPILER-LEMMA -- arbitrary values ops e1 e2 : -> Exp . -- induction hypothesis var L : CList . var S : Stack . eq exec(compile(e1) @ L,S) = exec(L,vm(compile(e1)) | S) . eq exec(compile(e2) @ L,S) = exec(L,vm(compile(e2)) | S) . -- check red lem1(e1 ++ e2,L1:CList,S1:Stack) . close --> 2. e1 -- e2 open COMPILER-LEMMA -- arbitrary values ops e1 e2 : -> Exp . -- induction hypothesis var L : CList . var S : Stack . eq exec(compile(e1) @ L,S) = exec(L,vm(compile(e1)) | S) . eq exec(compile(e2) @ L,S) = exec(L,vm(compile(e2)) | S) . -- check red lem1(e1 -- e2,L1:CList,S1:Stack) . close --> 3. e1 ** e2 open COMPILER-LEMMA -- arbitrary values ops e1 e2 : -> Exp . -- induction hypothesis var L : CList . var S : Stack . eq exec(compile(e1) @ L,S) = exec(L,vm(compile(e1)) | S) . eq exec(compile(e2) @ L,S) = exec(L,vm(compile(e2)) | S) . -- check red lem1(e1 ** e2,L1:CList,S1:Stack) . close --> 4. e1 // e2 open COMPILER-LEMMA -- arbitrary values ops e1 e2 : -> Exp . -- induction hypothesis var L : CList . var S : Stack . eq exec(compile(e1) @ L,S) = exec(L,vm(compile(e1)) | S) . eq exec(compile(e2) @ L,S) = exec(L,vm(compile(e2)) | S) . -- check red lem1(e1 // e2,L1:CList,S1:Stack) . close -- -- QED -- -- ========================================================== --> end end end -- ==========================================================