Stream: Beginner Questions

Topic: using and applying rule

Kevin Kappelmann (May 28 2020 at 08:59):

I need help getting using and rule to work together:

definition "P ≡ False" (* this is not important *)

lemma myLem: "P ⟹ A" (* a rule I want to use *)
  unfolding P_def by simp

lemma assumes "A" "A ⟹ P" shows "C"
  using assms by (rule myLem) (* Failed to apply initial proof method - how can I make it work? *)

lemma "⟦A; A ⟹ P⟧ ⟹ C"
  by (rule myLem) (* Works just fine *)

Kevin Kappelmann (May 28 2020 at 09:00):

Note: I want to insert assms with using because in my actual application, the (rule myLem) command is followed by an auto (or something more complicated) that needs to use assms.

Josh Chen (May 28 2020 at 09:02):

I always forget this issue and keep running into it too. rule does some funny thing with facts from using, try intro instead.

Kevin Kappelmann (May 28 2020 at 09:03):

intro loops because A is arbitrary :/

Lukas Stevens (May 28 2020 at 09:05):

what about apply(rule myLem) using assms by auto?

Kevin Kappelmann (May 28 2020 at 09:05):

that surely works, but I'd like to avoid apply

maximilian p.l. haslbeck (May 28 2020 at 09:09):

apply - apply rule

Josh Chen (May 28 2020 at 09:11):

I guess by (rule myLem) (auto intro: assms) would work.

Josh Chen (May 28 2020 at 09:11):

but then just auto intro: assms works as well, so... :grinning: No it doesn't! What?...

Kevin Kappelmann (May 28 2020 at 09:12):

hmm, what's actually going on if I do using facts by auto? In what way is auto picking up facts? As simp rules?

Kevin Kappelmann (May 28 2020 at 09:14):

Josh Chen said:

but then just auto intro: assms works as well, so... :grinning: No it doesn't! What?...

Because it does not know about myLem

Josh Chen (May 28 2020 at 09:14):

D'oh! auto intro: myLem assms works.

Josh Chen (May 28 2020 at 09:15):

Kevin Kappelmann said:

hmm, what's actually going on if I do using facts by auto? In what way is auto picking up facts? As simp rules?

I want to know this too, maybe it's in the docs somewhere, but I don't recall having seen something about exactly how using uses facts.

Kevin Kappelmann (May 28 2020 at 09:22):

Here's a relevant e-mail thread about the difference between using facts by auto and auto simp: facts.

Kevin Kappelmann (May 28 2020 at 09:25):

with some interesting insights like using fixing type variables and hence instantiation can fail (though not relevant in my case) and facts in using being simplified but not if added as a simp rule.

Kevin Kappelmann (May 28 2020 at 09:28):

But still, my 2 questions are open:

1. can I replace rule with some tactic X such that using assms by (X myLem) auto works?
2. how is auto picking up facts/assumptions in the goal state (e.g. inserted with using)? Are they used as simp rules? If so, I would replace using assms by (X myLem) by by (X myLem) (auto simp: assms)

Kevin Kappelmann (May 28 2020 at 09:32):

(Note: I could also do by (rule myLem, insert assms) auto, but that gives me bad feelings, haha)

Kevin Kappelmann (May 28 2020 at 09:50):

Kevin Kappelmann said:

how is auto picking up facts/assumptions in the goal state (e.g. inserted with using)? Are they used as simp rules? If so, I would replace using assms by (X myLem) by by (X myLem) (auto simp: assms)

I guess the answer is no - when assms are used for some registered dest rule, I get different results.

Simon Wimmer (May 28 2020 at 11:24):

Does this help you? https://github.com/isabelle-prover/cookbook/blob/master/src/proofs/methods/Chained_Facts.thy

Simon Wimmer (May 28 2020 at 11:24):

I think at least part of the issues are covered there

Simon Wimmer (May 28 2020 at 11:25):

But now it seems that I even need to add more information

Simon Wimmer (May 28 2020 at 11:27):

Kevin Kappelmann said:

But still, my 2 questions are open:

1. can I replace rule with some tactic X such that using assms by (X myLem) auto works?
2. how is auto picking up facts/assumptions in the goal state (e.g. inserted with using)? Are they used as simp rules? If so, I would replace using assms by (X myLem) by by (X myLem) (auto simp: assms)

Following the terminology I use in the cookbook entry, auto should be a simple method, hence the facts should be inserted into the goal state. This means that the classical-reasoner part of auto should do nothing special with them, and the simplifier part should use them for rewriting in the same way that simp does.

Simon Wimmer (May 28 2020 at 11:31):

Josh Chen said:

D'oh! auto intro: myLem assms works.

Btw, you will also find cases where by (rule myLem) (auto intro: assms) works but by (auto intro: myLem assms) won't. The reason is that afaik per default auto uses the classical reasoner with a search depth of 2. Thus by (auto 4 3 intro: myLem assms) should be a more robust translation. The first parameter sets the search depth for blast and the second the sets the search depth of the classical reasoner. And even then, by (auto 4 3 intro: myLem assms) may not terminate in some cases, while by (rule myLem) (auto intro: assms) will.

Simon Wimmer (May 28 2020 at 11:32):

(note that this may still contain some slight inaccuracies, it is just inferred from my understanding of these things that I gathered over the years)

Simon Wimmer (May 28 2020 at 11:34):

(And we should certainly add an entry about auto and friends to the cookbook)

Lukas Stevens (May 28 2020 at 11:38):

Damn, I didn't know you could adjust the search depth.

Kevin Kappelmann (May 28 2020 at 21:04):

That cookbook entry is fantastic! Helped me understanding things so much better - thank you! :smiley:

Manuel Eberl (Jun 19 2020 at 11:40):

Kevin Kappelmann said:

But still, my 2 questions are open:

1. can I replace rule with some tactic X such that using assms by (X myLem) auto works?
2. how is auto picking up facts/assumptions in the goal state (e.g. inserted with using)? Are they used as simp rules? If so, I would replace using assms by (X myLem) by by (X myLem) (auto simp: assms)

I usually use X = intro in these cases. Doesn't do exactly the same as rule (it applies the intro-rule repeatedly), but it usually gets the job done. Another possibility is by (rule myLem) (use assms in auto). Note however that if you want to give additional arguments to the auto in the last one, it has to be put in cartouches.

Last updated: Dec 21 2024 at 16:20 UTC