Compare commits
5 Commits
ad5f832f96
...
02b9ce9abb
| Author | SHA1 | Date |
|---|---|---|
 Shad Amethyst
|
02b9ce9abb | 11 months ago |
|
Shad Amethyst
|
82042039b9 | 11 months ago |
Benjamin Peters
|
cd222f11c5 | 11 months ago |
|
Benjamin Peters
|
4f600972e5 | 11 months ago |
mueck
|
d9bd2ee560 | 11 months ago |
File diff suppressed because it is too large
Load Diff
@ -0,0 +1,46 @@
|
|||||||
|
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.
|
||||||
File diff suppressed because it is too large
Load Diff
@ -0,0 +1,113 @@
|
|||||||
|
From semantics.ts.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.
|
||||||
@ -0,0 +1,279 @@
|
|||||||
|
From stdpp Require Import prelude.
|
||||||
|
From iris Require Import prelude.
|
||||||
|
From semantics.lib Require Import facts.
|
||||||
|
From semantics.ts.systemf_mu_state Require Import lang.
|
||||||
|
From semantics.lib Require Import maps.
|
||||||
|
|
||||||
|
Fixpoint subst_map (xs : gmap string expr) (e : expr) : expr :=
|
||||||
|
match e with
|
||||||
|
| Lit l => Lit l
|
||||||
|
| Var y => match xs !! y with Some es => es | _ => Var y end
|
||||||
|
| App e1 e2 => App (subst_map xs e1) (subst_map xs e2)
|
||||||
|
| Lam x e => Lam x (subst_map (binder_delete x xs) e)
|
||||||
|
| UnOp op e => UnOp op (subst_map xs e)
|
||||||
|
| BinOp op e1 e2 => BinOp op (subst_map xs e1) (subst_map xs e2)
|
||||||
|
| If e0 e1 e2 => If (subst_map xs e0) (subst_map xs e1) (subst_map xs e2)
|
||||||
|
| TApp e => TApp (subst_map xs e)
|
||||||
|
| TLam e => TLam (subst_map xs e)
|
||||||
|
| Pack e => Pack (subst_map xs e)
|
||||||
|
| Unpack x e1 e2 => Unpack x (subst_map xs e1) (subst_map (binder_delete x xs) e2)
|
||||||
|
| Pair e1 e2 => Pair (subst_map xs e1) (subst_map xs e2)
|
||||||
|
| Fst e => Fst (subst_map xs e)
|
||||||
|
| Snd e => Snd (subst_map xs e)
|
||||||
|
| InjL e => InjL (subst_map xs e)
|
||||||
|
| InjR e => InjR (subst_map xs e)
|
||||||
|
| Case e e1 e2 => Case (subst_map xs e) (subst_map xs e1) (subst_map xs e2)
|
||||||
|
| Roll e => Roll (subst_map xs e)
|
||||||
|
| Unroll e => Unroll (subst_map xs e)
|
||||||
|
| Load e => Load (subst_map xs e)
|
||||||
|
| Store e1 e2 => Store (subst_map xs e1) (subst_map xs e2)
|
||||||
|
| New e => New (subst_map xs e)
|
||||||
|
end.
|
||||||
|
|
||||||
|
Lemma subst_map_empty e :
|
||||||
|
subst_map ∅ e = e.
|
||||||
|
Proof.
|
||||||
|
induction e; simpl; f_equal; eauto.
|
||||||
|
all: destruct x; simpl; [done | by rewrite !delete_empty..].
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma subst_map_is_closed X e xs :
|
||||||
|
is_closed X e →
|
||||||
|
(∀ x : string, x ∈ dom xs → x ∉ X) →
|
||||||
|
subst_map xs e = e.
|
||||||
|
Proof.
|
||||||
|
intros Hclosed Hd.
|
||||||
|
induction e in xs, X, Hd, Hclosed |-*; simpl in *;try done.
|
||||||
|
all: repeat match goal with
|
||||||
|
| H : Is_true (_ && _) |- _ => apply andb_True in H as [ ? ? ]
|
||||||
|
end.
|
||||||
|
{ (* Var *)
|
||||||
|
apply bool_decide_spec in Hclosed.
|
||||||
|
assert (xs !! x = None) as ->; last done.
|
||||||
|
destruct (xs !! x) as [s | ] eqn:Helem; last done.
|
||||||
|
exfalso; eapply Hd; last apply Hclosed.
|
||||||
|
apply elem_of_dom; eauto.
|
||||||
|
}
|
||||||
|
{ (* lambdas *)
|
||||||
|
erewrite IHe; [done | done |].
|
||||||
|
intros y. destruct x as [ | x]; first apply Hd.
|
||||||
|
simpl.
|
||||||
|
rewrite dom_delete elem_of_difference not_elem_of_singleton.
|
||||||
|
intros [Hnx%Hd Hneq]. rewrite elem_of_cons. intros [? | ?]; done.
|
||||||
|
}
|
||||||
|
8: { (* Unpack *)
|
||||||
|
erewrite IHe1; [ | done | done].
|
||||||
|
erewrite IHe2; [ done | done | ].
|
||||||
|
intros y. destruct x as [ | x]; first apply Hd.
|
||||||
|
simpl.
|
||||||
|
rewrite dom_delete elem_of_difference not_elem_of_singleton.
|
||||||
|
intros [Hnx%Hd Hneq]. rewrite elem_of_cons. intros [? | ?]; done.
|
||||||
|
}
|
||||||
|
(* all other cases *)
|
||||||
|
all: repeat match goal with
|
||||||
|
| H : ∀ _ _, _ → _ → subst_map _ _ = _ |- _ => erewrite H; clear H
|
||||||
|
end; done.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma subst_map_subst map x (e e' : expr) :
|
||||||
|
is_closed [] e' →
|
||||||
|
subst_map map (subst x e' e) = subst_map (<[x:=e']>map) e.
|
||||||
|
Proof.
|
||||||
|
intros He'.
|
||||||
|
revert x map; induction e; intros xx map; simpl;
|
||||||
|
try (f_equal; eauto).
|
||||||
|
- case_decide.
|
||||||
|
+ simplify_eq/=. rewrite lookup_insert.
|
||||||
|
rewrite (subst_map_is_closed []); [done | apply He' | ].
|
||||||
|
intros ? ?. apply not_elem_of_nil.
|
||||||
|
+ rewrite lookup_insert_ne; done.
|
||||||
|
- destruct x; simpl; first done.
|
||||||
|
+ case_decide.
|
||||||
|
* simplify_eq/=. by rewrite delete_insert_delete.
|
||||||
|
* rewrite delete_insert_ne; last by congruence. done.
|
||||||
|
- destruct x; simpl; first done.
|
||||||
|
+ case_decide.
|
||||||
|
* simplify_eq/=. by rewrite delete_insert_delete.
|
||||||
|
* rewrite delete_insert_ne; last by congruence. done.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Definition subst_is_closed (X : list string) (map : gmap string expr) :=
|
||||||
|
∀ x e, map !! x = Some e → closed X e.
|
||||||
|
Lemma subst_is_closed_subseteq X map1 map2 :
|
||||||
|
map1 ⊆ map2 → subst_is_closed X map2 → subst_is_closed X map1.
|
||||||
|
Proof.
|
||||||
|
intros Hsub Hclosed2 x e Hl. eapply Hclosed2, map_subseteq_spec; done.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma subst_subst_map x es map e :
|
||||||
|
subst_is_closed [] map →
|
||||||
|
subst x es (subst_map (delete x map) e) =
|
||||||
|
subst_map (<[x:=es]>map) e.
|
||||||
|
Proof.
|
||||||
|
revert map es x; induction e; intros map v0 xx Hclosed; simpl;
|
||||||
|
try (f_equal; eauto).
|
||||||
|
- destruct (decide (xx=x)) as [->|Hne].
|
||||||
|
+ rewrite lookup_delete // lookup_insert //. simpl.
|
||||||
|
rewrite decide_True //.
|
||||||
|
+ rewrite lookup_delete_ne // lookup_insert_ne //.
|
||||||
|
destruct (_ !! x) as [rr|] eqn:Helem.
|
||||||
|
* apply Hclosed in Helem.
|
||||||
|
by apply subst_is_closed_nil.
|
||||||
|
* simpl. rewrite decide_False //.
|
||||||
|
- destruct x; simpl; first by auto.
|
||||||
|
case_decide.
|
||||||
|
+ simplify_eq. rewrite delete_idemp delete_insert_delete. done.
|
||||||
|
+ rewrite delete_insert_ne //; last congruence. rewrite delete_commute. apply IHe.
|
||||||
|
eapply subst_is_closed_subseteq; last done.
|
||||||
|
apply map_delete_subseteq.
|
||||||
|
- destruct x; simpl; first by auto.
|
||||||
|
case_decide.
|
||||||
|
+ simplify_eq. rewrite delete_idemp delete_insert_delete. done.
|
||||||
|
+ rewrite delete_insert_ne //; last congruence. rewrite delete_commute. apply IHe2.
|
||||||
|
eapply subst_is_closed_subseteq; last done.
|
||||||
|
apply map_delete_subseteq.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma subst'_subst_map b (es : expr) map e :
|
||||||
|
subst_is_closed [] map →
|
||||||
|
subst' b es (subst_map (binder_delete b map) e) =
|
||||||
|
subst_map (binder_insert b es map) e.
|
||||||
|
Proof.
|
||||||
|
destruct b; first done.
|
||||||
|
apply subst_subst_map.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma closed_subst_weaken e map X Y :
|
||||||
|
subst_is_closed [] map →
|
||||||
|
(∀ x, x ∈ X → x ∉ dom map → x ∈ Y) →
|
||||||
|
closed X e →
|
||||||
|
closed Y (subst_map map e).
|
||||||
|
Proof.
|
||||||
|
induction e in X, Y, map |-*; rewrite /closed; simpl; intros Hmclosed Hsub Hcl; first done.
|
||||||
|
all: repeat match goal with
|
||||||
|
| H : Is_true (_ && _) |- _ => apply andb_True in H as [ ? ? ]
|
||||||
|
end.
|
||||||
|
{ (* vars *)
|
||||||
|
destruct (map !! x) as [es | ] eqn:Heq.
|
||||||
|
+ apply is_closed_weaken_nil. by eapply Hmclosed.
|
||||||
|
+ apply bool_decide_pack. apply Hsub; first by eapply bool_decide_unpack.
|
||||||
|
by apply not_elem_of_dom.
|
||||||
|
}
|
||||||
|
{ (* lambdas *)
|
||||||
|
eapply IHe; last done.
|
||||||
|
+ eapply subst_is_closed_subseteq; last done.
|
||||||
|
destruct x; first done. apply map_delete_subseteq.
|
||||||
|
+ intros y. destruct x as [ | x]; first by apply Hsub.
|
||||||
|
rewrite !elem_of_cons. intros [-> | Hy] Hn; first by left.
|
||||||
|
destruct (decide (y = x)) as [ -> | Hneq]; first by left.
|
||||||
|
right. eapply Hsub; first done. set_solver.
|
||||||
|
}
|
||||||
|
8: { (* unpack *)
|
||||||
|
apply andb_True; split; first naive_solver.
|
||||||
|
eapply IHe2; last done.
|
||||||
|
+ eapply subst_is_closed_subseteq; last done.
|
||||||
|
destruct x; first done. apply map_delete_subseteq.
|
||||||
|
+ intros y. destruct x as [ | x]; first by apply Hsub.
|
||||||
|
rewrite !elem_of_cons. intros [-> | Hy] Hn; first by left.
|
||||||
|
destruct (decide (y = x)) as [ -> | Hneq]; first by left.
|
||||||
|
right. eapply Hsub; first done. set_solver.
|
||||||
|
}
|
||||||
|
(* all other cases *)
|
||||||
|
all: repeat match goal with
|
||||||
|
| |- Is_true (_ && _) => apply andb_True; split
|
||||||
|
end.
|
||||||
|
all: naive_solver.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma subst_is_closed_weaken X1 X2 θ :
|
||||||
|
subst_is_closed X1 θ →
|
||||||
|
X1 ⊆ X2 →
|
||||||
|
subst_is_closed X2 θ.
|
||||||
|
Proof.
|
||||||
|
intros Hcl Hincl x e Hlook.
|
||||||
|
eapply is_closed_weaken; last done.
|
||||||
|
by eapply Hcl.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma subst_is_closed_weaken_nil X θ :
|
||||||
|
subst_is_closed [] θ →
|
||||||
|
subst_is_closed X θ.
|
||||||
|
Proof.
|
||||||
|
intros; eapply subst_is_closed_weaken; first done.
|
||||||
|
apply list_subseteq_nil.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma subst_is_closed_insert X e f θ :
|
||||||
|
is_closed X e →
|
||||||
|
subst_is_closed X (delete f θ) →
|
||||||
|
subst_is_closed X (<[f := e]> θ).
|
||||||
|
Proof.
|
||||||
|
intros Hcl Hcl' x e'.
|
||||||
|
destruct (decide (x = f)) as [<- | ?].
|
||||||
|
- rewrite lookup_insert. intros [= <-]. done.
|
||||||
|
- rewrite lookup_insert_ne; last done.
|
||||||
|
intros Hlook. eapply Hcl'.
|
||||||
|
rewrite lookup_delete_ne; done.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
(* NOTE: this is a simplified version of the tactic in tactics.v which
|
||||||
|
suffice for this proof *)
|
||||||
|
Ltac simplify_closed :=
|
||||||
|
repeat match goal with
|
||||||
|
| |- closed _ _ => unfold closed; simpl
|
||||||
|
| |- Is_true (_ && _) => simpl; rewrite !andb_True; split_and!
|
||||||
|
| H : closed _ _ |- _ => unfold closed in H; simpl in H
|
||||||
|
| H: Is_true (_ && _) |- _ => simpl in H; apply andb_True in H
|
||||||
|
| H : _ ∧ _ |- _ => destruct H
|
||||||
|
end.
|
||||||
|
|
||||||
|
Lemma is_closed_subst_map X θ e :
|
||||||
|
subst_is_closed X θ →
|
||||||
|
closed (X ++ elements (dom θ)) e →
|
||||||
|
closed X (subst_map θ e).
|
||||||
|
Proof.
|
||||||
|
induction e in X, θ |-*; eauto.
|
||||||
|
all: try solve [intros; simplify_closed; naive_solver].
|
||||||
|
- unfold subst_map.
|
||||||
|
destruct (θ !! x) eqn:Heq.
|
||||||
|
+ intros Hcl _. eapply Hcl; done.
|
||||||
|
+ intros _ Hcl.
|
||||||
|
apply closed_is_closed in Hcl.
|
||||||
|
apply bool_decide_eq_true in Hcl.
|
||||||
|
apply elem_of_app in Hcl.
|
||||||
|
destruct Hcl as [ | H].
|
||||||
|
* apply closed_is_closed. by apply bool_decide_eq_true.
|
||||||
|
* apply elem_of_elements in H.
|
||||||
|
by apply not_elem_of_dom in Heq.
|
||||||
|
- intros. simplify_closed.
|
||||||
|
eapply IHe.
|
||||||
|
+ destruct x as [ | x]; simpl; first done.
|
||||||
|
intros y e'. rewrite lookup_delete_Some. intros (? & Hlook%H).
|
||||||
|
eapply is_closed_weaken; first done.
|
||||||
|
by apply list_subseteq_cons_r.
|
||||||
|
+ eapply is_closed_weaken; first done.
|
||||||
|
simpl. destruct x as [ | x]; first done; simpl.
|
||||||
|
apply list_subseteq_cons_l.
|
||||||
|
apply stdpp.sets.elem_of_subseteq.
|
||||||
|
intros y; simpl. rewrite elem_of_cons !elem_of_app.
|
||||||
|
intros [ | Helem]; first naive_solver.
|
||||||
|
destruct (decide (x = y)) as [<- | Hneq]; first naive_solver.
|
||||||
|
right. right. apply elem_of_elements. rewrite dom_delete elem_of_difference elem_of_singleton.
|
||||||
|
apply elem_of_elements in Helem; done.
|
||||||
|
- intros. simplify_closed. { naive_solver. }
|
||||||
|
(* same proof as for lambda *)
|
||||||
|
eapply IHe2.
|
||||||
|
+ destruct x as [ | x]; simpl; first done.
|
||||||
|
intros y e'. rewrite lookup_delete_Some. intros (? & Hlook%H).
|
||||||
|
eapply is_closed_weaken; first done.
|
||||||
|
by apply list_subseteq_cons_r.
|
||||||
|
+ eapply is_closed_weaken; first done.
|
||||||
|
simpl. destruct x as [ | x]; first done; simpl.
|
||||||
|
apply list_subseteq_cons_l.
|
||||||
|
apply stdpp.sets.elem_of_subseteq.
|
||||||
|
intros y; simpl. rewrite elem_of_cons !elem_of_app.
|
||||||
|
intros [ | Helem]; first naive_solver.
|
||||||
|
destruct (decide (x = y)) as [<- | Hneq]; first naive_solver.
|
||||||
|
right. right. apply elem_of_elements. rewrite dom_delete elem_of_difference elem_of_singleton.
|
||||||
|
apply elem_of_elements in Helem; done.
|
||||||
|
Qed.
|
||||||
@ -0,0 +1,91 @@
|
|||||||
|
From stdpp Require Import gmap base relations.
|
||||||
|
From iris Require Import prelude.
|
||||||
|
From semantics.lib Require Export facts maps sets.
|
||||||
|
From semantics.ts.systemf_mu_state Require Export lang notation parallel_subst types.
|
||||||
|
|
||||||
|
Ltac map_solver :=
|
||||||
|
repeat match goal with
|
||||||
|
| |- (⤉ _) !! _ = Some _ =>
|
||||||
|
rewrite fmap_insert
|
||||||
|
| |- <[ ?p := _ ]> _ !! ?p = Some _ =>
|
||||||
|
apply lookup_insert
|
||||||
|
| |- <[ _ := _ ]> _ !! _ = Some _ =>
|
||||||
|
rewrite lookup_insert_ne; [ | congruence]
|
||||||
|
end.
|
||||||
|
|
||||||
|
Ltac solve_typing_step := idtac.
|
||||||
|
Ltac solve_typing :=
|
||||||
|
intros;
|
||||||
|
repeat (asimpl; solve_typing_step).
|
||||||
|
Ltac solve_typing_fast :=
|
||||||
|
intros;
|
||||||
|
repeat (solve_typing_step).
|
||||||
|
Ltac solve_typing_step ::=
|
||||||
|
match goal with
|
||||||
|
| |- TY _; _ ; _ ⊢ ?e : ?A => first [eassumption | econstructor]
|
||||||
|
(* heuristic to solve tapp goals where we need to pick the right type for the substitution *)
|
||||||
|
| |- TY _ ; _ ; _ ⊢ ?e <> : ?A => eapply typed_tapp'; [solve_typing | | asimpl; reflexivity]
|
||||||
|
| |- TY _ ; _ ; _ ⊢ Unroll ?e : ?A => eapply typed_unroll'; [solve_typing | asimpl; reflexivity]
|
||||||
|
| |- bin_op_typed _ _ _ _ => econstructor
|
||||||
|
| |- un_op_typed _ _ _ _ => econstructor
|
||||||
|
| |- type_wf _ ?e => assert_fails (is_evar e); eassumption
|
||||||
|
| |- type_wf _ ?e => assert_fails (is_evar e); econstructor
|
||||||
|
| |- type_wf _ (subst _ ?A) => eapply type_wf_subst; [ | intros; simpl]
|
||||||
|
| |- type_wf _ ?e => assert_fails (is_evar e); eapply type_wf_mono; [eassumption | lia]
|
||||||
|
(* conditions spawned by the tyvar case of [type_wf] *)
|
||||||
|
| |- _ < _ => simpl; lia
|
||||||
|
(* conditions spawned by the variable case *)
|
||||||
|
| |- _ !! _ = Some _ => map_solver
|
||||||
|
end.
|
||||||
|
|
||||||
|
Tactic Notation "unify_type" uconstr(A) :=
|
||||||
|
match goal with
|
||||||
|
| |- TY ?Σ; ?n; ?Γ ⊢ ?e : ?B => unify A B
|
||||||
|
end.
|
||||||
|
Tactic Notation "replace_type" uconstr(A) :=
|
||||||
|
match goal with
|
||||||
|
| |- TY ?Σ; ?n; ?Γ ⊢ ?e : ?B => replace B%ty with A%ty; cycle -1; first try by asimpl
|
||||||
|
end.
|
||||||
|
|
||||||
|
|
||||||
|
Ltac simplify_list_elem :=
|
||||||
|
simpl;
|
||||||
|
repeat match goal with
|
||||||
|
| |- ?x ∈ ?y :: ?l => apply elem_of_cons; first [left; reflexivity | right]
|
||||||
|
| |- _ ∉ [] => apply not_elem_of_nil
|
||||||
|
| |- _ ∉ _ :: _ => apply not_elem_of_cons; split
|
||||||
|
end; try fast_done.
|
||||||
|
Ltac simplify_list_subseteq :=
|
||||||
|
simpl;
|
||||||
|
repeat match goal with
|
||||||
|
| |- ?x :: _ ⊆ ?x :: _ => apply list_subseteq_cons_l
|
||||||
|
| |- ?x :: _ ⊆ _ => apply list_subseteq_cons_elem; first solve [simplify_list_elem]
|
||||||
|
| |- elements _ ⊆ elements _ => apply elements_subseteq; set_solver
|
||||||
|
| |- [] ⊆ _ => apply list_subseteq_nil
|
||||||
|
| |- ?x :b: _ ⊆ ?x :b: _ => apply list_subseteq_cons_binder
|
||||||
|
(* NOTE: this might make the goal unprovable *)
|
||||||
|
(*| |- elements _ ⊆ _ :: _ => apply list_subseteq_cons_r*)
|
||||||
|
end;
|
||||||
|
try fast_done.
|
||||||
|
|
||||||
|
(* Try to solve [is_closed] goals using a number of heuristics (that shouldn't make the goal unprovable) *)
|
||||||
|
Ltac simplify_closed :=
|
||||||
|
simpl; intros;
|
||||||
|
repeat match goal with
|
||||||
|
| |- closed _ _ => unfold closed; simpl
|
||||||
|
| |- Is_true (is_closed [] _) => first [assumption | done]
|
||||||
|
| |- Is_true (is_closed _ (lang.subst _ _ _)) => rewrite subst_is_closed_nil; last solve[simplify_closed]
|
||||||
|
| |- Is_true (is_closed ?X ?v) => assert_fails (is_evar X); eapply is_closed_weaken
|
||||||
|
| |- Is_true (is_closed _ _) => eassumption
|
||||||
|
| |- Is_true (_ && true) => rewrite andb_true_r
|
||||||
|
| |- Is_true (true && _) => rewrite andb_true_l
|
||||||
|
| |- Is_true (?a && ?a) => rewrite andb_diag
|
||||||
|
| |- Is_true (_ && _) => simpl; rewrite !andb_True; split_and!
|
||||||
|
| |- _ ⊆ ?A => match type of A with | list _ => simplify_list_subseteq end
|
||||||
|
| |- _ ∈ ?A => match type of A with | list _ => simplify_list_elem end
|
||||||
|
| |- _ ≠ _ => congruence
|
||||||
|
| H : closed _ _ |- _ => unfold closed in H; simpl in H
|
||||||
|
| H: Is_true (_ && _) |- _ => simpl in H; apply andb_True in H
|
||||||
|
| H : _ ∧ _ |- _ => destruct H
|
||||||
|
| |- Is_true (bool_decide (_ ∈ _)) => apply bool_decide_pack; set_solver
|
||||||
|
end; try fast_done.
|
||||||
File diff suppressed because it is too large
Load Diff
Loading…
Reference in new issue