Merge pull request #14 from Blaisorblade/fix-dms

Fix object member lookup

theories/Dot/dotsyn.v

@@ -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
@@ -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
@@ -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 *)
@@ -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). *)
@@ -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).
@@ -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). *)
@@ -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
@@ -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
@@ -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
@@ -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.
@@ -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
@@ -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. *)
 
@@ -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 *)
 

theories/Dot/fundamental.v

@@ -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.
 
@@ -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.
@@ -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 →

theories/Dot/lr_lemmasDefs.v

@@ -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ρ.
@@ -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σ.
@@ -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:
@@ -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