No definition and rewrite in syntax

[HalflingHelper]

Though we can do
"definition" ident "in" proof and "rewrite" proof_list "in" proof,
there is no
"definition" "{" ident_list "}" "and" "rewrite" proof_list "in" proof like the equivalent
syntax for applying rewrites to the goal.

I'm happy to add this in, as I think it makes the language more consistent and makes
some proofs more concise, but I wanted to make sure that this is as trivial as I think
it will be, and that there isn't a reason that we don't want to do this.

[jsiek]

This should already be supported... is it broken?

[HalflingHelper]

It's situations like these:

import Nat
import List


theorem demo : all T : type, i : Nat, x : T, xs' : List<T>.
  if i = length(node(x, xs'))
  then i = suc(length(xs'))
proof
  arbitrary T : type, i : Nat, x : T, xs' : List<T>
  assume prem

  have i_slxs : i = suc(length(xs')) by
    definition length and rewrite one_add[length(xs')] in prem
  ?
end

[HalflingHelper]

Obviously here we don't need the intermediate have, but I was trying that as part of a larger proof and had to do this:

import Nat
import List

theorem demo : all T : type, i : Nat, x : T, xs' : List<T>.
  if i = length(node(x, xs'))
  then i = suc(length(xs'))
proof
  arbitrary T : type, i : Nat, x : T, xs' : List<T>
  assume prem

  // have i_slxs : i = suc(length(xs')) by
  //   definition length and rewrite one_add[length(xs')] in prem
  // ?
  have step : i = 1 + length(xs') by definition length in prem
  have i_slxs : i = suc(length(xs')) by rewrite one_add_suc[length(xs')] in step
  ?
end

[jsiek]

Oh, I see what you mean, with both definition and rewrite. Yeah, that would be great to add.

[jsiek]

In some sense one doesn't need and because they can be nested:

rewrite eq1 | eq2 in definition {x,y} in p

However, it wouldn't hurt to add support for and that desugars into the above.