{"action":"created","issue":{"url":"https://api.github.com/repos/snu-sf/pl2015/issues/101","labels_url":"https://api.github.com/repos/snu-sf/pl2015/issues/101/labels{/name}","comments_url":"https://api.github.com/repos/snu-sf/pl2015/issues/101/comments","events_url":"https://api.github.com/repos/snu-sf/pl2015/issues/101/events","html_url":"https://github.com/snu-sf/pl2015/issues/101","id":76963798,"number":101,"title":"About the definition of s_execute","user":{"login":"jaewooklee93","id":11328376,"avatar_url":"https://avatars.githubusercontent.com/u/11328376?v=3","gravatar_id":"","url":"https://api.github.com/users/jaewooklee93","html_url":"https://github.com/jaewooklee93","followers_url":"https://api.github.com/users/jaewooklee93/followers","following_url":"https://api.github.com/users/jaewooklee93/following{/other_user}","gists_url":"https://api.github.com/users/jaewooklee93/gists{/gist_id}","starred_url":"https://api.github.com/users/jaewooklee93/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jaewooklee93/subscriptions","organizations_url":"https://api.github.com/users/jaewooklee93/orgs","repos_url":"https://api.github.com/users/jaewooklee93/repos","events_url":"https://api.github.com/users/jaewooklee93/events{/privacy}","received_events_url":"https://api.github.com/users/jaewooklee93/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":6,"created_at":"2015-05-16T06:43:03Z","updated_at":"2015-05-20T15:01:57Z","closed_at":null,"body":"In our ```Assignment08_05.v```, we have to prove the correctness of stack compiler\r\n\r\n```Coq\r\n(* Assignment08_05.v *)\r\n\r\n(** **** Exercise: 3 stars, advanced (stack_compiler_correct)  *)\r\n(** The task of this exercise is to prove the correctness of the\r\n    compiler implemented in the previous exercise.  Remember that\r\n    the specification left unspecified what to do when encountering an\r\n    [SPlus], [SMinus], or [SMult] instruction if the stack contains\r\n    less than two elements.  (In order to make your correctness proof\r\n    easier you may find it useful to go back and change your\r\n    implementation!)\r\n\r\n    Prove the following theorem, stating that the [compile] function\r\n    behaves correctly.  You will need to start by stating a more\r\n    general lemma to get a usable induction hypothesis; the main\r\n    theorem will then be a simple corollary of this lemma. *)\r\nTheorem s_compile_correct : forall (st : state) (e : aexp),\r\n  s_execute st [] (s_compile e) = [ aeval st e ].\r\nProof.\r\n```\r\n\r\nHowever, I think the definition of ```s_execute``` given in the ```Assignment08_00.v``` is inappropriate to make the proof of correctness easier;\r\n\r\n```Coq\r\n(* Assignment08_00.v *)\r\n\r\nFixpoint s_execute (st : state) (stack : list nat)\r\n                   (prog : list sinstr)\r\n                 : list nat :=\r\n  match prog with\r\n  | [] => stack\r\n  | ins :: prog' => \r\n    match ins with\r\n    | SPush n => s_execute st (n :: stack) prog'\r\n    | SLoad x => s_execute st (st x :: stack) prog'\r\n    | SPlus => \r\n      match stack with\r\n      | na :: nb :: stack' => s_execute st (nb+na :: stack') prog'\r\n      | _ => []\r\n      end\r\n```\r\n\r\nbecause of the behavior at the error state. The definition you gave forces to stop the computation when invalid operations come in, but my desirable definition just ignores such invalid ops and keep going from the next ops.\r\n\r\nBecause of such slight difference at the error state, I cannot prove the following useful and intuitive ```Lemma``` with your definition, which is easily provable in my definition.\r\n**execute (l1++l2) on stack = execute l2 on (execute l1 on stack)**\r\nThis lemma doesn't hold with your definition, the counterexample is **l1=[SMult], l2=[SPush 0], stack=[]**\r\n\r\nSo I want to modify your definition in ```Assignment08_00.v```, but I think it is not allowed, but is there any possible way to alleviate this conflict between two def'ns?"},"comment":{"url":"https://api.github.com/repos/snu-sf/pl2015/issues/comments/103919338","html_url":"https://github.com/snu-sf/pl2015/issues/101#issuecomment-103919338","issue_url":"https://api.github.com/repos/snu-sf/pl2015/issues/101","id":103919338,"user":{"login":"jeehoonkang","id":1201316,"avatar_url":"https://avatars.githubusercontent.com/u/1201316?v=3","gravatar_id":"","url":"https://api.github.com/users/jeehoonkang","html_url":"https://github.com/jeehoonkang","followers_url":"https://api.github.com/users/jeehoonkang/followers","following_url":"https://api.github.com/users/jeehoonkang/following{/other_user}","gists_url":"https://api.github.com/users/jeehoonkang/gists{/gist_id}","starred_url":"https://api.github.com/users/jeehoonkang/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jeehoonkang/subscriptions","organizations_url":"https://api.github.com/users/jeehoonkang/orgs","repos_url":"https://api.github.com/users/jeehoonkang/repos","events_url":"https://api.github.com/users/jeehoonkang/events{/privacy}","received_events_url":"https://api.github.com/users/jeehoonkang/received_events","type":"User","site_admin":false},"created_at":"2015-05-20T15:01:56Z","updated_at":"2015-05-20T15:01:56Z","body":"@jaewooklee93 I believe that is because your proof did not rely on the altered part of the definition. It is the most pleasure thing that your proof is stripped down to 5 lines.\r\n\r\nJeehoon"}}