diff --git a/graphs/dependency.dot b/graphs/dependency.dot index 8efbe20..4a3e429 100644 --- a/graphs/dependency.dot +++ b/graphs/dependency.dot @@ -1,110 +1,107 @@ digraph theorem_deps { rankdir=LR; bgcolor="white"; - node [fontname=Inter, fontsize=10, fontcolor="#333333"]; - edge [fontname=Inter, fontsize=8, color="#333333"]; - graph [fontname=Inter, fontsize=12, labelloc=t, label="Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M0)"]; - subgraph cluster_M0 { - label="M0"; - style="rounded"; - color="#bbbbbb"; - fontcolor="#333333"; - 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]; - 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]; - } - subgraph cluster_M1 { - label="M1"; - style="rounded"; - color="#bbbbbb"; - fontcolor="#333333"; - 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]; - 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]; - 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]; - } - subgraph cluster_M2 { - label="M2"; - style="rounded"; - color="#bbbbbb"; - fontcolor="#333333"; - 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]; - 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]; - 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]; - } - subgraph cluster_M3 { - label="M3"; - style="rounded"; - color="#bbbbbb"; - fontcolor="#333333"; - 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]; - 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]; - 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]; - 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]; - } - subgraph cluster_M4 { - label="M4"; - style="rounded"; - color="#bbbbbb"; - fontcolor="#333333"; - 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]; - 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]; - 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]; - } - subgraph cluster_M5 { - label="M5"; - style="rounded"; - color="#bbbbbb"; - fontcolor="#333333"; - 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]; - 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]; - 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]; - 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]; - 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]; - } - subgraph cluster_M6 { - label="M6"; - style="rounded"; - color="#bbbbbb"; - fontcolor="#333333"; - 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]; - 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]; - 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]; - 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]; - 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]; - 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]; - } - exec_step -> exec_examples; - exec_examples -> m1_syntax; - m1_syntax -> m1_open_close; - m1_syntax -> m1_red1; - m1_open_close -> m1_red1; - m1_red1 -> lemma_2_1_fv_preserved; - m1_red1 -> lemma_2_2_full_comp; - m1_red1 -> lemma_2_3_beta_sim; + splines=spline; + nodesep=0.22; + 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=<Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M2)
proved stated planned blocked>]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + 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]; + lift_lc -> lift_0_lc; + fvs_lift -> open_rec_fvs; + open_rec_bvar -> open_rec_fvs; + open_rec_bvar_neq -> open_rec_fvs; + open_rec_bvar -> open_close; + lift_0_lc -> subst_fvar_self; + close_rec_fvs -> subst_fvs; + open_rec_fvs -> subst_fvs; + occurs_count_zero -> occurs_count_pos; + occurs_count_false -> occurs_count_zfill_plug; + occurs_lift_self -> occurs_count_zfill_plug; + occurs_lift_self -> open_rec_zplug_lift; + open_rec_occurs_false -> open_rec_zplug_lift; + occurs_count_zero -> full_comp_aux; + occurs_count_zfill_plug -> full_comp_aux; + open_rec_occurs_false -> full_comp_aux; + open_rec_zplug_lift -> full_comp_aux; + zdecs_nonempty -> full_comp_aux; + zdecs_sound -> full_comp_aux; + full_comp_aux -> lemma_2_2_full_comp; + fvs_lift -> fvs_zplug_lift; + fvs_zplug_lift -> red1_root_fv; + 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; - m3_measure -> m3_termination; - m3_termination -> m3_local_confluence; - m1_red1 -> m3_local_confluence; - m3_local_confluence -> lemma_3_2_sub_nf_unique; - m1_red1 -> m4_par; - lemma_3_2_sub_nf_unique -> m4_par; - m4_par -> m4_par_diamond; - m4_par_diamond -> theorem_confluence_terms; - lemma_2_3_beta_sim -> theorem_confluence_terms; - m1_syntax -> m5_mvar; - m5_mvar -> m5_rx; - m1_red1 -> m5_rx; - m5_mvar -> m5_eq_C; - m5_rx -> m5_coherence; - m5_eq_C -> m5_coherence; - lemma_3_2_sub_nf_unique -> m5_coherence; - m5_coherence -> theorem_confluence_metaterms; - m4_par_diamond -> theorem_confluence_metaterms; - m1_red1 -> m6_translation; - 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; + zdecs_sound -> root_steps_sound; + zdecs_complete -> root_steps_complete; + positions_at -> steps_sound; + root_steps_sound -> steps_sound; + steps_sound -> steps_sound_red1; + positions_hole -> root_steps_in_steps; + at_ctx_comp -> steps_complete; + plug_comp -> steps_complete; + positions_comp -> steps_complete; + root_steps_complete -> steps_complete; + root_steps_in_steps -> steps_complete; + has_red_f -> has_red_spec; + steps_complete -> has_red_spec; + steps_sound -> has_red_spec; + has_red_spec -> red1_dec; + steps_sound -> corpus_sound; + steps_complete -> corpus_complete; + has_red_spec -> corpus_decides; + lemma_2_1_fv_preserved -> corpus_fv_preserved; + steps_sound_red1 -> corpus_fv_preserved; } diff --git a/graphs/dependency.png b/graphs/dependency.png index e60c57a..d0955f3 100644 Binary files a/graphs/dependency.png and b/graphs/dependency.png differ diff --git a/graphs/dependency.svg b/graphs/dependency.svg index 971167a..a8e5d14 100644 --- a/graphs/dependency.svg +++ b/graphs/dependency.svg @@ -4,490 +4,750 @@ - - + + theorem_deps - -Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M0) - -cluster_M0 - -M0 - - -cluster_M1 - -M1 - - -cluster_M2 - -M2 - - -cluster_M3 - -M3 - - -cluster_M4 - -M4 - - -cluster_M5 - -M5 - - -cluster_M6 - -M6 - - + +Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M2) +proved +    +stated +    +planned +    +blocked + -exec_step - - -exec_step +fvs_lift + + +fvs_lift - - -exec_examples - - -exec_examples + + +open_rec_fvs + + +open_rec_fvs - - -exec_step->exec_examples - - - - - -m1_syntax - - -M1 syntax/binding - - - - + -exec_examples->m1_syntax - - +fvs_lift->open_rec_fvs + + - - -m1_open_close - - -open/close laws + + +fvs_zplug_lift + + +fvs_zplug_lift - - -m1_syntax->m1_open_close - - + + +fvs_lift->fvs_zplug_lift + + - - -m1_red1 - - -red1 (B, Gc, R) + + +lift_lc + + +lift_lc - - -m1_syntax->m1_red1 - - - - - -m5_mvar - - -XΔ metaterms + + +lift_0_lc + + +lift_0_lc - - -m1_syntax->m5_mvar - - + + +lift_lc->lift_0_lc + + - - -m1_open_close->m1_red1 - - - - - -lemma_2_1_fv_preserved - - -Lemma 2.1 fv preserved + + +subst_fvar_self + + +subst_fvar_self - + -m1_red1->lemma_2_1_fv_preserved - - +lift_0_lc->subst_fvar_self + + - - -lemma_2_2_full_comp - - -Lemma 2.2 full composition + + +open_rec_bvar + + +open_rec_bvar - + + +open_rec_bvar->open_rec_fvs + + + + + +open_close + + +open_close + + + + + +open_rec_bvar->open_close + + + + + +close_rec_fvar + + +close_rec_fvar + + + + + +open_rec_occurs_false + + +open_rec_occurs_false + + + + + +open_rec_zplug_lift + + +open_rec_zplug_lift + + + + + +open_rec_occurs_false->open_rec_zplug_lift + + + + + +full_comp_aux + + +full_comp_aux + + + + + +open_rec_occurs_false->full_comp_aux + + + + + +close_rec_notin + + +close_rec_notin + + + + + +close_rec_fvs + + +close_rec_fvs + + + + + +subst_fvs + + +subst_fvs + + + + -m1_red1->lemma_2_2_full_comp - - +close_rec_fvs->subst_fvs + + + + + +open_rec_bvar_neq + + +open_rec_bvar_neq + + + + + +open_rec_bvar_neq->open_rec_fvs + + + + + +open_rec_fvs->subst_fvs + + + + + +subst_fvar_other + + +subst_fvar_other + + + + + +Plus_red1_context + + +Plus_red1_context + + - + lemma_2_3_beta_sim - - -Lemma 2.3 β-simulation + + +lemma_2_3_beta_sim - - -m1_red1->lemma_2_3_beta_sim - - + + +Plus_red1_context->lemma_2_3_beta_sim + + - - -m3_measure - - -sub measure + + +occurs_count_zero + + +occurs_count_zero - - -m1_red1->m3_measure - - - - - -m3_local_confluence - - -{R,Gc} local confluence + + +occurs_count_pos + + +occurs_count_pos - - -m1_red1->m3_local_confluence - - + + +occurs_count_zero->occurs_count_pos + + - - -m4_par - - -parallel reduction par - + + +occurs_count_zero->full_comp_aux + + - - - -m1_red1->m4_par - - - - + -m5_rx - - -RX rule +occurs_count_false + + +occurs_count_false - - -m1_red1->m5_rx - - - - + -m6_translation - - -translation to λβp +occurs_count_zfill_plug + + +occurs_count_zfill_plug - - -m1_red1->m6_translation - - + + +occurs_count_false->occurs_count_zfill_plug + + + + + +occurs_lift_self + + +occurs_lift_self + + + + + +occurs_lift_self->occurs_count_zfill_plug + + + + + +occurs_lift_self->open_rec_zplug_lift + + + + + +zdecs_nonempty + + +zdecs_nonempty + + + + + +zdecs_nonempty->full_comp_aux + + + + + +occurs_count_zfill_plug->full_comp_aux + + + + + +open_rec_zplug_lift->full_comp_aux + + + + + +lemma_2_2_full_comp + + +lemma_2_2_full_comp + + + + + +full_comp_aux->lemma_2_2_full_comp + + - -lemma_2_2_full_comp->lemma_2_3_beta_sim - - - - - -theorem_confluence_terms - - -Confluence on terms - - - - - -lemma_2_3_beta_sim->theorem_confluence_terms - - - - - -m3_termination - - -{R,Gc} termination - - - - - -m3_measure->m3_termination - - - - - -m3_termination->m3_local_confluence - - - - - -lemma_3_2_sub_nf_unique - - -Lemma 3.2 sub NF unique - - - - - -m3_local_confluence->lemma_3_2_sub_nf_unique - - - - - -lemma_3_2_sub_nf_unique->m4_par - - - - - -m5_coherence - - -RX + =C coherence - - - - - -lemma_3_2_sub_nf_unique->m5_coherence - - - - - -m4_par_diamond - - -par diamond - - - - - -m4_par->m4_par_diamond - - - - - -m4_par_diamond->theorem_confluence_terms - - - - - -theorem_confluence_metaterms - - -Confluence on metaterms - - - - - -m4_par_diamond->theorem_confluence_metaterms - - - - - -corollary_6_21_psn - - -Cor 6.21 PSN - - - - - -theorem_confluence_terms->corollary_6_21_psn - - - - - -m5_mvar->m5_rx - - - - - -m5_eq_C - - -=C setoid - - - - - -m5_mvar->m5_eq_C - - - - - -m5_rx->m5_coherence - - - - - -m5_eq_C->m5_coherence - - - - -m5_coherence->theorem_confluence_metaterms - - +lemma_2_2_full_comp->lemma_2_3_beta_sim + + - - -m6_sn - - -SN for simply typed + + +red1_root_fv + + +red1_root_fv - + + +fvs_zplug_lift->red1_root_fv + + + + + +plug_fv_mono + + +plug_fv_mono + + + + + +red1r_fv + + +red1r_fv + + + + + +plug_fv_mono->red1r_fv + + + + + +red1_root_fv->red1r_fv + + + + + +lemma_2_1_fv_preserved + + +lemma_2_1_fv_preserved + + + + + +red1r_fv->lemma_2_1_fv_preserved + + + + + +corpus_fv_preserved + + +corpus_fv_preserved + + + + + +lemma_2_1_fv_preserved->corpus_fv_preserved + + + + + +zdecs_sound + + +zdecs_sound + + + + + +zdecs_sound->full_comp_aux + + + + + +root_steps_sound + + +root_steps_sound + + + + + +zdecs_sound->root_steps_sound + + + + + +zdecs_complete + + +zdecs_complete + + + + + +root_steps_complete + + +root_steps_complete + + + + + +zdecs_complete->root_steps_complete + + + + + +positions_at + + +positions_at + + + + + +steps_sound + + +steps_sound + + + + -m6_translation->m6_sn - - +positions_at->steps_sound + + - - -m6_intersection - - -intersection typing - - - - + -m6_sn->m6_intersection - - +root_steps_sound->steps_sound + + - - -m6_typable_sn - - -typable → SN + + +steps_complete + + +steps_complete - + + +root_steps_complete->steps_complete + + + + + +steps_sound_red1 + + +steps_sound_red1 + + + + -m6_intersection->m6_typable_sn - - +steps_sound->steps_sound_red1 + + - - -m6_sn_typable - - -SN → typable + + +has_red_spec + + +has_red_spec - - -m6_typable_sn->m6_sn_typable - - + + +steps_sound->has_red_spec + + - + + +corpus_sound + + +corpus_sound + + + + + +steps_sound->corpus_sound + + + + + +steps_sound_red1->corpus_fv_preserved + + + + + +positions_hole + + +positions_hole + + + + + +root_steps_in_steps + + +root_steps_in_steps + + + + + +positions_hole->root_steps_in_steps + + + + + +root_steps_in_steps->steps_complete + + + + + +plug_comp + + +plug_comp + + + + + +plug_comp->steps_complete + + + + + +positions_comp + + +positions_comp + + + + + +positions_comp->steps_complete + + + + + +at_ctx_comp + + +at_ctx_comp + + + + -m6_sn_typable->corollary_6_21_psn - - +at_ctx_comp->steps_complete + + + + + +steps_complete->has_red_spec + + + + + +corpus_complete + + +corpus_complete + + + + + +steps_complete->corpus_complete + + + + + +has_red_f + + +has_red_f + + + + + +has_red_f->has_red_spec + + + + + +red1_dec + + +red1_dec + + + + + +has_red_spec->red1_dec + + + + + +corpus_decides + + +corpus_decides + + + + + +has_red_spec->corpus_decides + + diff --git a/graphs/theorems.json b/graphs/theorems.json index f36a280..5f664a4 100644 --- a/graphs/theorems.json +++ b/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"], - "current": "M0", + "milestones": [ + "M1", + "M2" + ], + "current": "M2", "nodes": [ { - "id": "exec_step", - "label": "exec_step", + "id": "fvs_lift", + "label": "fvs_lift", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M1", "section": "", - "file": "theory/ExecReducer.v", + "file": "theory/Binding.v", "depends": [] }, { - "id": "exec_examples", - "label": "exec_examples", + "id": "lift_lc", + "label": "lift_lc", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M1", "section": "", - "file": "theory/ExecReducer.v", - "depends": ["exec_step"] + "file": "theory/Binding.v", + "depends": [] }, { - "id": "m1_syntax", - "label": "M1 syntax/binding", + "id": "lift_0_lc", + "label": "lift_0_lc", "kind": "infra", - "status": "planned", + "status": "proved", "milestone": "M1", - "section": "2", - "file": "", - "depends": ["exec_examples"] + "section": "", + "file": "theory/Binding.v", + "depends": [ + "lift_lc" + ] }, { - "id": "m1_open_close", - "label": "open/close laws", + "id": "open_rec_bvar", + "label": "open_rec_bvar", "kind": "infra", - "status": "planned", + "status": "proved", "milestone": "M1", - "section": "2", - "file": "", - "depends": ["m1_syntax"] + "section": "", + "file": "theory/Binding.v", + "depends": [] }, { - "id": "m1_red1", - "label": "red1 (B, Gc, R)", + "id": "close_rec_fvar", + "label": "close_rec_fvar", "kind": "infra", - "status": "planned", + "status": "proved", "milestone": "M1", - "section": "2", - "file": "", - "depends": ["m1_syntax", "m1_open_close"] + "section": "", + "file": "theory/Binding.v", + "depends": [] }, { - "id": "lemma_2_1_fv_preserved", - "label": "Lemma 2.1 fv preserved", - "kind": "paper", - "status": "planned", + "id": "open_rec_occurs_false", + "label": "open_rec_occurs_false", + "kind": "infra", + "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", - "file": "", - "depends": ["m1_red1"] + "section": "", + "file": "theory/Metatheory.v", + "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", - "file": "", - "depends": ["m1_red1"] + "section": "2.2", + "file": "theory/Metatheory.v", + "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", - "file": "", - "depends": ["m1_red1", "lemma_2_2_full_comp"] + "section": "2.3", + "file": "theory/Metatheory.v", + "depends": [ + "Plus_red1_context", + "lemma_2_2_full_comp" + ] }, { - "id": "m3_measure", - "label": "sub measure", + "id": "zdecs_sound", + "label": "zdecs_sound", "kind": "infra", - "status": "planned", - "milestone": "M3", - "section": "A", - "file": "", - "depends": ["m1_red1"] + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [] }, { - "id": "m3_termination", - "label": "{R,Gc} termination", - "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", + "id": "zdecs_complete", + "label": "zdecs_complete", "kind": "infra", - "status": "planned", - "milestone": "M4", - "section": "3.2", - "file": "", - "depends": ["m1_red1", "lemma_3_2_sub_nf_unique"] + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [] }, { - "id": "m4_par_diamond", - "label": "par diamond", - "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", + "id": "positions_at", + "label": "positions_at", "kind": "infra", - "status": "planned", - "milestone": "M5", - "section": "3.3", - "file": "", - "depends": ["m1_syntax"] + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [] }, { - "id": "m5_rx", - "label": "RX rule", - "kind": "paper", - "status": "planned", - "milestone": "M5", - "section": "3.3", - "file": "", - "depends": ["m5_mvar", "m1_red1"] + "id": "root_steps_sound", + "label": "root_steps_sound", + "kind": "infra", + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [ + "zdecs_sound" + ] }, { - "id": "m5_eq_C", - "label": "=C setoid", - "kind": "paper", - "status": "planned", - "milestone": "M5", - "section": "3.3", - "file": "", - "depends": ["m5_mvar"] + "id": "root_steps_complete", + "label": "root_steps_complete", + "kind": "infra", + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [ + "zdecs_complete" + ] }, { - "id": "m5_coherence", - "label": "RX + =C coherence", - "kind": "paper", - "status": "planned", - "milestone": "M5", - "section": "3.3", - "file": "", - "depends": ["m5_rx", "m5_eq_C", "lemma_3_2_sub_nf_unique"] + "id": "steps_sound", + "label": "steps_sound", + "kind": "infra", + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [ + "positions_at", + "root_steps_sound" + ] }, { - "id": "theorem_confluence_metaterms", - "label": "Confluence on metaterms", - "kind": "paper", - "status": "planned", - "milestone": "M5", - "section": "3.3", - "file": "", - "depends": ["m5_coherence", "m4_par_diamond"] + "id": "steps_sound_red1", + "label": "steps_sound_red1", + "kind": "infra", + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [ + "steps_sound" + ] }, { - "id": "m6_translation", - "label": "translation to λβp", - "kind": "paper", - "status": "planned", - "milestone": "M6", - "section": "4", - "file": "", - "depends": ["m1_red1"] + "id": "positions_hole", + "label": "positions_hole", + "kind": "infra", + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [] }, { - "id": "m6_sn", - "label": "SN for simply typed", - "kind": "paper", - "status": "planned", - "milestone": "M6", - "section": "6", - "file": "", - "depends": ["m6_translation"] + "id": "root_steps_in_steps", + "label": "root_steps_in_steps", + "kind": "infra", + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [ + "positions_hole" + ] }, { - "id": "m6_intersection", - "label": "intersection typing", - "kind": "paper", - "status": "planned", - "milestone": "M6", - "section": "6", - "file": "", - "depends": ["m6_sn"] + "id": "plug_comp", + "label": "plug_comp", + "kind": "infra", + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [] }, { - "id": "m6_typable_sn", - "label": "typable → SN", - "kind": "paper", - "status": "planned", - "milestone": "M6", - "section": "6", - "file": "", - "depends": ["m6_intersection"] + "id": "positions_comp", + "label": "positions_comp", + "kind": "infra", + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [] }, { - "id": "m6_sn_typable", - "label": "SN → typable", - "kind": "paper", - "status": "planned", - "milestone": "M6", - "section": "6", - "file": "", - "depends": ["m6_typable_sn"] + "id": "at_ctx_comp", + "label": "at_ctx_comp", + "kind": "infra", + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [] }, { - "id": "corollary_6_21_psn", - "label": "Cor 6.21 PSN", - "kind": "paper", - "status": "planned", - "milestone": "M6", - "section": "6", - "file": "", - "depends": ["m6_sn_typable", "theorem_confluence_terms"] + "id": "steps_complete", + "label": "steps_complete", + "kind": "infra", + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "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" + ] } ] } diff --git a/scripts/audit.sh b/scripts/audit.sh index a7f6d35..7a4166a 100755 --- a/scripts/audit.sh +++ b/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" diff --git a/scripts/difftest.sh b/scripts/difftest.sh new file mode 100755 index 0000000..3fc69fa --- /dev/null +++ b/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" diff --git a/scripts/extract_metadata.py b/scripts/extract_metadata.py index 425950f..211d60c 100755 --- a/scripts/extract_metadata.py +++ b/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( diff --git a/scripts/gen_graphs.py b/scripts/gen_graphs.py index 7dd2502..9e73456 100755 --- a/scripts/gen_graphs.py +++ b/scripts/gen_graphs.py @@ -42,48 +42,59 @@ def load(path): return json.load(f) +def esc_html(s): + return str(s).replace("&", "&").replace("<", "<").replace(">", ">") + + 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 = ( + "" + esc_html(title) + "" + "
" + "proved " + "stated " + "planned " + "blocked" + "" + ) lines = [ "digraph theorem_deps {", " rankdir=LR;", - " bgcolor=\"white\";", - " node [fontname=Inter, fontsize=10, fontcolor=\"%s\"];" % INK, - " edge [fontname=Inter, fontsize=8, color=\"%s\"];" % INK, - " graph [fontname=Inter, fontsize=12, labelloc=t, label=%s];" % q(title), + ' bgcolor="white";', + " splines=spline;", + " nodesep=0.22;", + " 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"]: - members = [n for n in nodes if n["milestone"] == ms] - if not members: - continue - lines.append(" subgraph cluster_%s {" % ms) - lines.append(" label=%s;" % q(ms)) - lines.append(" style=\"rounded\";") - lines.append(" color=\"#bbbbbb\";") - lines.append(" fontcolor=\"%s\";" % INK) - for n in members: - fill = STATUS_FILL.get(n["status"], "#f3f3f3") - pen = STATUS_PEN.get(n["status"], "#777777") - style = STATUS_STYLE.get(n["status"], "dashed") - tip = n["id"] - if n.get("section"): - tip += " (section " + n["section"] + ")" - if n.get("file"): - tip += " " + n["file"] - tip += " " + data["paper"]["html"] - attrs = [ - "label=%s" % q(n["label"]), - "color=%s" % q(pen), - "fillcolor=%s" % q(fill), - "style=%s" % q(style), - "fontcolor=%s" % q(INK), - "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: + fill = STATUS_FILL.get(n["status"], "#f3f3f3") + pen = STATUS_PEN.get(n["status"], "#777777") + style = STATUS_STYLE.get(n["status"], "dashed") + tip = n["id"] + if n.get("section"): + tip += " (section " + n["section"] + ")" + if n.get("file"): + tip += " " + n["file"] + tip += " " + data["paper"]["html"] + if n["kind"] == "paper": + shape = "box" + style = "rounded," + style + else: + shape = "ellipse" + attrs = [ + "label=%s" % q(n["label"]), + "color=%s" % q(pen), + "fillcolor=%s" % q(fill), + "style=%s" % q(style), + "fontcolor=%s" % q("#222222"), + "tooltip=%s" % q(tip), + "shape=%s" % shape, + ] + lines.append(" %s [%s];" % (n["id"], ", ".join(attrs))) for n in nodes: for d in n.get("depends", []): if d in by_id: diff --git a/theory/Tests.v b/theory/Tests.v new file mode 100644 index 0000000..1383a25 --- /dev/null +++ b/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.