Commit c9b8604d authored by Robbert Krebbers's avatar Robbert Krebbers

Remove old stuff.

parent 0d22cb10
...@@ -6,14 +6,14 @@ Set Default Proof Using "Type". ...@@ -6,14 +6,14 @@ Set Default Proof Using "Type".
dependencies between binders, hence we might have just used a list of [kind] dependencies between binders, hence we might have just used a list of [kind]
but might be needed for future extensions, such as for bounded polymorphism *) but might be needed for future extensions, such as for bounded polymorphism *)
(** Type Telescopes *) (** Type Telescopes *)
Inductive ktele {Σ} : Type := Inductive ktele {Σ} :=
| KTeleO : ktele | KTeleO : ktele
| KTeleS {k} (binder : lty Σ k ktele) : ktele. | KTeleS {k} (binder : lty Σ k ktele) : ktele.
Arguments ktele : clear implicits. Arguments ktele : clear implicits.
(** The telescope version of kind types *) (** The telescope version of kind types *)
Fixpoint ktele_fun {Σ} (kt : ktele Σ) (T : Type) : Type := Fixpoint ktele_fun {Σ} (kt : ktele Σ) (T : Type) :=
match kt with match kt with
| KTeleO => T | KTeleO => T
| KTeleS b => K, ktele_fun (b K) T | KTeleS b => K, ktele_fun (b K) T
...@@ -22,9 +22,7 @@ Fixpoint ktele_fun {Σ} (kt : ktele Σ) (T : Type) : Type := ...@@ -22,9 +22,7 @@ Fixpoint ktele_fun {Σ} (kt : ktele Σ) (T : Type) : Type :=
Notation "kt -k> A" := Notation "kt -k> A" :=
(ktele_fun kt A) (at level 99, A at level 200, right associativity). (ktele_fun kt A) (at level 99, A at level 200, right associativity).
(** An eliminator for elements of [ktele_fun]. (** An eliminator for elements of [ktele_fun]. *)
We use a [fix] because, for some reason, that makes stuff print nicer
in the proofs in iris:bi/lib/telescopes.v *)
Definition ktele_fold {Σ X Y kt} Definition ktele_fold {Σ X Y kt}
(step : {k}, (lty Σ k Y) Y) (base : X Y) : (kt -k> X) Y := (step : {k}, (lty Σ k Y) Y) (base : X Y) : (kt -k> X) Y :=
(fix rec {kt} : (kt -k> X) Y := (fix rec {kt} : (kt -k> X) Y :=
...@@ -52,10 +50,6 @@ Definition ktele_app {Σ kt T} (f : kt -k> T) : ltys Σ kt → T := ...@@ -52,10 +50,6 @@ Definition ktele_app {Σ kt T} (f : kt -k> T) : ltys Σ kt → T :=
end) kt Ks f. end) kt Ks f.
Arguments ktele_app {_} {!_ _} _ !_ /. Arguments ktele_app {_} {!_ _} _ !_ /.
(* Coercion ltys : ktele >-> Sortclass. *)
(* This is a local coercion because otherwise, the "λ.." notation stops working. *)
(* Local Coercion ktele_app : ktele_fun >-> Funclass. *)
(** Inversion lemma for [tele_arg] *) (** Inversion lemma for [tele_arg] *)
Lemma ltys_inv {Σ kt} (Ks : ltys Σ kt) : Lemma ltys_inv {Σ kt} (Ks : ltys Σ kt) :
match kt as kt return ltys _ kt Prop with match kt as kt return ltys _ kt Prop with
...@@ -68,31 +62,7 @@ Proof. exact (ltys_inv Ks). Qed. ...@@ -68,31 +62,7 @@ Proof. exact (ltys_inv Ks). Qed.
Lemma ltys_S_inv {Σ X} {f : lty Σ X ktele Σ} (Ks : ltys Σ (KTeleS f)) : Lemma ltys_S_inv {Σ X} {f : lty Σ X ktele Σ} (Ks : ltys Σ (KTeleS f)) :
K Ks', Ks = LTysS K Ks'. K Ks', Ks = LTysS K Ks'.
Proof. exact (ltys_inv Ks). Qed. Proof. exact (ltys_inv Ks). Qed.
(*
(** Map below a tele_fun *)
Fixpoint ktele_map {Σ} {T U} {kt : ktele Σ} : (T → U) → (kt -k> T) → kt -k> U :=
match kt as kt return (T → U) → (kt -k> T) → kt -k> U with
| KTeleO => λ F : T → U, F
| @KTeleS _ X b => λ (F : T → U) (f : KTeleS b -k> T) (x : lty Σ X),
ktele_map F (f x)
end.
Arguments ktele_map {_} {_ _ !_} _ _ /.
Lemma ktele_map_app {Σ} {T U} {kt : ktele Σ} (F : T → U) (t : kt -k> T) (x : kt) :
(ktele_map F t) x = F (t x).
Proof.
induction kt as [|X f IH]; simpl in *.
- rewrite (ltys_O_inv x). done.
- destruct (ltys_S_inv x) as [x' [a' ->]]. simpl.
rewrite <-IH. done.
Qed.
Global Instance ktele_fmap {Σ} {kt : ktele Σ} : FMap (ktele_fun kt) :=
λ T U, ktele_map.
Lemma ktele_fmap_app {Σ} {T U} {kt : ktele Σ} (F : T → U) (t : kt -k> T) (x : kt) :
(F <$> t) x = F (t x).
Proof. apply ktele_map_app. Qed.
*)
(** Operate below [tele_fun]s with argument telescope [kt]. *) (** Operate below [tele_fun]s with argument telescope [kt]. *)
Fixpoint ktele_bind {Σ U kt} : (ltys Σ kt U) kt -k> U := Fixpoint ktele_bind {Σ U kt} : (ltys Σ kt U) kt -k> U :=
match kt as kt return (ltys _ kt U) kt -k> U with match kt as kt return (ltys _ kt U) kt -k> U with
...@@ -111,74 +81,3 @@ Proof. ...@@ -111,74 +81,3 @@ Proof.
- destruct (ltys_S_inv K) as [K' [Ks' ->]]. simpl. - destruct (ltys_S_inv K) as [K' [Ks' ->]]. simpl.
rewrite IH. done. rewrite IH. done.
Qed. Qed.
Fixpoint ktele_to_tele {Σ} (kt : ktele Σ) : tele :=
match kt with
| KTeleO => TeleO
| KTeleS b => TeleS (λ x, ktele_to_tele (b x))
end.
Fixpoint ltys_to_tele_args {Σ} {kt} (Ks : ltys Σ kt) :
tele_arg (ktele_to_tele kt) :=
match Ks with
| LTysO => TargO
| LTysS K Ks => TargS K (ltys_to_tele_args Ks)
end.
(*
(** We can define the identity function and composition of the [-t>] function *)
(* space. *)
Definition ktele_fun_id {Σ} {kt : ktele Σ} : kt -k> kt := ktele_bind id.
Lemma ktele_fun_id_eq {Σ} {kt : ktele Σ} (x : kt) :
ktele_fun_id x = x.
Proof. unfold ktele_fun_id. rewrite ktele_app_bind. done. Qed.
Definition ktele_fun_compose {Σ} {kt1 kt2 kt3 : ktele Σ} :
(kt2 -k> kt3) → (kt1 -k> kt2) → (kt1 -k> kt3) :=
λ t1 t2, ktele_bind (compose (ktele_app t1) (ktele_app t2)).
Lemma ktele_fun_compose_eq {Σ} {kt1 kt2 kt3 : ktele Σ} (f : kt2 -k> kt3) (g : kt1 -k> kt2) x :
ktele_fun_compose f g $ x = (f ∘ g) x.
Proof. unfold ktele_fun_compose. rewrite ktele_app_bind. done. Qed.
*)
(*
(** Notation-compatible telescope mapping *)
(* This adds (tele_app ∘ tele_bind), which is an identity function, around every *)
(* binder so that, after simplifying, this matches the way we typically write *)
(* notations involving telescopes. *)
Notation "'λ..' x .. y , e" :=
(ktele_app (ktele_bind (λ x, .. (ktele_app (ktele_bind (λ y, e))) .. )))
(at level 200, x binder, y binder, right associativity,
format "'[ ' 'λ..' x .. y ']' , e") : stdpp_scope.
(** Telescopic quantifiers *)
Definition ktforall {Σ} {kt : ktele Σ} (Ψ : kt → Prop) : Prop :=
ktele_fold (λ (T : kind), λ (b : (lty Σ T) → Prop), (∀ x : (lty Σ T), b x)) (λ x, x) (ktele_bind Ψ).
Arguments ktforall {_ !_} _ /.
Notation "'∀..' x .. y , P" := (ktforall (λ x, .. (ktforall (λ y, P)) .. ))
(at level 200, x binder, y binder, right associativity,
format "∀.. x .. y , P") : stdpp_scope.
Lemma ktforall_forall {Σ} {kt : ktele Σ} (Ψ : kt → Prop) :
ktforall Ψ ↔ (∀ x, Ψ x).
Proof.
symmetry. unfold ktforall. induction kt as [|X ft IH].
- simpl. split.
+ done.
+ intros ? p. rewrite (ltys_O_inv p). done.
- simpl. split; intros Hx a.
+ rewrite <-IH. done.
+ destruct (ltys_S_inv a) as [x [pf ->]].
revert pf. setoid_rewrite IH. done.
Qed.
(* Teach typeclass resolution how to make progress on these binders *)
Typeclasses Opaque ktforall.
Hint Extern 1 (ktforall _) =>
progress cbn [ttforall ktele_fold ktele_bind ktele_app] : typeclass_instances.
*)
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