Mechanical Formalizations of Bidirectional Higher-Rank Polymorphism: An Experience Report (Supplementary Materiel)

Overview

This paper provides three formalizations for different type systems with worklist-based type inference algorithm:

1. Rocq formalization for DK (with matching, worklist substitution and syntax-directed transfer);
2. Rocq formalization for Elem (with matching, worklist substitution and syntax-directed transfer);
3. Abella formalization for DK (with matching, worklist substitution).

Component

• full-paper.pdf: Full paper with Appendix.
• supplementary/proof_rocq/: The whole Rocq proof project, which can be compiled with Coq 8.15.2;
  • supplementary/proof_rocq/systemdk/ Rocq proofs of system DK;
  • supplementary/proof_rocq/systemfe/ Rocq proofs of system Elem;
• supplementary/proof_abella/: The whole Abella proof project, which can be compiled with Abella 2.0.8;
  • supplementary/proof_rocq/systemdk/ Abella proofs of system DK (with matching and worklist substitution).

Rocq Proof

The _.v file contains all the references to the important lemmas and theorems of formalization.

The following table shows the mapping from all the theorems in the paper to their corresponding theorem names in the Rocq proof (for DK only).

Lemmas and Theorems

Lems / Thms	Rocq Name
Theorem 1	d_chk_inf'_d_chk_inf
Theorem 2	d_sub_d_wf, d_chk_inf_wf_typ
Theorem 3	d_sub_reflexivity
Theorem 4	d_sub_transitivity
Theorem 5	d_chk_subsumption
Theorem 6	a_wl_red_chk_soundness, a_wl_red_inf_soundness
Theorem 8	a_wl_red_decidability
Lemma 9	subst_typ_in_typ_fresh_eq
Lemma 12	d_sub_size_transitivity
Theorem 15	a_wl_red_soundness, a_wl_red_completeness
Theorem 16	d_wl_red_weakening_works, d_wl_red_strengthening_work
Lemma 22	aworklist_subst_transfer_same_dworklist, aworklist_subst_transfer_same_dworklist_rev
Lemma 28	rename_tvar_in_a_wf_wl_a_wl_red, rename_var_in_a_wf_wl_a_wl_red
Lemma 31	aworklist_subst_wf_typ_subst, aworklist_subst_wf_wl, aworklist_subst_wf_typ
Theorem 32	a_wf_typ_reorder_aenv
Theorem 33	a_wf_typ_weakening_cons
Theorem 34	a_wf_typ_weaken
Theorem 39	trans_typ_reorder_ss, trans_exp_reorder_ss, trans_conts_reorder_ss, trans_work_reorder_ss
Lemma 41	trans_typ_subst_etvar_same_ss
Lemma 42	trans_typ_subst_etvar, trans_typ_etvar_subst
Lemma 44	aworklist_subst_transfer_same_dworklist, aworklist_subst_transfer_same_dworklist_rev_exist'
Theorem 45	aworklist_subst_fresh_etvar_total
Theorem 47	d_sub_mono_refl

Usage

• Check the proofs: navigate to the supplementary/proof_rocq/ directory and run make coq. (NOTES: The proof may take a long time to check. For reference, it's about 1 hour on an M2 Max MacBook)

  Expected Output: Definition of each theorem and lemma and axioms used by it. The only axiom used is Eqdep.Eq_rect_eq.eq_rect_eq. This is introduced by the Coq built-in tactic dependent destruction and does not harm the consistency.

  d_sub_transitivity
      : forall (Ψ : systemfe.def_ott.denv) (A B C : systemfe.def_ott.typ),
      systemfe.decl.def_extra.d_sub Ψ A B ->
      systemfe.decl.def_extra.d_sub Ψ B C ->
      systemfe.decl.def_extra.d_sub Ψ A C
  Axioms:
  Eqdep.Eq_rect_eq.eq_rect_eq
  : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
      x = eq_rect p Q x p h
  d_chk_inf_subsumption
      : forall (n1 n2 : nat) (Ψ Ψ' : systemfe.def_ott.denv)
          (e : systemfe.def_ott.exp) (A : systemfe.def_ott.typ)
          (mode : systemfe.decl.def_extra.typing_mode),
      systemfe.decl.prop_typing.exp_size e < n1 ->
      dmode_size mode < n2 ->
      systemfe.decl.def_extra.d_chk_inf Ψ e mode A ->
      d_subenv Ψ' Ψ ->
      match mode with
      | systemfe.decl.def_extra.typingmode__inf =>
          exists A' : systemfe.def_ott.typ,
              systemfe.decl.def_extra.d_sub Ψ A' A /\
              systemfe.decl.def_extra.d_chk_inf Ψ' e
              systemfe.decl.def_extra.typingmode__inf A'
      | systemfe.decl.def_extra.typingmode__chk =>
          forall A' : systemfe.def_ott.typ,
          systemfe.decl.def_extra.d_sub Ψ A A' ->
          systemfe.decl.def_extra.d_chk_inf Ψ' e
              systemfe.decl.def_extra.typingmode__chk A'
      end
  ...
  

• Reproduce the generated code (optional): ott and lngen are used to generate the def_ott.v and prop_ln.v files (i.e. locally-namess related definitions and lemmas) from language.ott. These files (def_ott.v and prop_ln.v) are already generated and included in the artifact. You can check all the proofs without these tools installed. If you want to check if the Coq definitions (in def_ott.v) are consistent with the ones provided in language.ott or tweak the definitions yourself, you need to additionally install ott and lngen. Once installed, use make clean to delete the previously generated files, and then use make coq to regenerate the files and check all the proof.

Building from Source for Rocq Proof

• Dependencies: Requires Coq 8.15.2, along with Metalib for the locally nameless infrastructure.

• Installation guide: Install Coq 8.15.2 via opam (Please refer to the official guide for detailed steps). After installation, please clone and install Metalib using the following commands:

  git clone https://github.com/plclub/metalib
  cd metalib/Metalib
  make install
  

• (Optional (only if you want to regenerate def_ott.v and prop_ln.v)) Follow the installation guidelines for Ott (forked version) and LNgen to install them.

Abella Proof

Lemmas and Theorems

Lems / Thms	Abella Name
Theorem 2	sub_wft, chkInf_wft
Theorem 3	sub_refl
Theorem 4	sub_trans
Theorem 5	chk_subsumption
Theorem 6	soundness_chk, soundness_inf, completeness_chk, completeness_inf
Theorem 8	decidablity
Lemma 11	wft_prune
Lemma 12	sub_trans_thm
Theorem 15	soundness, completeness
Theorem 16	dc_remove_j, dcl_comp_thm
Lemma 22	tex_substwl, tex_substwl_inv_l, tex_substwl_inv_r
Lemma 31	substwl_wfj, substwl_wfta
Theorem 33	wfta_weaken_ex, wfta_weaken_ty, wfta_weaken_of
Theorem 34	wfta_weaken
Lemma 35	tex_insert_monoa, tex_extract
Lemma 36	tex_move_rev_exvar
Lemma 38	tex_substwl', tex_substwl_inv_l_
Theorem 45	substwl_total
Theorem 47	sub_mono
Theorem 48	judge_weaken_list_mono
Lemma 49	substwl_i, substwl_exvar, substwl_tyvar, substwl_arr_yz, substwl_exvar_b, substwl_exvar_b', substwl_arr_yz

Usage

• Check the proofs: navigate to the supplementary/proof_abella/ directory and run make. (This might take 20 seconds to finish)

  The shell command grep -r "skip" . further confirms that no theorems/lemmas are assumed but not proven.

Building from Source for Abella Proof

• Installation guide: Install Abella 2.0.8 via opam (Please refer to the official guide for detailed steps).