Stream: Beginner Questions

Topic: proof structure one-liners

view this post on Zulip Artem Khovanov (Aug 21 2022 at 00:01):

Is it possible to somehow "one line" a proof by cases/induction, where the proof in each case is easy? I ask because these proofs feel quite redundant. Here is an example of a proof I wrote with this issue (the cases are {a≤x≤b}\{a\leq x\leq b\}, {a≤x}\{a \leq x\}, {x≤b}\{x \leq b\} and the whole space):

lemma open_interval_connected:
  assumes "open_interval I" "x ∈ I" "y ∈ I" "z ∈ carrier L" "z between x y"
  shows "z ∈ I"
using assms proof (induction rule: open_interval.induct)
  case (both a b)
  thus ?case by (metis (no_types, lifting) btw_def lless_eq lless_trans mem_Collect_eq)
next
  case (lower a)
  thus ?case by (metis (no_types, lifting) btw_def lless_eq lless_trans mem_Collect_eq)
next
  case (upper b)
  thus ?case by (metis (no_types, lifting) btw_def lless_eq lless_trans mem_Collect_eq)
next
  case carrier
  then show ?case by blast
qed

view this post on Zulip Wenda Li (Aug 21 2022 at 00:49):

Something like this?

lemma open_interval_connected:
  assumes "open_interval I" "x ∈ I" "y ∈ I" "z ∈ carrier L" "z between x y"
  shows "z ∈ I"
using assms by (induction rule: open_interval.induct; (metis (no_types, lifting) btw_def lless_eq lless_trans mem_Collect_eq))

view this post on Zulip Simon Roßkopf (Aug 21 2022 at 00:51):

You could place a method after the qed to solve all remaining cases. Something like

lemma "foo"
proof(induction ...)
    case 1
    <complicated proof>
qed (something that solves all other suboals)

Last updated: Apr 18 2024 at 01:05 UTC