From 79e938f1ea4d8bcf8d69420bc523a14d68a2ef0e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 22 Apr 2017 20:24:45 +0200
Subject: [PATCH] Handle singleton in lists of type sepratatly, so that we
avoid "++ []".
---
theories/typing/lib/rc/rc.v | 4 ++--
theories/typing/type.v | 6 +++++-
2 files changed, 7 insertions(+), 3 deletions(-)
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 3471ce8a..3d9b2f04 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -970,8 +970,8 @@ Section code.
iApply type_let; [apply rc_drop_type|solve_typing|]. iIntros (drop). simpl_subst.
iApply (type_letcall ()); [try solve_typing..|].
{ (* FIXME : solve_typing should be able to do this. *)
- move=>ϝ' /=. replace (ty_outlives_E (option ty) ϝ') with (ty_outlives_E ty ϝ').
- solve_typing. by rewrite /ty_outlives_E /= app_nil_r. }
+ move=>ϝ' /=. change (ty_outlives_E (option ty) ϝ') with (ty_outlives_E ty ϝ').
+ solve_typing. }
iIntros (content). simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_assign; [solve_typing..|].
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 35739db0..9b2a19ae 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -83,18 +83,21 @@ Existing Instances tyl_wf_nil tyl_wf_cons.
Fixpoint tyl_lfts `{typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
match WF with
| tyl_wf_nil => []
+ | tyl_wf_cons ty [] _ _ => ty.(ty_lfts)
| tyl_wf_cons ty tyl _ _ => ty.(ty_lfts) ++ tyl.(tyl_lfts)
end.
Fixpoint tyl_wf_E `{typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
match WF with
| tyl_wf_nil => []
+ | tyl_wf_cons ty [] _ _ => ty.(ty_wf_E)
| tyl_wf_cons ty tyl _ _ => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
end.
Fixpoint tyl_outlives_E `{typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
match WF with
| tyl_wf_nil => []
+ | tyl_wf_cons ty [] _ _ => ty.(ty_outlives_E) κ
| tyl_wf_cons ty tyl _ _ => ty.(ty_outlives_E) κ ++ tyl.(tyl_outlives_E) κ
end.
@@ -103,8 +106,9 @@ Lemma tyl_outlives_E_elctx_sat `{typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
lctx_lft_incl E L α β →
elctx_sat E L (tyl.(tyl_outlives_E) α).
Proof.
- induction WF as [|???? IH]=>/=.
+ induction WF as [|? [] ?? IH]=>/=.
- solve_typing.
+ - intros. by eapply ty_outlives_E_elctx_sat.
- intros. apply elctx_sat_app, IH; [eapply ty_outlives_E_elctx_sat| |]=>//;
(etrans; [|done]); solve_typing.
Qed.
--
GitLab