Rocoma.Recipes_eval
Ltac tac_neu :=
first [ by apply closed_sneu
| by apply closedh_sneu
| by apply has_type_neu ].
Ltac htac_neu_ r U :=
have[??]: closed (neu r) /\ [ ⊢ neu r :- U ]
by split; tac_neu.
From Ltac2 Require Import Ltac2.
From Ltac2 Require Ltac1 List Option.
Set Default Proof Mode "Classic".
Ltac2 rec htac_neu u l :=
match l with
| [] => ()
| x :: l => ltac1:(x u |- htac_neu_ x u) x u; htac_neu u l
end.
Tactic Notation "htac_neu" constr(u) constr_list_sep(l, ",") :=
let g := ltac2:(u l |- Option.may (htac_neu u) (Ltac1.to_list l)) in
g u l.
Section Eval.
eval r l f is the inductive form of the
recipe evaluation procedure denoted ⟦ r ∘ l ⟧ = f in the paper
Inductive eval : recipe -> stack -> term -> Prop :=
| eval_zero :
eval Zero [::] FBot
| eval_top :
eval Top [::] FTop
| eval_imp s1 s2 f :
eval s1 [::] s2 ->
eval (Imp s1 f) [::] (FImp f s2)
| eval_and s1 s2 t1 t2 l :
eval s1 l s2 ->
eval t1 l t2 ->
eval (And s1 t1) l (FAnd s2 t2)
| eval_box s1 s2 l :
eval s1 l s2 ->
eval (Box s1) l s2
| eval_neu s s2 l :
eval (neu s) l s2 ->
eval (Neu s) l s2
| eval_tlam s1 s2 s l :
eval s1.|[s/] l s2 ->
eval (TLam s1) (T s :: l) s2
| eval_tall s1 s2 :
eval s1 [::] s2 ->
eval (TAll s1) [::] (FAll s2)
| eval_lam s1 s2 U r l :
eval s1.[Box r/] l s2 -> (* due to this case, we can't make it functionnal without a complicated proof *)
eval (Lam s1 U) (R r :: l) s2
| eval_app s t s2 l :
eval s (R t :: l) s2 ->
eval (App s t) l s2
| eval_tapp s t s2 l :
eval s (T t :: l) s2 ->
eval (TApp s t) l s2.
Lemma eval_eval0 s l f :
eval s l f <-> eval (to_stack s).1 ((to_stack s).2 ++ l) f.
Proof.
elim: s l f=>//=.
{ move=> s hs t ht l f.
rewrite /to_stack /= to_stack_l.
have e: (to_stack s).2 ++ R t :: l = (to_stack_rec s [:: R t]).2 ++ l.
{ exact: unfold_to_stack_2_corr. }
split=> h.
+ inv h. rewrite -e. by apply hs.
+ constructor. apply hs. by rewrite e. }
{ move=> s hs S l f.
rewrite /to_stack /= to_stack_l.
have e: (to_stack s).2 ++ T S :: l = (to_stack_rec s [:: T S]).2 ++ l.
{ exact: unfold_to_stack_2_corr. }
split=> h.
+ inv h. rewrite -e. by apply hs.
+ constructor. apply hs. by rewrite e. }
Qed.
Corollary eval_eval0_1 s l f :
eval (s ∘ l) [::] f <-> eval (to_stack s).1 ((to_stack s).2 ++ l) f.
Proof.
rewrite to_stack_appl_cat.
have->: (to_stack (s ∘ l)).2 = (to_stack (s ∘ l)).2 ++ [::] by rewrite cats0.
have->: (to_stack s).1 = (to_stack (s ∘ l)).1 by rewrite /to_stack to_stack_appl !to_stack_l.
by apply eval_eval0.
Qed.
Corollary eval_eval0_2 s f :
eval s [::] f <-> eval (to_stack s).1 ((to_stack s).2) f.
Proof.
have->: (to_stack s).2 = (to_stack s).2 ++ [::] by rewrite cats0.
by apply eval_eval0_1 with (l:=[::]).
Qed.
Corollary eval_move_stack s f l :
eval (s ∘ l) [::] f <-> eval s l f.
Proof.
by rewrite eval_eval0_1 -eval_eval0.
Qed.
Corollary eval_move_stack_right s f l :
eval (s ∘ l) [::] f -> eval s l f.
Proof.
by rewrite eval_eval0_1 -eval_eval0.
Qed.
Corollary eval_move_stack_left s f l :
eval s l f -> eval (s ∘ l) [::] f.
Proof.
by rewrite eval_eval0_1 -eval_eval0.
Qed.
box_rel from typing, by induction on the depth.
Lemma inner2g P :
(forall r U,
closed r -> [ ⊢ r :- U ] -> box_rel P r -> logrel P U r) ->
forall r U,
closed r -> [ ⊢ r :- U ] -> box_rel P r.
Proof.
move=> inner1.
have: forall n r Γ U a b,
depth r <= n ->
closed r ->
[ Γ, a, b ⊢ r :- U ] ->
box_rel P r.
2: { move=> h r U hc ht.
by apply (h (depth r) r empty_ctx U 0 0). }
elim.
(* depth zero: no box at all *)
{ move=> r Γ U a b hd _ _.
apply box_rel_nobox, mem_box_depth.
have := depth_nonneg r.
by lia. }
{ move=> n ih r Γ U a b hd hc ht.
apply unfold_box_rel with Γ U a b=>//.
move=> s V hdb hts ξ.
have hds := directly_box_depth hd hdb.
have hcs: closed s by apply directly_box_closed with r U Γ a b.
have hcsξ: closed s.|[ren ξ] by apply closed_unaffectedh.
have htsξ: [ ⊢ s.|[ren ξ] :- V ] by apply has_type_hsubst_0.
have hbs: box_rel P s.|[ren ξ].
{ apply ih with (Γ := empty_ctx) (U := V) (a := 0) (b := 0)=>//.
by rewrite depth_hsubst. }
split.
- exact: inner1.
- apply closed_sneu in hcsξ.
apply has_type_neu in htsξ.
apply box_rel_preserved_neu in hbs.
exact: inner1. }
Qed.
(forall r U,
closed r -> [ ⊢ r :- U ] -> box_rel P r -> logrel P U r) ->
forall r U,
closed r -> [ ⊢ r :- U ] -> box_rel P r.
Proof.
move=> inner1.
have: forall n r Γ U a b,
depth r <= n ->
closed r ->
[ Γ, a, b ⊢ r :- U ] ->
box_rel P r.
2: { move=> h r U hc ht.
by apply (h (depth r) r empty_ctx U 0 0). }
elim.
(* depth zero: no box at all *)
{ move=> r Γ U a b hd _ _.
apply box_rel_nobox, mem_box_depth.
have := depth_nonneg r.
by lia. }
{ move=> n ih r Γ U a b hd hc ht.
apply unfold_box_rel with Γ U a b=>//.
move=> s V hdb hts ξ.
have hds := directly_box_depth hd hdb.
have hcs: closed s by apply directly_box_closed with r U Γ a b.
have hcsξ: closed s.|[ren ξ] by apply closed_unaffectedh.
have htsξ: [ ⊢ s.|[ren ξ] :- V ] by apply has_type_hsubst_0.
have hbs: box_rel P s.|[ren ξ].
{ apply ih with (Γ := empty_ctx) (U := V) (a := 0) (b := 0)=>//.
by rewrite depth_hsubst. }
split.
- exact: inner1.
- apply closed_sneu in hcsξ.
apply has_type_neu in htsξ.
apply box_rel_preserved_neu in hbs.
exact: inner1. }
Qed.
totality
Definition tractable s := ex (eval s [::]).
Definition TRAC U := logrel tractable U.
Lemma inner1 :
forall r U,
closed r -> [ ⊢ r :- U ] ->
box_rel tractable r -> TRAC U r.
Proof.
(* We prove this lemma by induction over the weight r. *)
have:
forall n r U,
weight r <= n ->
closed r ->
[ ⊢ r :- U ] ->
box_rel tractable r -> TRAC U r.
(* The latter generalization subsumes the lemma. *)
2: { move=> h r U hc ht h2. by apply (h (weight r) r U). }
(* Now we prove it by induction over a bound of
the weight of the recipe r. *)
elim=>[r U hw|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=> ??? h3 ?. inv h3=>/=. exists FBot. by constructor. }
(* case {Top} *)
{ move=> ??? h3 ?. inv h3=>/=. exists FTop. by constructor. }
(* case {And s t} *)
{ move=> s t U /= hw /closed_and [hc1 hc2] hty hb.
apply logical_relation_lemma_proj2=>[l hl hcl htl|//].
have ts: TRAC U s.
{ apply ih=>//; first by lia. by inv hty. by inv hb. }
have tt: TRAC U t.
{ apply ih=>//; first by lia. by inv hty. by inv hb. }
have[sl h1]: tractable (s ∘ l).
{ apply logical_relation_lemma_proj1 with U=>//. by inv hty. }
have[tl h2]: tractable (t ∘ l).
{ apply logical_relation_lemma_proj1 with U=>//. by inv hty. }
econstructor.
apply eval_eval0_2=>/=.
rewrite /to_stack/= to_stack_appl /=.
constructor.
+ rewrite eval_eval0_1 in h1.
apply eval_eval0.
exact: h1.
+ rewrite eval_eval0_1 in h2.
apply eval_eval0.
exact: h2. }
(* case {App s t} *)
{ move=> s t W /= hw /closed_app [hc1 hc2] hty hb.
inv hty.
have hs: TRAC (Arr U W) s.
{ apply ih=>//; first by lia. by inv hb. }
apply hs=>//.
move=> ξ.
have hct: closed t.|[ren ξ] by apply closed_unaffectedh.
have htt: [ ⊢ t.|[ren ξ] :- U ] by apply has_type_hsubst_0.
have hbt: box_rel tractable 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 T} *)
{ move=> s S W /= hw /closed_tapp hc hty hb.
inv hty.
have: TRAC (TArr W) s.
{ apply ih=>//. by inv hb. }
by apply. }
(* case {Lam s U} *)
{ move=> s U W /= hw hc hty hb.
inv hty.
rewrite /TRAC/= => t hct htt hst.
apply logical_relation_lemma_proj2.
- move=> l hl hcl htl.
have[res hres]: tractable (s.[Box t/] ∘ l).
{ have hc2: closed s.[Box t/].
{ apply fv1.
by apply closed_lam in hc.
by apply closed_box. }
have hty1: [ ⊢ Box t :- U ] by constructor.
have hty2: [ ⊢ s.[Box t/] :- V ].
{ apply has_type_beta with U=>//. by apply closed_box. }
apply logical_relation_lemma_proj1 with V=>//.
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. }
exists res.
apply eval_eval0_1=>/=.
constructor.
apply eval_eval0_1 in hres.
by apply eval_eval0.
- apply ty_app with U=>//.
by constructor. }
(* case {Imp s f} *)
{ move=> s f ? /= hw /closed_imp hc hty hb.
inv hty.
have: TRAC Void s.
{ apply ih=>//. by inv hb. }
rewrite/TRAC/=.
move=> [y ?].
exists (FImp f y).
by constructor. }
(* case {TLam s} *)
{ move=> s W /= hw hc hty hb.
inv hty.
rewrite /TRAC/= => T.
apply logical_relation_lemma_proj2.
- move=> l hl hcl htl.
have[res hres]: tractable (s.|[T/] ∘ 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.
apply logical_relation_lemma_proj1 with U=>//.
apply ih=>//.
by rewrite weight_hsubst; lia.
inv hb.
by apply box_rel_preserved_hsubst0 with empty_ctx U 1 1. }
apply eval_eval0_1, eval_eval0 in hres.
exists res.
apply eval_eval0_1. simpl.
by constructor.
- apply ty_tapp; by [apply fv_plage_eq|apply ty_tlam]. }
(* case {TAll s} *)
{ move=> s W /= hw hc hty hb.
have hW: W = Void by inv hty.
rewrite hW in hty *.
have hts: [ ⊢ s :- Void ].
by apply has_type_lower_1; inv hty.
have hs: TRAC Void s.
{ apply ih=>//; by [apply closed_tall|inv hb]. }
rewrite /TRAC/= in hs.
move: hs=> [f hf].
apply logical_relation_lemma_proj2=>[l hl hcl htl|//].
(* a Void stack is empty *)
inv hl=>/=.
exists (FAll f).
by constructor. }
(* case {Neu s} *)
{ move=> s W /= hw /closed_neu hc hty hb.
have hts: [ ⊢ s :- W ] by inv hty.
have hbs: box_rel tractable s by inv hb.
have hs: TRAC W (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 hl hcl htl|//].
have[sl h1]: tractable (neu s ∘ l).
{ apply logical_relation_lemma_proj1 with W=>//.
by apply has_type_neu. }
exists sl.
apply eval_eval0_2=>/=.
rewrite /to_stack/= to_stack_appl /=.
constructor.
by apply eval_move_stack. }
(* case {Box s} *)
{ move=> s U hw hc hty hb.
have[V [hcs [hts hls]]] := box_rel_box_ids hb.
have e: V = U.
{ inv hty. by apply has_type_det with empty_ctx 0 0 s. }
rewrite e in hts hls.
apply logical_relation_lemma_proj2=>[l hl hcl htl|//].
have[sl h1]: tractable (s ∘ l).
{ apply logical_relation_lemma_proj1 with U=>//. by case: hls. }
exists sl.
apply eval_eval0_1=>/=.
constructor.
apply eval_eval0.
by apply eval_eval0_1 in h1. }
}
Qed.
Theorem eval_def :
forall r, complete r -> tractable r.
Proof.
move=> r [hc ht].
apply (@inner1 r Void)=>//.
by apply (inner2g inner1) with Void.
Qed.
Lemma uniqueness_eval_u s f g l U :
eval s l f ->
eval s l g ->
closed s ->
[ ⊢ s :- U ] ->
aligned l U ->
f = g.
Proof.
move=> h. move: h g U.
elim.
- by move=> > h; inv h.
- by move=> > h; inv h.
- move=> s1 s2 f0 _ ih g U hg hc ht ha.
inv hg.
inv ht.
f_equal.
apply ih with Void=>//.
by apply closed_imp in hc.
- move=> s1 s2 t1 t2 l0 _ ih1 _ ih2 g U hg /closed_and [hc1 hc2] ht ha.
inv hg.
inv ht.
f_equal; by [apply ih1 with U|apply ih2 with U].
- move=> s1 s2 l0 _ ih g U hg hc ht ha.
inv hg.
inv ht.
by apply ih with U.
- move=> s0 s2 l0 _ ih g U hg /closed_neu hc ht ha.
inv hg.
inv ht.
apply ih with U=>//; by [apply closed_sneu|apply has_type_neu].
- move=> s1 s2 T l0 _ ih g U hg hc ht ha.
inv hg.
inv ht.
move: ha=> [hcl hsl].
inv hcl.
inv hsl.
apply ih with U0=>//.
+ by apply closed_unaffectedh, closed_tlam.
+ by apply has_type_hsubst1.
- move=> s1 s2 _ ih g U hg hc ht ha.
inv hg.
inv ht.
f_equal.
apply ih with Void=>//.
+ by apply closed_tall.
+ apply has_type_swap_a with 1=>//.
by apply has_type_lower_b with 1.
- move=> s1 s2 W r l0 _ ih g U hg hc ht ha.
inv hg.
inv ht.
move: ha=> [hcl hsl].
inv hcl.
inv hsl.
apply ih with V=>//.
+ apply fv1; by [apply closed_lam in hc|apply closed_box].
+ apply has_type_beta with W=>//; by [apply closed_box|constructor].
- move=> s0 t s2 l0 _ ih g U hg /closed_app [hc1 hc2] ht ha.
inv hg.
inv ht.
move: ha=> [hcl hsl].
apply ih with (Arr U0 U)=>//.
by split; constructor.
- move=> s0 T s2 l0 _ ih g U hg /closed_tapp hc ht ha.
inv hg.
inv ht.
move: ha=> [hcl hsl].
apply ih with (TArr U)=>//.
by split; constructor=>//; apply fv_plage_eq.
Qed.
Theorem uniqueness_eval s :
complete s ->
uniqueness (eval s [::]).
Proof.
move=> [hc ht] f g h1 h2.
apply uniqueness_eval_u with s [::] Void=>//.
by split; constructor.
Qed.
Definition TRAC U := logrel tractable U.
Lemma inner1 :
forall r U,
closed r -> [ ⊢ r :- U ] ->
box_rel tractable r -> TRAC U r.
Proof.
(* We prove this lemma by induction over the weight r. *)
have:
forall n r U,
weight r <= n ->
closed r ->
[ ⊢ r :- U ] ->
box_rel tractable r -> TRAC U r.
(* The latter generalization subsumes the lemma. *)
2: { move=> h r U hc ht h2. by apply (h (weight r) r U). }
(* Now we prove it by induction over a bound of
the weight of the recipe r. *)
elim=>[r U hw|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=> ??? h3 ?. inv h3=>/=. exists FBot. by constructor. }
(* case {Top} *)
{ move=> ??? h3 ?. inv h3=>/=. exists FTop. by constructor. }
(* case {And s t} *)
{ move=> s t U /= hw /closed_and [hc1 hc2] hty hb.
apply logical_relation_lemma_proj2=>[l hl hcl htl|//].
have ts: TRAC U s.
{ apply ih=>//; first by lia. by inv hty. by inv hb. }
have tt: TRAC U t.
{ apply ih=>//; first by lia. by inv hty. by inv hb. }
have[sl h1]: tractable (s ∘ l).
{ apply logical_relation_lemma_proj1 with U=>//. by inv hty. }
have[tl h2]: tractable (t ∘ l).
{ apply logical_relation_lemma_proj1 with U=>//. by inv hty. }
econstructor.
apply eval_eval0_2=>/=.
rewrite /to_stack/= to_stack_appl /=.
constructor.
+ rewrite eval_eval0_1 in h1.
apply eval_eval0.
exact: h1.
+ rewrite eval_eval0_1 in h2.
apply eval_eval0.
exact: h2. }
(* case {App s t} *)
{ move=> s t W /= hw /closed_app [hc1 hc2] hty hb.
inv hty.
have hs: TRAC (Arr U W) s.
{ apply ih=>//; first by lia. by inv hb. }
apply hs=>//.
move=> ξ.
have hct: closed t.|[ren ξ] by apply closed_unaffectedh.
have htt: [ ⊢ t.|[ren ξ] :- U ] by apply has_type_hsubst_0.
have hbt: box_rel tractable 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 T} *)
{ move=> s S W /= hw /closed_tapp hc hty hb.
inv hty.
have: TRAC (TArr W) s.
{ apply ih=>//. by inv hb. }
by apply. }
(* case {Lam s U} *)
{ move=> s U W /= hw hc hty hb.
inv hty.
rewrite /TRAC/= => t hct htt hst.
apply logical_relation_lemma_proj2.
- move=> l hl hcl htl.
have[res hres]: tractable (s.[Box t/] ∘ l).
{ have hc2: closed s.[Box t/].
{ apply fv1.
by apply closed_lam in hc.
by apply closed_box. }
have hty1: [ ⊢ Box t :- U ] by constructor.
have hty2: [ ⊢ s.[Box t/] :- V ].
{ apply has_type_beta with U=>//. by apply closed_box. }
apply logical_relation_lemma_proj1 with V=>//.
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. }
exists res.
apply eval_eval0_1=>/=.
constructor.
apply eval_eval0_1 in hres.
by apply eval_eval0.
- apply ty_app with U=>//.
by constructor. }
(* case {Imp s f} *)
{ move=> s f ? /= hw /closed_imp hc hty hb.
inv hty.
have: TRAC Void s.
{ apply ih=>//. by inv hb. }
rewrite/TRAC/=.
move=> [y ?].
exists (FImp f y).
by constructor. }
(* case {TLam s} *)
{ move=> s W /= hw hc hty hb.
inv hty.
rewrite /TRAC/= => T.
apply logical_relation_lemma_proj2.
- move=> l hl hcl htl.
have[res hres]: tractable (s.|[T/] ∘ 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.
apply logical_relation_lemma_proj1 with U=>//.
apply ih=>//.
by rewrite weight_hsubst; lia.
inv hb.
by apply box_rel_preserved_hsubst0 with empty_ctx U 1 1. }
apply eval_eval0_1, eval_eval0 in hres.
exists res.
apply eval_eval0_1. simpl.
by constructor.
- apply ty_tapp; by [apply fv_plage_eq|apply ty_tlam]. }
(* case {TAll s} *)
{ move=> s W /= hw hc hty hb.
have hW: W = Void by inv hty.
rewrite hW in hty *.
have hts: [ ⊢ s :- Void ].
by apply has_type_lower_1; inv hty.
have hs: TRAC Void s.
{ apply ih=>//; by [apply closed_tall|inv hb]. }
rewrite /TRAC/= in hs.
move: hs=> [f hf].
apply logical_relation_lemma_proj2=>[l hl hcl htl|//].
(* a Void stack is empty *)
inv hl=>/=.
exists (FAll f).
by constructor. }
(* case {Neu s} *)
{ move=> s W /= hw /closed_neu hc hty hb.
have hts: [ ⊢ s :- W ] by inv hty.
have hbs: box_rel tractable s by inv hb.
have hs: TRAC W (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 hl hcl htl|//].
have[sl h1]: tractable (neu s ∘ l).
{ apply logical_relation_lemma_proj1 with W=>//.
by apply has_type_neu. }
exists sl.
apply eval_eval0_2=>/=.
rewrite /to_stack/= to_stack_appl /=.
constructor.
by apply eval_move_stack. }
(* case {Box s} *)
{ move=> s U hw hc hty hb.
have[V [hcs [hts hls]]] := box_rel_box_ids hb.
have e: V = U.
{ inv hty. by apply has_type_det with empty_ctx 0 0 s. }
rewrite e in hts hls.
apply logical_relation_lemma_proj2=>[l hl hcl htl|//].
have[sl h1]: tractable (s ∘ l).
{ apply logical_relation_lemma_proj1 with U=>//. by case: hls. }
exists sl.
apply eval_eval0_1=>/=.
constructor.
apply eval_eval0.
by apply eval_eval0_1 in h1. }
}
Qed.
Theorem eval_def :
forall r, complete r -> tractable r.
Proof.
move=> r [hc ht].
apply (@inner1 r Void)=>//.
by apply (inner2g inner1) with Void.
Qed.
Lemma uniqueness_eval_u s f g l U :
eval s l f ->
eval s l g ->
closed s ->
[ ⊢ s :- U ] ->
aligned l U ->
f = g.
Proof.
move=> h. move: h g U.
elim.
- by move=> > h; inv h.
- by move=> > h; inv h.
- move=> s1 s2 f0 _ ih g U hg hc ht ha.
inv hg.
inv ht.
f_equal.
apply ih with Void=>//.
by apply closed_imp in hc.
- move=> s1 s2 t1 t2 l0 _ ih1 _ ih2 g U hg /closed_and [hc1 hc2] ht ha.
inv hg.
inv ht.
f_equal; by [apply ih1 with U|apply ih2 with U].
- move=> s1 s2 l0 _ ih g U hg hc ht ha.
inv hg.
inv ht.
by apply ih with U.
- move=> s0 s2 l0 _ ih g U hg /closed_neu hc ht ha.
inv hg.
inv ht.
apply ih with U=>//; by [apply closed_sneu|apply has_type_neu].
- move=> s1 s2 T l0 _ ih g U hg hc ht ha.
inv hg.
inv ht.
move: ha=> [hcl hsl].
inv hcl.
inv hsl.
apply ih with U0=>//.
+ by apply closed_unaffectedh, closed_tlam.
+ by apply has_type_hsubst1.
- move=> s1 s2 _ ih g U hg hc ht ha.
inv hg.
inv ht.
f_equal.
apply ih with Void=>//.
+ by apply closed_tall.
+ apply has_type_swap_a with 1=>//.
by apply has_type_lower_b with 1.
- move=> s1 s2 W r l0 _ ih g U hg hc ht ha.
inv hg.
inv ht.
move: ha=> [hcl hsl].
inv hcl.
inv hsl.
apply ih with V=>//.
+ apply fv1; by [apply closed_lam in hc|apply closed_box].
+ apply has_type_beta with W=>//; by [apply closed_box|constructor].
- move=> s0 t s2 l0 _ ih g U hg /closed_app [hc1 hc2] ht ha.
inv hg.
inv ht.
move: ha=> [hcl hsl].
apply ih with (Arr U0 U)=>//.
by split; constructor.
- move=> s0 T s2 l0 _ ih g U hg /closed_tapp hc ht ha.
inv hg.
inv ht.
move: ha=> [hcl hsl].
apply ih with (TArr U)=>//.
by split; constructor=>//; apply fv_plage_eq.
Qed.
Theorem uniqueness_eval s :
complete s ->
uniqueness (eval s [::]).
Proof.
move=> [hc ht] f g h1 h2.
apply uniqueness_eval_u with s [::] Void=>//.
by split; constructor.
Qed.
TOPLAS: Theorem 3.2, in full.
Theorem exists_unique_eval s :
complete s ->
exists! f, eval s [::] f.
Proof.
move=> h.
have /eval_def [f h1] := h.
have /uniqueness_eval h2 := h.
exists f.
split=>//.
move=> g hg.
by apply h2.
Qed.
Lemma eval_hsubst s l f :
eval s l f ->
forall θ,
eval s.|[θ] (stack_hsubst θ l) f.[θ].
Proof.
elim=> /=.
- by move=> θ; constructor.
- by move=> θ; constructor.
- move=> ??? _ ih θ.
by constructor.
- move=> ????? _ ? _ ? θ.
by constructor.
- move=> ??? _ ih θ.
by constructor.
- move=> ??? _ ih θ.
constructor.
by rewrite neu_hsubst_comm.
- move=> ???? _ ih θ.
constructor.
move: (ih θ).
asimpl.
by [].
- move=> ?? _ ih θ.
by constructor.
- move=> ????? _ ih θ.
constructor.
move: (ih θ).
asimpl.
by [].
- move=> ???? _ ? θ.
by constructor.
- move=> ???? _ ? θ.
by constructor.
Qed.
Lemma eval_fall_inv n X G :
eval (fall n X) [::] G ->
exists G0, G = fallF n G0 /\ eval X [::] G0.
Proof.
elim: n G=> [|n ih] G /= h; first by exists G.
inv h.
match goal with hh: eval (fall n X) [::] _ |- _ =>
have [G0 [e h0]] := ih _ hh end.
exists G0.
by rewrite e.
Qed.
End Eval.
complete s ->
exists! f, eval s [::] f.
Proof.
move=> h.
have /eval_def [f h1] := h.
have /uniqueness_eval h2 := h.
exists f.
split=>//.
move=> g hg.
by apply h2.
Qed.
Lemma eval_hsubst s l f :
eval s l f ->
forall θ,
eval s.|[θ] (stack_hsubst θ l) f.[θ].
Proof.
elim=> /=.
- by move=> θ; constructor.
- by move=> θ; constructor.
- move=> ??? _ ih θ.
by constructor.
- move=> ????? _ ? _ ? θ.
by constructor.
- move=> ??? _ ih θ.
by constructor.
- move=> ??? _ ih θ.
constructor.
by rewrite neu_hsubst_comm.
- move=> ???? _ ih θ.
constructor.
move: (ih θ).
asimpl.
by [].
- move=> ?? _ ih θ.
by constructor.
- move=> ????? _ ih θ.
constructor.
move: (ih θ).
asimpl.
by [].
- move=> ???? _ ? θ.
by constructor.
- move=> ???? _ ? θ.
by constructor.
Qed.
Lemma eval_fall_inv n X G :
eval (fall n X) [::] G ->
exists G0, G = fallF n G0 /\ eval X [::] G0.
Proof.
elim: n G=> [|n ih] G /= h; first by exists G.
inv h.
match goal with hh: eval (fall n X) [::] _ |- _ =>
have [G0 [e h0]] := ih _ hh end.
exists G0.
by rewrite e.
Qed.
End Eval.