Full Iso-recursive Types (Artifact)

Introduction

This repository contains the artifact for OOPSLA'24 paper Full Iso-recursive Types.

We provide both pre-configured Docker image and original source code in the artifact. You may choose either one to use.

Proof Assistant and Libraries Dependency

Our proofs are verified in Coq 8.13.2. We rely on the Coq library: Metalib to formalize variables and binders using the Locally Nameless representation (Aydemir et al., 2008) in our proofs. We use Ott to write the definitions and LNgen to generate Locally Nameless definitions and proofs. We also use (a modified distribution of) LibTactics.v from the TLC Coq library by Arthur Chargueraud.

Proof Structure

There are two directories in this artifact. The cast_main directory contains the proofs for the main system presented in Section 3 and Section 4 of the paper. The cast_sub directory contains the proofs for the main system extended with subtyping presented in Section 5 of the paper.

The cast_main and cast_sub share the same structure, in which all the proof files have a sequential dependency, as can be found in _CoqProject file of each directory. The proof starts from syntax_ott.v, which is generated from the Ott specification in spec directory, and ends with theorems.v. The theorems.v file contains most of the main theorems of the paper. There is also a doc directory that contains a latex pdf generated from the Ott specification that presents all the rules of each system.

In addition, within cast_sub there is a subdirectory subtyping which contains the Coq proofs from the artifact of the paper "Revisiting Iso-recursive Subtyping" (Zhou et al. 2022). We transported their results (e.g. unfolding lemma) to our setting through subtyping.v in the cast_sub directory.

Key Definitions in the Paper

Definition	File	Notation in Paper	Name in Coq
Fig. 2. Brandt and Henglein's equi-recursive type equality	syntax_ott.v	$H \vdash A \doteq B$	`eqe2`
Fig. 4. Typing	syntax_ott.v	$\Gamma \vdash e: A $	`Typing`
Fig. 4. Type Casting	syntax_ott.v	$\Delta; \mathbb{E} \vdash A \hookrightarrow B : c $	`TypCast`
Fig. 5. Equi-recursive typing with rule Typ-eq	syntax_ott.v	$\Gamma \vdash_e e : A $	`EquiTyping`
Fig. 5. Full iso-recursive elaboration	syntax_ott.v	$\Gamma \vdash_e e : A \rhd e' $	`EquiTypingC`
Fig. 6. Reduction rules	syntax_ott.v	$e \hookrightarrow e' $	`Reduction`
Fig. 7. Iso-recursive Subtyping	syntax_ott.v	$\Sigma \vdash A \leq_{i} B $	`AmberSubtyping`
Fig. 7. Equi-recursive Subtyping	syntax_ott.v	$\Sigma \vdash A \leq_{e} B $	`ACSubtyping`

Difference between the Formalization and the Paper

In the formalization of the rules in literature (e.g. Brandt and Henglein's equi-recursive type equality in Fig. 2, Iso-recursive Subtyping, and Equi-recursive Subtyping in Fig. 7), we add a type context and well-formedness check to the rules in order to be consistent with the rest of the rules. The well-formedness conditions are omitted in the paper for simplicity.

Paper to Proof Table

The main system

Contains the proofs for the main system presented in Section 3 and Section 4 of the paper.

The paper to proof table:

Theorem	File	Name in Coq
Theorem 3.1 Soundness of Type Casting	theorems.v	`TypCast_soundness`
Theorem 3.1 Completeness of Type Casting	theorems.v	`TypCast_completeness`
Theorem 3.2 Equivalence of Alternative equi-recursive typing	theorems.v	`equi_alt_equiv`
Theorem 3.3 Equi-recursive to full iso-recursive typing	theorems.v	`EquiTypingC_sem`
Theorem 3.4 Full iso-recursive to equi-recursive typing	theorems.v	`typing_i2e`
Theorem 3.5 Round-tripping of the encoding	theorems.v	`erase_typing`
Theorem 3.6 Progress	Progress.v	`progress`
Theorem 3.7 Preservation	Preservation.v	`preservation`
Theorem 3.8 Full iso-recursive to equi-recursive reduction	theorems.v	`reductions_i2e`
Theorem 3.9 Behavioral equivalence	theorems.v	`behavior_equiv`

The subtyping system

Contains the proofs for the main system extended with subtyping presented in Section 5 of the paper.

The paper to proof table:

Theorem	File	Name in Coq
Theorem 5.1 Reflxixivty of Iso-recursive Subtyping	subtyping.v	`AmberWFT_refl`
Theorem 5.2 Transitivity of Iso-recursive Subtyping	subtyping.v	`AmberSub_trans`
Lemma 5.3 Unfolding Lemma	subtyping.v	`unfolding_lemma`
Theorem 5.4(1) Progress	Progress.v	`progress`
Theorem 5.4(2) Preservation	Preservation.v	`preservation`
Theorem 5.5 Equi-recursive subtyping decomposition	theorems.v	`subtyping_decomposition`
Theorem 5.6(1) Typing Equivalence - soundness	theorems.v	`typing_i2e`
Theorem 5.6(2) Typing Equivalence - completeness	theorems.v	`EquiTypingC_sem`
Theorem 5.6(3) Typing Equivalence - round-tripping	theorems.v	`erase_typing`
Theorem 5.7 Behavioral Equivalence	theorems.v	`behavior_equiv`

Hardware Dependencies

There is no special requirement on the hardware. Basically a typical laptop can fulfill the resource demand and complete all tasks. ~5GiB disk space is required for loading the Docker image, and the check can be done in a few minutes.

Note that the Docker image is built for x86 architecture, so emulation softwares may be needed if you are working on a platform other than that.

Getting Started Guide

For reviews who want to the pre-built Docker for quick testing, you can refer to section Using Docker. Or if you want to create the environ manually, you can refer to section Manual Installation.

Using Docker

Install Docker first. You may refer to the Docker Docs. For Windows users, WSL2 is recommended. Then run the following steps:

Start the Docker service on your system;
In the artifact directory, run xz -d fulliso.tar.xz to decompress the Docker image;
Run docker load -i fulliso.tar to import the image;
Run docker run -it --rm fulliso to start the container;
You'll see cast_main and cast_sub directories under the current location; you can cd into either one and run make to check our proofs.

Manual Installation

Prerequisites

Install Coq 8.13.2. The recommended way to install Coq is via OPAM. Refer to here for detailed steps. Or you could download the pre-built packages for Windows and MacOS here. Choose a suitable installer according to your platform.
Make sure Coq is installed, then install Metalib:
1. git clone -b coq8.10 https://github.com/plclub/metalib
2. cd metalib/Metalib
3. make install

For checking proofs of the paper, you can stop here and use the provided syntax_ott.v and rules_inf.v files. We have already built these files, which are generated by LNgen and Ott. If you want to modify the rules, you can follow the rest of the instructions below to install LNgen and Ott:

Make sure Haskell with stack is installed, then install LNgen:
1. git clone https://github.com/plclub/lngen
2. cd lngen
3. stack install
Install Ott 0.32 if you want to rewrite the rules. Make sure opam is installed:
1. git clone https://github.com/sweirich/ott -b ln-close
2. cd ott
3. opam pin add ott .
4. opam pin add coq-ott .
Check the Ott website for detailed instructions. Remember to switch to the correct forked version of Ott 0.32 during the installation process.

You may also take the provided Dockerfile for reference. The Docker image can be built by docker build -t fulliso ..

Build and Compile the Proofs

Enter the coq directory you would like to build.
Type make in the terminal to build and compile the proofs.

Expected Output

For cast_main:

/home/fulliso/cast_main$ make
coqdep -f _CoqProject > .depend
coq_makefile -arg '-w none' -f _CoqProject -o CoqSrc.mk
make[1]: Entering directory '/home/fulliso/cast_main'
COQDEP VFILES
COQC LibTactics.v
COQC syntax_ott.v
COQC rules_inf.v
COQC progress.v
COQC erasure.v
COQC equiRec.v
COQC preservation.v
COQC equiAux.v
COQC theorems.v
make[1]: Leaving directory '/home/fulliso/cast_main'

For cast_sub:

/home/fulliso/cast_sub$ make
coqdep -f _CoqProject > .depend
coq_makefile -arg '-w none' -f _CoqProject -o CoqSrc.mk
make[1]: Entering directory '/home/fulliso/cast_sub'
COQDEP VFILES
COQC LibTactics.v
COQC syntax_ott.v
COQC rules_inf.v
COQC subtyping/Rules.v
COQC subtyping/Infra.v
COQC subtyping/FiniteUnfolding.v
COQC subtyping/Typesafety.v
COQC subtyping/DoubleUnfolding.v
COQC subtyping/AmberBase.v
COQC subtyping/AmberLocal.v
COQC subtyping/AmberSoundness.v
COQC subtyping/PositiveBase.v
COQC subtyping/PositiveSubtyping.v
COQC subtyping/AmberCompleteness.v
COQC subtyping/NominalUnfolding.v
COQC subtyping/AnchorUnfolding.v
COQC subtyping/Decidability.v
COQC subtyping.v
COQC progress.v
COQC erasure.v
COQC equiRec.v
COQC preservation.v
COQC equiAux.v
COQC theorems.v
make[1]: Leaving directory '/home/fulliso/cast_sub'

The build should run to the end without any error message produced.

Step by Step Instructions

Evaluate the Result

All the claims made by the paper, as shown in section Proof Structure, is substantiated by the successful build.

Check Axioms and Assumptions

To verify the axioms that out proofs rely on, you can use Print Assumptions theorem_name in Coq, by replacing theorem_name with the name of the theorem you want to check in the paper-to-proof table.

For example, by adding Print Assumptions behavior_equiv. to the end of theorems.v (you may need to sudo apt update && sudo apt install nano -y (or vim based on your preference) first if you are inside the Docker image) and re-run make, you will see:

COQC theorems.v
Axioms:
JMeq_eq : forall (A : Type) (x y : A), x ~= y -> x = y

It should be the only axiom that the behavior_equiv theorem relies on, which is introduced by the use of dependent induction.

To show axioms we defined across the whole proof, you may run grep -Ir "Axiom" . under /home/fulliso.

For the main system cast_main it will return nothing, and for the subtyping system cast_sub it will return:

./theorems.v:Axiom subtyping_decomposition: forall A B D (Hwfa: WFT D A) (Hwfb: WFT D B),

The subtyping_decomposition (Theorem 5.5 in the paper) is the only axiom we defined in the proofs and we explained the reason in the paper.

Alternatively, you may run coqchk -R . Top Top.theorems -o -silent under the project folder as well to check all the axioms we introduced in the proofs.

For the main system cast_main it will return:

CONTEXT SUMMARY
===============

* Theory: Set is predicative
  
* Axioms:
    Metalib.MetatheoryAtom.AtomSetImpl.union_3
    Metalib.MetatheoryAtom.AtomSetImpl.union_2
    Metalib.MetatheoryAtom.AtomSetImpl.union_1
    Metalib.MetatheoryAtom.AtomSetImpl.subset
    Metalib.MetatheoryAtom.AtomSetImpl.remove
    Metalib.MetatheoryAtom.AtomSetImpl.eq_trans
    Metalib.MetatheoryAtom.AtomSetImpl.fold_1
    Metalib.MetatheoryAtom.AtomSetImpl.filter
    Metalib.MetatheoryAtom.AtomSetImpl.eq_sym
    Metalib.MetatheoryAtom.AtomSetImpl.eq_dec
    Metalib.MetatheoryAtom.AtomSetImpl.diff_3
    Metalib.MetatheoryAtom.AtomSetImpl.diff_2
    Metalib.MetatheoryAtom.AtomSetImpl.diff_1
    Metalib.MetatheoryAtom.AtomSetImpl.choose_2
    Metalib.MetatheoryAtom.AtomSetImpl.choose_1
    Metalib.MetatheoryAtom.AtomSetImpl.choose
    Coq.micromega.ZifyInst.ltac_gen_subproof9
    Coq.micromega.ZifyInst.ltac_gen_subproof8
    Coq.micromega.ZifyInst.ltac_gen_subproof7
    Coq.micromega.ZifyInst.ltac_gen_subproof6
    Coq.micromega.ZifyInst.ltac_gen_subproof5
    Coq.micromega.ZifyInst.ltac_gen_subproof4
    Coq.micromega.ZifyInst.ltac_gen_subproof3
    Coq.micromega.ZifyInst.ltac_gen_subproof2
    Coq.micromega.ZifyInst.ltac_gen_subproof1
    Coq.micromega.ZifyInst.ltac_gen_subproof0
    Metalib.MetatheoryAtom.AtomSetImpl.subset_2
    Metalib.MetatheoryAtom.AtomSetImpl.subset_1
    Metalib.MetatheoryAtom.AtomSetImpl.elements
    Metalib.MetatheoryAtom.AtomSetImpl.is_empty_2
    Metalib.MetatheoryAtom.AtomSetImpl.is_empty_1
    Metalib.MetatheoryAtom.AtomSetImpl.union
    Metalib.MetatheoryAtom.AtomSetImpl.mem_2
    Metalib.MetatheoryAtom.AtomSetImpl.mem_1
    Metalib.MetatheoryAtom.AtomSetImpl.inter
    Metalib.MetatheoryAtom.AtomSetImpl.equal
    Metalib.MetatheoryAtom.AtomSetImpl.empty
    Metalib.MetatheoryAtom.AtomSetImpl.add_3
    Metalib.MetatheoryAtom.AtomSetImpl.add_2
    Metalib.MetatheoryAtom.AtomSetImpl.add_1
    Coq.Logic.ProofIrrelevance.proof_irrelevance
    Metalib.MetatheoryAtom.AtomSetImpl.fold
    Metalib.MetatheoryAtom.AtomSetImpl.diff
    Metalib.MetatheoryAtom.AtomSetImpl.In_1
    Metalib.MetatheoryAtom.AtomSetImpl.mem
    Metalib.MetatheoryAtom.AtomSetImpl.add
    Metalib.MetatheoryAtom.AtomSetImpl.In
    Metalib.MetatheoryAtom.AtomSetImpl.t
    Metalib.MetatheoryAtom.AtomSetImpl.for_all_2
    Metalib.MetatheoryAtom.AtomSetImpl.for_all_1
    Metalib.MetatheoryAtom.AtomSetImpl.cardinal
    Metalib.MetatheoryAtom.AtomSetImpl.singleton_2
    Metalib.MetatheoryAtom.AtomSetImpl.singleton_1
    Coq.Logic.FunctionalExtensionality.functional_extensionality_dep
    Metalib.MetatheoryAtom.AtomSetImpl.cardinal_1
    Metalib.MetatheoryAtom.AtomSetImpl.inter_3
    Metalib.MetatheoryAtom.AtomSetImpl.inter_2
    Metalib.MetatheoryAtom.AtomSetImpl.inter_1
    Metalib.MetatheoryAtom.AtomSetImpl.elements_3w
    Metalib.MetatheoryAtom.AtomSetImpl.filter_3
    Metalib.MetatheoryAtom.AtomSetImpl.filter_2
    Metalib.MetatheoryAtom.AtomSetImpl.filter_1
    Metalib.MetatheoryAtom.AtomSetImpl.for_all
    Metalib.MetatheoryAtom.AtomSetImpl.exists_
    Metalib.MetatheoryAtom.AtomSetImpl.partition_2
    Metalib.MetatheoryAtom.AtomSetImpl.partition_1
    Metalib.MetatheoryAtom.AtomSetImpl.equal_2
    Metalib.MetatheoryAtom.AtomSetImpl.equal_1
    Metalib.MetatheoryAtom.AtomSetImpl.eq_refl
    Metalib.MetatheoryAtom.AtomSetImpl.empty_1
    Metalib.MetatheoryAtom.AtomSetImpl.is_empty
    Coq.micromega.ZifyInst.ltac_gen_subproof22
    Coq.micromega.ZifyInst.ltac_gen_subproof21
    Coq.micromega.ZifyInst.ltac_gen_subproof20
    Coq.micromega.ZifyInst.ltac_gen_subproof19
    Coq.micromega.ZifyInst.ltac_gen_subproof18
    Coq.micromega.ZifyInst.ltac_gen_subproof17
    Coq.micromega.ZifyInst.ltac_gen_subproof16
    Coq.micromega.ZifyInst.ltac_gen_subproof15
    Coq.micromega.ZifyInst.ltac_gen_subproof14
    Coq.micromega.ZifyInst.ltac_gen_subproof13
    Coq.micromega.ZifyInst.ltac_gen_subproof12
    Coq.micromega.ZifyInst.ltac_gen_subproof11
    Coq.micromega.ZifyInst.ltac_gen_subproof10
    Coq.Logic.JMeq.JMeq_eq
    Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq
    Coq.micromega.ZifyInst.ltac_gen_subproof
    Metalib.MetatheoryAtom.AtomSetImpl.exists_2
    Metalib.MetatheoryAtom.AtomSetImpl.exists_1
    Metalib.MetatheoryAtom.AtomSetImpl.remove_3
    Metalib.MetatheoryAtom.AtomSetImpl.remove_2
    Metalib.MetatheoryAtom.AtomSetImpl.remove_1
    Metalib.MetatheoryAtom.AtomSetImpl.partition
    Metalib.MetatheoryAtom.AtomSetImpl.elements_2
    Metalib.MetatheoryAtom.AtomSetImpl.elements_1
    Metalib.MetatheoryAtom.AtomSetImpl.singleton
  
* Constants/Inductives relying on type-in-type: <none>
  
* Constants/Inductives relying on unsafe (co)fixpoints: <none>
  
* Inductives whose positivity is assumed: <none>

Except those introduced by Lia (the Coq.micromega series) or Metalib, the axioms introduced by the Coq standard library are:

Axiom	File	Notes
`functional_extensionality_dep`	rules_inf.v	Generated by `LNgen`
`proof_irrelevance`	LibTactics.v
`eq_rect_eq`	LibTactics.v	By importing `Coq.Program.Equality` for `dependent induction` Equivalent to `UIP`, corollary of `proof_irrelevance`
`JMeq_eq`	LibTactics.v	By importing `Coq.Program.Equality` for `dependent induction` Corollary of `eq_rect_eq`

For the subtyping system cast_sub, it will also return Top.theorems.subtyping_decomposition in addition to the above results.

Check Unproved Hypotheses

Run grep -Ir "Admitted\." . under /home/fulliso, and there will be no output, indicating that all the proofs are complete.

Other `make` Commands

make rules # Generate the syntax_ott.v and rules_inf.v files
make pdf   # Generate the latex pdf from the Ott specification
make clean # Clean all the files generated by Coq checking
make realclean # Clean all the generated files including documents

You may make use of these commands after modifying the rules or proofs.

Note that the make pdf command requires a $\LaTeX$ installation. If you are using Docker, you may docker cp the doc folders out of the container after make rules, and run latexmk -pdf main.tex to generate the PDF file. Also note that make pdf will call latexmk.exe under WSL. If that's not your case (i.e. the $\LaTeX$ is directly installed inside the WSL), you may modify the Makefile by changing the LATEXMK variable.

Reusability Guide

The core pieces of the artifact intended to be reused is the rules, theorems, and the proofs. Future users can refer to the Proof Structure section for grasping the existing proofs, and make their own modification based on the existing ones. They may use the convenient shortcuts provided such as make pdf to generate the documentation, which facilitates the reusability.

The proofs may need to be adjusted if the downstream user is using a differenct Coq version, which can be a limitation in the reusability of this artifact.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Repository files navigation

Full Iso-recursive Types (Artifact)

Introduction

Proof Assistant and Libraries Dependency

Proof Structure

Key Definitions in the Paper

Difference between the Formalization and the Paper

Paper to Proof Table

Hardware Dependencies

Getting Started Guide

Using Docker

Manual Installation

Prerequisites

Build and Compile the Proofs

Expected Output

Step by Step Instructions

Evaluate the Result

Check Axioms and Assumptions

Check Unproved Hypotheses

Other `make` Commands

Reusability Guide

About

Releases

Packages

Contributors 2

Languages

Name		Name	Last commit message	Last commit date
Latest commit History 45 Commits
cast_main		cast_main
cast_sub		cast_sub
Dockerfile		Dockerfile
README.md		README.md
README_dev.md		README_dev.md

ltzone/Full-Iso-Recursive-Types

Folders and files

Latest commit

History

Repository files navigation

Full Iso-recursive Types (Artifact)

Introduction

Proof Assistant and Libraries Dependency

Proof Structure

Key Definitions in the Paper

Difference between the Formalization and the Paper

Paper to Proof Table

Hardware Dependencies

Getting Started Guide

Using Docker

Manual Installation

Prerequisites

Build and Compile the Proofs

Expected Output

Step by Step Instructions

Evaluate the Result

Check Axioms and Assumptions

Check Unproved Hypotheses

Other make Commands

Reusability Guide

About

Topics

Resources

Stars

Watchers

Forks

Releases

Packages 0

Contributors 2

Languages

Other `make` Commands

Packages