Commit b8b1e8da by Lennard Gäher

parent 973b87c5
 ... ... @@ -64,6 +64,19 @@ theories/systemf_mu/parallel_subst.v theories/systemf_mu/logrel.v theories/systemf_mu/z_combinator.v # SystemF + Mu + State theories/systemf_mu_state/locations.v theories/systemf_mu_state/lang.v theories/systemf_mu_state/notation.v theories/systemf_mu_state/types.v #theories/systemf_mu_state/tactics.v #theories/systemf_mu/execution.v #theories/systemf_mu/parallel_subst.v #theories/systemf_mu/logrel.v #theories/systemf_mu/mutbit.v # By removing the # below, you can add the exercise sheets to make ... ...
 ... ... @@ -9,6 +9,16 @@ Proof. naive_solver. Qed. Lemma if_iff' P R S : (P → R ↔ S) → (P → R) ↔ (P → S). Proof. tauto. Qed. Lemma and_iff' (P R S : Prop) : (P → R ↔ S) → (P ∧ R) ↔ (P ∧ S). Proof. tauto. Qed. Lemma and_iff (P Q R S : Prop) : (P ↔ Q) → ((P ∨ Q) → R ↔ S) → (P ∧ R) ↔ (Q ∧ S). Proof. tauto. Qed. Lemma list_subseteq_cons {X} (A B : list X) x : A ⊆ B → x :: A ⊆ x :: B. Proof. intros Hincl. intros y. rewrite !elem_of_cons. naive_solver. Qed. Lemma list_subseteq_cons_binder A B x : A ⊆ B → x :b: A ⊆ x :b: B. ... ...
 ... ... @@ -169,6 +169,37 @@ Section map. intros i x. rewrite lookup_delete_Some. intros [ ]; done. Qed. Lemma insert_union_singleton_l (k : K) m x : <[ k := x ]> m = {[ k := x ]} ∪ m. Proof. apply insert_union_singleton_l. Qed. Lemma insert_union_singleton_r (k : K) m x : m !! k = None → <[ k := x ]> m = m ∪ {[ k := x ]}. Proof. apply insert_union_singleton_r. Qed. Lemma lookup_union_Some_l m1 m2 (k : K) x : m1 !! k = Some x → (m1 ∪ m2) !! k = Some x. Proof. apply lookup_union_Some_l. Qed. Lemma lookup_union_r m1 m2 (k : K) : m1 !! k = None → (m1 ∪ m2) !! k = m2 !! k. Proof. apply lookup_union_r. Qed. (** map disjoint *) Definition map_disjoint := @map_disjoint K (gmap K) _ A. Lemma map_disjoint_spec m1 m2 : m1 ##ₘ m2 ↔ ∀ i x y, m1 !! i = Some x → m2 !! i = Some y → False. Proof. apply map_disjoint_spec. Qed. Lemma map_disjoint_alt m1 m2 : m1 ##ₘ m2 ↔ ∀ i, m1 !! i = None ∨ m2 !! i = None. Proof. apply map_disjoint_alt. Qed. Lemma map_not_disjoint m1 m2 : ¬m1 ##ₘ m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2. Proof. apply map_not_disjoint. Qed. Global Instance map_disjoint_sym : Symmetric (map_disjoint). Proof. apply map_disjoint_sym. Qed. Lemma map_disjoint_empty_l m : ∅ ##ₘ m. Proof. apply map_disjoint_empty_l. Qed. Lemma map_disjoint_empty_r m : m ##ₘ ∅. Proof. apply map_disjoint_empty_r. Qed. (** Domain *) Definition dom := @base.dom (gmap K A) (gset K) _. ... ... @@ -206,4 +237,48 @@ Section map. Lemma dom_fmap f m : dom (f <\$> m) = dom m. Proof. apply dom_fmap_L. Qed. (** difference *) (* TODO: upstream? *) Lemma map_difference_mono m1 m2 m3 : m1 ⊆ m2 → m1 ∖ m3 ⊆ m2 ∖ m3. Proof. intros ?. apply map_subseteq_spec. intros i x. rewrite !lookup_difference_Some. intros [? ?]; split; [ | done]. by eapply map_subseteq_spec. Qed. (* Upstream? *) Lemma map_difference_union' m1 m2 m3 : m1 ##ₘ m2 → (m1 ∪ m2) ∖ m3 = (m1 ∖ m3) ∪ (m2 ∖ m3). Proof. intros Hdisj. apply map_eq. intros i. destruct (((m1 ∪ m2) ∖ m3) !! i) as [ s | ] eqn:Hlook. - apply lookup_difference_Some in Hlook as [Hlook1 Hlook2]. apply lookup_union_Some in Hlook1; [ | done]. symmetry. apply lookup_union_Some. { eapply map_disjoint_weaken; [ done | | ]; apply map_subseteq_difference_l; done. } destruct Hlook1 as [ Hlook1 | Hlook1]; [left | right]; apply lookup_difference_Some; done. - symmetry. apply lookup_difference_None in Hlook as [ Hlook | Hlook]. + apply lookup_union_None in Hlook as [ ? ?]. apply lookup_union_None; split; apply lookup_difference_None; eauto. + apply lookup_union_None; split; apply lookup_difference_None; eauto. Qed. (* TODO: upstream the first inclusion as a lemma? *) Lemma map_disjoint_difference m1 m2 : m1 ##ₘ m2 → m1 = m1 ∖ m2. Proof. intros Hdisj. apply (partial_order_anti_symm (R := (⊆))). - apply map_subseteq_spec. intros i x Hlook. apply lookup_difference_Some. split; [done | ]. by eapply map_disjoint_Some_l. - by apply map_subseteq_difference_l. Qed. End map. Infix "##ₘ" := map_disjoint (at level 70) : stdpp_scope. Global Hint Extern 0 (_ ##ₘ _) => symmetry; eassumption : core.
This diff is collapsed.
 From stdpp Require Import countable numbers gmap. Record loc := Loc { loc_car : Z }. Add Printing Constructor loc. Global Instance loc_eq_decision : EqDecision loc. Proof. solve_decision. Defined. Global Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}. Global Instance loc_countable : Countable loc. Proof. by apply (inj_countable' loc_car Loc); intros []. Defined. Global Program Instance loc_infinite : Infinite loc := inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _. Next Obligation. done. Qed. Definition loc_add (l : loc) (off : Z) : loc := {| loc_car := loc_car l + off|}. Notation "l +ₗ off" := (loc_add l off) (at level 50, left associativity) : stdpp_scope. Lemma loc_add_assoc l i j : l +ₗ i +ₗ j = l +ₗ (i + j). Proof. destruct l; unfold loc_add; simpl; f_equal; lia. Qed. Lemma loc_add_0 l : l +ₗ 0 = l. Proof. destruct l; unfold loc_add; simpl; f_equal; lia. Qed. Global Instance loc_add_inj l : Inj eq eq (loc_add l). Proof. destruct l; unfold Inj, loc_add; simpl; intros; simplify_eq; lia. Qed. Definition fresh_locs (ls : gset loc) : loc := {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r)%Z 1%Z ls |}. Lemma fresh_locs_fresh ls i : (0 ≤ i)%Z → fresh_locs ls +ₗ i ∉ ls. Proof. intros Hi. cut (∀ l, l ∈ ls → loc_car l < loc_car (fresh_locs ls) + i)%Z. { intros help Hf%help. simpl in *. lia. } apply (set_fold_ind_L (λ r ls, ∀ l, l ∈ ls → (loc_car l < r + i)%Z)); set_solver by eauto with lia. Qed. Global Opaque fresh_locs.
 From semantics.systemf_mu_state Require Export lang. Set Default Proof Using "Type". (** Coercions to make programs easier to type. *) Coercion of_val : val >-> expr. Coercion LitInt : Z >-> base_lit. Coercion LitBool : bool >-> base_lit. Coercion LitLoc : loc >-> base_lit. Coercion App : expr >-> Funclass. Coercion Var : string >-> expr. (** Define some derived forms. *) Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing). Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing). Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing). (* No scope for the values, does not conflict and scope is often not inferred properly. *) Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l"). Notation "# l" := (Lit l%Z%E%stdpp) (at level 8, format "# l") : expr_scope. (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come first. *) Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope. Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope. Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" := (Match e0 x1%binder e1 x2%binder e2) (e0, x1, e1, x2, e2 at level 200, format "'[hv' 'match:' e0 'with' '/ ' '[' 'InjL' x1 => '/ ' e1 ']' '/' '[' | 'InjR' x2 => '/ ' e2 ']' '/' 'end' ']'") : expr_scope. Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" := (Match e0 x2%binder e2 x1%binder e1) (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope. Notation "()" := LitUnit : val_scope. Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) : expr_scope. Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E) : expr_scope. Notation "e1 * e2" := (BinOp MultOp e1%E e2%E) : expr_scope. Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) : expr_scope. Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) : expr_scope. Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) : expr_scope. (*Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.*) Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E) (at level 200, e1, e2, e3 at level 200) : expr_scope. Notation "λ: x , e" := (Lam x%binder e%E) (at level 200, x at level 1, e at level 200, format "'[' 'λ:' x , '/ ' e ']'") : expr_scope. Notation "λ: x y .. z , e" := (Lam x%binder (Lam y%binder .. (Lam z%binder e%E) ..)) (at level 200, x, y, z at level 1, e at level 200, format "'[' 'λ:' x y .. z , '/ ' e ']'") : expr_scope. Notation "λ: x , e" := (LamV x%binder e%E) (at level 200, x at level 1, e at level 200, format "'[' 'λ:' x , '/ ' e ']'") : val_scope. Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. )) (at level 200, x, y, z at level 1, e at level 200, format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope. Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E) (at level 200, x at level 1, e1, e2 at level 200, format "'[' 'let:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope. Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E) (at level 100, e2 at level 200, format "'[' '[hv' '[' e1 ']' ;; ']' '/' e2 ']'") : expr_scope. Notation "'Λ' , e" := (TLam e%E) (at level 200, e at level 200, format "'[' 'Λ' , '/ ' e ']'") : expr_scope. Notation "'Λ' , e" := (TLamV e%E) (at level 200, e at level 200, format "'[' 'Λ' , '/ ' e ']'") : val_scope. (* the [e] always needs to be paranthesized, due to the level (chosen to make this cooperate with the [App] coercion) *) Notation "e '<>'" := (TApp e%E) (at level 10) : expr_scope. (*Check ((Λ, #4) <>)%E.*) (*Check (((λ: "x", "x") #5) <>)%E.*) Notation "'pack' e" := (Pack e%E) (at level 200, e at level 200) : expr_scope. Notation "'pack' v" := (PackV v%V) (at level 200, v at level 200) : val_scope. Notation "'unpack' e1 'as' x 'in' e2" := (Unpack x%binder e1%E e2%E) (at level 200, e1, e2 at level 200, x at level 1) : expr_scope. Notation "'roll' e" := (Roll e%E) (at level 200, e at level 200) : expr_scope. Notation "'roll' v" := (RollV v%E) (at level 200, v at level 200) : val_scope. Notation "'unroll' e" := (Unroll e%E) (at level 200, e at level 200) : expr_scope. Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope. Notation "'new' e" := (New e%E) (at level 10) : expr_scope. Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope. Definition assert (e : expr) : expr := if: e then #LitUnit else (#0 #0). Definition Or (e1 e2 : expr) : expr := if: e1 then #true else e2. Definition And (e1 e2 : expr) : expr := if: e1 then e2 else #false. Notation "e1 '||' e2" := (Or e1 e2) : expr_scope. Notation "e1 '&&' e2" := (And e1 e2) : expr_scope.
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!