Convention for dealing with definition with multiple clauses · Beginner Questions

Stream: Beginner Questions

Topic: Convention for dealing with definition with multiple clauses

Yiming Xu (Jan 27 2025 at 18:25):

There are many definitions of such a format:

definition bounded_morphism ::
"('m set × ('m ⇒ nat)) × 'p set ⇒
 ('a ⇒ 'b) ⇒ ('m,'p,'a) model => ('m,'p,'b) model => bool"
where
"bounded_morphism sig f M M' ⟷
 (∀w. w ∈ world M ⟶ f w ∈ world M') ∧
 (∀w p. p ∈ props sig ⟶ w ∈ world M ⟶ valt M p w = valt M' p (f w)) ∧
 (∀m wl. in_rel_dom sig m wl ⟶ List.set wl ⊆ world M ⟶ rel M m wl ⟶ rel M' m (map f wl)) ∧
 (∀m w v'l. w ∈ world M ⟶ in_rel_dom sig m (f w # v'l) ⟶  List.set v'l ⊆ world M' ⟶
  (∃vl. List.set vl ⊆ world M ∧ rel M m (w # vl) ∧ map f vl = v'l))"

The definition consists of four conjunctions, each referring to a different property. In some proofs, one perhaps each one of these properties each time. I wonder what people will suggest on dealing with such cases: do we want to define four properties accordingly, and then define bounded_morphisms sig f M M' <==> property1 sig f M M' /\ ... /\ property 4 sig f M M', or do we want to prove some trivial lemmas such as:

lemma bounded_morphism_cod:
 "bounded_morphism sig f M M' ⟹ w ∈ world M ⟶ f w ∈ world M'"
  unfolding bounded_morphism_def by blast

and use it instead of directly relying on the definition when dealing with specific goals?

I know that people have different preferences. I just want to know if any of you want to encourage or discourage certain approaches because of certain reasons. Since it is a common thing, I also wonder if Isabelle already has some features to deal with that.

Mathias Fleury (Jan 27 2025 at 18:33):

My rule of thumb: if you can on a first glance know what the conjunction means (and if it is not introducing new variables), then the conjunction is fine. Otherwise, you want to give it a name that you can understand.

In my experience this also roughly matches how you do the proofs: if it is complicated, you are want to manipulate the thing as a whole instead of unfolding the definition each time.

For example, even vs ?x. n = 2*x: sometimes you want the x, but often you want manipulate the even concept directly.

Mathias Fleury (Jan 27 2025 at 18:33):

lemma bounded_morphism_cod:
 "bounded_morphism sig f M M' ⟹ w ∈ world M ⟶ f w ∈ world M'"
  unfolding bounded_morphism_def by blast

Ah the good old dest rules. Always a pain to write and you never know if it is a good one or a bad one.

Yiming Xu (Jan 27 2025 at 18:40):

Do you mean the lemma is pain to write? Or pain to use?

Yiming Xu (Jan 27 2025 at 18:41):

If pain to use, then why? I think I already find such a thing helpful.

Yiming Xu (Jan 27 2025 at 18:44):

Otherwise, you want to give it a name that you can understand.
Since I am rather familiar with them I can immediately tell what they means, but they do address different things and hence may deserve names. Is it possible to give the conjuncts of a definition separate names without defining them outside the definition individually?

Mathias Fleury (Jan 27 2025 at 18:51):

Yiming Xu said:

Do you mean the lemma is pain to write? Or pain to use?

a pain to read if it is in a goal

Mathias Fleury (Jan 27 2025 at 18:51):

I hate if I have a lemma, apply auto and see 230 goals generated

Yiming Xu (Jan 27 2025 at 18:52):

Ah I am not going to add it into the goal. I would like to feed it instead of the original definition to sledgehammer.

Yiming Xu (Jan 27 2025 at 18:52):

Ah? I am unclear with it, how do you use such a thing with auto and see 230 goals generated?

Mathias Fleury (Jan 27 2025 at 18:53):

Yiming Xu said:

Since I am rather familiar with them I can immediately tell what they means, but they do address different things and hence may deserve names. Is it possible to give the conjuncts of a definition separate names without defining them outside the definition individually?

Sure. But in 6 months? Usually, the right moment to decide is when you refactor the definitions for the first time.

Mathias Fleury (Jan 27 2025 at 18:54):

Yiming Xu said:

Ah? I am unclear with it, how do you use such a thing with auto and see 230 goals generated?

In your case bounded_morphism produces 5 goals. If there are 2 booleans in each goal, you get to 2*2*5 = 20 goals. And here we did not look at the goal yet