- update notations

proof/old_system/uni/algo_worklist/prop_completeness.v

@@ -136,10 +136,10 @@ Qed.
 
 Lemma d_mono_typ_strengthen_app : forall θ1 θ2 X T1 T2,
   wf_ss (θ2 ++ (X, dbind_typ T1) :: θ1) ->
-  d_mono_typ (ss_to_denv (θ2 ++ (X, dbind_typ T1) :: θ1)) T2 ->
-  d_mono_typ (ss_to_denv θ1) T1 ->
+  ss_to_denv (θ2 ++ (X, dbind_typ T1) :: θ1) ᵗ⊢ᵈₘ T2 ->
+  ss_to_denv θ1 ᵗ⊢ᵈₘ T1 ->
   (∀ Y : atom, Y `in` ftvar_in_typ T2 → Y `in` ftvar_in_typ T1) ->
-  d_mono_typ (ss_to_denv θ1) T2.
+  ss_to_denv θ1 ᵗ⊢ᵈₘ T2.
 Proof.
   intros. induction θ2; simpl in *; auto.
   - destruct a as [X0 b]. destruct b.
@@ -1139,7 +1139,7 @@ Ltac solve_wf_typ :=
     H_3: ?θ ᵗ⊩ ?Aᵃ ⇝ ?Aᵈ |- d_wf_typ (dwl_to_denv ?Ω) ?Aᵈ =>
     eapply trans_wl_a_wf_typ_d_wf_typ; eauto
   | H_1 : d_wf_typ (ss_to_denv ?θ) ?A,
-    H_2: nil ⊩ ?Γ ⇝ ?Ω ⫣ ?θ |- dwl_to_denv ?Ω ⊢ ?A =>
+    H_2: nil ⊩ ?Γ ⇝ ?Ω ⫣ ?θ |- dwl_to_denv ?Ω ᵗ⊢ᵈ ?A =>
     eapply trans_wl_ss_wf_typ_d_wf_typ; eauto
   | _ : _ |- _ => idtac
   end.

proof/old_system/uni/algo_worklist/prop_rename.v

@@ -9,7 +9,6 @@ Require Import uni.prop_basic.
 Require Import uni.algo_worklist.def_extra.
 Require Import uni.algo_worklist.prop_basic.
 Require Import ltac_utils.
-Require Import LibTactics.
 
 
 Open Scope aworklist_scope.
@@ -811,12 +810,12 @@ Qed.
 
 Lemma a_wl_rename_tvar_wf_exp : forall Γ X X' e,
   ⊢ᵃʷ Γ ->
-  X' `notin` dom (awl_to_aenv Γ) ->
+  X' ∉ dom (⌊ Γ ⌋ᵃ)  ->
   a_wf_exp (⌊ Γ ⌋ᵃ) e ->
   a_wf_exp (⌊ rename_tvar_in_aworklist X' X Γ ⌋ᵃ) (subst_tvar_in_exp (typ_var_f X') X e)
 with a_wl_rename_tvar_wf_body : forall Γ X X' b,
   ⊢ᵃʷ Γ ->
-  X' `notin` dom (awl_to_aenv Γ) ->
+  X' ∉ dom (⌊ Γ ⌋ᵃ)  ->
   a_wf_body (⌊ Γ ⌋ᵃ) b ->
   a_wf_body (⌊ rename_tvar_in_aworklist X' X Γ ⌋ᵃ) (subst_tvar_in_body (typ_var_f X') X b).
 Proof with eauto using a_wl_rename_tvar_wf_typ.
@@ -855,22 +854,22 @@ Qed.
 
 Lemma a_wl_rename_tvar_wf_conts : forall Γ X X' cs,
   ⊢ᵃʷ Γ ->
-  X' `notin` dom (awl_to_aenv Γ) ->
+  X' ∉ dom (⌊ Γ ⌋ᵃ)  ->
   a_wf_conts (⌊ Γ ⌋ᵃ) cs ->
-  a_wf_conts (⌊ rename_tvar_in_aworklist X' X Γ ⌋ᵃ) (subst_tvar_in_conts (typ_var_f X') X cs)
+  a_wf_conts (⌊ rename_tvar_in_aworklist X' X Γ ⌋ᵃ) ({` X' ᶜˢ/ₜ X} cs)
 with a_wl_rename_tvar_wf_contd : forall Γ X X' cd,
   ⊢ᵃʷ Γ ->
-  X' `notin` dom (awl_to_aenv Γ) ->
+  X' ∉ dom (⌊ Γ ⌋ᵃ)  ->
   a_wf_contd (⌊ Γ ⌋ᵃ) cd ->
-  a_wf_contd (⌊ rename_tvar_in_aworklist X' X Γ ⌋ᵃ) (subst_tvar_in_contd (typ_var_f X') X cd).
+  a_wf_contd (⌊ rename_tvar_in_aworklist X' X Γ ⌋ᵃ) ({` X' ᶜᵈ/ₜ X} cd).
 Proof with auto using a_wl_rename_tvar_wf_typ, a_wl_rename_tvar_wf_exp.
   - intros. clear a_wl_rename_tvar_wf_conts. dependent induction H1; simpl in *; auto...
   - intros. clear a_wl_rename_tvar_wf_contd. dependent induction H1; try repeat destruct_wf_arrow; simpl in *; auto...
 Qed.
 
 Lemma a_wl_rename_tvar_wf_work : forall Γ X X' w,
   ⊢ᵃʷ Γ ->
-  X' `notin` dom (awl_to_aenv Γ) ->
+  X' ∉ dom (⌊ Γ ⌋ᵃ)  ->
   a_wf_work (⌊ Γ ⌋ᵃ) w ->
   a_wf_work (⌊ rename_tvar_in_aworklist X' X Γ ⌋ᵃ) (subst_tvar_in_work (typ_var_f X') X w).
 Proof with auto 8 using a_wl_rename_tvar_wf_typ, a_wl_rename_tvar_wf_exp, a_wl_rename_tvar_wf_conts, a_wl_rename_tvar_wf_contd.
@@ -880,7 +879,7 @@ Qed.
 
 Lemma a_wf_wl_rename_tvar : forall Γ X X',
   ⊢ᵃʷ Γ ->
-  X' `notin` dom (awl_to_aenv Γ) ->
+  X' ∉ dom (⌊ Γ ⌋ᵃ) ->
   ⊢ᵃʷ (rename_tvar_in_aworklist X' X Γ).
 Proof with eauto.
   intros. induction H; try solve [simpl in *; eauto].
@@ -913,46 +912,44 @@ Qed.
 
 Lemma apply_conts_rename_tvar : forall cs A w X X',
   apply_conts cs A w ->
-  apply_conts (subst_tvar_in_conts (typ_var_f X') X cs) (subst_tvar_in_typ (typ_var_f X') X A)
-    (subst_tvar_in_work (typ_var_f X') X w).
+  apply_conts ({`X' ᶜˢ/ₜ X} cs) ({`X' ᵗ/ₜ X} A) ({` X' ʷ/ₜ X} w).
 Proof.
   intros. induction H; simpl; try solve [simpl; eauto].
 Qed.
 
 
 Lemma apply_contd_rename_tvar : forall cd A B w X X',
   apply_contd cd A B w ->
-  apply_contd (subst_tvar_in_contd (typ_var_f X') X cd) (subst_tvar_in_typ (typ_var_f X') X A) (subst_tvar_in_typ (typ_var_f X') X B)
-    (subst_tvar_in_work (typ_var_f X') X w).
+  apply_contd ({`X' ᶜᵈ/ₜ X} cd) ({`X' ᵗ/ₜ X} A) ({`X' ᵗ/ₜ X} B) ({`X' ʷ/ₜ X} w).
 Proof.
   intros. induction H; simpl; try solve [simpl; eauto].
 Qed.
 
 Lemma aworlist_subst_dom_upper1' : forall Γ X A Γ1 Γ2,
   aworklist_subst Γ X A Γ1 Γ2 ->
-  dom (awl_to_aenv Γ1) [<=] (dom (awl_to_aenv Γ)).
+  dom (⌊ Γ1 ⌋ᵃ) [<=] dom (⌊ Γ ⌋ᵃ).
 Proof.
   intros * Haws; simpl; induction Haws; simpl in *; try fsetdec.
   - autorewrite with core in *. simpl in *. fsetdec.
 Qed.
 
 Lemma aworlist_subst_dom_upper2' : forall Γ X A Γ1 Γ2,
   aworklist_subst Γ X A Γ1 Γ2 ->
-  dom (awl_to_aenv Γ2) [<=] dom (awl_to_aenv Γ).
+  dom (⌊ Γ2 ⌋ᵃ) [<=] dom (⌊ Γ ⌋ᵃ).
 Proof.
   intros. induction H; simpl; try fsetdec.
   - autorewrite with core in *. simpl in *. fsetdec.
 Qed.
 
 Lemma subst_typ_in_aworklist_dom_eq : forall Γ X A,
-  dom (awl_to_aenv ({A ᵃʷ/ₜ X} Γ)) [=] dom (awl_to_aenv Γ).
+  dom (⌊ {A ᵃʷ/ₜ X} Γ ⌋ᵃ) [=] dom (⌊ Γ ⌋ᵃ).
 Proof.
   intros. induction Γ; simpl; fsetdec.
 Qed.
 
 Lemma aworklist_subst_dom_upper : forall Γ X A Γ1 Γ2,
   aworklist_subst Γ X A Γ1 Γ2 ->
-  dom (⌊ {A ᵃʷ/ₜ X} Γ2 ⧺ Γ1 ⌋ᵃ) [<=] dom (awl_to_aenv Γ).
+  dom (⌊ {A ᵃʷ/ₜ X} Γ2 ⧺ Γ1⌋ᵃ) [<=] dom (⌊ Γ ⌋ᵃ).
 Proof.
   intros. autorewrite with core.
   rewrite subst_typ_in_aworklist_dom_eq.
@@ -1122,13 +1119,12 @@ Proof with eauto; solve_false.
     + intros. fold_subst. eapply s_in_subst in H0...
     + intros. simpl in *.
       apply worklist_subst_rename_tvar with (X':=X) (X1:=X') (X2:=X0) in H10 as Hws.
-      * destruct_eq_atom. simpl in Hws.
-        destruct_eq_atom.
+      * simpl in Hws. destruct_eq_atom.
         rewrite rename_tvar_in_typ_rev_eq in *...
         rewrite rename_tvar_in_typ_rev_eq in *...
         rewrite rename_tvar_in_aworklist_rev_eq in Hws; auto...
         apply H8 in Hws as Hawlred; simpl; auto.
-        -- clear Hws. destruct_eq_atom.
+        -- clear Hws. 
            rewrite_aworklist_rename; simpl; eauto.
            rewrite_aworklist_rename_rev.
            simpl in Hawlred. destruct_eq_atom. auto.
@@ -1196,10 +1192,8 @@ Proof with eauto; solve_false.
     + intros.
       inst_cofinites_with x. inst_cofinites_with X1. inst_cofinites_with X2.
       apply worklist_subst_rename_tvar with (X':=X) (X1:=X') (X2:=X') in H11 as Hws.
-      destruct_eq_atom.
-      * simpl in Hws.
-        destruct_eq_atom.
-        rewrite rename_tvar_in_aworklist_rev_eq in Hws; auto...
+      simpl in Hws. destruct_eq_atom.
+      * rewrite rename_tvar_in_aworklist_rev_eq in Hws; auto...
         simpl in Hws.
         replace (exp_var_f x) with (subst_tvar_in_exp (` X') X (exp_var_f x)) in Hws by auto.
         rewrite <- subst_tvar_in_exp_open_exp_wrt_exp in Hws.
@@ -1208,7 +1202,7 @@ Proof with eauto; solve_false.
            ++ assert (X `notin` (ftvar_in_exp (subst_tvar_in_exp ` X' X e ᵉ^ₑ exp_var_f x))) by (solve_notin_rename_tvar; auto).
               clear Hws. destruct_eq_atom.
               rewrite_aworklist_rename; simpl; auto.
-              rewrite_aworklist_rename_rev.
+              rewrite_aworklist_rename_rev. 
               simpl in Hawlred. destruct_eq_atom. auto.
            ++ eapply aworklist_subst_wf_wl in Hws; simpl in *; eauto 9. 
               ** repeat (constructor; simpl; eauto). eapply a_wf_exp_weaken_etvar_twice with (T:=T)...
@@ -1798,27 +1792,6 @@ Proof.
 Qed.
 
 
-Lemma lc_exp_subst_var_in_exp : forall e1 e2 x,
-  lc_exp e1 ->
-  lc_exp e2 ->
-  lc_exp (subst_var_in_exp e2 x e1)
-with lc_body_subst_var_in_body : forall b e x,
-  lc_body b ->
-  lc_exp e ->
-  lc_body (subst_var_in_body e x b).
-Proof with eauto using lc_typ_subst.
-  - intros. clear lc_exp_subst_var_in_exp. induction H; simpl...
-    + destruct_eq_atom; auto.
-    + pick fresh x0. apply lc_exp_abs_exists with (x1:=x0). 
-      replace (({e2 ᵉ/ₑ x} e) ᵉ^ₑ exp_var_f x0) with ({e2 ᵉ/ₑ x} (e ᵉ^ₑ exp_var_f x0))...
-      rewrite subst_var_in_exp_open_exp_wrt_exp... simpl; destruct_eq_atom...
-    + pick fresh X0. apply lc_exp_tabs_exists with (X1:=X0).
-      replace (open_body_wrt_typ ({e2 ᵇ/ₑ x} body5) ` X0) with ({e2 ᵇ/ₑ x} (open_body_wrt_typ body5 ` X0))...
-      rewrite subst_var_in_body_open_body_wrt_typ...
-  - intros. clear lc_body_subst_var_in_body. destruct b. 
-      dependent destruction H; simpl...
-Qed.
-
 Lemma a_wf_exp_rename_var : forall Γ x x' e,
   ⊢ᵃʷ Γ ->
   x' `notin` fvar_in_aworklist' Γ ->

proof/old_system/uni/algo_worklist/prop_soundness.v

@@ -527,7 +527,7 @@ Qed.
 #[local] Hint Immediate trans_wl_wf_ss : core.
 
 Lemma tvar_notin_dom_neq_tvar_in_ss_wf_typ : forall θ T X Y,
-  ss_to_denv θ ⊢ₘ T ->
+  ss_to_denv θ ᵗ⊢ᵈₘ T ->
   X `in` ftvar_in_typ T ->
   Y `notin` dom θ ->
   X <> Y.
@@ -596,7 +596,7 @@ Proof with auto.
     assert (wf_ss ((X ~ dbind_typ Aᵈ) ++ θ)). { 
       constructor; eauto.
       erewrite trans_wl_ss_dom_upper; eauto. 
-      eapply trans_wl_a_mono_typ_d_mono_typ with (Aᵃ:=A); eauto.
+      eapply trans_wl_a_mono_typ_d_mono_typ with (Tᵃ:=A); eauto.
     }
     dependent destruction H6.
     repeat split; auto.
@@ -682,7 +682,7 @@ Proof with auto.
     apply IHaworklist_subst in H6 as IH.
     destruct IH as [θ'1 [Tᵈ [Htrans [Htranst [Htranst' [Hbinds [Htransx Hwfss]]]]]]].    
     exists (Y ~ dbind_typ T ++ θ'1). exists Tᵈ.
-    assert (ss_to_denv θ'1 ⊢ₘ T). {
+    assert (ss_to_denv θ'1 ᵗ⊢ᵈₘ T). {
       apply d_mono_typ_reorder_ss with (θ:=θ'); eauto.
       intros. apply Hbinds; auto. apply neq_comm.
       eapply tvar_notin_dom_neq_tvar_in_ss_wf_typ with (X:=X0); eauto.
@@ -783,8 +783,8 @@ Ltac solve_notin_dom :=
 
 Lemma worklist_subst_fresh_etvar_total : forall Γ1 Γ2 X X1 X2,
   ⊢ᵃʷ (Γ2 ⧺ X ~ᵃ ⬒ ;ᵃ Γ1) ->
-  X1 `notin` dom (awl_to_aenv (Γ2 ⧺ X ~ᵃ ⬒ ;ᵃ Γ1)) ->
-  X2 `notin` add X1 (dom (awl_to_aenv (Γ2 ⧺ X ~ᵃ ⬒ ;ᵃ Γ1))) ->
+  X1 `notin` dom (⌊ Γ2 ⧺ X ~ᵃ ⬒ ;ᵃ Γ1 ⌋ᵃ) ->
+  X2 `notin` add X1 (dom (⌊ Γ2 ⧺ X ~ᵃ ⬒ ;ᵃ Γ1 ⌋ᵃ)) ->
   aworklist_subst (X2 ~ᵃ ⬒ ;ᵃ X1 ~ᵃ ⬒ ;ᵃ Γ2 ⧺ X ~ᵃ ⬒ ;ᵃ Γ1) X
     (typ_arrow ` X1 ` X2) (X1 ~ᵃ ⬒ ;ᵃ X2 ~ᵃ ⬒ ;ᵃ Γ1) Γ2.
 Proof with auto.
@@ -983,15 +983,6 @@ Proof.
     try repeat unify_trans_typ; try unify_trans_exp; try constructor.
 Qed.
 
-Ltac fold_open_wrt_rec' := 
-  match goal with 
-  | H : context [open_typ_wrt_typ_rec 0 ?B ?A] |- _ => replace (open_typ_wrt_typ_rec 0 B A) with (open_typ_wrt_typ A B) in H by auto
-  | H : context [open_exp_wrt_typ_rec 0 ?A ?e] |- _ => replace (open_exp_wrt_typ_rec 0 A e) with (open_exp_wrt_typ e A) in H by auto
-  end.
-
-Ltac fold_open_wrt_rec :=
-  repeat fold_open_wrt_rec'.
-
 #[local] Hint Resolve trans_typ_wf_ss trans_wl_a_wf_typ_d_wf_typ : core.
 
 #[local] Hint Resolve a_wf_wl_a_wf_bind_typ : core.
@@ -1357,9 +1348,10 @@ Proof with eauto.
   - destruct_a_wf_wl. 
     pick fresh X. inst_cofinites_with X.
     assert (Hwf: ⊢ᵃʷ (work_check (e ᵉ^ₜ ` X) (A ᵗ^ₜ X) ⫤ᵃ X ~ᵃ □ ;ᵃ work_applys cs (typ_all A) ⫤ᵃ Γ)). {
+      rewrite open_body_wrt_typ_anno in *.
       dependent destruction H0...
       dependent destruction H...
-      repeat (constructor; simpl; auto). fold_open_wrt_rec.
+      repeat (constructor; simpl; auto).
       inst_cofinites_for a_wf_typ__all; intros.
       solve_s_in.
       apply a_wf_typ_rename_tvar_cons with (Y:=X0) in H1. 
@@ -1392,7 +1384,8 @@ Proof with eauto.
       }
       unify_trans_typ. inversion H11. subst.
       apply d_wl_del_red__inf with (A:=typ_all (close_typ_wrt_typ X Axᵈ)).
-      * dependent destruction H. dependent destruction H1. fold_open_wrt_rec.
+      * rewrite open_body_wrt_typ_anno in *.
+        dependent destruction H. dependent destruction H1. 
         inst_cofinites_for d_chk_inf__inf_tabs. 
         -- inst_cofinites_for d_wf_typ__all; intros; inst_cofinites_with X0; 
            rewrite_close_open_subst. apply s_in_rename. 

proof/old_system/uni/algo_worklist/transfer.v

@@ -602,7 +602,7 @@ Qed.
 
 Lemma wf_ss_typ_no_etvar: forall θ X A T,
   wf_ss θ ->
-  ss_to_denv θ ⊢ A ->
+  ss_to_denv θ ᵗ⊢ᵈ A ->
   X ~ T ∈ᵈ θ ->
   X `notin` ftvar_in_typ A.
 Proof with eauto.
@@ -1145,7 +1145,7 @@ Qed.
 
 Lemma trans_typ_wf_dtyp : forall θ Aᵃ Aᵈ,
   θ ᵗ⊩ Aᵃ ⇝ Aᵈ ->
-  (ss_to_denv θ) ⊢ Aᵈ.
+  (ss_to_denv θ) ᵗ⊢ᵈ Aᵈ.
 Proof with eauto.
   intros. induction H...
   - constructor; auto.
@@ -1737,7 +1737,7 @@ Qed.
 Lemma trans_wl_wf_bind_typ : forall Γ Ω θ X T,
   nil ⊩ Γ ⇝ Ω ⫣ θ ->
   binds X (dbind_typ T) θ ->
-  dwl_to_denv Ω ⊢ T.
+  dwl_to_denv Ω ᵗ⊢ᵈ T.
 Proof.
   intros.
   apply trans_wl_wf_ss in H as Hwfss.
@@ -1763,14 +1763,14 @@ Proof with eauto using binds_ss_to_denv_binds_ss, binds_tvar_ss_binds_ss_to_denv
   - eapply wf_ss_binds_mono_typ; eauto.
 Qed.
 
-Lemma trans_wl_a_mono_typ_d_mono_typ : forall Γ Ω θ Aᵃ Aᵈ,
+Lemma trans_wl_a_mono_typ_d_mono_typ : forall Γ Ω θ Tᵃ Tᵈ,
   nil ⊩ Γ ⇝ Ω ⫣ θ ->
-  θ ᵗ⊩ Aᵃ ⇝ Aᵈ ->
-  a_mono_typ (awl_to_aenv Γ) Aᵃ ->
-  d_mono_typ (ss_to_denv θ) Aᵈ.
+  θ ᵗ⊩ Tᵃ ⇝ Tᵈ ->
+  a_mono_typ (awl_to_aenv Γ) Tᵃ ->
+  d_mono_typ (ss_to_denv θ) Tᵈ.
 Proof.
   intros * Htranswl Htransa Hmono. eapply trans_typ_a_mono_typ_d_mono_typ; eauto.
-   generalize dependent Aᵈ. dependent induction Hmono; intros.
+   generalize dependent Tᵈ. dependent induction Hmono; intros.
   - constructor.
   - constructor. eapply trans_wl_a_wl_binds_tvar_ss in H; eauto.
     apply binds_tvar_ss_binds_ss_to_aenv; eauto.
@@ -1794,7 +1794,7 @@ Qed.
 Lemma trans_typ_tvar_stvar_in_atyp_in_dtyp' : forall θ X Aᵃ Aᵈ,
   lc_typ Aᵃ ->
   θ ᵗ⊩ Aᵃ ⇝ Aᵈ ->
-  binds X dbind_tvar_empty θ \/ binds X dbind_stvar_empty θ ->
+  X ~ □ ∈ᵈ θ \/ X ~ ■ ∈ᵈ θ ->
   X `in` ftvar_in_typ Aᵃ -> 
   X `in` ftvar_in_typ Aᵈ.
 Proof.
@@ -1883,8 +1883,8 @@ Lemma trans_wl_a_wf_typ_d_wf_typ' : forall Γ Ω θ Aᵃ Aᵈ,
   lc_typ Aᵃ ->
   nil ⊩ Γ ⇝ Ω ⫣ θ ->
   θ ᵗ⊩ Aᵃ ⇝ Aᵈ ->
-  a_wf_typ (awl_to_aenv Γ) Aᵃ ->
-  d_wf_typ (dwl_to_denv Ω) Aᵈ.
+  ⌊ Γ ⌋ᵃ ᵗ⊢ᵃ Aᵃ ->
+  dwl_to_denv Ω ᵗ⊢ᵈ Aᵈ.
 Proof with eauto. 
   intros * Hlc. 
   generalize dependent Aᵈ.
@@ -2441,7 +2441,7 @@ Qed.
 
 
 Lemma trans_typ_refl: forall θ A,
-  ss_to_denv θ ⊢ A ->
+  ss_to_denv θ ᵗ⊢ᵈ A ->
   wf_ss θ ->
   θ ᵗ⊩ A ⇝ A.
 Proof with eauto.