Add induction hypotheses to the generated principles for inductive types.

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 <motive>)`, 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.

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)).

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)).

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)).