Stream: General

Topic: Convert case rules into split rules


view this post on Zulip Lukas Stevens (Mar 17 2020 at 16:33):

Is there any way to convert a case rule into a split rule such that the rule can be used with apply(simp split: rl)?

view this post on Zulip Kevin Kappelmann (Mar 17 2020 at 17:02):

how about auto elim: rl?

view this post on Zulip Lukas Stevens (Mar 17 2020 at 17:14):

That does not work. For reference, my proof looks like follows:

proof(induction φ)
  case (Atom x)
  then show ?case
    apply(cases x rule: o_literal_cases) by auto
qed (auto simp: and_def or_def neg_def split: if_splits)

What I want to have is:

apply(induction φ) by (auto simp: and_def or_def neg_def split: if_splits o_literal_cases)

I have several proofs of this form and all would go through if the split on x would happen automatically.

view this post on Zulip Kevin Kappelmann (Mar 17 2020 at 17:23):

Is it always about o_literal_cases? If so, I'd just prove the split rule form the case rule and then use it.

view this post on Zulip Lukas Stevens (Mar 17 2020 at 17:24):

Yes, that would work but shouldn't there be an automatic conversion?

view this post on Zulip Kevin Kappelmann (Mar 17 2020 at 18:47):

I think that only works under certain conditions (e.g. non-overlapping cases) and proving the split lemma is the easiest way in this case.

view this post on Zulip Manuel Eberl (Mar 17 2020 at 18:51):

I don't think you need non-overlapping. The problem is rather that a split rule requires an if-and-only-if

view this post on Zulip Manuel Eberl (Mar 17 2020 at 18:51):

which is more specific than an "elim" rule

view this post on Zulip Kevin Kappelmann (Mar 17 2020 at 19:42):

Manuel Eberl said:

I don't think you need non-overlapping. The problem is rather that a split rule requires an if-and-only-if

Yes that's the core problem. I thought that non-overlapping cases would maybe allow you to do some sort of automatic conversion, but idk


Last updated: Mar 29 2024 at 12:28 UTC