Rocoma.Recipes_joker
Open Scope valid_scope.
notations for the examples
Notation "◻" := Void (at level 0) : ty_scope.
Notation "U --> V" := (Arr U V) (at level 60, right associativity) : ty_scope.
Notation "\[ U ] s" := (Lam s U) (at level 60, right associativity, format "\[ U ] s") : ty_scope.
Notation "U --> V" := (Arr U V) (at level 60, right associativity) : ty_scope.
Notation "\[ U ] s" := (Lam s U) (at level 60, right associativity, format "\[ U ] s") : ty_scope.
Fixpoint c_len (U : type) :=
match U with
| Void => 0
| TArr V => c_len V
| Arr _ V => (c_len V).+1
end.
Numbers of term parameters
Fixpoint t_len (U : type) :=
match U with
| Void => 0
| TArr V => (t_len V).+1
| Arr _ V => t_len V
end.
see TOPLAS, Fig. 6
joker_abs z U acc
poses one binder per parameter of U and writes the conjunction acc at the bottom
each continuation parameter k : W adds its call ∀xs. k xs 0Ws to acc.
joker_call z W s tc
applies s to the parameters of W,
tc counting the term parameters left
z is the leaf of the nested jokers, Zero or Top (see Lemma neu_joker).
Fixpoint joker_abs (z : recipe) (U : type) (acc : recipe) : recipe :=
match U with
| Void => acc
| TArr V => TLam (joker_abs z V acc)
| Arr W V =>
\[ W ] (joker_abs z V (And acc
(fall (t_len W) (joker_call z W (Var (c_len V)) (t_len W)))))
end
with joker_call (z : recipe) (U : type) (s : recipe) (tc : nat) : recipe :=
match U with
| Void => s
| TArr V => joker_call z V (TApp s (TVar tc.-1)) tc.-1
| Arr W V => joker_call z V (App s (joker_abs z W z)) tc
end.
Definition joker U := joker_abs Zero U Zero.
Definition joker_all z W f :=
fall (t_len W) (joker_call z W f (t_len W)).
Eval compute in joker (TArr (◻ --> ◻ --> ◻)).
Eval compute in joker (TArr (TArr (TArr ((TArr Void) --> Void)))).
Eval compute in joker (TArr (◻ --> ◻) --> Void).
fall (t_len W) (joker_call z W f (t_len W)).
Eval compute in joker (TArr (◻ --> ◻ --> ◻)).
Eval compute in joker (TArr (TArr (TArr ((TArr Void) --> Void)))).
Eval compute in joker (TArr (◻ --> ◻) --> Void).
Closed in both sorts
Lemma fv_joker z U :
closed z ->
(forall acc n, fv (n + c_len U) acc -> fv n (joker_abs z U acc)) /\
(forall s tc n, fv n s -> fv n (joker_call z U s tc)).
Proof.
move=> *.
elim: U=> [|? [ih1 ih2] ? [ih3 ih4]|? [ih3 ih4]] /=.
- split=> > //.
by rewrite addn0.
- split=> *.
+ apply fv_lam, ih3, fv_and; split.
* by rewrite addSnnS.
* apply fv_fall, ih2, fv_var.
by lia.
+ apply ih4, fv_app; split=>//.
apply ih1.
by apply closed_fv.
- split=> *.
+ by apply fv_tlam, ih3.
+ by apply ih4, fv_tapp.
Qed.
Corollary closed_joker U :
closed (joker U).
Proof.
have hz: closed Zero by [].
by apply (fv_joker U hz).1.
Qed.
Lemma fvh_joker z U :
closedh z ->
(forall acc n,
fvh (n + t_len U) acc ->
fvh n (joker_abs z U acc)) /\
(forall s tc n,
t_len U <= tc -> tc <= n -> fvh n s ->
fvh n (joker_call z U s tc)).
Proof.
move=> *.
elim: U=> [|? [ih1 ih2] ? [ih3 ih4]|? [ih3 ih4]] /=.
- split=> > //.
by rewrite addn0.
- split=> *.
+ apply fvh_lam, ih3, fvh_and; split=>//.
apply fvh_fall, ih2=>//.
by lia.
+ apply ih4, fvh_app=>//; split=>//.
apply ih1.
by apply closedh_fvh.
- split=> *.
+ apply fvh_tlam, ih3.
by rewrite addSnnS.
+ apply ih4=>//; try by lia.
apply fvh_tapp; split=>//.
apply fv_tvar.
by lia.
Qed.
Corollary closedh_joker U :
closedh (joker U).
Proof.
have hz: closedh Zero by [].
by apply (fvh_joker U hz).1.
Qed.
closed z ->
(forall acc n, fv (n + c_len U) acc -> fv n (joker_abs z U acc)) /\
(forall s tc n, fv n s -> fv n (joker_call z U s tc)).
Proof.
move=> *.
elim: U=> [|? [ih1 ih2] ? [ih3 ih4]|? [ih3 ih4]] /=.
- split=> > //.
by rewrite addn0.
- split=> *.
+ apply fv_lam, ih3, fv_and; split.
* by rewrite addSnnS.
* apply fv_fall, ih2, fv_var.
by lia.
+ apply ih4, fv_app; split=>//.
apply ih1.
by apply closed_fv.
- split=> *.
+ by apply fv_tlam, ih3.
+ by apply ih4, fv_tapp.
Qed.
Corollary closed_joker U :
closed (joker U).
Proof.
have hz: closed Zero by [].
by apply (fv_joker U hz).1.
Qed.
Lemma fvh_joker z U :
closedh z ->
(forall acc n,
fvh (n + t_len U) acc ->
fvh n (joker_abs z U acc)) /\
(forall s tc n,
t_len U <= tc -> tc <= n -> fvh n s ->
fvh n (joker_call z U s tc)).
Proof.
move=> *.
elim: U=> [|? [ih1 ih2] ? [ih3 ih4]|? [ih3 ih4]] /=.
- split=> > //.
by rewrite addn0.
- split=> *.
+ apply fvh_lam, ih3, fvh_and; split=>//.
apply fvh_fall, ih2=>//.
by lia.
+ apply ih4, fvh_app=>//; split=>//.
apply ih1.
by apply closedh_fvh.
- split=> *.
+ apply fvh_tlam, ih3.
by rewrite addSnnS.
+ apply ih4=>//; try by lia.
apply fvh_tapp; split=>//.
apply fv_tvar.
by lia.
Qed.
Corollary closedh_joker U :
closedh (joker U).
Proof.
have hz: closedh Zero by [].
by apply (fvh_joker U hz).1.
Qed.
Neutralization: z becomes Top
Lemma neu_joker z U :
(forall acc, neu (joker_abs z U acc) = joker_abs (neu z) U (neu acc)) /\
(forall s tc, neu (joker_call z U s tc) = joker_call (neu z) U (neu s) tc).
Proof.
elim: U=> [|? [ih1 ih2] ? [ih3 ih4]|? [ih3 ih4]] /=.
- by split.
- split=> >.
+ by rewrite ih3 /= neu_fall ih2.
+ by rewrite ih4 /= ih1.
- split=> >.
+ by rewrite ih3.
+ by rewrite ih4.
Qed.
Corollary neu_joker_top U :
neu (joker U) = joker_abs Top U Top.
Proof.
by apply (neu_joker Zero U).1.
Qed.
Joker substitutions:
acc receives σ (at the bottom), calls are unnaffected.
Fixpoint subst_depth (U : type) (σ : var -> recipe) : var -> recipe :=
match U with
| Void => σ
| TArr V => subst_depth V (σ >>| ren (+1))
| Arr _ V => subst_depth V (up σ)
end.
Lemma subst_depth_var U σ k :
subst_depth U (upn k.+1 σ) (k + c_len U) = Var (k + c_len U).
Proof.
elim: U σ k => [|? _ ? ih|? ih] σ ? /=.
- by rewrite addn0 upn_k_sigma_x.
- rewrite fold_up_upn addnS -addSn.
by apply ih.
- asimpl.
rewrite upn_hcomp.
by apply ih.
Qed.
Lemma joker_subst z U :
closed z ->
(forall acc σ, (joker_abs z U acc).[σ] = joker_abs z U acc.[subst_depth U σ]) /\
(forall s tc σ, (joker_call z U s tc).[σ] = joker_call z U s.[σ] tc).
Proof.
move=> hz.
elim: U=> [|W [_ ih2] V [ih3 ih4]|V [ih3 ih4]] /=.
- by split.
- split=> [? σ|?? σ].
+ rewrite ih3 /= fall_subst ih2 /=.
have:= subst_depth_var V σ 0.
rewrite add0n /= => ->.
by asimpl.
+ have hc: closed (joker_abs z W z).
{ by apply (fv_joker W hz).1, closed_fv. }
by rewrite ih4 /= (closed_subst σ hc).
- split=> >.
+ by rewrite ih3.
+ by rewrite ih4.
Qed.
Lemma joker_hsubst z U :
closedh z ->
(forall acc θ,
(joker_abs z U acc).|[θ] = joker_abs z U acc.|[upn (t_len U) θ]) /\
(forall s tc θ,
t_len U <= tc ->
(forall i, i < tc -> θ i = TVar i) ->
(joker_call z U s tc).|[θ] = joker_call z U s.|[θ] tc).
Proof.
move=> hz.
elim: U=> [|W [_ ih2] ? [ih3 ih4]|? [ih3 ih4]] /=.
- by split.
- split=> [>|?? θ ??].
+ rewrite ih3 /= fall_hsubst ih2//.
move=> *.
by rewrite upn_k_sigma_x.
+ have hc: closedh (joker_abs z W z).
{ by apply (fvh_joker W hz).1, closedh_fvh. }
by rewrite ih4//= (closedh_hsubst θ hc).
- split=> >.
+ by rewrite ih3 fold_upn_up.
+ move=> ? h2.
rewrite ih4 //=.
* rewrite h2=>//.
by lia.
* by lia.
* move=> *.
rewrite h2=>//.
by lia.
Qed.
Fixpoint piΓ U Γ :=
match U with
| Void => Γ
| TArr V => piΓ V Γ
| Arr U V => piΓ V (U .: Γ)
end.
Lemma piΓ_shift U Γ i :
Γ i = piΓ U Γ (i + c_len U).
Proof.
elim: U Γ i=> [|U _ ? ih|? ih] Γ i /=.
- by rewrite addn0.
- rewrite addnS -addSn.
by have /= := ih (U .: Γ) i.+1.
- by apply ih.
Qed.
Lemma has_type_joker_gen z U :
(forall Γ a, [ Γ, a, a ⊢ z :- Void ]) ->
(forall acc Γ a,
[ piΓ U Γ, a + t_len U, a + t_len U ⊢ acc :- Void ] ->
[ Γ, a, a ⊢ joker_abs z U acc :- U ]) /\
(forall s tc Γ a,
[ Γ, a, a ⊢ s :- U ] ->
[ Γ, a, a ⊢ joker_call z U s tc :- Void ]).
Proof.
move=> *.
elim: U=> [|U [ih1 ih2] V [ih3 ih4]|V [ih3 ih4]] /=.
- split=> []> =>//.
by rewrite addn0.
- split=> [????|?????].
+ apply ty_lam, ih3, ty_and=>//.
apply has_type_fall, ih2, ty_var.
rewrite -[c_len V]add0n.
by rewrite -piΓ_shift.
+ apply ih4.
apply ty_app with U=>//.
by apply ih1.
- split=> [? Γ ??|?? Γ ??].
+ apply ty_tlam, ih3.
by rewrite addSnnS.
+ apply ih4.
apply ty_tapp=>//.
by apply fv_plage_eq.
Qed.
Corollary has_type_joker U :
[ ⊢ joker U :- U ].
Proof.
have hz: forall Γ a, [ Γ, a, a ⊢ Zero :- Void ]
by move=> *; apply ty_zero.
apply (has_type_joker_gen U hz).1.
by apply ty_zero.
Qed.
Corollary has_type_neu_joker U :
[ ⊢ neu (joker U) :- U ].
Proof.
by apply has_type_neu, has_type_joker.
Qed.
match U with
| Void => Γ
| TArr V => piΓ V Γ
| Arr U V => piΓ V (U .: Γ)
end.
Lemma piΓ_shift U Γ i :
Γ i = piΓ U Γ (i + c_len U).
Proof.
elim: U Γ i=> [|U _ ? ih|? ih] Γ i /=.
- by rewrite addn0.
- rewrite addnS -addSn.
by have /= := ih (U .: Γ) i.+1.
- by apply ih.
Qed.
Lemma has_type_joker_gen z U :
(forall Γ a, [ Γ, a, a ⊢ z :- Void ]) ->
(forall acc Γ a,
[ piΓ U Γ, a + t_len U, a + t_len U ⊢ acc :- Void ] ->
[ Γ, a, a ⊢ joker_abs z U acc :- U ]) /\
(forall s tc Γ a,
[ Γ, a, a ⊢ s :- U ] ->
[ Γ, a, a ⊢ joker_call z U s tc :- Void ]).
Proof.
move=> *.
elim: U=> [|U [ih1 ih2] V [ih3 ih4]|V [ih3 ih4]] /=.
- split=> []> =>//.
by rewrite addn0.
- split=> [????|?????].
+ apply ty_lam, ih3, ty_and=>//.
apply has_type_fall, ih2, ty_var.
rewrite -[c_len V]add0n.
by rewrite -piΓ_shift.
+ apply ih4.
apply ty_app with U=>//.
by apply ih1.
- split=> [? Γ ??|?? Γ ??].
+ apply ty_tlam, ih3.
by rewrite addSnnS.
+ apply ih4.
apply ty_tapp=>//.
by apply fv_plage_eq.
Qed.
Corollary has_type_joker U :
[ ⊢ joker U :- U ].
Proof.
have hz: forall Γ a, [ Γ, a, a ⊢ Zero :- Void ]
by move=> *; apply ty_zero.
apply (has_type_joker_gen U hz).1.
by apply ty_zero.
Qed.
Corollary has_type_neu_joker U :
[ ⊢ neu (joker U) :- U ].
Proof.
by apply has_type_neu, has_type_joker.
Qed.
TOPLAS, Appendix D:
S covers s
when s is in S,
or when s is Ψ ∘ l where 0 only occurs in Ψ under boxes,
S covers the directly boxed subrecipes of Ψ
and S covers the recipes of l.
covers_below is the condition on Ψ, covers_app follows the spine of
the application, n is (term binders crossed).
Fixpoint covers_below (S : stack) n s : Prop :=
match s with
| Zero => False
| Top | Var _ | Neu _ => True
| Box s => mem_ren S n s \/ covers_app S n s
| And s t | App s t => covers_below S n s /\ covers_below S n t
| TLam s | TAll s => covers_below S n.+1 s
| TApp s _ | Imp s _ | Lam s _ => covers_below S n s
end
with covers_app (S : stack) n s : Prop :=
match s with
| App s t => covers_app S n s /\ (mem_ren S n t \/ covers_app S n t)
| TApp s _ => covers_app S n s
| Zero => False
| Top | Var _ | Neu _ => True
| Box s => mem_ren S n s \/ covers_app S n s
| And s t => covers_below S n s /\ covers_below S n t
| TLam s | TAll s => covers_below S n.+1 s
| Imp s _ | Lam s _ => covers_below S n s
end.
Definition covers S n s := mem_ren S n s \/ covers_app S n s.
(* “Zero^neu_pi” :
cannot fail, but can call any of its continuation with any argument *)
Definition jokerT U := joker_abs Top U Top.
Definition submits U s :=
forall l, aligned l U -> covers l 0 s -> entails (jokerT U ∘ l) s.
Definition SUB W U := logrel (submits W) U.
Lemma mem_ren_0 S s :
mem_ren S 0 s <-> List.In (R s) S.
Proof.
split.
- move=> [t [??]].
subst.
by have->: t.|[ren (+0)] = t by asimpl.
- move=> *.
exists s.
split=>//.
by asimpl.
Qed.
Lemma covers_below_app S n s :
covers_below S n s ->
covers_app S n s.
Proof.
elim: s n=> //=.
move=> ? ih ? ih2 ? [??].
split.
- by apply ih.
- right.
by apply ih2.
Qed.
match s with
| Zero => False
| Top | Var _ | Neu _ => True
| Box s => mem_ren S n s \/ covers_app S n s
| And s t | App s t => covers_below S n s /\ covers_below S n t
| TLam s | TAll s => covers_below S n.+1 s
| TApp s _ | Imp s _ | Lam s _ => covers_below S n s
end
with covers_app (S : stack) n s : Prop :=
match s with
| App s t => covers_app S n s /\ (mem_ren S n t \/ covers_app S n t)
| TApp s _ => covers_app S n s
| Zero => False
| Top | Var _ | Neu _ => True
| Box s => mem_ren S n s \/ covers_app S n s
| And s t => covers_below S n s /\ covers_below S n t
| TLam s | TAll s => covers_below S n.+1 s
| Imp s _ | Lam s _ => covers_below S n s
end.
Definition covers S n s := mem_ren S n s \/ covers_app S n s.
(* “Zero^neu_pi” :
cannot fail, but can call any of its continuation with any argument *)
Definition jokerT U := joker_abs Top U Top.
Definition submits U s :=
forall l, aligned l U -> covers l 0 s -> entails (jokerT U ∘ l) s.
Definition SUB W U := logrel (submits W) U.
Lemma mem_ren_0 S s :
mem_ren S 0 s <-> List.In (R s) S.
Proof.
split.
- move=> [t [??]].
subst.
by have->: t.|[ren (+0)] = t by asimpl.
- move=> *.
exists s.
split=>//.
by asimpl.
Qed.
Lemma covers_below_app S n s :
covers_below S n s ->
covers_app S n s.
Proof.
elim: s n=> //=.
move=> ? ih ? ih2 ? [??].
split.
- by apply ih.
- right.
by apply ih2.
Qed.
S covers every recipe of the stack l.
Fixpoint covers_stack S n l :=
match l with
| [::] => True
| T _ :: l => covers_stack S n l
| R t :: l => covers S n t /\ covers_stack S n l
end.
Lemma covers_app_appl S n s l :
covers_app S n (s ∘ l) <-> covers_app S n s /\ covers_stack S n l.
Proof.
elim: l s=> [|[?|?] ? ih] ? /=.
- split=>//. by move=>[??].
- by rewrite ih.
- rewrite ih /covers.
repeat split=>*; unpack=>//.
by destruct H.
by destruct H.
Qed.
Lemma covers_stack_incl S l :
List.incl l S ->
covers_stack S 0 l.
Proof.
elim: l=> [|[?|?] ? ih] h //=.
- apply ih.
have [??] := List.incl_cons_inv h.
done.
- split.
+ left.
apply mem_ren_0.
apply h.
by left.
+ apply ih.
have [??] := List.incl_cons_inv h.
done.
Qed.
Lemma covers_neu S n s :
covers_below S n (neu s) /\ covers_app S n (neu s).
Proof.
elim: s n=> //=.
- move=> ? ih ? ih2 n.
have [??] := ih n.
have [??] := ih2 n.
by repeat split.
- move=> ? ih ? ih2 n.
have [??] := ih n.
have [??] := ih2 n.
repeat split=>//.
by right.
- move=> ? ih ? n.
by have [??] := ih n.
- move=> ? ih ? n.
by have [??] := ih n.
- move=> ? ih n.
by have [??] := ih n.+1.
- move=> ? ih n.
by have [??] := ih n.+1.
- move=> ? ih n.
have [??] := ih n.
by split; right.
Qed.
Lemma mem_ren_closed S n u :
closed_stack S ->
mem_ren S n u ->
closed u.
Proof.
move=> ? [? [??]].
subst.
apply closed_unaffectedh.
by apply closed_stack_in with S.
Qed.
Lemma mem_ren_ren S n j k u :
j <= n ->
mem_ren S n u ->
mem_ren S (n + k) u.|[upn j (ren (+k))].
Proof.
move=> ? [t [??]].
exists t.
split=>//.
subst.
by rewrite ren_upn_ren.
Qed.
Lemma covers_ren S k s n j :
j <= n ->
(covers_below S n s -> covers_below S (n + k) s.|[upn j (ren (+k))]) /\
(covers_app S n s -> covers_app S (n + k) s.|[upn j (ren (+k))]).
Proof.
elim: s n j=> //=.
- move=> ? ih ? ih2 n j hj.
have [h1 _] := ih n j hj.
have [h2 _] := ih2 n j hj.
repeat split; unpack.
+ by apply h1.
+ by apply h2.
+ by apply h1.
+ by apply h2.
- move=> ? ih ? ih2 n j hj.
have [h1 h1'] := ih n j hj.
have [h2 h2'] := ih2 n j hj.
split.
+ move=> [??]; split.
* by apply h1.
* by apply h2.
+ move=> [? [?|?]]; split; try by apply h1'.
* left. by apply mem_ren_ren.
* right. by apply h2'.
- move=> ? ih ? n j hj.
by have [??] := ih n j hj.
- move=> ? ih ? n j hj.
by have [??] := ih n j hj.
- move=> ? ih n j hj.
rewrite fold_up_upn -addSn.
by have [??] := ih n.+1 j.+1 hj.
- move=> ? ih n j hj.
rewrite fold_up_upn -addSn.
by have [??] := ih n.+1 j.+1 hj.
- move=> ? ih n j hj.
have [_ h] := ih n j hj.
split => -[?|?].
+ left. by apply mem_ren_ren.
+ right. by apply h.
+ left. by apply mem_ren_ren.
+ right. by apply h.
Qed.
Corollary covers_app_ren S k s n j :
j <= n ->
covers_app S n s ->
covers_app S (n + k) s.|[upn j (ren (+k))].
Proof.
move=> hj.
by apply (covers_ren S k s hj).
Qed.
match l with
| [::] => True
| T _ :: l => covers_stack S n l
| R t :: l => covers S n t /\ covers_stack S n l
end.
Lemma covers_app_appl S n s l :
covers_app S n (s ∘ l) <-> covers_app S n s /\ covers_stack S n l.
Proof.
elim: l s=> [|[?|?] ? ih] ? /=.
- split=>//. by move=>[??].
- by rewrite ih.
- rewrite ih /covers.
repeat split=>*; unpack=>//.
by destruct H.
by destruct H.
Qed.
Lemma covers_stack_incl S l :
List.incl l S ->
covers_stack S 0 l.
Proof.
elim: l=> [|[?|?] ? ih] h //=.
- apply ih.
have [??] := List.incl_cons_inv h.
done.
- split.
+ left.
apply mem_ren_0.
apply h.
by left.
+ apply ih.
have [??] := List.incl_cons_inv h.
done.
Qed.
Lemma covers_neu S n s :
covers_below S n (neu s) /\ covers_app S n (neu s).
Proof.
elim: s n=> //=.
- move=> ? ih ? ih2 n.
have [??] := ih n.
have [??] := ih2 n.
by repeat split.
- move=> ? ih ? ih2 n.
have [??] := ih n.
have [??] := ih2 n.
repeat split=>//.
by right.
- move=> ? ih ? n.
by have [??] := ih n.
- move=> ? ih ? n.
by have [??] := ih n.
- move=> ? ih n.
by have [??] := ih n.+1.
- move=> ? ih n.
by have [??] := ih n.+1.
- move=> ? ih n.
have [??] := ih n.
by split; right.
Qed.
Lemma mem_ren_closed S n u :
closed_stack S ->
mem_ren S n u ->
closed u.
Proof.
move=> ? [? [??]].
subst.
apply closed_unaffectedh.
by apply closed_stack_in with S.
Qed.
Lemma mem_ren_ren S n j k u :
j <= n ->
mem_ren S n u ->
mem_ren S (n + k) u.|[upn j (ren (+k))].
Proof.
move=> ? [t [??]].
exists t.
split=>//.
subst.
by rewrite ren_upn_ren.
Qed.
Lemma covers_ren S k s n j :
j <= n ->
(covers_below S n s -> covers_below S (n + k) s.|[upn j (ren (+k))]) /\
(covers_app S n s -> covers_app S (n + k) s.|[upn j (ren (+k))]).
Proof.
elim: s n j=> //=.
- move=> ? ih ? ih2 n j hj.
have [h1 _] := ih n j hj.
have [h2 _] := ih2 n j hj.
repeat split; unpack.
+ by apply h1.
+ by apply h2.
+ by apply h1.
+ by apply h2.
- move=> ? ih ? ih2 n j hj.
have [h1 h1'] := ih n j hj.
have [h2 h2'] := ih2 n j hj.
split.
+ move=> [??]; split.
* by apply h1.
* by apply h2.
+ move=> [? [?|?]]; split; try by apply h1'.
* left. by apply mem_ren_ren.
* right. by apply h2'.
- move=> ? ih ? n j hj.
by have [??] := ih n j hj.
- move=> ? ih ? n j hj.
by have [??] := ih n j hj.
- move=> ? ih n j hj.
rewrite fold_up_upn -addSn.
by have [??] := ih n.+1 j.+1 hj.
- move=> ? ih n j hj.
rewrite fold_up_upn -addSn.
by have [??] := ih n.+1 j.+1 hj.
- move=> ? ih n j hj.
have [_ h] := ih n j hj.
split => -[?|?].
+ left. by apply mem_ren_ren.
+ right. by apply h.
+ left. by apply mem_ren_ren.
+ right. by apply h.
Qed.
Corollary covers_app_ren S k s n j :
j <= n ->
covers_app S n s ->
covers_app S (n + k) s.|[upn j (ren (+k))].
Proof.
move=> hj.
by apply (covers_ren S k s hj).
Qed.
A substitution whose range is variables and covered closed boxes.
Definition sub_cov S n (σ : var -> recipe) :=
forall x, (exists y, σ x = Var y) \/
(exists u, σ x = Box u /\ closed u /\ covers S n u).
Lemma sub_cov_box S n t :
closed t ->
covers S n t ->
sub_cov S n (Box t .: ids).
Proof.
move=> ?? [|x].
- right.
by exists t.
- left.
by exists x.
Qed.
Lemma sub_cov_up S n σ :
sub_cov S n σ ->
sub_cov S n (up σ).
Proof.
move=> h [|x].
- left.
exists 0.
by asimpl.
- move: (h x)=> [[y e]|[u [e [hc ?]]]].
+ left.
exists y.+1.
asimpl.
rewrite e.
by asimpl.
+ right.
exists u.
asimpl.
rewrite e /=.
split=>//.
by rewrite (closed_subst _ hc).
Qed.
Lemma sub_cov_hcomp S n σ :
sub_cov S n σ ->
sub_cov S n.+1 (σ >>| ren (+1)).
Proof.
move=> h x.
have->: (σ >>| ren (+1)) x = (σ x).|[ren (+1)] by [].
move: (h x)=> [[y e]|[u [e [? hu]]]].
- left.
exists y.
by rewrite e.
- right.
exists u.|[ren (+1)].
rewrite e /=.
split=>//.
split; first by apply closed_unaffectedh.
move: hu=> [hu|hu].
+ left.
have := mem_ren_ren (j:=0) 1 (leq0n n) hu.
by rewrite addn1.
+ right.
have := covers_app_ren (j:=0) 1 (leq0n n) hu.
by rewrite addn1.
Qed.
Lemma covers_subst S s n σ :
closed_stack S ->
sub_cov S n σ ->
(covers_below S n s -> covers_below S n s.[σ]) /\
(covers_app S n s -> covers_app S n s.[σ]).
Proof.
move=> hS.
elim: s n σ=> //=.
- move=> x ? σ hσ.
by move: (hσ x)=> [[? ->]|[? [-> [_ ?]]]].
- move=> ? ih ? ih2 n σ hσ.
have [h1 _] := ih n σ hσ.
have [h2 _] := ih2 n σ hσ.
repeat split; unpack.
+ by apply h1.
+ by apply h2.
+ by apply h1.
+ by apply h2.
- move=> ? ih ? ih2 n σ hσ.
have [h1 h1'] := ih n σ hσ.
have [h2 h2'] := ih2 n σ hσ.
split.
+ move=> [??].
by split; [apply h1|apply h2].
+ move=> [? [h|h]]; split; try by apply h1'.
* left.
rewrite closed_subst=>//.
by apply mem_ren_closed with S n.
* right. by apply h2'.
- move=> ? ih ? n σ hσ.
have [??] := ih n (up σ) (sub_cov_up hσ).
by split.
- move=> ? ih ? n σ hσ.
by have [??] := ih n σ hσ.
- move=> ? ih n σ hσ.
have [??] := ih n.+1 _ (sub_cov_hcomp hσ).
by split.
- move=> ? ih n σ hσ.
have [??] := ih n.+1 _ (sub_cov_hcomp hσ).
by split.
- move=> ? ih n σ hσ.
have [_ h] := ih n σ hσ.
split=> -[hm|?]; [left|right|left|right]; try by apply h.
+ rewrite closed_subst=>//.
by apply mem_ren_closed with S n.
+ rewrite closed_subst=>//.
by apply mem_ren_closed with S n.
Qed.
Lemma mem_ren_hsubst S m j u (T : term) :
mem_ren S (m.+1 + j) u ->
mem_ren S (m + j) u.|[upn j (T .: ids)].
Proof.
move=> [t [??]].
exists t.
split=>//.
subst.
by rewrite ren_upn_subst.
Qed.
Lemma covers_hsubst S (T : term) s m j:
(covers_below S (m.+1 + j) s -> covers_below S (m + j) s.|[upn j (T .: ids)]) /\
(covers_app S (m.+1 + j) s -> covers_app S (m + j) s.|[upn j (T .: ids)]).
Proof.
elim: s m j=> //=.
- move=> ? ih ? ih2 m j.
have [h1 _] := ih m j.
have [h2 _] := ih2 m j.
by split=> -[??]; split; [apply h1|apply h2|apply h1|apply h2].
- move=> ? ih ? ih2 m j.
have [h1 h1'] := ih m j.
have [h2 h2'] := ih2 m j.
split.
+ move=> [??].
by split; [apply h1|apply h2].
+ move=> [? [?|?]]; split; try by apply h1'.
* left. by apply mem_ren_hsubst.
* right. by apply h2'.
- move=> ? ih ? m j.
by have [??] := ih m j.
- move=> ? ih ? m j.
by have [??] := ih m j.
- move=> ? ih m j.
rewrite fold_up_upn -!addnS.
have [h _] := ih m j.+1.
by split.
- move=> ? ih m j.
rewrite fold_up_upn -!addnS.
have [h _] := ih m j.+1.
by split.
- move=> ? ih m j.
have [_ h] := ih m j.
split=> -[?|?].
+ left. by apply mem_ren_hsubst.
+ right. by apply h.
+ left. by apply mem_ren_hsubst.
+ right. by apply h.
Qed.
Corollary covers_below_hsubst0 S (T : term) s m :
covers_below S m.+1 s ->
covers_below S m s.|[T/].
Proof.
move=> h.
have h2: covers_below S (m.+1 + 0) s by rewrite addn0.
have [h3 _] := covers_hsubst S T s m 0.
have := h3 h2.
by rewrite addn0.
Qed.
forall x, (exists y, σ x = Var y) \/
(exists u, σ x = Box u /\ closed u /\ covers S n u).
Lemma sub_cov_box S n t :
closed t ->
covers S n t ->
sub_cov S n (Box t .: ids).
Proof.
move=> ?? [|x].
- right.
by exists t.
- left.
by exists x.
Qed.
Lemma sub_cov_up S n σ :
sub_cov S n σ ->
sub_cov S n (up σ).
Proof.
move=> h [|x].
- left.
exists 0.
by asimpl.
- move: (h x)=> [[y e]|[u [e [hc ?]]]].
+ left.
exists y.+1.
asimpl.
rewrite e.
by asimpl.
+ right.
exists u.
asimpl.
rewrite e /=.
split=>//.
by rewrite (closed_subst _ hc).
Qed.
Lemma sub_cov_hcomp S n σ :
sub_cov S n σ ->
sub_cov S n.+1 (σ >>| ren (+1)).
Proof.
move=> h x.
have->: (σ >>| ren (+1)) x = (σ x).|[ren (+1)] by [].
move: (h x)=> [[y e]|[u [e [? hu]]]].
- left.
exists y.
by rewrite e.
- right.
exists u.|[ren (+1)].
rewrite e /=.
split=>//.
split; first by apply closed_unaffectedh.
move: hu=> [hu|hu].
+ left.
have := mem_ren_ren (j:=0) 1 (leq0n n) hu.
by rewrite addn1.
+ right.
have := covers_app_ren (j:=0) 1 (leq0n n) hu.
by rewrite addn1.
Qed.
Lemma covers_subst S s n σ :
closed_stack S ->
sub_cov S n σ ->
(covers_below S n s -> covers_below S n s.[σ]) /\
(covers_app S n s -> covers_app S n s.[σ]).
Proof.
move=> hS.
elim: s n σ=> //=.
- move=> x ? σ hσ.
by move: (hσ x)=> [[? ->]|[? [-> [_ ?]]]].
- move=> ? ih ? ih2 n σ hσ.
have [h1 _] := ih n σ hσ.
have [h2 _] := ih2 n σ hσ.
repeat split; unpack.
+ by apply h1.
+ by apply h2.
+ by apply h1.
+ by apply h2.
- move=> ? ih ? ih2 n σ hσ.
have [h1 h1'] := ih n σ hσ.
have [h2 h2'] := ih2 n σ hσ.
split.
+ move=> [??].
by split; [apply h1|apply h2].
+ move=> [? [h|h]]; split; try by apply h1'.
* left.
rewrite closed_subst=>//.
by apply mem_ren_closed with S n.
* right. by apply h2'.
- move=> ? ih ? n σ hσ.
have [??] := ih n (up σ) (sub_cov_up hσ).
by split.
- move=> ? ih ? n σ hσ.
by have [??] := ih n σ hσ.
- move=> ? ih n σ hσ.
have [??] := ih n.+1 _ (sub_cov_hcomp hσ).
by split.
- move=> ? ih n σ hσ.
have [??] := ih n.+1 _ (sub_cov_hcomp hσ).
by split.
- move=> ? ih n σ hσ.
have [_ h] := ih n σ hσ.
split=> -[hm|?]; [left|right|left|right]; try by apply h.
+ rewrite closed_subst=>//.
by apply mem_ren_closed with S n.
+ rewrite closed_subst=>//.
by apply mem_ren_closed with S n.
Qed.
Lemma mem_ren_hsubst S m j u (T : term) :
mem_ren S (m.+1 + j) u ->
mem_ren S (m + j) u.|[upn j (T .: ids)].
Proof.
move=> [t [??]].
exists t.
split=>//.
subst.
by rewrite ren_upn_subst.
Qed.
Lemma covers_hsubst S (T : term) s m j:
(covers_below S (m.+1 + j) s -> covers_below S (m + j) s.|[upn j (T .: ids)]) /\
(covers_app S (m.+1 + j) s -> covers_app S (m + j) s.|[upn j (T .: ids)]).
Proof.
elim: s m j=> //=.
- move=> ? ih ? ih2 m j.
have [h1 _] := ih m j.
have [h2 _] := ih2 m j.
by split=> -[??]; split; [apply h1|apply h2|apply h1|apply h2].
- move=> ? ih ? ih2 m j.
have [h1 h1'] := ih m j.
have [h2 h2'] := ih2 m j.
split.
+ move=> [??].
by split; [apply h1|apply h2].
+ move=> [? [?|?]]; split; try by apply h1'.
* left. by apply mem_ren_hsubst.
* right. by apply h2'.
- move=> ? ih ? m j.
by have [??] := ih m j.
- move=> ? ih ? m j.
by have [??] := ih m j.
- move=> ? ih m j.
rewrite fold_up_upn -!addnS.
have [h _] := ih m j.+1.
by split.
- move=> ? ih m j.
rewrite fold_up_upn -!addnS.
have [h _] := ih m j.+1.
by split.
- move=> ? ih m j.
have [_ h] := ih m j.
split=> -[?|?].
+ left. by apply mem_ren_hsubst.
+ right. by apply h.
+ left. by apply mem_ren_hsubst.
+ right. by apply h.
Qed.
Corollary covers_below_hsubst0 S (T : term) s m :
covers_below S m.+1 s ->
covers_below S m s.|[T/].
Proof.
move=> h.
have h2: covers_below S (m.+1 + 0) s by rewrite addn0.
have [h3 _] := covers_hsubst S T s m 0.
have := h3 h2.
by rewrite addn0.
Qed.
Lemma subst_depth_hit U r k :
closed r ->
subst_depth U (upn k (Box r .: ids)) (k + c_len U) = Box r.|[ren (+ t_len U)].
Proof.
elim: U r k=> [|? _ V ih|V ih] ?? hc /=.
- rewrite addn0 upnP_cond// subnn /=.
rewrite (closed_subst _ hc).
by asimpl.
- rewrite fold_up_upn addnS -addSn.
by apply ih.
- rewrite upn_hcomp scons_hcomp ih; last by apply closed_unaffectedh.
have e: forall e, e.|[ren (+ t_len V)] = e.|[upn 0 (ren (+ t_len V))] by [].
by rewrite e ren_upn_ren.
Qed.
Fixpoint joker_inst (z : recipe) (U : type) (l : stack) (acc : recipe) : recipe :=
match U, l with
| TArr V, T t :: l2 => joker_inst z V l2 acc.|[upn (t_len V) (t .: ids)]
| Arr W V, R r :: l2 =>
joker_inst z V l2
(And acc (joker_all z W (Var (c_len V))))
.[subst_depth V (Box r .: ids)]
| _, _ => acc
end.
Lemma joker_inst_arr z W V r l acc :
joker_inst z (Arr W V) (R r :: l) acc =
joker_inst z V l
(And acc (joker_all z W (Var (c_len V)))).[subst_depth V (Box r .: ids)].
Proof.
by [].
Qed.
Lemma joker_inst_tarr z V t l acc :
joker_inst z (TArr V) (T t :: l) acc =
joker_inst z V l acc.|[upn (t_len V) (t .: ids)].
Proof.
by [].
Qed.
Lemma joker_abs_arr z W V acc :
joker_abs z (Arr W V) acc =
Lam (joker_abs z V (And acc (joker_all z W (Var (c_len V))))) W.
Proof.
by [].
Qed.
Lemma joker_abs_tarr z V acc :
joker_abs z (TArr V) acc =
TLam (joker_abs z V acc).
Proof.
by [].
Qed.
Lemma eval_joker_abs z U :
closed z -> closedh z ->
forall l acc F,
aligned l U ->
eval (joker_abs z U acc ∘ l) [::] F <-> eval (joker_inst z U l acc) [::] F.
Proof.
move=> hcT hhT.
elim: U=> [|? _ ? ih|? ih] l ? F hl.
- move: l hl=> [|[?|?] l] [hc h]; inv h.
by split.
- move: l hl=> [|[?|?] l] [hc h]; try by inv h.
have hl := aligned_cons_r hc h.
rewrite joker_inst_arr.
apply: (iff_trans _ (ih l _ F hl)).
rewrite -((joker_subst _ hcT).1 _ _) joker_abs_arr.
split=> /eval_move_stack_right h2;
apply eval_move_stack_left.
+ by inv h2.
+ by constructor.
- move: l hl=> [|[?|?] l] [hc h]; try by inv h.
have hl := aligned_cons_t hc h.
rewrite joker_inst_tarr.
apply: (iff_trans _ (ih l _ F hl)).
rewrite -((joker_hsubst _ hhT).1 _ _) joker_abs_tarr.
split=> /eval_move_stack_right h2;
apply eval_move_stack_left.
+ by inv h2.
+ by constructor.
Qed.
u is a conjunct of the conjunction tree r.
Inductive conj_in (u : recipe) : recipe -> Prop :=
| conj_in_here : conj_in u u
| conj_in_l s t : conj_in u s -> conj_in u (And s t)
| conj_in_r s t : conj_in u t -> conj_in u (And s t).
Lemma conj_in_hsubst u r (θ : var -> term) :
conj_in u r ->
conj_in u.|[θ] r.|[θ].
Proof.
by elim; constructor.
Qed.
Lemma conj_in_subst_closed u r (σ : var -> recipe) :
closed u ->
conj_in u r ->
conj_in u r.[σ].
Proof.
move=> hc.
elim.
- rewrite (closed_subst _ hc).
by constructor.
- by constructor.
- by constructor.
Qed.
Lemma eval_conj_in u r :
conj_in u r ->
forall F,
eval r [::] F ->
exists G, eval u [::] G /\ F ||- G.
Proof.
elim=> [|s t _ ih|s t _ ih] F h.
- exists F.
split=>//.
by apply valid_assumption.
- inv h.
match goal with hs: eval s [::] _ |- _ => have [G [h1 h2]] := ih _ hs end.
exists G.
split=>//.
apply: valid_cut; last by apply h2.
apply valid_and_intro_l.
left.
by apply valid_assumption.
- inv h.
match goal with hs: eval t [::] _ |- _ => have [G [h1 h2]] := ih _ hs end.
exists G.
split=>//.
apply: valid_cut; last by apply h2.
apply valid_and_intro_l.
right.
by apply valid_assumption.
Qed.
Lemma conj_in_joker_inst U :
forall l acc s,
aligned l U ->
closed s ->
conj_in (Box s.|[ren (+ t_len U)]) acc ->
conj_in (Box s) (joker_inst Top U l acc).
Proof.
elim: U=> [|W _ V ih|V ih] l acc s hl ? h /=.
- move: l hl=> [|[t|r] l] [hc h2]; inv h2.
have e: s.|[ren (+0)] = s by asimpl.
by rewrite e in h.
- move: l hl=> [|[t|r] l] [hc h2]; try by inv h2.
have hl := aligned_cons_r hc h2.
apply ih=>//.
have hcB: closed (Box s.|[ren (+ t_len V)]) by apply closed_box, closed_unaffectedh.
by apply (conj_in_subst_closed (subst_depth V (Box r .: ids)) hcB
(conj_in_l (joker_all Top W (Var (c_len V))) h)).
- move: l hl=> [|[t|?] ?] [hc h2]; try by inv h2.
have hl := aligned_cons_t hc h2.
apply ih=>//.
have e := ren_upn_subst s 0 (t_len V) t.
rewrite add1n add0n in e.
have h3: conj_in (Box (s.|[ren (+(t_len V).+1)]).|[upn (t_len V) (t .: ids)])
acc.|[upn (t_len V) (t .: ids)] by apply (conj_in_hsubst _ h).
rewrite e in h3.
apply h3.
Qed.
Lemma conj_in_joker_mem U :
forall l acc s,
aligned l U ->
List.In (R s) l ->
[ ⊢ s :- Void ] ->
conj_in (Box s) (joker_inst Top U l acc).
Proof.
elim: U=> [|W _ V ih|V ih] l acc s hl hin ? /=.
- move: l hl hin=> [|[?|r] l] [hc h] hin; by inv h.
- move: l hl hin=> [|[?|r] l] [hc h] hin; try by inv h.
have hl := aligned_cons_r hc h.
move: hin=> [e|hin]; last by apply ih.
move: e=> [e].
subst.
have hcs: closed s by inv hc.
have htr: [ ⊢ s :- W ] by inv h.
have hW: W = Void by apply has_type_det with empty_ctx 0 0 s.
subst.
apply conj_in_joker_inst=>//.
have := subst_depth_hit V 0 hcs.
rewrite add0n /= => e.
have h3: conj_in (Box s.|[ren (+ t_len V)])
(And acc.[subst_depth V (Box s .: ids)] (subst_depth V (Box s .: ids) (c_len V))).
{ rewrite e. by apply conj_in_r, conj_in_here. }
apply h3.
- move: l hl hin=> [|[?|?] ?] [hc h] hin; try by inv h.
have hl := aligned_cons_t hc h.
apply ih=>//.
by case: hin.
Qed.
Lemma joker_entails_mem W l s :
aligned l W ->
[ ⊢ s :- Void ] ->
List.In (R s) l ->
entails (jokerT W ∘ l) s.
Proof.
move=> hl hts ? f g hf ?.
rewrite /jokerT in hf.
have p := eval_joker_abs closed_top closedh_top Top f hl.
have hf2 := proj1 p hf.
have hc: conj_in (Box s) (joker_inst Top W l Top) by apply conj_in_joker_mem.
have [G [hG hfG]] := eval_conj_in hc hf2.
inv hG.
have hcs: closed s by apply (closed_stack_in (S:=l))=>//; case: hl.
have e: G = g by apply (uniqueness_eval (conj hcs hts)).
by rewrite -e.
Qed.
| conj_in_here : conj_in u u
| conj_in_l s t : conj_in u s -> conj_in u (And s t)
| conj_in_r s t : conj_in u t -> conj_in u (And s t).
Lemma conj_in_hsubst u r (θ : var -> term) :
conj_in u r ->
conj_in u.|[θ] r.|[θ].
Proof.
by elim; constructor.
Qed.
Lemma conj_in_subst_closed u r (σ : var -> recipe) :
closed u ->
conj_in u r ->
conj_in u r.[σ].
Proof.
move=> hc.
elim.
- rewrite (closed_subst _ hc).
by constructor.
- by constructor.
- by constructor.
Qed.
Lemma eval_conj_in u r :
conj_in u r ->
forall F,
eval r [::] F ->
exists G, eval u [::] G /\ F ||- G.
Proof.
elim=> [|s t _ ih|s t _ ih] F h.
- exists F.
split=>//.
by apply valid_assumption.
- inv h.
match goal with hs: eval s [::] _ |- _ => have [G [h1 h2]] := ih _ hs end.
exists G.
split=>//.
apply: valid_cut; last by apply h2.
apply valid_and_intro_l.
left.
by apply valid_assumption.
- inv h.
match goal with hs: eval t [::] _ |- _ => have [G [h1 h2]] := ih _ hs end.
exists G.
split=>//.
apply: valid_cut; last by apply h2.
apply valid_and_intro_l.
right.
by apply valid_assumption.
Qed.
Lemma conj_in_joker_inst U :
forall l acc s,
aligned l U ->
closed s ->
conj_in (Box s.|[ren (+ t_len U)]) acc ->
conj_in (Box s) (joker_inst Top U l acc).
Proof.
elim: U=> [|W _ V ih|V ih] l acc s hl ? h /=.
- move: l hl=> [|[t|r] l] [hc h2]; inv h2.
have e: s.|[ren (+0)] = s by asimpl.
by rewrite e in h.
- move: l hl=> [|[t|r] l] [hc h2]; try by inv h2.
have hl := aligned_cons_r hc h2.
apply ih=>//.
have hcB: closed (Box s.|[ren (+ t_len V)]) by apply closed_box, closed_unaffectedh.
by apply (conj_in_subst_closed (subst_depth V (Box r .: ids)) hcB
(conj_in_l (joker_all Top W (Var (c_len V))) h)).
- move: l hl=> [|[t|?] ?] [hc h2]; try by inv h2.
have hl := aligned_cons_t hc h2.
apply ih=>//.
have e := ren_upn_subst s 0 (t_len V) t.
rewrite add1n add0n in e.
have h3: conj_in (Box (s.|[ren (+(t_len V).+1)]).|[upn (t_len V) (t .: ids)])
acc.|[upn (t_len V) (t .: ids)] by apply (conj_in_hsubst _ h).
rewrite e in h3.
apply h3.
Qed.
Lemma conj_in_joker_mem U :
forall l acc s,
aligned l U ->
List.In (R s) l ->
[ ⊢ s :- Void ] ->
conj_in (Box s) (joker_inst Top U l acc).
Proof.
elim: U=> [|W _ V ih|V ih] l acc s hl hin ? /=.
- move: l hl hin=> [|[?|r] l] [hc h] hin; by inv h.
- move: l hl hin=> [|[?|r] l] [hc h] hin; try by inv h.
have hl := aligned_cons_r hc h.
move: hin=> [e|hin]; last by apply ih.
move: e=> [e].
subst.
have hcs: closed s by inv hc.
have htr: [ ⊢ s :- W ] by inv h.
have hW: W = Void by apply has_type_det with empty_ctx 0 0 s.
subst.
apply conj_in_joker_inst=>//.
have := subst_depth_hit V 0 hcs.
rewrite add0n /= => e.
have h3: conj_in (Box s.|[ren (+ t_len V)])
(And acc.[subst_depth V (Box s .: ids)] (subst_depth V (Box s .: ids) (c_len V))).
{ rewrite e. by apply conj_in_r, conj_in_here. }
apply h3.
- move: l hl hin=> [|[?|?] ?] [hc h] hin; try by inv h.
have hl := aligned_cons_t hc h.
apply ih=>//.
by case: hin.
Qed.
Lemma joker_entails_mem W l s :
aligned l W ->
[ ⊢ s :- Void ] ->
List.In (R s) l ->
entails (jokerT W ∘ l) s.
Proof.
move=> hl hts ? f g hf ?.
rewrite /jokerT in hf.
have p := eval_joker_abs closed_top closedh_top Top f hl.
have hf2 := proj1 p hf.
have hc: conj_in (Box s) (joker_inst Top W l Top) by apply conj_in_joker_mem.
have [G [hG hfG]] := eval_conj_in hc hf2.
inv hG.
have hcs: closed s by apply (closed_stack_in (S:=l))=>//; case: hl.
have e: G = g by apply (uniqueness_eval (conj hcs hts)).
by rewrite -e.
Qed.
Lemma mem_ren_shift S n u :
mem_ren S n.+1 u ->
mem_ren (stack_hsubst (ren (+1)) S) n u.
Proof.
move=> [t [??]].
exists t.|[ren (+1)].
split; first by apply in_stack_hsubst.
subst.
by rewrite ren_add add1n.
Qed.
Lemma covers_shift S s :
forall n,
(covers_below S n.+1 s -> covers_below (stack_hsubst (ren (+1)) S) n s) /\
(covers_app S n.+1 s -> covers_app (stack_hsubst (ren (+1)) S) n s).
Proof.
elim: s=> //=.
- move=> ? ih ? ih2 n.
have [h1 _] := ih n.
have [h2 _] := ih2 n.
by split=> -[??]; split; [apply h1|apply h2|apply h1|apply h2].
- move=> ? ih ? ih2 n.
have [h1 h1'] := ih n.
have [h2 h2'] := ih2 n.
split.
+ move=> [??].
by split; [apply h1|apply h2].
+ move=> [? [?|?]]; split; try by apply h1'.
* left.
by apply mem_ren_shift.
* right.
by apply h2'.
- move=> ? ih ? n.
by have [??] := ih n.
- move=> ? ih ? n.
by have [??] := ih n.
- move=> ? ih n.
by have [??] := ih n.+1.
- move=> ? ih n.
by have [??] := ih n.+1.
- move=> ? ih n.
have [_ h] := ih n.
by split=> -[?|?]; [left|right|left|right]; by [apply mem_ren_shift|apply h].
Qed.
Lemma closed_jokerT U :
closed (jokerT U).
Proof.
by apply (fv_joker U closed_top).1.
Qed.
Lemma closedh_jokerT U :
closedh (jokerT U).
Proof.
by apply (fvh_joker U closedh_top).1.
Qed.
Lemma has_type_jokerT U :
[ ⊢ jokerT U :- U ].
Proof.
have hz: forall Γ a, [ Γ, a, a ⊢ Top :- Void ] by move=> *; apply ty_top.
apply (has_type_joker_gen U hz).1.
by apply ty_top.
Qed.
l where each recipe item is replaced by the joker of its signature
Fixpoint jstack (U : type) (l : stack) : stack :=
match U, l with
| TArr V, T t :: l2 => T t :: jstack V l2
| Arr W V, R _ :: l2 => R (jokerT W) :: jstack V l2
| _, _ => [::]
end.
Lemma aligned_jstack U l :
aligned l U ->
aligned (jstack U l) U.
Proof.
elim: U l=> [|? _ ? ih|? ih] l;
move: l=> [|[?|?] l] [hc h]; try by inv h.
- by split; constructor.
- have hl := aligned_cons_r hc h.
have [h1 h2] := ih l hl.
split; constructor=>//; by [apply closed_jokerT|apply has_type_jokerT].
- have hl := aligned_cons_t hc h.
have [h1 h2] := ih l hl.
by split; constructor.
Qed.
Lemma ent_jokerT W :
(forall W2, order W2 < order W ->
forall U r, closed r -> [ ⊢ r :- U ] -> SUB W2 U r) ->
forall U Ψ, order U < order W -> closed Ψ -> [ ⊢ Ψ :- U ] ->
ENT U (jokerT U) (neu Ψ).
Proof.
move=> ihW U Ψ ???.
apply entails_36; try by [apply closed_jokerT|apply has_type_jokerT
|apply closed_sneu|apply has_type_neu].
move=> l2 hl2.
have hsub: SUB U Void (neu Ψ ∘ l2).
{ apply ihW=>//.
- apply closed_appl; first by apply closed_sneu.
by case: hl2.
- apply aligned_type_void with U=>//.
by apply has_type_neu. }
apply hsub=>//.
right.
apply covers_app_appl.
split; first by apply (covers_neu _ _ _).2.
by apply covers_stack_incl.
Qed.
Lemma stack_rel2_jstack U l :
(forall W Ψ, arg_of W U -> closed Ψ -> [ ⊢ Ψ :- W ] -> ENT W (jokerT W) (neu Ψ)) ->
aligned l U -> stack_rel2 entails U (jstack U l) (neu_stack l).
Proof.
elim: U l=> [|W _ ? ih|? ih] l h;
move: l=> [|[?|r] ?] [hc ht]; try by inv ht.
- by constructor.
- have hl := aligned_cons_r hc ht.
have hcr: closed r by inv hc.
have htr: [ ⊢ r :- W ] by inv ht.
constructor.
+ move=> ξ.
have hj: (jokerT W).|[ren ξ] = jokerT W.
{ by apply closedh_hsubst, closedh_jokerT. }
rewrite /= hj -neu_hsubst_comm.
have hE: ENT W (jokerT W) (neu r.|[ren ξ]).
{ apply h; first by constructor.
- by apply closed_unaffectedh.
- by apply has_type_hsubst_0. }
split=>//.
by rewrite /jokerT (neu_joker Top W).1 neu_idempotent.
+ apply ih=>// ? Ψ ?.
apply h.
by constructor.
- have hl := aligned_cons_t hc ht.
constructor.
apply ih=>// ? Ψ ?.
apply h.
by constructor.
Qed.
Lemma closed_call W f m :
closed f ->
closed (fall m (joker_call Top W f m)).
Proof.
move=> *.
by apply fv_fall, (fv_joker W closed_top).2.
Qed.
Lemma conj_in_call_inst U :
forall l acc W r, aligned l U -> closed r ->
conj_in
(joker_all Top W (Box r.|[ren (+(t_len W + t_len U))])) acc ->
conj_in
(joker_all Top W (Box r.|[ren (+ t_len W)]))
(joker_inst Top U l acc).
Proof.
elim: U=> [|? _ V ih|V ih] l ? W r hl ? h /=.
- move: l hl=> [|[t|?] l] [hc h2]; inv h2.
by rewrite addn0 in h.
- move: l hl=> [|[t|?] l] [hc h2]; try by inv h2.
have hl := aligned_cons_r hc h2.
apply ih=>//.
have hcB: closed
(joker_all Top W (Box r.|[ren (+(t_len W + t_len V))])).
{ apply closed_call, closed_box. by apply closed_unaffectedh. }
by apply (conj_in_subst_closed _ hcB (conj_in_l _ h)).
- move: l hl=> [|[t|?] ?] [hc h2]; try by inv h2.
have hl := aligned_cons_t hc h2.
apply ih=>//.
have e:
(joker_all Top W (Box r.|[ren (+(t_len W + (t_len V).+1))]))
.|[upn (t_len V) (t .: ids)] =
joker_all Top W (Box r.|[ren (+(t_len W + t_len V))]).
{ rewrite fall_hsubst ((joker_hsubst _ closedh_top).2 _ _ _) //=;
last by move=> ??; rewrite upn_k_sigma_x.
rewrite upn_add addnS -add1n ren_upn_subst add0n.
by []. }
rewrite -e.
by apply conj_in_hsubst.
Qed.
Lemma conj_in_joker_call W :
forall l acc s U,
aligned l W ->
List.In (R s) l ->
[ ⊢ s :- U ] ->
conj_in (joker_all Top U (Box s.|[ren (+ t_len U)]))
(joker_inst Top W l acc).
Proof.
elim: W=> [|W _ V ih|V ih] l ? s U hl hin ? /=.
- move: l hl hin=> [|[?|r] l] [hc h] hin; by inv h.
- move: l hl hin=> [|[?|r] l] [hc h] hin; try by inv h.
have hl := aligned_cons_r hc h.
move: hin=> [e|hin]; last by apply ih.
move: e=> [e].
subst.
have hcs: closed s by inv hc.
have htr: [ ⊢ s :- W ] by inv h.
have e: W = U by apply has_type_det with empty_ctx 0 0 s.
subst.
apply conj_in_call_inst=>//.
have hsb := subst_depth_hit V 0 hcs.
rewrite add0n in hsb.
have e:
(joker_all Top U (Var (c_len V)))
.[subst_depth V (Box s .: ids)] =
joker_all Top U (Box s.|[ren (+(t_len U + t_len V))]).
{ rewrite fall_subst ((joker_subst _ closed_top).2 _ _ _) //= hsb /= ren_add.
by rewrite addnC. }
rewrite -e.
by apply conj_in_r, conj_in_here.
- move: l hl hin=> [|[?|?] ?] [hc h] hin; try by inv h.
have hl := aligned_cons_t hc h.
apply ih=>//.
by case: hin.
Qed.
match U, l with
| TArr V, T t :: l2 => T t :: jstack V l2
| Arr W V, R _ :: l2 => R (jokerT W) :: jstack V l2
| _, _ => [::]
end.
Lemma aligned_jstack U l :
aligned l U ->
aligned (jstack U l) U.
Proof.
elim: U l=> [|? _ ? ih|? ih] l;
move: l=> [|[?|?] l] [hc h]; try by inv h.
- by split; constructor.
- have hl := aligned_cons_r hc h.
have [h1 h2] := ih l hl.
split; constructor=>//; by [apply closed_jokerT|apply has_type_jokerT].
- have hl := aligned_cons_t hc h.
have [h1 h2] := ih l hl.
by split; constructor.
Qed.
Lemma ent_jokerT W :
(forall W2, order W2 < order W ->
forall U r, closed r -> [ ⊢ r :- U ] -> SUB W2 U r) ->
forall U Ψ, order U < order W -> closed Ψ -> [ ⊢ Ψ :- U ] ->
ENT U (jokerT U) (neu Ψ).
Proof.
move=> ihW U Ψ ???.
apply entails_36; try by [apply closed_jokerT|apply has_type_jokerT
|apply closed_sneu|apply has_type_neu].
move=> l2 hl2.
have hsub: SUB U Void (neu Ψ ∘ l2).
{ apply ihW=>//.
- apply closed_appl; first by apply closed_sneu.
by case: hl2.
- apply aligned_type_void with U=>//.
by apply has_type_neu. }
apply hsub=>//.
right.
apply covers_app_appl.
split; first by apply (covers_neu _ _ _).2.
by apply covers_stack_incl.
Qed.
Lemma stack_rel2_jstack U l :
(forall W Ψ, arg_of W U -> closed Ψ -> [ ⊢ Ψ :- W ] -> ENT W (jokerT W) (neu Ψ)) ->
aligned l U -> stack_rel2 entails U (jstack U l) (neu_stack l).
Proof.
elim: U l=> [|W _ ? ih|? ih] l h;
move: l=> [|[?|r] ?] [hc ht]; try by inv ht.
- by constructor.
- have hl := aligned_cons_r hc ht.
have hcr: closed r by inv hc.
have htr: [ ⊢ r :- W ] by inv ht.
constructor.
+ move=> ξ.
have hj: (jokerT W).|[ren ξ] = jokerT W.
{ by apply closedh_hsubst, closedh_jokerT. }
rewrite /= hj -neu_hsubst_comm.
have hE: ENT W (jokerT W) (neu r.|[ren ξ]).
{ apply h; first by constructor.
- by apply closed_unaffectedh.
- by apply has_type_hsubst_0. }
split=>//.
by rewrite /jokerT (neu_joker Top W).1 neu_idempotent.
+ apply ih=>// ? Ψ ?.
apply h.
by constructor.
- have hl := aligned_cons_t hc ht.
constructor.
apply ih=>// ? Ψ ?.
apply h.
by constructor.
Qed.
Lemma closed_call W f m :
closed f ->
closed (fall m (joker_call Top W f m)).
Proof.
move=> *.
by apply fv_fall, (fv_joker W closed_top).2.
Qed.
Lemma conj_in_call_inst U :
forall l acc W r, aligned l U -> closed r ->
conj_in
(joker_all Top W (Box r.|[ren (+(t_len W + t_len U))])) acc ->
conj_in
(joker_all Top W (Box r.|[ren (+ t_len W)]))
(joker_inst Top U l acc).
Proof.
elim: U=> [|? _ V ih|V ih] l ? W r hl ? h /=.
- move: l hl=> [|[t|?] l] [hc h2]; inv h2.
by rewrite addn0 in h.
- move: l hl=> [|[t|?] l] [hc h2]; try by inv h2.
have hl := aligned_cons_r hc h2.
apply ih=>//.
have hcB: closed
(joker_all Top W (Box r.|[ren (+(t_len W + t_len V))])).
{ apply closed_call, closed_box. by apply closed_unaffectedh. }
by apply (conj_in_subst_closed _ hcB (conj_in_l _ h)).
- move: l hl=> [|[t|?] ?] [hc h2]; try by inv h2.
have hl := aligned_cons_t hc h2.
apply ih=>//.
have e:
(joker_all Top W (Box r.|[ren (+(t_len W + (t_len V).+1))]))
.|[upn (t_len V) (t .: ids)] =
joker_all Top W (Box r.|[ren (+(t_len W + t_len V))]).
{ rewrite fall_hsubst ((joker_hsubst _ closedh_top).2 _ _ _) //=;
last by move=> ??; rewrite upn_k_sigma_x.
rewrite upn_add addnS -add1n ren_upn_subst add0n.
by []. }
rewrite -e.
by apply conj_in_hsubst.
Qed.
Lemma conj_in_joker_call W :
forall l acc s U,
aligned l W ->
List.In (R s) l ->
[ ⊢ s :- U ] ->
conj_in (joker_all Top U (Box s.|[ren (+ t_len U)]))
(joker_inst Top W l acc).
Proof.
elim: W=> [|W _ V ih|V ih] l ? s U hl hin ? /=.
- move: l hl hin=> [|[?|r] l] [hc h] hin; by inv h.
- move: l hl hin=> [|[?|r] l] [hc h] hin; try by inv h.
have hl := aligned_cons_r hc h.
move: hin=> [e|hin]; last by apply ih.
move: e=> [e].
subst.
have hcs: closed s by inv hc.
have htr: [ ⊢ s :- W ] by inv h.
have e: W = U by apply has_type_det with empty_ctx 0 0 s.
subst.
apply conj_in_call_inst=>//.
have hsb := subst_depth_hit V 0 hcs.
rewrite add0n in hsb.
have e:
(joker_all Top U (Var (c_len V)))
.[subst_depth V (Box s .: ids)] =
joker_all Top U (Box s.|[ren (+(t_len U + t_len V))]).
{ rewrite fall_subst ((joker_subst _ closed_top).2 _ _ _) //= hsb /= ren_add.
by rewrite addnC. }
rewrite -e.
by apply conj_in_r, conj_in_here.
- move: l hl hin=> [|[?|?] ?] [hc h] hin; try by inv h.
have hl := aligned_cons_t hc h.
apply ih=>//.
by case: hin.
Qed.
The call applied to the variables and jokers of its signature.
Fixpoint vcall (U : type) (tc : nat) : stack :=
match U with
| Void => [::]
| TArr V => T (TVar tc.-1) :: vcall V tc.-1
| Arr W V => R (jokerT W) :: vcall V tc
end.
Lemma joker_call_appl U :
forall f tc,
joker_call Top U f tc = f ∘ vcall U tc.
Proof.
elim: U=> //= ? _ ? ih ??; by rewrite ih.
Qed.
match U with
| Void => [::]
| TArr V => T (TVar tc.-1) :: vcall V tc.-1
| Arr W V => R (jokerT W) :: vcall V tc
end.
Lemma joker_call_appl U :
forall f tc,
joker_call Top U f tc = f ∘ vcall U tc.
Proof.
elim: U=> //= ? _ ? ih ??; by rewrite ih.
Qed.
The terms of a stack aligned with U.
Fixpoint terms (U : type) (l : stack) : seq term :=
match U, l with
| TArr V, T t :: l2 => t :: terms V l2
| Arr _ V, R _ :: l2 => terms V l2
| _, _ => [::]
end.
Lemma size_terms U :
forall l,
aligned l U ->
size (terms U l) = t_len U.
Proof.
elim: U=> [|? _ ? ih|? ih] l;
move: l=> [|[?|?] ?] [hc h] //=; try by inv h.
- apply ih.
by split; [inv hc|inv h].
- rewrite ih //.
by split; [inv hc|inv h].
Qed.
Lemma vcall_hsubst U :
forall l tc θ, aligned l U -> t_len U <= tc ->
(forall i, i < t_len U -> θ (tc - i.+1) = nth (TVar 0) (terms U l) i) ->
stack_hsubst θ (vcall U tc) = jstack U l.
Proof.
elim: U=> [|W _ V ih|V ih] l tc θ;
move: l=> [|[?|?] l] [hc h] htc hθ //=; try by inv h.
- have hl := aligned_cons_r hc h.
have hj: (jokerT W).|[θ] = jokerT W by apply closedh_hsubst, closedh_jokerT.
by rewrite hj (ih l).
- have hl := aligned_cons_t hc h.
have e0 := hθ 0 erefl.
rewrite /= subn1 in e0.
have htc2: t_len V <= tc.-1 by rewrite -subn1 leq_subRL //; apply: leq_trans htc.
rewrite e0 (ih l) // => i hi.
have := hθ i.+1 hi.
by rewrite -subn1 -subnDA add1n.
Qed.
Lemma joker_call_inst U l s G G2 :
aligned l U ->
closed s -> [ ⊢ s :- U ] ->
eval (joker_all Top U (Box s.|[ren (+ t_len U)])) [::] G ->
eval (s ∘ jstack U l) [::] G2 ->
G ||- G2.
Proof.
move=> hl ?? hG ?.
have [G0 [-> h0]] := eval_fall_inv hG.
rewrite joker_call_appl in h0.
have h1: eval (s.|[ren (+ t_len U)] ∘ vcall U (t_len U)) [::] G0.
{ apply eval_move_stack_left.
move/eval_move_stack_right: h0=> h0.
by inv h0. }
have hsz := size_terms hl.
have h2 := eval_hsubst h1 (inst (terms U l)).
have e: (s.|[ren (+ t_len U)] ∘ vcall U (t_len U)).|[inst (terms U l)] = s ∘ jstack U l.
{ rewrite appl_hsubst (vcall_hsubst hl) //.
- by rewrite -hsz hsubst_comp ren_inst hsubst_id.
- move=> *.
rewrite -{1}hsz inst_nth //.
by rewrite hsz.
}
rewrite e /= in h2.
have hc: complete (s ∘ jstack U l).
{ by apply aligned_complete with U=>//; apply aligned_jstack. }
have eG: G2 = G0.[inst (terms U l)] by apply (uniqueness_eval hc).
rewrite eG -hsz.
by apply valid_fallF_elim.
Qed.
match U, l with
| TArr V, T t :: l2 => t :: terms V l2
| Arr _ V, R _ :: l2 => terms V l2
| _, _ => [::]
end.
Lemma size_terms U :
forall l,
aligned l U ->
size (terms U l) = t_len U.
Proof.
elim: U=> [|? _ ? ih|? ih] l;
move: l=> [|[?|?] ?] [hc h] //=; try by inv h.
- apply ih.
by split; [inv hc|inv h].
- rewrite ih //.
by split; [inv hc|inv h].
Qed.
Lemma vcall_hsubst U :
forall l tc θ, aligned l U -> t_len U <= tc ->
(forall i, i < t_len U -> θ (tc - i.+1) = nth (TVar 0) (terms U l) i) ->
stack_hsubst θ (vcall U tc) = jstack U l.
Proof.
elim: U=> [|W _ V ih|V ih] l tc θ;
move: l=> [|[?|?] l] [hc h] htc hθ //=; try by inv h.
- have hl := aligned_cons_r hc h.
have hj: (jokerT W).|[θ] = jokerT W by apply closedh_hsubst, closedh_jokerT.
by rewrite hj (ih l).
- have hl := aligned_cons_t hc h.
have e0 := hθ 0 erefl.
rewrite /= subn1 in e0.
have htc2: t_len V <= tc.-1 by rewrite -subn1 leq_subRL //; apply: leq_trans htc.
rewrite e0 (ih l) // => i hi.
have := hθ i.+1 hi.
by rewrite -subn1 -subnDA add1n.
Qed.
Lemma joker_call_inst U l s G G2 :
aligned l U ->
closed s -> [ ⊢ s :- U ] ->
eval (joker_all Top U (Box s.|[ren (+ t_len U)])) [::] G ->
eval (s ∘ jstack U l) [::] G2 ->
G ||- G2.
Proof.
move=> hl ?? hG ?.
have [G0 [-> h0]] := eval_fall_inv hG.
rewrite joker_call_appl in h0.
have h1: eval (s.|[ren (+ t_len U)] ∘ vcall U (t_len U)) [::] G0.
{ apply eval_move_stack_left.
move/eval_move_stack_right: h0=> h0.
by inv h0. }
have hsz := size_terms hl.
have h2 := eval_hsubst h1 (inst (terms U l)).
have e: (s.|[ren (+ t_len U)] ∘ vcall U (t_len U)).|[inst (terms U l)] = s ∘ jstack U l.
{ rewrite appl_hsubst (vcall_hsubst hl) //.
- by rewrite -hsz hsubst_comp ren_inst hsubst_id.
- move=> *.
rewrite -{1}hsz inst_nth //.
by rewrite hsz.
}
rewrite e /= in h2.
have hc: complete (s ∘ jstack U l).
{ by apply aligned_complete with U=>//; apply aligned_jstack. }
have eG: G2 = G0.[inst (terms U l)] by apply (uniqueness_eval hc).
rewrite eG -hsz.
by apply valid_fallF_elim.
Qed.
TOPLAS Lemma D.1.1
Lemma d1_1 W :
(forall W2, order W2 < order W ->
forall U r, closed r -> [ ⊢ r :- U ] -> SUB W2 U r) ->
forall r U,
closed r -> [ ⊢ r :- U ] ->
box_rel (submits W) r -> SUB W U r.
Proof.
move=> ihW.
have:
forall n r U,
weight r <= n ->
closed r ->
[ ⊢ r :- U ] ->
box_rel (submits W) r -> SUB W U r.
2: { move=> h r U hc ht h2. by apply (h (weight r) r U). }
elim=>[r U ?|n ih].
(* case {0} *)
{ exfalso. have := weight_pos r. by lia. }
(* case {n.+1} *)
{ case.
(* case {Var x} *)
{ move=> ??? hc *. by apply closed_ids in hc. }
(* case {Zero} *)
{ move=> U ? hc hty hb.
inv hty.
rewrite /SUB/= => l0 hl0 [hm|//].
apply (joker_entails_mem (s:=Zero) hl0)=>//; first by apply ty_zero.
by apply mem_ren_0. }
(* case {Top} *)
{ move=> U ? hc hty hb.
inv hty.
rewrite /SUB/= => l0 hl0 hcov f g hf hg.
inv hg.
by apply valid_top. }
(* case {And s t} *)
{ move=> s t U /= ? /closed_and [? hc2] hty hb.
apply logical_relation_lemma_proj2=>[l hl hcl htl|//].
have hs: SUB W U s.
{ apply ih=>//; first by lia. by inv hty. by inv hb. }
have ht: SUB W U t.
{ apply ih=>//; first by lia. by inv hty. by inv hb. }
have hsl: submits W (s ∘ l).
{ apply logical_relation_lemma_proj1 with U=>//. by inv hty. }
have htl2: submits W (t ∘ l).
{ apply logical_relation_lemma_proj1 with U=>//. by inv hty. }
move=> l0 hl0 hcov f g hf /eval_move_stack_right hg.
inv hg.
move: hcov=> [/mem_ren_0 hm|/covers_app_appl [[hcs hct] hcl0]].
- have hty3: [ ⊢ And s t ∘ l :- Void ] by apply aligned_type_void with U.
apply (joker_entails_mem hl0 hty3 hm hf).
apply eval_move_stack_left.
by constructor.
- apply valid_and_intro.
+ have hcov2: covers l0 0 (s ∘ l).
{ right.
apply covers_app_appl.
split=>//.
by apply covers_below_app. }
apply (hsl l0 hl0 hcov2 f _ hf).
by apply eval_move_stack_left.
+ have hcov2: covers l0 0 (t ∘ l).
{ right.
apply covers_app_appl.
split=>//.
by apply covers_below_app. }
apply (htl2 l0 hl0 hcov2 f _ hf).
by apply eval_move_stack_left. }
(* case {App s t} *)
{ move=> s t V /= ? /closed_app [? hc2] hty hb.
inv hty.
have hs: SUB W (Arr U V) s.
{ apply ih=>//; first by lia. by inv hb. }
apply hs=>// ξ.
have hct: closed t.|[ren ξ] by apply closed_unaffectedh.
have htt: [ ⊢ t.|[ren ξ] :- U ] by apply has_type_hsubst_0.
have hbt: box_rel (submits W) t.|[ren ξ]
by inv hb; apply box_rel_preserved_ren.
split.
- apply ih=>//.
rewrite weight_hsubst.
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.
by lia.
+ by apply closed_sneu.
+ by apply has_type_neu.
+ by apply box_rel_preserved_neu. }
(* case {TApp s S} *)
{ move=> s ? V /= ? /closed_tapp hc hty hb.
inv hty.
have: SUB W (TArr V) s.
{ apply ih=>//. by inv hb. }
by apply. }
(* case {Lam s U} *)
{ move=> s U V /= ? hc hty hb.
inv hty.
rewrite /SUB/= => t ???.
apply logical_relation_lemma_proj2; last by apply ty_app with U=>//; constructor.
move=> l ???.
have hc2: closed s.[Box t/].
{ apply fv1; by [apply closed_lam in hc|apply closed_box]. }
have hty2: [ ⊢ s.[Box t/] :- V0 ].
{ apply has_type_beta with U=>//; by [apply closed_box | constructor]. }
have hs: SUB W V0 s.[Box t/].
{ apply ih=>//.
- have e := weight_subst_box 0 s t.
rewrite upn0 in e.
by rewrite -e.
- inv hb.
by apply box_rel_preserved_subst0 with U. }
have hsl: submits W (s.[Box t/] ∘ l).
{ by apply logical_relation_lemma_proj1 with V0. }
move=> l0 [hcl0 htl0] hcov f g hf /eval_move_stack_right hg.
inv hg.
match goal with h: eval (Lam _ _) _ _ |- _ => inv h end.
move: hcov=> [/mem_ren_0 hm|/covers_app_appl [[hcs hct] ?]].
- have hty3: [ ⊢ App (Lam s U) t ∘ l :- Void ].
{ apply aligned_type_void with V0=>//.
apply ty_app with U=>//.
by constructor. }
apply (joker_entails_mem (conj hcl0 htl0) hty3 hm hf).
apply eval_move_stack_left.
by do 2 constructor.
- have hcov2: covers l0 0 (s.[Box t/] ∘ l).
{ right.
apply covers_app_appl.
split=>//.
apply covers_below_app.
have hsc: sub_cov l0 0 (Box t .: ids) by apply sub_cov_box.
by apply (covers_subst s hcl0 hsc).1. }
apply (hsl l0 (conj hcl0 htl0) hcov2 f _ hf).
by apply eval_move_stack_left. }
(* case {Imp s f} *)
{ move=> s f U /= ? /closed_imp ? hty hb.
have hU: U = Void by inv hty.
have hts: [ ⊢ s :- Void ] by inv hty.
have hs: SUB W Void s.
{ apply ih=>//. by inv hb. }
rewrite /SUB/= in hs *.
rewrite hU in hty *.
move=> l0 hl0 hcov f0 g hf0 hg.
inv hg.
move: hcov=> [/mem_ren_0 hm|hcs].
- apply (joker_entails_mem hl0 hty hm hf0).
by constructor.
- apply valid_imp_intro, valid_weak.
by apply (hs l0 hl0 (or_intror (covers_below_app hcs)) f0 _ hf0). }
(* case {TLam s} *)
{ move=> s V /= ?? hty hb.
inv hty.
rewrite /SUB/= => T.
apply logical_relation_lemma_proj2;
last by apply ty_tapp; [apply fv_plage_eq|apply ty_tlam].
move=> l ???.
have hcs: closed s by apply closed_tlam.
have hcsT: closed s.|[T/] by apply closed_unaffectedh.
have htsT: [ ⊢ s.|[T/] :- U ] by apply has_type_hsubst1.
have hs: SUB W U s.|[T/].
{ apply ih=>//.
- by rewrite weight_hsubst; lia.
- inv hb.
by apply box_rel_preserved_hsubst0 with empty_ctx U 1 1. }
have hsl: submits W (s.|[T/] ∘ l).
{ by apply logical_relation_lemma_proj1 with U. }
move=> l0 [hcl0 htl0] hcov f g hf /eval_move_stack_right hg.
inv hg.
match goal with h: eval (TLam _) _ _ |- _ => inv h end.
move: hcov=> [/mem_ren_0 hm|/covers_app_appl [??]].
- have hty3: [ ⊢ TApp (TLam s) T ∘ l :- Void ].
{ apply aligned_type_void with U=>//.
apply ty_tapp; by [apply fv_plage_eq|apply ty_tlam]. }
apply (joker_entails_mem (conj hcl0 htl0) hty3 hm hf).
apply eval_move_stack_left.
by do 2 constructor.
- have hcov2: covers l0 0 (s.|[T/] ∘ l).
{ right.
apply covers_app_appl.
split=>//.
apply covers_below_app.
by apply covers_below_hsubst0. }
apply (hsl l0 (conj hcl0 htl0) hcov2 f _ hf).
by apply eval_move_stack_left. }
(* case {TAll s} *)
{ move=> s U /= ?? hty hb.
have hU: U = Void by inv hty.
subst.
have hts: [ ⊢ s :- Void ] by apply has_type_lower_1; inv hty.
have hcs: closed s by apply closed_tall.
have hs: SUB W Void s.
{ apply ih=>//. by inv hb. }
rewrite /SUB/= in hs *.
move=> l0 hl0 hcov f g hf hg.
inv hg.
move: hcov=> [/mem_ren_0 hm|?].
- apply (joker_entails_mem hl0 hty hm hf).
by constructor.
- apply valid_all_de_bruijn.
have hl02: aligned (stack_hsubst (ren (+1)) l0) W by apply aligned_hsubst.
have hcov2: covers (stack_hsubst (ren (+1)) l0) 0 s.
{ right.
apply covers_below_app.
by apply (covers_shift l0 s 0).1. }
have hf2: eval (jokerT W ∘ l0).|[ren (+1)] (stack_hsubst (ren (+1)) [::]) f.[ren (+1)]
by apply eval_hsubst.
have hcW: closedh (jokerT W) by apply closedh_jokerT.
rewrite appl_hsubst (closedh_hsubst (ren (+1)) hcW) in hf2.
apply (hs _ hl02 hcov2 _ _ hf2).
by match goal with h: eval s [::] _ |- _ => apply h end. }
(* case {Neu s} *)
{ move=> s U /= ? /closed_neu ? hty hb.
have hts: [ ⊢ s :- U ] by inv hty.
have hbs: box_rel (submits W) s by inv hb.
have hs: SUB W U (neu s).
{ apply ih.
- have:= weight_neu s.
by lia.
- by apply closed_sneu.
- by apply has_type_neu.
- by apply box_rel_preserved_neu. }
apply logical_relation_lemma_proj2=>[l ???|//].
have hsl: submits W (neu s ∘ l).
{ apply logical_relation_lemma_proj1 with U=>//.
by apply has_type_neu. }
move=> l0 hl0 hcov f g hf /eval_move_stack_right hg.
inv hg.
move: hcov=> [/mem_ren_0 hm|/covers_app_appl [_ ?]].
- have hty3: [ ⊢ Neu s ∘ l :- Void ] by apply aligned_type_void with U.
apply (joker_entails_mem hl0 hty3 hm hf).
apply eval_move_stack_left.
by constructor.
- have hcov2: covers l0 0 (neu s ∘ l).
{ right.
apply covers_app_appl.
split=>//.
by apply (covers_neu _ _ _).2. }
apply (hsl l0 hl0 hcov2 f _ hf).
by apply eval_move_stack_left. }
(* case {Box s} *)
{ move=> s U ?? hty hb.
have [V [hcs [hts hls]]] := box_rel_box_ids hb.
have e: V = U by inv hty; apply has_type_det with empty_ctx 0 0 s.
subst.
apply logical_relation_lemma_proj2=>[l ???|//].
have hsl: submits W (s ∘ l).
{ by apply logical_relation_lemma_proj1 with U; first by case: hls. }
have hnl: submits W (neu s ∘ l).
{ apply logical_relation_lemma_proj1 with U=>//; first by case: hls.
by apply has_type_neu. }
have hgl: aligned l U by [].
move=> l0 hl0 hcov f g hf /eval_move_stack_right hg.
inv hg.
have hg2: eval (s ∘ l) [::] g by apply eval_move_stack_left.
move: hcov=> [/mem_ren_0 hm|/covers_app_appl [hcb ?]].
- have hty3: [ ⊢ Box s ∘ l :- Void ] by apply aligned_type_void with U.
apply (joker_entails_mem hl0 hty3 hm hf).
apply eval_move_stack_left.
by constructor.
- move: hcb=> [/mem_ren_0 hin|hcs2].
+ have hc3: complete (s ∘ l) by apply aligned_complete with U.
have hcn: complete (neu s ∘ l).
{ apply aligned_complete with U=>//; by [apply has_type_neu|apply closed_sneu]. }
have hcm: complete (s ∘ neu_stack l).
{ apply aligned_complete with U=>//. by apply aligned_neu. }
have [g1 h1] := eval_def hcn.
have [g2 h2] := eval_def hcm.
have [_ hx] := cross_lemma hc3 hg2 h1 h2.
apply: valid_cut; last by apply hx.
apply valid_and_intro.
* have hcv: covers l0 0 (neu s ∘ l).
{ right.
apply covers_app_appl.
split=>//.
by apply (covers_neu _ _ _).2. }
by apply (hnl l0 hl0 hcv f g1 hf h1).
* have [U2 [hU2 htU2]] := in_aligned_arg hl0 hin.
have e: U2 = U by apply has_type_det with empty_ctx 0 0 s.
subst.
have hf2 := proj1 (eval_joker_abs closed_top closedh_top Top f hl0) hf.
have [G [hG hfG]] := eval_conj_in (conj_in_joker_call Top hl0 hin hts) hf2.
have hcj: complete (s ∘ jstack U l).
{ by apply aligned_complete with U=>//; apply aligned_jstack. }
have [G2 hG2] := eval_def hcj.
have hGG2 := joker_call_inst hgl hcs hts hG hG2.
have hent: entails (s ∘ jstack U l) (s ∘ neu_stack l).
{ apply logical_relation_lemma2_proj1 with U=>//.
- by apply entails_refl.
- apply stack_rel2_jstack=>// ? Ψ ha.
apply (ent_jokerT ihW)=>//.
have := order_arg ha.
have := order_arg hU2.
by lia.
- by apply aligned_jstack.
- by apply aligned_neu. }
apply: valid_cut; first by apply hfG.
apply: valid_cut; first by apply hGG2.
by apply hent.
+ have hcv: covers l0 0 (s ∘ l) by right; apply covers_app_appl.
by apply (hsl l0 hl0 hcv f g hf hg2). }
}
Qed.
(forall W2, order W2 < order W ->
forall U r, closed r -> [ ⊢ r :- U ] -> SUB W2 U r) ->
forall r U,
closed r -> [ ⊢ r :- U ] ->
box_rel (submits W) r -> SUB W U r.
Proof.
move=> ihW.
have:
forall n r U,
weight r <= n ->
closed r ->
[ ⊢ r :- U ] ->
box_rel (submits W) r -> SUB W U r.
2: { move=> h r U hc ht h2. by apply (h (weight r) r U). }
elim=>[r U ?|n ih].
(* case {0} *)
{ exfalso. have := weight_pos r. by lia. }
(* case {n.+1} *)
{ case.
(* case {Var x} *)
{ move=> ??? hc *. by apply closed_ids in hc. }
(* case {Zero} *)
{ move=> U ? hc hty hb.
inv hty.
rewrite /SUB/= => l0 hl0 [hm|//].
apply (joker_entails_mem (s:=Zero) hl0)=>//; first by apply ty_zero.
by apply mem_ren_0. }
(* case {Top} *)
{ move=> U ? hc hty hb.
inv hty.
rewrite /SUB/= => l0 hl0 hcov f g hf hg.
inv hg.
by apply valid_top. }
(* case {And s t} *)
{ move=> s t U /= ? /closed_and [? hc2] hty hb.
apply logical_relation_lemma_proj2=>[l hl hcl htl|//].
have hs: SUB W U s.
{ apply ih=>//; first by lia. by inv hty. by inv hb. }
have ht: SUB W U t.
{ apply ih=>//; first by lia. by inv hty. by inv hb. }
have hsl: submits W (s ∘ l).
{ apply logical_relation_lemma_proj1 with U=>//. by inv hty. }
have htl2: submits W (t ∘ l).
{ apply logical_relation_lemma_proj1 with U=>//. by inv hty. }
move=> l0 hl0 hcov f g hf /eval_move_stack_right hg.
inv hg.
move: hcov=> [/mem_ren_0 hm|/covers_app_appl [[hcs hct] hcl0]].
- have hty3: [ ⊢ And s t ∘ l :- Void ] by apply aligned_type_void with U.
apply (joker_entails_mem hl0 hty3 hm hf).
apply eval_move_stack_left.
by constructor.
- apply valid_and_intro.
+ have hcov2: covers l0 0 (s ∘ l).
{ right.
apply covers_app_appl.
split=>//.
by apply covers_below_app. }
apply (hsl l0 hl0 hcov2 f _ hf).
by apply eval_move_stack_left.
+ have hcov2: covers l0 0 (t ∘ l).
{ right.
apply covers_app_appl.
split=>//.
by apply covers_below_app. }
apply (htl2 l0 hl0 hcov2 f _ hf).
by apply eval_move_stack_left. }
(* case {App s t} *)
{ move=> s t V /= ? /closed_app [? hc2] hty hb.
inv hty.
have hs: SUB W (Arr U V) s.
{ apply ih=>//; first by lia. by inv hb. }
apply hs=>// ξ.
have hct: closed t.|[ren ξ] by apply closed_unaffectedh.
have htt: [ ⊢ t.|[ren ξ] :- U ] by apply has_type_hsubst_0.
have hbt: box_rel (submits W) t.|[ren ξ]
by inv hb; apply box_rel_preserved_ren.
split.
- apply ih=>//.
rewrite weight_hsubst.
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.
by lia.
+ by apply closed_sneu.
+ by apply has_type_neu.
+ by apply box_rel_preserved_neu. }
(* case {TApp s S} *)
{ move=> s ? V /= ? /closed_tapp hc hty hb.
inv hty.
have: SUB W (TArr V) s.
{ apply ih=>//. by inv hb. }
by apply. }
(* case {Lam s U} *)
{ move=> s U V /= ? hc hty hb.
inv hty.
rewrite /SUB/= => t ???.
apply logical_relation_lemma_proj2; last by apply ty_app with U=>//; constructor.
move=> l ???.
have hc2: closed s.[Box t/].
{ apply fv1; by [apply closed_lam in hc|apply closed_box]. }
have hty2: [ ⊢ s.[Box t/] :- V0 ].
{ apply has_type_beta with U=>//; by [apply closed_box | constructor]. }
have hs: SUB W V0 s.[Box t/].
{ apply ih=>//.
- have e := weight_subst_box 0 s t.
rewrite upn0 in e.
by rewrite -e.
- inv hb.
by apply box_rel_preserved_subst0 with U. }
have hsl: submits W (s.[Box t/] ∘ l).
{ by apply logical_relation_lemma_proj1 with V0. }
move=> l0 [hcl0 htl0] hcov f g hf /eval_move_stack_right hg.
inv hg.
match goal with h: eval (Lam _ _) _ _ |- _ => inv h end.
move: hcov=> [/mem_ren_0 hm|/covers_app_appl [[hcs hct] ?]].
- have hty3: [ ⊢ App (Lam s U) t ∘ l :- Void ].
{ apply aligned_type_void with V0=>//.
apply ty_app with U=>//.
by constructor. }
apply (joker_entails_mem (conj hcl0 htl0) hty3 hm hf).
apply eval_move_stack_left.
by do 2 constructor.
- have hcov2: covers l0 0 (s.[Box t/] ∘ l).
{ right.
apply covers_app_appl.
split=>//.
apply covers_below_app.
have hsc: sub_cov l0 0 (Box t .: ids) by apply sub_cov_box.
by apply (covers_subst s hcl0 hsc).1. }
apply (hsl l0 (conj hcl0 htl0) hcov2 f _ hf).
by apply eval_move_stack_left. }
(* case {Imp s f} *)
{ move=> s f U /= ? /closed_imp ? hty hb.
have hU: U = Void by inv hty.
have hts: [ ⊢ s :- Void ] by inv hty.
have hs: SUB W Void s.
{ apply ih=>//. by inv hb. }
rewrite /SUB/= in hs *.
rewrite hU in hty *.
move=> l0 hl0 hcov f0 g hf0 hg.
inv hg.
move: hcov=> [/mem_ren_0 hm|hcs].
- apply (joker_entails_mem hl0 hty hm hf0).
by constructor.
- apply valid_imp_intro, valid_weak.
by apply (hs l0 hl0 (or_intror (covers_below_app hcs)) f0 _ hf0). }
(* case {TLam s} *)
{ move=> s V /= ?? hty hb.
inv hty.
rewrite /SUB/= => T.
apply logical_relation_lemma_proj2;
last by apply ty_tapp; [apply fv_plage_eq|apply ty_tlam].
move=> l ???.
have hcs: closed s by apply closed_tlam.
have hcsT: closed s.|[T/] by apply closed_unaffectedh.
have htsT: [ ⊢ s.|[T/] :- U ] by apply has_type_hsubst1.
have hs: SUB W U s.|[T/].
{ apply ih=>//.
- by rewrite weight_hsubst; lia.
- inv hb.
by apply box_rel_preserved_hsubst0 with empty_ctx U 1 1. }
have hsl: submits W (s.|[T/] ∘ l).
{ by apply logical_relation_lemma_proj1 with U. }
move=> l0 [hcl0 htl0] hcov f g hf /eval_move_stack_right hg.
inv hg.
match goal with h: eval (TLam _) _ _ |- _ => inv h end.
move: hcov=> [/mem_ren_0 hm|/covers_app_appl [??]].
- have hty3: [ ⊢ TApp (TLam s) T ∘ l :- Void ].
{ apply aligned_type_void with U=>//.
apply ty_tapp; by [apply fv_plage_eq|apply ty_tlam]. }
apply (joker_entails_mem (conj hcl0 htl0) hty3 hm hf).
apply eval_move_stack_left.
by do 2 constructor.
- have hcov2: covers l0 0 (s.|[T/] ∘ l).
{ right.
apply covers_app_appl.
split=>//.
apply covers_below_app.
by apply covers_below_hsubst0. }
apply (hsl l0 (conj hcl0 htl0) hcov2 f _ hf).
by apply eval_move_stack_left. }
(* case {TAll s} *)
{ move=> s U /= ?? hty hb.
have hU: U = Void by inv hty.
subst.
have hts: [ ⊢ s :- Void ] by apply has_type_lower_1; inv hty.
have hcs: closed s by apply closed_tall.
have hs: SUB W Void s.
{ apply ih=>//. by inv hb. }
rewrite /SUB/= in hs *.
move=> l0 hl0 hcov f g hf hg.
inv hg.
move: hcov=> [/mem_ren_0 hm|?].
- apply (joker_entails_mem hl0 hty hm hf).
by constructor.
- apply valid_all_de_bruijn.
have hl02: aligned (stack_hsubst (ren (+1)) l0) W by apply aligned_hsubst.
have hcov2: covers (stack_hsubst (ren (+1)) l0) 0 s.
{ right.
apply covers_below_app.
by apply (covers_shift l0 s 0).1. }
have hf2: eval (jokerT W ∘ l0).|[ren (+1)] (stack_hsubst (ren (+1)) [::]) f.[ren (+1)]
by apply eval_hsubst.
have hcW: closedh (jokerT W) by apply closedh_jokerT.
rewrite appl_hsubst (closedh_hsubst (ren (+1)) hcW) in hf2.
apply (hs _ hl02 hcov2 _ _ hf2).
by match goal with h: eval s [::] _ |- _ => apply h end. }
(* case {Neu s} *)
{ move=> s U /= ? /closed_neu ? hty hb.
have hts: [ ⊢ s :- U ] by inv hty.
have hbs: box_rel (submits W) s by inv hb.
have hs: SUB W U (neu s).
{ apply ih.
- have:= weight_neu s.
by lia.
- by apply closed_sneu.
- by apply has_type_neu.
- by apply box_rel_preserved_neu. }
apply logical_relation_lemma_proj2=>[l ???|//].
have hsl: submits W (neu s ∘ l).
{ apply logical_relation_lemma_proj1 with U=>//.
by apply has_type_neu. }
move=> l0 hl0 hcov f g hf /eval_move_stack_right hg.
inv hg.
move: hcov=> [/mem_ren_0 hm|/covers_app_appl [_ ?]].
- have hty3: [ ⊢ Neu s ∘ l :- Void ] by apply aligned_type_void with U.
apply (joker_entails_mem hl0 hty3 hm hf).
apply eval_move_stack_left.
by constructor.
- have hcov2: covers l0 0 (neu s ∘ l).
{ right.
apply covers_app_appl.
split=>//.
by apply (covers_neu _ _ _).2. }
apply (hsl l0 hl0 hcov2 f _ hf).
by apply eval_move_stack_left. }
(* case {Box s} *)
{ move=> s U ?? hty hb.
have [V [hcs [hts hls]]] := box_rel_box_ids hb.
have e: V = U by inv hty; apply has_type_det with empty_ctx 0 0 s.
subst.
apply logical_relation_lemma_proj2=>[l ???|//].
have hsl: submits W (s ∘ l).
{ by apply logical_relation_lemma_proj1 with U; first by case: hls. }
have hnl: submits W (neu s ∘ l).
{ apply logical_relation_lemma_proj1 with U=>//; first by case: hls.
by apply has_type_neu. }
have hgl: aligned l U by [].
move=> l0 hl0 hcov f g hf /eval_move_stack_right hg.
inv hg.
have hg2: eval (s ∘ l) [::] g by apply eval_move_stack_left.
move: hcov=> [/mem_ren_0 hm|/covers_app_appl [hcb ?]].
- have hty3: [ ⊢ Box s ∘ l :- Void ] by apply aligned_type_void with U.
apply (joker_entails_mem hl0 hty3 hm hf).
apply eval_move_stack_left.
by constructor.
- move: hcb=> [/mem_ren_0 hin|hcs2].
+ have hc3: complete (s ∘ l) by apply aligned_complete with U.
have hcn: complete (neu s ∘ l).
{ apply aligned_complete with U=>//; by [apply has_type_neu|apply closed_sneu]. }
have hcm: complete (s ∘ neu_stack l).
{ apply aligned_complete with U=>//. by apply aligned_neu. }
have [g1 h1] := eval_def hcn.
have [g2 h2] := eval_def hcm.
have [_ hx] := cross_lemma hc3 hg2 h1 h2.
apply: valid_cut; last by apply hx.
apply valid_and_intro.
* have hcv: covers l0 0 (neu s ∘ l).
{ right.
apply covers_app_appl.
split=>//.
by apply (covers_neu _ _ _).2. }
by apply (hnl l0 hl0 hcv f g1 hf h1).
* have [U2 [hU2 htU2]] := in_aligned_arg hl0 hin.
have e: U2 = U by apply has_type_det with empty_ctx 0 0 s.
subst.
have hf2 := proj1 (eval_joker_abs closed_top closedh_top Top f hl0) hf.
have [G [hG hfG]] := eval_conj_in (conj_in_joker_call Top hl0 hin hts) hf2.
have hcj: complete (s ∘ jstack U l).
{ by apply aligned_complete with U=>//; apply aligned_jstack. }
have [G2 hG2] := eval_def hcj.
have hGG2 := joker_call_inst hgl hcs hts hG hG2.
have hent: entails (s ∘ jstack U l) (s ∘ neu_stack l).
{ apply logical_relation_lemma2_proj1 with U=>//.
- by apply entails_refl.
- apply stack_rel2_jstack=>// ? Ψ ha.
apply (ent_jokerT ihW)=>//.
have := order_arg ha.
have := order_arg hU2.
by lia.
- by apply aligned_jstack.
- by apply aligned_neu. }
apply: valid_cut; first by apply hfG.
apply: valid_cut; first by apply hGG2.
by apply hent.
+ have hcv: covers l0 0 (s ∘ l) by right; apply covers_app_appl.
by apply (hsl l0 hl0 hcv f g hf hg2). }
}
Qed.
Lemma d1 W U r :
closed r -> [ ⊢ r :- U ] ->
SUB W U r.
Proof.
have inner: forall W,
(forall W3, order W3 < order W ->
forall U1 r1, closed r1 -> [ ⊢ r1 :- U1 ] -> SUB W3 U1 r1) ->
forall n r0 U0, depth r0 <= n -> closed r0 -> [ ⊢ r0 :- U0 ] -> SUB W U0 r0.
{ move=> W3 ihW.
elim=>[|n ih] r0 U0 ? hc ht.
(* case {0} *)
- apply d1_1=>//.
apply box_rel_nobox, mem_box_depth.
have := depth_nonneg r0.
by lia.
(* case {n.+1} *)
- apply d1_1=>//.
apply unfold_box_rel with empty_ctx U0 0 0=>// s V ?? ξ.
have hcs: closed s by apply directly_box_closed with r0 U0 empty_ctx 0 0.
have hds: depth s <= n by apply directly_box_depth with r0.
have hcξ: closed s.|[ren ξ] by apply closed_unaffectedh.
have htξ: [ ⊢ s.|[ren ξ] :- V ] by apply has_type_hsubst_0.
split.
+ apply ih=>//.
by rewrite depth_hsubst.
+ apply ih.
* by rewrite -depth_neu depth_hsubst.
* by apply closed_sneu.
* by apply has_type_neu. }
have outer: forall k W, order W < k ->
forall U r, closed r -> [ ⊢ r :- U ] -> SUB W U r.
{ elim=>[|? ihk] W3 ? U3 r3 ??; first by lia.
have ihW: forall W2, order W2 < order W3 ->
forall U2 r2, closed r2 -> [ ⊢ r2 :- U2 ] -> SUB W2 U2 r2.
{ move=> W2 ?????.
apply (ihk W2)=>//.
by lia. }
by apply (inner W3 ihW (depth r3) r3 U3). }
move=> *.
by apply (outer (order W).+1 W).
Qed.
Lemma conj_in_leaf z U :
forall l acc u,
aligned l U ->
closed u -> closedh u ->
conj_in u acc ->
conj_in u (joker_inst z U l acc).
Proof.
elim: U=> [|W _ V ih|V ih] l acc u hl hcu hhu h /=.
- by move: l hl=> [|[t|?] l] [hc h2].
- move: l hl=> [|[t|?] l] [hc h2]; try by inv h2.
have hl := aligned_cons_r hc h2.
apply ih=>//.
by apply (conj_in_subst_closed _ hcu
(conj_in_l (joker_all z W (Var (c_len V))) h)).
- move: l hl=> [|[t|?] ?] [hc h2]; try by inv h2.
have hl := aligned_cons_t hc h2.
apply ih=>//.
have h3: conj_in u.|[upn (t_len V) (t .: ids)] acc.|[upn (t_len V) (t .: ids)]
by apply (conj_in_hsubst _ h).
by rewrite (closedh_hsubst _ hhu) in h3.
Qed.
Lemma joker_bot U l F :
aligned l U ->
eval (joker U ∘ l) [::] F ->
F ||- FBot.
Proof.
move=> hl hf.
have hz: closed Zero by [].
have hzh: closedh Zero by [].
have hf2 := proj1 (eval_joker_abs hz hzh Zero F hl) hf.
have hc: conj_in Zero (joker_inst Zero U l Zero)
by apply conj_in_leaf=>//; apply conj_in_here.
have [G [hG hFG]] := eval_conj_in hc hf2.
by inv hG.
Qed.
Lemma stack_rel_submits W U l :
aligned l U ->
stack_rel (submits W) U l.
Proof.
elim: U l=> [|U2 _ ? ih|? ih] l;
move: l=> [|[?|r] ?] [hc h]; try by inv h.
- by constructor.
- have hl := aligned_cons_r hc h.
have hcr: closed r by inv hc.
have htr: [ ⊢ r :- U2 ] by inv h.
constructor; last by apply ih.
move=> ξ.
have hcξ: closed r.|[ren ξ] by apply closed_unaffectedh.
have htξ: [ ⊢ r.|[ren ξ] :- U2 ] by apply has_type_hsubst_0.
split; apply d1=>//; by [apply closed_sneu|apply has_type_neu].
- have hl := aligned_cons_t hc h.
constructor. by apply ih.
Qed.
closed r -> [ ⊢ r :- U ] ->
SUB W U r.
Proof.
have inner: forall W,
(forall W3, order W3 < order W ->
forall U1 r1, closed r1 -> [ ⊢ r1 :- U1 ] -> SUB W3 U1 r1) ->
forall n r0 U0, depth r0 <= n -> closed r0 -> [ ⊢ r0 :- U0 ] -> SUB W U0 r0.
{ move=> W3 ihW.
elim=>[|n ih] r0 U0 ? hc ht.
(* case {0} *)
- apply d1_1=>//.
apply box_rel_nobox, mem_box_depth.
have := depth_nonneg r0.
by lia.
(* case {n.+1} *)
- apply d1_1=>//.
apply unfold_box_rel with empty_ctx U0 0 0=>// s V ?? ξ.
have hcs: closed s by apply directly_box_closed with r0 U0 empty_ctx 0 0.
have hds: depth s <= n by apply directly_box_depth with r0.
have hcξ: closed s.|[ren ξ] by apply closed_unaffectedh.
have htξ: [ ⊢ s.|[ren ξ] :- V ] by apply has_type_hsubst_0.
split.
+ apply ih=>//.
by rewrite depth_hsubst.
+ apply ih.
* by rewrite -depth_neu depth_hsubst.
* by apply closed_sneu.
* by apply has_type_neu. }
have outer: forall k W, order W < k ->
forall U r, closed r -> [ ⊢ r :- U ] -> SUB W U r.
{ elim=>[|? ihk] W3 ? U3 r3 ??; first by lia.
have ihW: forall W2, order W2 < order W3 ->
forall U2 r2, closed r2 -> [ ⊢ r2 :- U2 ] -> SUB W2 U2 r2.
{ move=> W2 ?????.
apply (ihk W2)=>//.
by lia. }
by apply (inner W3 ihW (depth r3) r3 U3). }
move=> *.
by apply (outer (order W).+1 W).
Qed.
Lemma conj_in_leaf z U :
forall l acc u,
aligned l U ->
closed u -> closedh u ->
conj_in u acc ->
conj_in u (joker_inst z U l acc).
Proof.
elim: U=> [|W _ V ih|V ih] l acc u hl hcu hhu h /=.
- by move: l hl=> [|[t|?] l] [hc h2].
- move: l hl=> [|[t|?] l] [hc h2]; try by inv h2.
have hl := aligned_cons_r hc h2.
apply ih=>//.
by apply (conj_in_subst_closed _ hcu
(conj_in_l (joker_all z W (Var (c_len V))) h)).
- move: l hl=> [|[t|?] ?] [hc h2]; try by inv h2.
have hl := aligned_cons_t hc h2.
apply ih=>//.
have h3: conj_in u.|[upn (t_len V) (t .: ids)] acc.|[upn (t_len V) (t .: ids)]
by apply (conj_in_hsubst _ h).
by rewrite (closedh_hsubst _ hhu) in h3.
Qed.
Lemma joker_bot U l F :
aligned l U ->
eval (joker U ∘ l) [::] F ->
F ||- FBot.
Proof.
move=> hl hf.
have hz: closed Zero by [].
have hzh: closedh Zero by [].
have hf2 := proj1 (eval_joker_abs hz hzh Zero F hl) hf.
have hc: conj_in Zero (joker_inst Zero U l Zero)
by apply conj_in_leaf=>//; apply conj_in_here.
have [G [hG hFG]] := eval_conj_in hc hf2.
by inv hG.
Qed.
Lemma stack_rel_submits W U l :
aligned l U ->
stack_rel (submits W) U l.
Proof.
elim: U l=> [|U2 _ ? ih|? ih] l;
move: l=> [|[?|r] ?] [hc h]; try by inv h.
- by constructor.
- have hl := aligned_cons_r hc h.
have hcr: closed r by inv hc.
have htr: [ ⊢ r :- U2 ] by inv h.
constructor; last by apply ih.
move=> ξ.
have hcξ: closed r.|[ren ξ] by apply closed_unaffectedh.
have htξ: [ ⊢ r.|[ren ξ] :- U2 ] by apply has_type_hsubst_0.
split; apply d1=>//; by [apply closed_sneu|apply has_type_neu].
- have hl := aligned_cons_t hc h.
constructor. by apply ih.
Qed.
TOPLAS Theorem 3.11
Theorem joker_entails U r :
closed r -> [ ⊢ r :- U ] ->
strongly2 (ENT U) (joker U) r.
Proof.
move=> hc ht.
split.
- apply entails_36;
try by [apply closed_joker|apply has_type_joker|apply hc|apply ht].
move=> l hl ?? hf ?.
apply: valid_cut; first by apply (joker_bot hl hf).
by apply valid_contradiction.
- rewrite /strongly2.
have hcj: closed (joker U) by apply closed_joker.
have htj: [ ⊢ joker U :- U ] by apply has_type_joker.
apply entails_36;
try by [apply closed_sneu|apply has_type_neu].
move=> l hl.
rewrite neu_joker_top.
change (entails (jokerT U ∘ l) (neu r ∘ l)).
have hsub: submits U (neu r ∘ l).
{ apply logical_relation_lemma_proj1 with U.
- apply d1; by [apply closed_sneu|apply has_type_neu].
- by apply has_type_neu.
- by apply stack_rel_submits.
- by case: hl.
- by case: hl. }
apply hsub=>//.
right.
apply covers_app_appl.
split; first by apply (covers_neu _ _ _).2.
by apply covers_stack_incl.
Qed.
closed r -> [ ⊢ r :- U ] ->
strongly2 (ENT U) (joker U) r.
Proof.
move=> hc ht.
split.
- apply entails_36;
try by [apply closed_joker|apply has_type_joker|apply hc|apply ht].
move=> l hl ?? hf ?.
apply: valid_cut; first by apply (joker_bot hl hf).
by apply valid_contradiction.
- rewrite /strongly2.
have hcj: closed (joker U) by apply closed_joker.
have htj: [ ⊢ joker U :- U ] by apply has_type_joker.
apply entails_36;
try by [apply closed_sneu|apply has_type_neu].
move=> l hl.
rewrite neu_joker_top.
change (entails (jokerT U ∘ l) (neu r ∘ l)).
have hsub: submits U (neu r ∘ l).
{ apply logical_relation_lemma_proj1 with U.
- apply d1; by [apply closed_sneu|apply has_type_neu].
- by apply has_type_neu.
- by apply stack_rel_submits.
- by case: hl.
- by case: hl. }
apply hsub=>//.
right.
apply covers_app_appl.
split; first by apply (covers_neu _ _ _).2.
by apply covers_stack_incl.
Qed.