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

graphs/dependency.dot

@@ -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/theorems.json

@@ -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",

scripts/audit.sh

@@ -35,7 +35,7 @@ done < <(find theory -name '*.v' -print0 2>/dev/null)
 echo "== Print Assumptions =="
 WORK="$(mktemp -d ./.audit-work.XXXXXX)"
 cp theory/*.v "$WORK"/
-for f in ExecReducer Binding Reduction Metatheory Subsystem Substitution Parallel Tests; do
+for f in ExecReducer Binding Reduction Metatheory Subsystem Substitution Parallel Tests Random; do
   echo "-- $f"
   out="$(rocq compile -Q "$WORK" LambdaSub "$WORK/$f.v" 2>&1 || true)"
   echo "$out"

scripts/samplecheck.sh

@@ -0,0 +1,19 @@
+#!/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 "SAMPLE CHECK OK: 16 generated terms checked against red1 by theory/Random.v"

theory/Random.v

@@ -0,0 +1,85 @@
+From Stdlib Require Import List Bool Arith Lia PeanoNat.
+Import ListNotations.
+From LambdaSub Require Import ExecReducer Binding Reduction Metatheory Subsystem Substitution Parallel.
+
+Definition next (s : nat) : nat := (s * 3 + 1) mod 97.
+
+Fixpoint gen (fuel : nat) (s : nat) : trm * nat :=
+  match fuel with
+  | 0 => (FVar (s mod 5), next s)
+  | S f =>
+    match next s mod 6 with
+    | 0 => (FVar (next s mod 5), next (next s))
+    | 1 => let (a, s1) := gen f (next s) in
+           let (b, s2) := gen f s1 in (App a b, next s2)
+    | 2 => let (a, s1) := gen f (next s) in (Lam a, next s1)
+    | 3 => let (a, s1) := gen f (next s) in
+           let (b, s2) := gen f s1 in (ESub a b, next s2)
+    | 4 => (BVar (next s mod 3), next (next s))
+    | _ => (FVar (next s mod 5), next (next s))
+    end
+  end.
+
+Fixpoint gen_list (count : nat) (s : nat) : list trm :=
+  match count with
+  | 0 => []
+  | S c => let (t, s') := gen 3 s in t :: gen_list c s'
+  end.
+
+Lemma gen_list_length : forall count s, length (gen_list count s) = count.
+Proof.
+  induction count; intros s.
+  - reflexivity.
+  - cbn [gen_list].
+    destruct (gen 3 s) as [t s'].
+    cbn [length].
+    rewrite IHcount. reflexivity.
+Qed.
+
+Definition check_term (t : trm) : bool :=
+  forallb (fun p => has_red t (snd p)) (steps t).
+
+Definition check_all (l : list trm) : bool := forallb check_term l.
+
+Lemma check_term_true : forall t, check_term t = true.
+Proof.
+  intros t. unfold check_term.
+  apply forallb_forall. intros [r s] Hp.
+  apply has_red_spec. exact (steps_sound_red1 t r s Hp).
+Qed.
+
+Lemma check_all_true : forall l, check_all l = true.
+Proof.
+  intros l. unfold check_all.
+  apply forallb_forall. intros t _. apply check_term_true.
+Qed.
+
+Example sample_agreement : check_all (gen_list 16 7) = true.
+Proof. apply check_all_true. Qed.
+
+Example sample_length : length (gen_list 16 7) = 16.
+Proof. apply gen_list_length. Qed.
+
+Lemma gen_sound : forall count seed t, In t (gen_list count seed) ->
+  forall p, In p (steps t) -> red1r (fst p) t (snd p).
+Proof. intros count seed t _ [r s] Hp. apply steps_sound. exact Hp. Qed.
+
+Lemma gen_complete : forall count seed t r t', In t (gen_list count seed) ->
+  red1r r t t' -> In (r,t') (steps t).
+Proof. intros count seed t r t' _ H. apply steps_complete. exact H. Qed.
+
+Lemma gen_fv_preserved : forall count seed t p, In t (gen_list count seed) ->
+  In p (steps t) -> incl (fvs (snd p)) (fvs t).
+Proof.
+  intros count seed t [r s] _ H. simpl.
+  apply (lemma_2_1_fv_preserved t s). exact (steps_sound_red1 t r s H).
+Qed.
+
+Print Assumptions gen_list_length.
+Print Assumptions check_term_true.
+Print Assumptions check_all_true.
+Print Assumptions sample_agreement.
+Print Assumptions sample_length.
+Print Assumptions gen_sound.
+Print Assumptions gen_complete.
+Print Assumptions gen_fv_preserved.