Commit 65e7a75e by Ralf Jung

show that the langauge we have so far, is an instance (with no atomic expressions...)

parent 4d5ff4eb
 Require Import mathcomp.ssreflect.ssreflect. Require Import mathcomp.ssreflect.ssreflect. Require Import Autosubst.Autosubst. Require Import Autosubst.Autosubst. Require Import prelude.option. Require Import prelude.option iris.language. Set Bullet Behavior "Strict Subproofs". Set Bullet Behavior "Strict Subproofs". ... @@ -86,7 +86,7 @@ Qed. ... @@ -86,7 +86,7 @@ Qed. Section e2e. (* To get local tactics. *) Section e2e. (* To get local tactics. *) Lemma e2e e v: Lemma e2e e v: e2v e = Some v -> e = v2e v. e2v e = Some v -> v2e v = e. Proof. Proof. Ltac case0 := case =><-; simpl; eauto using f_equal, f_equal2. Ltac case0 := case =><-; simpl; eauto using f_equal, f_equal2. Ltac case1 e1 := destruct (e2v e1); simpl; [|discriminate]; Ltac case1 e1 := destruct (e2v e1); simpl; [|discriminate]; ... @@ -273,6 +273,13 @@ Proof. ... @@ -273,6 +273,13 @@ Proof. Qed. Qed. End step_by_value. End step_by_value. (** Atomic expressions *) Definition atomic (e: expr) := match e with | _ => False end. (** Tests, making sure that stuff works. *) Module Tests. Module Tests. Definition lit := Lit 21. Definition lit := Lit 21. Definition term := Op2 plus lit lit. Definition term := Op2 plus lit lit. ... @@ -282,3 +289,24 @@ Module Tests. ... @@ -282,3 +289,24 @@ Module Tests. apply Op2S. apply Op2S. Qed. Qed. End Tests. End Tests. (** Instantiate the Iris language interface. This closes reduction under evaluation contexts. We could potentially make this a generic construction. *) Section Language. Local Obligation Tactic := idtac. Definition ctx_step e1 σ1 e2 σ2 (ef: option expr) := exists K e1' e2', e1 = fill K e1' /\ e2 = fill K e2' /\ prim_step e1' σ1 e2' σ2 ef. Instance heap_lang : Language expr value state := Build_Language v2e e2v atomic ctx_step. Proof. - exact v2v. - exact e2e. - intros e1 σ1 e2 σ2 ef (K & e1' & e2' & He1 & He2 & Hstep). subst e1 e2. eapply fill_not_value. case Heq:(e2v e1') => [v1'|]; last done. exfalso. eapply values_stuck; last by (do 4 eexists; eassumption). erewrite fill_empty. eapply e2e. eassumption. - intros. contradiction. - intros. contradiction. Qed. End Language.
 ... @@ -14,6 +14,7 @@ Class Language (E V S : Type) := { ... @@ -14,6 +14,7 @@ Class Language (E V S : Type) := { prim_step e1 σ1 e2 σ2 ef → prim_step e1 σ1 e2 σ2 ef → is_Some (of_expr e2) is_Some (of_expr e2) }. }. Arguments Build_Language {_ _ _} _ _ _ _ {_ _ _ _ _}. Section Lang. Section Lang. Context `{Language E V St}. Context `{Language E V St}. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!