From 647865fa8f9aa5267584365bae9b55ce2376df87 Mon Sep 17 00:00:00 2001 From: Meven Date: Tue, 11 Jul 2023 13:49:05 +0100 Subject: [PATCH] documentation and clean-up --- README.md | 59 +----- _CoqProject | 3 +- docs/index.md | 155 +++++++++++---- theories/AlgorithmicTypingProperties.v | 15 +- theories/BundledAlgorithmicTyping.v | 2 + theories/Decidability/Completeness.v | 14 +- theories/DeclarativeInstance.v | 2 +- theories/LogicalRelation/Neutral.v | 18 -- theories/LogicalRelation/Weakening.v | 2 +- theories/Normalisation.v | 6 +- theories/Substitution/Introductions/Pi.v | 2 +- theories/Substitution/Introductions/Poly.v | 2 +- theories/Substitution/Introductions/Sigma.v | 2 +- theories/Substitution/Properties.v | 2 +- theories/TypeUniqueness.v | 57 +----- theories/UntypedValues.v | 204 -------------------- theories/mapPiSigmaFunctorLaws.v | 2 +- 17 files changed, 153 insertions(+), 394 deletions(-) delete mode 100644 theories/UntypedValues.v diff --git a/README.md b/README.md index c96e258..3df8966 100644 --- a/README.md +++ b/README.md @@ -1,66 +1,25 @@ Presentation ======= -This repo contains formalisation work on implementing a logical relation over MLTT with one universe. -This formalisation follows the [work done by Abel et al.]((https://github.com/mr-ohman/logrel-mltt/)) (described in [Decidability of conversion for Type Theory in Type Theory, 2018](https://dl.acm.org/doi/10.1145/3158111)), and [Loïc Pujet's work](https://github.com/loic-p/logrel-mltt) on removing induction-recursion from the previous formalization, making it feasible to translate it from Agda to Coq. +This repo contains the formalisation work accompangy the paper *Definitional Functoriality for Dependent (Sub)Types*. -The definition of the logical relation (**LR**) ressembles Loïc's in many ways, but also had to be modified for a few reasons : -- Because of universe constraints and the fact that functors cannot be indexed by terms in Coq whereas it is possible in Agda, the relevant structures had to be parametrized by a type level and a recursor, and the module system had to be dropped out entirely. -- Since Coq and Agda's positivity checking for inductive types is different, it turns out that **LR**'s definition, even though it does not use any induction-induction or induction-recursion in Agda, is not accepted in Coq. As such, the predicate over Π-types for **LR** has been modified compared to Agda. You can find a MWE of the difference in positivity checking in the two systems in [Positivity.v] and [Positivity.agda]. - -In order to avoid some work on the syntax, this project uses the [AutoSubst](https://github.com/uds-psl/autosubst-ocaml) project to generate syntax-related boilerplate. +The formalisation follows a similar [Agda formalization]((https://github.com/mr-ohman/logrel-mltt/)) (described in [*Decidability of conversion for Type Theory in Type Theory*, 2018](https://dl.acm.org/doi/10.1145/3158111)). In order to avoid some work on the syntax, this project uses the [AutoSubst](https://github.com/uds-psl/autosubst-ocaml) project to generate syntax-related boilerplate. It also includes code from Winterhalter's [partial-fun](https://github.com/TheoWinterhalter/coq-partialfun) library to handle the definition of partial functions. Building =========== -The project builds with Coq version `8.16.1`. It needs the opam package `coq-smpl`. Once these have been installed, you can simply issue `make` in the root folder. - -The syntax has been generated using AutoSubst OCaml with the options `-s ucoq -v ge813 -allfv` (see the [AutoSubst OCaml documentation](https://github.com/uds-psl/autosubst-ocaml) for installation instructions for it). Currently, this package works only with older version of Coq (8.13), so we cannot add a recipe to the MakeFile for automatically -re-generating the syntax. +The project builds with Coq version `8.16.1`. It needs the opam package `coq-smpl`. Once these have been installed, you can simply issue `make` in the root folder. Apart from a few harmless warnings, the build should report on the assumptions of our main theorems: +- `typing_SN` in [Normalisation](./theories/Normalisation.v), states that reduction on well-typed terms is (strongly) normalizing; this is phrased in a constructively acceptable way, as accessibility of every well-typed term under reduction, i.e. as well-foundation of the reduction relation. +- `algo_typing_sound` in [BundledAlgorithmicTyping](./theories/BundledAlgorithmicTyping.v) says that algorithmic typing (assuming its inputs are well-formed), is sound with respect to declarative typing, and `algo_typing_complete` in [AlgorithmicTypingProperties](./theories/AlgorithmicTypingProperties.v) says that it is complete. +- `check_full` in file [Decidability](./theories/Decidability.v), says that typing is decidable. -**In order to regenerate the syntax**, install autosubst paying attention to [this issue](https://github.com/uds-psl/autosubst-ocaml/issues/1) -- in an opam installation do a `cp -R $OPAM_SWITCH_PREFIX/share/coq-autosubst-ocaml $OPAM_SWITCH_PREFIX/share/autosubst`--, modify the syntax file `AutoSubst/PiUniv.sig`, run autosubst on it (`autosubst -s ucoq -v ge813 -allfv PiUniv.sig -o Ast.v`) and patch the resulting files using the checked in patch (`git apply -R autosubst-patch.diff`). +The first three are axiom-free, while `check_full` +only requires a dependently-typed version of the function extensionality axiom. This harmless axiom is introduced by Equations for the definition of the functions. Browsing the Development ================== -The development, rendered using `coqdoc`, can be [browsed online](https://coqhott.github.io/logrel-coq/coqdoc/toc.html). - -Getting Started -================= - -A few things to get accustomed to if you want to use the development. - -Notations and refolding ------------ - -In a style somewhat similar to the [Math Classes](https://math-classes.github.io/) project, -generic notations for typing, conversion, renaming, etc. are implemented using type-classes. -While some care has been taken to try and respect the abstractions on which the notations are -based, they might still be broken by carefree reduction performed by tactics. In this case, -the `refold` tactic can be used, as the name suggests, to refold all lost notations. - -Induction principles ----------- - -The development relies on large, mutually-defined inductive relations. To make proofs by induction -more tractable, functions `XXXInductionConcl` are provided. These take the predicates -to be mutually proven, and construct the type of the conclusion of a proof by mutual induction. -Thus, a typical induction proof looks like the following: - -``` coq-lang -Section Foo. - -Let P := … . -… - -Theorem Foo : XXXInductionConcl P … . -Proof. - apply XXXInduction. - -End Section. -``` -The names of the arguments printed when querying `About XXXInductionConcl` should make it clear -to which mutually-defined relation each predicate corresponds. +The development, rendered using the [coqdoc](https://coq.inria.fr/refman/using/tools/coqdoc.html) utility, can be generated using `make coqdoc`, and then browed offline (as html files). To start navigating the sources, the best entry point is probably the [the table of content](./docs/coqdoc/toc.html). A [short description of the file contents](./docs/index.md) is also provided to make the navigation easier. [Utils]: ./theories/Utils.v [BasicAst]: ./theories/BasicAst.v diff --git a/_CoqProject b/_CoqProject index f901515..cb00325 100644 --- a/_CoqProject +++ b/_CoqProject @@ -17,7 +17,6 @@ theories/Notations.v theories/NormalForms.v theories/Weakening.v theories/UntypedReduction.v -theories/UntypedValues.v theories/GenericTyping.v theories/DeclarativeTyping.v @@ -59,10 +58,10 @@ theories/Substitution/Introductions/Sigma.v theories/Substitution/Introductions/List.v theories/Fundamental.v -theories/AlgorithmicTyping.v theories/DeclarativeSubst.v theories/TypeConstructorsInj.v theories/Normalisation.v +theories/AlgorithmicTyping.v theories/BundledAlgorithmicTyping.v theories/AlgorithmicConvProperties.v theories/AlgorithmicTypingProperties.v diff --git a/docs/index.md b/docs/index.md index 03297fa..29829a3 100644 --- a/docs/index.md +++ b/docs/index.md @@ -1,13 +1,31 @@ Browsing the sources ============================ -The table of content of the development is accessible [here](https://coqhott.github.io/logrel-coq/coqdoc/toc.html). +The table of content of the development is accessible [here](./coqdoc/toc.html). File description ========== To complement it, here is a rough description of the content of every file. +Partial functions library ([coq-partialfun folder](../coq-partialfun/theories)) +---------------- +This part of the repository is due to [Winterhalter](https://github.com/TheoWinterhalter/coq-partialfun), +we simply reproduce it here with minimal changes in the absence of an opam package. + +| File | Description | +|---|----| +| [Monad] | Monad and the error monad transformer, with notations. +| [PartialFun] | Support for the definition of potentially non-terminating recursive functions. +| Examples | Simple usage examples of the library. + +Miscellaneous +--------- + +| File | Description | +|---|----| +[mapPiSigmaFunctorLaws] | Shows that `mapΠ` and `mapΣ` are definable in Coq and satisfy the definitional functor laws. + Utilities and AST --------- @@ -18,7 +36,7 @@ Utilities and AST [AutoSubst/] | Abstract syntax tree, renamings, substitutions and many lemmas, generated using the [autosubst-ocaml] opam package. [AutoSubst/Extra] | Extra instances, notations and tactics to better handle the boilerplate generated by AutoSubst. [Notations] | Notations used throughout the development. It can be used as an index for notations! -[NormalForms] | Definition of normal and neutral forms, and properties. | +[NormalForms] | Definition of normal and neutral forms, and properties. Common typing-related definitions ------- @@ -27,7 +45,7 @@ Common typing-related definitions |---|----| [Context] | Definition of contexts and operations on them. [Weakening] | Definition of a well-formed weakening, and some properties. -[UntypedReduction] | Definiton and basic properties of untyped reduction, used to define algorithmic typing. +[UntypedReduction] | Definiton and basic properties of (untyped) reduction, used to define algorithmic typing and the logical relation. [GenericTyping] | A generic notion of typing, used to define the logical relation, to be instantiated three times: once with the fully declarative version, once with the mixed declarative and algorithmic one, and once with the fully algorithmic one. Declarative typing and its properties @@ -43,57 +61,110 @@ Logical relation and its properties | File | Description | |---|----| -[LogicalRelation] | Contains the logical relation's (**LR**) definition. | -[Induction] | Defines the induction principles over **LR**. Because of universe constraints, **LR** needs two induction principles, one for each type levels. | -[Escape] | Contains a proof of the escape lemma for **LR** | +[LogicalRelation] | Contains the logical relation's definition. | +[Induction] | Defines the induction principles for the logical relation. These are manual hand-crafted induction principles, that suit our needs better than the ones automatically generated by Coq. | +[Escape] | The escape lemma for the logical relation says that predicates in the logical relation imply their generic typing counterparts: a reducible type is a well-formed type, reducibly convertible terms are convertible, etc. | [ShapeView] | Technique to avoid considering non-diagonal cases for two reducibly convertible types. | -[Reflexivity] | Reflexivity of the logical relation. -[Irrelevance] | Irrelevance of the logical relation: two reducibly convertible types decode to equivalent predicates. Symmetry is a direct corollary. | +[LogicalRelation.Reflexivity] | Reflexivity of the logical relation. +[LogicalRelation.Irrelevance] | Irrelevance of the logical relation: two reducibly convertible types decode to equivalent predicates. Symmetry is a direct corollary. | +[Weakening] | Stability of the logical relation under weakening | +[Universe] | The universe is reducible | +[Neutral] | Well-typed neutrals are reducible at any type. | +[Transitivity] | The logical relation is transitive. | +[Reduction] | Reducible terms and types are stable under anti-reduction and reduction to weak-head normal form, and reduction of reducible terms/types in included in reducible conversion. | +[NormalRed] | Normalization of the proof-relevant components of proofs of reducibility. | +[Application] | Function application is reducible. | +[SimpleArr] | Non-dependent function types are reducible. | +[Validity] | Definition of **validity**: free closure of the logical relation under reducible substitution, necessary to handle the interaction of reducibility and binders. | +[Substitution.Irrelevance] | Irrelevance of validity. | +[Substitution.Properties] | Interaction of validity with context/substitution operations: weakening, extension, etc. | +[Substitution.Escape] | Escape for validity. | +[Substitution.Conversion] | Stability of validity by conversion. | +[Substitution.Reflexivity] | Reflexivity of validity. | +[Substitution.Reduction] | Stability of validity under reduction. | +[SingleSubst] | Recovering properties of unary substitution from those of n-ary substitution. | +[Substitution.Introductions.*] | Reducibilty of the various term- and type-formers. | +[Fundamental] | Fundamental lemma : every typable term is reducible. Combines most of the development above. | + Algorithmic typing and its properties ----------------- | File | Description | |---|----| +[DeclarativeSubst] | Consequence of the logical relation: declarative typing is stable under substitution. +[TypeConstructorsInj] | Consequence of the logical relation: type constructors are injective, and two different type constructors cannot be convertible (no-confusion). Many consequences, including subject reduction. +[Normalisation] | Consequence of the logical relation: well-typed terms always reduce to a normal form. [AlgorithmicTyping] | Definition of the second notion of typing: algorithmic typing (and algorithmic conversion together with it). -[LogRelConsequences] | Consequences of the logical relation on declarative typing necessary to establish properties of algorithmic typing. [BundledAlgorithmicTyping] | Algorithmic typing bundled with its pre-conditions, and a tailored induction principle showing invariant preservation in the "algorithm". -[AlgorithmicConvProperties] | Properties of algorithmic conversion, in order to derive the second instance of generic typing, consisting of declarative typing and algorithmic conversion. | -[AlgorithmicTypingProperties] | Derive the third instance of generic typing, consisting entierly of algorithmic notions. | +[AlgorithmicConvProperties] | Properties of algorithmic conversion, in order to derive the second instance of generic typing, consisting of declarative typing and algorithmic conversion, and completeness of algorithmic conversion. | +[AlgorithmicTypingProperties] | Derive the third instance of generic typing, consisting entierly of algorithmic notions, and completeness of algorithmic typing. | -Miscellaneous ------------ +Decidability results +--------------- | File | Description | |---|----| -| [Positivity.v] and [Positivity.agda] | Showcase the difference between Coq and Agda's positivity checkers. | +[Functions] | Definition of the evaluation abstract machine, conversion checking and type-checking programs. Independent of the meta-theory: they are written in a monadic style with recursive call as a free effect. +[Soundness] | The functions are sound: when they succeed, their answer is correct, e.g. the term is typable. +[Completeness] | The functions are complete: they always return successfully when they should. +[Termination] | The functions always terminate. +[Decidability] | Top-level pure decision procedure for typing. + + +[Monad]: ../coq-partialfun/theories/Monad.v +[PartialFun]: ../coq-partialfun/theories/PartialFun.v +[Examples]: ../coq-partialfun/theories/Examples.v -[Utils]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.Utils.html -[BasicAst]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.BasicAst.html -[Context]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.Context.html +[mapPiSigmaFunctorLaws]: ./coqdoc/LogRel.mapPiSigmaFunctorLaws.html +[Utils]: ./coqdoc/LogRel.Utils.html +[BasicAst]: ./coqdoc/LogRel.BasicAst.html +[Context]: ./coqdoc/LogRel.Context.html [AutoSubst/]: ./theories/AutoSubst/ -[AutoSubst/Extra]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.AutoSubst.Extra.html -[Notations]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.Notations.html -[Automation]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.Automation.html -[NormalForms]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.NormalForms.html -[UntypedReduction]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.UntypedReduction.html -[GenericTyping]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.GenericTyping.html -[DeclarativeTyping]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.DeclarativeTyping.html -[Properties]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.Properties.html -[DeclarativeInstance]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.DeclarativeInstance.html -[LogicalRelation]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.LogicalRelation.html -[Induction]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.LogicalRelation.Induction.html -[Escape]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.LogicalRelation.Escape.html -[Reflexivity]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.LogicalRelation.Reflexivity.html -[Irrelevance]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.LogicalRelation.Irrelevance.html -[ShapeView]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.LogicalRelation.ShapeView.html -[Positivity.v]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.Positivity.html -[Weakening]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.Weakening.html -[AlgorithmicTyping]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.AlgorithmicTyping.html -[AlgorithmicConvProperties]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.AlgorithmicConvProperties.html -[AlgorithmicTypingProperties]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.AlgorithmicTypingProperties.html -[LogRelConsequences]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.LogRelConsequences.html -[BundledAlgorithmicTyping]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.BundledAlgorithmicTyping.html - -[autosubst-ocaml]: https://github.com/uds-psl/autosubst-ocaml -[Positivity.agda]: https://coqhott.github.io/logrel-coq/coqdoc/LogRel.Posit.htmlity.agda \ No newline at end of file +[AutoSubst/Extra]: ./coqdoc/LogRel.AutoSubst.Extra.html +[Notations]: ./coqdoc/LogRel.Notations.html +[NormalForms]: ./coqdoc/LogRel.NormalForms.html +[UntypedReduction]: ./coqdoc/LogRel.UntypedReduction.html +[GenericTyping]: ./coqdoc/LogRel.GenericTyping.html +[DeclarativeTyping]: ./coqdoc/LogRel.DeclarativeTyping.html +[Properties]: ./coqdoc/LogRel.Properties.html +[DeclarativeInstance]: ./coqdoc/LogRel.DeclarativeInstance.html +[LogicalRelation]: ./coqdoc/LogRel.LogicalRelation.html +[Induction]: ./coqdoc/LogRel.LogicalRelation.Induction.html +[Escape]: ./coqdoc/LogRel.LogicalRelation.Escape.html +[LogicalRelation.Reflexivity]: ./coqdoc/LogRel.LogicalRelation.Reflexivity.html +[LogicalRelation.Irrelevance]: ./coqdoc/LogRel.LogicalRelation.Irrelevance.html +[ShapeView]: ./coqdoc/LogRel.LogicalRelation.ShapeView.html +[Universe]: ./coqdoc/LogRel.LogicalRelation.Universe.html +[Neutral]: ./coqdoc/LogRel.LogicalRelation.Neutral.html +[Transitivity]: ./coqdoc/LogRel.LogicalRelation.Transitivity.html +[Reduction]: ./coqdoc/LogRel.LogicalRelation.Reduction.html +[NormalRed]: ./coqdoc/LogRel.LogicalRelation.NormalRed.html +[Application]: ./coqdoc/LogRel.LogicalRelation.Application.html +[SimpleArr]: ./coqdoc/LogRel.LogicalRelation.SimpleArr.html +[Validity]: ./coqdoc/LogRel.Validity.html +[Substitution.Irrelevance]: ./coqdoc/LogRel.Substitution.Irrelevance.html +[Substitution.Properties]: ./coqdoc/LogRel.Substitution.Properties.html +[Substitution.Escape]: ./coqdoc/LogRel.Substitution.Escape.html +[Substitution.Conversion]: ./coqdoc/LogRel.Substitution.Conversion.html +[Substitution.Reflexivity]: ./coqdoc/LogRel.Substitution.Reflexivity.html +[Substitution.Reduction]: ./coqdoc/LogRel.Substitution.Reduction.html +[SingleSubst]: ./coqdoc/LogRel.Substitution.SingleSubst.html +[Substitution.Introductions.*]: ./coqdoc/toc.html +[Fundamental]: ./coqdoc/LogRel.Fundamental.html +[Weakening]: ./coqdoc/LogRel.Weakening.html +[AlgorithmicTyping]: ./coqdoc/LogRel.AlgorithmicTyping.html +[AlgorithmicConvProperties]: ./coqdoc/LogRel.AlgorithmicConvProperties.html +[AlgorithmicTypingProperties]: ./coqdoc/LogRel.AlgorithmicTypingProperties.html +[LogRelConsequences]: ./coqdoc/LogRel.LogRelConsequences.html +[BundledAlgorithmicTyping]: ./coqdoc/LogRel.BundledAlgorithmicTyping.html +[DeclarativeSubst]: ./coqdoc/LogRel.DeclarativeSubst.html +[TypeConstructorsInj]: ./coqdoc/LogRel.TypeConstructorsInj.html +[Normalisation]: ./coqdoc/LogRel.Normalisation.html +[Functions]: ./coqdoc/LogRel.Decidability.Functions.html +[Soundness]: ./coqdoc/LogRel.Decidability.Soundness.html +[Completeness]: ./coqdoc/LogRel.Decidability.Completeness.html +[Termination]: ./coqdoc/LogRel.Decidability.Termination.html +[Decidability]: ./coqdoc/LogRel.Decidability.Decidability.html + +[autosubst-ocaml]: https://github.com/uds-psl/autosubst-ocaml \ No newline at end of file diff --git a/theories/AlgorithmicTypingProperties.v b/theories/AlgorithmicTypingProperties.v index 98eb85f..2e65466 100644 --- a/theories/AlgorithmicTypingProperties.v +++ b/theories/AlgorithmicTypingProperties.v @@ -480,17 +480,4 @@ Proof. + now intros [??? h%algo_conv_sound]. Qed. -(** *** Uniqueness of types *) - -Lemma type_uniqueness Γ A A' t : - [Γ |-[de] t : A] -> - [Γ |-[de] t : A'] -> - [Γ |-[de] A ≅ A']. -Proof. - intros [?? Hinf]%algo_typing_complete [?? Hinf']%algo_typing_complete. - eapply algo_typing_det in Hinf. - 2: eassumption. - subst. - etransitivity ; tea. - now symmetry. -Qed. \ No newline at end of file +Print Assumptions algo_typing_complete. \ No newline at end of file diff --git a/theories/BundledAlgorithmicTyping.v b/theories/BundledAlgorithmicTyping.v index 6c0bffd..c7da3a0 100644 --- a/theories/BundledAlgorithmicTyping.v +++ b/theories/BundledAlgorithmicTyping.v @@ -1724,6 +1724,8 @@ Proof. now eapply algo_typing_sound in Hty. Qed. +Print Assumptions bn_typing_sound. + Corollary inf_conv_decl Γ t A A' : [Γ |-[al] t ▹ A] -> [Γ |-[de] A ≅ A'] -> diff --git a/theories/Decidability/Completeness.v b/theories/Decidability/Completeness.v index a4d18ca..d233fad 100644 --- a/theories/Decidability/Completeness.v +++ b/theories/Decidability/Completeness.v @@ -129,7 +129,7 @@ Proof. eapply typed_zip in Hzip as [A' []]. eexists ; split ; tea. eapply typed_stack_conv_in ; tea. - now eapply typing_unique. + now eapply type_uniqueness. Qed. Corollary typed_zip_cons Γ A t B s π : @@ -171,23 +171,23 @@ Proof. induction π as [|[] π] in A, t, B, Ht, Hπ |- * ; cbn. - easy. - eapply typed_zip_cons in Hπ as [? [(?&[[-> ? Ht']])%termGen']] ; subst ; tea. - unshelve eapply typing_unique, ty_conv_inj in Ht ; last first ; tea. + unshelve eapply type_uniqueness, ty_conv_inj in Ht ; last first ; tea. 2-3: now econstructor. now cbn in *. - eapply typed_zip_cons in Hπ as [? [(?&[[-> ? Ht']])%termGen']] ; subst ; tea. - unshelve eapply typing_unique, ty_conv_inj in Ht ; last first ; tea. + unshelve eapply type_uniqueness, ty_conv_inj in Ht ; last first ; tea. 2-3: now econstructor. now cbn in *. - eapply typed_zip_cons in Hπ as [? [(?&[(?&?&[->])])%termGen']] ; subst ; tea. - unshelve eapply typing_unique, ty_conv_inj in Ht ; last first ; tea. + unshelve eapply type_uniqueness, ty_conv_inj in Ht ; last first ; tea. 2-3: now econstructor. now cbn in *. - eapply typed_zip_cons in Hπ as [? [(?&[(?&?&[->])])%termGen']] ; subst ; tea. - unshelve eapply typing_unique, ty_conv_inj in Ht ; last first ; tea. + unshelve eapply type_uniqueness, ty_conv_inj in Ht ; last first ; tea. 2-3: now econstructor. now cbn in *. - eapply typed_zip_cons in Hπ as [? [(?&[(?&?&[->])])%termGen']] ; subst ; tea. - unshelve eapply typing_unique, ty_conv_inj in Ht ; last first ; tea. + unshelve eapply type_uniqueness, ty_conv_inj in Ht ; last first ; tea. 2-3: now econstructor. now cbn in *. - eapply typed_zip_cons in Hπ as [? [[? [[] Hconv]]%termGen' Hstack]] ; subst ; tea. @@ -231,7 +231,7 @@ Proof. pose proof Hty as [? [(?&[->]&?)%termGen' ?]]%typed_zip_cons ; tea. eapply list_stack_ismap. 2: eapply typed_stack_conv_in ; tea. - 2: now eapply typing_unique. + 2: now eapply type_uniqueness. eassumption. Qed. diff --git a/theories/DeclarativeInstance.v b/theories/DeclarativeInstance.v index adb886e..ec34d97 100644 --- a/theories/DeclarativeInstance.v +++ b/theories/DeclarativeInstance.v @@ -1,7 +1,7 @@ (** * LogRel.DeclarativeInstance: proof that declarative typing is an instance of generic typing. *) From Coq Require Import CRelationClasses. From LogRel.AutoSubst Require Import core unscoped Ast Extra. -From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedReduction UntypedValues Weakening GenericTyping DeclarativeTyping. +From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedReduction Weakening GenericTyping DeclarativeTyping. Import DeclarativeTypingData. diff --git a/theories/LogicalRelation/Neutral.v b/theories/LogicalRelation/Neutral.v index 9211242..ff1e8bd 100644 --- a/theories/LogicalRelation/Neutral.v +++ b/theories/LogicalRelation/Neutral.v @@ -66,24 +66,6 @@ Proof. gen_typing. Qed. -(* Lemma convneu_app_ren_var {Γ A f g dom cod} : - [Γ |- f ~ g : A] -> - [Γ |- A ≅ tProd dom cod] -> - [Γ ,, dom |- tRel 0 ≅ tRel 0 : dom⟨↑⟩] -> - [Γ ,, dom |- tApp f⟨↑⟩ (tRel 0) ~ tApp g⟨↑⟩ (tRel 0) : cod]. -Proof. - intros Hf HA Hrel. - erewrite <- wk1_ren_on. - eapply convne_meta_conv. - - eapply convneu_app_ren ; tea. - now rewrite wk1_ren_on. - - replace cod[_] with (cod[(0 .: ↑) >> tRel]) by now bsimpl. - renamify. - rewrite scons_eta_id'. - now bsimpl. - - now bsimpl. -Qed. *) - Record complete {l Γ A} (RA : [Γ ||- A]) := { reflect : forall n n', [Γ |- n : A] -> diff --git a/theories/LogicalRelation/Weakening.v b/theories/LogicalRelation/Weakening.v index 15b2711..21575a4 100644 --- a/theories/LogicalRelation/Weakening.v +++ b/theories/LogicalRelation/Weakening.v @@ -1,6 +1,6 @@ From Coq Require Import ssrbool. From LogRel.AutoSubst Require Import core unscoped Ast Extra. -From LogRel Require Import Notations Utils BasicAst Context NormalForms UntypedValues Weakening GenericTyping LogicalRelation. +From LogRel Require Import Notations Utils BasicAst Context NormalForms Weakening GenericTyping LogicalRelation. From LogRel.LogicalRelation Require Import Induction Irrelevance. Set Universe Polymorphism. diff --git a/theories/Normalisation.v b/theories/Normalisation.v index 2367737..872147e 100644 --- a/theories/Normalisation.v +++ b/theories/Normalisation.v @@ -3,7 +3,7 @@ From Coq Require Import CRelationClasses. From LogRel.AutoSubst Require Import core unscoped Ast Extra. From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening UntypedReduction GenericTyping DeclarativeTyping DeclarativeInstance AlgorithmicTyping. -From LogRel Require Import LogicalRelation UntypedValues Validity Fundamental. +From LogRel Require Import LogicalRelation Validity Fundamental. From LogRel.LogicalRelation Require Import Escape Neutral Induction ShapeView Reflexivity. From LogRel.Substitution Require Import Escape Poly. @@ -185,7 +185,7 @@ End Normalisation. Import DeclarativeTypingProperties. -Corollary typing_nf_alt {Γ t} : well_formed Γ t -> WN t. +Corollary typing_nf_alt {Γ t} : well_formed Γ t -> WN t. Proof. intros [[] Hty]. all: first [apply TypeRefl in Hty|apply TermRefl in Hty]. @@ -224,6 +224,8 @@ Proof. eapply WN_exp; [tea|]; now apply WN_whnf. Qed. +Print Assumptions typing_SN. + Section NeutralConversion. Import AlgorithmicTypingData. diff --git a/theories/Substitution/Introductions/Pi.v b/theories/Substitution/Introductions/Pi.v index d77c918..44353be 100644 --- a/theories/Substitution/Introductions/Pi.v +++ b/theories/Substitution/Introductions/Pi.v @@ -1,6 +1,6 @@ From Coq Require Import ssrbool. From LogRel.AutoSubst Require Import core unscoped Ast Extra. -From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedValues Weakening +From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening GenericTyping LogicalRelation Validity. From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance. From LogRel.Substitution Require Import Irrelevance Properties. diff --git a/theories/Substitution/Introductions/Poly.v b/theories/Substitution/Introductions/Poly.v index 8601611..57c62cf 100644 --- a/theories/Substitution/Introductions/Poly.v +++ b/theories/Substitution/Introductions/Poly.v @@ -1,6 +1,6 @@ From Coq Require Import ssrbool. From LogRel.AutoSubst Require Import core unscoped Ast Extra. -From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedValues Weakening +From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening GenericTyping LogicalRelation Validity. From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance. From LogRel.Substitution Require Import Irrelevance Properties. diff --git a/theories/Substitution/Introductions/Sigma.v b/theories/Substitution/Introductions/Sigma.v index 7f634b0..deab888 100644 --- a/theories/Substitution/Introductions/Sigma.v +++ b/theories/Substitution/Introductions/Sigma.v @@ -1,6 +1,6 @@ From Coq Require Import ssrbool. From LogRel.AutoSubst Require Import core unscoped Ast Extra. -From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedValues Weakening +From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening GenericTyping LogicalRelation Validity. From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Reduction NormalRed Induction Transitivity. From LogRel.Substitution Require Import Irrelevance Properties SingleSubst Reflexivity. diff --git a/theories/Substitution/Properties.v b/theories/Substitution/Properties.v index 9655dc5..ccaaf4d 100644 --- a/theories/Substitution/Properties.v +++ b/theories/Substitution/Properties.v @@ -1,5 +1,5 @@ From LogRel.AutoSubst Require Import core unscoped Ast Extra. -From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedValues Weakening GenericTyping LogicalRelation Validity. +From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening GenericTyping LogicalRelation Validity. From LogRel.LogicalRelation Require Import Irrelevance Escape Reflexivity Weakening Neutral Induction. From LogRel.Substitution Require Import Irrelevance. diff --git a/theories/TypeUniqueness.v b/theories/TypeUniqueness.v index bfa9d26..07464c5 100644 --- a/theories/TypeUniqueness.v +++ b/theories/TypeUniqueness.v @@ -6,54 +6,15 @@ From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakenin Import DeclarativeTypingProperties AlgorithmicTypingData BundledTypingData AlgorithmicTypingProperties. -Section AlgorithmicUnique. - - Lemma algo_typing_unique : AlgoTypingInductionConcl - (fun Γ A => True) - (fun Γ A t => forall A', [Γ |-[al] t ▹ A'] -> A' = A) - (fun Γ A t => forall A', [Γ |-[al] t ▹h A'] -> ∑ A'', [A'' ⇒* A] × [A'' ⇒* A']) - (fun Γ A t => True). - Proof. - apply AlgoTypingInduction. - all: try easy. - all: try solve [intros ** ; match goal with H : context [al] |- _ => now inversion H end]. - - intros * ? * Hty'. - inversion Hty' ; subst. - now eapply in_ctx_inj. - - intros * _ _ _ IHt ? Hty'. - inversion Hty' ; subst ; refold. - now erewrite <- IHt. - - intros * _ IHf _ _ ? Hty'. - inversion Hty' ; subst ; refold. - eapply IHf in H3 as [? [Hred Hred']]. - eapply whred_det in Hred ; tea. - 2-3: gen_typing. - now inversion Hred. - - intros * ? ih ? hty. - inversion hty; subst; refold. - edestruct ih as [? [r r']]; tea. - unshelve epose (e := whred_det _ _ _ _ _ r r'); try constructor. - now injection e. - - intros * ? ih ? hty. - inversion hty; subst; refold. - edestruct ih as [? [r r']]; tea. - unshelve epose (e := whred_det _ _ _ _ _ r r'); try constructor. - injection e; clear e; intros; now subst. - - intros * _ IHt ? ? Hty'. - inversion Hty' ; subst ; refold. - eapply IHt in H0 as ->. - now eexists. - Qed. - -End AlgorithmicUnique. - -Corollary typing_unique Γ T T' t : - [Γ |-[de] t : T] -> - [Γ |-[de] t : T'] -> - [Γ |-[de] T ≅ T']. +Lemma type_uniqueness Γ A A' t : + [Γ |-[de] t : A] -> + [Γ |-[de] t : A'] -> + [Γ |-[de] A ≅ A']. Proof. - intros [_ Ti Hty]%algo_typing_complete [_ Ti' Hty']%algo_typing_complete. - eapply algo_typing_unique in Hty ; tea ; subst. + intros [?? Hinf]%algo_typing_complete [?? Hinf']%algo_typing_complete. + eapply algo_typing_det in Hinf. + 2: eassumption. + subst. etransitivity ; tea. now symmetry. -Qed. \ No newline at end of file +Qed. \ No newline at end of file diff --git a/theories/UntypedValues.v b/theories/UntypedValues.v deleted file mode 100644 index ee91936..0000000 --- a/theories/UntypedValues.v +++ /dev/null @@ -1,204 +0,0 @@ -From LogRel.AutoSubst Require Import core unscoped Ast Extra. -From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedReduction GenericTyping. - -Unset Elimination Schemes. - -Inductive snf (r : term) : Type := - | snf_tSort {s} : [ r ⇒* tSort s ] -> snf r - | snf_tProd {A B} : [ r ⇒* tProd A B ] -> snf A -> snf B -> snf r - | snf_tLambda {A t} : [ r ⇒* tLambda A t ] -> snf A -> snf t -> snf r - | snf_tNat : [ r ⇒* tNat ] -> snf r - | snf_tZero : [ r ⇒* tZero ] -> snf r - | snf_tSucc {n} : [ r ⇒* tSucc n ] -> snf n -> snf r - | snf_tEmpty : [ r ⇒* tEmpty ] -> snf r - | snf_tSig {A B} : [r ⇒* tSig A B] -> snf A -> snf B -> snf r - | snf_tPair {A B a b} : [r ⇒* tPair A B a b] -> snf A -> snf B -> snf a -> snf b -> snf r - | snf_tList {A} : [ r ⇒* tList A ] -> snf A -> snf r - | snf_tNil {A} : [ r ⇒* tNil A ] -> snf A -> snf r - | snf_tCons {A hd tl} : [r ⇒* tCons A hd tl ] -> snf A -> snf hd -> snf tl -> snf r - | snf_sne {n} : [ r ⇒* n ] -> sne n -> snf r - | snf_sne_list {n} : [r ⇒* n] -> sne_list n -> snf r -with sne (r : term) : Type := - | sne_tRel {v} : r = tRel v -> sne r - | sne_tApp {n t} : r = tApp n t -> sne n -> snf t -> sne r - | sne_tNatElim {P hz hs n} : r = tNatElim P hz hs n -> snf P -> snf hz -> snf hs -> sne n -> sne r - | sne_tEmptyElim {P e} : r = tEmptyElim P e -> snf P -> sne e -> sne r - | sne_tFst {p} : r = tFst p -> sne p -> sne r - | sne_tSnd {p} : r = tSnd p -> sne p -> sne r -with sne_list (r : term) : Type := - | sne_tMap {A B f l} : r = tMap A B f l -> snf A -> snf B -> snf f -> sne l -> sne_list r - | sne_list_sne : sne r -> sne_list r. - -Set Elimination Schemes. - -Scheme - Induction for snf Sort Type with - Induction for sne Sort Type with - Induction for sne_list Sort Type. - -Definition snf_rec - (P : forall r : term, snf r -> Set) - (Q : forall r : term, sne r -> Set) - (R : forall r : term, sne_list r -> Set) := snf_rect P Q R. - -Definition snf_ind - (P : forall r : term, snf r -> Prop) - (Q : forall r : term, sne r -> Prop) - (R : forall r : term, sne_list r -> Prop) := snf_rect P Q R. - -Definition sne_rec - (P : forall r : term, snf r -> Set) - (Q : forall r : term, sne r -> Set) - (R : forall r : term, sne_list r -> Set) := sne_rect P Q R. - -Definition sne_ind - (P : forall r : term, snf r -> Prop) - (Q : forall r : term, sne r -> Prop) - (R : forall r : term, sne_list r -> Prop) := sne_rect P Q R. - -Definition sne_list_rec -(P : forall r : term, snf r -> Set) -(Q : forall r : term, sne r -> Set) -(R : forall r : term, sne_list r -> Set) := sne_list_rect P Q R. - -Definition sne_list_ind -(P : forall r : term, snf r -> Prop) -(Q : forall r : term, sne r -> Prop) -(R : forall r : term, sne_list r -> Prop) := sne_list_rect P Q R. - -(* A&Y: add as many ps as you added new constructors for snf and sne in total *) -Definition snf_sne_rect P Q R p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22 := - pair - (snf_rect P Q R p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22) - (pair - (sne_rect P Q R p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22) - (sne_list_rect P Q R p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22)). - -Lemma sne_whne : forall (t : term), sne t -> whne t. -Proof. -apply sne_rect with (P := fun _ _ => True) (P1 := fun _ _ => True); intros; subst; constructor; assumption. -Qed. - -Lemma sne_whne_list : forall (t : term), sne_list t -> whne_list t. -Proof. -apply sne_list_rect with (P := fun _ _ => True) (P0 := fun _ _ => True) ; intros; subst; constructor. -all: eauto using sne_whne. -Qed. - -Lemma snf_red : forall t u, [ t ⇒* u ] -> snf u -> snf t. -Proof. -intros t u Hr Hu; destruct Hu. -+ eapply snf_tSort. - transitivity u; eassumption. -+ eapply snf_tProd. - - transitivity u; eassumption. - - assumption. - - assumption. -+ eapply snf_tLambda. - - transitivity u; eassumption. - - assumption. - - assumption. -+ eapply snf_tNat; transitivity u; eassumption. -+ eapply snf_tZero. - transitivity u; eassumption. -+ eapply snf_tSucc. - - transitivity u; eassumption. - - assumption. -+ eapply snf_tEmpty; transitivity u; eassumption. -+ eapply snf_tSig. - 1: transitivity u; eassumption. - all: tea. -+ eapply snf_tPair. - 1: transitivity u; eassumption. - all: tea. -+ eapply snf_tList; tea; now etransitivity. -+ eapply snf_tNil; tea; now etransitivity. -+ eapply snf_tCons; [now etransitivity|..]; tea. -+ eapply snf_sne. - - transitivity u; eassumption. - - eassumption. -+ eapply snf_sne_list. - - transitivity u; eassumption. - - eassumption. -Qed. - -Section RenSnf. - - Lemma snf_sne_ren : - prod (forall t, snf t -> forall ρ, snf (t⟨ρ⟩)) - (prod (forall t, sne t -> forall ρ, sne (t⟨ρ⟩)) (forall t, sne_list t -> forall ρ, sne_list (t⟨ρ⟩))). - Proof. - apply snf_sne_rect. - + intros r s Hr ρ. - apply credalg_wk with (ρ := ρ) in Hr. - eapply snf_tSort; eassumption. - + intros r A B Hr HA IHA HB IHB ρ. - apply credalg_wk with (ρ := ρ) in Hr. - eapply snf_tProd; eauto. - + intros r A t Hr HA IHA Ht IHt ρ. - apply credalg_wk with (ρ := ρ) in Hr. - eapply snf_tLambda; eauto. - + intros r Hr ρ. - apply credalg_wk with (ρ := ρ) in Hr. - eapply snf_tNat; eassumption. - + intros r Hr ρ. - apply credalg_wk with (ρ := ρ) in Hr. - eapply snf_tZero; eauto. - + intros r t Hr Ht IHt ρ. - apply credalg_wk with (ρ := ρ) in Hr. - eapply snf_tSucc; eauto. - + intros r Hr ρ. - apply credalg_wk with (ρ := ρ) in Hr. - eapply snf_tEmpty; eassumption. - + intros r A B Hr ???? ρ. - apply credalg_wk with (ρ := ρ) in Hr. - eapply snf_tSig; eauto. - + intros r ???? Hr ???????? ρ. - apply credalg_wk with (ρ := ρ) in Hr. - eapply snf_tPair; eauto. - + intros r ? Hr ?? ρ. - apply credalg_wk with (ρ := ρ) in Hr; cbn in *. - eapply snf_tList; tea; eauto. - + intros r ? Hr ?? ρ. - apply credalg_wk with (ρ := ρ) in Hr; cbn in *. - eapply snf_tNil; tea; eauto. - + intros r ??? Hr ?????? ρ. - apply credalg_wk with (ρ := ρ) in Hr; cbn in *. - eapply snf_tCons; tea; eauto. - + intros r n Hr Hn IHn ρ. - apply credalg_wk with (ρ := ρ) in Hr. - eapply snf_sne; eauto. - + intros r n Hr Hn IHn ρ. - apply credalg_wk with (ρ := ρ) in Hr. - eapply snf_sne_list; eauto. - + intros r v -> ρ; econstructor; reflexivity. - + intros r n t -> Hn IHn Ht IHt ρ. - cbn; eapply sne_tApp; eauto. - + intros r P hz hs n -> HP IHP Hhz IHhz Hhs IHhs Hn IHn ρ; cbn. - eapply sne_tNatElim; eauto. - + intros. subst. cbn. - eapply sne_tEmptyElim; eauto. - + intros r ? -> ???; cbn; eapply sne_tFst; eauto. - + intros r ? -> ???; cbn; eapply sne_tSnd; eauto. - + intros; subst; cbn. - eapply sne_tMap; eauto. - + intros n Hn IHn ρ. - eapply sne_list_sne ; eauto. - Qed. - - Lemma sne_ren ρ t : sne t -> sne (t⟨ρ⟩). - Proof. - intros; apply snf_sne_ren; assumption. - Qed. - - Lemma sne_list_ren ρ t : sne_list t -> sne_list (t⟨ρ⟩). - Proof. - intros; apply snf_sne_ren; assumption. - Qed. - - Lemma snf_ren ρ t : snf t -> snf (t⟨ρ⟩). - Proof. - intros; apply snf_sne_ren; assumption. - Qed. - -End RenSnf. diff --git a/theories/mapPiSigmaFunctorLaws.v b/theories/mapPiSigmaFunctorLaws.v index 1956cbd..66d2713 100644 --- a/theories/mapPiSigmaFunctorLaws.v +++ b/theories/mapPiSigmaFunctorLaws.v @@ -1,4 +1,4 @@ -(** * LogRel.mapPiSigmaFunctorLaws: functor laws hold definitionally for Coq's Π and Σ *) +(** * LogRel.mapPiSigmaFunctorLaws: functor laws hold definitionally for Coq's Π and Σ. *) Set Primitive Projections. Record Sigma A B := pair { proj1 : A ; proj2 : B proj1 }. Notation "'∑' x .. y , p" := (Sigma _ (fun x => .. (Sigma _ (fun y => p%type)) ..))