add(tests): bounded conformance suite for the reducer against the relational semantics (golden corpus)

graphs/dependency.dot

@@ -1,110 +1,107 @@
 digraph theorem_deps {
   rankdir=LR;
   bgcolor="white";
-  node [fontname=Inter, fontsize=10, fontcolor="#333333"];
+  splines=spline;
-  edge [fontname=Inter, fontsize=8, color="#333333"];
+  nodesep=0.22;
-  graph [fontname=Inter, fontsize=12, labelloc=t, label="Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M0)"];
+  ranksep=0.6;
-  subgraph cluster_M0 {
+  node [fontname=Inter, fontsize=9, fontcolor="#222222"];
-    label="M0";
+  edge [fontname=Inter, fontsize=8, color="#9a9a9a", arrowsize=0.6, penwidth=0.8];
-    style="rounded";
+  graph [fontname=Inter, fontsize=12, labelloc=t, label=<<B>Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M2)</B><BR/><FONT POINT-SIZE="9"><FONT COLOR="#38761d">proved</FONT>   <FONT COLOR="#b45f06">stated</FONT>   <FONT COLOR="#777777">planned</FONT>   <FONT COLOR="#cc0000">blocked</FONT></FONT>>];
-    color="#bbbbbb";
+  fvs_lift [label="fvs_lift", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="fvs_lift theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    fontcolor="#333333";
+  lift_lc [label="lift_lc", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="lift_lc theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    exec_step [label="exec_step", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#333333", tooltip="exec_step theory/ExecReducer.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  lift_0_lc [label="lift_0_lc", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="lift_0_lc theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    exec_examples [label="exec_examples", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#333333", tooltip="exec_examples theory/ExecReducer.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  open_rec_bvar [label="open_rec_bvar", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_bvar theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-  }
+  close_rec_fvar [label="close_rec_fvar", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_fvar theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-  subgraph cluster_M1 {
+  open_rec_occurs_false [label="open_rec_occurs_false", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_occurs_false theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    label="M1";
+  close_rec_notin [label="close_rec_notin", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_notin theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    style="rounded";
+  close_rec_fvs [label="close_rec_fvs", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    color="#bbbbbb";
+  open_rec_bvar_neq [label="open_rec_bvar_neq", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_bvar_neq theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    fontcolor="#333333";
+  open_rec_fvs [label="open_rec_fvs", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    m1_syntax [label="M1 syntax/binding", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m1_syntax (section 2) https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  open_close [label="open_close", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_close theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    m1_open_close [label="open/close laws", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m1_open_close (section 2) https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  subst_fvar_self [label="subst_fvar_self", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_fvar_self theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    m1_red1 [label="red1 (B, Gc, R)", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m1_red1 (section 2) https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  subst_fvar_other [label="subst_fvar_other", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_fvar_other theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-  }
+  subst_fvs [label="subst_fvs", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_fvs theory/Binding.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-  subgraph cluster_M2 {
+  Plus_red1_context [label="Plus_red1_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_red1_context theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    label="M2";
+  occurs_count_zero [label="occurs_count_zero", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_zero theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    style="rounded";
+  occurs_count_false [label="occurs_count_false", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_false theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    color="#bbbbbb";
+  occurs_count_pos [label="occurs_count_pos", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_pos theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    fontcolor="#333333";
+  occurs_lift_self [label="occurs_lift_self", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_lift_self theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    lemma_2_1_fv_preserved [label="Lemma 2.1 fv preserved", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="lemma_2_1_fv_preserved (section 2) https://arxiv.org/html/2312.13270v1", shape=box];
+  zdecs_nonempty [label="zdecs_nonempty", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zdecs_nonempty theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    lemma_2_2_full_comp [label="Lemma 2.2 full composition", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="lemma_2_2_full_comp (section 2) https://arxiv.org/html/2312.13270v1", shape=box];
+  occurs_count_zfill_plug [label="occurs_count_zfill_plug", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_count_zfill_plug theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    lemma_2_3_beta_sim [label="Lemma 2.3 β-simulation", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="lemma_2_3_beta_sim (section 2) https://arxiv.org/html/2312.13270v1", shape=box];
+  open_rec_zplug_lift [label="open_rec_zplug_lift", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_zplug_lift theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-  }
+  full_comp_aux [label="full_comp_aux", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="full_comp_aux theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-  subgraph cluster_M3 {
+  lemma_2_2_full_comp [label="lemma_2_2_full_comp", color="#38761d", fillcolor="#d9ead3", style="rounded,filled", fontcolor="#222222", tooltip="lemma_2_2_full_comp (section 2.2) theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=box];
-    label="M3";
+  fvs_zplug_lift [label="fvs_zplug_lift", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="fvs_zplug_lift theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    style="rounded";
+  plug_fv_mono [label="plug_fv_mono", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="plug_fv_mono theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    color="#bbbbbb";
+  red1_root_fv [label="red1_root_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_root_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    fontcolor="#333333";
+  red1r_fv [label="red1r_fv", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1r_fv theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    m3_measure [label="sub measure", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m3_measure (section A) https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  lemma_2_1_fv_preserved [label="lemma_2_1_fv_preserved", color="#38761d", fillcolor="#d9ead3", style="rounded,filled", fontcolor="#222222", tooltip="lemma_2_1_fv_preserved (section 2.1) theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=box];
-    m3_termination [label="{R,Gc} termination", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m3_termination (section 3.1) https://arxiv.org/html/2312.13270v1", shape=box];
+  lemma_2_3_beta_sim [label="lemma_2_3_beta_sim", color="#38761d", fillcolor="#d9ead3", style="rounded,filled", fontcolor="#222222", tooltip="lemma_2_3_beta_sim (section 2.3) theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=box];
-    m3_local_confluence [label="{R,Gc} local confluence", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m3_local_confluence (section 3.1) https://arxiv.org/html/2312.13270v1", shape=box];
+  zdecs_sound [label="zdecs_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zdecs_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    lemma_3_2_sub_nf_unique [label="Lemma 3.2 sub NF unique", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="lemma_3_2_sub_nf_unique (section 3.1) https://arxiv.org/html/2312.13270v1", shape=box];
+  zdecs_complete [label="zdecs_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zdecs_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-  }
+  positions_at [label="positions_at", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="positions_at theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-  subgraph cluster_M4 {
+  root_steps_sound [label="root_steps_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="root_steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    label="M4";
+  root_steps_complete [label="root_steps_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="root_steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    style="rounded";
+  steps_sound [label="steps_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="steps_sound theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    color="#bbbbbb";
+  steps_sound_red1 [label="steps_sound_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="steps_sound_red1 theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    fontcolor="#333333";
+  positions_hole [label="positions_hole", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="positions_hole theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    m4_par [label="parallel reduction par", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m4_par (section 3.2) https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  root_steps_in_steps [label="root_steps_in_steps", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="root_steps_in_steps theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    m4_par_diamond [label="par diamond", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m4_par_diamond (section 3.2) https://arxiv.org/html/2312.13270v1", shape=box];
+  plug_comp [label="plug_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="plug_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    theorem_confluence_terms [label="Confluence on terms", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="theorem_confluence_terms (section 3.2) https://arxiv.org/html/2312.13270v1", shape=box];
+  positions_comp [label="positions_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="positions_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-  }
+  at_ctx_comp [label="at_ctx_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="at_ctx_comp theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-  subgraph cluster_M5 {
+  steps_complete [label="steps_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="steps_complete theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    label="M5";
+  has_red_f [label="has_red_f", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="has_red_f theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    style="rounded";
+  has_red_spec [label="has_red_spec", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="has_red_spec theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    color="#bbbbbb";
+  red1_dec [label="red1_dec", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    fontcolor="#333333";
+  corpus_sound [label="corpus_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_sound theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    m5_mvar [label="XΔ metaterms", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m5_mvar (section 3.3) https://arxiv.org/html/2312.13270v1", shape=ellipse];
+  corpus_complete [label="corpus_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_complete theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    m5_rx [label="RX rule", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m5_rx (section 3.3) https://arxiv.org/html/2312.13270v1", shape=box];
+  corpus_decides [label="corpus_decides", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_decides theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    m5_eq_C [label="=C setoid", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m5_eq_C (section 3.3) https://arxiv.org/html/2312.13270v1", shape=box];
+  corpus_fv_preserved [label="corpus_fv_preserved", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="corpus_fv_preserved theory/Tests.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
-    m5_coherence [label="RX + =C coherence", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m5_coherence (section 3.3) https://arxiv.org/html/2312.13270v1", shape=box];
+  lift_lc -> lift_0_lc;
-    theorem_confluence_metaterms [label="Confluence on metaterms", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="theorem_confluence_metaterms (section 3.3) https://arxiv.org/html/2312.13270v1", shape=box];
+  fvs_lift -> open_rec_fvs;
-  }
+  open_rec_bvar -> open_rec_fvs;
-  subgraph cluster_M6 {
+  open_rec_bvar_neq -> open_rec_fvs;
-    label="M6";
+  open_rec_bvar -> open_close;
-    style="rounded";
+  lift_0_lc -> subst_fvar_self;
-    color="#bbbbbb";
+  close_rec_fvs -> subst_fvs;
-    fontcolor="#333333";
+  open_rec_fvs -> subst_fvs;
-    m6_translation [label="translation to λβp", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_translation (section 4) https://arxiv.org/html/2312.13270v1", shape=box];
+  occurs_count_zero -> occurs_count_pos;
-    m6_sn [label="SN for simply typed", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_sn (section 6) https://arxiv.org/html/2312.13270v1", shape=box];
+  occurs_count_false -> occurs_count_zfill_plug;
-    m6_intersection [label="intersection typing", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_intersection (section 6) https://arxiv.org/html/2312.13270v1", shape=box];
+  occurs_lift_self -> occurs_count_zfill_plug;
-    m6_typable_sn [label="typable → SN", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_typable_sn (section 6) https://arxiv.org/html/2312.13270v1", shape=box];
+  occurs_lift_self -> open_rec_zplug_lift;
-    m6_sn_typable [label="SN → typable", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_sn_typable (section 6) https://arxiv.org/html/2312.13270v1", shape=box];
+  open_rec_occurs_false -> open_rec_zplug_lift;
-    corollary_6_21_psn [label="Cor 6.21 PSN", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="corollary_6_21_psn (section 6) https://arxiv.org/html/2312.13270v1", shape=box];
+  occurs_count_zero -> full_comp_aux;
-  }
+  occurs_count_zfill_plug -> full_comp_aux;
-  exec_step -> exec_examples;
+  open_rec_occurs_false -> full_comp_aux;
-  exec_examples -> m1_syntax;
+  open_rec_zplug_lift -> full_comp_aux;
-  m1_syntax -> m1_open_close;
+  zdecs_nonempty -> full_comp_aux;
-  m1_syntax -> m1_red1;
+  zdecs_sound -> full_comp_aux;
-  m1_open_close -> m1_red1;
+  full_comp_aux -> lemma_2_2_full_comp;
-  m1_red1 -> lemma_2_1_fv_preserved;
+  fvs_lift -> fvs_zplug_lift;
-  m1_red1 -> lemma_2_2_full_comp;
+  fvs_zplug_lift -> red1_root_fv;
-  m1_red1 -> lemma_2_3_beta_sim;
+  plug_fv_mono -> red1r_fv;
+  red1_root_fv -> red1r_fv;
+  red1r_fv -> lemma_2_1_fv_preserved;
+  Plus_red1_context -> lemma_2_3_beta_sim;
   lemma_2_2_full_comp -> lemma_2_3_beta_sim;
-  m1_red1 -> m3_measure;
+  zdecs_sound -> root_steps_sound;
-  m3_measure -> m3_termination;
+  zdecs_complete -> root_steps_complete;
-  m3_termination -> m3_local_confluence;
+  positions_at -> steps_sound;
-  m1_red1 -> m3_local_confluence;
+  root_steps_sound -> steps_sound;
-  m3_local_confluence -> lemma_3_2_sub_nf_unique;
+  steps_sound -> steps_sound_red1;
-  m1_red1 -> m4_par;
+  positions_hole -> root_steps_in_steps;
-  lemma_3_2_sub_nf_unique -> m4_par;
+  at_ctx_comp -> steps_complete;
-  m4_par -> m4_par_diamond;
+  plug_comp -> steps_complete;
-  m4_par_diamond -> theorem_confluence_terms;
+  positions_comp -> steps_complete;
-  lemma_2_3_beta_sim -> theorem_confluence_terms;
+  root_steps_complete -> steps_complete;
-  m1_syntax -> m5_mvar;
+  root_steps_in_steps -> steps_complete;
-  m5_mvar -> m5_rx;
+  has_red_f -> has_red_spec;
-  m1_red1 -> m5_rx;
+  steps_complete -> has_red_spec;
-  m5_mvar -> m5_eq_C;
+  steps_sound -> has_red_spec;
-  m5_rx -> m5_coherence;
+  has_red_spec -> red1_dec;
-  m5_eq_C -> m5_coherence;
+  steps_sound -> corpus_sound;
-  lemma_3_2_sub_nf_unique -> m5_coherence;
+  steps_complete -> corpus_complete;
-  m5_coherence -> theorem_confluence_metaterms;
+  has_red_spec -> corpus_decides;
-  m4_par_diamond -> theorem_confluence_metaterms;
+  lemma_2_1_fv_preserved -> corpus_fv_preserved;
-  m1_red1 -> m6_translation;
+  steps_sound_red1 -> corpus_fv_preserved;
-  m6_translation -> m6_sn;
-  m6_sn -> m6_intersection;
-  m6_intersection -> m6_typable_sn;
-  m6_typable_sn -> m6_sn_typable;
-  m6_sn_typable -> corollary_6_21_psn;
-  theorem_confluence_terms -> corollary_6_21_psn;
 }

graphs/theorems.json

@@ -1,272 +1,592 @@
 {
   "paper": {
     "title": "Milner's Lambda-Calculus with Partial Substitutions",
-    "authors": ["Delia Kesner", "Shane Ó Conchúir"],
+    "authors": [
+      "Delia Kesner",
+      "Shane Ó Conchúir"
+    ],
     "url": "https://arxiv.org/abs/2312.13270",
     "html": "https://arxiv.org/html/2312.13270v1"
   },
-  "milestones": ["M0", "M1", "M2", "M3", "M4", "M5", "M6"],
+  "milestones": [
-  "current": "M0",
+    "M1",
+    "M2"
+  ],
+  "current": "M2",
   "nodes": [
     {
-      "id": "exec_step",
+      "id": "fvs_lift",
-      "label": "exec_step",
+      "label": "fvs_lift",
       "kind": "infra",
       "status": "proved",
-      "milestone": "M0",
+      "milestone": "M1",
       "section": "",
-      "file": "theory/ExecReducer.v",
+      "file": "theory/Binding.v",
       "depends": []
     },
     {
-      "id": "exec_examples",
+      "id": "lift_lc",
-      "label": "exec_examples",
+      "label": "lift_lc",
       "kind": "infra",
       "status": "proved",
-      "milestone": "M0",
+      "milestone": "M1",
       "section": "",
-      "file": "theory/ExecReducer.v",
+      "file": "theory/Binding.v",
-      "depends": ["exec_step"]
+      "depends": []
     },
     {
-      "id": "m1_syntax",
+      "id": "lift_0_lc",
-      "label": "M1 syntax/binding",
+      "label": "lift_0_lc",
       "kind": "infra",
-      "status": "planned",
+      "status": "proved",
       "milestone": "M1",
-      "section": "2",
+      "section": "",
-      "file": "",
+      "file": "theory/Binding.v",
-      "depends": ["exec_examples"]
+      "depends": [
+        "lift_lc"
+      ]
     },
     {
-      "id": "m1_open_close",
+      "id": "open_rec_bvar",
-      "label": "open/close laws",
+      "label": "open_rec_bvar",
       "kind": "infra",
-      "status": "planned",
+      "status": "proved",
       "milestone": "M1",
-      "section": "2",
+      "section": "",
-      "file": "",
+      "file": "theory/Binding.v",
-      "depends": ["m1_syntax"]
+      "depends": []
     },
     {
-      "id": "m1_red1",
+      "id": "close_rec_fvar",
-      "label": "red1 (B, Gc, R)",
+      "label": "close_rec_fvar",
       "kind": "infra",
-      "status": "planned",
+      "status": "proved",
       "milestone": "M1",
-      "section": "2",
+      "section": "",
-      "file": "",
+      "file": "theory/Binding.v",
-      "depends": ["m1_syntax", "m1_open_close"]
+      "depends": []
     },
     {
-      "id": "lemma_2_1_fv_preserved",
+      "id": "open_rec_occurs_false",
-      "label": "Lemma 2.1 fv preserved",
+      "label": "open_rec_occurs_false",
-      "kind": "paper",
+      "kind": "infra",
-      "status": "planned",
+      "status": "proved",
+      "milestone": "M1",
+      "section": "",
+      "file": "theory/Binding.v",
+      "depends": []
+    },
+    {
+      "id": "close_rec_notin",
+      "label": "close_rec_notin",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M1",
+      "section": "",
+      "file": "theory/Binding.v",
+      "depends": []
+    },
+    {
+      "id": "close_rec_fvs",
+      "label": "close_rec_fvs",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M1",
+      "section": "",
+      "file": "theory/Binding.v",
+      "depends": []
+    },
+    {
+      "id": "open_rec_bvar_neq",
+      "label": "open_rec_bvar_neq",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M1",
+      "section": "",
+      "file": "theory/Binding.v",
+      "depends": []
+    },
+    {
+      "id": "open_rec_fvs",
+      "label": "open_rec_fvs",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M1",
+      "section": "",
+      "file": "theory/Binding.v",
+      "depends": [
+        "fvs_lift",
+        "open_rec_bvar",
+        "open_rec_bvar_neq"
+      ]
+    },
+    {
+      "id": "open_close",
+      "label": "open_close",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M1",
+      "section": "",
+      "file": "theory/Binding.v",
+      "depends": [
+        "open_rec_bvar"
+      ]
+    },
+    {
+      "id": "subst_fvar_self",
+      "label": "subst_fvar_self",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M1",
+      "section": "",
+      "file": "theory/Binding.v",
+      "depends": [
+        "lift_0_lc"
+      ]
+    },
+    {
+      "id": "subst_fvar_other",
+      "label": "subst_fvar_other",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M1",
+      "section": "",
+      "file": "theory/Binding.v",
+      "depends": []
+    },
+    {
+      "id": "subst_fvs",
+      "label": "subst_fvs",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M1",
+      "section": "",
+      "file": "theory/Binding.v",
+      "depends": [
+        "close_rec_fvs",
+        "open_rec_fvs"
+      ]
+    },
+    {
+      "id": "Plus_red1_context",
+      "label": "Plus_red1_context",
+      "kind": "infra",
+      "status": "proved",
       "milestone": "M2",
-      "section": "2",
+      "section": "",
-      "file": "",
+      "file": "theory/Metatheory.v",
-      "depends": ["m1_red1"]
+      "depends": []
+    },
+    {
+      "id": "occurs_count_zero",
+      "label": "occurs_count_zero",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Metatheory.v",
+      "depends": []
+    },
+    {
+      "id": "occurs_count_false",
+      "label": "occurs_count_false",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Metatheory.v",
+      "depends": []
+    },
+    {
+      "id": "occurs_count_pos",
+      "label": "occurs_count_pos",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Metatheory.v",
+      "depends": [
+        "occurs_count_zero"
+      ]
+    },
+    {
+      "id": "occurs_lift_self",
+      "label": "occurs_lift_self",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Metatheory.v",
+      "depends": []
+    },
+    {
+      "id": "zdecs_nonempty",
+      "label": "zdecs_nonempty",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Metatheory.v",
+      "depends": []
+    },
+    {
+      "id": "occurs_count_zfill_plug",
+      "label": "occurs_count_zfill_plug",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Metatheory.v",
+      "depends": [
+        "occurs_count_false",
+        "occurs_lift_self"
+      ]
+    },
+    {
+      "id": "open_rec_zplug_lift",
+      "label": "open_rec_zplug_lift",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Metatheory.v",
+      "depends": [
+        "occurs_lift_self",
+        "open_rec_occurs_false"
+      ]
+    },
+    {
+      "id": "full_comp_aux",
+      "label": "full_comp_aux",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Metatheory.v",
+      "depends": [
+        "occurs_count_zero",
+        "occurs_count_zfill_plug",
+        "open_rec_occurs_false",
+        "open_rec_zplug_lift",
+        "zdecs_nonempty",
+        "zdecs_sound"
+      ]
     },
     {
       "id": "lemma_2_2_full_comp",
-      "label": "Lemma 2.2 full composition",
+      "label": "lemma_2_2_full_comp",
       "kind": "paper",
-      "status": "planned",
+      "status": "proved",
       "milestone": "M2",
-      "section": "2",
+      "section": "2.2",
-      "file": "",
+      "file": "theory/Metatheory.v",
-      "depends": ["m1_red1"]
+      "depends": [
+        "full_comp_aux"
+      ]
+    },
+    {
+      "id": "fvs_zplug_lift",
+      "label": "fvs_zplug_lift",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Metatheory.v",
+      "depends": [
+        "fvs_lift"
+      ]
+    },
+    {
+      "id": "plug_fv_mono",
+      "label": "plug_fv_mono",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Metatheory.v",
+      "depends": []
+    },
+    {
+      "id": "red1_root_fv",
+      "label": "red1_root_fv",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Metatheory.v",
+      "depends": [
+        "fvs_zplug_lift"
+      ]
+    },
+    {
+      "id": "red1r_fv",
+      "label": "red1r_fv",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Metatheory.v",
+      "depends": [
+        "plug_fv_mono",
+        "red1_root_fv"
+      ]
+    },
+    {
+      "id": "lemma_2_1_fv_preserved",
+      "label": "lemma_2_1_fv_preserved",
+      "kind": "paper",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "2.1",
+      "file": "theory/Metatheory.v",
+      "depends": [
+        "red1r_fv"
+      ]
     },
     {
       "id": "lemma_2_3_beta_sim",
-      "label": "Lemma 2.3 β-simulation",
+      "label": "lemma_2_3_beta_sim",
       "kind": "paper",
-      "status": "planned",
+      "status": "proved",
       "milestone": "M2",
-      "section": "2",
+      "section": "2.3",
-      "file": "",
+      "file": "theory/Metatheory.v",
-      "depends": ["m1_red1", "lemma_2_2_full_comp"]
+      "depends": [
+        "Plus_red1_context",
+        "lemma_2_2_full_comp"
+      ]
     },
     {
-      "id": "m3_measure",
+      "id": "zdecs_sound",
-      "label": "sub measure",
+      "label": "zdecs_sound",
       "kind": "infra",
-      "status": "planned",
+      "status": "proved",
-      "milestone": "M3",
+      "milestone": "M1",
-      "section": "A",
+      "section": "",
-      "file": "",
+      "file": "theory/Reduction.v",
-      "depends": ["m1_red1"]
+      "depends": []
     },
     {
-      "id": "m3_termination",
+      "id": "zdecs_complete",
-      "label": "{R,Gc} termination",
+      "label": "zdecs_complete",
-      "kind": "paper",
-      "status": "planned",
-      "milestone": "M3",
-      "section": "3.1",
-      "file": "",
-      "depends": ["m3_measure"]
-    },
-    {
-      "id": "m3_local_confluence",
-      "label": "{R,Gc} local confluence",
-      "kind": "paper",
-      "status": "planned",
-      "milestone": "M3",
-      "section": "3.1",
-      "file": "",
-      "depends": ["m3_termination", "m1_red1"]
-    },
-    {
-      "id": "lemma_3_2_sub_nf_unique",
-      "label": "Lemma 3.2 sub NF unique",
-      "kind": "paper",
-      "status": "planned",
-      "milestone": "M3",
-      "section": "3.1",
-      "file": "",
-      "depends": ["m3_local_confluence"]
-    },
-    {
-      "id": "m4_par",
-      "label": "parallel reduction par",
       "kind": "infra",
-      "status": "planned",
+      "status": "proved",
-      "milestone": "M4",
+      "milestone": "M1",
-      "section": "3.2",
+      "section": "",
-      "file": "",
+      "file": "theory/Reduction.v",
-      "depends": ["m1_red1", "lemma_3_2_sub_nf_unique"]
+      "depends": []
     },
     {
-      "id": "m4_par_diamond",
+      "id": "positions_at",
-      "label": "par diamond",
+      "label": "positions_at",
-      "kind": "paper",
-      "status": "planned",
-      "milestone": "M4",
-      "section": "3.2",
-      "file": "",
-      "depends": ["m4_par"]
-    },
-    {
-      "id": "theorem_confluence_terms",
-      "label": "Confluence on terms",
-      "kind": "paper",
-      "status": "planned",
-      "milestone": "M4",
-      "section": "3.2",
-      "file": "",
-      "depends": ["m4_par_diamond", "lemma_2_3_beta_sim"]
-    },
-    {
-      "id": "m5_mvar",
-      "label": "XΔ metaterms",
       "kind": "infra",
-      "status": "planned",
+      "status": "proved",
-      "milestone": "M5",
+      "milestone": "M1",
-      "section": "3.3",
+      "section": "",
-      "file": "",
+      "file": "theory/Reduction.v",
-      "depends": ["m1_syntax"]
+      "depends": []
     },
     {
-      "id": "m5_rx",
+      "id": "root_steps_sound",
-      "label": "RX rule",
+      "label": "root_steps_sound",
-      "kind": "paper",
+      "kind": "infra",
-      "status": "planned",
+      "status": "proved",
-      "milestone": "M5",
+      "milestone": "M1",
-      "section": "3.3",
+      "section": "",
-      "file": "",
+      "file": "theory/Reduction.v",
-      "depends": ["m5_mvar", "m1_red1"]
+      "depends": [
+        "zdecs_sound"
+      ]
     },
     {
-      "id": "m5_eq_C",
+      "id": "root_steps_complete",
-      "label": "=C setoid",
+      "label": "root_steps_complete",
-      "kind": "paper",
+      "kind": "infra",
-      "status": "planned",
+      "status": "proved",
-      "milestone": "M5",
+      "milestone": "M1",
-      "section": "3.3",
+      "section": "",
-      "file": "",
+      "file": "theory/Reduction.v",
-      "depends": ["m5_mvar"]
+      "depends": [
+        "zdecs_complete"
+      ]
     },
     {
-      "id": "m5_coherence",
+      "id": "steps_sound",
-      "label": "RX + =C coherence",
+      "label": "steps_sound",
-      "kind": "paper",
+      "kind": "infra",
-      "status": "planned",
+      "status": "proved",
-      "milestone": "M5",
+      "milestone": "M1",
-      "section": "3.3",
+      "section": "",
-      "file": "",
+      "file": "theory/Reduction.v",
-      "depends": ["m5_rx", "m5_eq_C", "lemma_3_2_sub_nf_unique"]
+      "depends": [
+        "positions_at",
+        "root_steps_sound"
+      ]
     },
     {
-      "id": "theorem_confluence_metaterms",
+      "id": "steps_sound_red1",
-      "label": "Confluence on metaterms",
+      "label": "steps_sound_red1",
-      "kind": "paper",
+      "kind": "infra",
-      "status": "planned",
+      "status": "proved",
-      "milestone": "M5",
+      "milestone": "M1",
-      "section": "3.3",
+      "section": "",
-      "file": "",
+      "file": "theory/Reduction.v",
-      "depends": ["m5_coherence", "m4_par_diamond"]
+      "depends": [
+        "steps_sound"
+      ]
     },
     {
-      "id": "m6_translation",
+      "id": "positions_hole",
-      "label": "translation to λβp",
+      "label": "positions_hole",
-      "kind": "paper",
+      "kind": "infra",
-      "status": "planned",
+      "status": "proved",
-      "milestone": "M6",
+      "milestone": "M1",
-      "section": "4",
+      "section": "",
-      "file": "",
+      "file": "theory/Reduction.v",
-      "depends": ["m1_red1"]
+      "depends": []
     },
     {
-      "id": "m6_sn",
+      "id": "root_steps_in_steps",
-      "label": "SN for simply typed",
+      "label": "root_steps_in_steps",
-      "kind": "paper",
+      "kind": "infra",
-      "status": "planned",
+      "status": "proved",
-      "milestone": "M6",
+      "milestone": "M1",
-      "section": "6",
+      "section": "",
-      "file": "",
+      "file": "theory/Reduction.v",
-      "depends": ["m6_translation"]
+      "depends": [
+        "positions_hole"
+      ]
     },
     {
-      "id": "m6_intersection",
+      "id": "plug_comp",
-      "label": "intersection typing",
+      "label": "plug_comp",
-      "kind": "paper",
+      "kind": "infra",
-      "status": "planned",
+      "status": "proved",
-      "milestone": "M6",
+      "milestone": "M1",
-      "section": "6",
+      "section": "",
-      "file": "",
+      "file": "theory/Reduction.v",
-      "depends": ["m6_sn"]
+      "depends": []
     },
     {
-      "id": "m6_typable_sn",
+      "id": "positions_comp",
-      "label": "typable → SN",
+      "label": "positions_comp",
-      "kind": "paper",
+      "kind": "infra",
-      "status": "planned",
+      "status": "proved",
-      "milestone": "M6",
+      "milestone": "M1",
-      "section": "6",
+      "section": "",
-      "file": "",
+      "file": "theory/Reduction.v",
-      "depends": ["m6_intersection"]
+      "depends": []
     },
     {
-      "id": "m6_sn_typable",
+      "id": "at_ctx_comp",
-      "label": "SN → typable",
+      "label": "at_ctx_comp",
-      "kind": "paper",
+      "kind": "infra",
-      "status": "planned",
+      "status": "proved",
-      "milestone": "M6",
+      "milestone": "M1",
-      "section": "6",
+      "section": "",
-      "file": "",
+      "file": "theory/Reduction.v",
-      "depends": ["m6_typable_sn"]
+      "depends": []
     },
     {
-      "id": "corollary_6_21_psn",
+      "id": "steps_complete",
-      "label": "Cor 6.21 PSN",
+      "label": "steps_complete",
-      "kind": "paper",
+      "kind": "infra",
-      "status": "planned",
+      "status": "proved",
-      "milestone": "M6",
+      "milestone": "M1",
-      "section": "6",
+      "section": "",
-      "file": "",
+      "file": "theory/Reduction.v",
-      "depends": ["m6_sn_typable", "theorem_confluence_terms"]
+      "depends": [
+        "at_ctx_comp",
+        "plug_comp",
+        "positions_comp",
+        "root_steps_complete",
+        "root_steps_in_steps"
+      ]
+    },
+    {
+      "id": "has_red_f",
+      "label": "has_red_f",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M1",
+      "section": "",
+      "file": "theory/Reduction.v",
+      "depends": []
+    },
+    {
+      "id": "has_red_spec",
+      "label": "has_red_spec",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M1",
+      "section": "",
+      "file": "theory/Reduction.v",
+      "depends": [
+        "has_red_f",
+        "steps_complete",
+        "steps_sound"
+      ]
+    },
+    {
+      "id": "red1_dec",
+      "label": "red1_dec",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M1",
+      "section": "",
+      "file": "theory/Reduction.v",
+      "depends": [
+        "has_red_spec"
+      ]
+    },
+    {
+      "id": "corpus_sound",
+      "label": "corpus_sound",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Tests.v",
+      "depends": [
+        "steps_sound"
+      ]
+    },
+    {
+      "id": "corpus_complete",
+      "label": "corpus_complete",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Tests.v",
+      "depends": [
+        "steps_complete"
+      ]
+    },
+    {
+      "id": "corpus_decides",
+      "label": "corpus_decides",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Tests.v",
+      "depends": [
+        "has_red_spec"
+      ]
+    },
+    {
+      "id": "corpus_fv_preserved",
+      "label": "corpus_fv_preserved",
+      "kind": "infra",
+      "status": "proved",
+      "milestone": "M2",
+      "section": "",
+      "file": "theory/Tests.v",
+      "depends": [
+        "lemma_2_1_fv_preserved",
+        "steps_sound_red1"
+      ]
     }
   ]
 }

scripts/audit.sh

@@ -33,9 +33,11 @@ while IFS= read -r -d '' f; do
 done < <(find theory -name '*.v' -print0 2>/dev/null)
 
 echo "== Print Assumptions =="
-for f in ExecReducer Binding Reduction; do
+WORK="$(mktemp -d ./.audit-work.XXXXXX)"
+cp theory/*.v "$WORK"/
+for f in ExecReducer Binding Reduction Metatheory Tests; do
   echo "-- $f"
-  out="$(rocq compile -Q theory LambdaSub "theory/$f.v" 2>&1 || true)"
+  out="$(rocq compile -Q "$WORK" LambdaSub "$WORK/$f.v" 2>&1 || true)"
   echo "$out"
   if echo "$out" | grep -q "Axioms:"; then
     echo "unexpected axioms reported in $f" >&2
@@ -46,6 +48,7 @@ for f in ExecReducer Binding Reduction; do
     fail=1
   fi
 done
+rm -rf "$WORK"
 
 if [ "$fail" -ne 0 ]; then
   echo "AUDIT FAIL"

scripts/difftest.sh

@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+set -euo pipefail
+ROOT="$(cd "$(dirname "$0")/.." && pwd)"
+cd "$ROOT"
+
+if ! command -v rocq >/dev/null 2>&1; then
+  if command -v opam >/dev/null 2>&1; then
+    eval "$(opam env --switch=rocq-system --set-switch 2>/dev/null || true)"
+  fi
+fi
+
+if ! command -v rocq >/dev/null 2>&1; then
+  echo "rocq not on PATH; run: eval \$(opam env --switch=rocq-system --set-switch)" >&2
+  exit 1
+fi
+
+dune build
+./scripts/audit.sh
+echo "CONFORMANCE OK: 7 term corpus checked against the relational semantics by theory/Tests.v"
+echo "DIFFTEST OK"

scripts/extract_metadata.py

@@ -85,7 +85,7 @@ def extract(theory_dir):
         with open(path, "r", encoding="utf-8") as fh:
             text = fh.read()
         for decl in split_decls(text):
-            if decl["kind"] not in ("Lemma", "Theorem", "Corollary", "Proposition", "Example"):
+            if decl["kind"] not in ("Lemma", "Theorem", "Corollary", "Proposition"):
                 continue
             name = decl["name"]
             nodes.append(

scripts/gen_graphs.py

@@ -42,48 +42,59 @@ def load(path):
         return json.load(f)
 
 
+def esc_html(s):
+    return str(s).replace("&", "&amp;").replace("<", "&lt;").replace(">", "&gt;")
+
+
 def dependency_dot(data):
     nodes = data["nodes"]
     by_id = {n["id"]: n for n in nodes}
     title = data["paper"]["title"] + " - theorem dependency (" + data["current"] + ")"
+    legend = (
+        "<B>" + esc_html(title) + "</B>"
+        "<BR/><FONT POINT-SIZE=\"9\">"
+        "<FONT COLOR=\"#38761d\">proved</FONT>   "
+        "<FONT COLOR=\"#b45f06\">stated</FONT>   "
+        "<FONT COLOR=\"#777777\">planned</FONT>   "
+        "<FONT COLOR=\"#cc0000\">blocked</FONT>"
+        "</FONT>"
+    )
     lines = [
         "digraph theorem_deps {",
         "  rankdir=LR;",
-        "  bgcolor=\"white\";",
+        '  bgcolor="white";',
-        "  node [fontname=Inter, fontsize=10, fontcolor=\"%s\"];" % INK,
+        "  splines=spline;",
-        "  edge [fontname=Inter, fontsize=8, color=\"%s\"];" % INK,
+        "  nodesep=0.22;",
-        "  graph [fontname=Inter, fontsize=12, labelloc=t, label=%s];" % q(title),
+        "  ranksep=0.6;",
+        '  node [fontname=Inter, fontsize=9, fontcolor="#222222"];',
+        '  edge [fontname=Inter, fontsize=8, color="#9a9a9a", arrowsize=0.6, penwidth=0.8];',
+        "  graph [fontname=Inter, fontsize=12, labelloc=t, label=<%s>];" % legend,
     ]
-    for ms in data["milestones"]:
+    for n in nodes:
-        members = [n for n in nodes if n["milestone"] == ms]
+        fill = STATUS_FILL.get(n["status"], "#f3f3f3")
-        if not members:
+        pen = STATUS_PEN.get(n["status"], "#777777")
-            continue
+        style = STATUS_STYLE.get(n["status"], "dashed")
-        lines.append("  subgraph cluster_%s {" % ms)
+        tip = n["id"]
-        lines.append("    label=%s;" % q(ms))
+        if n.get("section"):
-        lines.append("    style=\"rounded\";")
+            tip += " (section " + n["section"] + ")"
-        lines.append("    color=\"#bbbbbb\";")
+        if n.get("file"):
-        lines.append("    fontcolor=\"%s\";" % INK)
+            tip += " " + n["file"]
-        for n in members:
+        tip += " " + data["paper"]["html"]
-            fill = STATUS_FILL.get(n["status"], "#f3f3f3")
+        if n["kind"] == "paper":
-            pen = STATUS_PEN.get(n["status"], "#777777")
+            shape = "box"
-            style = STATUS_STYLE.get(n["status"], "dashed")
+            style = "rounded," + style
-            tip = n["id"]
+        else:
-            if n.get("section"):
+            shape = "ellipse"
-                tip += " (section " + n["section"] + ")"
+        attrs = [
-            if n.get("file"):
+            "label=%s" % q(n["label"]),
-                tip += " " + n["file"]
+            "color=%s" % q(pen),
-            tip += " " + data["paper"]["html"]
+            "fillcolor=%s" % q(fill),
-            attrs = [
+            "style=%s" % q(style),
-                "label=%s" % q(n["label"]),
+            "fontcolor=%s" % q("#222222"),
-                "color=%s" % q(pen),
+            "tooltip=%s" % q(tip),
-                "fillcolor=%s" % q(fill),
+            "shape=%s" % shape,
-                "style=%s" % q(style),
+        ]
-                "fontcolor=%s" % q(INK),
+        lines.append("  %s [%s];" % (n["id"], ", ".join(attrs)))
-                "tooltip=%s" % q(tip),
-                "shape=%s" % ("box" if n["kind"] == "paper" else "ellipse"),
-            ]
-            lines.append("    %s [%s];" % (n["id"], ", ".join(attrs)))
-        lines.append("  }")
     for n in nodes:
         for d in n.get("depends", []):
             if d in by_id:

theory/Tests.v

@@ -0,0 +1,77 @@
+From Stdlib Require Import List Bool Arith Lia PeanoNat.
+Import ListNotations.
+From LambdaSub Require Import ExecReducer Binding Reduction Metatheory.
+
+Definition t_id : trm := App (Lam (BVar 0)) (FVar 1).
+Definition t_dup : trm := App (Lam (App (BVar 0) (BVar 0))) (FVar 1).
+Definition t_dup_es : trm := ESub (App (BVar 0) (BVar 0)) (FVar 1).
+Definition t_gc : trm := ESub (FVar 2) (FVar 1).
+Definition t_nested : trm := ESub (ESub (BVar 0) (FVar 1)) (FVar 2).
+Definition t_capture : trm := App (Lam (Lam (BVar 1))) (FVar 1).
+Definition t_under : trm := ESub (Lam (BVar 1)) (FVar 2).
+
+Definition corpus : list trm :=
+  [t_id; t_dup; t_dup_es; t_gc; t_nested; t_capture; t_under].
+
+Example g_id_beta : has_rule RB (steps t_id) = true.
+Proof. reflexivity. Qed.
+
+Example g_dup_beta : has_rule RB (steps t_dup) = true.
+Proof. reflexivity. Qed.
+
+Example g_dup_es_two_R : count_rule RR (steps t_dup_es) = 2.
+Proof. reflexivity. Qed.
+
+Example g_dup_es_no_Gc : has_rule RGc (steps t_dup_es) = false.
+Proof. reflexivity. Qed.
+
+Example g_gc_gc : has_rule RGc (steps t_gc) = true.
+Proof. reflexivity. Qed.
+
+Example g_gc_no_R : has_rule RR (steps t_gc) = false.
+Proof. reflexivity. Qed.
+
+Example g_nested_gc : has_rule RGc (steps t_nested) = true.
+Proof. reflexivity. Qed.
+
+Example g_under_R : has_rule RR (steps t_under) = true.
+Proof. reflexivity. Qed.
+
+Example g_capture_beta : has_rule RB (steps t_capture) = true.
+Proof. reflexivity. Qed.
+
+Example g_normal_var : normal_form (FVar 5) = true.
+Proof. reflexivity. Qed.
+
+Example g_normal_lam : normal_form (Lam (BVar 0)) = true.
+Proof. reflexivity. Qed.
+
+Example g_capture_avoid_lam : subst 0 (FVar 1) (Lam (Lam (BVar 1))) = Lam (Lam (BVar 1)).
+Proof. reflexivity. Qed.
+
+Example g_capture_avoid_es : subst 0 (FVar 1) (ESub (FVar 0) (FVar 2)) = ESub (FVar 1) (FVar 2).
+Proof. reflexivity. Qed.
+
+Example g_occurs0_lam : occurs0 (Lam (BVar 0)) = false.
+Proof. reflexivity. Qed.
+
+Example g_occurs0_bvar : occurs0 (BVar 0) = true.
+Proof. reflexivity. Qed.
+
+Lemma corpus_sound : forall t p, In t corpus -> In p (steps t) -> red1r (fst p) t (snd p).
+Proof. intros t [r s] _ H. simpl. apply steps_sound. exact H. Qed.
+
+Lemma corpus_complete : forall t r t', In t corpus -> red1r r t t' -> In (r,t') (steps t).
+Proof. intros t r t' _ H. apply steps_complete. exact H. Qed.
+
+Lemma corpus_decides : forall t t', In t corpus -> has_red t t' = true <-> red1 t t'.
+Proof. intros t t' _. apply has_red_spec. Qed.
+
+Lemma corpus_fv_preserved : forall t p, In t corpus -> In p (steps t) ->
+  incl (fvs (snd p)) (fvs t).
+Proof. intros t [r s] _ H. simpl. apply (lemma_2_1_fv_preserved t s). exact (steps_sound_red1 t r s H). Qed.
+
+Print Assumptions corpus_sound.
+Print Assumptions corpus_complete.
+Print Assumptions corpus_decides.
+Print Assumptions corpus_fv_preserved.