Failed to input the tactics step-by-step within a case block

[ohyeat]

First thanks for such excellent tools!

I'm testing repl to see if I can enter the tactics one-by-one so that I can get state information within each step. When I was testing the following simple problem, I met the problem on case analysis.

open Real
example (a b c d e : ℝ) (h₀ : a ≤ b) (h₁ : c < d) : a + rexp c + e < b + rexp d + e := by
  apply add_lt_add_of_lt_of_le
  · apply add_lt_add_of_le_of_lt h₀
    apply exp_lt_exp.mpr h₁
  apply le_refl

Here is the input/output from my terminal

> lake exe repl 
{"cmd": "import Mathlib\nopen Real\nexample (a b c d e : ℝ) (h₀ : a ≤ b) (h₁ : c < d) : a + rexp c + e < b + rexp d + e := by sorry"}

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 3, "column": 90},
   "goal":
   "a b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ a + rexp c + e < b + rexp d + e",
   "endPos": {"line": 3, "column": 95}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 7},
   "data": "declaration uses 'sorry'"}],
 "env": 0}

{"tactic": "apply add_lt_add_of_lt_of_le", "proofState": 0}

{"proofState": 1,
 "goals":
 ["case h₁\na b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ a + rexp c < b + rexp d",
  "case h₂\na b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ e ≤ e"]}

{"tactic": "·apply add_lt_add_of_le_of_lt h₀", "proofState": 1}

{"proofState": 2,
 "messages":
 [{"severity": "error",
   "pos": {"line": 0, "column": 0},
   "endPos": {"line": 0, "column": 0},
   "data":
   "unsolved goals\ncase h₁\na b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ rexp c < rexp d"}],
 "goals": ["case h₂\na b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ e ≤ e"]}

{"tactic": "  apply exp_lt_exp.mpr h₁", "proofState": 2}

{"message":
 "tactic 'apply' failed, failed to unify\n  rexp c < rexp d\nwith\n  e ≤ e\ncase h₂\na b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ e ≤ e"}

The problem occurred after I entered the second tactic {"tactic": " apply exp_lt_exp.mpr h₁", "proofState": 2} from the case block. However, if I entered the two tactics from the case block within one command, normal state information will be returned.

{"tactic": "· apply add_lt_add_of_le_of_lt h₀\n  apply exp_lt_exp.mpr h₁", "proofState": 1}

{"proofState": 3,
 "goals": ["case h₂\na b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ e ≤ e"]}

I guess repl just ignores the two whitespaces before the second tactic within the case block when I enter them separately, because I tried to remove the two leading whitespaces in the interactive mode using vscode, and got the same error message

open Real
example (a b c d e : ℝ) (h₀ : a ≤ b) (h₁ : c < d) : a + rexp c + e < b + rexp d + e := by
  apply add_lt_add_of_lt_of_le
  · apply add_lt_add_of_le_of_lt h₀
  apply exp_lt_exp.mpr h₁

tactic 'apply' failed, failed to unify
  rexp c < rexp d
with
  e ≤ e

So I wonder if it's possible to handle this issue? Thanks!

[semorrison]

The issue here is that the "focusing dot" in

{"tactic": "·apply add_lt_add_of_le_of_lt h₀", "proofState": 1}

says: "I am now giving you a tactic which must close the goal".

You can see this from the error message:

 "messages":
 [{"severity": "error",
   "pos": {"line": 0, "column": 0},
   "endPos": {"line": 0, "column": 0},
   "data":
   "unsolved goals\ncase h₁\na b c d e : ℝ\nh₀ : a ≤ b\nh₁ : c < d\n⊢ rexp c < rexp d"}],

Options: 1) Just don't use the focusing dot. 2) (Requires REPL upgrade): send the command

  · apply add_lt_add_of_le_of_lt h₀
    sorry

instead, and then pick up the "proofState" in the "sorries" field of the response to then replace the sorry with apply exp_lt_exp.mpr h₁ 3) (Requires a more fundamental REPL upgrade): Have the REPL try to pay attention to the focusing dots and indenting itself, and internally manage the process described in 2) itself.

The short answer is essentially that the current tactic mode is not compatible with structured proofs, and only supports "linear" proofs, which are just a stream of one-liners.

I won't have time to make changes addressing these issues until January. But please feel free to make suggestions about which behaviour would be most useful to you!

[ohyeat]

@semorrison Thanks for your prompt reply! I will try to find other ways to solve this issue.

[semorrison]

I'm going to reopen this issue, as it is something I would like to improve!