commit
3b3c8c67e7
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
@ -0,0 +1,97 @@
|
|||||||
|
From semantics.ts.systemf_mu 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 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.
|
||||||
@ -0,0 +1,275 @@
|
|||||||
|
From stdpp Require Import prelude.
|
||||||
|
From iris Require Import prelude.
|
||||||
|
From semantics.lib Require Import facts maps.
|
||||||
|
From semantics.ts.systemf_mu Require Import lang.
|
||||||
|
|
||||||
|
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)
|
||||||
|
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,84 @@
|
|||||||
|
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 Require Export lang notation 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 :=
|
||||||
|
intros;
|
||||||
|
repeat 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] *)
|
||||||
|
| |- _ < _ => 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
@ -0,0 +1,80 @@
|
|||||||
|
From stdpp Require Import gmap base relations tactics.
|
||||||
|
From iris Require Import prelude.
|
||||||
|
From semantics.ts.systemf_mu Require Import lang notation types pure tactics.
|
||||||
|
From Autosubst Require Import Autosubst.
|
||||||
|
|
||||||
|
(** * Encoding of the untyped lambda calculus *)
|
||||||
|
|
||||||
|
Definition D := (μ: #0 → #0)%ty.
|
||||||
|
|
||||||
|
Definition lame (x : string) (e : expr) : val := RollV (λ: x, e).
|
||||||
|
Definition appe (e1 e2 : expr) : expr := (unroll e1) e2.
|
||||||
|
|
||||||
|
Lemma lame_typed n Γ x e :
|
||||||
|
TY n; (<[x := D]> Γ) ⊢ e : D →
|
||||||
|
TY n; Γ ⊢ lame x e : D.
|
||||||
|
Proof. solve_typing. Qed.
|
||||||
|
|
||||||
|
Lemma app_typed n Γ e1 e2 :
|
||||||
|
TY n; Γ ⊢ e1 : D →
|
||||||
|
TY n; Γ ⊢ e2 : D →
|
||||||
|
TY n; Γ ⊢ appe e1 e2 : D.
|
||||||
|
Proof.
|
||||||
|
solve_typing.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma appe_step_l e1 e1' (v : val) :
|
||||||
|
contextual_step e1 e1' →
|
||||||
|
contextual_step (appe e1 v) (appe e1' v).
|
||||||
|
Proof.
|
||||||
|
intros Hstep. unfold appe.
|
||||||
|
by eapply (fill_contextual_step [UnrollCtx; AppLCtx _]).
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma appe_step_r e1 e2 e2' :
|
||||||
|
contextual_step e2 e2' →
|
||||||
|
contextual_step (appe e1 e2) (appe e1 e2').
|
||||||
|
Proof.
|
||||||
|
intros Hstep. unfold appe.
|
||||||
|
by eapply (fill_contextual_step [AppRCtx _]).
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma lame_step_beta x e (v : val) :
|
||||||
|
rtc contextual_step (appe (lame x e) v) (lang.subst x v e).
|
||||||
|
Proof.
|
||||||
|
unfold appe, lame.
|
||||||
|
econstructor 2.
|
||||||
|
{ eapply (fill_contextual_step [AppLCtx _]).
|
||||||
|
eapply base_contextual_step. by econstructor.
|
||||||
|
}
|
||||||
|
econstructor 2.
|
||||||
|
{ eapply base_contextual_step. econstructor; eauto. }
|
||||||
|
reflexivity.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
(* Divergence *)
|
||||||
|
Definition ω : expr :=
|
||||||
|
roll (λ: "x", (unroll "x") "x").
|
||||||
|
|
||||||
|
Definition Ω := ((unroll ω) ω)%E.
|
||||||
|
|
||||||
|
Lemma Ω_loops:
|
||||||
|
tc contextual_step Ω Ω.
|
||||||
|
Proof.
|
||||||
|
econstructor 2; [|econstructor 1].
|
||||||
|
- rewrite /Ω /ω. eauto.
|
||||||
|
- rewrite /Ω. eauto.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma ω_typed :
|
||||||
|
TY 0; ∅ ⊢ ω : D.
|
||||||
|
Proof.
|
||||||
|
solve_typing.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma Ω_typed : TY 0; ∅ ⊢ Ω : D.
|
||||||
|
Proof.
|
||||||
|
rewrite /Ω. econstructor.
|
||||||
|
- eapply typed_unroll'; eauto using ω_typed.
|
||||||
|
- eapply ω_typed.
|
||||||
|
Qed.
|
||||||
Loading…
Reference in new issue