Rocoma.Recipes_fv_lemmas
Ltac prove_fv :=
unfold fv; intros; asimpl;
split; intros; unpack; [ injections | f_equal ]; eauto.
Ltac prove_fvh :=
unfold fvh; intros; asimpl;
split; intros; unpack; [ injections | f_equal ]; eauto.
Lemma subSn1 (n: nat) :
n.+1 - 1 = n.
Proof.
by lia.
Qed.
Lemma closed_top : closed Top.
Proof.
by [].
Qed.
Lemma closedh_top : closedh Top.
Proof.
by [].
Qed.
Lemma fv_var x n :
x < n -> fv n (Var x).
Proof.
by apply fv_ids_eq.
Qed.
Lemma fv_tvar x n :
x < n -> fv n (TVar x).
Proof.
by apply fv_ids_eq.
Qed.
Lemma fv_app s t n :
fv n (App s t) <-> fv n s /\ fv n t.
Proof.
by prove_fv.
Qed.
Lemma fvh_app s t n :
fvh n (App s t) <-> fvh n s /\ fvh n t.
Proof.
by prove_fvh.
Qed.
Lemma closed_app s t :
closed (App s t) <-> closed s /\ closed t.
Proof.
exact: fv_app.
Qed.
Lemma closedh_app s t :
closedh (App s t) <-> closedh s /\ closedh t.
Proof.
exact: fvh_app.
Qed.
Corollary closed_app1 s t :
closed (App s t) -> closed s /\ closed t.
Proof.
exact: proj1 (closed_app _ _).
Qed.
Lemma fv_and s t n :
fv n (And s t) <-> fv n s /\ fv n t.
Proof.
by prove_fv.
Qed.
Lemma fvh_and s t n :
fvh n (And s t) <-> fvh n s /\ fvh n t.
Proof.
by prove_fvh.
Qed.
Lemma closed_and s t :
closed (And s t) <-> closed s /\ closed t.
Proof.
exact: fv_and.
Qed.
Lemma closedh_and s t :
closedh (And s t) <-> closedh s /\ closedh t.
Proof.
exact: fvh_and.
Qed.
Corollary closed_and1 s t :
closed (And s t) -> closed s /\ closed t.
Proof.
exact: proj1 (closed_and _ _).
Qed.
Lemma fv_lam s U n :
fv n (Lam s U) <-> fv n.+1 s.
Proof.
by prove_fv.
Qed.
Lemma fvh_lam s U n :
fvh n (Lam s U) <-> fvh n s.
Proof.
by prove_fvh.
Qed.
Lemma closed_lam s U n :
fv n (Lam s U) <-> fv n.+1 s.
Proof.
exact: fv_lam.
Qed.
Lemma closedh_lam s U n :
fvh n (Lam s U) <-> fvh n s.
Proof.
exact: fvh_lam.
Qed.
Corollary closed_lam1 s U n :
fv n (Lam s U) -> fv n.+1 s.
Proof.
exact: proj1 (fv_lam _ _ _).
Qed.
Lemma fv_neu s n :
fv n (Neu s) <-> fv n s.
Proof.
by prove_fv.
Qed.
Lemma fvh_neu s n :
fvh n (Neu s) <-> fvh n s.
Proof.
by prove_fvh.
Qed.
Lemma closed_neu s :
closed (Neu s) <-> closed s.
Proof.
exact: fv_neu.
Qed.
Lemma closedh_neu s :
closedh (Neu s) <-> closedh s.
Proof.
exact: fvh_neu.
Qed.
Corollary closed_neu1 s :
closed (Neu s) -> closed s.
Proof.
exact: proj1 (fv_neu _ _).
Qed.
Corollary closedh_neu1 s :
closedh (Neu s) -> closedh s.
Proof.
exact: proj1 (fvh_neu _ _).
Qed.
Lemma fv_box s n :
fv n (Box s) <-> fv n s.
Proof.
by prove_fv.
Qed.
Lemma fvh_box s n :
fvh n (Box s) <-> fvh n s.
Proof.
by prove_fvh.
Qed.
Corollary fv_box1 s n :
fv n (Box s) -> fv n s.
Proof.
exact: proj1 (fv_box _ _).
Qed.
Lemma closed_box s :
closed (Box s) <-> closed s.
Proof.
exact: fv_box.
Qed.
Lemma closedh_box s :
closedh (Box s) <-> closedh s.
Proof.
exact: fvh_box.
Qed.
Corollary closedh_box1 s :
closedh (Box s) -> closedh s.
Proof.
exact: proj1 (fvh_box _ _).
Qed.
Corollary closed_box1 s :
closed (Box s) -> closed s.
Proof.
exact: proj1 (fv_box _ _).
Qed.
Lemma fv_tapp s T n :
fv n (TApp s T) <-> fv n s.
Proof.
by prove_fv.
Qed.
Lemma fvh_tapp s T n :
fvh n (TApp s T) <-> fvh n s /\ fv n T.
Proof.
unfold fvh; intros; asimpl.
split; intros; unpack; injections.
+ by split.
+ by f_equal.
Qed.
Lemma closed_tapp s T :
closed (TApp s T) <-> closed s.
Proof.
exact: fv_tapp.
Qed.
Lemma closedh_tapp s T :
closedh (TApp s T) <-> closedh s /\ closed T.
Proof.
exact: fvh_tapp.
Qed.
Corollary closed_tapp1 s T :
closed (TApp s T) -> closed s.
Proof.
exact: proj1 (closed_tapp _ _).
Qed.
Lemma fv_imp s f n :
fv n (Imp s f) <-> fv n s.
Proof.
by prove_fv.
Qed.
Lemma fvh_imp s f n :
fvh n (Imp s f) <-> fvh n s /\ fv n f.
Proof.
unfold fvh; intros; asimpl.
split; intros; unpack; injections.
+ by split.
+ by f_equal.
Qed.
Lemma closedh_imp s f :
closedh (Imp s f) <-> closedh s /\ closed f.
Proof.
exact: fvh_imp.
Qed.
Lemma closed_imp s f :
closed (Imp s f) <-> closed s.
Proof.
by apply fv_imp.
Qed.
Corollary closed_imp1 s f :
closed (Imp s f) -> closed s.
Proof.
exact: proj1 (closed_imp _ _).
Qed.
Lemma fv_tlam s n :
fv n (TLam s) <-> fv n s.
Proof.
prove_fv;
move: H;
by have->: s.[fun x => (upn n (ren (+1)) x).|[ren (+1)]] = s.[upn n (ren (+1))]
by (f_equal; f_ext=> x; rewrite upnP; case (boolP (x < n))).
Qed.
Lemma fvh_tlam s n :
fvh n (TLam s) <-> fvh n.+1 s.
Proof.
by prove_fvh.
Qed.
Lemma closedh_tlam1 s :
closedh (TLam s) -> fvh 1 s.
Proof.
rewrite /closedh/fvh/= => h.
injection h=> {2}<-.
autosubst.
Qed.
Lemma closed_tlam s :
closed (TLam s) <-> closed s.
Proof.
exact: fv_tlam.
Qed.
Corollary closed_tlam1 s :
closed (TLam s) -> closed s.
Proof.
exact: proj1 (closed_tlam _).
Qed.
Lemma fv_tall s n :
fv n (TAll s) <-> fv n s.
Proof.
prove_fv;
move: H;
by have->: s.[fun x => (upn n (ren (+1)) x).|[ren (+1)]] = s.[upn n (ren (+1))]
by (f_equal; f_ext=> x; rewrite upnP; case (boolP (x < n))).
Qed.
Lemma fvh_tall s n :
fvh n (TAll s) <-> fvh n.+1 s.
Proof.
by prove_fvh.
Qed.
Lemma fv_fall m s n :
fv n (fall m s) <-> fv n s.
Proof.
elim: m=>//= *.
by rewrite fv_tall.
Qed.
Lemma fvh_fall m s n :
fvh n (fall m s) <-> fvh (n + m) s.
Proof.
elim: m n=> [|? ih] ? /=.
- by rewrite addn0.
- by rewrite fvh_tall ih addSnnS.
Qed.
Lemma closedh_tall1 s :
closedh (TAll s) -> fvh 1 s.
Proof.
rewrite /closedh/fvh/= => h.
injection h=> {2}<-.
autosubst.
Qed.
Lemma closed_tall s :
closed (TAll s) <-> closed s.
Proof.
exact: fv_tall.
Qed.
Corollary closed_tall1 s :
closed (TAll s) -> closed s.
Proof.
exact: proj1 (closed_tall _).
Qed.
Hint Rewrite fv_and fv_app fv_lam fv_imp fv_neu
fv_box fv_tlam fv_tall fv_tapp : fv.
Hint Rewrite fvh_and fvh_app fvh_lam fvh_imp fvh_neu
fvh_box fvh_tlam fvh_tall fvh_tapp : fvh.
Lemma fv_sneu r n :
fv n r <-> fv n (neu r).
Proof.
by split; elim: r n=>/= *; fv; unpack; eauto.
Qed.
Lemma fvh_sneu r n :
fvh n r <-> fvh n (neu r).
Proof.
by split; elim: r n=>/= *; fvh; unpack; eauto.
Qed.
Corollary closed_sneu r :
closed r -> closed (neu r).
Proof.
exact: (proj1 (fv_sneu _ 0)).
Qed.
Corollary closedh_sneu r :
closedh r -> closedh (neu r).
Proof.
exact: (proj1 (fvh_sneu _ 0)).
Qed.
Corollary closed_sneu2 r :
closed (neu r) -> closed r.
Proof.
exact: (proj2 (fv_sneu _ 0)).
Qed.
Corollary closedh_sneu2 r :
closedh (neu r) -> closedh r.
Proof.
exact: (proj2 (fvh_sneu _ 0)).
Qed.
Ltac tac_closed :=
match goal with
| h: closed (And _ _) |- _ => apply closed_and in h as []
| h: closed (App _ _) |- _ => apply closed_app in h as []
| h: closed (Box _) |- _ => apply closed_box1 in h
| h: closed (Imp _ _) |- _ => apply closed_imp in h
| h: closed (Neu _) |- _ => apply closed_neu1 in h
| h: closed (TLam _) |- _ => apply closed_tlam1 in h
| h: closed (Lam _ _) |- _ => apply closed_lam1 in h
| h: closed (TApp _ _) |- _ => apply closed_tapp in h
| h: closed (neu _) |- _ => apply closed_sneu2 in h
end.
Ltac tac_closedh :=
match goal with
| h: closedh (And _ _) |- _ => apply closedh_and in h as []
| h: closedh (App _ _) |- _ => apply closedh_app in h as []
| h: closedh (Box _) |- _ => apply closedh_box1 in h
| h: closedh (Imp _ _) |- _ => apply closedh_imp in h as []
| h: closedh (Neu _) |- _ => apply closedh_neu1 in h
| h: closedh (Lam _ _) |- _ => apply closedh_lam in h
| h: closedh (TLam _) |- _ => apply closedh_tlam1 in h
| h: closedh (TApp _ _) |- _ => apply closedh_tapp in h as []
| h: closedh (neu _) |- _ => apply closedh_sneu2 in h
end.
Ltac tac_cch := tac_closed; tac_closedh.
Ltac split_fv :=
repeat match goal with
| h: fv _ (And _ _) |- _ =>
move: h=>[hl hr]
| h: fv _ (App _ _) |- _ =>
move: h=>[hl hr]
end.
Lemma fv_unaffected:
forall t k σ θ,
fv k t ->
t.[upn k σ >>| θ] = t.
Proof.
elim; intros; fv; unpack; asimpl;
try solve [ eauto using upn_k_sigma_x with typeclass_instances
| f_equal; eauto ].
{ by rewrite upn2P ifT. }
{ f_equal.
rewrite -{2}(H k.+1 σ θ H0) {1}upn1.
f_equal; f_ext=> -[] //= x.
rewrite !upnP /=.
rewrite upnP.
have->: (x.+1 - 1 < k) = (x.+1 < k.+1) by lia.
case (x.+1 < k.+1)=>//=.
- have->: ids = Var by autosubst.
by f_equal; lia.
- asimpl.
do 3 f_equal.
by lia. }
Qed.
Corollary closed_unaffected:
forall t σ θ,
closed t ->
t.[σ >>| θ] = t.
Proof.
have := @fv_unaffected _ 0.
by apply.
Qed.
Corollary closed_subst:
forall t σ,
closed t ->
t.[σ] = t.
Proof.
move=> t σ hc.
have h:= @closed_unaffected t σ ids hc.
rewrite -{2}h.
autosubst.
Qed.
Lemma fv_unaffected_term:
forall (t: term) k σ,
fv k t ->
t.[upn k σ] = t.
Proof.
elim; intros ; fv; unpack; asimpl; try (by f_equal; eauto).
- by rewrite upnP ifT; [|lia].
- rewrite /fv/= in H1. injections. by f_equal; eauto.
- rewrite /fv/= in H1. injections. by f_equal; eauto.
- rewrite /fv/= in H1. injections. by f_equal; eauto.
- rewrite /fv/= in H0. injections. by f_equal; eauto.
- rewrite /fv/= in H0. injections. by f_equal; eauto.
- rewrite /fv/= in H1. injections. by f_equal; eauto.
Qed.
Corollary closed_unaffected_term:
forall (t: term) σ,
fv 0 t ->
t.[σ] = t.
Proof.
have := @fv_unaffected_term _ 0.
by apply.
Qed.
Lemma fvh_hsubst s n θ :
fvh n s -> s.|[upn n θ] = s.
Proof with asimpl; f_equal; eauto using fv_unaffected_term.
elim: s n θ; try by
(rewrite /fvh/= =>*;
injections; f_equal;
eauto using closed_unaffected_term).
- move=> s ih > /fvh_tapp [??]...
- move=> s ih > /fvh_imp [??]...
- move=> s ih > /fvh_tlam ?...
- move=> s ih > /fvh_tall ?...
Qed.
Lemma closedh_hsubst s θ :
closedh s -> s.|[θ] = s.
Proof.
have := @fvh_hsubst _ 0.
by apply.
Qed.
Lemma fv_unaffectedh:
forall t n θ,
fv n t ->
fv n t.|[θ].
Proof.
elim=>//=.
- move=> s h1 t h2 n θ /fv_and [??].
by rewrite /fv/=; f_equal; [apply h1|apply h2].
- move=> s h1 t h2 n θ /fv_app [??].
by rewrite /fv/=; f_equal; [apply h1|apply h2].
- move=> s h1 S n θ /fv_tapp [?].
by rewrite /fv/=; f_equal; apply h1.
- move=> s h1 S n θ /fv_lam [?].
by rewrite /fv/=; f_equal; asimpl; apply h1.
- move=> s h1 S n θ /fv_imp [?].
by rewrite /fv/=; f_equal; apply h1.
- move=> s h1 n θ /fv_tlam [h].
rewrite /fv/=; f_equal.
rewrite /fv/= in h.
specialize (h1 _ (up θ) h).
rewrite /fv/= in h1.
rewrite -{2}h1.
f_equal; f_ext=> x.
asimpl.
rewrite upnP.
by case (boolP (x < n)).
- move=> s h1 n θ /fv_tall [h].
rewrite /fv/=; f_equal.
rewrite /fv/= in h.
specialize (h1 _ (up θ) h).
rewrite /fv/= in h1.
rewrite -{2}h1.
f_equal; f_ext=> x.
asimpl.
rewrite upnP.
by case (boolP (x < n)).
- move=> s h1 n θ /fv_neu [?].
by rewrite /fv/=; f_equal; apply h1.
- move=> s h1 n θ /fv_box [?].
by rewrite /fv/=; f_equal; apply h1.
Qed.
Lemma fv_unaffectedh2:
forall t n θ,
fv n t.|[θ] ->
fv n t.
Proof.
elim=>//=.
- move=> s h1 t h2 n θ /fv_and [??].
by rewrite /fv/=; f_equal; [apply h1 with θ|apply h2 with θ].
- move=> s h1 t h2 n θ /fv_app [??].
by rewrite /fv/=; f_equal; [apply h1 with θ|apply h2 with θ].
- move=> s h1 S n θ /fv_tapp [?].
by rewrite /fv/=; f_equal; apply h1 with θ.
- move=> s h1 S n θ /fv_lam [?].
by rewrite /fv/=; f_equal; asimpl; apply h1 with θ.
- move=> s h1 S n θ /fv_imp [?].
by rewrite /fv/=; f_equal; apply h1 with θ.
- move=> s h1 n θ /fv_tlam [h].
rewrite /fv/=; f_equal.
rewrite /fv/= in h.
specialize (h1 _ (up θ) h).
rewrite /fv/= in h1.
rewrite -{2}h1.
f_equal; f_ext=> x.
asimpl.
rewrite upnP.
by case (boolP (x < n)).
- move=> s h1 n θ /fv_tall [h].
rewrite /fv/=; f_equal.
rewrite /fv/= in h.
specialize (h1 _ (up θ) h).
rewrite /fv/= in h1.
rewrite -{2}h1.
f_equal; f_ext=> x.
asimpl.
rewrite upnP.
by case (boolP (x < n)).
- move=> s h1 n θ /fv_neu [?].
by rewrite /fv/=; f_equal; apply h1 with θ.
- move=> s h1 n θ /fv_box [?].
by rewrite /fv/=; f_equal; apply h1 with θ.
Qed.
Corollary closed_unaffectedh:
forall t θ,
closed t <->
closed t.|[θ].
Proof.
split.
- have := @fv_unaffectedh _ 0.
by apply.
- have := @fv_unaffectedh2 _ 0.
by apply.
Qed.
Lemma closed_fv n s :
closed s -> fv n s.
Proof.
rewrite /fv. by apply closed_subst.
Qed.
Lemma closedh_fvh n s :
closedh s -> fvh n s.
Proof.
rewrite /fvh. by apply closedh_hsubst.
Qed.
Lemma fvu_tlam n k s :
fvu n k (TLam s) ->
fvu n k s.
Proof.
prove_fvu. move: H.
have->:
(fun i => if i < n then Var i.+1 else if i < k then Var i else Var i.+1)
>>| ren (+1) =
(fun i => if i < n then Var i.+1 else if i < k then Var i else Var i.+1).
by f_ext=> x/=; case (boolP (x < n)); case (boolP (x < k)).
done.
Qed.
Lemma fvu_tall n k s :
fvu n k (TAll s) ->
fvu n k s.
Proof.
prove_fvu. move: H.
have->:
(fun i => if i < n then Var i.+1 else if i < k then Var i else Var i.+1)
>>| ren (+1) =
(fun i => if i < n then Var i.+1 else if i < k then Var i else Var i.+1).
by f_ext=> x/=; case (boolP (x < n)); case (boolP (x < k)).
done.
Qed.
Lemma fvu2_var sub lo hi x :
fvu2 sub lo hi (ids x) ->
x < sub \/ (lo <= x /\ x < hi).
Proof.
rewrite /fvu2/=.
case (x < sub). by left.
case (boolP (x < lo))=> h1. by intros; injections; lia.
case (boolP (x < hi))=> h2. by right; split; lia.
by intros; injections; lia.
Qed.
Lemma fvu2_tlam sub lo hi s :
fvu2 sub lo hi (TLam s) ->
fvu2 sub lo hi s.
Proof.
prove_fvu2.
have e:
s.[(fun i => if i < sub then Var i
else if i < lo then Var i.+1 else if i < hi then Var i else Var i.+1)
>>| ren (+1)] =
s.[(fun i => if i < sub then Var i
else if i < lo then Var i.+1 else if i < hi then Var i else Var i.+1)].
{ f_equal; f_ext=> x/=.
by case (boolP (x < sub));
case (boolP (x < lo));
case (boolP (x < hi)). }
rewrite e in H.
by rewrite H.
Qed.
Lemma fvu2_tall sub lo hi s :
fvu2 sub lo hi (TAll s) ->
fvu2 sub lo hi s.
Proof.
prove_fvu2.
have e:
s.[(fun i => if i < sub then Var i
else if i < lo then Var i.+1 else if i < hi then Var i else Var i.+1)
>>| ren (+1)] =
s.[(fun i => if i < sub then Var i
else if i < lo then Var i.+1 else if i < hi then Var i else Var i.+1)].
{ f_equal; f_ext=> x/=.
by case (boolP (x < sub));
case (boolP (x < lo));
case (boolP (x < hi)). }
rewrite e in H.
by rewrite H.
Qed.
Lemma fvu2_tlam_op sub lo hi s :
fvu2 sub lo hi s ->
fvu2 sub lo hi (TLam s).
Proof.
rewrite/fvu2/=.
have->: (fun i =>
if i < sub then Var i
else if i < lo then Var i.+1
else if i < hi then Var i else Var i.+1) >>| ren (+1)
= (fun i =>
if i < sub then Var i
else if i < lo then Var i.+1
else if i < hi then Var i else Var i.+1).
{ f_ext=> x/=.
by case (boolP (x < sub));
case (boolP (x < lo));
case (boolP (x < hi)). }
move=>h.
by f_equal.
Qed.
Lemma fvu2_tall_op sub lo hi s :
fvu2 sub lo hi s ->
fvu2 sub lo hi (TAll s).
Proof.
rewrite/fvu2/=.
have->: (fun i =>
if i < sub then Var i
else if i < lo then Var i.+1
else if i < hi then Var i else Var i.+1) >>| ren (+1)
= (fun i =>
if i < sub then Var i
else if i < lo then Var i.+1
else if i < hi then Var i else Var i.+1).
{ f_ext=> x/=.
by case (boolP (x < sub));
case (boolP (x < lo));
case (boolP (x < hi)). }
move=>h.
by f_equal.
Qed.
Lemma fvu2_lam sub lo hi s U :
fvu2 sub lo hi (Lam s U) ->
fvu2 sub.+1 lo.+1 hi.+1 s.
Proof.
prove_fvu2.
rewrite -{2}H=>{H}.
f_equal. f_ext=>n.
Print ssrnat.
rewrite !subSS upn1 !upnP.
case (boolP (n < sub))=> h1.
- rewrite ifT; last by lia.
case (boolP (n < 1))=> h2//.
have{}h2: 0 < n by lia.
rewrite ifT; last by lia. simpl. f_equal.
by have->: (n - 1).+1 = n by lia.
- have{}h1: n >= sub by lia.
case (boolP (n <= sub))=> h2.
+ have{h1 h2}h: sub = n by lia. subst=>//=.
rewrite ifT; last by lia.
case (boolP (n < 1))=> e1//.
rewrite ifT; last by lia.
asimpl. by have->: (n - 1).+1 = n by lia.
+ have{h1 h2} h: sub < n by lia.
have h1: n > 0 by lia.
rewrite ifF; last by lia.
have->:
(if n < 1 then Var n else
(if n - 1 < sub
then Var (n - 1)
else if n - 1 < lo then Var (n - 1).+1
else if n - 1 < hi then Var (n - 1) else Var (n - 1).+1).[ren (+1)])
= (if n - 1 < lo then Var (n - 1).+1
else if n - 1 < hi then Var (n - 1) else Var (n - 1).+1).[ren (+1)].
{ by do 2 (rewrite ifF; [|lia]). }
asimpl.
have->: (n - 1).+1 = n by lia.
case (boolP (eqn (n - lo) 0)); asimpl=>// h2.
have{}h2: n > lo by lia.
case (boolP (eqn (n - hi) 0)); asimpl=>// h3.
by have->: (n - 1).+1 = n by lia.
Qed.
Lemma fvu2_subst sub lo hi s σ1 σ2 :
fvu2 sub lo hi s ->
(forall i, (i < sub) \/ (lo <= i /\ i < hi) -> σ1 i = σ2 i) ->
s.[σ1] = s.[σ2].
Proof.
elim: s sub lo hi σ1 σ2=>//=.
- rewrite /fvu2.
move=> x sub lo hi σ1 σ2 /= e.
have[h|h]: (x < sub) \/ (lo <= x /\ x < hi).
{ move: e. case (boolP (x < sub)); [left|]=>// xsub.
case (boolP (x < lo))=> xlo.
- by intros; injections; lia.
- case (boolP (x < hi)).
by right; lia.
by intros; injections; lia. }
+ apply. by left.
+ apply. by right.
- move=> > hs > ht sub lo hi > fvu1 *.
by f_equal; [ apply (hs sub lo hi) | apply (ht sub lo hi)];
move: fvu1; prove_fvu2.
- move=> > hs > ht sub lo hi > fvu1 *.
by f_equal; [ apply (hs sub lo hi) | apply (ht sub lo hi)];
move: fvu1; prove_fvu2.
- move=> > hs ? sub lo hi > fvu1 *.
by f_equal; apply (hs sub lo hi); move: fvu1; prove_fvu2.
- move=> > h ? sub lo hi > /fvu2_lam fvu h1.
f_equal.
apply (h sub.+1 lo.+1 hi.+1)=>//.
case=>// i [] h2.
+ rewrite upn1 !upnP /= subSn1.
f_equal. apply h1. left. by lia.
+ rewrite upn1 !upnP /= subSn1.
f_equal. apply h1. right. done.
- move=> > hs ? sub lo hi > fvu1 *.
by f_equal; apply (hs sub lo hi); move: fvu1; prove_fvu2.
- move=> s hs sub lo hi σ1 σ2 /fvu2_tlam fvu1 h.
f_equal.
by apply (hs sub lo hi)=>//= i [h1|h1]; f_equal; apply h; [left|right].
- move=> s hs sub lo hi σ1 σ2 /fvu2_tall fvu1 h.
f_equal.
by apply (hs sub lo hi)=>//= i [h1|h1]; f_equal; apply h; [left|right].
- move=> > hs sub lo hi > fvu1 *.
by f_equal; apply (hs sub lo hi); move: fvu1; prove_fvu2.
- move=> > hs sub lo hi > fvu1 *.
by f_equal; apply (hs sub lo hi); move: fvu1; prove_fvu2.
Qed.
Important result of the section
Corollary fvu_subst lo hi s σ1 σ2 :
fvu lo hi s ->
(forall i, lo <= i -> i < hi -> σ1 i = σ2 i) ->
s.[σ1] = s.[σ2].
Proof.
rewrite -fvu_fvu2=> h1 h2.
apply fvu2_subst with 0 lo hi=>//.
move=> i [?|[??]]=>//.
by apply h2.
Qed.
Ltac simp_vnf :=
rewrite /var_not_free; asimpl;
intros; injections; f_equal.
Lemma var_not_free_hsubst s n θ:
var_not_free n s ->
var_not_free n s.|[θ].
Proof.
elim: s n θ=>//.
- asimpl=> > h1 > h2 > [e1 e2]. simp_vnf.
by apply h1.
by apply h2.
- asimpl=> > h1 > h2 > [e1 e2]. simp_vnf.
by apply h1. by apply h2.
- asimpl=> > h1 >. simp_vnf.
by apply h1.
- asimpl=> s h1 U n θ. simp_vnf.
rewrite subst_var_lemma_up1_alt in H.
rewrite subst_var_lemma_up1_alt.
rewrite /var_not_free in h1.
rewrite -{2}(h1 n.+1).
+ f_equal; f_ext; case=>//= x.
rewrite subSn1.
by case (boolP (eqn x n))=>//=.
+ clear h1.
rewrite -H.
f_equal=>//.
f_ext; case=>//= x.
rewrite subSn1.
by case (boolP (eqn x n))=>//=.
- asimpl=> > h1 >. simp_vnf. by apply h1.
- asimpl=> s h1 n θ. simp_vnf.
rewrite subst_var_tsubst_recipe_alt_3.
rewrite subst_var_tsubst_recipe_alt_3 in H.
by apply h1.
- asimpl=> s h1 n θ. simp_vnf.
rewrite subst_var_tsubst_recipe_alt_3.
rewrite subst_var_tsubst_recipe_alt_3 in H.
by apply h1.
- asimpl=> > h1 >. simp_vnf. by apply h1.
- asimpl=> > h1 >. simp_vnf. by apply h1.
Qed.
Ltac unfold_var_not_free :=
match goal with
| h: var_not_free _ _ |- _ =>
move: h; rewrite/var_not_free/=; intros; injections; f_equal
end.
Lemma var_not_free_neu s n:
var_not_free n s ->
var_not_free n (neu s).
Proof.
elim: s n;
try (by rewrite /var_not_free/==> *; injections; f_equal; eauto).
- rewrite /var_not_free/=.
move=> s hs U n h; injections; f_equal.
specialize (hs n.+1).
rewrite subst_var_lemma_up1_alt.
rewrite subst_var_lemma_up1_alt in H.
rewrite -{2}hs=>//=.
+ f_equal; f_ext; case=>//= x.
have->: x.+1 - 1 = x by lia.
by asimpl.
+ rewrite -{2}H.
f_equal; f_ext; case=>//= x.
have->: x.+1 - 1 = x by lia.
by asimpl.
- rewrite /var_not_free/=.
move=> s hs n h; injections; f_equal.
rewrite subst_var_tsubst_recipe_alt hs=>//.
by rewrite subst_var_tsubst_recipe_alt in H.
- rewrite /var_not_free/=.
move=> s hs n h; injections; f_equal.
rewrite subst_var_tsubst_recipe_alt hs=>//.
by rewrite subst_var_tsubst_recipe_alt in H.
Qed.
Lemma subst_var2_up n :
up (subst_var2 n (ids n.+1)) =
subst_var2 n.+1 (ids n.+2) .
Proof.
rewrite subst_var_lemma_up1_alt.
f_ext=> x.
case (boolP (x < 1))=> lt; asimpl;
case (boolP (eqn x n.+1))=> h2.
+ by lia.
+ by rewrite /subst_var2/= ifF; [|lia].
+ case (boolP (eqn (x-1) n))=> h3 //=.
by rewrite /subst_var2/= ifT; [|lia].
by lia.
+ case (boolP (eqn (x-1) n))=> h3 //=.
by lia.
by rewrite /subst_var2/= ifF; [|lia].
Qed.
Lemma golfouse b n k u :
b <= n -> n <= k ->
fvu2 b n k u <->
(forall i, b <= i -> (i < n \/ k <= i) -> u.[subst_var2 i (Var i.+1)] = u).
Proof.
elim: u b n k=>//.
{ move=> x b n k bn nk.
split=> h.
- case (fvu2_var h)=>{}h.
+ rewrite /subst_var2.
move=> i bi [] h2 /=;
by rewrite ifF; [autosubst|lia].
+ rewrite /subst_var2/=.
move=> i bi [] h2.
(* b <= i < n <= x < k *)
by rewrite ifF; [autosubst|lia].
(* b <= n <= x < k <= i *)
by rewrite ifF; [autosubst|lia].
- rewrite /fvu2/=.
case (boolP (x < b))=>// xb.
case (boolP (x < n))=>// xn.
+ (* b <= x < n <= k *)
rewrite -(h x) /= /subst_var2; try lia.
by rewrite ifT.
+ (* b <= n <= k <= x *)
case (boolP (x < k))=>// xk.
rewrite -(h x) /= /subst_var2; try lia.
by rewrite ifT. }
{ move=> s h1 t h2 b n k bn nk.
split.
- rewrite /fvu2=> *; asimpl; injections.
f_equal.
by rewrite (proj1 (h1 _ _ _ bn nk)).
by rewrite (proj1 (h2 _ _ _ bn nk)).
- move=> h.
have hs: forall i : nat,
b <= i -> i < n \/ k <= i ->
s.[subst_var2 i (Var i.+1)] = s.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
have ht: forall i : nat,
b <= i -> i < n \/ k <= i ->
t.[subst_var2 i (Var i.+1)] = t.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
rewrite /fvu2/=; f_equal.
by apply (h1 _ _ _ bn nk).
by apply (h2 _ _ _ bn nk). }
{ move=> s h1 t h2 b n k bn nk.
split.
- rewrite /fvu2=> *; asimpl; injections.
f_equal.
by rewrite (proj1 (h1 _ _ _ bn nk)).
by rewrite (proj1 (h2 _ _ _ bn nk)).
- move=> h.
have hs: forall i : nat,
b <= i -> i < n \/ k <= i ->
s.[subst_var2 i (Var i.+1)] = s.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
have ht: forall i : nat,
b <= i -> i < n \/ k <= i ->
t.[subst_var2 i (Var i.+1)] = t.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
rewrite /fvu2/=; f_equal.
by apply (h1 _ _ _ bn nk).
by apply (h2 _ _ _ bn nk). }
{ move=> s h1 S b n k bn nk.
split.
- rewrite /fvu2=> *; asimpl; injections.
f_equal.
by rewrite (proj1 (h1 _ _ _ bn nk)).
- move=> h.
have hs: forall i : nat,
b <= i -> i < n \/ k <= i ->
s.[subst_var2 i (Var i.+1)] = s.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
rewrite /fvu2/=; f_equal.
by apply (h1 _ _ _ bn nk). }
{ move=> s ih U b n k bn nk.
split=> h.
- apply fvu2_lam in h.
move=> i hb2 [] hi /=; f_equal; rewrite subst_var2_up.
+ have{}bn: b.+1 <= n.+1 by lia.
have{}nk: n.+1 <= k.+1 by lia.
have:= proj1 (ih _ _ _ bn nk).
apply=>//.
lia.
+ have{}bn: b.+1 <= n.+1 by lia.
have{}nk: n.+1 <= k.+1 by lia.
have:= proj1 (ih _ _ _ bn nk).
apply=>//.
lia.
- rewrite/fvu2/=; f_equal.
have{}h:
forall i : nat,
b <= i -> i < n \/ k <= i ->
s.[subst_var2 i.+1 (Var i.+2)] = s.
{ clear_except h=> i h1 h2.
specialize (h i h1 h2).
simpl in h. injection h.
by rewrite subst_var2_up. }
have->: up (fun i =>
if i < b then Var i else
if i < n then Var i.+1 else
if i < k then Var i else Var i.+1)
= (fun i =>
if i < b.+1 then Var i else
if i < n.+1 then Var i.+1 else
if i < k.+1 then Var i else Var i.+1).
{ f_ext=> -[]//= x; rewrite upn1 upnP=>/=.
have->: x.+1 - 1 = x by lia.
have->: (x.+1 < b.+1) = (x < b) by lia.
have->: (x.+1 < n.+1) = (x < n) by lia.
have->: (x.+1 < k.+1) = (x < k) by lia.
by case (x < b);
case (x < n);
case (x < k). }
have: fvu2 b.+1 n.+1 k.+1 s. 2: apply.
apply ih=>// i bi hi.
have?: 0 < i by lia.
rewrite -{2}(h i.-1)=>//.
by have->: i.-1.+1 = i by lia.
by lia.
by lia. }
{ move=> s h1 f b n k bn nk.
split.
- rewrite /fvu2=> *; asimpl; injections.
f_equal.
by rewrite (proj1 (h1 _ _ _ bn nk)).
- move=> h.
have hs: forall i : nat,
b <= i -> i < n \/ k <= i ->
s.[subst_var2 i (Var i.+1)] = s.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
rewrite /fvu2/=; f_equal.
by apply (h1 _ _ _ bn nk). }
{ move=> s h1 b n k bn nk.
split.
- move=>h i l r; asimpl.
f_equal.
rewrite subst_var_tsubst_recipe_alt.
rewrite (proj1 (h1 _ _ _ bn nk))=>//.
by apply fvu2_tlam.
- move=>h. apply fvu2_tlam_op.
apply h1=>//.
move=> i hi1 hi2. specialize (h i hi1 hi2).
simpl in h; injection h.
by rewrite subst_var_tsubst_recipe_alt. }
{ move=> s h1 b n k bn nk.
split.
- move=>h i l r; asimpl.
f_equal.
rewrite subst_var_tsubst_recipe_alt.
rewrite (proj1 (h1 _ _ _ bn nk))=>//.
by apply fvu2_tall.
- move=>h. apply fvu2_tall_op.
apply h1=>//.
move=> i hi1 hi2. specialize (h i hi1 hi2).
simpl in h; injection h.
by rewrite subst_var_tsubst_recipe_alt. }
{ move=> s h1 b n k bn nk.
split.
- rewrite /fvu2=> *; asimpl; injections.
f_equal.
by rewrite (proj1 (h1 _ _ _ bn nk)).
- move=> h.
have hs: forall i : nat,
b <= i -> i < n \/ k <= i ->
s.[subst_var2 i (Var i.+1)] = s.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
rewrite /fvu2/=; f_equal.
by apply (h1 _ _ _ bn nk). }
{ move=> s h1 b n k bn nk.
split.
- rewrite /fvu2=> *; asimpl; injections.
f_equal.
by rewrite (proj1 (h1 _ _ _ bn nk)).
- move=> h.
have hs: forall i : nat,
b <= i -> i < n \/ k <= i ->
s.[subst_var2 i (Var i.+1)] = s.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
rewrite /fvu2/=; f_equal.
by apply (h1 _ _ _ bn nk). }
Qed.
Corollary golfousec_le n k u :
n <= k ->
fvu n k u <->
(forall i, (i < n \/ k <= i) -> u.[subst_var2 i (Var i.+1)] = u).
Proof.
have:= @golfouse 0 n k u.
rewrite fvu_fvu2=>h nk.
split=>h1*; apply h=>//.
intros.
by apply h1.
Qed.
Lemma neu_eq_fv s t n :
fv n s ->
neu s = neu t ->
fv n t.
Proof.
elim: s t n.
- by move=> > ? /inversion_neu_var ->.
- by move=> /= > ? /inversion_neu_top [] ->; rewrite /fv/=.
- by move=> /= > ? /inversion_neu_top [] ->; rewrite /fv/=.
- move=> s h1 t h2 > /fv_and [??] /inversion_neu_and [?[?[?[??]]]].
subst. by apply fv_and; split; eauto.
- move=> s h1 t h2 > /fv_app [??] /inversion_neu_app [?[?[?[??]]]].
subst. by apply fv_app; split; eauto.
- move=> s h1 > /fv_tapp ? /inversion_neu_tapp [?[??]].
subst. by apply fv_tapp; eauto.
- move=> s h1 > /fv_lam ? /inversion_neu_lam [?[??]].
subst. by apply fv_lam; eauto.
- move=> s h1 > /fv_imp ? /inversion_neu_imp [?[??]].
subst. by apply fv_imp; eauto.
- move=> s h1 > /fv_tlam ? /inversion_neu_tlam [?[??]].
subst. by apply fv_tlam; eauto.
- move=> s h1 > /fv_tall ? /inversion_neu_tall [?[??]].
subst. by apply fv_tall; eauto.
- move=> s h1 > /fv_neu ? /inversion_neu_neu [?[??]].
subst. by apply fv_neu; eauto.
- move=> s h1 > /fv_box ? /inversion_neu_box [?[??]].
subst. by apply fv_box; eauto.
Qed.
Corollary neu_eq_closed s t :
closed s ->
neu s = neu t ->
closed t.
Proof.
rewrite !/closed.
by apply neu_eq_fv.
Qed.
Lemma neu_eq_fvh s t n :
fvh n s ->
neu s = neu t ->
fvh n t.
Proof.
elim: s t n.
- by move=> > ? /inversion_neu_var ->.
- by move=> /= > ? /inversion_neu_top [] ->; rewrite /fv/=.
- by move=> /= > ? /inversion_neu_top [] ->; rewrite /fv/=.
- move=> s h1 t h2 > /fvh_and [??] /inversion_neu_and [?[?[?[??]]]].
subst. by apply fvh_and; split; eauto.
- move=> s h1 t h2 > /fvh_app [??] /inversion_neu_app [?[?[?[??]]]].
subst. by apply fvh_app; split; eauto.
- move=> s h1 > /fvh_tapp [??] /inversion_neu_tapp [?[??]].
subst. by apply fvh_tapp; eauto.
- move=> s h1 > /fvh_lam ? /inversion_neu_lam [?[??]].
subst. by apply fvh_lam; eauto.
- move=> s h1 > /fvh_imp [??] /inversion_neu_imp [?[??]].
subst. by apply fvh_imp; eauto.
- move=> s h1 > /fvh_tlam ? /inversion_neu_tlam [?[??]].
subst. by apply fvh_tlam; eauto.
- move=> s h1 > /fvh_tall ? /inversion_neu_tall [?[??]].
subst. by apply fvh_tall; eauto.
- move=> s h1 > /fvh_neu ? /inversion_neu_neu [?[??]].
subst. by apply fvh_neu; eauto.
- move=> s h1 > /fvh_box ? /inversion_neu_box [?[??]].
subst. by apply fvh_box; eauto.
Qed.
Corollary neu_eq_closedh s t n :
fvh n s ->
neu s = neu t ->
fvh n t.
Proof.
rewrite !/closed.
by apply neu_eq_fvh.
Qed.
fvu lo hi s ->
(forall i, lo <= i -> i < hi -> σ1 i = σ2 i) ->
s.[σ1] = s.[σ2].
Proof.
rewrite -fvu_fvu2=> h1 h2.
apply fvu2_subst with 0 lo hi=>//.
move=> i [?|[??]]=>//.
by apply h2.
Qed.
Ltac simp_vnf :=
rewrite /var_not_free; asimpl;
intros; injections; f_equal.
Lemma var_not_free_hsubst s n θ:
var_not_free n s ->
var_not_free n s.|[θ].
Proof.
elim: s n θ=>//.
- asimpl=> > h1 > h2 > [e1 e2]. simp_vnf.
by apply h1.
by apply h2.
- asimpl=> > h1 > h2 > [e1 e2]. simp_vnf.
by apply h1. by apply h2.
- asimpl=> > h1 >. simp_vnf.
by apply h1.
- asimpl=> s h1 U n θ. simp_vnf.
rewrite subst_var_lemma_up1_alt in H.
rewrite subst_var_lemma_up1_alt.
rewrite /var_not_free in h1.
rewrite -{2}(h1 n.+1).
+ f_equal; f_ext; case=>//= x.
rewrite subSn1.
by case (boolP (eqn x n))=>//=.
+ clear h1.
rewrite -H.
f_equal=>//.
f_ext; case=>//= x.
rewrite subSn1.
by case (boolP (eqn x n))=>//=.
- asimpl=> > h1 >. simp_vnf. by apply h1.
- asimpl=> s h1 n θ. simp_vnf.
rewrite subst_var_tsubst_recipe_alt_3.
rewrite subst_var_tsubst_recipe_alt_3 in H.
by apply h1.
- asimpl=> s h1 n θ. simp_vnf.
rewrite subst_var_tsubst_recipe_alt_3.
rewrite subst_var_tsubst_recipe_alt_3 in H.
by apply h1.
- asimpl=> > h1 >. simp_vnf. by apply h1.
- asimpl=> > h1 >. simp_vnf. by apply h1.
Qed.
Ltac unfold_var_not_free :=
match goal with
| h: var_not_free _ _ |- _ =>
move: h; rewrite/var_not_free/=; intros; injections; f_equal
end.
Lemma var_not_free_neu s n:
var_not_free n s ->
var_not_free n (neu s).
Proof.
elim: s n;
try (by rewrite /var_not_free/==> *; injections; f_equal; eauto).
- rewrite /var_not_free/=.
move=> s hs U n h; injections; f_equal.
specialize (hs n.+1).
rewrite subst_var_lemma_up1_alt.
rewrite subst_var_lemma_up1_alt in H.
rewrite -{2}hs=>//=.
+ f_equal; f_ext; case=>//= x.
have->: x.+1 - 1 = x by lia.
by asimpl.
+ rewrite -{2}H.
f_equal; f_ext; case=>//= x.
have->: x.+1 - 1 = x by lia.
by asimpl.
- rewrite /var_not_free/=.
move=> s hs n h; injections; f_equal.
rewrite subst_var_tsubst_recipe_alt hs=>//.
by rewrite subst_var_tsubst_recipe_alt in H.
- rewrite /var_not_free/=.
move=> s hs n h; injections; f_equal.
rewrite subst_var_tsubst_recipe_alt hs=>//.
by rewrite subst_var_tsubst_recipe_alt in H.
Qed.
Lemma subst_var2_up n :
up (subst_var2 n (ids n.+1)) =
subst_var2 n.+1 (ids n.+2) .
Proof.
rewrite subst_var_lemma_up1_alt.
f_ext=> x.
case (boolP (x < 1))=> lt; asimpl;
case (boolP (eqn x n.+1))=> h2.
+ by lia.
+ by rewrite /subst_var2/= ifF; [|lia].
+ case (boolP (eqn (x-1) n))=> h3 //=.
by rewrite /subst_var2/= ifT; [|lia].
by lia.
+ case (boolP (eqn (x-1) n))=> h3 //=.
by lia.
by rewrite /subst_var2/= ifF; [|lia].
Qed.
Lemma golfouse b n k u :
b <= n -> n <= k ->
fvu2 b n k u <->
(forall i, b <= i -> (i < n \/ k <= i) -> u.[subst_var2 i (Var i.+1)] = u).
Proof.
elim: u b n k=>//.
{ move=> x b n k bn nk.
split=> h.
- case (fvu2_var h)=>{}h.
+ rewrite /subst_var2.
move=> i bi [] h2 /=;
by rewrite ifF; [autosubst|lia].
+ rewrite /subst_var2/=.
move=> i bi [] h2.
(* b <= i < n <= x < k *)
by rewrite ifF; [autosubst|lia].
(* b <= n <= x < k <= i *)
by rewrite ifF; [autosubst|lia].
- rewrite /fvu2/=.
case (boolP (x < b))=>// xb.
case (boolP (x < n))=>// xn.
+ (* b <= x < n <= k *)
rewrite -(h x) /= /subst_var2; try lia.
by rewrite ifT.
+ (* b <= n <= k <= x *)
case (boolP (x < k))=>// xk.
rewrite -(h x) /= /subst_var2; try lia.
by rewrite ifT. }
{ move=> s h1 t h2 b n k bn nk.
split.
- rewrite /fvu2=> *; asimpl; injections.
f_equal.
by rewrite (proj1 (h1 _ _ _ bn nk)).
by rewrite (proj1 (h2 _ _ _ bn nk)).
- move=> h.
have hs: forall i : nat,
b <= i -> i < n \/ k <= i ->
s.[subst_var2 i (Var i.+1)] = s.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
have ht: forall i : nat,
b <= i -> i < n \/ k <= i ->
t.[subst_var2 i (Var i.+1)] = t.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
rewrite /fvu2/=; f_equal.
by apply (h1 _ _ _ bn nk).
by apply (h2 _ _ _ bn nk). }
{ move=> s h1 t h2 b n k bn nk.
split.
- rewrite /fvu2=> *; asimpl; injections.
f_equal.
by rewrite (proj1 (h1 _ _ _ bn nk)).
by rewrite (proj1 (h2 _ _ _ bn nk)).
- move=> h.
have hs: forall i : nat,
b <= i -> i < n \/ k <= i ->
s.[subst_var2 i (Var i.+1)] = s.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
have ht: forall i : nat,
b <= i -> i < n \/ k <= i ->
t.[subst_var2 i (Var i.+1)] = t.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
rewrite /fvu2/=; f_equal.
by apply (h1 _ _ _ bn nk).
by apply (h2 _ _ _ bn nk). }
{ move=> s h1 S b n k bn nk.
split.
- rewrite /fvu2=> *; asimpl; injections.
f_equal.
by rewrite (proj1 (h1 _ _ _ bn nk)).
- move=> h.
have hs: forall i : nat,
b <= i -> i < n \/ k <= i ->
s.[subst_var2 i (Var i.+1)] = s.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
rewrite /fvu2/=; f_equal.
by apply (h1 _ _ _ bn nk). }
{ move=> s ih U b n k bn nk.
split=> h.
- apply fvu2_lam in h.
move=> i hb2 [] hi /=; f_equal; rewrite subst_var2_up.
+ have{}bn: b.+1 <= n.+1 by lia.
have{}nk: n.+1 <= k.+1 by lia.
have:= proj1 (ih _ _ _ bn nk).
apply=>//.
lia.
+ have{}bn: b.+1 <= n.+1 by lia.
have{}nk: n.+1 <= k.+1 by lia.
have:= proj1 (ih _ _ _ bn nk).
apply=>//.
lia.
- rewrite/fvu2/=; f_equal.
have{}h:
forall i : nat,
b <= i -> i < n \/ k <= i ->
s.[subst_var2 i.+1 (Var i.+2)] = s.
{ clear_except h=> i h1 h2.
specialize (h i h1 h2).
simpl in h. injection h.
by rewrite subst_var2_up. }
have->: up (fun i =>
if i < b then Var i else
if i < n then Var i.+1 else
if i < k then Var i else Var i.+1)
= (fun i =>
if i < b.+1 then Var i else
if i < n.+1 then Var i.+1 else
if i < k.+1 then Var i else Var i.+1).
{ f_ext=> -[]//= x; rewrite upn1 upnP=>/=.
have->: x.+1 - 1 = x by lia.
have->: (x.+1 < b.+1) = (x < b) by lia.
have->: (x.+1 < n.+1) = (x < n) by lia.
have->: (x.+1 < k.+1) = (x < k) by lia.
by case (x < b);
case (x < n);
case (x < k). }
have: fvu2 b.+1 n.+1 k.+1 s. 2: apply.
apply ih=>// i bi hi.
have?: 0 < i by lia.
rewrite -{2}(h i.-1)=>//.
by have->: i.-1.+1 = i by lia.
by lia.
by lia. }
{ move=> s h1 f b n k bn nk.
split.
- rewrite /fvu2=> *; asimpl; injections.
f_equal.
by rewrite (proj1 (h1 _ _ _ bn nk)).
- move=> h.
have hs: forall i : nat,
b <= i -> i < n \/ k <= i ->
s.[subst_var2 i (Var i.+1)] = s.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
rewrite /fvu2/=; f_equal.
by apply (h1 _ _ _ bn nk). }
{ move=> s h1 b n k bn nk.
split.
- move=>h i l r; asimpl.
f_equal.
rewrite subst_var_tsubst_recipe_alt.
rewrite (proj1 (h1 _ _ _ bn nk))=>//.
by apply fvu2_tlam.
- move=>h. apply fvu2_tlam_op.
apply h1=>//.
move=> i hi1 hi2. specialize (h i hi1 hi2).
simpl in h; injection h.
by rewrite subst_var_tsubst_recipe_alt. }
{ move=> s h1 b n k bn nk.
split.
- move=>h i l r; asimpl.
f_equal.
rewrite subst_var_tsubst_recipe_alt.
rewrite (proj1 (h1 _ _ _ bn nk))=>//.
by apply fvu2_tall.
- move=>h. apply fvu2_tall_op.
apply h1=>//.
move=> i hi1 hi2. specialize (h i hi1 hi2).
simpl in h; injection h.
by rewrite subst_var_tsubst_recipe_alt. }
{ move=> s h1 b n k bn nk.
split.
- rewrite /fvu2=> *; asimpl; injections.
f_equal.
by rewrite (proj1 (h1 _ _ _ bn nk)).
- move=> h.
have hs: forall i : nat,
b <= i -> i < n \/ k <= i ->
s.[subst_var2 i (Var i.+1)] = s.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
rewrite /fvu2/=; f_equal.
by apply (h1 _ _ _ bn nk). }
{ move=> s h1 b n k bn nk.
split.
- rewrite /fvu2=> *; asimpl; injections.
f_equal.
by rewrite (proj1 (h1 _ _ _ bn nk)).
- move=> h.
have hs: forall i : nat,
b <= i -> i < n \/ k <= i ->
s.[subst_var2 i (Var i.+1)] = s.
{ move=> i hi1 hi2. specialize (h i hi1 hi2).
by simpl in h; injections. }
rewrite /fvu2/=; f_equal.
by apply (h1 _ _ _ bn nk). }
Qed.
Corollary golfousec_le n k u :
n <= k ->
fvu n k u <->
(forall i, (i < n \/ k <= i) -> u.[subst_var2 i (Var i.+1)] = u).
Proof.
have:= @golfouse 0 n k u.
rewrite fvu_fvu2=>h nk.
split=>h1*; apply h=>//.
intros.
by apply h1.
Qed.
Lemma neu_eq_fv s t n :
fv n s ->
neu s = neu t ->
fv n t.
Proof.
elim: s t n.
- by move=> > ? /inversion_neu_var ->.
- by move=> /= > ? /inversion_neu_top [] ->; rewrite /fv/=.
- by move=> /= > ? /inversion_neu_top [] ->; rewrite /fv/=.
- move=> s h1 t h2 > /fv_and [??] /inversion_neu_and [?[?[?[??]]]].
subst. by apply fv_and; split; eauto.
- move=> s h1 t h2 > /fv_app [??] /inversion_neu_app [?[?[?[??]]]].
subst. by apply fv_app; split; eauto.
- move=> s h1 > /fv_tapp ? /inversion_neu_tapp [?[??]].
subst. by apply fv_tapp; eauto.
- move=> s h1 > /fv_lam ? /inversion_neu_lam [?[??]].
subst. by apply fv_lam; eauto.
- move=> s h1 > /fv_imp ? /inversion_neu_imp [?[??]].
subst. by apply fv_imp; eauto.
- move=> s h1 > /fv_tlam ? /inversion_neu_tlam [?[??]].
subst. by apply fv_tlam; eauto.
- move=> s h1 > /fv_tall ? /inversion_neu_tall [?[??]].
subst. by apply fv_tall; eauto.
- move=> s h1 > /fv_neu ? /inversion_neu_neu [?[??]].
subst. by apply fv_neu; eauto.
- move=> s h1 > /fv_box ? /inversion_neu_box [?[??]].
subst. by apply fv_box; eauto.
Qed.
Corollary neu_eq_closed s t :
closed s ->
neu s = neu t ->
closed t.
Proof.
rewrite !/closed.
by apply neu_eq_fv.
Qed.
Lemma neu_eq_fvh s t n :
fvh n s ->
neu s = neu t ->
fvh n t.
Proof.
elim: s t n.
- by move=> > ? /inversion_neu_var ->.
- by move=> /= > ? /inversion_neu_top [] ->; rewrite /fv/=.
- by move=> /= > ? /inversion_neu_top [] ->; rewrite /fv/=.
- move=> s h1 t h2 > /fvh_and [??] /inversion_neu_and [?[?[?[??]]]].
subst. by apply fvh_and; split; eauto.
- move=> s h1 t h2 > /fvh_app [??] /inversion_neu_app [?[?[?[??]]]].
subst. by apply fvh_app; split; eauto.
- move=> s h1 > /fvh_tapp [??] /inversion_neu_tapp [?[??]].
subst. by apply fvh_tapp; eauto.
- move=> s h1 > /fvh_lam ? /inversion_neu_lam [?[??]].
subst. by apply fvh_lam; eauto.
- move=> s h1 > /fvh_imp [??] /inversion_neu_imp [?[??]].
subst. by apply fvh_imp; eauto.
- move=> s h1 > /fvh_tlam ? /inversion_neu_tlam [?[??]].
subst. by apply fvh_tlam; eauto.
- move=> s h1 > /fvh_tall ? /inversion_neu_tall [?[??]].
subst. by apply fvh_tall; eauto.
- move=> s h1 > /fvh_neu ? /inversion_neu_neu [?[??]].
subst. by apply fvh_neu; eauto.
- move=> s h1 > /fvh_box ? /inversion_neu_box [?[??]].
subst. by apply fvh_box; eauto.
Qed.
Corollary neu_eq_closedh s t n :
fvh n s ->
neu s = neu t ->
fvh n t.
Proof.
rewrite !/closed.
by apply neu_eq_fvh.
Qed.
Under upn k θ, any j < k keeps its status.
Lemma var_not_free_upn_lt_gen j k (θ : var -> term) (f : term) :
j < k ->
var_not_free j f ->
var_not_free j f.[upn k θ].
Proof.
elim: f j k θ;
rewrite /var_not_free/= =>//;
try (by move=> > h1 > h2 > hjk [e1 e2]; f_equal; [apply h1|apply h2]);
try (by move=> > h1 > hjk [e1]; f_equal; apply h1).
- move=> x j k θ hjk.
rewrite {1}/subst_var2.
case (boolP (x == j))=> hx.
+ by rewrite (eqP hx)=> [[]]; lia.
+ move=> _.
rewrite upnP; case: ifPn=> hxk.
* by rewrite /= /subst_var2 (negbTE hx).
* have hh: var_not_free j (θ (x - k)).[upn 0 (ren (+k))]
by apply var_not_free_upn_mid; lia.
by move: hh; rewrite upn0 /var_not_free.
- move=> f h1 j k θ hjk [e1].
have e: (up (subst_var2 j (ids j.+1)) : var -> term)
= subst_var2 j.+1 (ids j.+2)
by rewrite upn1 subst_var_lemma_up1_alt_2 addn1.
rewrite e.
rewrite fold_up_upn; f_equal.
rewrite e in e1.
by apply h1.
Qed.
Lemma upn_hcomp k (σ : var -> recipe) (θ : var -> term) :
(upn k σ) >>| θ = upn k (σ >>| θ).
Proof.
elim: k σ=> [|k ih] σ //=.
asimpl.
by rewrite !iterate_S ih.
Qed.
j < k ->
var_not_free j f ->
var_not_free j f.[upn k θ].
Proof.
elim: f j k θ;
rewrite /var_not_free/= =>//;
try (by move=> > h1 > h2 > hjk [e1 e2]; f_equal; [apply h1|apply h2]);
try (by move=> > h1 > hjk [e1]; f_equal; apply h1).
- move=> x j k θ hjk.
rewrite {1}/subst_var2.
case (boolP (x == j))=> hx.
+ by rewrite (eqP hx)=> [[]]; lia.
+ move=> _.
rewrite upnP; case: ifPn=> hxk.
* by rewrite /= /subst_var2 (negbTE hx).
* have hh: var_not_free j (θ (x - k)).[upn 0 (ren (+k))]
by apply var_not_free_upn_mid; lia.
by move: hh; rewrite upn0 /var_not_free.
- move=> f h1 j k θ hjk [e1].
have e: (up (subst_var2 j (ids j.+1)) : var -> term)
= subst_var2 j.+1 (ids j.+2)
by rewrite upn1 subst_var_lemma_up1_alt_2 addn1.
rewrite e.
rewrite fold_up_upn; f_equal.
rewrite e in e1.
by apply h1.
Qed.
Lemma upn_hcomp k (σ : var -> recipe) (θ : var -> term) :
(upn k σ) >>| θ = upn k (σ >>| θ).
Proof.
elim: k σ=> [|k ih] σ //=.
asimpl.
by rewrite !iterate_S ih.
Qed.
Lemma ren_upn_ren (t : recipe) m j k :
j <= m ->
t.|[ren (+m)].|[upn j (ren (+k))] = t.|[ren (+(m + k))].
Proof.
move=> *.
asimpl.
f_equal.
f_ext=> ?.
rewrite /funcomp upn_ren_app /ren /funcomp /lift.
case: ifP=> [/ltP|_]; first by lia.
f_equal.
by lia.
Qed.
Lemma ren_add (t : recipe) n k :
t.|[ren (+n)].|[ren (+k)] = t.|[ren (+(n + k))].
Proof.
asimpl.
by rewrite addnC.
Qed.
Lemma ren_upn_subst (t : recipe) m j (T : term) :
t.|[ren (+(m.+1 + j))].|[upn j (T .: ids)] = t.|[ren (+(m + j))].
Proof.
asimpl.
f_equal.
f_ext=> x.
rewrite /funcomp /lift upnP_cond; last by lia.
have->: m.+1 + j + x - j = (m + x).+1 by lia.
asimpl.
f_equal.
by lia.
Qed.
Lemma upn_add m n (θ : var -> term) :
upn m (upn n θ) = upn (m + n) θ.
Proof.
elim: m=> //= ? ih.
by rewrite !iterate_S ih.
Qed.
Lemma scons_hcomp (r : recipe) (θ : var -> term) :
(Box r .: ids) >>| θ = Box r.|[θ] .: ids.
Proof.
f_ext=> -[|?]; by asimpl.
Qed.
n quantifiers instantiated by the list of their terms, first for the outermost
Fixpoint inst (ts : seq term) : var -> term :=
match ts with
| [::] => ids
| t :: ts2 => upn (size ts2) (t .: ids) >> inst ts2
end.
Lemma inst_high ts k :
inst ts (size ts + k) = TVar k.
Proof.
elim: ts k=> //= ? ts ih k.
rewrite /funcomp upnP_cond; last by lia.
have->: (size ts).+1 + k - size ts = k.+1 by lia.
asimpl.
by rewrite ih.
Qed.
Lemma ren_inst ts :
ren (+ size ts) >> inst ts = ids.
Proof.
f_ext=> ?.
by rewrite /funcomp /= inst_high.
Qed.
Lemma inst_nth ts i :
i < size ts ->
inst ts (size ts - i.+1) = nth (TVar 0) ts i.
Proof.
elim: ts i=> //= ? ts ih [|i] ? /=.
- rewrite subn1 /= /funcomp upnP_cond// subnn /=.
by rewrite subst_comp ren_inst subst_id.
- rewrite /funcomp upn_k_sigma_x; last by lia.
have->: (size ts).+1 - i.+2 = size ts - i.+1 by lia.
by rewrite /= ih.
Qed.
match ts with
| [::] => ids
| t :: ts2 => upn (size ts2) (t .: ids) >> inst ts2
end.
Lemma inst_high ts k :
inst ts (size ts + k) = TVar k.
Proof.
elim: ts k=> //= ? ts ih k.
rewrite /funcomp upnP_cond; last by lia.
have->: (size ts).+1 + k - size ts = k.+1 by lia.
asimpl.
by rewrite ih.
Qed.
Lemma ren_inst ts :
ren (+ size ts) >> inst ts = ids.
Proof.
f_ext=> ?.
by rewrite /funcomp /= inst_high.
Qed.
Lemma inst_nth ts i :
i < size ts ->
inst ts (size ts - i.+1) = nth (TVar 0) ts i.
Proof.
elim: ts i=> //= ? ts ih [|i] ? /=.
- rewrite subn1 /= /funcomp upnP_cond// subnn /=.
by rewrite subst_comp ren_inst subst_id.
- rewrite /funcomp upn_k_sigma_x; last by lia.
have->: (size ts).+1 - i.+2 = size ts - i.+1 by lia.
by rewrite /= ih.
Qed.