06fb4bec52
This PR wraps the top-level command parser with `withPosition` to enforce indentation in `by` blocks, combined with an empty-by fallback for better error messages. This subsumes #3215 (which introduced `withPosition commandParser` but without the empty-by fallback). It is also related to #9524, which explores elaboration with empty tactic sequences — this PR reuses that idea for the empty-by fallback, so that a `by` not followed by an indented tactic produces an elaboration error (unsolved goals) rather than a parse error. **Changes:** - `topLevelCommandParserFn` now uses `(withPosition commandParser).fn`, setting the saved position at the start of each top-level command - `tacticSeqIndentGt` gains an empty tactic sequence fallback (`pushNone`) so that missing indentation produces an elaboration error (unsolved goals) instead of a parse error - `isEmptyBy` in `goalsAt?` removed: with strict `by` indentation, empty `by` blocks parse successfully via `pushNone` (producing empty nodes) rather than producing `.missing` syntax, making the `isEmptyBy` check dead code. The `isEmpty` helper in `isSyntheticTacticCompletion` continues to work correctly because it handles both `.missing` and empty nodes from `pushNone` (via the vacuously-true `args.all isEmpty` on `#[]`) - Test files updated to indent `by` blocks and expression continuations that were previously at column 0 **Behavior:** - Top-level `by` blocks now require indentation (column > 0 for commands at column 0) - Commands indented inside `section` require proofs to be indented past the command's column - `#guard_msgs in example : True := by` works because tactic indentation is checked against the outermost command's column - Expression continuations (not just `by`) must also be indented past the command, which is slightly more strict but more consistent - `have : True := by` followed by a dedent now correctly puts `this` in scope in the outer tactic block (the `have` is structurally complete with an unsolved-goal error, rather than a parse error) **Code changes observed in practice (lean4 test suite + Mathlib):** - `by` blocks: top-level `theorem ... := by` / `decreasing_by` followed by tactics at column 0 must be indented - `variable` continuations: `variable {A : Type*} [Foo A]\n{B : Type*}` where the second line starts at column 0 must be indented (most common category in Mathlib) - Expression continuations: `def f : T :=\nexpr` or `#synth Foo\n[args]` where the body/arguments start at column 0 - Structure literals: `.symm\n{ toFun := ...` where the struct literal starts at column 0 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
97 lines
3.4 KiB
Text
97 lines
3.4 KiB
Text
theorem tst1 {α : Type} {p : Prop} (xs : List α) (h₁ : (a : α) → (as : List α) → xs = a :: as → p) (h₂ : xs = [] → p) : p :=
|
||
by match (generalizing := false) h : xs with
|
||
| [] => exact h₂ h
|
||
| z::zs => apply h₁ z zs; assumption
|
||
|
||
theorem tst1' {α : Type} {p : Prop} (xs : List α) (h₁ : (a : α) → (as : List α) → xs = a :: as → p) (h₂ : xs = [] → p) : p :=
|
||
by match xs with
|
||
| [] => exact h₂ rfl
|
||
| z::zs => exact h₁ z zs rfl
|
||
|
||
theorem tst2 {α : Type} {p : Prop} (xs : List α) (h₁ : (a : α) → (as : List α) → xs = a :: as → p) (h₂ : xs = [] → p) : p :=
|
||
by match (generalizing := false) h:xs with
|
||
| [] => ?nilCase
|
||
| z::zs => ?consCase;
|
||
case consCase => exact h₁ z zs h;
|
||
case nilCase => exact h₂ h
|
||
|
||
def tst3 {α β γ : Type} (h : α × β × γ) : β × α × γ :=
|
||
by {
|
||
match h with
|
||
| (a, b, c) => exact (b, a, c)
|
||
}
|
||
|
||
theorem tst4 {α : Type} {p : Prop} (xs : List α) (h₁ : (a : α) → (as : List α) → xs = a :: as → p) (h₂ : xs = [] → p) : p := by
|
||
match (generalizing := false) h : xs with
|
||
| [] => _
|
||
| z::zs => _
|
||
case match_2 => exact h₁ z zs h
|
||
exact h₂ h
|
||
|
||
theorem tst5 {p q r} (h : p ∨ q ∨ r) : r ∨ q ∨ p:= by
|
||
match h with
|
||
| Or.inl h => exact Or.inr (Or.inr h)
|
||
| Or.inr (Or.inl h) => ?c1
|
||
| Or.inr (Or.inr h) => ?c2
|
||
case c2 =>
|
||
apply Or.inl
|
||
assumption
|
||
case c1 =>
|
||
apply Or.inr
|
||
apply Or.inl
|
||
assumption
|
||
|
||
theorem tst6 {p q r} (h : p ∨ q ∨ r) : r ∨ q ∨ p:= by
|
||
match h with
|
||
| Or.inl h => exact Or.inr (Or.inr h)
|
||
| Or.inr (Or.inl h) => ?c1
|
||
| Or.inr (Or.inr h) =>
|
||
apply Or.inl
|
||
assumption
|
||
case c1 => apply Or.inr; apply Or.inl; assumption
|
||
|
||
theorem tst7 {p q r} (h : p ∨ q ∨ r) : r ∨ q ∨ p:=
|
||
by match h with
|
||
| Or.inl h =>
|
||
exact Or.inr (Or.inr h)
|
||
| Or.inr (Or.inl h) =>
|
||
apply Or.inr;
|
||
apply Or.inl;
|
||
assumption
|
||
| Or.inr (Or.inr h) =>
|
||
apply Or.inl;
|
||
assumption
|
||
|
||
inductive ListLast.{u} {α : Type u} : List α → Type u
|
||
| empty : ListLast []
|
||
| nonEmpty : (as : List α) → (a : α) → ListLast (as ++ [a])
|
||
|
||
axiom last {α} (xs : List α) : ListLast xs
|
||
axiom back {α} [Inhabited α] (xs : List α) : α
|
||
axiom popBack {α} : List α → List α
|
||
axiom backEq {α} [Inhabited α] : (xs : List α) → (x : α) → back (xs ++ [x]) = x
|
||
axiom popBackEq {α} : (xs : List α) → (x : α) → popBack (xs ++ [x]) = xs
|
||
|
||
theorem tst8 {α} [Inhabited α] (xs : List α) : xs ≠ [] → xs = popBack xs ++ [back xs] :=
|
||
match (generalizing := false) xs, h:last xs with
|
||
| _, ListLast.empty => fun h => absurd rfl h
|
||
| _, ListLast.nonEmpty ys y => fun _ => sorry
|
||
|
||
theorem tst9 {α} [Inhabited α] (xs : List α) : xs ≠ [] → xs = popBack xs ++ [back xs] := by
|
||
match (generalizing := false) xs, h:last xs with
|
||
| _, ListLast.empty => intro h; exact absurd rfl h
|
||
| _, ListLast.nonEmpty ys y => intro; rw [popBackEq, backEq]
|
||
|
||
theorem tst8' {α} [Inhabited α] (xs : List α) : xs ≠ [] → xs = popBack xs ++ [back xs] :=
|
||
match xs, last xs with
|
||
| _, ListLast.empty => fun h => absurd rfl h
|
||
| _, ListLast.nonEmpty ys y => fun _ => sorry
|
||
|
||
theorem tst8'' {α} [Inhabited α] (xs : List α) (h : xs ≠ []) : xs = popBack xs ++ [back xs] :=
|
||
match xs, last xs with
|
||
| _, ListLast.empty => absurd rfl h
|
||
| _, ListLast.nonEmpty ys y => sorry
|
||
|
||
example (xs : List α) : xs = xs := by
|
||
match xs with
|
||
| [] | [x] | x::x'::xs => rfl
|