## 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: Sep 25 2021 at 09:17 UTC