Rocoma.Recipes_stacks
Reserved Notation "s ∘ l" (at level 60, format "s ∘ l").
s ∘ [l1,…,ln] is a left-associative application chain.
Fixpoint appl s l :=
match l with
| [::] => s
| (T t) :: ls => (TApp s t) ∘ ls
| (R t) :: ls => (App s t) ∘ ls
end
where "s ∘ l" := (appl s l).
Reserved Notation "[ Γ , a , b ⊨ l :- U ]" (format "[ Γ , a , b ⊨ l :- U ]").
Reserved Notation "[ ⊨ l :- U ]" (format "[ ⊨ l :- U ]").
Inductive stack_has_type (Γ : ctx) (a b : nat) : stack -> type -> Prop :=
| stack_has_type_void :
[ Γ, a, b ⊨ [::] :- Void ]
| stack_has_type_term s l V :
fv_plage a b s ->
[ Γ, a, b ⊨ l :- V ] ->
[ Γ, a, b ⊨ (T s :: l) :- TArr V ]
| stack_has_type_recipe s U l V :
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a, b ⊨ l :- V ] ->
[ Γ, a, b ⊨ (R s :: l) :- Arr U V ]
where "[ Γ , a , b ⊨ l :- U ]" := (stack_has_type Γ a b l U) : ty_scope.
Notation "[ ⊨ l :- U ]" := (stack_has_type empty_ctx 0 0 l U) : ty_scope.
Lemma void_stack l Γ a b :
[ Γ, a, b ⊨ l :- Void ] -> l = [::].
Proof.
by move=> h; inv h.
Qed.
match l with
| [::] => s
| (T t) :: ls => (TApp s t) ∘ ls
| (R t) :: ls => (App s t) ∘ ls
end
where "s ∘ l" := (appl s l).
Reserved Notation "[ Γ , a , b ⊨ l :- U ]" (format "[ Γ , a , b ⊨ l :- U ]").
Reserved Notation "[ ⊨ l :- U ]" (format "[ ⊨ l :- U ]").
Inductive stack_has_type (Γ : ctx) (a b : nat) : stack -> type -> Prop :=
| stack_has_type_void :
[ Γ, a, b ⊨ [::] :- Void ]
| stack_has_type_term s l V :
fv_plage a b s ->
[ Γ, a, b ⊨ l :- V ] ->
[ Γ, a, b ⊨ (T s :: l) :- TArr V ]
| stack_has_type_recipe s U l V :
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a, b ⊨ l :- V ] ->
[ Γ, a, b ⊨ (R s :: l) :- Arr U V ]
where "[ Γ , a , b ⊨ l :- U ]" := (stack_has_type Γ a b l U) : ty_scope.
Notation "[ ⊨ l :- U ]" := (stack_has_type empty_ctx 0 0 l U) : ty_scope.
Lemma void_stack l Γ a b :
[ Γ, a, b ⊨ l :- Void ] -> l = [::].
Proof.
by move=> h; inv h.
Qed.
discriminate-like series
Lemma appl_not_var x s t S l :
~ Var x = TApp s S ∘ l
/\ ~ Var x = App s t ∘ l.
Proof.
elim: l s x t S =>/=.
{ by move=> >; split; discriminate. }
{ case=>/=.
+ move=> S l ih s x u T; split.
by move: (ih (TApp s T) x s S)=> [] h1 h2.
by move: (ih (App s u) x s S)=> [] h1 h2.
+ move=> r l ih s x t T; split.
by move: (ih (TApp s T) x r T)=> [] h1 h2.
by move: (ih (App s t) x r T)=> [] h1 h2. }
Qed.
Lemma appl_not_zero s t S l :
~ Zero = TApp s S ∘ l
/\ ~ Zero = App s t ∘ l.
Proof.
elim: l s t S =>/=.
{ by move=> >; split; discriminate. }
{ case=>/=.
+ move=> S l ih s u T; split.
by move: (ih (TApp s T) s S)=> [] h1 h2.
by move: (ih (App s u) s S)=> [] h1 h2.
+ move=> r l ih s t T; split.
by move: (ih (TApp s T) r T)=> [] h1 h2.
by move: (ih (App s t) r T)=> [] h1 h2. }
Qed.
Lemma appl_not_top s t S l :
~ Top = TApp s S ∘ l
/\ ~ Top = App s t ∘ l.
Proof.
elim: l s t S =>/=.
{ by move=> >; split; discriminate. }
{ case=>/=.
+ move=> S l ih s u T; split.
by move: (ih (TApp s T) s S)=> [] h1 h2.
by move: (ih (App s u) s S)=> [] h1 h2.
+ move=> r l ih s t T; split.
by move: (ih (TApp s T) r T)=> [] h1 h2.
by move: (ih (App s t) r T)=> [] h1 h2. }
Qed.
Lemma appl_not_lam u f s t S l :
~ Lam u f = TApp s S ∘ l
/\ ~ Lam u f = App s t ∘ l.
Proof.
elim: l u f s t S =>/=.
{ by move=> >; split; discriminate. }
{ case=>/=.
+ move=> S l ih u f s r T; split.
by move: (ih u f (TApp s T) s S)=> [] h1 h2.
by move: (ih u f (App s r) s S)=> [] h1 h2.
+ move=> r l ih u f s t T; split.
by move: (ih u f (TApp s T) r T)=> [] h1 h2.
by move: (ih u f (App s t) r T)=> [] h1 h2. }
Qed.
Lemma appl_not_imp u f s t S l :
~ Imp u f = TApp s S ∘ l
/\ ~ Imp u f = App s t ∘ l.
Proof.
elim: l u f s t S =>/=.
{ by move=> >; split; discriminate. }
{ case=>/=.
+ move=> S l ih u f s r T; split.
by move: (ih u f (TApp s T) s S)=> [] h1 h2.
by move: (ih u f (App s r) s S)=> [] h1 h2.
+ move=> r l ih u f s t T; split.
by move: (ih u f (TApp s T) r T)=> [] h1 h2.
by move: (ih u f (App s t) r T)=> [] h1 h2. }
Qed.
Lemma appl_not_and u w s t S l :
~ And u w = TApp s S ∘ l
/\ ~ And u w = App s t ∘ l.
Proof.
elim: l u w s t S =>/=.
{ by move=> >; split; discriminate. }
{ case=>/=.
+ move=> S l ih u w s r T; split.
by move: (ih u w (TApp s T) s S)=> [] h1 h2.
by move: (ih u w (App s r) s S)=> [] h1 h2.
+ move=> r l ih u w s t T; split.
by move: (ih u w (TApp s T) r T)=> [] h1 h2.
by move: (ih u w (App s t) r T)=> [] h1 h2. }
Qed.
Lemma appl_not_box u s t S l :
~ Box u = TApp s S ∘ l
/\ ~ Box u = App s t ∘ l.
Proof.
elim: l u s t S =>/=.
{ by move=> >; split; discriminate. }
{ case=>/=.
+ move=> S l ih u s r T; split.
by move: (ih u (TApp s T) s S)=> [] h1 h2.
by move: (ih u (App s r) s S)=> [] h1 h2.
+ move=> r l ih u s t T; split.
by move: (ih u (TApp s T) r T)=> [] h1 h2.
by move: (ih u (App s t) r T)=> [] h1 h2. }
Qed.
Lemma appl_not_neu u s t S l :
~ Neu u = TApp s S ∘ l
/\ ~ Neu u = App s t ∘ l.
Proof.
elim: l u s t S =>/=.
{ by move=> >; split; discriminate. }
{ case=>/=.
+ move=> S l ih u s r T; split.
by move: (ih u (TApp s T) s S)=> [] h1 h2.
by move: (ih u (App s r) s S)=> [] h1 h2.
+ move=> r l ih u s t T; split.
by move: (ih u (TApp s T) r T)=> [] h1 h2.
by move: (ih u (App s t) r T)=> [] h1 h2. }
Qed.
Lemma appl_not_tlam u s t S l :
~ TLam u = TApp s S ∘ l
/\ ~ TLam u = App s t ∘ l.
Proof.
elim: l u s t S =>/=.
{ by move=> >; split; discriminate. }
{ case=>/=.
+ move=> S l ih u s r T; split.
by move: (ih u (TApp s T) s S)=> [] h1 h2.
by move: (ih u (App s r) s S)=> [] h1 h2.
+ move=> r l ih u s t T; split.
by move: (ih u (TApp s T) r T)=> [] h1 h2.
by move: (ih u (App s t) r T)=> [] h1 h2. }
Qed.
The function to_stacks s compute the pair (u,l) where u is
the left-most non-(T)App subrecipe of s and l the stack to be applied
in order to reform the initial s.
Fixpoint to_stack_rec u l :=
match u with
| App s t => to_stack_rec s ((R t) :: l)
| TApp s t => to_stack_rec s ((T t) :: l)
| _ => (u, l)
end.
Definition to_stack (s: recipe) := to_stack_rec s [::].
simpl is now authorized to unfold to_stack.
Arguments to_stack _ /.
Lemma to_stack_l u l :
(to_stack_rec u l).1 = (to_stack u).1.
Proof.
by elim: u l=>//=; etransitivity.
Qed.
Lemma to_stack_l u l :
(to_stack_rec u l).1 = (to_stack u).1.
Proof.
by elim: u l=>//=; etransitivity.
Qed.
Minimality argument
Lemma to_stack_idempotent :
forall u,
(to_stack u).1 = (to_stack (to_stack u).1).1.
Proof.
by elim=>//= *; rewrite !to_stack_l.
Qed.
Lemma to_stack_idempotent2 u l:
(to_stack_rec u l).1 = (to_stack_rec (to_stack u).1 l).1.
Proof.
by elim: u l=>//= *; rewrite !to_stack_l; exact: to_stack_idempotent.
Qed.
Lemma to_stack_r s l1 l2 :
(to_stack_rec (to_stack_rec s l1).1 l2).2 = l2.
Proof.
by elim: s l1 l2=>/=.
Qed.
Lemma appl_one_step s l t :
s ∘ (l ++ (cons (R t) nil)) = App (s ∘ l) t.
Proof.
elim: l s t=>// -[].
{ move=> t l h u s.
by rewrite -[RHS]/(App ((TApp u t) ∘ l) s) -h. }
{ move=> s l h u t.
by rewrite -[RHS]/(App ((App u s) ∘ l) t) -h. }
Qed.
Lemma appl_one_stept s l t :
s ∘ (l ++ (cons (T t) nil)) = TApp (s ∘ l) t.
Proof.
elim: l s t=>// -[].
{ move=> t l h u s.
by rewrite -[RHS]/(TApp ((TApp u t) ∘ l) s) -h. }
{ move=> s l h u t.
by rewrite -[RHS]/(TApp ((App u s) ∘ l) t) -h. }
Qed.
Lemma to_stack_appl s l :
to_stack_rec (s ∘ l) [::] = to_stack_rec s l.
Proof.
by elim: l s=>//= -[].
Qed.
Lemma unfold_to_stack_2 s l1 l2:
(to_stack s).2 ++ l1 ++ l2 = (to_stack_rec s l1).2 ++ l2.
Proof.
elim: s l1 l2=>//.
{ move=> s hs t _ l1 l2.
set l3 := l1 ++ l2.
rewrite /to_stack/=.
rewrite -(hs [:: R t] l3).
rewrite -(hs (R t :: l1) l2).
by f_equal. }
{ move=> s hs S l1 l2.
set l3 := l1 ++ l2.
rewrite /to_stack/=.
rewrite -(hs [:: T S] l3).
rewrite -(hs (T S :: l1) l2).
by f_equal. }
Qed.
Corollary unfold_to_stack_2_corr s a l:
(to_stack s).2 ++ a :: l = (to_stack_rec s [:: a]).2 ++ l.
Proof.
by rewrite (unfold_to_stack_2 s [:: a] l).
Qed.
Lemma to_stack_appl_cat s l :
(to_stack s).2 ++ l = (to_stack (s ∘ l)).2.
Proof.
rewrite/to_stack/= to_stack_appl.
rewrite -(cats0 (to_stack_rec s l).2).
rewrite -(unfold_to_stack_2 _ l).
by rewrite cats0.
Qed.
Lemma stack_form s :
s = appl (to_stack s).1
(to_stack s).2.
Proof.
elim: s=>//.
- move=> s.
set s1:= (to_stack s).1.
set s2:= (to_stack s).2.
move=> -> t ht.
rewrite -appl_one_step.
f_equal=>/=.
+ by rewrite to_stack_appl -to_stack_idempotent2 to_stack_l.
+ by rewrite to_stack_appl /s1 to_stack_r.
- move=> s.
set s1:= (to_stack s).1.
set s2:= (to_stack s).2.
move=> -> S.
rewrite -appl_one_stept.
f_equal=>/=.
+ by rewrite to_stack_appl -to_stack_idempotent2 to_stack_l.
+ by rewrite to_stack_appl /s1 to_stack_r.
Qed.
Lemma surjective_to_stack s :
to_stack s = ((to_stack s).1, (to_stack s).2).
Proof.
exact: surjective_pairing.
Qed.
Corollary surjective_to_stack2 s :
((to_stack s).1, (to_stack s).2) = to_stack s.
Proof.
by rewrite {3}surjective_to_stack.
Qed.
Fixpoint neu_stack l :=
match l with
| [::] => [::]
| R r :: l => R (neu r) :: neu_stack l
| T s :: l => T s :: neu_stack l
end.
Lemma neu_stack_lemma s l :
neu (s ∘ l) = neu s ∘ neu_stack l.
Proof.
elim: l s=>//.
case=>/= a l h s.
by rewrite h.
by rewrite h.
Qed.
Lemma neu_stack_idempotent l :
neu_stack (neu_stack l) = neu_stack l.
Proof.
elim: l=>// -[]/= > -> //.
by rewrite neu_idempotent.
Qed.
Inductive closed_stack : stack -> Prop :=
| closed_stack_empty : closed_stack [::]
| closed_stack_recipe r l :
closed r ->
closed_stack l ->
closed_stack (R r :: l)
| closed_stack_term s l :
closed_stack l ->
closed_stack (T s :: l).
Lemma closed_appl r l :
closed r ->
closed_stack l ->
closed (r ∘ l).
Proof.
elim: l r=>//.
move=> []a l h1 r h2 h3 /=; inv h3; apply h1=>//.
- by apply closed_tapp.
- by apply closed_app.
Qed.
Lemma closed_appl_inv_strong r l :
closed (r ∘ l) ->
closed r /\ closed (neu r) /\ closed_stack l /\ closed_stack (neu_stack l).
Proof.
elim: l r.
- move=> r /=; repeat split=>//.
by apply closed_sneu.
by constructor.
by constructor.
- move=> []a l h1 r h2=>/=; repeat split.
+ apply h1 in h2 as [h3 _].
simpl in h3.
by apply closed_tapp in h3.
+ apply h1 in h2 as [_ [h3 _]].
simpl in h3.
by apply closed_tapp in h3.
+ apply h1 in h2 as [h3 [h4 [h5 h6]]].
by constructor.
+ constructor.
by apply h1 in h2 as [_ [_ [_ ?]]].
+ apply h1 in h2 as [h3 [h4 [h5 h6]]].
simpl in h3.
by apply closed_app in h3 as [? _].
+ apply h1 in h2 as [h3 _].
apply closed_app in h3 as [h7 _].
by apply closed_sneu.
+ apply h1 in h2 as [h3 [_ [??]]].
constructor=>//.
by apply closed_app in h3 as [_ ?].
+ apply h1 in h2 as [h3 [_ [??]]].
constructor=>//.
apply closed_app in h3 as [_ ?].
by apply closed_sneu.
Qed.
Lemma closed_appl_neu_head r l :
closed (r ∘ l) ->
closed (neu r ∘ l).
Proof.
move/closed_appl_inv_strong=> [? [? [? ?]]].
by apply closed_appl.
Qed.
Lemma closed_appl_neu_stack r l :
closed (r ∘ l) ->
closed (r ∘ neu_stack l).
Proof.
move/closed_appl_inv_strong=> [? [? [? ?]]].
by apply closed_appl.
Qed.
Lemma has_type_appl_void r l Γ a b :
[ Γ, a, b ⊢ r ∘ l :- Void ] ->
exists V, [ Γ, a, b ⊢ r :- V ] /\ [ Γ, a, b ⊨ l :- V ].
Proof.
elim: l r Γ.
- move=> r Γ /= ?. exists Void. split=>//. by constructor.
- move=> []c l h1 r Γ /= ht.
+ apply h1 in ht as [V [ht2 ?]].
inv ht2.
exists (TArr V).
split=>//.
by constructor.
+ apply h1 in ht as [V [ht2 ?]].
inv ht2.
exists (Arr U V).
split=>//.
by constructor.
Qed.
Lemma has_type_appl r l Γ U a b :
[ Γ, a, b ⊢ r ∘ l :- U ] ->
exists V, [ Γ, a, b ⊢ r :- V ].
Proof.
elim: l r U Γ.
- move=> r U Γ /= ?. by exists U.
- move=> []c l h1 r U Γ /= ht.
+ apply h1 in ht as [V ht2].
inv ht2.
by exists (TArr V).
+ apply h1 in ht as [V ht2].
inv ht2.
by exists (Arr U0 V).
Qed.
Lemma has_type_appl2 r l Γ U a b :
[ Γ, a, b ⊢ r ∘ l :- U ] ->
exists V, [ Γ, a, b ⊨ l :- V ].
Proof.
elim: l r U Γ.
- move=> *.
exists Void.
by constructor.
- move=> []c l h1 r Z Γ /= ht.
+ have ht3:= ht.
apply h1 in ht as [V ht2].
apply has_type_appl in ht3 as [VV ht3].
inv ht3.
exists (TArr V).
by constructor.
+ have[V ht2]:= h1 _ _ _ ht.
have[W ht3]:= has_type_appl ht.
inv ht3.
exists (Arr U V).
by constructor.
Qed.
Corollary has_type_appl_neu_head_ex r l Γ U a b :
[ Γ, a, b ⊢ r ∘ l :- U ] ->
exists V, [ Γ, a, b ⊢ neu r :- V ].
Proof.
move/has_type_appl=> [V ht].
exists V.
by apply has_type_neu.
Qed.
Lemma has_type_appl2_neu r l Γ U a b :
[ Γ, a, b ⊢ r ∘ l :- U ] ->
exists V, [ Γ, a, b ⊨ (neu_stack l) :- V ].
Proof.
elim: l r U Γ.
- move=> *.
exists Void.
by constructor.
- move=> []c l h1 r Z Γ /= ht.
+ have ht3:= ht.
apply h1 in ht as [V ht2].
apply has_type_appl in ht3 as [VV ht3].
inv ht3.
exists (TArr V).
by constructor.
+ have[V ht2]:= h1 _ _ _ ht.
have[W ht3]:= has_type_appl ht.
inv ht3.
exists (Arr U V).
constructor=>//.
by apply has_type_neu.
Qed.
Corollary has_type_appl_hole r s l Γ U V a b :
[ Γ, a, b ⊢ r :- U ] ->
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a, b ⊢ r ∘ l :- V ] ->
[ Γ, a, b ⊢ s ∘ l :- V ].
Proof.
elim: l r s Γ U V=>//.
- move=> r s Γ U V h1 h2 /= h3.
have ?:= has_type_det h1 h3.
by subst.
- move=> []c l h1 r s Γ V W h2 h3 /= h4.
+ have[U h]:= has_type_appl h4.
inv h.
have ?:= has_type_det h2 H3.
subst.
apply h1 with (TApp r c) U=>//.
by constructor.
by constructor.
+ have[Z h]:= has_type_appl h4.
inv h.
have ?:= has_type_det h2 H1.
subst.
apply h1 with (App r c) Z=>//.
by apply ty_app with U.
by apply ty_app with U.
Qed.
Corollary has_type_appl2_hole r p l Γ U V a b :
[ Γ, a, b ⊨ l :- V ] ->
[ Γ, a, b ⊨ p :- V ] ->
[ Γ, a, b ⊢ r ∘ l :- U ] ->
[ Γ, a, b ⊢ r ∘ p :- U ].
Proof.
elim: l p r Γ U V=>//.
- move=> > h1 h2. inv h1. inv h2. done.
- move=> []c ll ih p r Γ U W hl hp /= ht.
+ inv hl. inv hp. simpl.
apply ih with V=>//.
have[Z hz]:=has_type_appl ht.
apply has_type_appl_hole with (TApp r c) Z=>//.
inv hz.
by constructor.
+ inv hl. inv hp. simpl.
apply ih with V=>//.
have[Z hz]:=has_type_appl ht.
apply has_type_appl_hole with (App r c) Z=>//.
inv hz.
apply ty_app with U1=>//.
by have <-:= has_type_det H1 H7.
Qed.
Corollary has_type_appl_neu_head r l Γ U a b :
[ Γ, a, b ⊢ r ∘ l :- U ] ->
[ Γ, a, b ⊢ neu r ∘ l :- U ].
Proof.
move=> h.
have[V h2]:= has_type_appl h.
apply has_type_appl_hole with r V=>//.
by apply has_type_neu.
Qed.
Lemma has_type_appl_neu_stack r l Γ U a b :
[ Γ, a, b ⊢ r ∘ l :- U ] ->
[ Γ, a, b ⊢ r ∘ neu_stack l :- U ].
Proof.
move=> h.
have[V h2]:= has_type_appl2 h.
apply has_type_appl2_hole with l V=>//.
clear_except h2.
elim: l V h2.
- move=> > h. inv h. by constructor.
- move=> []c l h1 U h /=; inv h.
+ constructor=>//. by apply h1.
+ constructor.
by apply has_type_neu.
by apply h1.
Qed.
Lemma closed_stack_in S t :
closed_stack S ->
List.In (R t) S ->
closed t.
Proof.
elim=> //= [r l hr _ ih [e|h]|s2 l _ ih [//|h]]; by [case: e=> <-|apply ih].
Qed.
Fixpoint stack_hsubst (θ : var -> term) (l : stack) : stack :=
match l with
| [::] => [::]
| T t :: l => T t.[θ] :: stack_hsubst θ l
| R r :: l => R r.|[θ] :: stack_hsubst θ l
end.
Lemma appl_hsubst θ s l :
(s ∘ l).|[θ] = s.|[θ] ∘ stack_hsubst θ l.
Proof.
elim: l s=> [|[?|?] ? ih] ? //=; by rewrite ih.
Qed.
Lemma closed_stack_hsubst θ l :
closed_stack l ->
closed_stack (stack_hsubst θ l).
Proof.
elim=> /=.
- by constructor.
- move=> ??? _ ?.
constructor=>//.
by apply closed_unaffectedh.
- move=> ?? _ ?.
by constructor.
Qed.
Lemma stack_has_type_hsubst θ l U :
[ ⊨ l :- U ] ->
[ ⊨ stack_hsubst θ l :- U ].
Proof.
elim=> /=.
- by constructor.
- move=> ??? _ _ ?.
by constructor.
- move=> ????? _ ?.
constructor=>//.
by apply has_type_hsubst_0.
Qed.
Lemma in_stack_hsubst θ S t :
List.In (R t) S ->
List.In (R t.|[θ]) (stack_hsubst θ S).
Proof.
elim: S=> //= -[?|?] ? ih [e|?]; try by right; apply ih.
move: e=> [<-].
by left.
Qed.
Print Assumptions has_type_appl_neu_stack.
forall u,
(to_stack u).1 = (to_stack (to_stack u).1).1.
Proof.
by elim=>//= *; rewrite !to_stack_l.
Qed.
Lemma to_stack_idempotent2 u l:
(to_stack_rec u l).1 = (to_stack_rec (to_stack u).1 l).1.
Proof.
by elim: u l=>//= *; rewrite !to_stack_l; exact: to_stack_idempotent.
Qed.
Lemma to_stack_r s l1 l2 :
(to_stack_rec (to_stack_rec s l1).1 l2).2 = l2.
Proof.
by elim: s l1 l2=>/=.
Qed.
Lemma appl_one_step s l t :
s ∘ (l ++ (cons (R t) nil)) = App (s ∘ l) t.
Proof.
elim: l s t=>// -[].
{ move=> t l h u s.
by rewrite -[RHS]/(App ((TApp u t) ∘ l) s) -h. }
{ move=> s l h u t.
by rewrite -[RHS]/(App ((App u s) ∘ l) t) -h. }
Qed.
Lemma appl_one_stept s l t :
s ∘ (l ++ (cons (T t) nil)) = TApp (s ∘ l) t.
Proof.
elim: l s t=>// -[].
{ move=> t l h u s.
by rewrite -[RHS]/(TApp ((TApp u t) ∘ l) s) -h. }
{ move=> s l h u t.
by rewrite -[RHS]/(TApp ((App u s) ∘ l) t) -h. }
Qed.
Lemma to_stack_appl s l :
to_stack_rec (s ∘ l) [::] = to_stack_rec s l.
Proof.
by elim: l s=>//= -[].
Qed.
Lemma unfold_to_stack_2 s l1 l2:
(to_stack s).2 ++ l1 ++ l2 = (to_stack_rec s l1).2 ++ l2.
Proof.
elim: s l1 l2=>//.
{ move=> s hs t _ l1 l2.
set l3 := l1 ++ l2.
rewrite /to_stack/=.
rewrite -(hs [:: R t] l3).
rewrite -(hs (R t :: l1) l2).
by f_equal. }
{ move=> s hs S l1 l2.
set l3 := l1 ++ l2.
rewrite /to_stack/=.
rewrite -(hs [:: T S] l3).
rewrite -(hs (T S :: l1) l2).
by f_equal. }
Qed.
Corollary unfold_to_stack_2_corr s a l:
(to_stack s).2 ++ a :: l = (to_stack_rec s [:: a]).2 ++ l.
Proof.
by rewrite (unfold_to_stack_2 s [:: a] l).
Qed.
Lemma to_stack_appl_cat s l :
(to_stack s).2 ++ l = (to_stack (s ∘ l)).2.
Proof.
rewrite/to_stack/= to_stack_appl.
rewrite -(cats0 (to_stack_rec s l).2).
rewrite -(unfold_to_stack_2 _ l).
by rewrite cats0.
Qed.
Lemma stack_form s :
s = appl (to_stack s).1
(to_stack s).2.
Proof.
elim: s=>//.
- move=> s.
set s1:= (to_stack s).1.
set s2:= (to_stack s).2.
move=> -> t ht.
rewrite -appl_one_step.
f_equal=>/=.
+ by rewrite to_stack_appl -to_stack_idempotent2 to_stack_l.
+ by rewrite to_stack_appl /s1 to_stack_r.
- move=> s.
set s1:= (to_stack s).1.
set s2:= (to_stack s).2.
move=> -> S.
rewrite -appl_one_stept.
f_equal=>/=.
+ by rewrite to_stack_appl -to_stack_idempotent2 to_stack_l.
+ by rewrite to_stack_appl /s1 to_stack_r.
Qed.
Lemma surjective_to_stack s :
to_stack s = ((to_stack s).1, (to_stack s).2).
Proof.
exact: surjective_pairing.
Qed.
Corollary surjective_to_stack2 s :
((to_stack s).1, (to_stack s).2) = to_stack s.
Proof.
by rewrite {3}surjective_to_stack.
Qed.
Fixpoint neu_stack l :=
match l with
| [::] => [::]
| R r :: l => R (neu r) :: neu_stack l
| T s :: l => T s :: neu_stack l
end.
Lemma neu_stack_lemma s l :
neu (s ∘ l) = neu s ∘ neu_stack l.
Proof.
elim: l s=>//.
case=>/= a l h s.
by rewrite h.
by rewrite h.
Qed.
Lemma neu_stack_idempotent l :
neu_stack (neu_stack l) = neu_stack l.
Proof.
elim: l=>// -[]/= > -> //.
by rewrite neu_idempotent.
Qed.
Inductive closed_stack : stack -> Prop :=
| closed_stack_empty : closed_stack [::]
| closed_stack_recipe r l :
closed r ->
closed_stack l ->
closed_stack (R r :: l)
| closed_stack_term s l :
closed_stack l ->
closed_stack (T s :: l).
Lemma closed_appl r l :
closed r ->
closed_stack l ->
closed (r ∘ l).
Proof.
elim: l r=>//.
move=> []a l h1 r h2 h3 /=; inv h3; apply h1=>//.
- by apply closed_tapp.
- by apply closed_app.
Qed.
Lemma closed_appl_inv_strong r l :
closed (r ∘ l) ->
closed r /\ closed (neu r) /\ closed_stack l /\ closed_stack (neu_stack l).
Proof.
elim: l r.
- move=> r /=; repeat split=>//.
by apply closed_sneu.
by constructor.
by constructor.
- move=> []a l h1 r h2=>/=; repeat split.
+ apply h1 in h2 as [h3 _].
simpl in h3.
by apply closed_tapp in h3.
+ apply h1 in h2 as [_ [h3 _]].
simpl in h3.
by apply closed_tapp in h3.
+ apply h1 in h2 as [h3 [h4 [h5 h6]]].
by constructor.
+ constructor.
by apply h1 in h2 as [_ [_ [_ ?]]].
+ apply h1 in h2 as [h3 [h4 [h5 h6]]].
simpl in h3.
by apply closed_app in h3 as [? _].
+ apply h1 in h2 as [h3 _].
apply closed_app in h3 as [h7 _].
by apply closed_sneu.
+ apply h1 in h2 as [h3 [_ [??]]].
constructor=>//.
by apply closed_app in h3 as [_ ?].
+ apply h1 in h2 as [h3 [_ [??]]].
constructor=>//.
apply closed_app in h3 as [_ ?].
by apply closed_sneu.
Qed.
Lemma closed_appl_neu_head r l :
closed (r ∘ l) ->
closed (neu r ∘ l).
Proof.
move/closed_appl_inv_strong=> [? [? [? ?]]].
by apply closed_appl.
Qed.
Lemma closed_appl_neu_stack r l :
closed (r ∘ l) ->
closed (r ∘ neu_stack l).
Proof.
move/closed_appl_inv_strong=> [? [? [? ?]]].
by apply closed_appl.
Qed.
Lemma has_type_appl_void r l Γ a b :
[ Γ, a, b ⊢ r ∘ l :- Void ] ->
exists V, [ Γ, a, b ⊢ r :- V ] /\ [ Γ, a, b ⊨ l :- V ].
Proof.
elim: l r Γ.
- move=> r Γ /= ?. exists Void. split=>//. by constructor.
- move=> []c l h1 r Γ /= ht.
+ apply h1 in ht as [V [ht2 ?]].
inv ht2.
exists (TArr V).
split=>//.
by constructor.
+ apply h1 in ht as [V [ht2 ?]].
inv ht2.
exists (Arr U V).
split=>//.
by constructor.
Qed.
Lemma has_type_appl r l Γ U a b :
[ Γ, a, b ⊢ r ∘ l :- U ] ->
exists V, [ Γ, a, b ⊢ r :- V ].
Proof.
elim: l r U Γ.
- move=> r U Γ /= ?. by exists U.
- move=> []c l h1 r U Γ /= ht.
+ apply h1 in ht as [V ht2].
inv ht2.
by exists (TArr V).
+ apply h1 in ht as [V ht2].
inv ht2.
by exists (Arr U0 V).
Qed.
Lemma has_type_appl2 r l Γ U a b :
[ Γ, a, b ⊢ r ∘ l :- U ] ->
exists V, [ Γ, a, b ⊨ l :- V ].
Proof.
elim: l r U Γ.
- move=> *.
exists Void.
by constructor.
- move=> []c l h1 r Z Γ /= ht.
+ have ht3:= ht.
apply h1 in ht as [V ht2].
apply has_type_appl in ht3 as [VV ht3].
inv ht3.
exists (TArr V).
by constructor.
+ have[V ht2]:= h1 _ _ _ ht.
have[W ht3]:= has_type_appl ht.
inv ht3.
exists (Arr U V).
by constructor.
Qed.
Corollary has_type_appl_neu_head_ex r l Γ U a b :
[ Γ, a, b ⊢ r ∘ l :- U ] ->
exists V, [ Γ, a, b ⊢ neu r :- V ].
Proof.
move/has_type_appl=> [V ht].
exists V.
by apply has_type_neu.
Qed.
Lemma has_type_appl2_neu r l Γ U a b :
[ Γ, a, b ⊢ r ∘ l :- U ] ->
exists V, [ Γ, a, b ⊨ (neu_stack l) :- V ].
Proof.
elim: l r U Γ.
- move=> *.
exists Void.
by constructor.
- move=> []c l h1 r Z Γ /= ht.
+ have ht3:= ht.
apply h1 in ht as [V ht2].
apply has_type_appl in ht3 as [VV ht3].
inv ht3.
exists (TArr V).
by constructor.
+ have[V ht2]:= h1 _ _ _ ht.
have[W ht3]:= has_type_appl ht.
inv ht3.
exists (Arr U V).
constructor=>//.
by apply has_type_neu.
Qed.
Corollary has_type_appl_hole r s l Γ U V a b :
[ Γ, a, b ⊢ r :- U ] ->
[ Γ, a, b ⊢ s :- U ] ->
[ Γ, a, b ⊢ r ∘ l :- V ] ->
[ Γ, a, b ⊢ s ∘ l :- V ].
Proof.
elim: l r s Γ U V=>//.
- move=> r s Γ U V h1 h2 /= h3.
have ?:= has_type_det h1 h3.
by subst.
- move=> []c l h1 r s Γ V W h2 h3 /= h4.
+ have[U h]:= has_type_appl h4.
inv h.
have ?:= has_type_det h2 H3.
subst.
apply h1 with (TApp r c) U=>//.
by constructor.
by constructor.
+ have[Z h]:= has_type_appl h4.
inv h.
have ?:= has_type_det h2 H1.
subst.
apply h1 with (App r c) Z=>//.
by apply ty_app with U.
by apply ty_app with U.
Qed.
Corollary has_type_appl2_hole r p l Γ U V a b :
[ Γ, a, b ⊨ l :- V ] ->
[ Γ, a, b ⊨ p :- V ] ->
[ Γ, a, b ⊢ r ∘ l :- U ] ->
[ Γ, a, b ⊢ r ∘ p :- U ].
Proof.
elim: l p r Γ U V=>//.
- move=> > h1 h2. inv h1. inv h2. done.
- move=> []c ll ih p r Γ U W hl hp /= ht.
+ inv hl. inv hp. simpl.
apply ih with V=>//.
have[Z hz]:=has_type_appl ht.
apply has_type_appl_hole with (TApp r c) Z=>//.
inv hz.
by constructor.
+ inv hl. inv hp. simpl.
apply ih with V=>//.
have[Z hz]:=has_type_appl ht.
apply has_type_appl_hole with (App r c) Z=>//.
inv hz.
apply ty_app with U1=>//.
by have <-:= has_type_det H1 H7.
Qed.
Corollary has_type_appl_neu_head r l Γ U a b :
[ Γ, a, b ⊢ r ∘ l :- U ] ->
[ Γ, a, b ⊢ neu r ∘ l :- U ].
Proof.
move=> h.
have[V h2]:= has_type_appl h.
apply has_type_appl_hole with r V=>//.
by apply has_type_neu.
Qed.
Lemma has_type_appl_neu_stack r l Γ U a b :
[ Γ, a, b ⊢ r ∘ l :- U ] ->
[ Γ, a, b ⊢ r ∘ neu_stack l :- U ].
Proof.
move=> h.
have[V h2]:= has_type_appl2 h.
apply has_type_appl2_hole with l V=>//.
clear_except h2.
elim: l V h2.
- move=> > h. inv h. by constructor.
- move=> []c l h1 U h /=; inv h.
+ constructor=>//. by apply h1.
+ constructor.
by apply has_type_neu.
by apply h1.
Qed.
Lemma closed_stack_in S t :
closed_stack S ->
List.In (R t) S ->
closed t.
Proof.
elim=> //= [r l hr _ ih [e|h]|s2 l _ ih [//|h]]; by [case: e=> <-|apply ih].
Qed.
Fixpoint stack_hsubst (θ : var -> term) (l : stack) : stack :=
match l with
| [::] => [::]
| T t :: l => T t.[θ] :: stack_hsubst θ l
| R r :: l => R r.|[θ] :: stack_hsubst θ l
end.
Lemma appl_hsubst θ s l :
(s ∘ l).|[θ] = s.|[θ] ∘ stack_hsubst θ l.
Proof.
elim: l s=> [|[?|?] ? ih] ? //=; by rewrite ih.
Qed.
Lemma closed_stack_hsubst θ l :
closed_stack l ->
closed_stack (stack_hsubst θ l).
Proof.
elim=> /=.
- by constructor.
- move=> ??? _ ?.
constructor=>//.
by apply closed_unaffectedh.
- move=> ?? _ ?.
by constructor.
Qed.
Lemma stack_has_type_hsubst θ l U :
[ ⊨ l :- U ] ->
[ ⊨ stack_hsubst θ l :- U ].
Proof.
elim=> /=.
- by constructor.
- move=> ??? _ _ ?.
by constructor.
- move=> ????? _ ?.
constructor=>//.
by apply has_type_hsubst_0.
Qed.
Lemma in_stack_hsubst θ S t :
List.In (R t) S ->
List.In (R t.|[θ]) (stack_hsubst θ S).
Proof.
elim: S=> //= -[?|?] ? ih [e|?]; try by right; apply ih.
move: e=> [<-].
by left.
Qed.
Print Assumptions has_type_appl_neu_stack.