| theories | ||
| .gitignore | ||
| _CoqProject | ||
| dcoi-omega.opam | ||
| gen_syntax.pl | ||
| LICENSE | ||
| Makefile | ||
| README.md | ||
| syntax.sig | ||
Rocq Mechanization of DCOI$^omega$
Coq Development
System specification
The file theories/Lattice/All.v defines the specification of a lattice structure as a module type. We parameterize our development over this lattice structure by placing most of our the definitions and proofs inside Coq module functors.
We use the autosubst2 tool to convert the HOAS syntax specification
of DCOI (syntax.sig) into a Coq file containing
its de Bruijn representation
(syntax.v). The generated Coq
file includes not only the inductive definition of the term syntax
tm, but also the renaming (ren_tm) and substitution (subst_tm)
functions. The notation a[σ] (resp. a⟨ξ⟩) represents the application of
a substitution σ (resp. a renaming ξ) to the term a.
Since autosubst2 doesn't support module functors, we use a perl script to wrap the generated syntax inside a functor.
The typing rules can be found in
typing.v. The inductive types Wt and
Wff represent well-typedness and context well-formedness
respectively. Every rule with an admissible premise in the text is
accompanied by a lemma that justifies the admissible version of
rule. We include those lemmas in our claimed results section.
The definition of untyped convertibility used in rule WT-Conv (the
T_Conv constructor in the Coq file) can be found in
conv.v. The indistinguishability judgment
is named IEq and can be found in geq.v.
Instantiated lemmas
To ensure that we did not accidentally parameterize our development over an inconsistent assumption, we instantiate the module functors to a concrete lattice in the file toplevel.v.
In toplevel.v, we print out the signatures of the top-level theorems and the axioms they depend on. By instantiating the module functors, we ensure that the parameterized lattice structure does not appear alongside the axioms we actually used.
Reviewers can refer to Axioms made in the Coq development for a detailed discussion of the use of axioms.
Key results
The individual results can be found in the corresponding Coq files and theorem
statements as directed by the paper's footnotes. All Coq files are in
the directory /home/dcoi/proofs inside the image and we also duplicate the
same files in the proofs subdirectory of the tarball so they can be
more easily accessed through the host machine and navigated through
this README file.
-
Lemma 3.1 (Regularity)
- preservation.v:
Wt_Wff,Wt_regularity
- preservation.v:
-
Lemma 3.2 (Simulation)
- conv.v:
simulation_star
- conv.v:
-
Admissibility of the premises in
Wt-Abs,Wt-J,Wt-Let- preservation.v:
T_Abs_simpl,T_J_simpl,T_Let_simpl
- preservation.v:
-
Admissibility of
Wt-Proj1,Wt-Proj2,Wt-Proj2Alt,Wt-T,Wt-Box,Wt-Unbox- admissible.v:
T_Proj1,T_Proj2,T_Proj2_Alt,T_T,T_Box,T_Unbox
- admissible.v:
-
Lemma 3.3 (Downgrade)
- admissible.v:
T_Down_Alt
- admissible.v:
-
Figure 11
L-Subst,L-Sub,I-Subst,I-Cong,I-Down:- geq.v:
iok_subst,iok_subsumption,ieq_iok_subst,ieq_morphing_mutual,ieq_downgrade_mutual
- geq.v:
-
Figure 11
Wt-Subst,Wt-Sub:- preservation.v:
subst_Syn,subsumption
- preservation.v:
-
Lemma 4.1 (Diamond)
- par.v:
Par_confluent
- par.v:
-
Lemma 4.2 (Confluence)
- par.v:
Pars_confluent
- par.v:
-
Lemma 4.3 (Transitivity of Equality)
- conv.v:
conv_trans
- conv.v:
-
Lemma 4.4
- preservation.v:
Wt_Refl_Coherent
- preservation.v:
-
Lemma 4.5 (Type Preservation)
- preservation.v:
subject_reduction(_star)
- preservation.v:
-
Definition 5.1 (Weakly normalizing terms)
- normalform.v:
wn,wne
- normalform.v:
-
Lemma 5.2
- normalform.v:
nf_refl
- normalform.v:
-
Figure 12 (Definition of the logical predicate)
- semtyping.v:
InterpExt
- semtyping.v:
-
Lemma 5.4 (Escape)
- semtyping.v:
InterpUniv_Ok
- semtyping.v:
-
Lemma 5.5 (Subsumption for the logical predicate)
- semtyping.v:
InterpUnivN_subsumption
- semtyping.v:
-
Lemma 5.6 (Inversion of the logical predicate)
- semtyping.v:
InterpUnivN_Eq_inv,InterpUnivN_Fun_inv_nopf,InterpUnivN_Void_inv
- semtyping.v:
-
Lemma 5.7 (Backward closure)
- semtyping.v:
InterpUnivN_back_clos
- semtyping.v:
-
Lemma 5.8 (Cumulativity)
- semtyping.v:
InterpUnivN_cumulative
- semtyping.v:
-
Lemma 5.9 (Reduction preserves interpretation)
- semtyping.v:
InterpUnivN_preservation
- semtyping.v:
-
Lemma 5.10 (Functionality)
- semtyping.v:
InterpUnivN_deterministic
- semtyping.v:
-
Lemma 5.11 (Functionality for indistinguishable terms)
- semtyping.v:
InterpUnivN_Eq
- semtyping.v:
-
Lemma 5.12 (Antirenaming for parallel reduction)
- normalform.v:
Par_antirenaming
- normalform.v:
-
Lemma 5.13 (Antirenaming for normal and neutral forms)
- normalform.v:
ne_nf_renaming_with_d
- normalform.v:
-
Lemma 5.14 (Antirenaming for weak normalization)
- normalform.v:
wn_antirenaming
- normalform.v:
-
Lemma 5.15 (Adequacy)
- semtyping.v:
adequacy
- semtyping.v:
-
Definition 5.17 (Valid substitutions)
- soundness.v:
ρ_ok
- soundness.v:
-
Lemma 5.18
- soundness.v:
iok_ρ_ok_morphing
- soundness.v:
-
Lemma 5.19 (Structural rules for valid substitutions)
- soundness.v:
ρ_ok_id,ρ_ok_cons
- soundness.v:
-
Definition 5.20 (Semantic well-typedness)
- soundness.v:
SemWt
- soundness.v:
-
Lemma 5.21 (Weakening for valid substitutions and semantic well-typedness)
- soundness.v:
ρ_ok_renaming,weakening_Sem
- soundness.v:
-
Theorem 5.22 (Fundamental theorem)
- soundness.v:
soundness
- soundness.v:
-
Corollary 5.23 (Weak normalization for well-typed terms)
- soundness.v:
normalization
- soundness.v:
-
Corollary 5.24 (Logical consistency)
- consistency.v:
consistency
- consistency.v:
-
Lemma 5.25 (Standardization)
- factorization.v:
standardization
- factorization.v:
-
Corollary 5.26 (Normalization is decidable)
- factorization.v:
LoRed_normalize
- factorization.v:
-
Lemma 5.27 (Indistinguishability is decidable)
- geq.v:
IEq_dec
- geq.v:
-
Definition 5.28 (Algorithm for type conversion)
- iconv_dec.v:
convb
- iconv_dec.v:
-
Theorem 5.29 (Decidability of type conversion with bottom)
- iconv_dec.v:
conv_dec
- iconv_dec.v:
-
Theorem 5.30 (Decidability of indexed type conversion)
- iconv_dec.v:
iconv_dec
- iconv_dec.v:
Differences between the mechanization and the paper presentation
In Coq, inductively generated types and propositions must be defined at the top-level. The definition of the logical predicate, on the other hand, is a recursive function (over the universe levels) that returns an inductive proposition. In an ideal world, we would want to define our logical relation as follows.
Fixpoint InterpUnivN Ξ (n : nat) ... :=
Inductive InterpUniv Ξ := ...
| ...
Instead, we need to factor this definition into two parts. First, we
define the top-level inductive type InterpExt Ξ n I. The
parameter I is a function representing the recursive call, which
gives the interpretation of types at universe levels that are strictly
lower than n. We then tie the knot by defining a recursive function
InterpUnivN Ξ n over n, which simply calls InterpExt with I
instantiated to itself. The function InterpUnivN gives us the
logical predicate we wanted.
Axioms made in the Coq development
To check the axioms used in the development, the reviewers can run the
Print Assumptions command in toplevel.v to
query the axioms used in the instantiated modules.
Print Assumptions dcoi_with_nat_lattice.consistency.consistency.
Here's the output.
Axioms:
propositional_extensionality : forall P Q : Prop, P <-> Q -> P = Q
functional_extensionality_dep
: forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
(forall x : A, f x = g x) -> f = g
The command make validate runs coqchk to dump all axioms used in our development.
make -f CoqMakefile validate
make[1]: Entering directory '/home/dcoi/proofs'
"coqchk" -silent -o -R theories DCOIOmega theories/Autosubst2/axioms.vo theories/Autosubst2/syntax.vo theories/Autosubst2/unscoped.vo theories/Lattice/All.vo theories/admissible.vo theories/consistency.vo theories/conv.vo theories/factorization.vo theories/geq.vo theories/iconv_dec.vo theories/imports.vo theories/normalform.vo theories/par.vo theories/preservation.vo theories/semtyping.vo theories/soundness.vo theories/toplevel.vo theories/typing.vo theories/typing_conv.vo
CONTEXT SUMMARY
===============
* Theory: Set is predicative
* Axioms:
Coq.Logic.FunctionalExtensionality.functional_extensionality_dep
Coq.Reals.ClassicalDedekindReals.sig_not_dec
Coq.Reals.ClassicalDedekindReals.sig_forall_dec
Coq.Logic.PropExtensionality.propositional_extensionality
Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq
* Constants/Inductives relying on type-in-type: <none>
* Constants/Inductives relying on unsafe (co)fixpoints: <none>
* Inductives whose positivity is assumed: <none>
make[1]: Leaving directory '/home/dcoi/proofs'
Note that we don't actually use eq_rect_eq or the axioms about
dedekind reals in our development. They are never printed when we run
the Print Assumptions command. coqchk is known to report axioms
that are part of external modules despite them not being used by the
development.
Functional and propositional extensionality allow us to recover the
type of reasoning in set theory where two sets are considered equal if
and only if they contain the same elements (in Coq, the predicate A -> Prop can be thought of as a subset of the type A). These two
axioms are known to be consistent with Coq.
The introduction of axioms in the Prop sort means that we can no
longer prove decidability of a proposition P by providing an
inhabitance of P \/ not P since types in Prop lose canonicity. Instead, in
our development, we explicitly define a computable function in the
relevant universe Type and use the ssreflect's reflect type to
connect between the function and the proposition it's meant to decide.
Extending the system
To extend DCOI$^\omega$ with extra features, one can modify syntax.sig to add new syntactic forms to the grammar and add new rules for the typing and equality judgments in typing.v and geq.v.