Stream: Beginner Questions

Topic: subsetI followed by an induction

Yiming Xu (Oct 20 2024 at 05:33):

I would like to prove:

lemma gen_set_subset_world :
  assumes M: "is_model sig M" and X : "X ⊆ world M"
  shows "gen_set (rel M) X  ⊆ world M"

I want to start with proof (intro subsetI,induction rule:gen_set.induct) but it complains "Failed to apply initial proof method". May I please ask why?
If I delete induction rule:gen_set.induct, then intro subsetI works correctly, and gives the goal:

 1. ⋀x. x ∈ gen_set Op (rel M) X ⟹ x ∈ world M

The induction principle looks gen_set.induct looks like this:

?x ∈ gen_set ?Op ?R ?X ⟹
(⋀x. x ∈ ?X ⟹ ?P x) ⟹
(⋀w m ul u.
    w ∈ gen_set ?Op ?R ?X ⟹
    ?P w ⟹ m ∈ ?Op ⟹ ?R m (w # ul) ⟹ u ∈ list.set ul ⟹ ?P u) ⟹
?P ?x

Any attempt to help would be very appreciated!

Mathias Fleury (Oct 20 2024 at 06:52):

The problem is the ⋀. The high-level tactics do not unify the x from the theorem with the x from the assumptions. So either you go for the more low-level version:

proof (intro subsetI, induct_tac rule:gen_set.induct, assumption)

(_tac is the low-level version and you need to unify with assumption)

Mathias Fleury (Oct 20 2024 at 06:54):

Or you go with a nested proof block:

lemma gen_set_subset_world :
  assumes M: "is_model sig M" and X : "X ⊆ world M"
  shows "gen_set (rel M) X  ⊆ world M" (is ‹?set ⊆ ?W›)
proof (intro subsetI)
  fix x
  assume ‹x ∈ ?set›
  then show ‹x ∈ ?W›
  proof (induction rule: gen_set.induct)

Yiming Xu (Oct 20 2024 at 07:02):

Thanks! I see. (For terminology, I conceive "high-level" means HOL level, and "low level" means "meta-level" here. Thanks for correcting me if I misunderstand.)

Mathias Fleury (Oct 20 2024 at 07:10):

Isabelle has this distinction between nice "user-level" tactics (induction, rule, ...) and the "older lower-level" version of them (induct_tac, rule_tac, ...), which allow you to write things that are bad.

For example: you can write rule_tac x=x in exI to provide the witness, but this x can refer to an internal name, meaning that if the naming convention ever changes, the proof might break.

Mathias Fleury (Oct 20 2024 at 07:11):

I am not sure if there is a proper name for this distinction

Yiming Xu (Oct 20 2024 at 07:16):

I see. Then it might be safer to avoid the low-level versions, but it is very good to know.
Seems to me that the user-level tactics might be packed up from the low-level ones though.

Mathias Fleury (Oct 20 2024 at 14:03):

Seems to me that the user-level tactics might be packed up from the low-level ones though.

They are

Yiming Xu (Oct 20 2024 at 14:10):

Aha, a lucky guess! Thank you that is good to know.

Last updated: Dec 21 2024 at 16:20 UTC