updating `pretty_cases` in place

Stream: general

[Kayla Thomas]

Is there a method to update in place the result of using pretty_cases in an induction proof if the hypotheses or the type the induction is done on is changed? Not to automatically fix the proof, just what is generated by the pretty_cases command?

[Eric Wieser]

Can you give a #mwe of what you're asking for?

[Kayla Thomas]

Suppose I have:

inductive day : Type
| mon : day
| tue : day

def is_weekday : day → Prop
| day.mon := true
| day.tue := true

example
  (d : day) :
  is_weekday d :=
begin
  cases d,
  case day.mon
  {
    unfold is_weekday,
  },
  case day.tue
  {
    unfold is_weekday,
  },
end

Then I add wed to the day type and to is_weekday. Can I run something that will add

  case day.wed
  { admit },

to the example in place?

[Kayla Thomas]

Or if something about the definitions changes that changes the list of arguments to one or more cases, to have that list of arguments be updated in place.

[Kayla Thomas]

In the proof, pretty_cases is run to generate the list of cases.

[Kayla Thomas]

Currently I would write the statement of the new theorem, run pretty_cases on it, update the variable names generated by pretty_cases, and copy the previous code over for each case and then fix it as needed.

[Kayla Thomas]

I'm wondering if there might be a faster alternative.

[Eric Wieser]

Try this doesn't support editing existing code, only replacing the tactic that generates it

[Eric Wieser]

It might be possible to write a tactic of the form

pretty_cases {
  case day.mon
  {
    unfold is_weekday,
  },
  case day.tue
  {
    unfold is_weekday,
  },
},

but I imagine it would be prohibitively messy in Lean 3

[Eric Wieser]

Can't you just run pretty_cases after the other cases?

[Kevin Buzzard]

In Lean 4 we can have infoview stuff changing code, right?

[Kayla Thomas]

Eric Wieser said:

Can't you just run pretty_cases after the other cases?

That is a good point for this example. Unfortunately the additional cases are not always added at the end, and sometimes the list of variable names for each case can change as well.

[Eric Wieser]

The cases don't have to be in order

[Eric Wieser]

Kevin Buzzard said:

In Lean 4 we can have infoview stuff changing code, right?

More importantly, we can more reliably turn expressions back into the code that generates them.