Stream: General

Topic: proof using exI

Craig Alan Feinstein (Nov 21 2024 at 01:01):

I'm now trying to do my first existential proof in Isabelle. I have proven have "e0 ∈ ℚ ∧ e1 ∈ ℚ ∧ e2 ∈ ℚ ∧ e3 ∈ ℚ ∧ (∑h ∈ {0..<m}. N $$ (h,i) * x $$ (h,0)) = e0 * ?y0 + e1 * ?y1 + e2 * ?y2 + e3 * ?y3 + (∑h ∈ {4..<m}. N $$ (h,i) * x $$ (h,0))" using eq2 by simp
I want to prove "∃e0 e1 e2 e3. e0 ∈ ℚ ∧ e1 ∈ ℚ ∧ e2 ∈ ℚ ∧ e3 ∈ ℚ ∧ (∑h ∈ {0..<m}. N $$ (h,i) * x $$ (h,0)) = e0 * one_of(y_of((a, b, c, d),(x0, x1, x2, x3))) + e1 * two_of(y_of((a, b, c, d),(x0, x1, x2, x3))) + e2 * three_of(y_of((a, b, c, d),(x0, x1, x2, x3))) + e3 * four_of(y_of((a, b, c, d),(x0, x1, x2, x3))) + (∑h ∈ {4..<m}. N $$ (h,i) * x $$ (h,0))"
Looking at the reference manual, I found exI and tried using it in the proof, but it didn't accept it. This seems like a straight-forward application. Is the fact that I have four variables e0, e1, e2, e3 instead of one variable the problem?

Craig Alan Feinstein (Nov 21 2024 at 01:17):

I forgot to mention this definition:

 let ?y0 = "one_of(y_of((a, b, c, d),(x0, x1, x2, x3)))"
  let ?y1 = "two_of(y_of((a, b, c, d),(x0, x1, x2, x3)))"
  let ?y2 = "three_of(y_of((a, b, c, d),(x0, x1, x2, x3)))"
  let ?y3 = "four_of(y_of((a, b, c, d),(x0, x1, x2, x3)))"

Craig Alan Feinstein (Nov 21 2024 at 01:18):

So it is really just a case of P(e0 e1 e2 e3) implies there exists e0 e1 e2 e3 such that P(e0 e1 e2 e3)

Yong Kiam (Nov 21 2024 at 01:19):

maybe just press sledgehammer and see what if gives you?

Craig Alan Feinstein (Nov 21 2024 at 01:19):

I tried sledgehammering with no luck

Yong Kiam (Nov 21 2024 at 01:19):

huh, then something's probably off then

Craig Alan Feinstein (Nov 21 2024 at 01:20):

Assuming I did everything correctly, should exI work?

Yong Kiam (Nov 21 2024 at 01:21):

I think so, but you may need to apply it multiple times

Craig Alan Feinstein (Nov 21 2024 at 01:22):

Can you please give an example of how to apply it multiple times?

Yong Kiam (Nov 21 2024 at 01:23):

apply (intro exI[of ...])
apply (intro exI[of ...])

I guess

Craig Alan Feinstein (Nov 21 2024 at 01:25):

What do the three dots represent in this instance?

Yong Kiam (Nov 21 2024 at 01:25):

oh just something you should write to instantiate the exI

Craig Alan Feinstein (Nov 21 2024 at 01:30):

I just tried this with no luck, where ?thesis is what I want to prove:

thus ?thesis using (intro exI[of e0 e1 e2 e3]) by sledgehammer

Yong Kiam (Nov 21 2024 at 01:31):

that should give you an error

Craig Alan Feinstein (Nov 21 2024 at 01:32):

I'm not sure how to do it with apply.

Yong Kiam (Nov 21 2024 at 01:33):

lemma foo:
  assumes "P a0 a1 a2 a3"
  shows "∃a0 a1 a2 a3. P a0 a1 a2 a3"
  apply (intro exI)

Yong Kiam (Nov 21 2024 at 01:33):

look at the goal state afterwards

Craig Alan Feinstein (Nov 21 2024 at 01:35):

I see. I'll try that. Thank you.

Mathias Fleury (Nov 21 2024 at 06:06):

For this kind of cases you want unify_trace_failure

  apply (intro exI[of _ e1])
  apply (intro exI[of _ e2])
  apply (intro exI[of _ e3])
  supply [[unify_trace_failure]]
  apply (rule assumption_with_e1_e2_e2)

Craig Alan Feinstein (Nov 21 2024 at 23:11):

thank you, I found another way to prove my lemma without even using the existence proof. However, I will need to do an existence proof in my main theorem, so this should help.

Craig Alan Feinstein (Nov 24 2024 at 03:04):

It turns out that definitely I will need to do at least five existence proofs, including the one I originally tried. I have been learning Isabelle mostly from the Fisher’s Inequality section of the archive of formal proofs, which doesn’t use “apply”, so this is all new to me. Are there any sections where you would recommend I learn “apply”.

Craig Alan Feinstein (Nov 24 2024 at 04:27):

Or is there a way to do it without using “apply”?

Mathias Fleury (Nov 24 2024 at 07:24):

apply is the best way to debug why auto or sledgehammer does not work

Mathias Fleury (Nov 24 2024 at 07:25):

With unify_trace_failure, you should reach the point where the error will tell you why the instantiation does not work

Mathias Fleury (Nov 24 2024 at 07:25):

(type classes being different, an equality being reversed -- unlikely but possible)

Mathias Fleury (Nov 24 2024 at 07:33):

You can work-around it with commas:

  supply [[unify_trace_failure]]
  by  (rule exI[of _ e1],  rule exI[of _ e2], rule exI[of _ e5], rule assumption_with_e1_e2_e2)

but this will produce more output as rule will also produce unification failures

Craig Alan Feinstein (Nov 24 2024 at 17:58):

I just tried

  then have "e0 ∈ ℚ ∧ e1 ∈ ℚ ∧ e2 ∈ ℚ ∧ e3 ∈ ℚ ∧
    (∑h ∈ {0..<m}. N $$ (h,i) * x $$ (h,0)) =
    e0 * ?y0 + e1 * ?y1 + e2 * ?y2 + e3 * ?y3 +
    (∑h ∈ {4..<m}. N $$ (h,i) * x $$ (h,0))" using eq2 by simp
  apply (intro exI[of _ e0])
  apply (intro exI[of _ e1])
  apply (intro exI[of _ e2])
  apply (intro exI[of _ e3])
  supply [[unify_trace_failure]]
  apply (rule assumption_with_e0_e1_e2_e3)

it gave me "Illegal application of proof command in "state" mode" I also tried:

  then have "e0 ∈ ℚ ∧ e1 ∈ ℚ ∧ e2 ∈ ℚ ∧ e3 ∈ ℚ ∧
    (∑h ∈ {0..<m}. N $$ (h,i) * x $$ (h,0)) =
    e0 * ?y0 + e1 * ?y1 + e2 * ?y2 + e3 * ?y3 +
    (∑h ∈ {4..<m}. N $$ (h,i) * x $$ (h,0))" using eq2 by simp
   supply [[unify_trace_failure]]
    by  (rule exI[of _ e0],  rule exI[of _ e1], rule exI[of _ e2], rule exI[of _ e3],
        rule assumption_with_e0_e1_e2_e3)

and got the same thing "Illegal application of proof command in "state" mode"

Mathias Fleury (Nov 24 2024 at 18:01):

  then have ...
    by simp
   supply [[unify_trace_failure]]
    by  (rule exI[of _ e0],  rule exI[of _ e1], rule exI[of _ e2], rule exI[of _ e3],
        rule assumption_with_e0_e1_e2_e3)

Mathias Fleury (Nov 24 2024 at 18:01):

you cannot have two bys

Mathias Fleury (Nov 24 2024 at 18:39):

And this is not the place where I suggested putting it

Mathias Fleury (Nov 24 2024 at 18:39):

show ?thesis
   supply ...
   by ...

Craig Alan Feinstein (Nov 24 2024 at 22:52):

Do you mean this?

  then have final_eq: "e0 ∈ ℚ ∧ e1 ∈ ℚ ∧ e2 ∈ ℚ ∧ e3 ∈ ℚ ∧
    (∑h ∈ {0..<m}. N $$ (h,i) * x $$ (h,0)) =
    e0 * ?y0 + e1 * ?y1 + e2 * ?y2 + e3 * ?y3 +
    (∑h ∈ {4..<m}. N $$ (h,i) * x $$ (h,0))" using eq2 by simp
  show ?thesis
   supply [[unify_trace_failure]]
    by  (rule exI[of _ e0],  rule exI[of _ e1], rule exI[of _ e2], rule exI[of _ e3],
        rule assumption_with_e0_e1_e2_e3)

I tried it but got "Undefined fact: "assumption_with_e0_e1_e2_e3"
?thesis is:

"∃e0 e1 e2 e3. e0 ∈ ℚ ∧ e1 ∈ ℚ ∧ e2 ∈ ℚ ∧ e3 ∈ ℚ ∧
    (∑h ∈ {0..<m}. N $$ (h,i) * x $$ (h,0)) =
    e0 * one_of(y_of((a, b, c, d),(x0, x1, x2, x3))) +
    e1 * two_of(y_of((a, b, c, d),(x0, x1, x2, x3))) +
    e2 * three_of(y_of((a, b, c, d),(x0, x1, x2, x3))) +
    e3 * four_of(y_of((a, b, c, d),(x0, x1, x2, x3))) +
    (∑h ∈ {4..<m}. N $$ (h,i) * x $$ (h,0))"

Mathias Fleury (Nov 25 2024 at 05:57):

assumption_with_e0_e1_e2_e3 should be final_eq (you did not provide the name so far…)

Craig Alan Feinstein (Nov 25 2024 at 13:33):

I just replaced it with

 by  (rule exI[of _ e0],  rule exI[of _ e1], rule exI[of _ e2], rule exI[of _ e3],
        final_eq)

I got "Undefined method: "final_eq"⌂"

Mathias Fleury (Nov 25 2024 at 16:34):

rule final_eq

Craig Alan Feinstein (Nov 25 2024 at 16:50):

I got a better message, but not sure what it means.

No subgoals!
The following types do not unify:
(real ⇒ bool) ⇒ bool
(rat ⇒ bool) ⇒ bool
Failed to apply initial proof method⌂:
goal (1 subgoal):
 1. ∃e0 e1 e2 e3.
       e0 ∈ ℚ ∧
       e1 ∈ ℚ ∧
       e2 ∈ ℚ ∧
       e3 ∈ ℚ ∧
       complex_of_int (∑h = 0..<m. N $$ (h, i) * x $$ (h, 0)) =
       complex_of_rat
        (e0 * one_of (y_of ((a, b, c, d), x0, x1, x2, x3)) +
         e1 * two_of (y_of ((a, b, c, d), x0, x1, x2, x3)) +
         e2 * three_of (y_of ((a, b, c, d), x0, x1, x2, x3)) +
         e3 * four_of (y_of ((a, b, c, d), x0, x1, x2, x3))) +
       complex_of_int (∑h = 4..<m. N $$ (h, i) * x $$ (h, 0))

Mathias Fleury (Nov 25 2024 at 16:53):

It means that some function (probably equality, but I am not sure) is taking a real instead of a rat as argument

Mathias Fleury (Nov 25 2024 at 16:53):

So, time for you to look at all types

Craig Alan Feinstein (Nov 25 2024 at 16:57):

Excellent, thank you for your help. I’ve faced that type of issue before. It’s a pain but can be overcome with diligence.

Craig Alan Feinstein (Nov 28 2024 at 00:59):

I fixed it and it works now. The problem was a type error. Also, I was able to just use blast and not even bother with exI. So existence proofs aren't so hard as long as the types are correct.

Last updated: Dec 21 2024 at 12:33 UTC