diff --git a/graphs/dependency.dot b/graphs/dependency.dot index 2b856c8..3171ae0 100644 --- a/graphs/dependency.dot +++ b/graphs/dependency.dot @@ -6,7 +6,7 @@ digraph theorem_deps { 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>]; + graph [fontname=Inter, fontsize=12, labelloc=t, label=<Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M4)
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]; @@ -21,6 +21,17 @@ digraph theorem_deps { 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]; + Star_trans [label="Star_trans", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Star_trans theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + red1_star [label="red1_star", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_star theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + Plus_to_Star [label="Plus_to_Star", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_to_Star theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + Star_red1_context [label="Star_red1_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Star_red1_context theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + star_one_trans [label="star_one_trans", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="star_one_trans theory/Closure.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + in_comb [label="in_comb", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="in_comb theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + pow2_pos [label="pow2_pos", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="pow2_pos theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + size_all_terms [label="size_all_terms", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="size_all_terms theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + enumerate_check [label="enumerate_check", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="enumerate_check theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + enumerate_sound [label="enumerate_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="enumerate_sound theory/Enumerate.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + enumerate_complete [label="enumerate_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="enumerate_complete theory/Enumerate.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]; @@ -37,6 +48,8 @@ digraph theorem_deps { 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]; + Plus_trans [label="Plus_trans", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_trans theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + Plus_step_trans [label="Plus_step_trans", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Plus_step_trans theory/Metatheory.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; par_red1_iff [label="par_red1_iff", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_red1_iff theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; red1_in_par [label="red1_in_par", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_in_par theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; par_context [label="par_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_context theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; @@ -65,6 +78,9 @@ digraph theorem_deps { 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]; + nf_iff_steps_nil [label="nf_iff_steps_nil", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nf_iff_steps_nil theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + normal_form_iff_nf [label="normal_form_iff_nf", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="normal_form_iff_nf theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + nf_dec [label="nf_dec", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="nf_dec theory/Reduction.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; open_rec_app [label="open_rec_app", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; open_rec_lam [label="open_rec_lam", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; open_rec_esub [label="open_rec_esub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; @@ -77,6 +93,8 @@ digraph theorem_deps { subst_notin [label="subst_notin", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_notin theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; subst_lc_self [label="subst_lc_self", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_lc_self theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; subst_other [label="subst_other", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_other theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + open_rec_lc_atom [label="open_rec_lc_atom", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_lc_atom theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + open_rec_lc [label="open_rec_lc", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="open_rec_lc theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; red_sub_root_to_red1 [label="red_sub_root_to_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_root_to_red1 theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; red_sub_to_red1 [label="red_sub_to_red1", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_to_red1 theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; red_sub_context [label="red_sub_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; @@ -85,6 +103,14 @@ digraph theorem_deps { occurs_zfill [label="occurs_zfill", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="occurs_zfill theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; zfill_occurs0 [label="zfill_occurs0", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="zfill_occurs0 theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; R_Gc_disjoint [label="R_Gc_disjoint", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="R_Gc_disjoint theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + Star_red_sub_context [label="Star_red_sub_context", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="Star_red_sub_context theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + full_comp_aux_sub [label="full_comp_aux_sub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="full_comp_aux_sub theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + plus_red_sub_full_comp [label="plus_red_sub_full_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="plus_red_sub_full_comp theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + star_red_sub_full_comp [label="star_red_sub_full_comp", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="star_red_sub_full_comp theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + es_count_plug_mono [label="es_count_plug_mono", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="es_count_plug_mono theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + red_gc_measure [label="red_gc_measure", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_gc_measure theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + red_gc_terminates [label="red_gc_terminates", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_gc_terminates theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + red_gc_to_red_sub [label="red_gc_to_red_sub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_gc_to_red_sub theory/Subsystem.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]; @@ -97,6 +123,11 @@ digraph theorem_deps { lift_0_lc -> subst_fvar_self; close_rec_fvs -> subst_fvs; open_rec_fvs -> subst_fvs; + in_comb -> size_all_terms; + pow2_pos -> size_all_terms; + check_all_true -> enumerate_check; + steps_sound -> enumerate_sound; + steps_complete -> enumerate_complete; occurs_count_zero -> occurs_count_pos; occurs_count_false -> occurs_count_zfill_plug; occurs_lift_self -> occurs_count_zfill_plug; @@ -140,13 +171,33 @@ digraph theorem_deps { steps_complete -> has_red_spec; steps_sound -> has_red_spec; has_red_spec -> red1_dec; + steps_complete -> nf_iff_steps_nil; + steps_sound_red1 -> nf_iff_steps_nil; + nf_iff_steps_nil -> normal_form_iff_nf; + nf_iff_steps_nil -> nf_dec; close_rec_notin -> subst_notin; open_rec_occurs_false -> subst_notin; subst_fvar_self -> subst_lc_self; subst_fvar_other -> subst_other; + open_rec_lc_atom -> open_rec_lc; red_sub_root_to_red1 -> red_sub_to_red1; occurs_zfill -> zfill_occurs0; zfill_occurs0 -> R_Gc_disjoint; + red_sub_context -> Star_red_sub_context; + occurs_count_zero -> full_comp_aux_sub; + occurs_count_zfill_plug -> full_comp_aux_sub; + open_rec_occurs_false -> full_comp_aux_sub; + open_rec_zplug_lift -> full_comp_aux_sub; + red_sub_gc -> full_comp_aux_sub; + red_sub_r -> full_comp_aux_sub; + zdecs_nonempty -> full_comp_aux_sub; + zdecs_sound -> full_comp_aux_sub; + full_comp_aux_sub -> plus_red_sub_full_comp; + Plus_to_Star -> star_red_sub_full_comp; + plus_red_sub_full_comp -> star_red_sub_full_comp; + es_count_plug_mono -> red_gc_measure; + red_gc_measure -> red_gc_terminates; + red_sub_gc -> red_gc_to_red_sub; steps_sound -> corpus_sound; steps_complete -> corpus_complete; has_red_spec -> corpus_decides; diff --git a/graphs/dependency.png b/graphs/dependency.png index b319001..f78ac40 100644 Binary files a/graphs/dependency.png and b/graphs/dependency.png differ diff --git a/graphs/dependency.svg b/graphs/dependency.svg index ca398b7..aa81263 100644 --- a/graphs/dependency.svg +++ b/graphs/dependency.svg @@ -4,25 +4,25 @@ - - + + theorem_deps - -Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M2) -proved -    -stated -    -planned -    -blocked + +Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M4) +proved +    +stated +    +planned +    +blocked fvs_lift - -fvs_lift + +fvs_lift @@ -30,38 +30,38 @@ open_rec_fvs - -open_rec_fvs + +open_rec_fvs fvs_lift->open_rec_fvs - - + + - + fvs_zplug_lift - - -fvs_zplug_lift + + +fvs_zplug_lift - + fvs_lift->fvs_zplug_lift - - + + lift_lc - -lift_lc + +lift_lc @@ -69,68 +69,68 @@ lift_0_lc - -lift_0_lc + +lift_0_lc lift_lc->lift_0_lc - - + + subst_fvar_self - -subst_fvar_self + +subst_fvar_self lift_0_lc->subst_fvar_self - - + + open_rec_bvar - -open_rec_bvar + +open_rec_bvar open_rec_bvar->open_rec_fvs - - + + open_close - -open_close + +open_close open_rec_bvar->open_close - - + + close_rec_fvar - -close_rec_fvar + +close_rec_fvar @@ -138,55 +138,70 @@ open_rec_occurs_false - -open_rec_occurs_false + +open_rec_occurs_false - + open_rec_zplug_lift - - -open_rec_zplug_lift + + +open_rec_zplug_lift - + open_rec_occurs_false->open_rec_zplug_lift - - + + - + full_comp_aux - - -full_comp_aux + + +full_comp_aux - + open_rec_occurs_false->full_comp_aux - - + + - + subst_notin - + subst_notin - + open_rec_occurs_false->subst_notin - - + + + + + +full_comp_aux_sub + + +full_comp_aux_sub + + + + + +open_rec_occurs_false->full_comp_aux_sub + + @@ -198,7 +213,7 @@ - + close_rec_notin->subst_notin @@ -207,8 +222,8 @@ close_rec_fvs - -close_rec_fvs + +close_rec_fvs @@ -216,922 +231,1291 @@ subst_fvs - -subst_fvs + +subst_fvs close_rec_fvs->subst_fvs - - + + open_rec_bvar_neq - -open_rec_bvar_neq + +open_rec_bvar_neq open_rec_bvar_neq->open_rec_fvs - - + + open_rec_fvs->subst_fvs - - + + - + subst_lc_self - - -subst_lc_self + + +subst_lc_self - + subst_fvar_self->subst_lc_self - - + + subst_fvar_other - -subst_fvar_other + +subst_fvar_other - + subst_other - - -subst_other + + +subst_other - + subst_fvar_other->subst_other - - + + + + + +Star_trans + + +Star_trans + + + + + +red1_star + + +red1_star + + + + + +Plus_to_Star + + +Plus_to_Star + + + + + +star_red_sub_full_comp + + +star_red_sub_full_comp + + + + + +Plus_to_Star->star_red_sub_full_comp + + + + + +Star_red1_context + + +Star_red1_context + + + + + +star_one_trans + + +star_one_trans + + + + + +in_comb + + +in_comb + + + + + +size_all_terms + + +size_all_terms + + + + + +in_comb->size_all_terms + + + + + +pow2_pos + + +pow2_pos + + + + + +pow2_pos->size_all_terms + + + + + +enumerate_check + + +enumerate_check + + + + + +enumerate_sound + + +enumerate_sound + + + + + +enumerate_complete + + +enumerate_complete + + - + Plus_red1_context - - -Plus_red1_context + + +Plus_red1_context - + lemma_2_3_beta_sim - - -lemma_2_3_beta_sim + + +lemma_2_3_beta_sim - + Plus_red1_context->lemma_2_3_beta_sim - - + + - + occurs_count_zero - - -occurs_count_zero + + +occurs_count_zero - + occurs_count_pos - - -occurs_count_pos + + +occurs_count_pos - + occurs_count_zero->occurs_count_pos - - + + - + occurs_count_zero->full_comp_aux - - + + + + + +occurs_count_zero->full_comp_aux_sub + + - + occurs_count_false - - -occurs_count_false + + +occurs_count_false - + occurs_count_zfill_plug - - -occurs_count_zfill_plug + + +occurs_count_zfill_plug - + occurs_count_false->occurs_count_zfill_plug - - + + - + occurs_lift_self - - -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 - + zdecs_nonempty->full_comp_aux - - + + + + + +zdecs_nonempty->full_comp_aux_sub + + - + occurs_count_zfill_plug->full_comp_aux - - + + + + + +occurs_count_zfill_plug->full_comp_aux_sub + + - + open_rec_zplug_lift->full_comp_aux - - + + + + + +open_rec_zplug_lift->full_comp_aux_sub + + - + lemma_2_2_full_comp - - -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 - - + + - + red1_root_fv - - -red1_root_fv + + +red1_root_fv - + fvs_zplug_lift->red1_root_fv - - + + - + plug_fv_mono - - -plug_fv_mono + + +plug_fv_mono - + red1r_fv - - -red1r_fv + + +red1r_fv - + plug_fv_mono->red1r_fv - - + + - + red1_root_fv->red1r_fv - - + + - + lemma_2_1_fv_preserved - - -lemma_2_1_fv_preserved + + +lemma_2_1_fv_preserved - + red1r_fv->lemma_2_1_fv_preserved - - + + - + gen_fv_preserved - - -gen_fv_preserved + + +gen_fv_preserved - + lemma_2_1_fv_preserved->gen_fv_preserved - - + + - + corpus_fv_preserved - - -corpus_fv_preserved + + +corpus_fv_preserved - + lemma_2_1_fv_preserved->corpus_fv_preserved - - + + + + + +Plus_trans + + +Plus_trans + + + + + +Plus_step_trans + + +Plus_step_trans + + - + par_red1_iff - - -par_red1_iff + + +par_red1_iff - + par_to_red1_or_eq - - -par_to_red1_or_eq + + +par_to_red1_or_eq - + par_red1_iff->par_to_red1_or_eq - - + + - + red1_or_eq_to_par - - -red1_or_eq_to_par + + +red1_or_eq_to_par - + par_red1_iff->red1_or_eq_to_par - - + + - + red1_in_par - - -red1_in_par + + +red1_in_par - + par_context - - -par_context + + +par_context - + par_reflexive - - -par_reflexive + + +par_reflexive - + gen_list_length - - -gen_list_length + + +gen_list_length - + check_term_true - - -check_term_true + + +check_term_true - + check_all_true - - -check_all_true + + +check_all_true - + check_term_true->check_all_true - - + + + + + +check_all_true->enumerate_check + + - + gen_sound - - -gen_sound + + +gen_sound - + gen_complete - - -gen_complete + + +gen_complete - + zdecs_sound - - -zdecs_sound + + +zdecs_sound - + zdecs_sound->full_comp_aux - - + + - + root_steps_sound - - -root_steps_sound + + +root_steps_sound - + zdecs_sound->root_steps_sound - - + + + + + +zdecs_sound->full_comp_aux_sub + + - + zdecs_complete - - -zdecs_complete + + +zdecs_complete - + root_steps_complete - - -root_steps_complete + + +root_steps_complete - + zdecs_complete->root_steps_complete - - + + - + positions_at - - -positions_at + + +positions_at - + steps_sound - - -steps_sound + + +steps_sound - + positions_at->steps_sound - - + + - + root_steps_sound->steps_sound - - + + - + steps_complete - - -steps_complete + + +steps_complete - + root_steps_complete->steps_complete - - + + + + + +steps_sound->enumerate_sound + + - + steps_sound->gen_sound - - + + - + steps_sound_red1 - - -steps_sound_red1 + + +steps_sound_red1 - + steps_sound->steps_sound_red1 - - + + - + has_red_spec - - -has_red_spec + + +has_red_spec - + steps_sound->has_red_spec - - + + - + corpus_sound - - -corpus_sound + + +corpus_sound - + steps_sound->corpus_sound - - + + - + steps_sound_red1->check_term_true - - + + - + steps_sound_red1->gen_fv_preserved - - + + + + + +nf_iff_steps_nil + + +nf_iff_steps_nil + + + + + +steps_sound_red1->nf_iff_steps_nil + + - + steps_sound_red1->corpus_fv_preserved - - + + - + positions_hole - - -positions_hole + + +positions_hole - + root_steps_in_steps - - -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 - + plug_comp->steps_complete - - + + - + positions_comp - - -positions_comp + + +positions_comp - + positions_comp->steps_complete - - + + - + at_ctx_comp - - -at_ctx_comp + + +at_ctx_comp - + at_ctx_comp->steps_complete - - + + + + + +steps_complete->enumerate_complete + + - + steps_complete->gen_complete - - + + - + steps_complete->has_red_spec - - + + + + + +steps_complete->nf_iff_steps_nil + + - + corpus_complete - - -corpus_complete + + +corpus_complete - + steps_complete->corpus_complete - - + + - + has_red_f - - -has_red_f + + +has_red_f - + has_red_f->has_red_spec - - + + - + has_red_spec->check_term_true - - + + - + red1_dec - - -red1_dec + + +red1_dec - + has_red_spec->red1_dec - - + + - + corpus_decides - - -corpus_decides + + +corpus_decides - + has_red_spec->corpus_decides - - + + + + + +normal_form_iff_nf + + +normal_form_iff_nf + + + + + +nf_iff_steps_nil->normal_form_iff_nf + + + + + +nf_dec + + +nf_dec + + + + + +nf_iff_steps_nil->nf_dec + + - + open_rec_app - - -open_rec_app + + +open_rec_app - + open_rec_lam - - -open_rec_lam + + +open_rec_lam - + open_rec_esub - - -open_rec_esub + + +open_rec_esub - + close_rec_app - - -close_rec_app + + +close_rec_app - + close_rec_lam - - -close_rec_lam + + +close_rec_lam - + close_rec_esub - - -close_rec_esub + + +close_rec_esub - + subst_app - - -subst_app + + +subst_app - + subst_lam - - -subst_lam + + +subst_lam - + subst_esub - - -subst_esub + + +subst_esub + + +open_rec_lc_atom + + +open_rec_lc_atom + + + + + +open_rec_lc + + +open_rec_lc + + + + + +open_rec_lc_atom->open_rec_lc + + + - + red_sub_root_to_red1 - - -red_sub_root_to_red1 + + +red_sub_root_to_red1 - + red_sub_to_red1 - - -red_sub_to_red1 + + +red_sub_to_red1 - + red_sub_root_to_red1->red_sub_to_red1 - - + + - + red_sub_context - - -red_sub_context + + +red_sub_context + + +Star_red_sub_context + + +Star_red_sub_context + + + + + +red_sub_context->Star_red_sub_context + + + - + red_sub_gc - - -red_sub_gc + + +red_sub_gc + + +red_sub_gc->full_comp_aux_sub + + + + + +red_gc_to_red_sub + + +red_gc_to_red_sub + + + + + +red_sub_gc->red_gc_to_red_sub + + + - + red_sub_r - - -red_sub_r + + +red_sub_r + + +red_sub_r->full_comp_aux_sub + + + - + occurs_zfill - - -occurs_zfill + + +occurs_zfill - + zfill_occurs0 - - -zfill_occurs0 + + +zfill_occurs0 - + occurs_zfill->zfill_occurs0 - - + + - + R_Gc_disjoint - - -R_Gc_disjoint + + +R_Gc_disjoint - + zfill_occurs0->R_Gc_disjoint - - + + + + + +plus_red_sub_full_comp + + +plus_red_sub_full_comp + + + + + +full_comp_aux_sub->plus_red_sub_full_comp + + + + + +plus_red_sub_full_comp->star_red_sub_full_comp + + + + + +es_count_plug_mono + + +es_count_plug_mono + + + + + +red_gc_measure + + +red_gc_measure + + + + + +es_count_plug_mono->red_gc_measure + + + + + +red_gc_terminates + + +red_gc_terminates + + + + + +red_gc_measure->red_gc_terminates + + diff --git a/graphs/index.txt b/graphs/index.txt new file mode 100644 index 0000000..8e8e42a --- /dev/null +++ b/graphs/index.txt @@ -0,0 +1,109 @@ +status milestone kind name file +proved M1 infra at_ctx_comp theory/Reduction.v +proved M1 infra close_rec_fvar theory/Binding.v +proved M1 infra close_rec_fvs theory/Binding.v +proved M1 infra close_rec_notin theory/Binding.v +proved M1 infra fvs_lift theory/Binding.v +proved M1 infra has_red_f theory/Reduction.v +proved M1 infra has_red_spec theory/Reduction.v +proved M1 infra lift_0_lc theory/Binding.v +proved M1 infra lift_lc theory/Binding.v +proved M1 infra nf_dec theory/Reduction.v +proved M1 infra nf_iff_steps_nil theory/Reduction.v +proved M1 infra normal_form_iff_nf theory/Reduction.v +proved M1 infra open_close theory/Binding.v +proved M1 infra open_rec_bvar theory/Binding.v +proved M1 infra open_rec_bvar_neq theory/Binding.v +proved M1 infra open_rec_fvs theory/Binding.v +proved M1 infra open_rec_occurs_false theory/Binding.v +proved M1 infra plug_comp theory/Reduction.v +proved M1 infra positions_at theory/Reduction.v +proved M1 infra positions_comp theory/Reduction.v +proved M1 infra positions_hole theory/Reduction.v +proved M1 infra red1_dec theory/Reduction.v +proved M1 infra root_steps_complete theory/Reduction.v +proved M1 infra root_steps_in_steps theory/Reduction.v +proved M1 infra root_steps_sound theory/Reduction.v +proved M1 infra steps_complete theory/Reduction.v +proved M1 infra steps_sound theory/Reduction.v +proved M1 infra steps_sound_red1 theory/Reduction.v +proved M1 infra subst_fvar_other theory/Binding.v +proved M1 infra subst_fvar_self theory/Binding.v +proved M1 infra subst_fvs theory/Binding.v +proved M1 infra zdecs_complete theory/Reduction.v +proved M1 infra zdecs_sound theory/Reduction.v +proved M2 infra Plus_red1_context theory/Metatheory.v +proved M2 infra Plus_step_trans theory/Metatheory.v +proved M2 infra Plus_to_Star theory/Closure.v +proved M2 infra Plus_trans theory/Metatheory.v +proved M2 infra Star_red1_context theory/Closure.v +proved M2 infra Star_trans theory/Closure.v +proved M2 infra check_all_true theory/Random.v +proved M2 infra check_term_true theory/Random.v +proved M2 infra close_rec_app theory/Substitution.v +proved M2 infra close_rec_esub theory/Substitution.v +proved M2 infra close_rec_lam theory/Substitution.v +proved M2 infra corpus_complete theory/Tests.v +proved M2 infra corpus_decides theory/Tests.v +proved M2 infra corpus_fv_preserved theory/Tests.v +proved M2 infra corpus_sound theory/Tests.v +proved M2 infra enumerate_check theory/Enumerate.v +proved M2 infra enumerate_complete theory/Enumerate.v +proved M2 infra enumerate_sound theory/Enumerate.v +proved M2 infra full_comp_aux theory/Metatheory.v +proved M2 infra fvs_zplug_lift theory/Metatheory.v +proved M2 infra gen_complete theory/Random.v +proved M2 infra gen_fv_preserved theory/Random.v +proved M2 infra gen_list_length theory/Random.v +proved M2 infra gen_sound theory/Random.v +proved M2 infra in_comb theory/Enumerate.v +proved M2 paper lemma_2_1_fv_preserved theory/Metatheory.v +proved M2 paper lemma_2_2_full_comp theory/Metatheory.v +proved M2 paper lemma_2_3_beta_sim theory/Metatheory.v +proved M2 infra occurs_count_false theory/Metatheory.v +proved M2 infra occurs_count_pos theory/Metatheory.v +proved M2 infra occurs_count_zero theory/Metatheory.v +proved M2 infra occurs_count_zfill_plug theory/Metatheory.v +proved M2 infra occurs_lift_self theory/Metatheory.v +proved M2 infra open_rec_app theory/Substitution.v +proved M2 infra open_rec_esub theory/Substitution.v +proved M2 infra open_rec_lam theory/Substitution.v +proved M2 infra open_rec_lc theory/Substitution.v +proved M2 infra open_rec_lc_atom theory/Substitution.v +proved M2 infra open_rec_zplug_lift theory/Metatheory.v +proved M2 infra plug_fv_mono theory/Metatheory.v +proved M2 infra pow2_pos theory/Enumerate.v +proved M2 infra red1_root_fv theory/Metatheory.v +proved M2 infra red1_star theory/Closure.v +proved M2 infra red1r_fv theory/Metatheory.v +proved M2 infra size_all_terms theory/Enumerate.v +proved M2 infra star_one_trans theory/Closure.v +proved M2 infra subst_app theory/Substitution.v +proved M2 infra subst_esub theory/Substitution.v +proved M2 infra subst_lam theory/Substitution.v +proved M2 infra subst_lc_self theory/Substitution.v +proved M2 infra subst_notin theory/Substitution.v +proved M2 infra subst_other theory/Substitution.v +proved M2 infra zdecs_nonempty theory/Metatheory.v +proved M3 infra R_Gc_disjoint theory/Subsystem.v +proved M3 infra Star_red_sub_context theory/Subsystem.v +proved M3 infra es_count_plug_mono theory/Subsystem.v +proved M3 infra full_comp_aux_sub theory/Subsystem.v +proved M3 infra occurs_zfill theory/Subsystem.v +proved M3 infra plus_red_sub_full_comp theory/Subsystem.v +proved M3 infra red_gc_measure theory/Subsystem.v +proved M3 infra red_gc_terminates theory/Subsystem.v +proved M3 infra red_gc_to_red_sub theory/Subsystem.v +proved M3 infra red_sub_context theory/Subsystem.v +proved M3 infra red_sub_gc theory/Subsystem.v +proved M3 infra red_sub_r theory/Subsystem.v +proved M3 infra red_sub_root_to_red1 theory/Subsystem.v +proved M3 infra red_sub_to_red1 theory/Subsystem.v +proved M3 infra star_red_sub_full_comp theory/Subsystem.v +proved M3 infra zfill_occurs0 theory/Subsystem.v +proved M4 infra par_context theory/Parallel.v +proved M4 infra par_red1_iff theory/Parallel.v +proved M4 infra par_reflexive theory/Parallel.v +proved M4 infra par_to_red1_or_eq theory/Parallel.v +proved M4 infra red1_in_par theory/Parallel.v +proved M4 infra red1_or_eq_to_par theory/Parallel.v diff --git a/graphs/theorems.json b/graphs/theorems.json index d0844ea..9a78af6 100644 --- a/graphs/theorems.json +++ b/graphs/theorems.json @@ -9,11 +9,12 @@ "html": "https://arxiv.org/html/2312.13270v1" }, "milestones": [ - "M0", "M1", - "M2" + "M2", + "M3", + "M4" ], - "current": "M2", + "current": "M4", "nodes": [ { "id": "fvs_lift", @@ -168,6 +169,125 @@ "open_rec_fvs" ] }, + { + "id": "Star_trans", + "label": "Star_trans", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Closure.v", + "depends": [] + }, + { + "id": "red1_star", + "label": "red1_star", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Closure.v", + "depends": [] + }, + { + "id": "Plus_to_Star", + "label": "Plus_to_Star", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Closure.v", + "depends": [] + }, + { + "id": "Star_red1_context", + "label": "Star_red1_context", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Closure.v", + "depends": [] + }, + { + "id": "star_one_trans", + "label": "star_one_trans", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Closure.v", + "depends": [] + }, + { + "id": "in_comb", + "label": "in_comb", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Enumerate.v", + "depends": [] + }, + { + "id": "pow2_pos", + "label": "pow2_pos", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Enumerate.v", + "depends": [] + }, + { + "id": "size_all_terms", + "label": "size_all_terms", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Enumerate.v", + "depends": [ + "in_comb", + "pow2_pos" + ] + }, + { + "id": "enumerate_check", + "label": "enumerate_check", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Enumerate.v", + "depends": [ + "check_all_true" + ] + }, + { + "id": "enumerate_sound", + "label": "enumerate_sound", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Enumerate.v", + "depends": [ + "steps_sound" + ] + }, + { + "id": "enumerate_complete", + "label": "enumerate_complete", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Enumerate.v", + "depends": [ + "steps_complete" + ] + }, { "id": "Plus_red1_context", "label": "Plus_red1_context", @@ -357,12 +477,32 @@ "lemma_2_2_full_comp" ] }, + { + "id": "Plus_trans", + "label": "Plus_trans", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Metatheory.v", + "depends": [] + }, + { + "id": "Plus_step_trans", + "label": "Plus_step_trans", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Metatheory.v", + "depends": [] + }, { "id": "par_red1_iff", "label": "par_red1_iff", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M4", "section": "", "file": "theory/Parallel.v", "depends": [] @@ -372,7 +512,7 @@ "label": "red1_in_par", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M4", "section": "", "file": "theory/Parallel.v", "depends": [] @@ -382,7 +522,7 @@ "label": "par_context", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M4", "section": "", "file": "theory/Parallel.v", "depends": [] @@ -392,7 +532,7 @@ "label": "par_to_red1_or_eq", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M4", "section": "", "file": "theory/Parallel.v", "depends": [ @@ -404,7 +544,7 @@ "label": "red1_or_eq_to_par", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M4", "section": "", "file": "theory/Parallel.v", "depends": [ @@ -416,7 +556,7 @@ "label": "par_reflexive", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M4", "section": "", "file": "theory/Parallel.v", "depends": [] @@ -426,7 +566,7 @@ "label": "gen_list_length", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Random.v", "depends": [] @@ -436,7 +576,7 @@ "label": "check_term_true", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Random.v", "depends": [ @@ -449,7 +589,7 @@ "label": "check_all_true", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Random.v", "depends": [ @@ -461,7 +601,7 @@ "label": "gen_sound", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Random.v", "depends": [ @@ -473,7 +613,7 @@ "label": "gen_complete", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Random.v", "depends": [ @@ -485,7 +625,7 @@ "label": "gen_fv_preserved", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Random.v", "depends": [ @@ -676,12 +816,49 @@ "has_red_spec" ] }, + { + "id": "nf_iff_steps_nil", + "label": "nf_iff_steps_nil", + "kind": "infra", + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [ + "steps_complete", + "steps_sound_red1" + ] + }, + { + "id": "normal_form_iff_nf", + "label": "normal_form_iff_nf", + "kind": "infra", + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [ + "nf_iff_steps_nil" + ] + }, + { + "id": "nf_dec", + "label": "nf_dec", + "kind": "infra", + "status": "proved", + "milestone": "M1", + "section": "", + "file": "theory/Reduction.v", + "depends": [ + "nf_iff_steps_nil" + ] + }, { "id": "open_rec_app", "label": "open_rec_app", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Substitution.v", "depends": [] @@ -691,7 +868,7 @@ "label": "open_rec_lam", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Substitution.v", "depends": [] @@ -701,7 +878,7 @@ "label": "open_rec_esub", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Substitution.v", "depends": [] @@ -711,7 +888,7 @@ "label": "close_rec_app", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Substitution.v", "depends": [] @@ -721,7 +898,7 @@ "label": "close_rec_lam", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Substitution.v", "depends": [] @@ -731,7 +908,7 @@ "label": "close_rec_esub", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Substitution.v", "depends": [] @@ -741,7 +918,7 @@ "label": "subst_app", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Substitution.v", "depends": [] @@ -751,7 +928,7 @@ "label": "subst_lam", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Substitution.v", "depends": [] @@ -761,7 +938,7 @@ "label": "subst_esub", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Substitution.v", "depends": [] @@ -771,7 +948,7 @@ "label": "subst_notin", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Substitution.v", "depends": [ @@ -784,7 +961,7 @@ "label": "subst_lc_self", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Substitution.v", "depends": [ @@ -796,19 +973,41 @@ "label": "subst_other", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M2", "section": "", "file": "theory/Substitution.v", "depends": [ "subst_fvar_other" ] }, + { + "id": "open_rec_lc_atom", + "label": "open_rec_lc_atom", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Substitution.v", + "depends": [] + }, + { + "id": "open_rec_lc", + "label": "open_rec_lc", + "kind": "infra", + "status": "proved", + "milestone": "M2", + "section": "", + "file": "theory/Substitution.v", + "depends": [ + "open_rec_lc_atom" + ] + }, { "id": "red_sub_root_to_red1", "label": "red_sub_root_to_red1", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M3", "section": "", "file": "theory/Subsystem.v", "depends": [] @@ -818,7 +1017,7 @@ "label": "red_sub_to_red1", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M3", "section": "", "file": "theory/Subsystem.v", "depends": [ @@ -830,7 +1029,7 @@ "label": "red_sub_context", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M3", "section": "", "file": "theory/Subsystem.v", "depends": [] @@ -840,7 +1039,7 @@ "label": "red_sub_gc", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M3", "section": "", "file": "theory/Subsystem.v", "depends": [] @@ -850,7 +1049,7 @@ "label": "red_sub_r", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M3", "section": "", "file": "theory/Subsystem.v", "depends": [] @@ -860,7 +1059,7 @@ "label": "occurs_zfill", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M3", "section": "", "file": "theory/Subsystem.v", "depends": [] @@ -870,7 +1069,7 @@ "label": "zfill_occurs0", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M3", "section": "", "file": "theory/Subsystem.v", "depends": [ @@ -882,13 +1081,115 @@ "label": "R_Gc_disjoint", "kind": "infra", "status": "proved", - "milestone": "M0", + "milestone": "M3", "section": "", "file": "theory/Subsystem.v", "depends": [ "zfill_occurs0" ] }, + { + "id": "Star_red_sub_context", + "label": "Star_red_sub_context", + "kind": "infra", + "status": "proved", + "milestone": "M3", + "section": "", + "file": "theory/Subsystem.v", + "depends": [ + "red_sub_context" + ] + }, + { + "id": "full_comp_aux_sub", + "label": "full_comp_aux_sub", + "kind": "infra", + "status": "proved", + "milestone": "M3", + "section": "", + "file": "theory/Subsystem.v", + "depends": [ + "occurs_count_zero", + "occurs_count_zfill_plug", + "open_rec_occurs_false", + "open_rec_zplug_lift", + "red_sub_gc", + "red_sub_r", + "zdecs_nonempty", + "zdecs_sound" + ] + }, + { + "id": "plus_red_sub_full_comp", + "label": "plus_red_sub_full_comp", + "kind": "infra", + "status": "proved", + "milestone": "M3", + "section": "", + "file": "theory/Subsystem.v", + "depends": [ + "full_comp_aux_sub" + ] + }, + { + "id": "star_red_sub_full_comp", + "label": "star_red_sub_full_comp", + "kind": "infra", + "status": "proved", + "milestone": "M3", + "section": "", + "file": "theory/Subsystem.v", + "depends": [ + "Plus_to_Star", + "plus_red_sub_full_comp" + ] + }, + { + "id": "es_count_plug_mono", + "label": "es_count_plug_mono", + "kind": "infra", + "status": "proved", + "milestone": "M3", + "section": "", + "file": "theory/Subsystem.v", + "depends": [] + }, + { + "id": "red_gc_measure", + "label": "red_gc_measure", + "kind": "infra", + "status": "proved", + "milestone": "M3", + "section": "", + "file": "theory/Subsystem.v", + "depends": [ + "es_count_plug_mono" + ] + }, + { + "id": "red_gc_terminates", + "label": "red_gc_terminates", + "kind": "infra", + "status": "proved", + "milestone": "M3", + "section": "", + "file": "theory/Subsystem.v", + "depends": [ + "red_gc_measure" + ] + }, + { + "id": "red_gc_to_red_sub", + "label": "red_gc_to_red_sub", + "kind": "infra", + "status": "proved", + "milestone": "M3", + "section": "", + "file": "theory/Subsystem.v", + "depends": [ + "red_sub_gc" + ] + }, { "id": "corpus_sound", "label": "corpus_sound", diff --git a/scripts/extract_metadata.py b/scripts/extract_metadata.py index 211d60c..0173a34 100755 --- a/scripts/extract_metadata.py +++ b/scripts/extract_metadata.py @@ -21,7 +21,13 @@ MILESTONE = { "Binding": "M1", "Reduction": "M1", "Metatheory": "M2", + "Closure": "M2", + "Substitution": "M2", + "Subsystem": "M3", + "Parallel": "M4", "Tests": "M2", + "Random": "M2", + "Enumerate": "M2", } MILESTONE_ORDER = ["M0", "M1", "M2", "M3", "M4", "M5", "M6"] PAPER_META = { diff --git a/scripts/index.py b/scripts/index.py new file mode 100755 index 0000000..5441643 --- /dev/null +++ b/scripts/index.py @@ -0,0 +1,28 @@ +#!/usr/bin/env python3 +import json +import os +import sys + +ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +META = os.path.join(ROOT, "graphs", "theorems.json") +OUT = os.path.join(ROOT, "graphs", "index.txt") + + +def main(): + with open(META, "r", encoding="utf-8") as fh: + data = json.load(fh) + rows = [] + for n in sorted(data["nodes"], key=lambda x: (x["milestone"], x["id"])): + rows.append( + "\t".join([n["status"], n["milestone"], n["kind"], n["id"], n["file"]]) + ) + header = "\t".join(["status", "milestone", "kind", "name", "file"]) + with open(OUT, "w", encoding="utf-8") as fh: + fh.write(header + "\n") + fh.write("\n".join(rows) + "\n") + print("wrote", os.path.relpath(OUT, ROOT), "with", len(rows), "results") + return 0 + + +if __name__ == "__main__": + sys.exit(main())