Stream: Beginner Questions

Topic: intro exI is overzealous

Jakub Kądziołka (Mar 12 2021 at 02:45):

I have a goal with the shape ∃l r. ?P l r. I would like to provide the expressions to be used for l and r. I can do it like this:

    show ?thesis
      apply (rule exI[of _ "x # l"])
      apply (rule exI[of _ r])
      using `x ≠ a` * by auto

but that's really clumsy. Ideally I'd have a proof method with behavior in between rule and intro, in that it can deal with goals that have an extra assumption, but the rule is applied only once. For reference, here is the full proof:

lemma remove1_split:
  assumes "a ∈ set xs"
  shows "∃l r. xs = l @ a # r ∧ remove1 a xs = l @ r"
using assms proof (induction xs)
  case (Cons x xs)
  show ?case
  proof cases
    assume "x = a"
    show ?thesis
      apply (rule exI[of _ "[]"])
      using `x = a` by simp
  next
    assume "x ≠ a"
    then have "a ∈ set xs"
      using `a ∈ set (x # xs)`
      by simp
    then obtain l r where *: "xs = l @ a # r ∧ remove1 a xs = l @ r"
      using Cons.IH by auto
    show ?thesis
      apply (rule exI[of _ "x # l"])
      apply (rule exI[of _ r])
      using `x ≠ a` * by auto
  qed
qed simp

Mathias Fleury (Mar 12 2021 at 06:11):

      by (rule exI[of _ "[]"])
        (use `x = a` in auto)
...

      by (rule exI[of _ "x # l"], rule exI[of _ r])
        (use `x ≠ a` * in auto)

Mathias Fleury (Mar 12 2021 at 06:12):

Otherwise, you go for

      apply  (use `x ≠ a` * in ‹auto intro: exI[of _ "x # l"] exI[of _ r]›)

Mathias Fleury (Mar 12 2021 at 06:13):

However, I don't believe that there is a rule that applies the theorems one-by-one.

Manuel Eberl (Mar 12 2021 at 08:34):

I wrote a method called inst_existentials for this once, it can be found e.g. in HOL-Real_Asymp.Inst_Existentials. Perhaps I should put it in a more prominent place at some point…

Manuel Eberl (Mar 12 2021 at 08:35):

It can also instantiate existentials nested inside conjunctions. I wrote it because in coinductive proofs, your goal can sometimes be of the shape that you have 6 existential quantifiers (sometimes nested in conjunctions) and once you instantiate them correctly the rest is automatic.

Last updated: Nov 13 2025 at 04:27 UTC