Tealeaves.Backends.DB.DB
From Tealeaves.Misc Require Export
NaturalNumbers
Iterate.
From Tealeaves.Theory Require Export
DecoratedTraversableMonad.
Import DecoratedContainerMonad.
Import Kleisli.DecoratedTraversableMonad.
Import Kleisli.Theory.DecoratedTraversableFunctor.
Import DecoratedTraversableMonad.UsefulInstances.
Import PeanoNat.
#[local] Open Scope nat_scope.
Import DecoratedContainerFunctor.Notations.
Import DecoratedMonad.Notations.
Import Kleisli.Comonad.Notations.
Import Monoid.Notations.
Implicit Types (ρ: nat → nat).
#[local] Generalizable Variables W T U.
NaturalNumbers
Iterate.
From Tealeaves.Theory Require Export
DecoratedTraversableMonad.
Import DecoratedContainerMonad.
Import Kleisli.DecoratedTraversableMonad.
Import Kleisli.Theory.DecoratedTraversableFunctor.
Import DecoratedTraversableMonad.UsefulInstances.
Import PeanoNat.
#[local] Open Scope nat_scope.
Import DecoratedContainerFunctor.Notations.
Import DecoratedMonad.Notations.
Import Kleisli.Comonad.Notations.
Import Monoid.Notations.
Implicit Types (ρ: nat → nat).
#[local] Generalizable Variables W T U.
Section section.
Context
`{ret_inst: Return T}
`{Mapd_T_inst: Mapd nat T}
`{Mapd_U_inst: Mapd nat U}
`{Mapdt_U_inst: Mapdt nat U}
`{Bindd_U_inst: Bindd nat T U}
`{ToCtxset_U_inst: ToCtxset nat U}
`{! Compat_ToCtxset_Mapdt nat U}.
Context
`{ret_inst: Return T}
`{Mapd_T_inst: Mapd nat T}
`{Mapd_U_inst: Mapd nat U}
`{Mapdt_U_inst: Mapdt nat U}
`{Bindd_U_inst: Bindd nat T U}
`{ToCtxset_U_inst: ToCtxset nat U}
`{! Compat_ToCtxset_Mapdt nat U}.
Definition level_loc: nat × nat → nat :=
fun p ⇒ match p with
| (d, n) ⇒ n + 1 - d
end.
Definition level: U nat → nat :=
mapdReduce (op := Monoid_op_max) (unit := Monoid_unit_max)
level_loc.
fun p ⇒ match p with
| (d, n) ⇒ n + 1 - d
end.
Definition level: U nat → nat :=
mapdReduce (op := Monoid_op_max) (unit := Monoid_unit_max)
level_loc.
Definition bound_within_b (gap: nat): nat → nat → bool :=
fun ix depth ⇒ ix <? depth + gap.
Definition bound_b: nat → nat → bool :=
bound_within_b 0.
Definition cl_at_loc_b (gap: nat) (p: nat × nat): bool :=
match p with
| (depth, ix) ⇒ bound_within_b gap ix depth
end.
Definition cl_at_b (gap: nat) (t: U nat): bool :=
Forall_ctx_b (cl_at_loc_b gap) t.
Definition closed_b (t: U nat): bool :=
cl_at_b 0 t.
fun ix depth ⇒ ix <? depth + gap.
Definition bound_b: nat → nat → bool :=
bound_within_b 0.
Definition cl_at_loc_b (gap: nat) (p: nat × nat): bool :=
match p with
| (depth, ix) ⇒ bound_within_b gap ix depth
end.
Definition cl_at_b (gap: nat) (t: U nat): bool :=
Forall_ctx_b (cl_at_loc_b gap) t.
Definition closed_b (t: U nat): bool :=
cl_at_b 0 t.
Definition bound_within (gap: nat): nat → nat → Prop :=
fun ix depth ⇒ ix < depth + gap.
Definition bound: nat → nat → Prop :=
bound_within 0.
Definition cl_at_loc (gap: nat) (p: nat × nat): Prop :=
match p with
| (depth, ix) ⇒ bound_within gap ix depth
end.
Definition cl_at (gap: nat) (t: U nat): Prop :=
Forall_ctx (cl_at_loc gap) t.
Definition closed (t: U nat): Prop :=
cl_at 0 t.
fun ix depth ⇒ ix < depth + gap.
Definition bound: nat → nat → Prop :=
bound_within 0.
Definition cl_at_loc (gap: nat) (p: nat × nat): Prop :=
match p with
| (depth, ix) ⇒ bound_within gap ix depth
end.
Definition cl_at (gap: nat) (t: U nat): Prop :=
Forall_ctx (cl_at_loc gap) t.
Definition closed (t: U nat): Prop :=
cl_at 0 t.
Lemma bound_within_spec (gap: nat): ∀ (ix depth: nat),
bound_within_b gap ix depth = true ↔ ix < gap + depth.
Proof.
intros.
unfold bound_within_b.
rewrite Nat.ltb_lt.
lia.
Qed.
Lemma bound_within_spec_not (gap: nat): ∀ (ix depth: nat),
bound_within_b gap ix depth = false ↔ ¬ (ix < gap + depth).
Proof.
intros.
unfold bound_within_b.
rewrite Nat.ltb_nlt.
lia.
Qed.
Lemma bound_spec: ∀ (ix depth: nat),
bound_b ix depth = true ↔ ix < depth.
Proof.
intros.
unfold bound_b, bound_within_b.
rewrite Nat.ltb_lt.
lia.
Qed.
Lemma bound_spec_not: ∀ (ix depth: nat),
bound_b ix depth = false ↔ ¬ (ix < depth).
Proof.
intros.
unfold bound_b, bound_within_b.
rewrite Nat.ltb_nlt.
lia.
Qed.
Lemma cl_at_loc_spec {gap: nat}: ∀ (p: nat × nat),
cl_at_loc_b gap p = true ↔ cl_at_loc gap p.
Proof.
intros.
unfold cl_at_loc, cl_at_loc_b.
unfold bound_within_b, bound_within.
destruct p as [d n].
rewrite Nat.ltb_lt.
reflexivity.
Qed.
Corollary closed_at_spec `{! DecoratedTraversableFunctor nat U}:
∀ (gap: nat) (t: U nat),
cl_at_b gap t = true ↔ cl_at gap t.
Proof.
intros gap t.
unfold cl_at_b, cl_at.
rewrite decidable_Forall_ctx_b.
reflexivity.
apply cl_at_loc_spec.
Qed.
End section.
#[local] Infix "`bound in`" := (bound_b) (at level 10): tealeaves_scope.
bound_within_b gap ix depth = true ↔ ix < gap + depth.
Proof.
intros.
unfold bound_within_b.
rewrite Nat.ltb_lt.
lia.
Qed.
Lemma bound_within_spec_not (gap: nat): ∀ (ix depth: nat),
bound_within_b gap ix depth = false ↔ ¬ (ix < gap + depth).
Proof.
intros.
unfold bound_within_b.
rewrite Nat.ltb_nlt.
lia.
Qed.
Lemma bound_spec: ∀ (ix depth: nat),
bound_b ix depth = true ↔ ix < depth.
Proof.
intros.
unfold bound_b, bound_within_b.
rewrite Nat.ltb_lt.
lia.
Qed.
Lemma bound_spec_not: ∀ (ix depth: nat),
bound_b ix depth = false ↔ ¬ (ix < depth).
Proof.
intros.
unfold bound_b, bound_within_b.
rewrite Nat.ltb_nlt.
lia.
Qed.
Lemma cl_at_loc_spec {gap: nat}: ∀ (p: nat × nat),
cl_at_loc_b gap p = true ↔ cl_at_loc gap p.
Proof.
intros.
unfold cl_at_loc, cl_at_loc_b.
unfold bound_within_b, bound_within.
destruct p as [d n].
rewrite Nat.ltb_lt.
reflexivity.
Qed.
Corollary closed_at_spec `{! DecoratedTraversableFunctor nat U}:
∀ (gap: nat) (t: U nat),
cl_at_b gap t = true ↔ cl_at gap t.
Proof.
intros gap t.
unfold cl_at_b, cl_at.
rewrite decidable_Forall_ctx_b.
reflexivity.
apply cl_at_loc_spec.
Qed.
End section.
#[local] Infix "`bound in`" := (bound_b) (at level 10): tealeaves_scope.
Lemma bound_within_spec_b: ∀ ix d k,
bound_within_b k ix d =
ix `bound in` (d + k).
Proof.
intros. cbn. replace (d + k + 0) with (d + k) by lia.
reflexivity.
Qed.
Lemma bound_zero: ∀ ix,
ix `bound in` 0 = false.
Proof.
reflexivity.
Qed.
Lemma bound_lt: ∀ ix n,
ix < n → ix `bound in` n = true.
Proof.
introv Hlt.
rewrite <- Nat.ltb_lt in Hlt.
unfold bound_b, bound_within_b.
replace (n + 0) with n by lia.
destruct n; auto.
Qed.
Lemma bound_lt_iff: ∀ ix n,
ix < n ↔ ix `bound in` n = true.
Proof.
intros. split.
- apply bound_lt.
- cbn. destruct n.
+ inversion 1.
+ cbn. rewrite Nat.leb_le. lia.
Qed.
Lemma bound_ge: ∀ ix n,
ix ≥ n → ix `bound in` n = false.
Proof.
introv Hlt.
unfold bound_b, bound_within_b.
replace (n + 0) with n by lia.
destruct n; cbn; auto.
now rewrite Nat.leb_gt.
Qed.
Lemma bound_ge_iff: ∀ ix n,
ix ≥ n ↔ ix `bound in` n = false.
Proof.
intros. split.
- apply bound_ge.
- cbn. replace (n + 0) with n by lia.
destruct n.
+ lia.
+ intros.
rewrite Nat.leb_gt in H.
lia.
Qed.
Lemma bound_ind: ∀ ix n (P:Prop),
(ix ≥ n → ix `bound in` n = false → P) →
(ix < n → ix `bound in` n = true → P) →
P.
Proof.
introv.
rewrite <- bound_ge_iff.
rewrite <- bound_lt_iff.
introv Hge Hlt.
compare naturals ix and n; auto.
apply Hge; lia.
Qed.
Lemma bound_mono: ∀ ix n m,
m > n →
(ix `bound in` n = true) →
ix `bound in` m = true.
Proof.
introv Hlt Hbound.
rewrite <- bound_lt_iff in Hbound.
rewrite <- bound_lt_iff.
lia.
Qed.
Lemma bound_rev_mono: ∀ ix n m,
m < n →
bound_b ix n = false →
bound_b ix m = false.
Proof.
introv Hlt Hbound.
rewrite <- bound_ge_iff in Hbound.
rewrite <- bound_ge_iff.
lia.
Qed.
Lemma bound_1: ∀ ix,
bound_b ix 1 = true ↔ ix = 0.
Proof.
destruct ix; cbv; intuition.
Qed.
Ltac bound_induction :=
match goal with
| |- context[bound_b ?ix ?n] ⇒
apply (bound_ind ix n);
let Hord := fresh "Hord" in
let Hbound := fresh "Hbound" in
introv Hord Hbound;
try rewrite Hbound in *;
try solve [lia | easy]
end.
Ltac bound_induction_in H :=
match type of H with
| context[bound_b ?ix ?n] ⇒
apply (bound_ind ix n);
let Hord := fresh "Hord" in
let Hbound := fresh "Hbound" in
introv Hord Hbound;
try rewrite Hbound in *;
try solve [lia | easy]
end.
bound_within_b k ix d =
ix `bound in` (d + k).
Proof.
intros. cbn. replace (d + k + 0) with (d + k) by lia.
reflexivity.
Qed.
Lemma bound_zero: ∀ ix,
ix `bound in` 0 = false.
Proof.
reflexivity.
Qed.
Lemma bound_lt: ∀ ix n,
ix < n → ix `bound in` n = true.
Proof.
introv Hlt.
rewrite <- Nat.ltb_lt in Hlt.
unfold bound_b, bound_within_b.
replace (n + 0) with n by lia.
destruct n; auto.
Qed.
Lemma bound_lt_iff: ∀ ix n,
ix < n ↔ ix `bound in` n = true.
Proof.
intros. split.
- apply bound_lt.
- cbn. destruct n.
+ inversion 1.
+ cbn. rewrite Nat.leb_le. lia.
Qed.
Lemma bound_ge: ∀ ix n,
ix ≥ n → ix `bound in` n = false.
Proof.
introv Hlt.
unfold bound_b, bound_within_b.
replace (n + 0) with n by lia.
destruct n; cbn; auto.
now rewrite Nat.leb_gt.
Qed.
Lemma bound_ge_iff: ∀ ix n,
ix ≥ n ↔ ix `bound in` n = false.
Proof.
intros. split.
- apply bound_ge.
- cbn. replace (n + 0) with n by lia.
destruct n.
+ lia.
+ intros.
rewrite Nat.leb_gt in H.
lia.
Qed.
Lemma bound_ind: ∀ ix n (P:Prop),
(ix ≥ n → ix `bound in` n = false → P) →
(ix < n → ix `bound in` n = true → P) →
P.
Proof.
introv.
rewrite <- bound_ge_iff.
rewrite <- bound_lt_iff.
introv Hge Hlt.
compare naturals ix and n; auto.
apply Hge; lia.
Qed.
Lemma bound_mono: ∀ ix n m,
m > n →
(ix `bound in` n = true) →
ix `bound in` m = true.
Proof.
introv Hlt Hbound.
rewrite <- bound_lt_iff in Hbound.
rewrite <- bound_lt_iff.
lia.
Qed.
Lemma bound_rev_mono: ∀ ix n m,
m < n →
bound_b ix n = false →
bound_b ix m = false.
Proof.
introv Hlt Hbound.
rewrite <- bound_ge_iff in Hbound.
rewrite <- bound_ge_iff.
lia.
Qed.
Lemma bound_1: ∀ ix,
bound_b ix 1 = true ↔ ix = 0.
Proof.
destruct ix; cbv; intuition.
Qed.
Ltac bound_induction :=
match goal with
| |- context[bound_b ?ix ?n] ⇒
apply (bound_ind ix n);
let Hord := fresh "Hord" in
let Hbound := fresh "Hbound" in
introv Hord Hbound;
try rewrite Hbound in *;
try solve [lia | easy]
end.
Ltac bound_induction_in H :=
match type of H with
| context[bound_b ?ix ?n] ⇒
apply (bound_ind ix n);
let Hord := fresh "Hord" in
let Hbound := fresh "Hbound" in
introv Hord Hbound;
try rewrite Hbound in *;
try solve [lia | easy]
end.
Definition lift (x y: nat): nat := plus x y.
#[local] Notation "( + x )" := (lift x) (format "( + x )").
#[global] Arguments lift x y/.
Lemma lift0: (+0) = id. reflexivity. Qed.
Lemma lift_comp :∀ m n, (+m) ∘ (+n) = (+ (m + n)).
Proof.
intros. unfold compose, lift. ext y.
lia.
Qed.
Lemma lift_compR n m {X}(f: nat → X): (f ∘ (+m)) ∘ (+n) = f ∘ (+ (m + n)).
Proof.
now rewrite <- lift_comp.
Qed.
Lemma plusSn n m: S n + m = S (n + m). reflexivity. Qed.
Lemma plusnS n m: n + S m = S (n + m). symmetry. apply plus_n_Sm. Qed.
Lemma plusOn n: O + n = n. reflexivity. Qed.
Lemma plusnO n: n + O = n. symmetry. apply plus_n_O. Qed.
Ltac simplify_lift :=
progress repeat match goal with
| [|- context[(+0)]] ⇒ change (+0) with (@id nat)
| [|- context[?s S]] ⇒ change (s S) with (s (+1))
| [|- context[S ?n + ?m]] ⇒ rewrite (plusSn n m)
| [|- context[?n + S ?m]] ⇒ rewrite (plusnS n m)
| [|- context[?n + 0]] ⇒ rewrite (plusnO n)
| [|- context[0 + ?n]] ⇒ rewrite (plusOn n)
| [|- context[(+ ?m) ∘ (+ ?n)]] ⇒ rewrite (lift_comp m n)
| [|- context[(?f ∘ (+ ?m)) ∘ (+ ?n)]] ⇒ rewrite (lift_compR m n f)
end.
#[local] Notation "( + x )" := (lift x) (format "( + x )").
#[global] Arguments lift x y/.
Lemma lift0: (+0) = id. reflexivity. Qed.
Lemma lift_comp :∀ m n, (+m) ∘ (+n) = (+ (m + n)).
Proof.
intros. unfold compose, lift. ext y.
lia.
Qed.
Lemma lift_compR n m {X}(f: nat → X): (f ∘ (+m)) ∘ (+n) = f ∘ (+ (m + n)).
Proof.
now rewrite <- lift_comp.
Qed.
Lemma plusSn n m: S n + m = S (n + m). reflexivity. Qed.
Lemma plusnS n m: n + S m = S (n + m). symmetry. apply plus_n_Sm. Qed.
Lemma plusOn n: O + n = n. reflexivity. Qed.
Lemma plusnO n: n + O = n. symmetry. apply plus_n_O. Qed.
Ltac simplify_lift :=
progress repeat match goal with
| [|- context[(+0)]] ⇒ change (+0) with (@id nat)
| [|- context[?s S]] ⇒ change (s S) with (s (+1))
| [|- context[S ?n + ?m]] ⇒ rewrite (plusSn n m)
| [|- context[?n + S ?m]] ⇒ rewrite (plusnS n m)
| [|- context[?n + 0]] ⇒ rewrite (plusnO n)
| [|- context[0 + ?n]] ⇒ rewrite (plusOn n)
| [|- context[(+ ?m) ∘ (+ ?n)]] ⇒ rewrite (lift_comp m n)
| [|- context[(?f ∘ (+ ?m)) ∘ (+ ?n)]] ⇒ rewrite (lift_compR m n f)
end.
Definition scons {X: Type}: X → (nat → X) → (nat → X) :=
fun new sub n ⇒ match n with
| O ⇒ new
| S n' ⇒ sub n'
end.
#[local] Infix "⋅" := (scons) (at level 10).
fun new sub n ⇒ match n with
| O ⇒ new
| S n' ⇒ sub n'
end.
#[local] Infix "⋅" := (scons) (at level 10).
Lemma scons_rw0 {A}: ∀ `(x: A) (σ: nat → A),
(x ⋅ σ) 0 = x.
Proof.
reflexivity.
Qed.
Lemma scons_rw1 {A}: ∀ `(x: A) (n: nat) (σ: nat → A),
(x ⋅ σ) (S n) = σ n.
Proof.
reflexivity.
Qed.
Lemma scons_sub_id {X}: ∀ (σ: nat → X),
(σ 0) ⋅ (σ ∘ S) = σ.
Proof.
intros.
ext ix.
destruct ix.
- rewrite scons_rw0.
reflexivity.
- rewrite scons_rw1.
reflexivity.
Qed.
Lemma cons_compose {X Y}: ∀ (σ: nat → X) (f: X → Y) (x: X),
f ∘ (x ⋅ σ) = (f x) ⋅ (f ∘ σ).
Proof.
intros; now ext [|n].
Qed.
(x ⋅ σ) 0 = x.
Proof.
reflexivity.
Qed.
Lemma scons_rw1 {A}: ∀ `(x: A) (n: nat) (σ: nat → A),
(x ⋅ σ) (S n) = σ n.
Proof.
reflexivity.
Qed.
Lemma scons_sub_id {X}: ∀ (σ: nat → X),
(σ 0) ⋅ (σ ∘ S) = σ.
Proof.
intros.
ext ix.
destruct ix.
- rewrite scons_rw0.
reflexivity.
- rewrite scons_rw1.
reflexivity.
Qed.
Lemma cons_compose {X Y}: ∀ (σ: nat → X) (f: X → Y) (x: X),
f ∘ (x ⋅ σ) = (f x) ⋅ (f ∘ σ).
Proof.
intros; now ext [|n].
Qed.
Lemma cons_eta {X}: ∀ (σ: nat → X) (n: nat),
(σ n) ⋅ (σ ∘ (+ (S n))) = σ ∘ (+ n).
Proof.
intros.
unfold compose, lift.
ext [|m].
- cbn. simplify_lift. reflexivity.
- cbn. simplify_lift. reflexivity.
Qed.
Lemma lift_eta n: n ⋅ (+ (S n)) = (+ n).
Proof.
apply (cons_eta id).
Qed.
(σ n) ⋅ (σ ∘ (+ (S n))) = σ ∘ (+ n).
Proof.
intros.
unfold compose, lift.
ext [|m].
- cbn. simplify_lift. reflexivity.
- cbn. simplify_lift. reflexivity.
Qed.
Lemma lift_eta n: n ⋅ (+ (S n)) = (+ n).
Proof.
apply (cons_eta id).
Qed.
(* Given a depth and renaming ρ, adjust ρ to account for the
depth *)
Definition lift__ren: nat → (nat → nat) → (nat → nat) :=
fun depth ρ ix ⇒
if bound_b ix depth
then ix
else let free_ix := ix - depth
in ρ free_ix + depth.
Definition local__ren (ρ: nat → nat) (p: nat × nat): nat :=
match p with
| (depth, ix) ⇒ lift__ren depth ρ ix
end.
Definition rename `{Mapd_T_inst: Mapd nat T} (ρ: nat → nat): T nat → T nat :=
mapd (T := T) (local__ren ρ).
(* adjust a renaming to go under one binder *)
Definition up__ren (ρ: nat → nat): nat → nat :=
0 ⋅ (S ∘ ρ).
depth *)
Definition lift__ren: nat → (nat → nat) → (nat → nat) :=
fun depth ρ ix ⇒
if bound_b ix depth
then ix
else let free_ix := ix - depth
in ρ free_ix + depth.
Definition local__ren (ρ: nat → nat) (p: nat × nat): nat :=
match p with
| (depth, ix) ⇒ lift__ren depth ρ ix
end.
Definition rename `{Mapd_T_inst: Mapd nat T} (ρ: nat → nat): T nat → T nat :=
mapd (T := T) (local__ren ρ).
(* adjust a renaming to go under one binder *)
Definition up__ren (ρ: nat → nat): nat → nat :=
0 ⋅ (S ∘ ρ).
Section level_theory.
Context
`{Mapdt_T_inst: Mapdt nat T}
`{Functor_inst: ! DecoratedTraversableFunctor nat T}.
Lemma level1: ∀ (gap: nat) (t: T nat),
level t ≤ gap →
cl_at gap t.
Proof.
intros gap t.
unfold level.
unfold cl_at.
rewrite mapdReduce_through_toctxlist.
unfold Forall_ctx.
rewrite (mapdReduce_through_toctxlist _ (cl_at_loc gap)).
unfold compose.
induction (toctxlist t).
- cbv. easy.
- cbn.
do 2 unfold transparent tcs.
intros. split.
+ split; auto.
unfold cl_at_loc.
destruct a as (d, n).
unfold bound_within.
unfold level_loc in H.
lia.
+ apply IHe. lia.
Qed.
Lemma level2: ∀ (gap: nat) (t: T nat),
cl_at gap t →
level t ≤ gap.
Proof.
intros gap t.
unfold level.
unfold cl_at.
rewrite mapdReduce_through_toctxlist.
unfold Forall_ctx.
rewrite (mapdReduce_through_toctxlist _ (cl_at_loc gap)).
unfold compose.
induction (toctxlist t).
- cbv. lia.
- cbn.
do 2 unfold transparent tcs.
intros [[_ H1] H2].
unfold cl_at_loc in H1.
destruct a as (d, n).
unfold bound_within in H1.
specialize (IHe H2).
unfold level_loc at 1.
lia.
Qed.
Lemma level_iff: ∀ (gap: nat) (t: T nat),
cl_at gap t ↔ level t ≤ gap.
Proof.
intros. split.
- apply level2.
- apply level1.
Qed.
End level_theory.
Context
`{Mapdt_T_inst: Mapdt nat T}
`{Functor_inst: ! DecoratedTraversableFunctor nat T}.
Lemma level1: ∀ (gap: nat) (t: T nat),
level t ≤ gap →
cl_at gap t.
Proof.
intros gap t.
unfold level.
unfold cl_at.
rewrite mapdReduce_through_toctxlist.
unfold Forall_ctx.
rewrite (mapdReduce_through_toctxlist _ (cl_at_loc gap)).
unfold compose.
induction (toctxlist t).
- cbv. easy.
- cbn.
do 2 unfold transparent tcs.
intros. split.
+ split; auto.
unfold cl_at_loc.
destruct a as (d, n).
unfold bound_within.
unfold level_loc in H.
lia.
+ apply IHe. lia.
Qed.
Lemma level2: ∀ (gap: nat) (t: T nat),
cl_at gap t →
level t ≤ gap.
Proof.
intros gap t.
unfold level.
unfold cl_at.
rewrite mapdReduce_through_toctxlist.
unfold Forall_ctx.
rewrite (mapdReduce_through_toctxlist _ (cl_at_loc gap)).
unfold compose.
induction (toctxlist t).
- cbv. lia.
- cbn.
do 2 unfold transparent tcs.
intros [[_ H1] H2].
unfold cl_at_loc in H1.
destruct a as (d, n).
unfold bound_within in H1.
specialize (IHe H2).
unfold level_loc at 1.
lia.
Qed.
Lemma level_iff: ∀ (gap: nat) (t: T nat),
cl_at gap t ↔ level t ≤ gap.
Proof.
intros. split.
- apply level2.
- apply level1.
Qed.
End level_theory.
Section renaming_theory.
Context
`{Mapd_T_inst: Mapd nat T}
`{Functor_inst: ! DecoratedFunctor nat T}.
Context
`{Mapd_T_inst: Mapd nat T}
`{Functor_inst: ! DecoratedFunctor nat T}.
Lemma lift__ren_zero:
lift__ren 0 = id.
Proof.
unfold lift__ren.
ext ρ ix.
bound_induction.
replace (ix - 0) with ix by lia.
replace (ρ ix + 0) with (ρ ix) by lia.
reflexivity.
Qed.
Corollary local__ren_zero: ∀ ρ ix,
local__ren ρ (0, ix) = ρ ix.
Proof.
intros.
unfold local__ren.
rewrite lift__ren_zero.
reflexivity.
Qed.
Corollary rename_ret
`{Return T}
`{Bindd nat T T}
`{! Compat_Mapd_Bindd nat T T}
`{! DecoratedMonad nat T}: ∀ ρ ix,
rename ρ (ret ix) = ret (ρ ix).
Proof.
intros.
unfold rename.
compose near ix.
rewrite mapd_ret.
unfold compose.
unfold_ops @Return_Writer.
unfold_ops @Monoid_unit_zero.
rewrite local__ren_zero.
reflexivity.
Qed.
lift__ren 0 = id.
Proof.
unfold lift__ren.
ext ρ ix.
bound_induction.
replace (ix - 0) with ix by lia.
replace (ρ ix + 0) with (ρ ix) by lia.
reflexivity.
Qed.
Corollary local__ren_zero: ∀ ρ ix,
local__ren ρ (0, ix) = ρ ix.
Proof.
intros.
unfold local__ren.
rewrite lift__ren_zero.
reflexivity.
Qed.
Corollary rename_ret
`{Return T}
`{Bindd nat T T}
`{! Compat_Mapd_Bindd nat T T}
`{! DecoratedMonad nat T}: ∀ ρ ix,
rename ρ (ret ix) = ret (ρ ix).
Proof.
intros.
unfold rename.
compose near ix.
rewrite mapd_ret.
unfold compose.
unfold_ops @Return_Writer.
unfold_ops @Monoid_unit_zero.
rewrite local__ren_zero.
reflexivity.
Qed.
Lemma lift__ren_id: ∀ depth,
lift__ren depth id = id.
Proof.
unfold lift__ren.
intro depth. ext ix.
unfold id.
bound_induction.
Qed.
Corollary local__ren_id:
local__ren id = extract.
Proof.
ext [depth ix].
unfold local__ren.
rewrite lift__ren_id.
reflexivity.
Qed.
Lemma remame_id:
rename id = (@id (T nat)).
Proof.
unfold rename.
rewrite local__ren_id.
apply kdf_mapd1.
Qed.
lift__ren depth id = id.
Proof.
unfold lift__ren.
intro depth. ext ix.
unfold id.
bound_induction.
Qed.
Corollary local__ren_id:
local__ren id = extract.
Proof.
ext [depth ix].
unfold local__ren.
rewrite lift__ren_id.
reflexivity.
Qed.
Lemma remame_id:
rename id = (@id (T nat)).
Proof.
unfold rename.
rewrite local__ren_id.
apply kdf_mapd1.
Qed.
Lemma lift__ren_loc_compose1: ∀ depth ix ρ1 ρ2,
ix ≥ depth →
lift__ren depth ρ2 (ρ1 (ix - depth) + depth) =
ρ2 (ρ1 (ix - depth)) + depth.
Proof.
intros. unfold lift__ren.
bound_induction.
cbn. fequal. fequal. lia.
Qed.
Lemma lift__ren_loc_compose2: ∀ ρ depth ix,
ix < depth →
lift__ren depth ρ ix = ix.
Proof.
intros. unfold lift__ren.
bound_induction.
Qed.
Lemma lift__ren_loc_compose: ∀ depth ρ1 ρ2,
lift__ren depth ρ2 ∘ lift__ren depth ρ1 =
lift__ren depth (ρ2 ∘ ρ1).
Proof.
intros. ext ix.
unfold compose.
unfold lift__ren at 2 3.
bound_induction;
auto using lift__ren_loc_compose1, lift__ren_loc_compose2.
Qed.
Lemma rename_rename_loc: ∀ ρ2 ρ1,
local__ren ρ2 ⋆1 local__ren ρ1 = local__ren (ρ2 ∘ ρ1).
Proof.
intros.
ext [depth ix]. cbn.
compose near ix on left.
rewrite lift__ren_loc_compose.
reflexivity.
Qed.
Lemma rename_rename: ∀ ρ2 ρ1,
rename ρ2 ∘ rename ρ1 = rename (T := T) (ρ2 ∘ ρ1).
Proof.
intros.
unfold rename.
rewrite kdf_mapd2.
rewrite rename_rename_loc.
reflexivity.
Qed.
ix ≥ depth →
lift__ren depth ρ2 (ρ1 (ix - depth) + depth) =
ρ2 (ρ1 (ix - depth)) + depth.
Proof.
intros. unfold lift__ren.
bound_induction.
cbn. fequal. fequal. lia.
Qed.
Lemma lift__ren_loc_compose2: ∀ ρ depth ix,
ix < depth →
lift__ren depth ρ ix = ix.
Proof.
intros. unfold lift__ren.
bound_induction.
Qed.
Lemma lift__ren_loc_compose: ∀ depth ρ1 ρ2,
lift__ren depth ρ2 ∘ lift__ren depth ρ1 =
lift__ren depth (ρ2 ∘ ρ1).
Proof.
intros. ext ix.
unfold compose.
unfold lift__ren at 2 3.
bound_induction;
auto using lift__ren_loc_compose1, lift__ren_loc_compose2.
Qed.
Lemma rename_rename_loc: ∀ ρ2 ρ1,
local__ren ρ2 ⋆1 local__ren ρ1 = local__ren (ρ2 ∘ ρ1).
Proof.
intros.
ext [depth ix]. cbn.
compose near ix on left.
rewrite lift__ren_loc_compose.
reflexivity.
Qed.
Lemma rename_rename: ∀ ρ2 ρ1,
rename ρ2 ∘ rename ρ1 = rename (T := T) (ρ2 ∘ ρ1).
Proof.
intros.
unfold rename.
rewrite kdf_mapd2.
rewrite rename_rename_loc.
reflexivity.
Qed.
Lemma lift__ren_compose: ∀ (n m: nat),
lift__ren m ∘ lift__ren n = lift__ren (m + n).
Proof.
intros. ext σ ix.
unfold compose, lift__ren.
bound_induction.
- bound_induction.
+ bound_induction.
rewrite (Nat.add_comm m n).
rewrite Nat.add_assoc.
fequal. fequal. fequal. lia.
+ bound_induction.
- bound_induction.
Qed.
Corollary lift__ren_S: ∀ (n: nat) ρ,
lift__ren (S n) ρ = lift__ren n (lift__ren 1 ρ).
Proof.
intros.
replace (S n) with (n + 1) by lia.
compose near ρ on right.
now rewrite lift__ren_compose.
Qed.
Lemma lift__ren_iter: ∀ n,
lift__ren n = iterate n (lift__ren 1).
Proof.
intros.
induction n.
- rewrite lift__ren_zero.
reflexivity.
- ext ρ.
rewrite lift__ren_S.
rewrite IHn.
rewrite iterate_rw1.
reflexivity.
Qed.
Lemma local__ren_preincr (ρ: nat → nat) (n: nat):
(local__ren ρ) ⦿ n =
local__ren (lift__ren n ρ).
Proof.
ext (depth, ix); cbn.
change (?n ● ?m) with (n + m).
compose near ρ.
rewrite (lift__ren_compose).
fequal; lia.
Qed.
lift__ren m ∘ lift__ren n = lift__ren (m + n).
Proof.
intros. ext σ ix.
unfold compose, lift__ren.
bound_induction.
- bound_induction.
+ bound_induction.
rewrite (Nat.add_comm m n).
rewrite Nat.add_assoc.
fequal. fequal. fequal. lia.
+ bound_induction.
- bound_induction.
Qed.
Corollary lift__ren_S: ∀ (n: nat) ρ,
lift__ren (S n) ρ = lift__ren n (lift__ren 1 ρ).
Proof.
intros.
replace (S n) with (n + 1) by lia.
compose near ρ on right.
now rewrite lift__ren_compose.
Qed.
Lemma lift__ren_iter: ∀ n,
lift__ren n = iterate n (lift__ren 1).
Proof.
intros.
induction n.
- rewrite lift__ren_zero.
reflexivity.
- ext ρ.
rewrite lift__ren_S.
rewrite IHn.
rewrite iterate_rw1.
reflexivity.
Qed.
Lemma local__ren_preincr (ρ: nat → nat) (n: nat):
(local__ren ρ) ⦿ n =
local__ren (lift__ren n ρ).
Proof.
ext (depth, ix); cbn.
change (?n ● ?m) with (n + m).
compose near ρ.
rewrite (lift__ren_compose).
fequal; lia.
Qed.
Lemma lift__ren_1:
lift__ren 1 = up__ren.
Proof.
ext ρ ix.
unfold lift__ren, up__ren.
bound_induction.
- cbn. destruct ix.
+ exfalso. lia.
+ cbn. unfold compose.
rewrite Nat.add_1_r.
do 2 fequal. lia.
- apply bound_1 in Hbound.
subst. reflexivity.
Qed.
Lemma lift__ren_repr: ∀ depth,
lift__ren depth = iterate depth up__ren.
Proof.
intros.
induction depth.
- rewrite lift__ren_zero.
rewrite iterate_rw0.
reflexivity.
- ext ρ.
rewrite lift__ren_S.
rewrite iterate_rw1.
rewrite IHdepth.
rewrite lift__ren_1.
reflexivity.
Qed.
Corollary local__ren_repr: ∀ ρ depth ix,
local__ren ρ (depth, ix) = iterate depth up__ren ρ ix.
Proof.
intros. cbn.
rewrite lift__ren_repr.
reflexivity.
Qed.
lift__ren 1 = up__ren.
Proof.
ext ρ ix.
unfold lift__ren, up__ren.
bound_induction.
- cbn. destruct ix.
+ exfalso. lia.
+ cbn. unfold compose.
rewrite Nat.add_1_r.
do 2 fequal. lia.
- apply bound_1 in Hbound.
subst. reflexivity.
Qed.
Lemma lift__ren_repr: ∀ depth,
lift__ren depth = iterate depth up__ren.
Proof.
intros.
induction depth.
- rewrite lift__ren_zero.
rewrite iterate_rw0.
reflexivity.
- ext ρ.
rewrite lift__ren_S.
rewrite iterate_rw1.
rewrite IHdepth.
rewrite lift__ren_1.
reflexivity.
Qed.
Corollary local__ren_repr: ∀ ρ depth ix,
local__ren ρ (depth, ix) = iterate depth up__ren ρ ix.
Proof.
intros. cbn.
rewrite lift__ren_repr.
reflexivity.
Qed.
Definition map_with_policy `{Mapd nat T}
(policy: (nat → nat) → (nat → nat)) (ρ: nat → nat): T nat → T nat :=
mapd (fun '(depth, ix) ⇒ iterate depth policy ρ ix).
Lemma rename_policy_repr (ρ: nat → nat):
rename (T := T) ρ = map_with_policy up__ren ρ.
Proof.
unfold rename, map_with_policy.
fequal. ext [depth ix].
apply local__ren_repr.
Qed.
Lemma local__ren_preincr_1 (ρ: nat → nat):
(local__ren ρ) ⦿ 1 =
local__ren (up__ren ρ).
Proof.
rewrite local__ren_preincr.
rewrite lift__ren_1.
reflexivity.
Qed.
(policy: (nat → nat) → (nat → nat)) (ρ: nat → nat): T nat → T nat :=
mapd (fun '(depth, ix) ⇒ iterate depth policy ρ ix).
Lemma rename_policy_repr (ρ: nat → nat):
rename (T := T) ρ = map_with_policy up__ren ρ.
Proof.
unfold rename, map_with_policy.
fequal. ext [depth ix].
apply local__ren_repr.
Qed.
Lemma local__ren_preincr_1 (ρ: nat → nat):
(local__ren ρ) ⦿ 1 =
local__ren (up__ren ρ).
Proof.
rewrite local__ren_preincr.
rewrite lift__ren_1.
reflexivity.
Qed.
Context
`{Mapdt_inst: Mapdt nat T}
`{! Compat_Mapd_Mapdt nat T}
`{DTF_inst: ! DecoratedTraversableFunctor nat T}.
Lemma ind_rename_iff: ∀ l n (t:T nat) ρ,
(n, l) ∈d rename ρ t ↔ ∃ l1,
(n, l1) ∈d t ∧
l = (if l1 `bound in` n then l1
else n + ρ (l1 - n)).
Proof.
intros.
unfold rename in ×.
rewrite ind_mapd_iff.
unfold local__ren, lift__ren.
setoid_rewrite Nat.add_comm at 1.
intuition; preprocess; eauto.
Qed.
End renaming_theory.
Section ops.
Context
`{ret_inst: Return T}
`{Mapd_T_inst: Mapd nat T}
`{Bindd_U_inst: Bindd nat T U}.
(* Given a depth and substitution σ, adjust σ to account for the
depth *)
Definition lift__sub: nat → (nat → T nat) → (nat → T nat) :=
fun depth σ ix ⇒
if ix `bound in` depth
then ret ix
else let free_ix := ix - depth
in rename (+ depth) (σ free_ix).
Definition local__sub (σ: nat → T nat) (p: nat × nat): T nat :=
match p with
| (depth, ix) ⇒ lift__sub depth σ ix
end.
Definition subst (σ: nat → T nat): U nat → U nat :=
bindd (local__sub σ).
(* adjust a substitution to go under one binder *)
Definition up__sub (σ: nat → T nat): nat → T nat :=
(ret 0) ⋅ (rename (+1) ∘ σ).
End ops.
Section theory.
Context
`{ret_inst: Return T}
`{Map_T_inst: Map T}
`{Mapd_T_inst: Mapd nat T}
`{Traverse_T_inst: Traverse T}
`{Bind_T_inst: Bind T T}
`{Mapdt_T_inst: Mapdt nat T}
`{Bindd_T_inst: Bindd nat T T}
`{Bindt_T_inst: Bindt T T}
`{Binddt_T_inst: Binddt nat T T}
`{! Compat_Map_Binddt nat T T}
`{! Compat_Mapd_Binddt nat T T}
`{! Compat_Traverse_Binddt nat T T}
`{! Compat_Bind_Binddt nat T T}
`{! Compat_Mapdt_Binddt nat T T}
`{! Compat_Bindd_Binddt nat T T}
`{! Compat_Bindt_Binddt nat T T}
`{Monad_inst: ! DecoratedTraversableMonad nat T}.
Context
`{Map_U_inst: Map U}
`{Mapd_U_inst: Mapd nat U}
`{Traverse_U_inst: Traverse U}
`{Bind_U_inst: Bind T U}
`{Mapdt_U_inst: Mapdt nat U}
`{Bindd_U_inst: Bindd nat T U}
`{Bindt_U_inst: Bindt T U}
`{Binddt_U_inst: Binddt nat T U}
`{! Compat_Map_Binddt nat T U}
`{! Compat_Mapd_Binddt nat T U}
`{! Compat_Traverse_Binddt nat T U}
`{! Compat_Bind_Binddt nat T U}
`{! Compat_Mapdt_Binddt nat T U}
`{! Compat_Bindd_Binddt nat T U}
`{! Compat_Bindt_Binddt nat T U}
`{Module_inst: ! DecoratedTraversableRightPreModule nat T U
(unit := Monoid_unit_zero)
(op := Monoid_op_plus)}.
Context
`{ret_inst: Return T}
`{Mapd_T_inst: Mapd nat T}
`{Bindd_U_inst: Bindd nat T U}.
(* Given a depth and substitution σ, adjust σ to account for the
depth *)
Definition lift__sub: nat → (nat → T nat) → (nat → T nat) :=
fun depth σ ix ⇒
if ix `bound in` depth
then ret ix
else let free_ix := ix - depth
in rename (+ depth) (σ free_ix).
Definition local__sub (σ: nat → T nat) (p: nat × nat): T nat :=
match p with
| (depth, ix) ⇒ lift__sub depth σ ix
end.
Definition subst (σ: nat → T nat): U nat → U nat :=
bindd (local__sub σ).
(* adjust a substitution to go under one binder *)
Definition up__sub (σ: nat → T nat): nat → T nat :=
(ret 0) ⋅ (rename (+1) ∘ σ).
End ops.
Section theory.
Context
`{ret_inst: Return T}
`{Map_T_inst: Map T}
`{Mapd_T_inst: Mapd nat T}
`{Traverse_T_inst: Traverse T}
`{Bind_T_inst: Bind T T}
`{Mapdt_T_inst: Mapdt nat T}
`{Bindd_T_inst: Bindd nat T T}
`{Bindt_T_inst: Bindt T T}
`{Binddt_T_inst: Binddt nat T T}
`{! Compat_Map_Binddt nat T T}
`{! Compat_Mapd_Binddt nat T T}
`{! Compat_Traverse_Binddt nat T T}
`{! Compat_Bind_Binddt nat T T}
`{! Compat_Mapdt_Binddt nat T T}
`{! Compat_Bindd_Binddt nat T T}
`{! Compat_Bindt_Binddt nat T T}
`{Monad_inst: ! DecoratedTraversableMonad nat T}.
Context
`{Map_U_inst: Map U}
`{Mapd_U_inst: Mapd nat U}
`{Traverse_U_inst: Traverse U}
`{Bind_U_inst: Bind T U}
`{Mapdt_U_inst: Mapdt nat U}
`{Bindd_U_inst: Bindd nat T U}
`{Bindt_U_inst: Bindt T U}
`{Binddt_U_inst: Binddt nat T U}
`{! Compat_Map_Binddt nat T U}
`{! Compat_Mapd_Binddt nat T U}
`{! Compat_Traverse_Binddt nat T U}
`{! Compat_Bind_Binddt nat T U}
`{! Compat_Mapdt_Binddt nat T U}
`{! Compat_Bindd_Binddt nat T U}
`{! Compat_Bindt_Binddt nat T U}
`{Module_inst: ! DecoratedTraversableRightPreModule nat T U
(unit := Monoid_unit_zero)
(op := Monoid_op_plus)}.
Lemma lift__sub_zero:
lift__sub 0 = id.
Proof.
ext σ ix. unfold id.
unfold lift__sub.
cbn.
replace (ix - 0) with ix by lia.
replace (+ 0) with (@id nat).
2:{ ext n. unfold lift, id. lia. }
unfold rename.
rewrite local__ren_id.
rewrite mapd_id.
reflexivity.
Qed.
Lemma local__sub_zero: ∀ σ n,
local__sub σ (0, n) = σ n.
Proof.
intros. unfold local__sub.
rewrite lift__sub_zero.
reflexivity.
Qed.
Lemma local__sub_compose_ret: ∀ σ x,
(local__sub σ ∘ ret) x = σ x.
Proof.
intros.
unfold_ops @Return_Writer @Monoid_unit_zero.
unfold compose.
rewrite local__sub_zero.
reflexivity.
Qed.
Lemma subst_ret: ∀ σ x,
subst σ (ret x) = σ x.
Proof.
intros.
unfold subst.
compose near x on left.
rewrite bindd_ret.
apply local__sub_compose_ret.
Qed.
Lemma subst_compose_ret: ∀ σ,
subst σ ∘ ret = σ.
Proof.
intros. ext x.
unfold compose. apply subst_ret.
Qed.
lift__sub 0 = id.
Proof.
ext σ ix. unfold id.
unfold lift__sub.
cbn.
replace (ix - 0) with ix by lia.
replace (+ 0) with (@id nat).
2:{ ext n. unfold lift, id. lia. }
unfold rename.
rewrite local__ren_id.
rewrite mapd_id.
reflexivity.
Qed.
Lemma local__sub_zero: ∀ σ n,
local__sub σ (0, n) = σ n.
Proof.
intros. unfold local__sub.
rewrite lift__sub_zero.
reflexivity.
Qed.
Lemma local__sub_compose_ret: ∀ σ x,
(local__sub σ ∘ ret) x = σ x.
Proof.
intros.
unfold_ops @Return_Writer @Monoid_unit_zero.
unfold compose.
rewrite local__sub_zero.
reflexivity.
Qed.
Lemma subst_ret: ∀ σ x,
subst σ (ret x) = σ x.
Proof.
intros.
unfold subst.
compose near x on left.
rewrite bindd_ret.
apply local__sub_compose_ret.
Qed.
Lemma subst_compose_ret: ∀ σ,
subst σ ∘ ret = σ.
Proof.
intros. ext x.
unfold compose. apply subst_ret.
Qed.
Lemma lift__sub_id: ∀ depth ix,
lift__sub depth ret ix = (ret ∘ extract) (depth, ix).
Proof.
intros.
unfold lift__sub.
bound_induction.
rewrite rename_ret.
unfold compose. cbn.
fequal. lia.
Qed.
Corollary local__subst_id:
local__sub (T := T) (@ret T _ nat) = ret ∘ extract.
Proof.
unfold local__sub. ext [depth ix].
apply lift__sub_id.
Qed.
Lemma subst_id:
subst (@ret T _ nat) = id.
Proof.
unfold subst.
rewrite local__subst_id.
apply bindd_id.
Qed.
lift__sub depth ret ix = (ret ∘ extract) (depth, ix).
Proof.
intros.
unfold lift__sub.
bound_induction.
rewrite rename_ret.
unfold compose. cbn.
fequal. lia.
Qed.
Corollary local__subst_id:
local__sub (T := T) (@ret T _ nat) = ret ∘ extract.
Proof.
unfold local__sub. ext [depth ix].
apply lift__sub_id.
Qed.
Lemma subst_id:
subst (@ret T _ nat) = id.
Proof.
unfold subst.
rewrite local__subst_id.
apply bindd_id.
Qed.
Lemma lift__sub_compose: ∀ (n m: nat),
lift__sub m ∘ lift__sub n =
lift__sub (m + n).
Proof.
intros. ext σ ix.
unfold compose, lift__sub.
bound_induction.
- bound_induction.
+ bound_induction.
compose near (σ (ix - m - n)) on left.
rewrite rename_rename.
rewrite lift_comp.
fequal. fequal.
lia.
+ bound_induction.
compose near (ix - m).
unfold rename.
rewrite mapd_ret.
unfold compose; cbn.
fequal.
unfold_ops @Monoid_unit_zero.
lia.
- bound_induction.
Qed.
Corollary lift__sub_S: ∀ (n: nat) σ,
lift__sub (S n) σ =
lift__sub n (lift__sub 1 σ).
Proof.
intros.
replace (S n) with (n + 1) by lia.
compose near σ on right.
now rewrite lift__sub_compose.
Qed.
Lemma lift__sub_iter: ∀ n,
lift__sub n = iterate n (lift__sub 1).
Proof.
intros. induction n.
- rewrite lift__sub_zero.
reflexivity.
- ext σ.
rewrite lift__sub_S.
rewrite iterate_rw1A.
rewrite IHn.
reflexivity.
Qed.
Lemma local__sub_preincr (σ: nat → T nat) (n: nat):
(local__sub σ) ⦿ n =
local__sub (lift__sub n σ).
Proof.
unfold local__sub.
ext (depth, ix); cbn.
compose near σ on right.
rewrite (lift__sub_compose).
change (?n ● ?m) with (n + m).
fequal. lia.
Qed.
lift__sub m ∘ lift__sub n =
lift__sub (m + n).
Proof.
intros. ext σ ix.
unfold compose, lift__sub.
bound_induction.
- bound_induction.
+ bound_induction.
compose near (σ (ix - m - n)) on left.
rewrite rename_rename.
rewrite lift_comp.
fequal. fequal.
lia.
+ bound_induction.
compose near (ix - m).
unfold rename.
rewrite mapd_ret.
unfold compose; cbn.
fequal.
unfold_ops @Monoid_unit_zero.
lia.
- bound_induction.
Qed.
Corollary lift__sub_S: ∀ (n: nat) σ,
lift__sub (S n) σ =
lift__sub n (lift__sub 1 σ).
Proof.
intros.
replace (S n) with (n + 1) by lia.
compose near σ on right.
now rewrite lift__sub_compose.
Qed.
Lemma lift__sub_iter: ∀ n,
lift__sub n = iterate n (lift__sub 1).
Proof.
intros. induction n.
- rewrite lift__sub_zero.
reflexivity.
- ext σ.
rewrite lift__sub_S.
rewrite iterate_rw1A.
rewrite IHn.
reflexivity.
Qed.
Lemma local__sub_preincr (σ: nat → T nat) (n: nat):
(local__sub σ) ⦿ n =
local__sub (lift__sub n σ).
Proof.
unfold local__sub.
ext (depth, ix); cbn.
compose near σ on right.
rewrite (lift__sub_compose).
change (?n ● ?m) with (n + m).
fequal. lia.
Qed.
Lemma subst_subst_loc: ∀ (σ2 σ1: nat → T nat),
local__sub (T := T) σ2 ⋆5 local__sub (T := T) σ1 =
local__sub (T := T) (subst σ2 ∘ σ1).
Proof.
intros.
unfold kc5.
ext [depth ix].
unfold local__sub at 2 3.
unfold lift__sub.
bound_induction.
2:{ compose near ix on left.
rewrite bindd_ret.
unfold compose.
unfold_ops @Return_Writer.
unfold local__sub. cbn.
rewrite monoid_id_r.
unfold lift__sub.
rewrite Hbound. reflexivity. }
{ unfold compose at 1.
unfold rename.
rewrite local__sub_preincr.
compose near (σ1 (ix - depth)) on left.
compose near (σ1 (ix - depth)) on right.
rewrite bindd_mapd.
unfold subst.
rewrite mapd_bindd.
fequal.
ext [depth' ix'].
{ rewrite local__ren_preincr.
cbn. unfold lift__ren at 1.
unfold lift__sub at 3.
bound_induction.
- unfold lift at 1.
replace (depth + (ix' - depth') + depth') with (ix' + depth) by lia.
unfold rename.
compose near (σ2 (ix' - depth')).
rewrite kdf_mapd2.
rewrite rename_rename_loc.
unfold lift__sub.
bound_induction.
bound_induction.
replace (ix' + depth - depth' - depth) with (ix' - depth') by lia.
compose near (σ2 (ix' - depth')) on left.
rewrite rename_rename.
unfold rename. fequal.
unfold compose.
fequal.
ext m. unfold lift__ren.
unfold lift.
bound_induction.
- compose near ix' on right.
rewrite mapd_ret.
compose near σ2 on left.
rewrite lift__sub_compose.
unfold compose. unfold transparent tcs.
cbn.
unfold lift__sub.
bound_induction.
fequal.
unfold lift__ren.
replace (ix' - 0) with ix' by lia. bound_induction.
}
}
Qed.
Lemma subst_subst: ∀ (σ2 σ1: nat → T nat),
subst σ2 ∘ subst σ1 = subst (T := T) (subst σ2 ∘ σ1).
Proof.
intros.
unfold subst.
rewrite bindd_bindd.
rewrite subst_subst_loc.
reflexivity.
Qed.
local__sub (T := T) σ2 ⋆5 local__sub (T := T) σ1 =
local__sub (T := T) (subst σ2 ∘ σ1).
Proof.
intros.
unfold kc5.
ext [depth ix].
unfold local__sub at 2 3.
unfold lift__sub.
bound_induction.
2:{ compose near ix on left.
rewrite bindd_ret.
unfold compose.
unfold_ops @Return_Writer.
unfold local__sub. cbn.
rewrite monoid_id_r.
unfold lift__sub.
rewrite Hbound. reflexivity. }
{ unfold compose at 1.
unfold rename.
rewrite local__sub_preincr.
compose near (σ1 (ix - depth)) on left.
compose near (σ1 (ix - depth)) on right.
rewrite bindd_mapd.
unfold subst.
rewrite mapd_bindd.
fequal.
ext [depth' ix'].
{ rewrite local__ren_preincr.
cbn. unfold lift__ren at 1.
unfold lift__sub at 3.
bound_induction.
- unfold lift at 1.
replace (depth + (ix' - depth') + depth') with (ix' + depth) by lia.
unfold rename.
compose near (σ2 (ix' - depth')).
rewrite kdf_mapd2.
rewrite rename_rename_loc.
unfold lift__sub.
bound_induction.
bound_induction.
replace (ix' + depth - depth' - depth) with (ix' - depth') by lia.
compose near (σ2 (ix' - depth')) on left.
rewrite rename_rename.
unfold rename. fequal.
unfold compose.
fequal.
ext m. unfold lift__ren.
unfold lift.
bound_induction.
- compose near ix' on right.
rewrite mapd_ret.
compose near σ2 on left.
rewrite lift__sub_compose.
unfold compose. unfold transparent tcs.
cbn.
unfold lift__sub.
bound_induction.
fequal.
unfold lift__ren.
replace (ix' - 0) with ix' by lia. bound_induction.
}
}
Qed.
Lemma subst_subst: ∀ (σ2 σ1: nat → T nat),
subst σ2 ∘ subst σ1 = subst (T := T) (subst σ2 ∘ σ1).
Proof.
intros.
unfold subst.
rewrite bindd_bindd.
rewrite subst_subst_loc.
reflexivity.
Qed.
Lemma lift__ren_to_sub: ∀ n ρ,
ret ∘ lift__ren n ρ = lift__sub n (ret ∘ ρ).
Proof.
intros. ext m.
unfold compose; cbn.
unfold lift__sub, lift__ren.
unfold lift.
bound_induction.
rewrite rename_ret.
fequal. lia.
Qed.
Lemma rename_to_subst_loc: ∀ ρ,
ret ∘ local__ren ρ = local__sub (T := T) (ret ∘ ρ).
Proof.
intros. ext [depth ix].
unfold compose. cbn.
compose near ix on left.
rewrite lift__ren_to_sub.
reflexivity.
Qed.
Lemma rename_to_subst: ∀ ρ,
rename ρ = subst (U := T) (ret ∘ ρ).
Proof.
intros.
unfold rename, subst.
rewrite mapd_to_bindd.
fequal.
(* Fails with a universe error for some reason
now rewrite (rename_to_subst_loc ρ).
*)
intros. ext [depth ix]. unfold compose.
cbn. unfold lift__ren, lift__sub.
unfold lift.
bound_induction.
rewrite rename_ret.
fequal; lia.
Qed.
ret ∘ lift__ren n ρ = lift__sub n (ret ∘ ρ).
Proof.
intros. ext m.
unfold compose; cbn.
unfold lift__sub, lift__ren.
unfold lift.
bound_induction.
rewrite rename_ret.
fequal. lia.
Qed.
Lemma rename_to_subst_loc: ∀ ρ,
ret ∘ local__ren ρ = local__sub (T := T) (ret ∘ ρ).
Proof.
intros. ext [depth ix].
unfold compose. cbn.
compose near ix on left.
rewrite lift__ren_to_sub.
reflexivity.
Qed.
Lemma rename_to_subst: ∀ ρ,
rename ρ = subst (U := T) (ret ∘ ρ).
Proof.
intros.
unfold rename, subst.
rewrite mapd_to_bindd.
fequal.
(* Fails with a universe error for some reason
now rewrite (rename_to_subst_loc ρ).
*)
intros. ext [depth ix]. unfold compose.
cbn. unfold lift__ren, lift__sub.
unfold lift.
bound_induction.
rewrite rename_ret.
fequal; lia.
Qed.
Lemma up__sub_unfold (σ: nat → T nat):
up__sub σ = ret 0 ⋅ (subst (ret ∘ (+1)) ∘ σ).
Proof.
unfold up__sub.
rewrite rename_to_subst.
reflexivity.
Qed.
Lemma up_spec:
lift__sub 1 = up__sub.
Proof.
ext σ ix.
unfold up__sub, lift__sub.
bound_induction.
- destruct ix.
+ exfalso. lia.
+ replace (S ix - 1) with ix by lia.
reflexivity.
- apply bound_1 in Hbound.
now subst.
Qed.
Lemma local__sub_policy_repr: ∀ depth ix σ,
local__sub σ (depth, ix) = iterate depth up__sub σ ix.
Proof.
intros.
unfold local__sub.
rewrite lift__sub_iter.
fequal.
apply up_spec.
Qed.
Lemma local__sub_preincr_1 (σ: nat → T nat):
(local__sub σ) ⦿ 1 =
local__sub (up__sub σ).
Proof.
rewrite local__sub_preincr.
rewrite up_spec.
reflexivity.
Qed.
Definition bind_with_policy `{Bindd nat T U}
(policy: (nat → T nat) → (nat → T nat)) (σ: nat → T nat): U nat → U nat :=
bindd (fun '(depth, ix) ⇒ iterate depth policy σ ix).
Lemma subst_policy_repr (σ: nat → T nat):
subst σ = bind_with_policy up__sub σ.
Proof.
unfold subst, bind_with_policy.
fequal.
ext [depth ix].
rewrite local__sub_policy_repr.
reflexivity.
Qed.
Lemma iterate_up__sub_unfold (σ: nat → T nat) (n: nat):
iterate (S n) up__sub σ = ret 0 ⋅ (subst (ret ∘ (+1)) ∘ iterate n up__sub σ).
Proof.
rewrite iterate_rw2A.
rewrite up__sub_unfold.
reflexivity.
Qed.
up__sub σ = ret 0 ⋅ (subst (ret ∘ (+1)) ∘ σ).
Proof.
unfold up__sub.
rewrite rename_to_subst.
reflexivity.
Qed.
Lemma up_spec:
lift__sub 1 = up__sub.
Proof.
ext σ ix.
unfold up__sub, lift__sub.
bound_induction.
- destruct ix.
+ exfalso. lia.
+ replace (S ix - 1) with ix by lia.
reflexivity.
- apply bound_1 in Hbound.
now subst.
Qed.
Lemma local__sub_policy_repr: ∀ depth ix σ,
local__sub σ (depth, ix) = iterate depth up__sub σ ix.
Proof.
intros.
unfold local__sub.
rewrite lift__sub_iter.
fequal.
apply up_spec.
Qed.
Lemma local__sub_preincr_1 (σ: nat → T nat):
(local__sub σ) ⦿ 1 =
local__sub (up__sub σ).
Proof.
rewrite local__sub_preincr.
rewrite up_spec.
reflexivity.
Qed.
Definition bind_with_policy `{Bindd nat T U}
(policy: (nat → T nat) → (nat → T nat)) (σ: nat → T nat): U nat → U nat :=
bindd (fun '(depth, ix) ⇒ iterate depth policy σ ix).
Lemma subst_policy_repr (σ: nat → T nat):
subst σ = bind_with_policy up__sub σ.
Proof.
unfold subst, bind_with_policy.
fequal.
ext [depth ix].
rewrite local__sub_policy_repr.
reflexivity.
Qed.
Lemma iterate_up__sub_unfold (σ: nat → T nat) (n: nat):
iterate (S n) up__sub σ = ret 0 ⋅ (subst (ret ∘ (+1)) ∘ iterate n up__sub σ).
Proof.
rewrite iterate_rw2A.
rewrite up__sub_unfold.
reflexivity.
Qed.
Lemma ind_local_sub1: ∀ (σ: nat → T nat) n1 ix1,
ix1 `bound in` n1 = true →
(0, ix1) ∈d local__sub σ (n1, ix1).
Proof.
introv H.
unfold local__sub, lift__sub.
bound_induction_in H.
rewrite ind_ret_iff.
auto.
Qed.
Lemma ind_local_sub_iff: ∀ (σ: nat → T nat) n2 ix2 n1 ix1,
(n2, ix2) ∈d local__sub σ (n1, ix1) →
(ix1 ≥ n1 ∧
∃ l1: nat,
(n2, l1) ∈d σ (ix1 - n1) ∧
ix2 = (if l1 `bound in` n2 then l1 else n2 + (+n1) (l1 - n2)))
∨ (ix1 < n1 ∧ n2 = 0 ∧ ix2 = ix1).
Proof.
intros.
unfold local__sub, lift__sub in H.
bound_induction_in H.
{ rewrite ind_rename_iff in H.
tauto. }
{ right. rewrite ind_ret_iff in H.
inversion H; subst. intuition.
}
Qed.
Lemma ind_subst_iff: ∀ l n (t:U nat) σ,
(n, l) ∈d subst σ t ↔ ∃ n1 n2 l1,
(n1, l1) ∈d t ∧ (n2, l) ∈d local__sub σ (n1, l1) ∧ n = n1 + n2.
Proof.
intros. unfold subst in ×.
now rewrite ind_bindd_iff'.
Qed.
Lemma ind_subst_iff2: ∀ l n (t:U nat) σ,
(n, l) ∈d subst σ t ↔
((n, l) ∈d t ∧ (l `bound in` n = true))
∨ ∃ n1 n2 l1,
(n1, l1) ∈d t ∧
(n2, l) ∈d local__sub σ (n1, l1) ∧ n = n1 + n2.
Proof.
intros. unfold subst in ×.
rewrite ind_bindd_iff'.
split.
- intros.
destruct H as [n1 [n2 [a [H1 [H2 H3]]]]].
assert (H2copy: (n2, l) ∈d local__sub σ (n1, a)) by apply H2.
unfold local__sub, lift__sub in H2.
bound_induction_in H2.
+ right.
∃ n1. ∃ n2. ∃ a. auto.
+ rewrite ind_ret_iff in H2.
inversion H2; subst.
simpl_monoid. now left.
- intros. destruct H.
+ ∃ n. ∃ 0. ∃ l. split.
{ tauto. }
split.
{ unfold local__sub, lift__sub.
bound_induction. now rewrite ind_ret_iff. }
{ easy. }
+ assumption.
Qed.
End theory.
ix1 `bound in` n1 = true →
(0, ix1) ∈d local__sub σ (n1, ix1).
Proof.
introv H.
unfold local__sub, lift__sub.
bound_induction_in H.
rewrite ind_ret_iff.
auto.
Qed.
Lemma ind_local_sub_iff: ∀ (σ: nat → T nat) n2 ix2 n1 ix1,
(n2, ix2) ∈d local__sub σ (n1, ix1) →
(ix1 ≥ n1 ∧
∃ l1: nat,
(n2, l1) ∈d σ (ix1 - n1) ∧
ix2 = (if l1 `bound in` n2 then l1 else n2 + (+n1) (l1 - n2)))
∨ (ix1 < n1 ∧ n2 = 0 ∧ ix2 = ix1).
Proof.
intros.
unfold local__sub, lift__sub in H.
bound_induction_in H.
{ rewrite ind_rename_iff in H.
tauto. }
{ right. rewrite ind_ret_iff in H.
inversion H; subst. intuition.
}
Qed.
Lemma ind_subst_iff: ∀ l n (t:U nat) σ,
(n, l) ∈d subst σ t ↔ ∃ n1 n2 l1,
(n1, l1) ∈d t ∧ (n2, l) ∈d local__sub σ (n1, l1) ∧ n = n1 + n2.
Proof.
intros. unfold subst in ×.
now rewrite ind_bindd_iff'.
Qed.
Lemma ind_subst_iff2: ∀ l n (t:U nat) σ,
(n, l) ∈d subst σ t ↔
((n, l) ∈d t ∧ (l `bound in` n = true))
∨ ∃ n1 n2 l1,
(n1, l1) ∈d t ∧
(n2, l) ∈d local__sub σ (n1, l1) ∧ n = n1 + n2.
Proof.
intros. unfold subst in ×.
rewrite ind_bindd_iff'.
split.
- intros.
destruct H as [n1 [n2 [a [H1 [H2 H3]]]]].
assert (H2copy: (n2, l) ∈d local__sub σ (n1, a)) by apply H2.
unfold local__sub, lift__sub in H2.
bound_induction_in H2.
+ right.
∃ n1. ∃ n2. ∃ a. auto.
+ rewrite ind_ret_iff in H2.
inversion H2; subst.
simpl_monoid. now left.
- intros. destruct H.
+ ∃ n. ∃ 0. ∃ l. split.
{ tauto. }
split.
{ unfold local__sub, lift__sub.
bound_induction. now rewrite ind_ret_iff. }
{ easy. }
+ assumption.
Qed.
End theory.
Module Notations.
Notation "↑" := S.
Notation "'⇑'" := up__sub.
Notation "'⇑__ren'" := up__ren.
Notation "f ';' g" := (kc1 g f) (at level 30).
Infix "⋅" := (scons) (at level 10).
Notation "( + x )" := (lift x) (format "( + x )").
End Notations.
Import Notations.
Notation "↑" := S.
Notation "'⇑'" := up__sub.
Notation "'⇑__ren'" := up__ren.
Notation "f ';' g" := (kc1 g f) (at level 30).
Infix "⋅" := (scons) (at level 10).
Notation "( + x )" := (lift x) (format "( + x )").
End Notations.
Import Notations.
Section theory.
Context
`{ret_inst: Return T}
`{Map_T_inst: Map T}
`{Mapd_T_inst: Mapd nat T}
`{Traverse_T_inst: Traverse T}
`{Bind_T_inst: Bind T T}
`{Mapdt_T_inst: Mapdt nat T}
`{Bindd_T_inst: Bindd nat T T}
`{Bindt_T_inst: Bindt T T}
`{Binddt_T_inst: Binddt nat T T}
`{! Compat_Map_Binddt nat T T}
`{! Compat_Mapd_Binddt nat T T}
`{! Compat_Traverse_Binddt nat T T}
`{! Compat_Bind_Binddt nat T T}
`{! Compat_Mapdt_Binddt nat T T}
`{! Compat_Bindd_Binddt nat T T}
`{! Compat_Bindt_Binddt nat T T}
`{Monad_inst: ! DecoratedTraversableMonad nat T}.
Context
`{Map_U_inst: Map U}
`{Mapd_U_inst: Mapd nat U}
`{Traverse_U_inst: Traverse U}
`{Bind_U_inst: Bind T U}
`{Mapdt_U_inst: Mapdt nat U}
`{Bindd_U_inst: Bindd nat T U}
`{Bindt_U_inst: Bindt T U}
`{Binddt_U_inst: Binddt nat T U}
`{! Compat_Map_Binddt nat T U}
`{! Compat_Mapd_Binddt nat T U}
`{! Compat_Traverse_Binddt nat T U}
`{! Compat_Bind_Binddt nat T U}
`{! Compat_Mapdt_Binddt nat T U}
`{! Compat_Bindd_Binddt nat T U}
`{! Compat_Bindt_Binddt nat T U}
`{Module_inst: ! DecoratedTraversableRightPreModule nat T U
(unit := Monoid_unit_zero)
(op := Monoid_op_plus)}.
Lemma cl_at_loc_dec {gap}:
decidable_pred (fun p: nat × nat ⇒ cl_at_loc gap p).
Proof.
unfold decidable_pred.
intros [p n].
unfold cl_at_loc.
unfold bound_within.
unfold Decidable.decidable.
lia.
Qed.
Lemma cl_at_spec (gap: nat) (t: U nat):
cl_at gap t = ∀ (d: nat) (n: nat), (d, n) ∈d t → cl_at_loc gap (d, n).
Proof.
unfold cl_at.
apply propositional_extensionality.
rewrite forall_ctx_iff.
reflexivity.
Qed.
Lemma cl_at_decidable (gap: nat) (t: U nat):
cl_at gap t ∨ ¬ cl_at gap t.
Proof.
apply decidable_Forall_ctx.
apply cl_at_loc_dec.
Qed.
Lemma cl_at_spec_not (gap: nat) (t: U nat):
(¬ cl_at gap t) = ∃ (d: nat) (n: nat), (d, n) ∈d t ∧ (¬ cl_at_loc gap (d, n)).
Proof.
unfold cl_at.
apply propositional_extensionality.
rewrite not_forall_ctx_iff.
reflexivity.
apply cl_at_loc_dec.
Qed.
Lemma closed_at_sub1: ∀ (σ: nat → T nat) (k d1 i1: nat),
(∀ (n: nat), cl_at k (σ n)) →
cl_at (k + d1) (lift__sub d1 σ i1).
Proof.
introv Hpremise.
unfold cl_at, cl_at_loc in ×.
rewrite forall_ctx_iff.
setoid_rewrite forall_ctx_iff in Hpremise.
unfold bound_within in ×.
unfold lift__sub.
bound_induction.
- intros e a.
rewrite ind_rename_iff.
intros [l1 [Hin Heq]].
subst.
bound_induction.
cbn.
specialize (Hpremise (i1 - d1) e l1 Hin).
lia.
- setoid_rewrite ind_ret_iff.
unfold transparent tcs.
intros e a [HeZ Hai1].
subst. lia.
Qed.
Lemma closed_at_sub2:
∀ (t: T nat) (σ: nat → T nat) (k: nat),
(∀ (n: nat), cl_at k (σ n)) →
cl_at k (subst σ t).
Proof.
introv Hpremise.
unfold cl_at in ×.
unfold cl_at_loc in ×.
unfold bound_within in ×.
rewrite forall_ctx_iff.
setoid_rewrite forall_ctx_iff in Hpremise.
setoid_rewrite ind_subst_iff.
intros e a Hin.
destruct Hin as [d1 [d2 [i1 [H1 [H2 H3]]]]].
subst.
unfold local__sub, lift__sub in ×.
bound_induction_in H2.
+ rewrite ind_rename_iff in H2.
preprocess.
unfold lift.
specialize (Hpremise (i1 - d1) d2 x H).
bound_induction.
+ rewrite ind_ret_iff in H2.
inversion H2. subst.
unfold transparent tcs. lia.
Qed.
Lemma not_closed_at_ret:
∀ n, ¬ (cl_at n (@ret T _ nat n)).
Proof.
intros.
introv H.
unfold cl_at in H.
rewrite forall_ctx_iff in H.
specialize (H 0 n).
rewrite ind_ret_iff in H.
specialize (H ltac:(auto)).
unfold cl_at_loc in H.
unfold bound_within in H.
lia.
Qed.
Lemma closed_at_ret:
∀ n, cl_at (S n) (@ret T _ nat n).
Proof.
intros.
unfold cl_at.
rewrite forall_ctx_iff.
intros.
rewrite ind_ret_iff in H.
inversion H. subst. cbn.
unfold bound_within.
cbv.
lia.
Qed.
Lemma subst_pointwise (k: nat) (σ1 σ2: nat → T nat) (t: T nat):
cl_at k t →
(∀ i, i < k → σ1 i = σ2 i) →
subst σ1 t = subst σ2 t.
Proof.
unfold subst, cl_at.
intros Hclosed Hpw.
apply bindd_respectful.
intros w a Hin.
rewrite forall_ctx_iff in Hclosed.
specialize (Hclosed w a Hin).
unfold cl_at_loc, bound_within in Hclosed.
unfold local__sub, lift__sub.
bound_induction. fequal.
apply Hpw. lia.
Qed.
End theory.
Context
`{ret_inst: Return T}
`{Map_T_inst: Map T}
`{Mapd_T_inst: Mapd nat T}
`{Traverse_T_inst: Traverse T}
`{Bind_T_inst: Bind T T}
`{Mapdt_T_inst: Mapdt nat T}
`{Bindd_T_inst: Bindd nat T T}
`{Bindt_T_inst: Bindt T T}
`{Binddt_T_inst: Binddt nat T T}
`{! Compat_Map_Binddt nat T T}
`{! Compat_Mapd_Binddt nat T T}
`{! Compat_Traverse_Binddt nat T T}
`{! Compat_Bind_Binddt nat T T}
`{! Compat_Mapdt_Binddt nat T T}
`{! Compat_Bindd_Binddt nat T T}
`{! Compat_Bindt_Binddt nat T T}
`{Monad_inst: ! DecoratedTraversableMonad nat T}.
Context
`{Map_U_inst: Map U}
`{Mapd_U_inst: Mapd nat U}
`{Traverse_U_inst: Traverse U}
`{Bind_U_inst: Bind T U}
`{Mapdt_U_inst: Mapdt nat U}
`{Bindd_U_inst: Bindd nat T U}
`{Bindt_U_inst: Bindt T U}
`{Binddt_U_inst: Binddt nat T U}
`{! Compat_Map_Binddt nat T U}
`{! Compat_Mapd_Binddt nat T U}
`{! Compat_Traverse_Binddt nat T U}
`{! Compat_Bind_Binddt nat T U}
`{! Compat_Mapdt_Binddt nat T U}
`{! Compat_Bindd_Binddt nat T U}
`{! Compat_Bindt_Binddt nat T U}
`{Module_inst: ! DecoratedTraversableRightPreModule nat T U
(unit := Monoid_unit_zero)
(op := Monoid_op_plus)}.
Lemma cl_at_loc_dec {gap}:
decidable_pred (fun p: nat × nat ⇒ cl_at_loc gap p).
Proof.
unfold decidable_pred.
intros [p n].
unfold cl_at_loc.
unfold bound_within.
unfold Decidable.decidable.
lia.
Qed.
Lemma cl_at_spec (gap: nat) (t: U nat):
cl_at gap t = ∀ (d: nat) (n: nat), (d, n) ∈d t → cl_at_loc gap (d, n).
Proof.
unfold cl_at.
apply propositional_extensionality.
rewrite forall_ctx_iff.
reflexivity.
Qed.
Lemma cl_at_decidable (gap: nat) (t: U nat):
cl_at gap t ∨ ¬ cl_at gap t.
Proof.
apply decidable_Forall_ctx.
apply cl_at_loc_dec.
Qed.
Lemma cl_at_spec_not (gap: nat) (t: U nat):
(¬ cl_at gap t) = ∃ (d: nat) (n: nat), (d, n) ∈d t ∧ (¬ cl_at_loc gap (d, n)).
Proof.
unfold cl_at.
apply propositional_extensionality.
rewrite not_forall_ctx_iff.
reflexivity.
apply cl_at_loc_dec.
Qed.
Lemma closed_at_sub1: ∀ (σ: nat → T nat) (k d1 i1: nat),
(∀ (n: nat), cl_at k (σ n)) →
cl_at (k + d1) (lift__sub d1 σ i1).
Proof.
introv Hpremise.
unfold cl_at, cl_at_loc in ×.
rewrite forall_ctx_iff.
setoid_rewrite forall_ctx_iff in Hpremise.
unfold bound_within in ×.
unfold lift__sub.
bound_induction.
- intros e a.
rewrite ind_rename_iff.
intros [l1 [Hin Heq]].
subst.
bound_induction.
cbn.
specialize (Hpremise (i1 - d1) e l1 Hin).
lia.
- setoid_rewrite ind_ret_iff.
unfold transparent tcs.
intros e a [HeZ Hai1].
subst. lia.
Qed.
Lemma closed_at_sub2:
∀ (t: T nat) (σ: nat → T nat) (k: nat),
(∀ (n: nat), cl_at k (σ n)) →
cl_at k (subst σ t).
Proof.
introv Hpremise.
unfold cl_at in ×.
unfold cl_at_loc in ×.
unfold bound_within in ×.
rewrite forall_ctx_iff.
setoid_rewrite forall_ctx_iff in Hpremise.
setoid_rewrite ind_subst_iff.
intros e a Hin.
destruct Hin as [d1 [d2 [i1 [H1 [H2 H3]]]]].
subst.
unfold local__sub, lift__sub in ×.
bound_induction_in H2.
+ rewrite ind_rename_iff in H2.
preprocess.
unfold lift.
specialize (Hpremise (i1 - d1) d2 x H).
bound_induction.
+ rewrite ind_ret_iff in H2.
inversion H2. subst.
unfold transparent tcs. lia.
Qed.
Lemma not_closed_at_ret:
∀ n, ¬ (cl_at n (@ret T _ nat n)).
Proof.
intros.
introv H.
unfold cl_at in H.
rewrite forall_ctx_iff in H.
specialize (H 0 n).
rewrite ind_ret_iff in H.
specialize (H ltac:(auto)).
unfold cl_at_loc in H.
unfold bound_within in H.
lia.
Qed.
Lemma closed_at_ret:
∀ n, cl_at (S n) (@ret T _ nat n).
Proof.
intros.
unfold cl_at.
rewrite forall_ctx_iff.
intros.
rewrite ind_ret_iff in H.
inversion H. subst. cbn.
unfold bound_within.
cbv.
lia.
Qed.
Lemma subst_pointwise (k: nat) (σ1 σ2: nat → T nat) (t: T nat):
cl_at k t →
(∀ i, i < k → σ1 i = σ2 i) →
subst σ1 t = subst σ2 t.
Proof.
unfold subst, cl_at.
intros Hclosed Hpw.
apply bindd_respectful.
intros w a Hin.
rewrite forall_ctx_iff in Hclosed.
specialize (Hclosed w a Hin).
unfold cl_at_loc, bound_within in Hclosed.
unfold local__sub, lift__sub.
bound_induction. fequal.
apply Hpw. lia.
Qed.
End theory.