Rocoma.Recipes_neuneu
Zeros under boxes
Fixpoint allzbb r :=
match r with
| Top | Var _ | Box _ => True
| Zero => False
| And s t
| App s t => allzbb s /\ allzbb t
| TLam s
| TAll s
| Neu s
| Imp s _
| Lam s _
| TApp s _ => allzbb s
end.
Lemma allzbb_neu s :
allzbb (neu s).
Proof.
elim: s=>//=.
Qed.
Lemma dec_allzbb s : decidable (allzbb s).
Proof.
elim: s=>//=; try (by left); try (by right).
- move=> s [] h1 t [] h2.
by left.
by right; tauto.
by right; tauto.
by right; tauto.
- move=> s [] h1 t [] h2.
by left.
by right; tauto.
by right; tauto.
by right; tauto.
Qed.
Lemma allzbb_subst_var_n s u n :
allzbb s ->
allzbb s.[Box u//n].
Proof.
elim: s u n=>//=; try by (intros; unpack; eauto).
- move=> h u n ?.
rewrite /subst_var.
by case (lt_eq_lt_dec h n)=>[[]|].
- move=> s h1 _ u n ?. rewrite upn1 subst_var_lemma /=. by apply h1.
- move=> s h1 u n ?. rewrite subst_var_hsubst. by apply h1.
- move=> s h1 u n ?. rewrite subst_var_hsubst. by apply h1.
Qed.
Corollary allzbb_subst_var s u :
allzbb s ->
allzbb s.[Box u/].
Proof.
rewrite -subst_var_0.
by apply allzbb_subst_var_n.
Qed.
Lemma allzbb_hsubst s θ τ :
allzbb s.|[θ] ->
allzbb s.|[τ].
Proof.
by elim: s θ τ=>//= *; unpack; eauto.
Qed.
Declare Module Export V : VALID.
Notation "a ||- b" := (valid (FImp a b)) (at level 61, format "a ||- b") : valid_scope.
Notation "||- b" := (valid b) (at level 61, format "||- b") : valid_scope.
Notation "a ⟛ b" := (valid (FImp a b) /\ valid (FImp b a)) (at level 61, format "a ⟛ b") : valid_scope.
Section Sem.
Open Scope valid_scope.
Lemma valid_exfalso f g :
f ||- FBot ->
f ||- g.
Proof.
move=> h.
apply valid_cut with FBot=>//.
by apply valid_contradiction.
Qed.
Lemma valid_dup f : f ⟛ f ++ f.
Proof.
split.
- apply valid_and_intro; by apply valid_assumption.
- apply valid_and_intro_l.
left. by apply valid_assumption.
Qed.
Lemma valid_and f g :
||- f ->
||- g ->
||- f ++ g.
Proof.
move=> /valid_top_l2 h1 /valid_top_l2 h2.
apply valid_top_l1.
by apply valid_and_intro.
Qed.
Lemma valid_and_l_sym f g h :
h ++ g ||- f ->
g ++ h ||- f.
Proof.
move=> h1.
apply valid_cut with (h ++ g)=>//.
apply valid_and_intro.
- apply valid_weak.
by apply valid_assumption.
- apply valid_contr.
do 2 apply valid_and_l_cycle.
do 2 apply valid_weak.
by apply valid_assumption.
Qed.
Lemma valid_and_l_weak2 :
forall f1 f2 g,
f1 ||- g ->
f1 ++ f2 ||- g.
Proof.
move=>*.
by apply valid_and_l_sym, valid_weak.
Qed.
Lemma valid_assumption_and : forall f g,
f ++ g ||- f.
Proof.
move=> f g.
apply valid_and_l_weak2.
by apply valid_assumption.
Qed.
Lemma valid_and_and_intro f1 g1 f2 g2 :
f1 ||- f2 ->
g1 ||- g2 ->
f1 ++ g1 ||- f2 ++ g2.
Proof.
move=> h1 h2.
apply valid_and_intro.
- by apply valid_and_l_weak2.
- by apply valid_weak.
Qed.
Lemma valid_top0 :
||- FTop.
Proof.
apply valid_top_l1.
by apply valid_assumption.
Qed.
Lemma valid_all_intro f : ||- f -> ||- FAll f.
Proof.
move=> h.
apply valid_top_l1, valid_all_de_bruijn.
have->: FTop.[ren (+1)] = FTop by [].
by apply valid_top_l2.
Qed.
Lemma valid_fallF_elim ts f :
fallF (size ts) f ||- f.[inst ts].
Proof.
elim: ts f=> [|?? ih] ? /=.
- asimpl.
by apply valid_assumption.
- apply: valid_cut; first by apply valid_all_elim.
rewrite fallF_subst.
apply: valid_cut; first by apply ih.
asimpl.
by apply valid_assumption.
Qed.
Ltac valid_trivial :=
by first [ apply valid_top
| apply valid_top0
| apply valid_contradiction
| apply valid_assumption
| apply valid_assumption_and ].
Ltac tac_valid :=
first [ done | valid_trivial
| do 1 apply valid_weak; valid_trivial
| do 2 apply valid_weak; valid_trivial
| do 3 apply valid_weak; valid_trivial
| apply valid_and_l_sym; valid_trivial
| apply valid_and_l_weak2; valid_trivial
].
Ltac tac_valid_cut c :=
apply valid_cut with c; tac_valid.
Lemma valid_weak0 f g :
||- g ->
f ||- g.
Proof.
move /valid_top_l2 => h.
apply valid_cut with (f ++ FTop)=>//.
- apply valid_and_intro.
tac_valid.
tac_valid.
- by apply valid_weak.
Qed.
Lemma valid_imp_imp_split h f g :
f ||- g ->
(FImp h f) ||- (FImp h g).
Proof.
move=> h1.
apply valid_imp_intro.
apply valid_imp_elim.
tac_valid_cut f.
Qed.
Lemma valid_equiv_sym f g :
f ⟛ g ->
g ⟛ f.
Proof.
by move=>[]; split.
Qed.
Lemma valid_equiv_cut f g h :
f ⟛ g ->
f ⟛ h ->
g ⟛ h.
Proof.
move=> []??[]??.
split; tac_valid_cut f.
Qed.
Lemma valid_and_mix_r f a b c d :
f ||- (a ++ c) ++ (b ++ d) ->
f ||- (a ++ b) ++ (c ++ d).
Proof.
move=> /valid_and_elim []
/valid_and_elim []??
/valid_and_elim []??.
by repeat apply valid_and_intro.
Qed.
Lemma valid_and_mix_l f a b c d :
(a ++ c) ++ (b ++ d) ||- f ->
(a ++ b) ++ (c ++ d) ||- f.
Proof.
move=> h.
apply valid_cut with ((a ++ c) ++ (b ++ d))=>//.
repeat apply valid_and_intro; try tac_valid.
apply valid_and_l_weak2.
tac_valid.
Qed.
Lemma valid_and_imp3_l f g1 g2 h :
g1 ++ g2 ||- h ->
(FImp f g1) ++ (FImp f g2) ||- FImp f h.
Proof.
move=> h1.
apply valid_imp_intro.
apply: valid_cut _ h1.
apply valid_and_intro.
- apply valid_and_l_cycle.
apply valid_and_l_cycle.
apply valid_weak.
apply valid_imp_elim.
tac_valid.
- apply valid_and_l_cycle.
apply valid_weak.
apply valid_and_l_sym.
apply valid_imp_elim.
tac_valid.
Qed.
Lemma valid_and_imp3_r f h g1 g2 :
h ||- g1 ++ g2 ->
FImp f h ||- FImp f g1 ++ FImp f g2.
Proof.
move=> h1.
apply valid_and_intro.
+ apply valid_imp_imp_split.
by have[]:= valid_and_elim h1.
+ apply valid_imp_imp_split.
by have[]:= valid_and_elim h1.
Qed.
match r with
| Top | Var _ | Box _ => True
| Zero => False
| And s t
| App s t => allzbb s /\ allzbb t
| TLam s
| TAll s
| Neu s
| Imp s _
| Lam s _
| TApp s _ => allzbb s
end.
Lemma allzbb_neu s :
allzbb (neu s).
Proof.
elim: s=>//=.
Qed.
Lemma dec_allzbb s : decidable (allzbb s).
Proof.
elim: s=>//=; try (by left); try (by right).
- move=> s [] h1 t [] h2.
by left.
by right; tauto.
by right; tauto.
by right; tauto.
- move=> s [] h1 t [] h2.
by left.
by right; tauto.
by right; tauto.
by right; tauto.
Qed.
Lemma allzbb_subst_var_n s u n :
allzbb s ->
allzbb s.[Box u//n].
Proof.
elim: s u n=>//=; try by (intros; unpack; eauto).
- move=> h u n ?.
rewrite /subst_var.
by case (lt_eq_lt_dec h n)=>[[]|].
- move=> s h1 _ u n ?. rewrite upn1 subst_var_lemma /=. by apply h1.
- move=> s h1 u n ?. rewrite subst_var_hsubst. by apply h1.
- move=> s h1 u n ?. rewrite subst_var_hsubst. by apply h1.
Qed.
Corollary allzbb_subst_var s u :
allzbb s ->
allzbb s.[Box u/].
Proof.
rewrite -subst_var_0.
by apply allzbb_subst_var_n.
Qed.
Lemma allzbb_hsubst s θ τ :
allzbb s.|[θ] ->
allzbb s.|[τ].
Proof.
by elim: s θ τ=>//= *; unpack; eauto.
Qed.
Declare Module Export V : VALID.
Notation "a ||- b" := (valid (FImp a b)) (at level 61, format "a ||- b") : valid_scope.
Notation "||- b" := (valid b) (at level 61, format "||- b") : valid_scope.
Notation "a ⟛ b" := (valid (FImp a b) /\ valid (FImp b a)) (at level 61, format "a ⟛ b") : valid_scope.
Section Sem.
Open Scope valid_scope.
Lemma valid_exfalso f g :
f ||- FBot ->
f ||- g.
Proof.
move=> h.
apply valid_cut with FBot=>//.
by apply valid_contradiction.
Qed.
Lemma valid_dup f : f ⟛ f ++ f.
Proof.
split.
- apply valid_and_intro; by apply valid_assumption.
- apply valid_and_intro_l.
left. by apply valid_assumption.
Qed.
Lemma valid_and f g :
||- f ->
||- g ->
||- f ++ g.
Proof.
move=> /valid_top_l2 h1 /valid_top_l2 h2.
apply valid_top_l1.
by apply valid_and_intro.
Qed.
Lemma valid_and_l_sym f g h :
h ++ g ||- f ->
g ++ h ||- f.
Proof.
move=> h1.
apply valid_cut with (h ++ g)=>//.
apply valid_and_intro.
- apply valid_weak.
by apply valid_assumption.
- apply valid_contr.
do 2 apply valid_and_l_cycle.
do 2 apply valid_weak.
by apply valid_assumption.
Qed.
Lemma valid_and_l_weak2 :
forall f1 f2 g,
f1 ||- g ->
f1 ++ f2 ||- g.
Proof.
move=>*.
by apply valid_and_l_sym, valid_weak.
Qed.
Lemma valid_assumption_and : forall f g,
f ++ g ||- f.
Proof.
move=> f g.
apply valid_and_l_weak2.
by apply valid_assumption.
Qed.
Lemma valid_and_and_intro f1 g1 f2 g2 :
f1 ||- f2 ->
g1 ||- g2 ->
f1 ++ g1 ||- f2 ++ g2.
Proof.
move=> h1 h2.
apply valid_and_intro.
- by apply valid_and_l_weak2.
- by apply valid_weak.
Qed.
Lemma valid_top0 :
||- FTop.
Proof.
apply valid_top_l1.
by apply valid_assumption.
Qed.
Lemma valid_all_intro f : ||- f -> ||- FAll f.
Proof.
move=> h.
apply valid_top_l1, valid_all_de_bruijn.
have->: FTop.[ren (+1)] = FTop by [].
by apply valid_top_l2.
Qed.
Lemma valid_fallF_elim ts f :
fallF (size ts) f ||- f.[inst ts].
Proof.
elim: ts f=> [|?? ih] ? /=.
- asimpl.
by apply valid_assumption.
- apply: valid_cut; first by apply valid_all_elim.
rewrite fallF_subst.
apply: valid_cut; first by apply ih.
asimpl.
by apply valid_assumption.
Qed.
Ltac valid_trivial :=
by first [ apply valid_top
| apply valid_top0
| apply valid_contradiction
| apply valid_assumption
| apply valid_assumption_and ].
Ltac tac_valid :=
first [ done | valid_trivial
| do 1 apply valid_weak; valid_trivial
| do 2 apply valid_weak; valid_trivial
| do 3 apply valid_weak; valid_trivial
| apply valid_and_l_sym; valid_trivial
| apply valid_and_l_weak2; valid_trivial
].
Ltac tac_valid_cut c :=
apply valid_cut with c; tac_valid.
Lemma valid_weak0 f g :
||- g ->
f ||- g.
Proof.
move /valid_top_l2 => h.
apply valid_cut with (f ++ FTop)=>//.
- apply valid_and_intro.
tac_valid.
tac_valid.
- by apply valid_weak.
Qed.
Lemma valid_imp_imp_split h f g :
f ||- g ->
(FImp h f) ||- (FImp h g).
Proof.
move=> h1.
apply valid_imp_intro.
apply valid_imp_elim.
tac_valid_cut f.
Qed.
Lemma valid_equiv_sym f g :
f ⟛ g ->
g ⟛ f.
Proof.
by move=>[]; split.
Qed.
Lemma valid_equiv_cut f g h :
f ⟛ g ->
f ⟛ h ->
g ⟛ h.
Proof.
move=> []??[]??.
split; tac_valid_cut f.
Qed.
Lemma valid_and_mix_r f a b c d :
f ||- (a ++ c) ++ (b ++ d) ->
f ||- (a ++ b) ++ (c ++ d).
Proof.
move=> /valid_and_elim []
/valid_and_elim []??
/valid_and_elim []??.
by repeat apply valid_and_intro.
Qed.
Lemma valid_and_mix_l f a b c d :
(a ++ c) ++ (b ++ d) ||- f ->
(a ++ b) ++ (c ++ d) ||- f.
Proof.
move=> h.
apply valid_cut with ((a ++ c) ++ (b ++ d))=>//.
repeat apply valid_and_intro; try tac_valid.
apply valid_and_l_weak2.
tac_valid.
Qed.
Lemma valid_and_imp3_l f g1 g2 h :
g1 ++ g2 ||- h ->
(FImp f g1) ++ (FImp f g2) ||- FImp f h.
Proof.
move=> h1.
apply valid_imp_intro.
apply: valid_cut _ h1.
apply valid_and_intro.
- apply valid_and_l_cycle.
apply valid_and_l_cycle.
apply valid_weak.
apply valid_imp_elim.
tac_valid.
- apply valid_and_l_cycle.
apply valid_weak.
apply valid_and_l_sym.
apply valid_imp_elim.
tac_valid.
Qed.
Lemma valid_and_imp3_r f h g1 g2 :
h ||- g1 ++ g2 ->
FImp f h ||- FImp f g1 ++ FImp f g2.
Proof.
move=> h1.
apply valid_and_intro.
+ apply valid_imp_imp_split.
by have[]:= valid_and_elim h1.
+ apply valid_imp_imp_split.
by have[]:= valid_and_elim h1.
Qed.
Neutrality
Definition neutral s :=
forall f,
eval s [::] f ->
||- f.
Definition NEU U := logrel neutral U.
Lemma neuneu :
forall r U,
closed r -> [ ⊢ r :- U ] ->
allzbb r ->
box_rel neutral r -> NEU U r.
Proof.
(* We proceed as in Theorem 3.2, by proving the neutrality of any closed recipe Υ,
where 0 only occurs inside angle brackets
and all directly boxed subrecipes are strongly neutral. *)
(* We prove this lemma by induction over the weight r. *)
have:
forall n r U,
weight r <= n ->
closed r -> [ ⊢ r :- U ] ->
allzbb r ->
box_rel neutral r -> NEU U r.
(* The latter generalization subsumes the lemma. *)
2: { move=> h r U hc ht ha hb. by apply (h (weight r) r U). }
elim=>[r U hw|n ih].
(* case {0} *)
{ exfalso. have := weight_pos r. by lia. }
(* case {n.+1} *)
{ case.
(* case {Var x} *)
{ by move=> >? /closed_ids. }
(* case {Zero} *)
{ by move=> U ??? []. }
(* case {Top} *)
{ move=> U ?? hty /= _ _.
inv hty.
rewrite /NEU/= => f h. inv h. exact valid_top0. }
(* case {And s t} *)
{ move=> s t U hw /closed_and [hc1 hc2] hty /= [ha1 ha2] hb.
inv hb.
have hts: [ ⊢ s :- U ] by inv hty.
have htt: [ ⊢ t :- U ] by inv hty.
have ns: NEU U s by apply ih=>//; try (simpl in hw; lia).
have nt: NEU U t by apply ih=>//; try (simpl in hw; lia).
apply logical_relation_lemma_proj2=>[l hl hcl htl|//].
rewrite /neutral=> f hf.
apply eval_move_stack_right in hf.
inv hf.
apply valid_and.
- apply: (logical_relation_lemma_proj1 ns (l:=l))=>//.
by apply eval_move_stack_left.
- apply: (logical_relation_lemma_proj1 nt (l:=l))=>//.
by apply eval_move_stack_left. }
(* case {App s t} *)
{ move=> s t U hw /closed_app [hc1 hc2] hty /= [ha1 ha2] hb.
inv hb.
inv hty.
have ns: NEU (Arr U0 U) s by apply ih=>//; try (simpl in hw; lia).
apply ns=>// ξ.
have hct: closed t.|[ren ξ] by apply closed_unaffectedh.
have htt: [ ⊢ t.|[ren ξ] :- U0 ] by apply has_type_hsubst_0.
have hat: allzbb t.|[ren ξ].
{ apply (@allzbb_hsubst _ ids).
by asimpl. }
have hbt: box_rel neutral t.|[ren ξ] by apply box_rel_preserved_ren.
split.
- apply ih=>//.
rewrite weight_hsubst.
simpl in hw.
by lia.
- apply ih.
+ have e: weight t.|[ren ξ] = weight t by apply weight_hsubst.
have hwn: weight (neu t.|[ren ξ]) <= weight t.|[ren ξ] by apply weight_neu.
simpl in hw.
by lia.
+ by apply closed_sneu.
+ by apply has_type_neu.
+ by apply allzbb_neu.
+ by apply box_rel_preserved_neu. }
(* case {TApp s T} *)
{ move=> s T U hw /closed_tapp hc hty /= ha hb.
inv hb.
inv hty.
have ns: NEU (TArr U) s by apply ih.
by apply ns. }
(* case {Lam s U} *)
{ move=> s U V /= hw hc hty ha hb.
inv hb.
inv hty.
rewrite /NEU/= => t hct htt hst.
apply logical_relation_lemma_proj2.
- move=> l hl hcl htl.
have->: App (Lam s U) t ∘ l = Lam s U ∘ (R t :: l) by [].
rewrite /neutral=> f hf.
apply eval_move_stack_right in hf.
inv hf.
have hcs: closed s.[Box t/].
{ apply fv1; by [apply closed_lam in hc|apply closed_box]. }
have hts: [ ⊢ s.[Box t/] :- V0 ].
{ apply has_type_beta with U=>//; by [apply closed_box|constructor]. }
have ns: NEU V0 s.[Box t/].
{ apply ih=>//.
- have e := weight_subst_box 0 s t.
rewrite upn0 in e.
by rewrite -e.
- by apply allzbb_subst_var.
- by apply box_rel_preserved_subst0 with U. }
apply: (logical_relation_lemma_proj1 ns (l:=l))=>//.
by apply eval_move_stack_left.
- apply ty_app with U=>//.
by constructor. }
(* case {Imp s f} *)
{ move=> s f U hw /closed_imp hc hty /= ha hb.
inv hb.
inv hty.
have ns: NEU Void s by apply ih.
move=> g hg.
inv hg.
apply valid_weak0.
by apply ns. }
(* case {TLam s} *)
{ move=> s U /= hw hc hty ha hb.
inv hb.
inv hty.
rewrite /NEU/= => S.
apply logical_relation_lemma_proj2.
- move=> l hl hcl htl.
have->: TApp (TLam s) S ∘ l = TLam s ∘ (T S :: l) by [].
rewrite /neutral=> f hf.
apply eval_move_stack_right in hf.
inv hf.
have hcs: closed s.|[S/] by apply closed_unaffectedh, closed_tlam.
have hts: [ ⊢ s.|[S/] :- U0 ].
by apply has_type_hsubst1.
have ns: NEU U0 s.|[S/].
{ apply ih=>//.
- by rewrite weight_hsubst; lia.
- apply (@allzbb_hsubst _ ids). by asimpl.
- by apply box_rel_preserved_hsubst0 with empty_ctx U0 1 1. }
apply: (logical_relation_lemma_proj1 ns (l:=l))=>//.
by apply eval_move_stack_left.
- apply ty_tapp; by [apply fv_plage_eq|apply ty_tlam]. }
(* case {TAll s} *)
{ move=> s U /= hw hc hty ha hb.
inv hb.
have hU: U = Void by inv hty.
rewrite hU in hty *.
have hts: [ ⊢ s :- Void ].
by apply has_type_lower_1; inv hty.
have ns: NEU Void s by apply ih=>//; apply closed_tall.
rewrite /NEU/= => f hf.
inv hf.
apply valid_all_intro.
by apply ns. }
(* case {Neu s} *)
{ move=> s U /= hw /closed_neu hc hty ha hb.
inv hb.
have hts: [ ⊢ s :- U ] by inv hty.
have nsn: NEU U (neu s).
{ apply ih=>//.
- have:= weight_neu s.
simpl in hw.
by lia.
- by apply closed_sneu.
- by apply has_type_neu.
- by apply allzbb_neu.
- by apply box_rel_preserved_neu. }
have hcn: closed (neu s) by apply closed_sneu.
have htn: [ ⊢ neu s :- U ] by apply has_type_neu.
apply logical_relation_lemma_proj2=>[l hl hcl htl|//].
rewrite /neutral=> f hf.
apply eval_move_stack_right in hf.
inv hf.
apply: (logical_relation_lemma_proj1 nsn (l:=l))=>//.
by apply eval_move_stack_left. }
(* case {Box s} *)
{ move=> s U hw hc hty /= _ hb.
have[V [hcs [hts hls]]] := box_rel_box_ids hb.
have e: V = U.
{ inv hty. by apply has_type_det with empty_ctx 0 0 s. }
rewrite e in hts hls.
apply logical_relation_lemma_proj2=>[l hl hcl htl|//].
move=> f hf.
apply eval_move_stack_right in hf.
inv hf.
apply: (logical_relation_lemma_proj1 (proj1 hls) (l:=l))=>//.
by apply eval_move_stack_left. }
}
Qed.
Lemma neuneu2 :
forall r U,
closed (neu r) -> [ ⊢ r :- U ] ->
box_rel neutral (neu r).
Proof.
(* We prove this lemma by induction over depth r. *)
have:
forall n r U,
depth r <= n ->
closed (neu r) -> [ ⊢ r :- U ] ->
box_rel neutral (neu r).
(* The latter generalization subsumes the lemma. *)
2: { move=> h r U hc ht. by apply (h (depth r) r U). }
elim=>[r U hd|n ih].
(* case {0} *)
{ move=> _ _.
apply box_rel_nobox, mem_box_depth.
rewrite -depth_neu.
by lia. }
(* case {n.+1} *)
{ move=> r U hd hc ht.
have htn: [ ⊢ neu r :- U ] by apply has_type_neu.
have ss: forall s, directly_box s (neu r) -> s = neu s.
{ move=>*. by apply directly_box_neu_idempotent with r. }
apply unfold_box_rel with empty_ctx U 0 0=>// s V hdb hts ξ.
have hcs: closed s by apply directly_box_closed with (neu r) U empty_ctx 0 0.
have hds: depth s <= n.
{ apply directly_box_depth with (neu r)=>//.
by rewrite -depth_neu. }
have hcsξ: closed s.|[ren ξ] by apply closed_unaffectedh.
have htsξ: [ ⊢ s.|[ren ξ] :- V ] by apply has_type_hsubst_0.
have hsξ: s.|[ren ξ] = neu s.|[ren ξ].
{ rewrite {1}(ss _ hdb). by rewrite -neu_hsubst_comm. }
have hbs: box_rel neutral s.|[ren ξ].
{ rewrite hsξ.
apply ih with (U := V)=>//.
- by rewrite depth_hsubst.
- by rewrite -hsξ. }
split.
- apply neuneu=>//.
rewrite hsξ.
by apply allzbb_neu.
- apply neuneu=>//.
+ by apply closed_sneu.
+ by apply has_type_neu.
+ by apply allzbb_neu.
+ by apply box_rel_preserved_neu. }
Qed.
forall f,
eval s [::] f ->
||- f.
Definition NEU U := logrel neutral U.
Lemma neuneu :
forall r U,
closed r -> [ ⊢ r :- U ] ->
allzbb r ->
box_rel neutral r -> NEU U r.
Proof.
(* We proceed as in Theorem 3.2, by proving the neutrality of any closed recipe Υ,
where 0 only occurs inside angle brackets
and all directly boxed subrecipes are strongly neutral. *)
(* We prove this lemma by induction over the weight r. *)
have:
forall n r U,
weight r <= n ->
closed r -> [ ⊢ r :- U ] ->
allzbb r ->
box_rel neutral r -> NEU U r.
(* The latter generalization subsumes the lemma. *)
2: { move=> h r U hc ht ha hb. by apply (h (weight r) r U). }
elim=>[r U hw|n ih].
(* case {0} *)
{ exfalso. have := weight_pos r. by lia. }
(* case {n.+1} *)
{ case.
(* case {Var x} *)
{ by move=> >? /closed_ids. }
(* case {Zero} *)
{ by move=> U ??? []. }
(* case {Top} *)
{ move=> U ?? hty /= _ _.
inv hty.
rewrite /NEU/= => f h. inv h. exact valid_top0. }
(* case {And s t} *)
{ move=> s t U hw /closed_and [hc1 hc2] hty /= [ha1 ha2] hb.
inv hb.
have hts: [ ⊢ s :- U ] by inv hty.
have htt: [ ⊢ t :- U ] by inv hty.
have ns: NEU U s by apply ih=>//; try (simpl in hw; lia).
have nt: NEU U t by apply ih=>//; try (simpl in hw; lia).
apply logical_relation_lemma_proj2=>[l hl hcl htl|//].
rewrite /neutral=> f hf.
apply eval_move_stack_right in hf.
inv hf.
apply valid_and.
- apply: (logical_relation_lemma_proj1 ns (l:=l))=>//.
by apply eval_move_stack_left.
- apply: (logical_relation_lemma_proj1 nt (l:=l))=>//.
by apply eval_move_stack_left. }
(* case {App s t} *)
{ move=> s t U hw /closed_app [hc1 hc2] hty /= [ha1 ha2] hb.
inv hb.
inv hty.
have ns: NEU (Arr U0 U) s by apply ih=>//; try (simpl in hw; lia).
apply ns=>// ξ.
have hct: closed t.|[ren ξ] by apply closed_unaffectedh.
have htt: [ ⊢ t.|[ren ξ] :- U0 ] by apply has_type_hsubst_0.
have hat: allzbb t.|[ren ξ].
{ apply (@allzbb_hsubst _ ids).
by asimpl. }
have hbt: box_rel neutral t.|[ren ξ] by apply box_rel_preserved_ren.
split.
- apply ih=>//.
rewrite weight_hsubst.
simpl in hw.
by lia.
- apply ih.
+ have e: weight t.|[ren ξ] = weight t by apply weight_hsubst.
have hwn: weight (neu t.|[ren ξ]) <= weight t.|[ren ξ] by apply weight_neu.
simpl in hw.
by lia.
+ by apply closed_sneu.
+ by apply has_type_neu.
+ by apply allzbb_neu.
+ by apply box_rel_preserved_neu. }
(* case {TApp s T} *)
{ move=> s T U hw /closed_tapp hc hty /= ha hb.
inv hb.
inv hty.
have ns: NEU (TArr U) s by apply ih.
by apply ns. }
(* case {Lam s U} *)
{ move=> s U V /= hw hc hty ha hb.
inv hb.
inv hty.
rewrite /NEU/= => t hct htt hst.
apply logical_relation_lemma_proj2.
- move=> l hl hcl htl.
have->: App (Lam s U) t ∘ l = Lam s U ∘ (R t :: l) by [].
rewrite /neutral=> f hf.
apply eval_move_stack_right in hf.
inv hf.
have hcs: closed s.[Box t/].
{ apply fv1; by [apply closed_lam in hc|apply closed_box]. }
have hts: [ ⊢ s.[Box t/] :- V0 ].
{ apply has_type_beta with U=>//; by [apply closed_box|constructor]. }
have ns: NEU V0 s.[Box t/].
{ apply ih=>//.
- have e := weight_subst_box 0 s t.
rewrite upn0 in e.
by rewrite -e.
- by apply allzbb_subst_var.
- by apply box_rel_preserved_subst0 with U. }
apply: (logical_relation_lemma_proj1 ns (l:=l))=>//.
by apply eval_move_stack_left.
- apply ty_app with U=>//.
by constructor. }
(* case {Imp s f} *)
{ move=> s f U hw /closed_imp hc hty /= ha hb.
inv hb.
inv hty.
have ns: NEU Void s by apply ih.
move=> g hg.
inv hg.
apply valid_weak0.
by apply ns. }
(* case {TLam s} *)
{ move=> s U /= hw hc hty ha hb.
inv hb.
inv hty.
rewrite /NEU/= => S.
apply logical_relation_lemma_proj2.
- move=> l hl hcl htl.
have->: TApp (TLam s) S ∘ l = TLam s ∘ (T S :: l) by [].
rewrite /neutral=> f hf.
apply eval_move_stack_right in hf.
inv hf.
have hcs: closed s.|[S/] by apply closed_unaffectedh, closed_tlam.
have hts: [ ⊢ s.|[S/] :- U0 ].
by apply has_type_hsubst1.
have ns: NEU U0 s.|[S/].
{ apply ih=>//.
- by rewrite weight_hsubst; lia.
- apply (@allzbb_hsubst _ ids). by asimpl.
- by apply box_rel_preserved_hsubst0 with empty_ctx U0 1 1. }
apply: (logical_relation_lemma_proj1 ns (l:=l))=>//.
by apply eval_move_stack_left.
- apply ty_tapp; by [apply fv_plage_eq|apply ty_tlam]. }
(* case {TAll s} *)
{ move=> s U /= hw hc hty ha hb.
inv hb.
have hU: U = Void by inv hty.
rewrite hU in hty *.
have hts: [ ⊢ s :- Void ].
by apply has_type_lower_1; inv hty.
have ns: NEU Void s by apply ih=>//; apply closed_tall.
rewrite /NEU/= => f hf.
inv hf.
apply valid_all_intro.
by apply ns. }
(* case {Neu s} *)
{ move=> s U /= hw /closed_neu hc hty ha hb.
inv hb.
have hts: [ ⊢ s :- U ] by inv hty.
have nsn: NEU U (neu s).
{ apply ih=>//.
- have:= weight_neu s.
simpl in hw.
by lia.
- by apply closed_sneu.
- by apply has_type_neu.
- by apply allzbb_neu.
- by apply box_rel_preserved_neu. }
have hcn: closed (neu s) by apply closed_sneu.
have htn: [ ⊢ neu s :- U ] by apply has_type_neu.
apply logical_relation_lemma_proj2=>[l hl hcl htl|//].
rewrite /neutral=> f hf.
apply eval_move_stack_right in hf.
inv hf.
apply: (logical_relation_lemma_proj1 nsn (l:=l))=>//.
by apply eval_move_stack_left. }
(* case {Box s} *)
{ move=> s U hw hc hty /= _ hb.
have[V [hcs [hts hls]]] := box_rel_box_ids hb.
have e: V = U.
{ inv hty. by apply has_type_det with empty_ctx 0 0 s. }
rewrite e in hts hls.
apply logical_relation_lemma_proj2=>[l hl hcl htl|//].
move=> f hf.
apply eval_move_stack_right in hf.
inv hf.
apply: (logical_relation_lemma_proj1 (proj1 hls) (l:=l))=>//.
by apply eval_move_stack_left. }
}
Qed.
Lemma neuneu2 :
forall r U,
closed (neu r) -> [ ⊢ r :- U ] ->
box_rel neutral (neu r).
Proof.
(* We prove this lemma by induction over depth r. *)
have:
forall n r U,
depth r <= n ->
closed (neu r) -> [ ⊢ r :- U ] ->
box_rel neutral (neu r).
(* The latter generalization subsumes the lemma. *)
2: { move=> h r U hc ht. by apply (h (depth r) r U). }
elim=>[r U hd|n ih].
(* case {0} *)
{ move=> _ _.
apply box_rel_nobox, mem_box_depth.
rewrite -depth_neu.
by lia. }
(* case {n.+1} *)
{ move=> r U hd hc ht.
have htn: [ ⊢ neu r :- U ] by apply has_type_neu.
have ss: forall s, directly_box s (neu r) -> s = neu s.
{ move=>*. by apply directly_box_neu_idempotent with r. }
apply unfold_box_rel with empty_ctx U 0 0=>// s V hdb hts ξ.
have hcs: closed s by apply directly_box_closed with (neu r) U empty_ctx 0 0.
have hds: depth s <= n.
{ apply directly_box_depth with (neu r)=>//.
by rewrite -depth_neu. }
have hcsξ: closed s.|[ren ξ] by apply closed_unaffectedh.
have htsξ: [ ⊢ s.|[ren ξ] :- V ] by apply has_type_hsubst_0.
have hsξ: s.|[ren ξ] = neu s.|[ren ξ].
{ rewrite {1}(ss _ hdb). by rewrite -neu_hsubst_comm. }
have hbs: box_rel neutral s.|[ren ξ].
{ rewrite hsξ.
apply ih with (U := V)=>//.
- by rewrite depth_hsubst.
- by rewrite -hsξ. }
split.
- apply neuneu=>//.
rewrite hsξ.
by apply allzbb_neu.
- apply neuneu=>//.
+ by apply closed_sneu.
+ by apply has_type_neu.
+ by apply allzbb_neu.
+ by apply box_rel_preserved_neu. }
Qed.
Any neutralized closed recipe neu s is neutral.
Theorem neuneug :
forall r U,
closed r -> [ ⊢ r :- U ] ->
NEU U (neu r).
Proof.
move=> r U hc ht.
apply neuneu=>//.
- by apply closed_sneu.
- by apply has_type_neu.
- by apply allzbb_neu.
- apply neuneu2 with U=>//.
by apply closed_sneu.
Qed.
(* Print Assumptions neuneug. (* only axioms *) *)
forall r U,
closed r -> [ ⊢ r :- U ] ->
NEU U (neu r).
Proof.
move=> r U hc ht.
apply neuneu=>//.
- by apply closed_sneu.
- by apply has_type_neu.
- by apply allzbb_neu.
- apply neuneu2 with U=>//.
by apply closed_sneu.
Qed.
(* Print Assumptions neuneug. (* only axioms *) *)
Definition entails s t :=
forall f g,
eval s [::] f ->
eval t [::] g ->
f ||- g.
Lemma entails_toptop :
entails Top Top.
Proof.
move=> > h1 h2. inv h1. inv h2. tac_valid.
Qed.
Definition ENT U := logrel2 entails U.
Lemma b1 :
forall s t U,
closed s -> [ ⊢ s :- U ] ->
closed t -> [ ⊢ t :- U ] ->
box_rel2 entails s t ->
ENT U s t.
Proof.
(* We prove this lemma by induction over the weight r. *)
have:
forall n s t U,
weight s <= n ->
closed s -> [ ⊢ s :- U ] ->
closed t -> [ ⊢ t :- U ] ->
box_rel2 entails s t ->
ENT U s t.
(* The latter generalization subsumes the lemma. *)
2: { move=>h s?? ?? ?? hb. by apply (h (weight s)). }
elim=>[s t U hw|n ih].
(* case {0} *)
{ exfalso. have := weight_pos s. by lia. }
(* case {n.+1} *)
{ case.
(* case {Var x} *)
{ by move=> >? /closed_ids. }
(* case {Zero} *)
{ move=> t U /= _ _ h.
inv h=> _ ht hb.
inv hb.
rewrite /ENT/=/entails/= => f g hf hg.
inv hf. inv hg. valid_trivial. }
(* case {Top} *)
{ move=> t U /= _ _ h.
inv h=> _ ht hb.
inv hb.
rewrite /ENT/=/entails/= => f g hf hg.
inv hf. inv hg. valid_trivial. }
(* case {And} *)
{ move=> s t u U hw hc hty1 hcu hty2 hb.
inv hb.
have[hc1 hc2]: closed s /\ closed t by apply closed_and.
have[hc3 hc4]: closed s2 /\ closed t2 by apply closed_and.
have hts: [ ⊢ s :- U ] by inv hty1.
have htt: [ ⊢ t :- U ] by inv hty1.
have hts2: [ ⊢ s2 :- U ] by inv hty2.
have htt2: [ ⊢ t2 :- U ] by inv hty2.
have ih1: ENT U s s2 by apply ih=>//; try (simpl in hw; lia).
have ih2: ENT U t t2 by apply ih=>//; try (simpl in hw; lia).
apply logical_relation_lemma2_proj2=>// l1 l2 hl ha1 ha2 f g hf hg.
apply eval_move_stack_right in hf.
apply eval_move_stack_right in hg.
inv hf. inv hg.
apply valid_and_and_intro.
+ have: ENT Void (s ∘ l1) (s2 ∘ l2).
{ by apply: (logical_relation_lemma2_proj1 ih1). }
apply; by apply eval_move_stack_left.
+ have: ENT Void (t ∘ l1) (t2 ∘ l2).
{ by apply: (logical_relation_lemma2_proj1 ih2). }
apply; by apply eval_move_stack_left. }
(* case {App} *)
{ move=> s t u U hw /closed_app [hc1 hc2] hty1 hcu hty2 hb.
inv hb.
inv hty1.
inv hty2.
move: hcu=> /closed_app [hc3 hc4].
have hU: U0 = U1.
{ apply box_rel2_type_det with
(P:=entails) (s:=t) (t:=t2) (Γ:=empty_ctx) (a:=0) (b:=0)=>//. }
subst U1.
have h: ENT (Arr U0 U) s s2 by apply ih=>//; try (simpl in hw; lia).
apply h=>// ξ.
have hct: closed t.|[ren ξ] by apply closed_unaffectedh.
have hct2: closed t2.|[ren ξ] by apply closed_unaffectedh.
have htt: [ ⊢ t.|[ren ξ] :- U0 ] by apply has_type_hsubst_0.
have htt2: [ ⊢ t2.|[ren ξ] :- U0 ] by apply has_type_hsubst_0.
have hbt: box_rel2 entails t.|[ren ξ] t2.|[ren ξ] by apply box_rel2_preserved_ren.
split.
- apply ih=>//.
rewrite weight_hsubst.
simpl in hw.
by lia.
- apply ih=>//.
+ have e: weight t.|[ren ξ] = weight t by apply weight_hsubst.
have hwn: weight (neu t.|[ren ξ]) <= weight t.|[ren ξ] by apply weight_neu.
simpl in hw.
by lia.
+ by apply closed_sneu.
+ by apply has_type_neu.
+ by apply closed_sneu.
+ by apply has_type_neu.
+ by apply box_rel2_preserved_neu. }
(* case {TApp} *)
{ move=> s T u U hw /closed_tapp hc1 hty1 hcu hty2 hb.
inv hb.
inv hty1.
inv hty2.
move: hcu=> /closed_tapp hc2.
have h: ENT (TArr U) s t by apply ih=>//; try (simpl in hw; lia).
by apply h. }
(* case {Lam} *)
{ move=> s U u W hw hc1 hty1 hc2 hty2 hb.
inv hb.
inv hty1.
inv hty2.
move=> u v hcu htu hcv htv huv.
apply logical_relation_lemma2_proj2;
try (by apply closed_app);
try (by apply ty_app with U=>//; constructor).
have h_1: closed s.[Box u/].
{ apply fv1; by [apply closed_lam in hc1|apply closed_box]. }
have h_3: [ ⊢ s.[Box u/] :- V ].
{ apply has_type_beta with U=>//; by [apply closed_box|constructor]. }
have h_4: closed t.[Box v/].
{ apply fv1; by [apply closed_lam in hc2|apply closed_box]. }
have h_6: [ ⊢ t.[Box v/] :- V ].
{ apply has_type_beta with U=>//; by [apply closed_box|constructor]. }
have hsutv: box_rel2 entails s.[Box u/] t.[Box v/].
{ by apply box_rel2_preserved_subst0 with U. }
have hw2: weight s.[Box u/] <= n.
{ have e := weight_subst_box 0 s u.
rewrite upn0 in e.
rewrite -e.
simpl in hw.
by lia. }
specialize (ih s.[Box u/] t.[Box v/] V hw2 h_1 h_3 h_4 h_6 hsutv).
move=> l1 l2 hl ha1 ha2 /=.
have->: App (Lam s U) u ∘ l1 = Lam s U ∘ (R u :: l1) by [].
have->: App (Lam t U) v ∘ l2 = Lam t U ∘ (R v :: l2) by [].
move=> f g hf hg.
apply eval_move_stack_right in hf.
apply eval_move_stack_right in hg.
inv hf. inv hg.
apply: (logical_relation_lemma2_proj1 ih (l1:=l1) (l2:=l2))=>//.
by apply eval_move_stack_left.
by apply eval_move_stack_left. }
(* case {Imp} *)
{ move=> s f t U hw /closed_imp hc1 hty1 hct hty2 hb.
inv hb.
inv hty1.
inv hty2.
move: hct=> /closed_imp hc2.
have {}ih: ENT Void s t0 by apply ih.
move=> f1 f2 hf1 hf2. inv hf1. inv hf2.
apply valid_imp_imp_split.
by apply ih. }
(* case {TLam} *)
{ move=> s u V /= hw hc1 hty1 hc2 hty2 hb.
inv hb.
inv hty1.
inv hty2.
rewrite /ENT/= => S.
apply logical_relation_lemma2_proj2;
try (by apply closed_tapp);
try (by apply ty_tapp; [apply fv_plage_eq|apply ty_tlam]).
have ?: closed s.|[S/] by apply closed_unaffectedh, closed_tlam.
have ?: closed t.|[S/] by apply closed_unaffectedh, closed_tlam.
have hts: [ ⊢ s.|[S/] :- U ].
by apply has_type_hsubst1.
have htt: [ ⊢ t.|[S/] :- U ].
by apply has_type_hsubst1.
have ih1: ENT U s.|[S/] t.|[S/].
{ apply ih=>//.
- by rewrite weight_hsubst.
- by apply box_rel2_preserved_hsubst0 with empty_ctx U U 1 1. }
move=> l1 l2 hl ha1 ha2.
have->: TApp (TLam s) S ∘ l1 = TLam s ∘ (T S :: l1) by [].
have->: TApp (TLam t) S ∘ l2 = TLam t ∘ (T S :: l2) by [].
move=> f g hf hg.
apply eval_move_stack_right in hf.
apply eval_move_stack_right in hg.
inv hf. inv hg.
apply: (logical_relation_lemma2_proj1 ih1 (l1:=l1) (l2:=l2))=>//.
by apply eval_move_stack_left.
by apply eval_move_stack_left. }
(* case {TAll} *)
{ move=> s u V /= hw hc1 hty1 hc2 hty2 hb.
inv hb.
have hV: V = Void by inv hty1.
rewrite hV in hty1 hty2 *.
have hts: [ ⊢ s :- Void ].
by apply has_type_lower_1; inv hty1.
have htt: [ ⊢ t :- Void ].
by apply has_type_lower_1; inv hty2.
have hcs: closed s by apply closed_tall.
have hct: closed t by apply closed_tall.
have ih1: ENT Void s t by apply ih.
rewrite /ENT/=/entails/= => f g hf hg.
inv hf. inv hg.
apply valid_all_mono.
by apply ih1. }
(* case {Neu} *)
{ move=> s u U hw hc hty1 hcu hty2 hb.
inv hb.
have hc1: closed s by apply closed_neu.
have hc2: closed t by apply closed_neu.
have hts: [ ⊢ s :- U ] by inv hty1.
have htt: [ ⊢ t :- U ] by inv hty2.
have hcn: closed (neu s) by apply closed_sneu.
have htn: [ ⊢ neu s :- U ] by apply has_type_neu.
have hcn2: closed (neu t) by apply closed_sneu.
have htn2: [ ⊢ neu t :- U ] by apply has_type_neu.
have ih1: ENT U (neu s) (neu t).
{ apply ih=>//.
- have:= weight_neu s.
simpl in hw.
by lia.
- by apply box_rel2_preserved_neu. }
apply logical_relation_lemma2_proj2=>// l1 l2 hl ha1 ha2 f g hf hg.
apply eval_move_stack_right in hf.
apply eval_move_stack_right in hg.
inv hf. inv hg.
apply: (logical_relation_lemma2_proj1 ih1 (l1:=l1) (l2:=l2))=>//.
by apply eval_move_stack_left.
by apply eval_move_stack_left. }
(* case {Box} *)
{ move=> s u U hw hc1 hty1 hc2 hty2 hb.
inv hb.
have hb': box_rel2 entails (Box s) (Box t) by apply box_rel2_box with U0.
have[V [hcs [hts [hct [htt hst]]]]] := box_rel2_box_ids hb'.
have e: V = U.
{ inv hty1.
by apply has_type_det with empty_ctx 0 0 s. }
rewrite e in hts htt hst.
apply logical_relation_lemma2_proj2=>// l1 l2 hl ha1 ha2 f g hf hg.
apply eval_move_stack_right in hf.
apply eval_move_stack_right in hg.
inv hf. inv hg.
apply: (logical_relation_lemma2_proj1 (proj1 hst) (l1:=l1) (l2:=l2))=>//.
by apply eval_move_stack_left.
by apply eval_move_stack_left. } }
Qed.
TOPLAS: Corr 3.4.
Theorem entails_refl r U :
closed r -> [ ⊢ r :- U ] ->
ENT U r r.
Proof.
have:
forall n r Γ U a b,
depth r <= n ->
[ Γ, a, b ⊢ r :- U ] ->
box_rel2 entails r r.
2: { move=> h hc ht.
apply b1=>//.
by apply (h (depth r) r empty_ctx U 0 0). }
clear r U.
elim=>[r Γ U a b hd _|n ih].
{ apply box_rel2_nobox, mem_box_depth.
have := depth_nonneg r.
by lia. }
move=> r.
elim: r=>/=.
- move=> > _ _.
by constructor.
- move=> > _ _.
by constructor.
- move=> > _ _.
by constructor.
- move=> s h1 t h2 Γ U a b hd hty.
inv hty.
constructor; by [apply h1 with Γ U a b; [lia|]|apply h2 with Γ U a b; [lia|]].
- move=> s h1 t h2 Γ U a b hd hty.
inv hty.
constructor; by [apply h1 with Γ (Arr U0 U) a b; [lia|]|apply h2 with Γ U0 a b; [lia|]].
- move=> s h1 S Γ U a b hd hty.
inv hty.
constructor.
by apply h1 with Γ (TArr U) a b.
- move=> s h1 W Γ U a b hd hty.
inv hty.
constructor.
by apply h1 with (W .: Γ) V a b.
- move=> s h1 f Γ U a b hd hty.
inv hty.
constructor.
by apply h1 with Γ Void a b.
- move=> s h1 Γ U a b hd hty.
inv hty.
constructor.
by apply h1 with Γ U0 a.+1 b.+1.
- move=> s h1 Γ U a b hd hty.
inv hty.
constructor.
by apply h1 with Γ Void a.+1 b.+1.
- move=> s h1 Γ U a b hd hty.
inv hty.
constructor.
by apply h1 with Γ U a b.
- move=> s _ Γ U a b hd hty.
inv hty.
have hts: [ ⊢ s :- U ].
{ apply (has_type_lower_b (b:=b))=>//.
by apply closed_has_ty_contr with Γ. }
apply box_rel2_box with U=>// ξ.
have hcξ: closed s.|[ren ξ] by apply closed_unaffectedh.
have htξ: [ ⊢ s.|[ren ξ] :- U ] by apply has_type_hsubst_0.
have hbξ: box_rel2 entails s.|[ren ξ] s.|[ren ξ].
{ apply ih with (Γ := empty_ctx) (U := U) (a := 0) (b := 0)=>//.
rewrite depth_hsubst.
by lia. }
split.
+ by apply b1.
+ apply b1=>//; by [apply closed_sneu|apply has_type_neu|apply box_rel2_preserved_neu].
Qed.
Lemma stack_rel_entails_refl2 l U :
aligned l U ->
stack_rel2 entails U l l.
Proof.
elim: U l=> [|U h1 V h2|V h1] l [hcl htl]; inv hcl; inv htl.
- by constructor.
- constructor; last by apply h2; split.
move=> ξ.
have hc: closed r.|[ren ξ] by apply closed_unaffectedh.
have ht: [ ⊢ r.|[ren ξ] :- U ] by apply has_type_hsubst_0.
split.
+ by apply entails_refl.
+ apply entails_refl; by [apply closed_sneu|apply has_type_neu].
- constructor.
by apply h1; split.
Qed.
closed r -> [ ⊢ r :- U ] ->
ENT U r r.
Proof.
have:
forall n r Γ U a b,
depth r <= n ->
[ Γ, a, b ⊢ r :- U ] ->
box_rel2 entails r r.
2: { move=> h hc ht.
apply b1=>//.
by apply (h (depth r) r empty_ctx U 0 0). }
clear r U.
elim=>[r Γ U a b hd _|n ih].
{ apply box_rel2_nobox, mem_box_depth.
have := depth_nonneg r.
by lia. }
move=> r.
elim: r=>/=.
- move=> > _ _.
by constructor.
- move=> > _ _.
by constructor.
- move=> > _ _.
by constructor.
- move=> s h1 t h2 Γ U a b hd hty.
inv hty.
constructor; by [apply h1 with Γ U a b; [lia|]|apply h2 with Γ U a b; [lia|]].
- move=> s h1 t h2 Γ U a b hd hty.
inv hty.
constructor; by [apply h1 with Γ (Arr U0 U) a b; [lia|]|apply h2 with Γ U0 a b; [lia|]].
- move=> s h1 S Γ U a b hd hty.
inv hty.
constructor.
by apply h1 with Γ (TArr U) a b.
- move=> s h1 W Γ U a b hd hty.
inv hty.
constructor.
by apply h1 with (W .: Γ) V a b.
- move=> s h1 f Γ U a b hd hty.
inv hty.
constructor.
by apply h1 with Γ Void a b.
- move=> s h1 Γ U a b hd hty.
inv hty.
constructor.
by apply h1 with Γ U0 a.+1 b.+1.
- move=> s h1 Γ U a b hd hty.
inv hty.
constructor.
by apply h1 with Γ Void a.+1 b.+1.
- move=> s h1 Γ U a b hd hty.
inv hty.
constructor.
by apply h1 with Γ U a b.
- move=> s _ Γ U a b hd hty.
inv hty.
have hts: [ ⊢ s :- U ].
{ apply (has_type_lower_b (b:=b))=>//.
by apply closed_has_ty_contr with Γ. }
apply box_rel2_box with U=>// ξ.
have hcξ: closed s.|[ren ξ] by apply closed_unaffectedh.
have htξ: [ ⊢ s.|[ren ξ] :- U ] by apply has_type_hsubst_0.
have hbξ: box_rel2 entails s.|[ren ξ] s.|[ren ξ].
{ apply ih with (Γ := empty_ctx) (U := U) (a := 0) (b := 0)=>//.
rewrite depth_hsubst.
by lia. }
split.
+ by apply b1.
+ apply b1=>//; by [apply closed_sneu|apply has_type_neu|apply box_rel2_preserved_neu].
Qed.
Lemma stack_rel_entails_refl2 l U :
aligned l U ->
stack_rel2 entails U l l.
Proof.
elim: U l=> [|U h1 V h2|V h1] l [hcl htl]; inv hcl; inv htl.
- by constructor.
- constructor; last by apply h2; split.
move=> ξ.
have hc: closed r.|[ren ξ] by apply closed_unaffectedh.
have ht: [ ⊢ r.|[ren ξ] :- U ] by apply has_type_hsubst_0.
split.
+ by apply entails_refl.
+ apply entails_refl; by [apply closed_sneu|apply has_type_neu].
- constructor.
by apply h1; split.
Qed.
TOPLAS: Lemma 3.5.
Theorem entails_trans r s t U :
closed r -> [ ⊢ r :- U ] ->
closed s -> [ ⊢ s :- U ] ->
closed t -> [ ⊢ t :- U ] ->
ENT U r s ->
ENT U s t ->
ENT U r t.
Proof.
move=> hr1 hr3 hs1 hs3 ht1 ht3 h1 h2.
apply logical_relation_lemma2_proj2=>// l1 l2 hl ha1 ha2 f g hf hg.
have cs: complete (s ∘ l2) by apply aligned_complete with U.
have[mid hmid] := eval_def cs.
have hl2 := stack_rel_entails_refl2 ha2.
apply valid_cut with mid.
by apply (logical_relation_lemma2_proj1 h1 (l1:=l1) (l2:=l2))=>//.
by apply (logical_relation_lemma2_proj1 h2 (l1:=l2) (l2:=l2))=>//.
Qed.
closed r -> [ ⊢ r :- U ] ->
closed s -> [ ⊢ s :- U ] ->
closed t -> [ ⊢ t :- U ] ->
ENT U r s ->
ENT U s t ->
ENT U r t.
Proof.
move=> hr1 hr3 hs1 hs3 ht1 ht3 h1 h2.
apply logical_relation_lemma2_proj2=>// l1 l2 hl ha1 ha2 f g hf hg.
have cs: complete (s ∘ l2) by apply aligned_complete with U.
have[mid hmid] := eval_def cs.
have hl2 := stack_rel_entails_refl2 ha2.
apply valid_cut with mid.
by apply (logical_relation_lemma2_proj1 h1 (l1:=l1) (l2:=l2))=>//.
by apply (logical_relation_lemma2_proj1 h2 (l1:=l2) (l2:=l2))=>//.
Qed.
TOPLAS: Lemma 3.6.
Theorem entails_36 s t U :
closed s -> [ ⊢ s :- U ] ->
closed t -> [ ⊢ t :- U ] ->
(forall l, aligned l U -> entails (s ∘ l) (t ∘ l)) ->
ENT U s t.
Proof.
move=> hs1 hs3 ht1 ht3 h.
apply logical_relation_lemma2_proj2=>// l1 l2 hl ha1 ha2.
have?: entails (s ∘ l2) (t ∘ l2) by apply h.
have?: entails (s ∘ l1) (s ∘ l2).
{ have hss: ENT U s s by apply entails_refl.
by apply: (logical_relation_lemma2_proj1 hss). }
have[??]:= aligned_closed_appl2 hs1 ha1 ha2.
have[??]:= aligned_closed_appl2 ht1 ha1 ha2.
have[??]:= aligned_type_void2 hs3 ha1 ha2.
have[??]:= aligned_type_void2 ht3 ha1 ha2.
have:= @entails_trans (s ∘ l1) (s ∘ l2) (t ∘ l2) Void.
by apply.
Qed.
Print Assumptions entails_36.
End Sem.
closed s -> [ ⊢ s :- U ] ->
closed t -> [ ⊢ t :- U ] ->
(forall l, aligned l U -> entails (s ∘ l) (t ∘ l)) ->
ENT U s t.
Proof.
move=> hs1 hs3 ht1 ht3 h.
apply logical_relation_lemma2_proj2=>// l1 l2 hl ha1 ha2.
have?: entails (s ∘ l2) (t ∘ l2) by apply h.
have?: entails (s ∘ l1) (s ∘ l2).
{ have hss: ENT U s s by apply entails_refl.
by apply: (logical_relation_lemma2_proj1 hss). }
have[??]:= aligned_closed_appl2 hs1 ha1 ha2.
have[??]:= aligned_closed_appl2 ht1 ha1 ha2.
have[??]:= aligned_type_void2 hs3 ha1 ha2.
have[??]:= aligned_type_void2 ht3 ha1 ha2.
have:= @entails_trans (s ∘ l1) (s ∘ l2) (t ∘ l2) Void.
by apply.
Qed.
Print Assumptions entails_36.
End Sem.