closes#1814
@kenmcmil: the error messages will now list aliased variables.
For example, in your file, the new error message is:
```
invalid type ascription, term has type
triple (ctxpre c' s_1 ∧ ctxpre c'_1 s_1) (bndngapp b s_1) (ctxpost c' s_1 ∧ ctxpost c'_1 s_1)
but is expected to have type
triple (ctxpre c' s_1 ∧ ctxpre c'_1 s_1) (bndngapp b s_1) (ctxpost c' s_1 ∧ ctxpost c'_1 s_1)
types contain aliased name(s): c'
remark: the tactic `dedup` can be used to rename aliases
state:
...
```
This is the equivalent of the `ginduction` tactic for cases, but rolled into the same syntax as `cases` itself. `cases h : term` is the syntax, and it will introduce a hypothesis `h : term = C a b...` demonstrating that the original term is equal to the current case.
I considered the possibility of calling `injection` on the generated equalities, but it's useless in the casaes when the equality carries some real information (such as `f x = C1 a`), and when the input term is a local constant, `injection` will do subst, which will undo the effect of the `cases`. If the input term is a constructor, then `injection` would do something interesting, but you would never want to call `cases` in this case because the constructor is already exposed.
@kha I'm trying to improve the equation compiler. I have added a
preprocessing step, and got the following wierd output when testing
tests/lean/interactive/info_goal.lean
```
> {"record":{"doc":"This tactic applies to any goal. It gives directly the exact proof\nterm of the goal. Let `T` be our goal, let `p` be a term of type `U` then\n`exact p` succeeds iff `T` and `U` are definitionally equal.","source":,"state":"⊢ ℕ → ℕ","tactic_params":["<error while executing interactive.param_desc: don't know how to pretty print lean.parser.pexpr 2>"],"text":"exact","type":"interactive.parse interactive.types.texpr → tactic unit"},"response":"ok","seq_num":4}
```
The problem seems to be the pattern
`(parser.pexpr)
which is sugar for
`(parser.pexpr std.prec.max)
and will not match `(pexpr 2)`
So, I fixed it by replacing the pattern with `(parser.pexpr %%v).
However, it is not clear to me why it was working before.
Any ideas?
To make the equation compiler more convenient to use, we will add a
couple of preprocessing steps.
This commit adds the first one of them. In this step, we use
type inference to refine pattern variables, and we relax the
restrictions on inaccessible annotations.
We will also add a preprocessing step that implements the "complete
transition" step before we execute the elim_match step.
This gives a workaround for the situation where the `congr` tactic does too much congruence applications, such as reducing `|- a + b = b + a` to `|- a = b` and `|- b = a`, by supplying the desired equalities to stop at using `have`.
Now tactics supporting locations can also specify the goal among the locations by using the name `⊢` or `|-`. Also `rw at *` is implemented so that it will rewrite any hypotheses or the goal for which the whole sequence of rewrites succeeds. (This is different from `rw at h1 h2 ... hn |-`, which requires that all rewrites run to completion on each specified target.)
