Add induction hypotheses to the generated principles for inductive types.#2
Closed
DIJamner wants to merge 2 commits into
Closed
Add induction hypotheses to the generated principles for inductive types.#2DIJamner wants to merge 2 commits into
DIJamner wants to merge 2 commits into
Conversation
The auto-generated <T>_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 <T>_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) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
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) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
Contributor
Author
|
A work-in-progress note: I'm triangulating the sources of the bugs (they all see fixpoint related (e.g. a stack overflow)) and will have more info on them soon. |
Contributor
Author
|
Here is a quick summary of my understanding of these bugs, which have some common roots:
#3 also identifies a couple unrelated bugs and provides speculative (LLM-written, and so untrustworthy) fixes that might be useful either for careful human review or as a reference. |
Contributor
Author
|
#3 now also contains (un-reviewed, LLM-generated) fixes for these bugs, which may or may not be helpful. |
Merged
Contributor
Author
|
This has been folded into #4 . It can be broken out separately if needed, but for now I am closing this issue. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Warning: the code in this PR was AI-generated and not human-validated. It should be treated with suspicion until reviewed line-by-line or rewritten.
Currently, generated principles like
nat_indare case-splitting principles, not induction principles, because they lack induction hypotheses. For example, currently the successor branch ofnat_indexpects a proof of this shape:forall arg0, P (S arg0). With this PR, it should have this shape:forall arg0, P arg0 -> P (S arg0), which makes it possible to use it for induction. This PR also add support for parametric inductives like lists.Given that we have fixpoints, it would seem like we could do the Rocq thing and generate a fixpoint definition rather than just the signature, but that seems blocked on dependent pattern matching, which is too much work to be worth it.
This branch also contains minimal examples of 3 (related) bugs, two of which cause segfaults and the third prevents some reducible terms from normalizing. It's probably worth fixing these if possible.