From 2f569a21f0cd557505551a8c30689a5d9bdd9e1e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Laurent?= Date: Wed, 22 Nov 2023 10:30:56 +0100 Subject: [PATCH] statement of the directed theorem --- _CoqProject | 3 +- theories/DirectedDeclarativeTyping.v | 4 +- theories/DirectedMorphisms.v | 128 ++++++++++ theories/DirectedSemantics.v | 283 +++++----------------- theories/DirectedTyping.v | 342 --------------------------- 5 files changed, 191 insertions(+), 569 deletions(-) create mode 100644 theories/DirectedMorphisms.v delete mode 100644 theories/DirectedTyping.v diff --git a/_CoqProject b/_CoqProject index 0de81a5..6fe3d39 100644 --- a/_CoqProject +++ b/_CoqProject @@ -24,8 +24,9 @@ theories/DeclarativeInstance.v theories/DirectedDirections.v theories/DirectedContext.v theories/DirectedDirectioning.v -theories/DirectedSemantics.v theories/DirectedDeclarativeTyping.v +theories/DirectedMorphisms.v +theories/DirectedSemantics.v theories/LogicalRelation.v theories/LogicalRelation/Induction.v diff --git a/theories/DirectedDeclarativeTyping.v b/theories/DirectedDeclarativeTyping.v index e28b4f2..8a2c203 100644 --- a/theories/DirectedDeclarativeTyping.v +++ b/theories/DirectedDeclarativeTyping.v @@ -510,7 +510,7 @@ Module Examples. Module Morphism. - From LogRel Require Import DirectedSemantics. + From LogRel Require Import DirectedMorphisms. From LogRel Require Import Notations Context DeclarativeTyping DeclarativeInstance Weakening GenericTyping DeclarativeInstance. Lemma morphism_fwd_characterization `{GenericTypingProperties} Δ (A B : term) l : @@ -612,7 +612,7 @@ Module Examples. Module Morphism. - From LogRel Require Import DirectedSemantics. + From LogRel Require Import DirectedMorphisms. From LogRel Require Import Notations Context DeclarativeTyping DeclarativeInstance Weakening GenericTyping DeclarativeInstance. Lemma morphism_fwd_characterization `{GenericTypingProperties} Δ (A1 B1 A2 B2 : term) l : diff --git a/theories/DirectedMorphisms.v b/theories/DirectedMorphisms.v new file mode 100644 index 0000000..014c3dc --- /dev/null +++ b/theories/DirectedMorphisms.v @@ -0,0 +1,128 @@ + +From Coq Require Import ssreflect. +From Equations Require Import Equations. +From smpl Require Import Smpl. +From LogRel.AutoSubst Require Import core unscoped Ast Extra. +From LogRel Require Import Utils BasicAst. +From LogRel Require Import DirectedDirections DirectedContext DirectedDirectioning. + +Reserved Notation "[ Δ |- w : t -( d )- u : A ]" (at level 0, Δ, d, t, u, A, w at level 50). +Reserved Notation "[ Δ |- ϕ : σ -( )- τ : Θ ]" (at level 0, Δ, Θ, σ, τ, ϕ at level 50). + +Definition err_term : term := tApp U U. + +Definition action + (δ: list direction) + (dt: direction) (t: term) : + [δ |- t ▹ dt] -> + forall (σ τ: nat -> term), list term -> term. +Proof. + induction 1 eqn: eq; intros σ τ l. + - exact (tLambda U (tRel 0)). + - exact (List.nth n l err_term). + - remember d'' as dt. destruct d''. + + pose (tA := IHd1 _ eq_refl σ τ l). + pose (tB := IHd2 _ eq_refl + (scons (tApp tA⟨↑⟩ (tRel 0)) σ) + (scons (tRel 0) τ) + (cons err_term l)). + exact (tLambda (tProd A B)[σ] (tLambda A[τ] ( + tApp tB⟨up_ren ↑⟩ (tApp (tRel 1) (tApp tA⟨↑⟩⟨↑⟩ (tRel 0))) + ))). + + pose (tA := IHd1 _ eq_refl σ τ l). + pose (tB := IHd2 _ eq_refl + (scons (tRel 0) σ) + (scons (tApp tA⟨↑⟩ (tRel 0)) τ) + (cons err_term l)). + exact (tLambda (tProd A B)[τ] (tLambda A[σ] ( + tApp tB⟨up_ren ↑⟩ (tApp (tRel 1) (tApp tA⟨↑⟩⟨↑⟩ (tRel 0))) + ))). + + exact (tLambda (tProd A B)[σ] (tRel 0)). + - pose (tA := IHd1 _ eq_refl σ τ l). + remember dA as d''. destruct d''. + + pose (tt := IHd2 _ eq_refl + (scons (tRel 0) σ) + (scons (tApp tA⟨↑⟩ (tRel 0)) τ) + (cons (tLambda (* TODO FixMe *) err_term (tRel 0)) l)). + exact (tLambda A[σ] (tLambda A[τ] tt⟨↑⟩)). + + pose (tt := IHd2 _ eq_refl + (scons (tApp tA⟨↑⟩ (tRel 0)) σ) + (scons (tRel 0) τ) + (cons (tLambda (* TODO FixMe *) err_term (tRel 0)) l)). + exact (tLambda A[σ] (tLambda A[τ] tt)⟨↑⟩). + + pose (tt := IHd2 _ eq_refl + (scons (tRel 0) σ) + (scons (tRel 0) τ) + (cons (tLambda A[σ] (* ≅ A[τ]*) (tRel 0)) l)). + exact (tLambda A[σ] (tLambda A[τ] tt⟨↑⟩)). + - (* TODO: I think the direction of A is (dir_op dT) *) + pose (tf := IHd1 _ eq_refl σ τ l). + exact (tApp (tApp tf a[σ]) a[τ]). +Defined. + +Definition compute_action (δ: list direction) (t: term) (σ τ: nat -> term) (ϕ: list term) : term := + match compute_DirInfer δ t with + | None => err_term + | Some (d; der) => action δ d t der σ τ ϕ + end. + + +From LogRel Require Import Notations Context Weakening GenericTyping. + + +Section MorphismDefinition. + Context `{GenericTypingProperties}. + + Fixpoint termRelArr Δ t u A : term := + match A with + | U => arr t u + | tProd A B => tProd A (termRelArr (Δ ,, A) (eta_expand t) (eta_expand u) B) + | _ => err_term + end. + + Definition termRel Δ t u d (A : term) : Type := + match d with + | Fun => ∑ f, [ Δ |- f : termRelArr Δ t u A ] + | Cofun => ∑ f, [ Δ |- f : termRelArr Δ u t A ] + | Discr => [Δ |- t ≅ u : A] + end. + + + Definition termRelPred Δ t u d (A : term) (f : term) : Type := + match d with + | Fun => [ Δ |- f : termRelArr Δ t u A ] + | Cofun => [ Δ |- f : termRelArr Δ u t A ] + | Discr => [Δ |- t ≅ u : A] + end. + + Definition dispatchDir γ σ τ φ A dA t u := + match dA with + (* Discrete case, A[σ] ≅ A[τ], no transport needed *) + | Discr => (t, u, A[σ]) + (* Fun case, A @ φ : A[σ] → A[τ] *) + | Fun => (tApp (compute_action γ A σ τ φ) t, u, A[τ]) + (* Cofun case, A @ φ : A[τ] → A[σ] *) + | Cofun => (t, tApp (compute_action γ A σ τ φ) u, A[σ]) + end. + + Definition tail (σ : nat -> term) := fun n => σ (S n). + + Fixpoint substRel + (Δ: Context.context) + (σ τ : nat -> term) + (Θ : DirectedContext.context) + (φ : list term) : Type := + match Θ, φ with + | nil, nil => unit + | (cons Adecl Θ), (cons w φ) => + substRel Δ (tail σ) (tail τ) Θ φ × + let '(t',u',A') := + dispatchDir (dirs Θ) (tail σ) (tail τ) φ Adecl.(ty) Adecl.(ty_dir) (σ 0) (τ 0) + in termRelPred Δ t' u' Adecl.(dir) A' w + | _, _ => False + end. + + +End MorphismDefinition. + + Notation "[ Δ |- ϕ : σ -( )- τ : Θ ]" := (substRel Δ σ τ Θ ϕ). diff --git a/theories/DirectedSemantics.v b/theories/DirectedSemantics.v index b322fb6..a7c2866 100644 --- a/theories/DirectedSemantics.v +++ b/theories/DirectedSemantics.v @@ -3,230 +3,61 @@ From Coq Require Import ssreflect. From Equations Require Import Equations. From smpl Require Import Smpl. From LogRel.AutoSubst Require Import core unscoped Ast Extra. -From LogRel Require Import Utils BasicAst. -From LogRel Require Import DirectedDirections DirectedContext DirectedDirectioning. +From LogRel Require Import DirectedDirections DirectedContext DirectedDirectioning DirectedMorphisms DirectedDeclarativeTyping. +From LogRel Require Import Utils BasicAst Notations GenericTyping. -Reserved Notation "[ Δ |- w : t -( d )- u : A ]" (at level 0, Δ, d, t, u, A, w at level 50). -Reserved Notation "[ Δ |- ϕ : σ -( )- τ : Θ ]" (at level 0, Δ, Θ, σ, τ, ϕ at level 50). +(* TODO: reorganize files! *) +Section DirectedValid. -Definition err_term : term := tApp U U. - -Definition action - (δ: list direction) - (dt: direction) (t: term) : - [δ |- t ▹ dt] -> - forall (σ τ: nat -> term), list term -> term. -Proof. - induction 1 eqn: eq; intros σ τ l. - - exact (tLambda U (tRel 0)). - - exact (List.nth n l err_term). - - remember d'' as dt. destruct d''. - + pose (tA := IHd1 _ eq_refl σ τ l). - pose (tB := IHd2 _ eq_refl - (scons (tApp tA⟨↑⟩ (tRel 0)) σ) - (scons (tRel 0) τ) - (cons err_term l)). - exact (tLambda (tProd A B)[σ] (tLambda A[τ] ( - tApp tB⟨up_ren ↑⟩ (tApp (tRel 1) (tApp tA⟨↑⟩⟨↑⟩ (tRel 0))) - ))). - + pose (tA := IHd1 _ eq_refl σ τ l). - pose (tB := IHd2 _ eq_refl - (scons (tRel 0) σ) - (scons (tApp tA⟨↑⟩ (tRel 0)) τ) - (cons err_term l)). - exact (tLambda (tProd A B)[τ] (tLambda A[σ] ( - tApp tB⟨up_ren ↑⟩ (tApp (tRel 1) (tApp tA⟨↑⟩⟨↑⟩ (tRel 0))) - ))). - + exact (tLambda (tProd A B)[σ] (tRel 0)). - - pose (tA := IHd1 _ eq_refl σ τ l). - remember dA as d''. destruct d''. - + pose (tt := IHd2 _ eq_refl - (scons (tRel 0) σ) - (scons (tApp tA⟨↑⟩ (tRel 0)) τ) - (cons (tLambda (* TODO FixMe *) err_term (tRel 0)) l)). - exact (tLambda A[σ] (tLambda A[τ] tt⟨↑⟩)). - + pose (tt := IHd2 _ eq_refl - (scons (tApp tA⟨↑⟩ (tRel 0)) σ) - (scons (tRel 0) τ) - (cons (tLambda (* TODO FixMe *) err_term (tRel 0)) l)). - exact (tLambda A[σ] (tLambda A[τ] tt)⟨↑⟩). - + pose (tt := IHd2 _ eq_refl - (scons (tRel 0) σ) - (scons (tRel 0) τ) - (cons (tLambda A[σ] (* ≅ A[τ]*) (tRel 0)) l)). - exact (tLambda A[σ] (tLambda A[τ] tt⟨↑⟩)). - - (* TODO: I think the direction of A is (dir_op dT) *) - pose (tf := IHd1 _ eq_refl σ τ l). - exact (tApp (tApp tf a[σ]) a[τ]). -Defined. - -Definition compute_action (δ: list direction) (t: term) (σ τ: nat -> term) (ϕ: list term) : term := - match compute_DirInfer δ t with - | None => err_term - | Some (d; der) => action δ d t der σ τ ϕ - end. - - -From LogRel Require Import Notations Context DeclarativeTyping DeclarativeInstance Weakening GenericTyping DeclarativeInstance. - - -Section MorphismDefinition. Context `{GenericTypingProperties}. - - Fixpoint termRelArr Δ t u A : term := - match A with - | U => arr t u - | tProd A B => tProd A (termRelArr (Δ ,, A) (eta_expand t) (eta_expand u) B) - | _ => err_term - end. - - Definition termRel Δ t u d (A : term) : Type := - match d with - | Fun => ∑ f, [ Δ |- f : termRelArr Δ t u A ] - | Cofun => ∑ f, [ Δ |- f : termRelArr Δ u t A ] - | Discr => [Δ |- t ≅ u : A] - end. - - Definition termRelPred Δ t u d (A : term) (f : term) : Type := - match d with - | Fun => [ Δ |- f : termRelArr Δ t u A ] - | Cofun => [ Δ |- f : termRelArr Δ u t A ] - | Discr => [Δ |- t ≅ u : A] - end. - - Definition dispatchDir γ σ τ φ A dA t u := - match dA with - (* Discrete case, A[σ] ≅ A[τ], no transport needed *) - | Discr => (t, u, A[σ]) - (* Fun case, A @ φ : A[σ] → A[τ] *) - | Fun => (tApp (compute_action γ A σ τ φ) t, u, A[τ]) - (* Cofun case, A @ φ : A[τ] → A[σ] *) - | Cofun => (t, tApp (compute_action γ A σ τ φ) u, A[σ]) - end. - - Definition tail (σ : nat -> term) := fun n => σ (S n). - - Fixpoint substRel - (Δ: Context.context) - (σ τ : nat -> term) - (Θ : DirectedContext.context) - (φ : list term) : Type := - match Θ, φ with - | nil, nil => unit - | (cons Adecl Θ), (cons w φ) => - substRel Δ (tail σ) (tail τ) Θ φ × - let '(t',u',A') := - dispatchDir (dirs Θ) (tail σ) (tail τ) φ Adecl.(ty) Adecl.(ty_dir) (σ 0) (τ 0) - in termRelPred Δ t' u' Adecl.(dir) A' w - | _, _ => False - end. - - Inductive TermRel (Δ: Context.context) (t u: term) : forall (d: direction), term -> term -> Type := - | termRelFun { f } : - [ Δ |- f : arr t u ] -> - [ Δ |- f : t -( Fun )- u : U ] - | termRelCofun { f } : - [ Δ |- f : arr u t ] -> - [ Δ |- f : t -( Cofun )- u : U ] - | termRelDiscr { A } : - [ Δ |- t ≅ u : A ] -> - [ Δ |- err_term : t -( Discr )- u : A ] - | termRelPiFun { A B w }: - (* KM: I'm a bit skeptical that this typing premise should be needed. - This relation should assume that the type is well-formed and comes with all the inversion lemmas needed *) - [ Δ |- A ] -> - [ Δ ,, A |- w : tApp t⟨@wk1 Δ A⟩ (tRel 0) -( Fun )- tApp u⟨@wk1 Δ A⟩ (tRel 0) : B ] -> - [ Δ |- tLambda A w : t -( Fun )- u : tProd A B ] - | termRelPiCofun { A B w }: - [ Δ |- A ] -> - [ Δ ,, A |- w : tApp t⟨@wk1 Δ A⟩ (tRel 0) -( Cofun )- tApp u⟨@wk1 Δ A⟩ (tRel 0) : B ] -> - [ Δ |- tLambda A w : t -( Cofun )- u : tProd A B ] - - where "[ Δ |- w : t -( d )- u : A ]" := (TermRel Δ t u d A w). - - Close Scope typing_scope. - - Context (type_act : forall (γ : list direction) (dA : direction) (A : term) (wdA : [γ |- A ◃ dA]) (σ τ : nat -> term) (φ : list term), term). - - (* Given a context of directions γ coming from Θ, - substitutions, Δ |- σ, τ : |Θ|, - a morphism Δ |- φ : σ ⇒ τ : Θ, - a type |Θ| |- A, terms Δ |- t : A[σ], Δ |- u : A[τ], - returns the adequate triple (t',u', A') by acting - on t/u and substituting A according to the direction dA of A *) - Definition dispatch_dir γ σ τ φ A dA wdA t u := - match dA with - (* Discrete case, A[σ] ≅ A[τ], no transport needed *) - | Discr => (t, u, A[σ]) - (* Fun case, A @ φ : A[σ] → A[τ] *) - | Fun => (tApp (type_act γ dA A wdA σ τ φ) t, u, A[τ]) - (* Cofun case, A @ φ : A[τ] → A[σ] *) - | Cofun => (t, tApp (type_act γ dA A wdA σ τ φ) u, A[σ]) - end. - - Inductive SubstRel (Δ: Context.context) : - (nat -> term) -> (nat -> term) -> DirectedContext.context -> list term -> Type := - | substRelSEmpty : forall σ τ, [ Δ |- nil : σ -( )- τ : nil ] - | substRelSCons {Θ σ τ φ A dA t u w d} (wdA : [dirs Θ |- A ◃ dA]) - (tuA := dispatch_dir (dirs Θ) σ τ φ A dA wdA t u) (t':= fst tuA) (u' := fst (snd tuA)) (A' := snd (snd tuA)): - [ Δ |- φ : σ -( )- τ : Θ] -> - [ Δ |- w : t' -( d )- u' : A' ] -> - [ Δ |- (w :: φ) : (t .: σ) -( )- (u .: τ) : (Θ ,, d \ A @ dA)] - where "[ Δ |- ϕ : σ -( )- τ : Θ ]" := (SubstRel Δ σ τ Θ ϕ). - -End MorphismDefinition. - -(* (* TODO: reorganize files! *) *) -(* Section DirectedAction. *) - -(* Context {Δ} (wfΔ: [ |- Δ ]). *) - -(* Let Pctx θ := [ |-( ) θ ] -> unit. *) - -(* Let Pty Θ d A := forall (wfA : [ Θ |-( d ) A ]), *) -(* forall (σ τ: nat -> term) ϕ, [ Δ |- ϕ : σ -( )- τ : Θ ] -> *) -(* match d with *) -(* | Fun => [ Δ |- wfty_action ϕ wfA : arr A[σ] A[τ] ] *) -(* | Cofun => [ Δ |- wfty_action ϕ wfA : arr A[τ] A[σ] ] *) -(* | Discr => [ Δ |- A[σ] ≅ A[τ] ] *) -(* end. *) - -(* Let Ptm Θ dt A dA t := forall (wtt: [ Θ |-( dt ) t : A @( dA ) ]), *) -(* forall (σ τ: nat -> term) ϕ, [ Δ |- ϕ : σ -( )- τ : Θ ] -> *) -(* match dA with *) -(* | Fun => ∑ (w: witType dt), [ Δ |- w : tApp (wtterm_action ϕ wtt) t[σ] -( dt )- t[τ] : A[τ] ] *) -(* | Cofun => ∑ (w: witType dt), [ Δ |- w : t[σ] -( dt )- tApp (wtterm_action ϕ wtt) t[τ] : A[σ] ] *) -(* | Discr => ∑ (w: witType dt), [ Δ |- w : t[σ] -( dt )- t[τ] : A[σ] ] *) -(* end. *) - -(* Let Pconvty Θ d A B := [ Θ |-( d ) A ≅ B ] -> unit. *) - -(* Let Pconvtm Θ dt A dA t u := [ Θ |-( dt ) t ≅ u : A @( dA ) ] -> unit. *) - -(* Definition DirectedAction : *) -(* DirectedDeclarativeTyping.WfDeclInductionConcl Pctx Pty Ptm Pconvty Pconvtm. *) -(* Proof. *) -(* eapply DirectedDeclarativeTyping.WfDeclInduction. *) -(* all: revert Pctx Pty Ptm Pconvty Pconvtm; simpl. *) -(* all: try (intros; exact tt). *) -(* - (* wfTypeU *) *) -(* intros Θ d wfΘ _ wfU σ τ l rel. *) -(* have wfU' : [ Δ |- U ] by constructor. *) -(* destruct d. *) -(* 1-3: repeat (constructor; tea). *) -(* - (* wfTypeProd *) *) -(* intros Θ d A B wfA IHA wfB IHB wfProd σ τ l rel. *) -(* destruct d. *) -(* + admit. *) -(* + admit. *) -(* + cbn in *. *) -(* constructor. *) + Context {Δ} (wfΔ: [ |- Δ ]). + + Let Pctx θ := [ |-( ) θ ] -> unit. + + Let Pty Θ d A := forall (wfA : [ Θ |-( d ) A ]), + forall (σ τ: nat -> term) ϕ, + [ Δ |- ϕ : σ -( )- τ : Θ ] -> + match d with + | Fun => [ Δ |- compute_action (dirs Θ) A σ τ ϕ : arr A[σ] A[τ] ] + | Cofun => [ Δ |- compute_action (dirs Θ) A σ τ ϕ : arr A[τ] A[σ] ] + | Discr => [ Δ |- A[σ] ≅ A[τ] ] + end. + + Let Ptm Θ dt A dA t := forall (wtt: [ Θ |-( dt ) t : A @( dA ) ]), + forall (σ τ: nat -> term) ϕ, [ Δ |- ϕ : σ -( )- τ : Θ ] -> + (let '(t,u,A) := + dispatchDir (dirs Θ) σ τ ϕ A dA t[σ] t[τ] + in termRel Δ t u dt A). + + Let Pconvty Θ d A B := [ Θ |-( d ) A ≅ B ] -> unit. + + Let Pconvtm Θ dt A dA t u := [ Θ |-( dt ) t ≅ u : A @( dA ) ] -> unit. + + Definition DirectedAction : + DirectedDeclarativeTyping.WfDeclInductionConcl Pctx Pty Ptm Pconvty Pconvtm. + Proof. + eapply DirectedDeclarativeTyping.WfDeclInduction. + all: revert Pctx Pty Ptm Pconvty Pconvtm; simpl. + all: try (intros; exact tt). + - (* wfTypeU *) + intros Θ d wfΘ _ wfU σ τ l rel. + cbn. + destruct d. + 1-3: admit. + - (* wfTypeProd *) + intros Θ A dA B dB d wfA IHA wfB IHB maxd wfProd σ τ ϕ rel. + destruct d. + + admit. + + admit. + + admit. + (* constructor. *) (* * eapply typing_subst; tea. *) (* now eapply typing_erased. *) (* admit. *) (* * now trivial. *) (* * admit. *) -(* - (* wfTypeUniv *) *) + - (* wfTypeUniv *) + admit. (* intros Θ d A wtA IHA wfA σ τ l rel. *) (* pose (X := IHA wtA _ _ l rel). *) (* admit. *) @@ -237,16 +68,19 @@ End MorphismDefinition. (* (* eexists. eassumption. *) *) (* (* + inversion X. eapply convUniv. *) *) (* (* exact H. *) *) -(* - (* wfVar *) *) + - (* wfVar *) + admit. (* intros Θ d' n d A dA wfΘ _ inctx dleq wtRel σ τ l rel. *) (* admit. *) -(* - (* wfTermProd *) *) + - (* wfTermProd *) + admit. (* intros Θ d A B wfA IHA wfB IHB wfProd σ τ rel. *) (* destruct d. *) (* + admit. *) (* + admit. *) (* + admit. *) -(* - (* wfTermLam *) *) + - (* wfTermLam *) + admit. (* intros Θ dt dT A B t wfA IHA wfB IHB wtLam σ τ rel. *) (* destruct dT; simpl in *. *) (* + admit. *) @@ -262,14 +96,15 @@ End MorphismDefinition. (* * admit. *) (* * constructor. *) (* admit. *) -(* - (* wfTermApp *) *) + - (* wfTermApp *) + admit. (* intros Θ d dA f a A B wtf IHf wta IHa wtApp σ τ rel. *) (* destruct dA. *) (* + cbn in *. admit. *) (* + admit. *) (* + cbn in *. admit. *) -(* - (* wfTermConv *) *) -(* admit. *) -(* Abort. *) + - (* wfTermConv *) + admit. + Abort. -(* End DirectedAction. *) +End DirectedValid. diff --git a/theories/DirectedTyping.v b/theories/DirectedTyping.v deleted file mode 100644 index 966a812..0000000 --- a/theories/DirectedTyping.v +++ /dev/null @@ -1,342 +0,0 @@ -(** * LogRel.DeclarativeTyping: specification of conversion and typing, in a declarative fashion. *) -From Coq Require Import ssreflect. -From Equations Require Import Equations. -From smpl Require Import Smpl. -From LogRel.AutoSubst Require Import core unscoped Ast Extra. -From LogRel Require Import Utils BasicAst Notations Context DirectedDirections DirectedContext DirectedDirectioning GenericTyping. - -Set Primitive Projections. - -Reserved Notation "[ |-( ) Γ ]" (at level 0, Γ at level 50, only parsing). -Reserved Notation "[ Γ |-( d ) A ]" (at level 0, Γ, d, A at level 50, only parsing). -Reserved Notation "[ Γ |-( dt ) t : A @( dA ) ]" (at level 0, Γ, dt, t, A, dA at level 50, only parsing). -Reserved Notation "[ Γ |-( d ) A ≅ B ]" (at level 0, Γ, d, A, B at level 50, only parsing). -Reserved Notation "[ Γ |-( dt ) t ≅ t' : A @( dA ) ]" (at level 0, Γ, dt, t, t', A, dA at level 50, only parsing). -(* Reserved Notation "[ Γ |-( dt ) t ⤳* u ∈ A @( dA ) ]" (at level 0, Γ, dt, t, u, A, dA at level 50). *) - - -(* I think these should be provable after the fundamental lemma for any - typing judgement sound with respect to the declarative typing *) -Class GenericConsequences `{GP : GenericTypingProperties} := { - wft_ty : forall {Γ A t}, [Γ |- t : A] -> [Γ |- A] -}. - - -Record WfDirectedCtx `{WfContext} (Θ: context) := - { wf_ctx: [ |- List.map ty Θ ] - ; wf_ctx_dir: DirCtx (List.map ty Θ) (List.map dir Θ) (List.map ty_dir Θ) - }. -Notation "[ |-( ) Θ ]" := (WfDirectedCtx Θ). - -Record WfType `{WfType} (Θ: context) (d: direction) (A: term) := - { wft: [ List.map ty Θ |- A ] - ; wft_ctx_dir: DirCtx (List.map ty Θ) (List.map dir Θ) (List.map ty_dir Θ) - ; wft_dir: [ List.map dir Θ |- A ◃ d ] - }. -Notation "[ Θ |-( d ) A ]" := (WfType Θ d A). - -Record Typing `{Typing} (Θ: context) (dt: direction) (T: term) (dT: direction) (t: term) := - { wt: [ List.map ty Θ |- t : T ] - ; wt_ctx_dir: DirCtx (List.map ty Θ) (List.map dir Θ) (List.map ty_dir Θ) - ; wt_dir: [ List.map dir Θ |- t ◃ dt ] - ; wt_ty_dir: [ List.map dir Θ |- T ◃ dT ] - }. -Notation "[ Γ |-( dt ) t : T @( dT ) ]" := (Typing Γ dt T dT t). - - -Section DirectedTypingLemmas. - -Context `{GP:GenericTypingProperties}. - (* `{!WfContext ta} `{!WfType ta} `{!Typing ta} - `{!ConvType ta} `{!ConvTerm ta} `{!ConvNeuConv ta} - `{!RedType ta} `{!RedTerm ta} - `{!GenericTypingProperties ta _ _ _ _ _ _ _ _ _ _}. *) - -Lemma wfCtxEmpty : [|-() εᵈ ]. -Proof. - constructor; cbn; [| constructor]; gen_typing. -Qed. - -Lemma wfCtxCons {Θ d A dA} : [|-() Θ] -> [Θ |-(dA) A] -> [|-() Θ ,, d \ A @ dA]. -Proof. - intros [] []; split; [now eapply wfc_cons| now econstructor]. -Qed. - -Lemma wfCtxWfType {Θ d A} : [ Θ |-( d ) A ] -> [ |-( ) Θ ]. -Proof. - intros []; econstructor; tea; now eapply wfc_wft. -Qed. - -(* TODO: note that I prove rules using naming convention from DeclarativeTyping *) -Lemma wfTypeU {Θ d} : [ |-( ) Θ ] -> [ Θ |-( d ) U ]. -Proof. - intros []. - constructor; tea. - - now apply wft_U. - - now apply dirU'. -Qed. - - -Lemma wfTypeProd {Γ d} {A B} : - [ Γ |-( dir_op d ) A ] -> - [Γ ,, Discr \ A @ dir_op d |-( d ) B ] -> - [ Γ |-( d ) tProd A B ]. -Proof. - intros [] []. - constructor; tea. - - now apply wft_prod. - - now apply dirProd'. -Qed. - -Lemma wfTemWfType `{!GenericConsequences (GP:=GP)} {Θ T dT t dt} : [Θ |-(dt) t : T @(dT) ] -> [Θ |-(dT) T]. -Proof. - intros []; econstructor; tea. now eapply wft_ty. -Qed. - -Lemma wfTypeUniv {Θ d dU} {A} : - [ Θ |-( d ) A : U @( dU ) ] -> - [ Θ |-( d ) A ]. -Proof. - intros []. - constructor; tea. - now apply wft_term. -Qed. - -Corollary wfTypeUnivDiscr {Θ d} {A} : - [ Θ |-( d ) A : U @( Discr ) ] -> - [ Θ |-( d ) A ]. -Proof. - apply wfTypeUniv. -Qed. - - -Lemma in_ctx_erased {Θ n} decl : - in_ctx Θ n decl -> in_ctx (tys Θ) n (ty decl). -Proof. - induction 1; now constructor. -Qed. - -Lemma in_ctx_nth_dir {Θ n} decl : - in_ctx Θ n decl -> List.nth_error (list_map dir Θ) n = Some (dir decl). -Proof. - induction 1; tea. - reflexivity. -Qed. - -Lemma in_ctx_nth_ty_dir {Θ n} decl : - in_ctx Θ n decl -> List.nth_error (list_map ty_dir Θ) n = Some (ty_dir decl). -Proof. - induction 1; tea. - reflexivity. -Qed. - -Lemma wfTermVar {Θ d'} {n d T dT} : - [ |-( ) Θ ] -> - in_ctx Θ n (d \ T @ dT) -> - dir_leq d d' -> - [ Θ |-( d' ) tRel n : T @( dT ) ]. -Proof. - intros [] inΘ leq. - split; tea. - - apply ty_var; tea. - now apply (in_ctx_erased (d \ T @ dT)). - - eapply dirVar'; tea. - now apply (in_ctx_nth_dir (d \ T @ dT)). - - eapply dir_ctx_nth_ty; tea. - + now apply (in_ctx_erased (d \ T @ dT)). - + now apply (in_ctx_nth_ty_dir (d \ T @ dT)). -Qed. - -Lemma wfTermProd {Θ d dU} {A B} : - [ Θ |-( dir_op d ) A : U @( dU ) ] -> - [ Θ ,, Discr \ A @ dir_op d |-( d ) B : U @( dU ) ] -> - [ Θ |-( d ) tProd A B : U @( dU ) ]. -Proof. - intros [] []. - split; tea. - - now apply ty_prod. - - now apply dirProd'. -Qed. - -Corollary wfTermProdDiscr {Θ d} {A B} : - [ Θ |-( dir_op d ) A : U @( Discr ) ] -> - [ Θ ,, Discr \ A @ dir_op d |-( d ) B : U @( Discr ) ] -> - [ Θ |-( d ) tProd A B : U @( Discr ) ]. -Proof. apply wfTermProd. Qed. - - -Lemma wfTermLam {Θ d} {dT A B t} : - [ Θ |-( dir_op dT ) A ] -> - [ Θ ,, Discr \ A @ dir_op dT |-( d ) t : B @( dT ) ] -> - [ Θ |-( d ) tLambda A t : tProd A B @( dT ) ]. -Proof. - intros [] []. - split; tea. - - now apply ty_lam. - - now apply dirLam'. - - now apply dirProd'. -Qed. - -Lemma wfTermApp {Θ d} {dT f a A B} : - [ Θ |-( d ) f : tProd A B @( dT ) ] -> - [ Θ |-( Discr ) a : A @( dir_op dT ) ] -> - [ Θ |-( d ) tApp f a : B[a..] @( dT ) ]. -Proof. - intros [? ? ? [d' [infProd leq]]] []. - split; tea. - - now eapply ty_app. - - now apply dirApp'. - - eapply dir_subst1; tea. - inversion infProd ; subst. - repeat econstructor; tea. - etransitivity; tea. - now eapply MaxDirProp.upper_bound2. -Qed. - - -(** More derived typing lemmas *) - -Lemma wfCtxCons' {Θ d A dA} : [|-() Θ] -> ([|-() Θ] -> [Θ |-(dA) A]) -> [|-() Θ ,, d \ A @ dA]. -Proof. - intros hΘ hA; exact (wfCtxCons hΘ (hA hΘ)). -Qed. - -Lemma wfTypeProd' {Γ d} {A B} : - [ Γ |-( dir_op d ) A ] -> - ( [|-() Γ ,, Discr \ A @ dir_op d] -> - [ Γ |-( dir_op d ) A ] -> - [Γ ,, Discr \ A @ dir_op d |-( d ) B ]) -> - [ Γ |-( d ) tProd A B ]. -Proof. - intros hA hB. - apply wfTypeProd; tea. - apply hB; tea. - apply wfCtxCons; tea. - now eapply wfCtxWfType. -Qed. - -Fixpoint shift_n {A} `{Ren1 (nat -> nat) A A} (t : A) n := match n with 0 => t | S m => (shift_n t m)⟨↑⟩ end. - -Lemma wfTypeVar {Θ n d d' dU} : - [ |-( ) Θ ] -> - in_ctx Θ n (shift_n (d \ U @ dU) n) -> - dir_leq d d' -> - [ Θ |-( d' ) tRel n ]. -Proof. - assert (h : forall k, shift_n (d \ U @ dU) k = (d \ U @ dU)). - by (intros k; induction k as [| ? ih]; cbn; rewrite ?ih; reflexivity). - rewrite h. - intros. - eapply wfTypeUniv. - now eapply wfTermVar. -Qed. - - -End DirectedTypingLemmas. - -Module Examples. - - Module List. - - (* Context of parameters for list *) - Definition ctx := εᵈ ,, Fun \ U @ Discr. - (* Context of arguments for nil; - the parameters of list should form a prefix *) - Definition nil_ctx := ctx. - (* Not sure how we will represent inductive occurences - of the inductive being defined so I abstract that - as an arbitrary function tList taking |ctx| arguments of type term - and producing a term for now *) - Definition cons_ctx (tList : term -> term) := ctx,, Discr \ tRel 0 @ Fun,, Discr \ tList (tRel 1) @ Fun. - - Section ListTyping. - Context `{GenericConsequences}. - - Lemma ctxWfCtx : [|-() ctx ]. - Proof. - eapply wfCtxCons'; [apply wfCtxEmpty |intros; now apply wfTypeU]. - Qed. - - Lemma nil_ctxWfCtx : [|-() nil_ctx ]. - Proof. - apply ctxWfCtx. - Qed. - - Lemma cons_ctxWfCtx - (tList : term -> term) - (ih : forall Θ A, [Θ |-(Fun) A] -> [Θ |-(Fun) tList A]) : - [|-() cons_ctx tList ]. - Proof. - apply wfCtxCons'; [apply wfCtxCons'|]; intros. - - apply ctxWfCtx. - - eapply wfTypeVar; tea; [econstructor| reflexivity]. - - eapply ih. - eapply wfTypeVar; tea. - 2: reflexivity. - do 2 econstructor. - Qed. - - End ListTyping. - End List. - - - Module W. - - Definition ctx := εᵈ ,, Fun \ U @ Discr ,, Cofun \ tProd (tRel 0) U @ Cofun. - - [ Θ |-(Fun) A ] - [ Θ ,, Discr \ A @ Fun |-(Cofun) B ] - - Definition sup_ctx - (* tW should bind one variable in its second argument *) - (tW : term -> term -> term) := - ctx ,, Discr \ tRel 1 @ Fun ,, Discr \ tProd (tApp (tRel 1) (tRel 0)) (tW (tRel 3) (tApp (tRel 3) (tRel 0))) @ Fun. - - Section WTyping. - Context `{GenericConsequences}. - - Lemma ctxWfCtx : [|-() ctx ]. - Proof. - eapply wfCtxCons'; [eapply wfCtxCons'|]; try apply wfCtxEmpty; intros. - - now apply wfTypeU. - - apply wfTypeProd'. - + eapply wfTypeVar; tea; [econstructor| reflexivity]. - + intros; now eapply wfTypeU. - Qed. - - Lemma supWfCtx (tW : term -> term -> term) - (ih : forall Θ A B, - [Θ |-(Fun) A] -> - [Θ ,, Discr \ A @ Fun |-(Cofun) B ] -> - [Θ |-(Fun) tW A B]) : - [|-() sup_ctx tW ]. - Proof. - eapply wfCtxCons'; [eapply wfCtxCons'|]; try apply ctxWfCtx; intros. - 1: eapply wfTypeVar; tea; [do 2 econstructor|reflexivity]. - eapply wfTypeProd'; intros. - + eapply (wfTypeUniv (dU:=Cofun)). - change U with (U[(tRel 0)..]). - eapply (wfTermApp (A:=(tRel 2))). - 1,2: eapply wfTermVar; tea; try reflexivity. - 2: econstructor. - change (?d \ tProd _ _ @ ?dT) with (shift_n (d \ tProd (tRel 0) U @ dT) 2). - do 2 econstructor. - + set (ctx' := _,, _ ,, _). - assert [ctx' |-(Fun) tRel 3]. - 1:{ eapply wfTypeVar; tea; try reflexivity; repeat econstructor. } - assert [|-() ctx' ,, Discr \ tRel 3 @ Fun] by now eapply wfCtxCons. - apply ih; tea. - eapply (wfTypeUniv (dU:=Cofun)). - change U with (U[(tRel 0)..]); eapply (wfTermApp (A:=(tRel 4))). - 1,2: eapply wfTermVar; tea; try reflexivity. - 2: econstructor. - change (?d \ tProd _ _ @ ?dT) with (shift_n (d \ tProd (tRel 1) U @ dT) 3). - repeat econstructor. - Qed. - - End WTyping. - End W. - -End Examples. - -