sneeker/lambda-sub
1
30 Fork 3
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

add(check): deterministic sample terms and a bounded computed agreement check against red1 (tests)

Browse Source
This commit is contained in:
sneeker committed 2026-09-22 15:12:00 +02:00
1 parent 6a78e651c6
commit 6f96530564
7 files changed
+1153 -267
Download Patch File Download Diff File Expand all files Collapse all files

No files matched your search

graphs/dependency.dot
+48
View File
@@ -37,6 +37,18 @@ 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];
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];
par_to_red1_or_eq [label="par_to_red1_or_eq", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_to_red1_or_eq theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
red1_or_eq_to_par [label="red1_or_eq_to_par", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red1_or_eq_to_par theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
par_reflexive [label="par_reflexive", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="par_reflexive theory/Parallel.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
gen_list_length [label="gen_list_length", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="gen_list_length theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
check_term_true [label="check_term_true", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="check_term_true theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
check_all_true [label="check_all_true", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="check_all_true theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
gen_sound [label="gen_sound", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="gen_sound theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
gen_complete [label="gen_complete", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="gen_complete theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
gen_fv_preserved [label="gen_fv_preserved", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="gen_fv_preserved theory/Random.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
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];
@@ -53,6 +65,26 @@ 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];
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];
close_rec_app [label="close_rec_app", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_app theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
close_rec_lam [label="close_rec_lam", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
close_rec_esub [label="close_rec_esub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="close_rec_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
subst_app [label="subst_app", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_app theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
subst_lam [label="subst_lam", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_lam theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
subst_esub [label="subst_esub", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="subst_esub theory/Substitution.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
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];
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];
red_sub_gc [label="red_sub_gc", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_gc theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
red_sub_r [label="red_sub_r", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#222222", tooltip="red_sub_r theory/Subsystem.v https://arxiv.org/html/2312.13270v1", shape=ellipse];
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];
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];
@@ -84,6 +116,15 @@ digraph theorem_deps {
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;
par_red1_iff -> par_to_red1_or_eq;
par_red1_iff -> red1_or_eq_to_par;
has_red_spec -> check_term_true;
steps_sound_red1 -> check_term_true;
check_term_true -> check_all_true;
steps_sound -> gen_sound;
steps_complete -> gen_complete;
lemma_2_1_fv_preserved -> gen_fv_preserved;
steps_sound_red1 -> gen_fv_preserved;
zdecs_sound -> root_steps_sound;
zdecs_complete -> root_steps_complete;
positions_at -> steps_sound;
@@ -99,6 +140,13 @@ digraph theorem_deps {
steps_complete -> has_red_spec;
steps_sound -> has_red_spec;
has_red_spec -> red1_dec;
close_rec_notin -> subst_notin;
open_rec_occurs_false -> subst_notin;
subst_fvar_self -> subst_lc_self;
subst_fvar_other -> subst_other;
red_sub_root_to_red1 -> red_sub_to_red1;
occurs_zfill -> zfill_occurs0;
zfill_occurs0 -> R_Gc_disjoint;
steps_sound -> corpus_sound;
steps_complete -> corpus_complete;
has_red_spec -> corpus_decides;
graphs/dependency.png
BIN
View File
Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 222 KiB

After

Width:  |  Height:  |  Size: 395 KiB

graphs/dependency.svg
+650 -266
View File
File diff suppressed because it is too large. Load diff
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 40 KiB

After

Width:  |  Height:  |  Size: 59 KiB

graphs/theorems.json
+350
View File
@@ -9,6 +9,7 @@
"html": "https://arxiv.org/html/2312.13270v1"
},
"milestones": [
"M0",
"M1",
"M2"
],
@@ -356,6 +357,142 @@
"lemma_2_2_full_comp"
]
},
{
"id": "par_red1_iff",
"label": "par_red1_iff",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Parallel.v",
"depends": []
},
{
"id": "red1_in_par",
"label": "red1_in_par",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Parallel.v",
"depends": []
},
{
"id": "par_context",
"label": "par_context",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Parallel.v",
"depends": []
},
{
"id": "par_to_red1_or_eq",
"label": "par_to_red1_or_eq",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Parallel.v",
"depends": [
"par_red1_iff"
]
},
{
"id": "red1_or_eq_to_par",
"label": "red1_or_eq_to_par",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Parallel.v",
"depends": [
"par_red1_iff"
]
},
{
"id": "par_reflexive",
"label": "par_reflexive",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Parallel.v",
"depends": []
},
{
"id": "gen_list_length",
"label": "gen_list_length",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Random.v",
"depends": []
},
{
"id": "check_term_true",
"label": "check_term_true",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Random.v",
"depends": [
"has_red_spec",
"steps_sound_red1"
]
},
{
"id": "check_all_true",
"label": "check_all_true",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Random.v",
"depends": [
"check_term_true"
]
},
{
"id": "gen_sound",
"label": "gen_sound",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Random.v",
"depends": [
"steps_sound"
]
},
{
"id": "gen_complete",
"label": "gen_complete",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Random.v",
"depends": [
"steps_complete"
]
},
{
"id": "gen_fv_preserved",
"label": "gen_fv_preserved",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Random.v",
"depends": [
"lemma_2_1_fv_preserved",
"steps_sound_red1"
]
},
{
"id": "zdecs_sound",
"label": "zdecs_sound",
@@ -539,6 +676,219 @@
"has_red_spec"
]
},
{
"id": "open_rec_app",
"label": "open_rec_app",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Substitution.v",
"depends": []
},
{
"id": "open_rec_lam",
"label": "open_rec_lam",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Substitution.v",
"depends": []
},
{
"id": "open_rec_esub",
"label": "open_rec_esub",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Substitution.v",
"depends": []
},
{
"id": "close_rec_app",
"label": "close_rec_app",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Substitution.v",
"depends": []
},
{
"id": "close_rec_lam",
"label": "close_rec_lam",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Substitution.v",
"depends": []
},
{
"id": "close_rec_esub",
"label": "close_rec_esub",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Substitution.v",
"depends": []
},
{
"id": "subst_app",
"label": "subst_app",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Substitution.v",
"depends": []
},
{
"id": "subst_lam",
"label": "subst_lam",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Substitution.v",
"depends": []
},
{
"id": "subst_esub",
"label": "subst_esub",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Substitution.v",
"depends": []
},
{
"id": "subst_notin",
"label": "subst_notin",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Substitution.v",
"depends": [
"close_rec_notin",
"open_rec_occurs_false"
]
},
{
"id": "subst_lc_self",
"label": "subst_lc_self",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Substitution.v",
"depends": [
"subst_fvar_self"
]
},
{
"id": "subst_other",
"label": "subst_other",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Substitution.v",
"depends": [
"subst_fvar_other"
]
},
{
"id": "red_sub_root_to_red1",
"label": "red_sub_root_to_red1",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Subsystem.v",
"depends": []
},
{
"id": "red_sub_to_red1",
"label": "red_sub_to_red1",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Subsystem.v",
"depends": [
"red_sub_root_to_red1"
]
},
{
"id": "red_sub_context",
"label": "red_sub_context",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Subsystem.v",
"depends": []
},
{
"id": "red_sub_gc",
"label": "red_sub_gc",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Subsystem.v",
"depends": []
},
{
"id": "red_sub_r",
"label": "red_sub_r",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Subsystem.v",
"depends": []
},
{
"id": "occurs_zfill",
"label": "occurs_zfill",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Subsystem.v",
"depends": []
},
{
"id": "zfill_occurs0",
"label": "zfill_occurs0",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Subsystem.v",
"depends": [
"occurs_zfill"
]
},
{
"id": "R_Gc_disjoint",
"label": "R_Gc_disjoint",
"kind": "infra",
"status": "proved",
"milestone": "M0",
"section": "",
"file": "theory/Subsystem.v",
"depends": [
"zfill_occurs0"
]
},
{
"id": "corpus_sound",
"label": "corpus_sound",