Stating a theorem so "unfolding" automatically split · Beginner Questions

Stream: Beginner Questions

Topic: Stating a theorem so "unfolding" automatically split

Yiming Xu (Nov 05 2024 at 07:47):

I have

"csatis sig M w (cDIAM m fl) =
  (m ∈ mops sig ∧
   marity sig m = length fl ∧
   w ∈ world M ∧
   (∃vl. length vl = length fl ∧ rel M m (w # vl) ∧
   (∀i<length vl. csatis sig M (vl ! i) (fl ! i))))"

If I unfold it, it will give:

proof (prove)
using this:
    m ∈ mops sig ∧
    marity sig m = length fl ∧
    w ∈ world M ∧
    (∃vl. length vl = length fl ∧
          rel M m (w # vl) ∧
          (∀i<length vl. csatis sig M (vl ! i) (fl ! i)))

Is there any thing I can do to let "unfold" automatically give me, instead of a conjunction, a list of assumptions instead, like:

using this:
    m ∈ mops sig

    marity sig m = length fl

    w ∈ world M

    (∃vl. length vl = length fl ∧
          rel M m (w # vl) ∧
          (∀i<length vl. csatis sig M (vl ! i) (fl ! i)))

Balazs Toth (Nov 05 2024 at 09:13):

I don't fully get the question, but I think you are looking for apply(intro conjI)

Yiming Xu (Nov 05 2024 at 09:34):

This is about intro but about elim, sorry for my poor presentation of the question.

Yiming Xu (Nov 05 2024 at 09:37):

If we have a definition like:
sth a b c \equiv A /\ B

and there is an assumption (assumption, not the target) sth a b c. Say, we are proving:

sth a b c ==> D

Then if we unfold sth_def, it will turn it into

A /\ B ==> D

But I do not like this, I want the goal to look like

assumptions:
- A
- B
target:
D

Yiming Xu (Nov 05 2024 at 09:38):

However, it seems not possible without opening another proof-qed block. There is "elim conjE', but it only applies to a separate proof-read block.

Yiming Xu (Nov 05 2024 at 09:40):

If it is tricky or even impossible then that is also understandable. I think it might be tricks to state definitions with conjunctions such that an "unfold" will not give a conjunction, but give a list of conjuncts that build up to the definition.

Balazs Toth (Nov 05 2024 at 09:45):

I don't understand what elim conjE is not doing but you want

Yiming Xu (Nov 05 2024 at 09:54):

Just because I do not want to open a proof-qed block. Otherwise it is what I want.

Yiming Xu (Nov 05 2024 at 09:55):

Since sometimes if I can take the conjuncts out, then I can finish it off by using (some_thm[OF some_conjunct]) with a dot. So a proof-qed block can be bulky in this case.

Mathias Fleury (Nov 05 2024 at 12:24):

OF conjI

Mathias Fleury (Nov 05 2024 at 12:24):

Full example:

context
  fixes A B :: bool
begin
definition t where
  ‹t ≡ (A ∧ B)›

lemma H: ‹t ⟹ A›
  sorry
thm H[unfolded t_def, OF conjI]

Yiming Xu (Nov 05 2024 at 12:38):

Thanks! My original question is actually asking, if we start the proof using t_def, then is there any method to write the definition of "t" such that

lemma H: "t ⟹ A"
  unfolding t_def

does not give

proof (prove)
goal (1 subgoal):
 1. A ∧ B ⟹ A

but instead, to give:

proof (prove)
goal (1 subgoal):
 assumptions
-A
- B

target  A

Knowing the "conjI" still makes me very happy. It is very useful!

Yiming Xu (Nov 05 2024 at 12:39):

Maybe some technology can be developed using induction principle of t I guess.

Yiming Xu (Nov 05 2024 at 12:40):

A/\ B ==> C ==> t ==> C

And use conjI to curry the A/\B maybe?

Yiming Xu (Nov 05 2024 at 12:42):

Seems to me that OF conjI strips only the first conjunct. Any thing to do to repeat the conjI until it cannot go any further?

Mathias Fleury (Nov 05 2024 at 12:49):

I often start proofs with

proof (intro conjI impI allI)

Mathias Fleury (Nov 05 2024 at 12:49):

And/or this thing:

method normalize_goal =
  (match premises in
    J[thin]: \<open>\<exists>x. _\<close> \<Rightarrow> \<open>rule exE[OF J]\<close>
  \<bar> J[thin]: \<open>_ \<and> _\<close> \<Rightarrow> \<open>rule conjE[OF J]\<close>
  )
....

proof normalize_goal+

Yiming Xu (Nov 05 2024 at 13:00):

Mathias Fleury said:

And/or this thing:

method normalize_goal =
  (match premises in
    J[thin]: \<open>\<exists>x. _\<close> \<Rightarrow> \<open>rule exE[OF J]\<close>
  \<bar> J[thin]: \<open>_ \<and> _\<close> \<Rightarrow> \<open>rule conjE[OF J]\<close>
  )
....

proof normalize_goal+

Isabelle does not accept this code. the method seems not recognised as a keyword.
image.png

Yiming Xu (Nov 05 2024 at 13:01):

If opening a proof block then I can just use elim. Nevertheless I have not seen the method thing and now I am curious what it is.

Mathias Fleury (Nov 05 2024 at 13:01):

You need Eisabach for that

Mathias Fleury (Nov 05 2024 at 13:02):

HOL-Eisbach.Eisbach_Tools (see https://isabelle.in.tum.de/website-Isabelle2024/dist/library/HOL/HOL-Eisbach/Example_Metric.html for an example)

Yiming Xu (Nov 05 2024 at 13:03):

Mathias Fleury said:

I often start proofs with
proof (intro conjI impI allI)

Aha I have it, it is in front of my office (Joking, I have heard that this is a thing for tactic writing. :-) .)

Yiming Xu (Nov 05 2024 at 13:03):

Mathias Fleury said:

HOL-Eisbach.Eisbach_Tools (see https://isabelle.in.tum.de/website-Isabelle2024/dist/library/HOL/HOL-Eisbach/Example_Metric.html for an example)

Thanks a lot and I will check it!

Yong Kiam (Nov 06 2024 at 15:48):

Mathias Fleury said:

I often start proofs with
proof (intro conjI impI allI)

why not proof (standard)?

Mathias Fleury (Nov 06 2024 at 16:09):

standard can do too much

lemma "A⇧*⇧* x y"
proof standard
(*
proof (state)
goal (2 subgoals):
 1. A⇧*⇧* x ?b
 2. A ?b y
*)

Mathias Fleury (Nov 06 2024 at 16:10):

and too little

lemma "∃x. A x ⟹ (∀x. B x ⟶ Q x)"
proof standard
(*⋀x. ∃x. A x ⟹ B x ⟶ Q x*)

Mathias Fleury (Nov 06 2024 at 16:10):

so you want standard+ actually

Mathias Fleury (Nov 06 2024 at 16:11):

which is also doing too much:

lemma "∃x. A x ⟹ (∀x. B x ⟶ rtranclp Q x y)"
proof standard+
(*
⋀x. ∃x. A x ⟹ B x ⟹ Q x y
*)

Mathias Fleury (Nov 06 2024 at 16:26):

and it is sometimes unintuitive:

lemma "A⇧*⇧* x y"
proof standard+
(*
A⇧*⇧* x y
*)

(first example again with a +)

Yiming Xu (Nov 06 2024 at 17:22):

I have not encountered "standard". I see! The behavior onA^** indeed looks confusing.

I sometimes use safe.

Yiming Xu (Nov 06 2024 at 17:22):

But it does not do the elimination.

Yong Kiam (Nov 07 2024 at 02:59):

thanks for the examples!

Mathias Fleury (Nov 07 2024 at 05:59):

Yiming Xu said:

I have not encountered "standard". I see! The behavior onA^** indeed looks confusing.

I sometimes use safe.

proof is the same as proof standard. So it is usually not spelled out explicitly unless you really want to apply it several times

Yiming Xu (Nov 07 2024 at 12:28):

Mathias Fleury said:

Yiming Xu said:

I have not encountered "standard". I see! The behavior onA^** indeed looks confusing.

I sometimes use safe.

proof is the same as proof standard. So it is usually not spelled out explicitly unless you really want to apply it several times

I see. That is the "proof -" is getting rid of.

Last updated: Dec 21 2024 at 16:20 UTC