Commit 49ac37b8 authored by Robbert Krebbers's avatar Robbert Krebbers

Some tweaks to the telescope file.

parent 6a854a8a
......@@ -10,15 +10,14 @@ but might be needed for future extensions, such as for bounded polymorphism *)
(** Type Telescopes *)
Inductive ktele {Σ} :=
| KTeleO : ktele
| KTeleS {k} (binder : lty Σ k ktele) : ktele.
| KTeleS {k} : (lty Σ k ktele) ktele.
Arguments ktele : clear implicits.
(** The telescope version of kind types *)
Fixpoint ktele_fun {Σ} (kt : ktele Σ) (T : Type) :=
Fixpoint ktele_fun {Σ} (kt : ktele Σ) (A : Type) :=
match kt with
| KTeleO => T
| KTeleS b => K, ktele_fun (b K) T
| KTeleO => A
| KTeleS b => K, ktele_fun (b K) A
end.
Notation "kt -k> A" :=
......@@ -34,25 +33,13 @@ Definition ktele_fold {Σ X Y kt}
end) kt.
Arguments ktele_fold {_ _ _ !_} _ _ _ /.
(** A sigma-like type for an "element" of a telescope, i.e. the data it *)
(* takes to get a [T] from a [kt -t> T]. *)
(** A sigma-like type for an "element" of a telescope, i.e., the data it *)
Inductive ltys {Σ} : ktele Σ Type :=
| LTysO : ltys KTeleO
(* the [X] is the only relevant data here *)
| LTysS {k} {binder} (K : lty Σ k) :
ltys (binder K)
ltys (KTeleS binder).
| LTysS {k b} : K : lty Σ k, ltys (b K) ltys (KTeleS b).
Arguments ltys : clear implicits.
Definition ktele_app {Σ kt T} (f : kt -k> T) : ltys Σ kt T :=
λ Ks, (fix rec {kt} (Ks : ltys Σ kt) : (kt -k> T) T :=
match Ks in ltys _ kt return (kt -k> T) T with
| LTysO => λ t : T, t
| LTysS K Ks => λ f, rec Ks (f K)
end) kt Ks f.
Arguments ktele_app {_} {!_ _} _ !_ /.
(** Inversion lemma for [tele_arg] *)
(** Inversion lemmas for [ltys] *)
Lemma ltys_inv {Σ kt} (Ks : ltys Σ kt) :
match kt as kt return ltys _ kt Prop with
| KTeleO => λ Ks, Ks = LTysO
......@@ -65,7 +52,14 @@ Lemma ltys_S_inv {Σ X} {f : lty Σ X → ktele Σ} (Ks : ltys Σ (KTeleS f)) :
K Ks', Ks = LTysS K Ks'.
Proof. exact (ltys_inv Ks). Qed.
(** Operate below [tele_fun]s with argument telescope [kt]. *)
Definition ktele_app {Σ kt T} (f : kt -k> T) (Ks : ltys Σ kt) : T :=
(fix rec {kt} (Ks : ltys Σ kt) : (kt -k> T) T :=
match Ks in ltys _ kt return (kt -k> T) T with
| LTysO => λ t : T, t
| LTysS K Ks => λ f, rec Ks (f K)
end) kt Ks f.
Arguments ktele_app {_} {!_ _} _ !_ /.
Fixpoint ktele_bind {Σ U kt} : (ltys Σ kt U) kt -k> U :=
match kt as kt return (ltys _ kt U) kt -k> U with
| KTeleO => λ F, F LTysO
......@@ -74,12 +68,10 @@ Fixpoint ktele_bind {Σ U kt} : (ltys Σ kt → U) → kt -k> U :=
end.
Arguments ktele_bind {_} {_ !_} _ /.
(* Show that tele_app ∘ tele_bind is the identity. *)
Lemma ktele_app_bind {Σ U kt} (f : ltys Σ kt U) K :
ktele_app (ktele_bind f) K = f K.
Proof.
induction kt as [|k b IH]; simpl in *.
- rewrite (ltys_O_inv K). done.
- destruct (ltys_S_inv K) as [K' [Ks' ->]]. simpl.
rewrite IH. done.
- by rewrite (ltys_O_inv K).
- destruct (ltys_S_inv K) as [K' [Ks' ->]]; simpl. by rewrite IH.
Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment