From f9a0b347880728d8385e694a4c24b189f948e7dd Mon Sep 17 00:00:00 2001 From: Dustin Jamner Date: Sat, 27 Jun 2026 21:07:58 +0000 Subject: [PATCH 1/2] Generate induction principles with induction hypotheses The auto-generated _ind was a dependent case-analysis principle: each constructor case was `forall args, P (c args)`, with no hypothesis for recursive arguments. That makes induction impossible (apply _ind gives no IH to work with). Add an induction hypothesis for every first-order recursive constructor argument, so e.g. nat_ind's step case becomes `forall (n:nat), P n -> P (S n)` and tree_ind's becomes `forall l r, P l -> P r -> P (node l r)`. Non-recursive arguments and non-recursive types (bool) are unaffected. Scope: non-parametric inductives only. Parametric `_ind` generation is still skipped for a separate, pre-existing reason (constructor types use fresh per-constructor parameter copies that don't match the builder's parameter variables) and is left for a follow-up. Adds a semantic regression test: a full abstract induction proof that only type-checks when the IH is present. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT --- src/commandlanguage/command_exec.c | 66 ++++++++++++++++++++++++++---- tests/engine/test_integration.c | 18 ++++++++ 2 files changed, 76 insertions(+), 8 deletions(-) diff --git a/src/commandlanguage/command_exec.c b/src/commandlanguage/command_exec.c index edbb9ed8..34094d11 100644 --- a/src/commandlanguage/command_exec.c +++ b/src/commandlanguage/command_exec.c @@ -261,9 +261,9 @@ static int _handle_print_command(MEngineRuntime *rt, PrintCmd *print_cmd) { } static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *ctor_type, - Expression *motive_var, Expression **param_vars, - size_t param_count, size_t index_count, - Context *elim_ctx); + Expression *motive_var, Expression *ind_var, + Expression **param_vars, size_t param_count, + size_t index_count, Context *elim_ctx); static Expression *_build_motive_type(Expression *ind_var, Expression **param_vars, size_t param_count, Context *ctx, @@ -365,8 +365,8 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres Expression *ctor_type = kernel_expr_type(ctor_expr); Expression *case_type = - _build_constructor_case_type(ctor_expr, ctor_type, motive_var, param_vars, param_count, - index_count, case_contexts[i]); + _build_constructor_case_type(ctor_expr, ctor_type, motive_var, ind_var, param_vars, + param_count, index_count, case_contexts[i]); if (!case_type) { fprintf(stderr, ERROR "Failed to build case type for %s\n" CRESET, ctor->name); @@ -500,10 +500,47 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres return result; } +// Build the induction hypothesis for a single constructor argument, or NULL when +// the argument is not a recursive occurrence of the inductive being defined. +// +// An argument `arg : I p0..p_{m-1} x0..x_{k-1}` (the inductive applied to its +// parameters and indices) yields the hypothesis `P x0..x_{k-1} arg` — the motive +// applied to the argument's own indices and then the argument itself. This is +// what turns the generated principle from plain case analysis into induction. +// +// Only first-order recursion is recognised; a higher-order argument such as +// `(nat -> I)` is treated as non-recursive and gets no hypothesis. +static Expression *_build_recursive_arg_hypothesis(Expression *arg_var, Expression *arg_type, + Expression *ind_var, Expression *motive_var, + size_t param_count, size_t index_count, + Context *ctx) { + if (!kernel_expr_congruent(kernel_expr_head(arg_type), ind_var)) { + return NULL; + } + + Expression *hypothesis = motive_var; + if (index_count > 0) { + // arg_type is the spine `I p0..p_{m-1} x0..x_{k-1}`; the indices are the + // arguments past the parameters. + DoublyLinkedList *spine = dll_create(); + Expression *head = arg_type; + while (kernel_app_func(head) != NULL) { + dll_insert_at_head(spine, dll_new_node(kernel_app_arg(head))); + head = kernel_app_func(head); + } + for (size_t i = 0; i < index_count; i++) { + Expression *index = (Expression *)dll_at(spine, param_count + i)->data; + hypothesis = kernel_app_create(hypothesis, index, ctx); + } + dll_destroy(spine); + } + return kernel_app_create(hypothesis, arg_var, ctx); +} + static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *ctor_type, - Expression *motive_var, Expression **param_vars, - size_t param_count, size_t index_count, - Context *elim_ctx) { + Expression *motive_var, Expression *ind_var, + Expression **param_vars, size_t param_count, + size_t index_count, Context *elim_ctx) { Expression *core_type = ctor_type; for (size_t i = 0; i < param_count; i++) { if (kernel_forall_var(core_type) != NULL) { @@ -615,6 +652,19 @@ static Expression *_build_constructor_case_type(Expression *ctor_expr, Expressio free(ctor_indices); } Expression *case_type = case_result; + + // Wrap the conclusion with an induction hypothesis per recursive argument, + // giving `IH_0 -> .. -> IH_k -> P (c args)`. These sit inside the argument + // binders below because each hypothesis mentions its argument. + for (size_t i = arg_count; i > 0; i--) { + Expression *arg_type = (Expression *)dll_at(arg_types, i - 1)->data; + Expression *hypothesis = _build_recursive_arg_hypothesis( + arg_vars[i - 1], arg_type, ind_var, motive_var, param_count, index_count, case_ctx); + if (hypothesis) { + case_type = kernel_arrow_create(hypothesis, case_type, case_ctx); + } + } + for (size_t i = arg_count; i > 0; i--) { case_type = kernel_forall_create(arg_vars[i - 1], case_type); } diff --git a/tests/engine/test_integration.c b/tests/engine/test_integration.c index f2e77ee3..3c1229ce 100644 --- a/tests/engine/test_integration.c +++ b/tests/engine/test_integration.c @@ -51,6 +51,23 @@ static void test_inductive_nat(void) { "Check nat_ind.\n"); } +/* The generated induction principle must carry an induction hypothesis for each + * recursive argument (not just case analysis). This proof only type-checks if + * `case_S` is `forall n, P n -> P (S n)`: `step` would not match a hypothesis- + * free `forall n, P (S n)`. */ +static void test_induction_principle_has_ih(void) { + run_ok("induction principle carries the induction hypothesis", + "Inductive nat : Type := | O : nat | S : forall (_: nat), nat.\n" + "Axiom P : forall (_: nat), Prop.\n" + "Axiom base : P O.\n" + "Axiom step : forall (n : nat), forall (_: P n), P (S n).\n" + "Theorem allP : forall (n : nat), P n.\n" + "intro n.\n" + "apply (nat_ind P).\n" + "exact base.\n" + "exact step.\n"); +} + static void test_inductive_match_pred(void) { run_ok("match expression: predecessor", "Inductive nat : Type := | O : nat | S : forall (_: nat), nat.\n" @@ -390,6 +407,7 @@ void run_integration_tests(void) { test_axiom_and_check(); test_definition(); test_inductive_nat(); + test_induction_principle_has_ih(); test_inductive_match_pred(); test_inductive_bool(); test_fixpoint_add(); From b73fd1685dab3c4d74a7135f303b40b57d96e392 Mon Sep 17 00:00:00 2001 From: Dustin Jamner Date: Sat, 27 Jun 2026 21:33:55 +0000 Subject: [PATCH 2/2] Generate induction principles for parametric inductives Previously the generator skipped the induction principle entirely for parametric inductives (param_count > 0), because the principle was built with the inductive's own param_vars while each constructor's stored type used fresh per-constructor parameter copies in a divergent context branch. Build the principle with its own parameter set, bound once after ind_var, and derive each constructor case by *applying* the constructor to those parameters (letting the kernel substitute them) rather than textually stripping parameter binders. Argument variables are created fresh and the remaining telescope is recomputed from the partial application after each one, so argument and return types are rebased onto our variables and stay valid even when a type mentions an earlier argument or a parameter (e.g. cons's tail of type `list A`). This unifies the parametric and non-parametric paths. list_ind now matches Coq: forall A P, P (nil A) -> (forall a l, P l -> P (cons A a l)) -> forall l, P l Adds a regression test that proves an abstract list induction (only type-checks if list_ind has the IH-bearing shape). Also adds bugs/ with two minimal reproducers (plus a clean-failure contrast) for pre-existing crashes when inducting over goals stated with a Fixpoint: `apply` with a fixpoint-mentioning motive, and type-checking an explicit eliminator term whose step case must reduce `add (S n) O`. These are documented, not fixed (Tier 2: symbolic iota/fix reduction). Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT --- bugs/README.md | 42 +++++ bugs/note_clean_conversion_failure.me | 17 +++ bugs/segfault_apply_fixpoint_motive.me | 16 ++ bugs/segfault_exact_eliminator_fixpoint.me | 19 +++ src/commandlanguage/command_exec.c | 169 +++++++++------------ tests/engine/test_integration.c | 21 +++ 6 files changed, 191 insertions(+), 93 deletions(-) create mode 100644 bugs/README.md create mode 100644 bugs/note_clean_conversion_failure.me create mode 100644 bugs/segfault_apply_fixpoint_motive.me create mode 100644 bugs/segfault_exact_eliminator_fixpoint.me diff --git a/bugs/README.md b/bugs/README.md new file mode 100644 index 00000000..1ce388a2 --- /dev/null +++ b/bugs/README.md @@ -0,0 +1,42 @@ +# Known segfaults: induction over computational goals + +These two minimal examples crash the engine (SIGSEGV). They are **pre-existing** +kernel issues, not caused by the induction-principle generator change on this +branch — that change only fixed the *type* of the generated `_ind`. They surface +now because a correct, IH-bearing induction principle can finally be applied to a +goal stated with a `Fixpoint`. + +Both involve the same shape: an induction principle whose motive applies a +fixpoint (`add`) to a constructor-headed *symbolic* argument, so type-checking the +step case must reduce/convert `add (S n) O` with `n` a variable. (MEngine's +reduction is ground-only — `add (S n) O` does not reduce when `n` is symbolic; see +`bugs/note_clean_conversion_failure.me`, which fails *cleanly* with exit 1 rather +than crashing.) The crash is specific to the eliminator-*application* paths below. + +Run them with: + +```bash +./build/mengine -q bugs/segfault_apply_fixpoint_motive.me # exit 139 +./build/mengine -q bugs/segfault_exact_eliminator_fixpoint.me # exit 139 +``` + +## 1. `segfault_apply_fixpoint_motive.me` — the `apply` / unifier path + +`apply (nat_ind )`, where the motive mentions the `add` fixpoint, crashes +while the tactic unifies the principle against the goal and builds the subgoals. +This is the direct route a real induction proof would take, so it currently blocks +proving e.g. `forall n, add n O = n` by induction. + +## 2. `segfault_exact_eliminator_fixpoint.me` — the kernel type-check path + +`Check` (equivalently `exact`) of a fully explicit eliminator proof term crashes +while type-checking the step case, where `add (S n) O` must be converted to +`S (add n O)` under the `n` binder. This isolates the crash to the kernel's +handling of the eliminator application itself: the bare conversion alone does not +crash (it fails cleanly), but wrapping it in the eliminator application does. + +## Not fixed here + +Per the branch's scope, these crashes are documented, not fixed. Fixing them is +the "Tier 2" work: make iota/fix reduction fire on symbolic constructor-headed +arguments, and harden the eliminator application / conversion path against it. diff --git a/bugs/note_clean_conversion_failure.me b/bugs/note_clean_conversion_failure.me new file mode 100644 index 00000000..b30256dc --- /dev/null +++ b/bugs/note_clean_conversion_failure.me @@ -0,0 +1,17 @@ +(* NOT a crash: this fails cleanly (exit 1) with a type error. + + It shows the underlying limitation behind the two segfaults: MEngine's + reduction is ground-only, so `add (S n) O` does not reduce to `S (add n O)` + when `n` is a variable, and the conversion is rejected. On its own this is a + clean rejection; only the eliminator-application paths (the two segfault_*.me + files) turn it into a crash. + + Run: ./build/mengine -q bugs/note_clean_conversion_failure.me *) + +Inductive nat : Type := | O : nat | S : forall (_: nat), nat. + +Fixpoint add (n : nat) (m : nat) {struct n} : nat := + match n with | O => m | S p => S (add p m) end. + +Definition step_conv : forall (n : nat), eq nat (add (S n) O) (S (add n O)) := + fun (n : nat) => eq_refl nat (S (add n O)). diff --git a/bugs/segfault_apply_fixpoint_motive.me b/bugs/segfault_apply_fixpoint_motive.me new file mode 100644 index 00000000..f91cfbc4 --- /dev/null +++ b/bugs/segfault_apply_fixpoint_motive.me @@ -0,0 +1,16 @@ +(* SEGFAULT (exit 139). Pre-existing kernel crash, not fixed on this branch. + + Applying an induction principle whose motive mentions a Fixpoint crashes the + `apply` tactic while it unifies the principle with the goal and builds the + subgoals. This is the natural route an induction proof of `add n O = n` takes. + + Run: ./build/mengine -q bugs/segfault_apply_fixpoint_motive.me *) + +Inductive nat : Type := | O : nat | S : forall (_: nat), nat. + +Fixpoint add (n : nat) (m : nat) {struct n} : nat := + match n with | O => m | S p => S (add p m) end. + +Theorem add_O_r : forall (n : nat), eq nat (add n O) n. +intro n. +apply (nat_ind (fun (k : nat) => eq nat (add k O) k)). diff --git a/bugs/segfault_exact_eliminator_fixpoint.me b/bugs/segfault_exact_eliminator_fixpoint.me new file mode 100644 index 00000000..9af25c23 --- /dev/null +++ b/bugs/segfault_exact_eliminator_fixpoint.me @@ -0,0 +1,19 @@ +(* SEGFAULT (exit 139). Pre-existing kernel crash, not fixed on this branch. + + Type-checking a fully explicit eliminator proof term crashes in the step case, + where `add (S n) O` must convert to `S (add n O)` under the `n` binder. The + bare conversion on its own fails *cleanly* (see note_clean_conversion_failure.me); + only wrapping it in the eliminator application crashes. + + Run: ./build/mengine -q bugs/segfault_exact_eliminator_fixpoint.me *) + +Inductive nat : Type := | O : nat | S : forall (_: nat), nat. + +Fixpoint add (n : nat) (m : nat) {struct n} : nat := + match n with | O => m | S p => S (add p m) end. + +Axiom f_equal_S : forall (a : nat), forall (b : nat), forall (_: eq nat a b), + eq nat (S a) (S b). + +Check (nat_ind (fun (k : nat) => eq nat (add k O) k) (eq_refl nat O) + (fun (n : nat) => fun (ih : eq nat (add n O) n) => f_equal_S (add n O) n ih)). diff --git a/src/commandlanguage/command_exec.c b/src/commandlanguage/command_exec.c index 34094d11..592a0970 100644 --- a/src/commandlanguage/command_exec.c +++ b/src/commandlanguage/command_exec.c @@ -260,10 +260,10 @@ static int _handle_print_command(MEngineRuntime *rt, PrintCmd *print_cmd) { return 0; } -static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *ctor_type, - Expression *motive_var, Expression *ind_var, - Expression **param_vars, size_t param_count, - size_t index_count, Context *elim_ctx); +static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *motive_var, + Expression *ind_var, Expression **param_vars, + size_t param_count, size_t index_count, + Context *elim_ctx); static Expression *_build_motive_type(Expression *ind_var, Expression **param_vars, size_t param_count, Context *ctx, @@ -341,10 +341,23 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres Context **contexts) { Context *elim_ctx = contexts[param_count]; + // The inductive's own parameter variables (param_vars) were built in a context + // branch created *before* ind_var, so they are not in scope where the principle + // lives. Re-bind one shared set of parameters here, after ind_var; the motive, + // every constructor case, and the conclusion all refer to these. Parameter + // types are taken verbatim, which assumes a parameter's type does not mention + // earlier parameters (the usual case, e.g. `(A : Type)`). + Expression **params = malloc(param_count * sizeof(Expression *)); + for (size_t i = 0; i < param_count; i++) { + params[i] = kernel_var_create(kernel_var_name(param_vars[i]), + kernel_expr_type(param_vars[i]), elim_ctx); + elim_ctx = params[i]; + } + Expression **index_vars = NULL; size_t index_count = 0; Expression *motive_type = - _build_motive_type(ind_var, param_vars, param_count, elim_ctx, &index_vars, &index_count); + _build_motive_type(ind_var, params, param_count, elim_ctx, &index_vars, &index_count); Expression *motive_var = kernel_var_create("P", motive_type, elim_ctx); elim_ctx = motive_var; @@ -358,18 +371,19 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres Expression *ctor_expr = kernel_context_lookup(elim_ctx, ctor->name); if (!ctor_expr) { fprintf(stderr, ERROR "Constructor %s not found in context\n" CRESET, ctor->name); + free(params); free(case_vars); free(case_contexts); return NULL; } - Expression *ctor_type = kernel_expr_type(ctor_expr); Expression *case_type = - _build_constructor_case_type(ctor_expr, ctor_type, motive_var, ind_var, param_vars, - param_count, index_count, case_contexts[i]); + _build_constructor_case_type(ctor_expr, motive_var, ind_var, params, param_count, + index_count, case_contexts[i]); if (!case_type) { fprintf(stderr, ERROR "Failed to build case type for %s\n" CRESET, ctor->name); + free(params); free(case_vars); free(case_contexts); return NULL; @@ -380,6 +394,7 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres case_vars[i] = kernel_var_create(case_name, case_type, case_contexts[i]); if (!case_vars[i]) { fprintf(stderr, ERROR "Failed to create case variable for %s\n" CRESET, ctor->name); + free(params); free(case_vars); free(case_contexts); return NULL; @@ -407,13 +422,14 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres // Build (ind params concl_index_0 ... concl_index_n) Expression *ind_applied = ind_var; for (size_t i = 0; i < param_count; i++) { - ind_applied = kernel_app_create(ind_applied, param_vars[i], final_ctx); + ind_applied = kernel_app_create(ind_applied, params[i], final_ctx); if (!ind_applied) { fprintf(stderr, ERROR "Failed to apply parameter %zu to inductive in " "conclusion\n" CRESET, i); + free(params); free(case_vars); free(case_contexts); if (index_vars) { @@ -441,6 +457,7 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres target_applied = kernel_app_create(target_applied, target_var, target_ctx); if (!target_applied) { fprintf(stderr, ERROR "Failed to apply motive to target\n" CRESET); + free(params); free(case_vars); free(case_contexts); if (index_vars) { @@ -468,6 +485,7 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres result = kernel_forall_create(case_vars[i - 1], result); if (!result) { fprintf(stderr, ERROR "Failed to wrap with constructor case %zu\n" CRESET, i - 1); + free(params); free(case_vars); free(case_contexts); return NULL; @@ -477,21 +495,24 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres result = kernel_forall_create(motive_var, result); if (!result) { fprintf(stderr, ERROR "Failed to wrap with motive P\n" CRESET); + free(params); free(case_vars); free(case_contexts); return NULL; } for (size_t i = param_count; i > 0; i--) { - result = kernel_forall_create(param_vars[i - 1], result); + result = kernel_forall_create(params[i - 1], result); if (!result) { fprintf(stderr, ERROR "Failed to wrap with parameter %zu\n" CRESET, i - 1); + free(params); free(case_vars); free(case_contexts); return NULL; } } + free(params); free(case_vars); free(case_contexts); if (index_vars) { @@ -537,140 +558,110 @@ static Expression *_build_recursive_arg_hypothesis(Expression *arg_var, Expressi return kernel_app_create(hypothesis, arg_var, ctx); } -static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *ctor_type, - Expression *motive_var, Expression *ind_var, - Expression **param_vars, size_t param_count, - size_t index_count, Context *elim_ctx) { - Expression *core_type = ctor_type; - for (size_t i = 0; i < param_count; i++) { - if (kernel_forall_var(core_type) != NULL) { - core_type = kernel_forall_body(core_type); - } - } - - DoublyLinkedList *arg_types = dll_create(); - Expression *current = core_type; - while (kernel_forall_var(current) != NULL) { - Expression *arg_type = kernel_expr_type(kernel_forall_var(current)); - dll_insert_at_tail(arg_types, dll_new_node(arg_type)); - current = kernel_forall_body(current); - } - +static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *motive_var, + Expression *ind_var, Expression **param_vars, + size_t param_count, size_t index_count, + Context *elim_ctx) { + // Instantiate the constructor at the principle's parameters by applying it, + // rather than stripping parameter binders from its type textually. The kernel + // substitutes the parameters into the resulting argument and return types, so + // everything below is expressed in terms of param_vars and valid in elim_ctx. Expression *ctor_app = ctor_expr; for (size_t i = 0; i < param_count; i++) { ctor_app = kernel_app_create(ctor_app, param_vars[i], elim_ctx); if (!ctor_app) { fprintf(stderr, ERROR "Failed to apply parameter %zu to constructor\n" CRESET, i); - dll_destroy(arg_types); return NULL; } } - size_t arg_count = dll_len(arg_types); - Expression **arg_vars = malloc(arg_count * sizeof(Expression *)); + // Walk the parameter-instantiated constructor telescope, creating a fresh + // variable for each argument. After applying each fresh argument we recompute + // the remaining type from the partial application, so the kernel rebases the + // following argument and return types onto our fresh variables — keeping them + // valid here even when a type mentions an earlier argument or a parameter + // (e.g. cons's tail of type `list A`). + DoublyLinkedList *args = dll_create(); + Expression *current = kernel_expr_type(ctor_app); Context *case_ctx = elim_ctx; - - for (size_t i = 0; i < arg_count; i++) { - Expression *arg_type = (Expression *)dll_at(arg_types, i)->data; + size_t arg_i = 0; + while (kernel_forall_var(current) != NULL) { + Expression *arg_type = kernel_expr_type(kernel_forall_var(current)); char arg_name[32]; - sprintf(arg_name, "arg%zu", i); - - arg_vars[i] = kernel_var_create(arg_name, arg_type, case_ctx); - case_ctx = arg_vars[i]; - ctor_app = kernel_app_create(ctor_app, arg_vars[i], case_ctx); + sprintf(arg_name, "arg%zu", arg_i++); + Expression *arg_var = kernel_var_create(arg_name, arg_type, case_ctx); + dll_insert_at_tail(args, dll_new_node(arg_var)); + case_ctx = arg_var; + ctor_app = kernel_app_create(ctor_app, arg_var, case_ctx); if (!ctor_app) { - fprintf(stderr, ERROR "Failed to apply constructor arg %zu\n" CRESET, i); - dll_destroy(arg_types); - free(arg_vars); + fprintf(stderr, ERROR "Failed to apply constructor argument\n" CRESET); + dll_destroy(args); return NULL; } + current = kernel_expr_type(ctor_app); } + size_t arg_count = dll_len(args); - // Extract indices from constructor return type - // current holds the return type after stripping foralls + // `current` now holds the return type `I params indices`; pull the indices out + // of its application spine (the arguments after the parameters). Expression **ctor_indices = NULL; if (index_count > 0) { ctor_indices = malloc(index_count * sizeof(Expression *)); - - // Parse the return type as a spine of applications - // For eq_refl: (((eq A) x) x) - we want to extract the indices (the - // trailing applications) DoublyLinkedList *spine = dll_create(); Expression *head = current; while (kernel_app_func(head) != NULL) { dll_insert_at_head(spine, dll_new_node(kernel_app_arg(head))); head = kernel_app_func(head); } - - // The spine now has all the arguments. Skip param_count, take - // index_count - size_t total_args = dll_len(spine); - if (total_args < param_count + index_count) { + if (dll_len(spine) < param_count + index_count) { fprintf(stderr, ERROR "Constructor return type has too few arguments\n" CRESET); dll_destroy(spine); - dll_destroy(arg_types); - free(arg_vars); + dll_destroy(args); free(ctor_indices); return NULL; } - - // Extract the indices (skip parameters) for (size_t i = 0; i < index_count; i++) { ctor_indices[i] = (Expression *)dll_at(spine, param_count + i)->data; } - dll_destroy(spine); } - // Apply motive to indices first, then to constructor application + // Conclusion: `P indices (c params args)`, valid in case_ctx (the innermost + // argument, or elim_ctx for a constructor with no arguments). Expression *case_result = motive_var; for (size_t i = 0; i < index_count; i++) { case_result = kernel_app_create(case_result, ctor_indices[i], case_ctx); - if (!case_result) { - fprintf(stderr, ERROR "Failed to apply motive to index %zu\n" CRESET, i); - dll_destroy(arg_types); - free(arg_vars); - if (ctor_indices) { - free(ctor_indices); - } - return NULL; - } } - case_result = kernel_app_create(case_result, ctor_app, case_ctx); + if (ctor_indices) { + free(ctor_indices); + } if (!case_result) { fprintf(stderr, ERROR "Failed to apply motive to constructor application\n" CRESET); - dll_destroy(arg_types); - free(arg_vars); - if (ctor_indices) { - free(ctor_indices); - } + dll_destroy(args); return NULL; } - if (ctor_indices) { - free(ctor_indices); - } Expression *case_type = case_result; // Wrap the conclusion with an induction hypothesis per recursive argument, // giving `IH_0 -> .. -> IH_k -> P (c args)`. These sit inside the argument // binders below because each hypothesis mentions its argument. for (size_t i = arg_count; i > 0; i--) { - Expression *arg_type = (Expression *)dll_at(arg_types, i - 1)->data; + Expression *arg_var = (Expression *)dll_at(args, i - 1)->data; Expression *hypothesis = _build_recursive_arg_hypothesis( - arg_vars[i - 1], arg_type, ind_var, motive_var, param_count, index_count, case_ctx); + arg_var, kernel_expr_type(arg_var), ind_var, motive_var, param_count, index_count, + case_ctx); if (hypothesis) { case_type = kernel_arrow_create(hypothesis, case_type, case_ctx); } } for (size_t i = arg_count; i > 0; i--) { - case_type = kernel_forall_create(arg_vars[i - 1], case_type); + case_type = kernel_forall_create((Expression *)dll_at(args, i - 1)->data, case_type); } - dll_destroy(arg_types); - free(arg_vars); + dll_destroy(args); return case_type; } @@ -842,16 +833,8 @@ static int _handle_inductive_command(MEngineRuntime *rt, InductiveCmd *ind_cmd) char *ind_principle_name = malloc(strlen(name) + 5); sprintf(ind_principle_name, "%s_ind", name); - /* The induction principle builder uses the original param_vars, but - * constructor types now use fresh parameter copies. The resulting case - * types would fail the application type check (fresh_param != original_param). - * Skip the induction principle for parametric inductives; it is not needed - * by the tactics that use parametric types (e.g., sep_list in cancel). */ - Expression *ind_principle_type = NULL; - if (param_count == 0) { - ind_principle_type = - _build_induction_principle_type(ind_cmd, ind_var, param_vars, param_count, contexts); - } + Expression *ind_principle_type = + _build_induction_principle_type(ind_cmd, ind_var, param_vars, param_count, contexts); Expression *ind_principle_var = NULL; if (ind_principle_type) { diff --git a/tests/engine/test_integration.c b/tests/engine/test_integration.c index 3c1229ce..ce513283 100644 --- a/tests/engine/test_integration.c +++ b/tests/engine/test_integration.c @@ -401,6 +401,26 @@ static void test_parametric_list(void) { "Check cons.\n"); } +/* Parametric inductives also get an induction principle (parameters bound once, + * out front), with an induction hypothesis on the recursive argument. This proof + * only type-checks if list_ind has the shape + * forall A P, P (nil A) -> (forall a l, P l -> P (cons A a l)) -> forall l, P l. */ +static void test_parametric_induction_principle(void) { + run_ok("parametric induction principle is usable", + "Inductive list (A : Type) : Type :=\n" + " | nil : list A\n" + " | cons : forall (_: A), forall (_: list A), list A.\n" + "Axiom A : Type.\n" + "Axiom P : forall (_: list A), Prop.\n" + "Axiom base : P (nil A).\n" + "Axiom step : forall (a : A), forall (l : list A), forall (_: P l), P (cons A a l).\n" + "Theorem allL : forall (l : list A), P l.\n" + "intro l.\n" + "apply (list_ind A P).\n" + "exact base.\n" + "exact step.\n"); +} + void run_integration_tests(void) { test_suite_start("Integration Tests"); @@ -408,6 +428,7 @@ void run_integration_tests(void) { test_definition(); test_inductive_nat(); test_induction_principle_has_ih(); + test_parametric_induction_principle(); test_inductive_match_pred(); test_inductive_bool(); test_fixpoint_add();