Zulip Chat Archive

Stream: general

Topic: updating `pretty_cases` in place


Kayla Thomas (Dec 22 2022 at 16:03):

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 (Dec 22 2022 at 16:26):

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

Kayla Thomas (Dec 22 2022 at 16:42):

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 (Dec 22 2022 at 16:45):

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 (Dec 22 2022 at 16:46):

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

Kayla Thomas (Dec 22 2022 at 16:48):

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 (Dec 22 2022 at 16:49):

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

Eric Wieser (Dec 22 2022 at 17:15):

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

Eric Wieser (Dec 22 2022 at 17:16):

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 (Dec 22 2022 at 17:17):

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

Kevin Buzzard (Dec 22 2022 at 17:18):

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

Kayla Thomas (Dec 22 2022 at 17:21):

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 (Dec 22 2022 at 17:24):

The cases don't have to be in order

Eric Wieser (Dec 22 2022 at 17:25):

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.


Last updated: Dec 20 2023 at 11:08 UTC