Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix object member lookup #14

Merged
merged 2 commits into from
Feb 2, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
67 changes: 53 additions & 14 deletions theories/Dot/dotsyn.v
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
From stdpp Require Import numbers.
From stdpp Require Import numbers strings.
From D Require Export prelude tactics.

Definition label := nat.
Definition label := string.

Inductive tm : Type :=
| tv : vl -> tm
Expand All @@ -12,7 +12,7 @@ Inductive tm : Type :=
| var_vl : var -> vl
| vnat : nat -> vl
| vabs : tm -> vl
| vobj : (list dm) -> vl
| vobj : list (label * dm) -> vl
with dm : Type :=
| dtysyn : ty -> dm
| dtysem : (list vl) -> positive -> dm
Expand All @@ -35,13 +35,33 @@ Inductive tm : Type :=
| TNat : ty.

Definition vls := list vl.
Definition dms := list dm.
Definition dms := list (label * dm).
Definition ctx := list ty.

Implicit Types
(T: ty) (v: vl) (t e: tm) (d: dm) (ds: dms) (vs: vls)
(Γ : ctx).

Definition label_of_ty (T: ty): option label :=
match T with
| TTMem l _ _ => Some l
| TVMem l _ => Some l
| _ => None
end.

Fixpoint dms_lookup (l : label) (ds : dms): option dm :=
match ds with
| [] => None
| (l', d) :: ds =>
match (decide (l = l')) with
| left Heq => Some d
| right _ => dms_lookup l ds
end
end.

Definition dms_has ds l d := dms_lookup l ds = Some d.
Definition dms_hasnt ds l := dms_lookup l ds = None.

(* Module Coq_IndPrinciples_Bad. *)
(* Scheme tm_bad_mut_ind := Induction for tm Sort Prop *)
(* with vl_bad_mut_ind := Induction for vl Sort Prop *)
Expand Down Expand Up @@ -79,7 +99,7 @@ Section syntax_mut_rect.
Variable step_vabs: ∀ t, Ptm t → Pvl (vabs t).
(* Original: *)
(* Variable step_vobj: ∀ l, Pvl (vobj l). *)
Variable step_vobj: ∀ ds, ForallT Pdm ds → Pvl (vobj ds).
Variable step_vobj: ∀ ds, ForallT Pdm (map snd ds) → Pvl (vobj ds).
Variable step_dtysyn: ∀ T, Pty T → Pdm (dtysyn T).
(* Original: *)
(* Variable step_dtysem: ∀ vsl g, Pdm (dtysem vs g). *)
Expand Down Expand Up @@ -118,7 +138,8 @@ Section syntax_mut_rect.
| Hstep: context [?P (?c _)] |- ?P (?c _) => apply Hstep; trivial
| Hstep: context [?P (?c)] |- ?P (?c) => apply Hstep; trivial
end.
all: elim: l => [|x xs IHxs] //=; auto.
- elim: l => [|[l d] ds IHds] //=; auto.
- elim: l => [|v vs IHxs] //=; auto.
Qed.

Lemma syntax_mut_rect: (∀ t, Ptm t) * (∀ v, Pvl v) * (∀ d, Pdm d) * (∀ p, Ppt p) * (∀ T, Pty T).
Expand Down Expand Up @@ -148,7 +169,7 @@ Section syntax_mut_ind.
Variable step_vabs: ∀ t, Ptm t → Pvl (vabs t).
(* Original: *)
(* Variable step_vobj: ∀ l, Pvl (vobj l). *)
Variable step_vobj: ∀ ds, Forall Pdm ds → Pvl (vobj ds).
Variable step_vobj: ∀ ds, Forall Pdm (map snd ds) → Pvl (vobj ds).
Variable step_dtysyn: ∀ T, Pty T → Pdm (dtysyn T).
(* Original: *)
(* Variable step_dtysem: ∀ vsl g, Pdm (dtysem vs g). *)
Expand Down Expand Up @@ -196,8 +217,12 @@ Instance Ids_vls : Ids vls := _.
Instance Ids_dms : Ids dms := _.
Instance Ids_ctx : Ids ctx := _.

Definition mapsnd {A} `(f: B → C) : A * B → A * C := λ '(a, b), (a, f b).

Instance list_rename `{Rename X} : Rename (list X) :=
λ sb xs, map (rename sb) xs.
Instance list_pair_rename {A} `{Rename X}: Rename (list (A * X)) :=
λ sb xs, map (mapsnd (rename sb)) xs.

Fixpoint tm_rename (sb : var → var) (e : tm) {struct e} : tm :=
let a := tm_rename : Rename tm in
Expand Down Expand Up @@ -262,17 +287,19 @@ Instance Rename_dm : Rename dm := dm_rename.
Instance Rename_pth : Rename path := path_rename.

Definition list_rename_fold `{Rename X} (sb : var → var) (xs : list X) : map (rename sb) xs = rename sb xs := eq_refl.
Definition list_pair_rename_fold {A} `{Rename X} sb (xs: list (A * X)): map (mapsnd (rename sb)) xs = rename sb xs := eq_refl.

Definition vls_rename_fold: ∀ sb vs, map (rename sb) vs = rename sb vs := list_rename_fold.
Definition dms_rename_fold: ∀ sb ds, map (rename sb) ds = rename sb ds := list_rename_fold.
Definition ctx_rename_fold: ∀ sb Γ, map (rename sb) Γ = rename sb Γ := list_rename_fold.
Definition dms_rename_fold: ∀ sb ds, map (mapsnd (rename sb)) ds = rename sb ds := list_pair_rename_fold.

Hint Rewrite @list_rename_fold : autosubst.
Hint Rewrite @list_rename_fold @list_pair_rename_fold : autosubst.

Instance vls_hsubst `{Subst vl} : HSubst vl vls :=
λ (sb : var → vl) (vs : vls), map (subst sb) vs.

Instance list_hsubst `{HSubst vl X}: HSubst vl (list X) := λ sb xs, map (hsubst sb) xs.
Instance list_pair_hsubst {A} `{HSubst vl X}: HSubst vl (list (A * X)) := λ sb xs, map (mapsnd (hsubst sb)) xs.

Fixpoint tm_hsubst (sb : var → vl) (e : tm) : tm :=
let a := tm_hsubst : HSubst vl tm in
Expand Down Expand Up @@ -345,11 +372,13 @@ Hint Mode HSubst - + : typeclass_instances.

Definition vls_subst_fold (sb : var → vl) (vs : vls) : map (subst sb) vs = hsubst sb vs := eq_refl.
Definition list_hsubst_fold `{HSubst vl X} sb (xs : list X) : map (hsubst sb) xs = hsubst sb xs := eq_refl.
Definition list_pair_hsubst_fold {A} `{HSubst vl X} sb (xs : list (A * X)) : map (mapsnd (hsubst sb)) xs = hsubst sb xs := eq_refl.

Hint Rewrite vls_subst_fold @list_hsubst_fold : autosubst.
Hint Rewrite vls_subst_fold @list_hsubst_fold @list_pair_hsubst_fold : autosubst.

Arguments vls_hsubst /.
Arguments list_hsubst /.
Arguments list_pair_hsubst /.

Lemma vl_eq_dec (v1 v2 : vl) : Decision (v1 = v2)
with
Expand All @@ -362,9 +391,10 @@ with
path_eq_dec (pth1 pth2 : path) : Decision (pth1 = pth2).
Proof.
all: rewrite /Decision; decide equality;
try (apply vl_eq_dec || apply tm_eq_dec || apply ty_eq_dec || apply path_eq_dec ||
try repeat (apply vl_eq_dec || apply tm_eq_dec || apply ty_eq_dec || apply path_eq_dec ||
apply @prod_eq_dec ||
apply @list_eq_dec ||
apply nat_eq_dec || apply positive_eq_dec); auto.
apply nat_eq_dec || apply positive_eq_dec || apply string_eq_dec); auto.
Qed.

Instance vl_eq_dec' : EqDecision vl := vl_eq_dec.
Expand All @@ -376,7 +406,7 @@ Instance vls_eq_dec' : EqDecision vls := list_eq_dec.
Instance dms_eq_dec' : EqDecision dms := list_eq_dec.

Local Ltac finish_lists l x :=
elim: l => [|x xs IHds] //=; by f_equal.
elim: l => [|x xs IHds] //=; idtac + elim: x => [l d] //=; f_equal => //; by f_equal.

Lemma vl_rename_Lemma (ξ : var → var) (v : vl) : rename ξ v = v.[ren ξ]
with
Expand Down Expand Up @@ -493,9 +523,15 @@ Proof.
induction s; asimpl; by f_equal.
Qed.

Instance HSubstLemmas_dms : HSubstLemmas vl dms := _.
Instance HSubstLemmas_ctx : HSubstLemmas vl ctx := _.

Instance HSubstLemmas_list_pair {A} `{Ids X} `{HSubst vl X} {hsl: HSubstLemmas vl X}: HSubstLemmas vl (list (A * X)).
Proof.
split; trivial; intros; rewrite /hsubst /list_pair_hsubst;
elim: s => [|[l d] xs IHds] //; asimpl; by f_equal.
Qed.
Instance HSubstLemmas_dms : HSubstLemmas vl dms := _.

(** After instantiating Autosubst, a few binding-related syntactic definitions
that need not their own file. *)

Expand Down Expand Up @@ -557,6 +593,9 @@ Ltac solve_fv_congruence :=
Lemma fv_cons `{Ids X} `{HSubst vl X} {hsla: HSubstLemmas vl X} (x: X) xs n: nclosed xs n → nclosed x n → nclosed (x :: xs) n.
Proof. solve_fv_congruence. Qed.

Lemma fv_pair_cons {A} `{Ids X} `{HSubst vl X} {hsla: HSubstLemmas vl X} (a: A) (x: X) xs n: nclosed xs n → nclosed x n → nclosed ((a, x) :: xs) n.
Proof. solve_fv_congruence. Qed.

(** The following ones are "inverse" lemmas: by knowing that an expression is closed,
deduce that one of its subexpressions is closed *)

Expand Down
21 changes: 11 additions & 10 deletions theories/Dot/fundamental.v
Original file line number Diff line number Diff line change
Expand Up @@ -44,9 +44,9 @@ Section fundamental.
iIntros "#H".
cbn; fold t_dm t_dms.
(* remember t_dms as t_ds eqn:Heqt. unfold t_dms in Heqt. rewrite -Heqt. fold t_dms in Heqt. rewrite Heqt. *)
iInduction ds as [] "IHds" forall (ds'); destruct ds' => //.
iInduction ds as [|(l, d) ds] "IHds" forall (ds'); destruct ds' as [| (l', d') ds' ]=> //.
cbn; fold t_dms.
iDestruct "H" as "[Hd Hds]".
iDestruct "H" as "[% [Hd Hds]]".
by iPoseProof ("IHds" with "Hds") as "<-".
Qed.

Expand All @@ -61,9 +61,9 @@ Section fundamental.
iIntros (Hlook1 Hlook2) "#HTr".
inversion Hlook1 as (ds1 & -> & Hl1).
inversion Hlook2 as (ds2 & -> & Hl2).
rewrite lookup_reverse_indexr in Hl1.
rewrite lookup_reverse_indexr in Hl2.
iInduction ds1 as [| dh1 ds1] "IHds" forall (ds2 Hlook2 Hl2); destruct ds2 as [|dh2 ds2]=>//.
(* rewrite lookup_reverse_indexr in Hl1. *)
(* rewrite lookup_reverse_indexr in Hl2. *)
iInduction ds1 as [| (l1, dh1) ds1] "IHds" forall (ds2 Hlook2 Hl2); destruct ds2 as [|(l2, dh2) ds2]=>//.
iPoseProof (transl_len with "HTr") as "%". move: H => Hlen.
injection Hlen; clear Hlen; intro Hlen.
cbn in *; fold t_dm t_dms.
Expand All @@ -84,14 +84,15 @@ Section fundamental.
destruct v => //.
iPoseProof (transl_len with "HTr1") as "%". move: H => Hlen1.
iPoseProof (transl_len with "HTr2") as "%". move: H => Hlen2.
assert (∃ d, reverse (selfSubst l0) !! l = Some d) as [d Hl]. {
apply lookup_lt_is_Some_2.
rewrite reverse_length selfSubst_len Hlen1 -selfSubst_len -reverse_length.
eapply lookup_lt_is_Some_1. rewrite Hl1; eauto.
assert (∃ d, dms_lookup l (selfSubst l0) = Some d) as [d Hl]. {
(* (* apply lookup_lt_is_Some_2. *) *)
(* rewrite reverse_length selfSubst_len Hlen1 -selfSubst_len -reverse_length. *)
(* eapply lookup_lt_is_Some_1. rewrite Hl1; eauto. *)
admit.
}
assert (vobj l0 @ l ↘ d). by exists l0.
iExists d. repeat iSplit => //; by iApply transl_lookup_commute'.
Qed.
Admitted.

Lemma lookups_agree v0 v1 v2 ρ σ1 σ2 γ1 γ2 φ1 l:
v1.[to_subst ρ] @ l ↘ dtysem σ1 γ1 → v2.[to_subst ρ] @ l ↘ dtysem σ2 γ2 →
Expand Down
100 changes: 54 additions & 46 deletions theories/Dot/lr_lemmasDefs.v
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ Section Sec.
worst-case, we can add a fancy update to definition typing. *)
Lemma idtp_vmem_i T v l:
ivtp Γ (TLater T) v -∗
Γ ⊨d { l = dvl v } : TVMem l T.
Γ ⊨d dvl v : TVMem l T.
Proof.
iIntros "#[% #Hv]". move: H => Hclv. iSplit. auto using fv_dvl. iIntros "!> * #Hg".
iPoseProof (interp_env_ρ_closed with "Hg") as "%". move: H => Hclρ.
Expand Down Expand Up @@ -63,7 +63,7 @@ Section Sec.
Γ ⊨ [T, 1] <: [U, 1] -∗
Γ ⊨ [L, 1] <: [T, 1] -∗
γ ⤇ dot_interp T -∗
Γ ⊨d { l = dtysem (idsσ (length Γ)) γ } : TTMem l L U.
Γ ⊨d dtysem (idsσ (length Γ)) γ : TTMem l L U.
Proof.
iIntros " #HLU #HTU #HLT #Hγ /=".
iSplit. by auto using fv_dtysem, fv_idsσ.
Expand Down Expand Up @@ -100,51 +100,58 @@ Section Sec.

Lemma idtp_tmem_i T γ l:
γ ⤇ dot_interp T -∗
Γ ⊨d { l = dtysem (idsσ (length Γ)) γ } : TTMem l T T.
Γ ⊨d dtysem (idsσ (length Γ)) γ : TTMem l T T.
Proof.
iIntros " #Hγ".
iApply (idtp_tmem_abs_i T T T) => //=;
by iIntros "!> **".
Qed.

Lemma dtp_tand_i T U ρ d ds:
defs_interp T ρ ds -∗
def_interp U (length ds) ρ d -∗
defs_interp (TAnd T U) ρ (cons d ds).
Proof. naive_solver. Qed.
(* Lemma dtp_tand_i T U ρ d ds l: *)
(* defs_interp T ρ ds -∗ *)
(* def_interp U ρ d -∗ *)
(* defs_interp (TAnd T U) ρ (cons (l, d) ds). *)
(* Proof. naive_solver. Qed. *)

Lemma def_interp_to_interp T d ds ρ s:
let v0 := (vobj (d :: ds)).[s] in
Lemma def_interp_to_interp T d ds ρ s l:
let v0 := (vobj ((l, d) :: ds)).[s] in
nclosed_vl v0 0 →
def_interp T (length ds) ρ (d.|[v0 .: s]) ⊢
label_of_ty T = Some l →
def_interp T ρ (d.|[v0 .: s]) ⊢
interp T ρ v0.
Proof.
intros * Hfvv0. asimpl.
intros * Hfvv0 HTlabel. asimpl.
set (d' := d.|[up s]); set (ds' := ds.|[up s]).
assert (nclosed_vl (vobj (d' :: ds')) 0) as Hfv'. {
assert (nclosed_vl (vobj ((l, d') :: ds')) 0) as Hfv'. {
revert v0 Hfvv0.
asimpl.
by subst d' ds'.
}
assert (length ds = length ds') as Hlen'. by rewrite /ds' /hsubst map_length.
assert (vobj (d' :: ds') @ length ds ↘ d'.|[vobj (d' :: ds')/]) as Hlookup.
by rewrite Hlen'; apply obj_lookup_cons.
assert (vobj ((l, d') :: ds') @ l ↘ d'.|[vobj ((l, d') :: ds')/]) as Hlookup.
admit.
(* XXX we need to rewrite this lemma for the new lookup relation, after fixing typing.
by rewrite Hlen'; apply obj_lookup_cons. *)
induction T => //=; try (by iIntros "**").
all: iIntros "[% [% #H]]"; move: H H0 => Hlen Hfvd; rewrite <- Hlen.
all: cbn in HTlabel; injectHyps; iIntros "[% #H]"; move: H => Hvd.
- iDestruct "H" as (vmem) "[#H1 #H2]".
iSplit => //.
iExists (d'.|[vobj (d' :: ds')/]). iSplit => //.
subst d'. asimpl.
iExists (d'.|[vobj ((l, d') :: ds')/]).
subst d' ds'; iSplit => //.
asimpl; trivial.
(* subst d' ds'. asimpl. apply Hlookup. *)
(* subst; eauto. *)
(* subst d'. asimpl. *)
iSplit => //. iExists _. iSplit => //.
- iDestruct "H" as (φ σ) "[#Hl [#? [#? #?]]]".
iDestruct "Hl" as (γ) "[% #Hγ]". move: H => Hl.
iSplit => //.
iExists (d'.|[vobj (d' :: ds')/]). iSplit => //.
iExists (d'.|[vobj ((l, d') :: ds')/]). iSplit => //.
subst d'; asimpl.
iSplit => //. iExists φ, σ; iSplit => //.
* iExists γ; iSplit => //.
* iModIntro. repeat iSplitL; naive_solver.
Qed.
Admitted.

(* Formerly wip_hard. *)
Lemma defs_interp_to_interp T ds ρ s:
Expand All @@ -163,32 +170,33 @@ Section Sec.

simpl; iIntros (Hcl) "#H".
iPoseProof (defs_interp_v_closed with "H") as "%". move: H => Hclds.
iInduction T as [] "IHT" forall (ds Hcl Hclds) => //.
destruct ds => //=. rewrite map_length.
iDestruct "H" as "[#H1 #H2]".
iSplit.
2: { by iApply (def_interp_to_interp T2 d ds ρ s). }
- asimpl.
iAssert (⟦ T1 ⟧ ρ (vobj (ds.|[up s]))) as "#H3". {
iApply ("IHT" $! ds) => //.
admit.
admit.
asimpl.
Fail iApply "H1".
admit.
}
(* We could probably go from H3 to the thesis... *)
iApply ("IHT" $! (d :: ds)) => //.
admit.

(* iApply (IHT1 (d :: ds)). *)
(* set (d' := d.|[up (to_subst ρ)]). *)
(* set (ds' := ds.|[up (to_subst ρ)]). *)
(* change (ds.|[up (to_subst ρ)]) with ds'. *)

(* simpl. *)
(* induction T; rewrite /defs_interp => //=; fold defs_interp; *)
(* try solve [iIntros; try done]. *)
iInduction T as [] "IHT" forall (ds Hcl Hclds) => //=; try iDestruct "H" as (l1 d) "[% H']"; trivial.

(* destruct ds => //=. rewrite map_length. *)
(* iDestruct "H" as "[#H1 #H2]". *)
(* iSplit. *)
(* 2: { by iApply (def_interp_to_interp T2 d ds ρ s). } *)
(* - asimpl. *)
(* iAssert (⟦ T1 ⟧ ρ (vobj (ds.|[up s]))) as "#H3". { *)
(* iApply ("IHT" $! ds) => //. *)
(* admit. *)
(* admit. *)
(* asimpl. *)
(* Fail iApply "H1". *)
(* admit. *)
(* } *)
(* (* We could probably go from H3 to the thesis... *) *)
(* iApply ("IHT" $! (d :: ds)) => //. *)
(* admit. *)

(* (* iApply (IHT1 (d :: ds)). *) *)
(* (* set (d' := d.|[up (to_subst ρ)]). *) *)
(* (* set (ds' := ds.|[up (to_subst ρ)]). *) *)
(* (* change (ds.|[up (to_subst ρ)]) with ds'. *) *)

(* (* simpl. *) *)
(* (* induction T; rewrite /defs_interp => //=; fold defs_interp; *) *)
(* (* try solve [iIntros; try done]. *) *)
Admitted.

(* Check that Löb induction works as expected for proving introduction of
Expand Down