[isabelle] Meta-implication in a premise · Mirror: Isabelle Users Mailing List

I've now encountered a similar, but reversed problem: OF and THEN don't
work as expected with a premise that contains a meta-implication.

notepad
begin
fix P Q R
assume a: "(P ⟹ Q) ⟹ R"
assume b: "P ⟹ Q"
thm a [OF b]
thm b [THEN a]
(* expected R, got (P ⟹ P) ⟹ R *)
end

I would like to compose two facts, one of which matches the first premise
of the other one (up to unification), just like AppP does. Is there a way
to achieve this?

Email Gateway (Apr 28 2024 at 19:41):

notepad
begin
fix P Q R
assume a: "(P ⟹ Q) ⟹ R"
assume b: "P ⟹ Q"
thm a [OF b, simplified]
thm b [THEN a, simplified]
end

Frédéric Boulanger
CentraleSupélec - Département Informatique Laboratoire Méthodes Formelles (LMF)
3 rue Joliot-Curie, 91192 Gif-sur-Yvette cedex Bât. 650 - 1 rue Raimond Castaing, 91190 Gif-sur-Yvette
+33 [0]1 75 31 78 32‬

Email Gateway (Apr 29 2024 at 08:18):

From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Here's an option if you don't mind using the AFP:

theory Scratch
   imports
     ML_Unification.ML_Unification_HOL_Setup
     ML_Unification.Unification_Attributes
begin

notepad
begin
   fix P Q R
   assume a: "(P ⟹ Q) ⟹ R"
   assume b: "P ⟹ Q"
   (*the result you want*)
   thm a[uOF b]
   (*the result you get when using OF*)
   thm a[uOF b where mode = resolve]
end

end

Email Gateway (Apr 29 2024 at 09:13):

From: Makarius <makarius@sketis.net>
The question is what to expect, or rather how Isabelle/Pure really works.

The "implementation" manual has some explanations in chapter 2, notably
section "2.4.2 Rule composition". The Isabelle/Isar proof language also works
within this school of thinking.

So the canonical meta-question is: What are you trying to do? What is your
application?

Email Gateway (Apr 30 2024 at 20:49):

From: Roland Lutz <rlutz@hedmen.org>
Unfortunately, in my case, this doesn't work:

The theorem I'm using is while_option_commute, and the terms ?b and ?b'
both have the form (λx. cur x ≠ 0) in the facts I use.

Email Gateway (May 01 2024 at 14:25):

From: Lawrence Paulson <lp15@cam.ac.uk>
Isabelle implements a logical framework (Pure) and the operators it provides for doing proofs rely on that framework to put user-level proofs together: in some object logic, typically HOL. The kernel does provide some primitives allowing you to perform derivations within Pure, but they are low-level, not well documented, and not easily reached from Isar.

Email Gateway (May 01 2024 at 19:46):

In the terminology of this section, what I want to do is close a branch by
composing with a fact (that isn't necessarily atomic).

What I'm trying to do, on a meta-level, is learn how to prove things in
Isabelle. Despite having spent quite some time with Isabelle now, I still
find myself struggling to do even simple things.

In my previous question, I've been trying to prove by induction that 2ⁿ ≤
n! for n ≥ 4:

theorem fac_outgrows_powers_of_two:
fixes n :: nat
assumes "n ≥ 4"
shows "2 ^ n ≤ fac n"
proof ...
fix n :: nat
assume "n = 4"
thus "2 ^ n ≤ fac n" ...
next
fix n :: nat
assume "n > 4" and "2 ^ (n - 1) ≤ fac (n - 1)"
hence "2 * 2 ^ (n - 1) ≤ n * fac (n - 1)" ...
thus "2 ^ n ≤ fac n" ...
qed

lemma induction_from_start:
fixes P :: "nat ⇒ bool"
fixes n₀ :: "nat"
assumes "⋀n. n = n₀ ⟹ P n"
assumes "⋀n. n > n₀ ⟹ P (n - 1) ⟹ P n"
shows "⋀n. n ≥ n₀ ⟹ P n"
using assms by (metis dec_induct diff_Suc_1 le_imp_less_Suc)

theorem fac_outgrows_powers_of_two:
fixes n :: nat
assumes "n ≥ 4"
shows "2 ^ n ≤ fac n"
proof (rule assms [THEN [3] induction_from_start])
fix n :: nat
assume "n = 4"
thus "2 ^ n ≤ fac n" unfolding fac_def by simp
next
fix n :: nat
assume "n > 4"
hence "n > 0" by fastforce
assume "2 ^ (n - 1) ≤ fac (n - 1)"
hence "2 * 2 ^ (n - 1) ≤ n * fac (n - 1)"
using ‹n > 4› by (simp add: mult_le_mono)
moreover have "2 * 2 ^ (n - 1) = 2 ^ n"
using ‹n > 0› by (simp add: power_eq_if)
moreover have "n * fac (n - 1) = fac n"
using ‹n > 0› by (metis One_nat_def Suc_pred fac.simps(2))
ultimately show "2 ^ n ≤ fac n" by (rule box_le)
qed

While that works, it took me a long time to figure out, and I'm not too
happy about the result (in particular, about the initial proof method and
the two separate helper lemmata).

Being able to write structured proofs in Isar is great; it's the low-level
stuff leaking through the gaps that's driving me insane. It often happens
that I have some assumptions and a goal, and I know they fit together, I
just can't figure out what to tell Isabelle to make it work.

From a conceptual point of view, I really miss composability: the ability
to break complex things down into an equivalent combination of more
elementary building blocks.

Email Gateway (May 01 2024 at 22:10):

From: "John F. Hughes" <jfh@cs.brown.edu>
As a comparative beginner, I'm almost certainly the wrong person to advise
you on your more general problem, but it seems to me that your initial
lemma isn't expressing the thing you wanted to express. It should probably
be something more like this:

lemma induction_from_start:
fixes P:: "nat ⇒ bool"
fixes s::"nat"
assumes "P s"
assumes "⋀n. n > s ⟹ P (n - 1) ⟹ P n"
shows "⋀n. n ≥ s ⟹ P n"

i.e., you assume that for some fixed starting point s, P is true, and
that inductive steps work for anything bigger than s. You've used "n" both
for the starting point and for the induction variable, and I think that's
not what you want.

You've also used subtraction, and that may have coerced things to be ints
rather than nats or something, so a rewritten form would be:

lemma induction_from_start:
fixes P:: "nat ⇒ bool"
fixes s::"nat"
assumes "P s"
assumes "⋀n. n ≥ s ⟹ P (n) ⟹ P (Suc n)"
shows "⋀n. n ≥ s ⟹ P n"

which uses the Successor, which is what induction over the naturals works
well on.

(highlight mine). The highlighted theorem in fact says exactly what
you're trying to say in your lemma. It's in $ISABELLE_HOME/src/HOL/Nat.thy,
which I found by typing

in my file and then command-clicking on nat_induct_at_least with my cursor
(use ctrl-click on Windows), which then opened up the definition of the
lemma for me to look at.

I hope this is of some help. I definitely know how it feels to struggle
with this stuff.

Email Gateway (May 01 2024 at 23:41):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
The rule nat_induct_at_least will work for this if the condition n ≥ 4 is incorporated
into the conclusion to be proved, so that it is available in the induction step:

theorem fac_outgrows_powers_of_two:
shows "n ≥ 4 ⟹ 2 ^ n ≤ fac n"
proof (induct n rule: nat_induct_at_least)
show "2 ^ 4 ≤ fac 4"
by (simp add: numeral_3_eq_3 numeral_Bit0)
fix n
assume 1: "4 ≤ n" and 2: "2 ^ n ≤ fac n"
have "2 ^ Suc n ≤ n * 2 ^ n"
using 1 by simp
also have "... ≤ n * fac n"
using 1 2 by simp
also have "... ≤ fac (Suc n)"
by simp
finally show "2 ^ Suc n ≤ fac (Suc n)"
by blast
qed

I would like to be able to collapse some of the steps, but then I am not very good with
getting Isabelle to do arithmetic reasoning. The base case was proved with
Sledgehammer. It seems that automatic conversion of numerals into 0/Suc form
stops at 3, so some funny business is required to turn the numeral 4 into something
that the simplification rules for function fac can deal with.

As far as the induction proof is concerned, the approach I would take is to first work
on stating the result in such a way that one of the available induction rules can
understand it and produce subgoals that look like they are sensible and true.
I don't know the available induction rules here particularly well, but John saved the
day by pointing out the rule nat_induct_at_least.

Email Gateway (May 02 2024 at 07:57):

notepad
begin
fix cur::"'a ⇒ nat" and cur'::"'b ⇒ nat" and f1::"'a ⇒ 'b" and
c1::"'a ⇒ 'a" and c'1::"'b ⇒ 'b"
define b1 where "b1 = (λx. cur x ≠ 0)"
define b'1 where "b'1 = (λx. cur' x ≠ 0)"
assume p1: "⋀s::'a. b1 s = b'1 (f1 s)"
assume p2: "⋀s::'a. b1 s ⟹ f1 (c1 s) = c'1 (f1 s)"
thm while_option_commute[of b1 b'1 f1 c1, OF p1 p2, simplified] (*
obtain the desired statement *)
thm while_option_commute[OF p1 p2, simplified] (*error: THM 0 raised *)
end

Email Gateway (May 02 2024 at 08:50):

From: Thomas Sewell <tals4@cam.ac.uk>
I hope this isn't too flippant, but I thought that the stages of this discussion were typical in a humorous way:

original poster: I'm trying to get some specialised features of the Pure meta-logic to do exactly what I want and getting confused.
Makarius: what are you trying to do, anyway?
original poster: Oh, I'm trying to do an induction proof about a recursive function on naturals in HOL.

* From a conceptual point of view, I really miss composability: the ability
* to break complex things down into an equivalent combination of more
*
elementary building blocks.

I think that this is exactly the right instinct. If you feel blocked from proceeding this way, it's probably because you don't
yet know enough moves in Isabelle.

As others have pointed out, the library contains nat_induct_at_least which is very similar to your induction_from_start lemma.
It's also already been set up with the attribute [consumes 1], which doesn't change its logical meaning but is a hint to the
induct method to prove its first premise immediately by consuming an assumption (much like erule), which results in the desired
induction shape.

Indeed, induct is a bit of a complex beast, and it's not straightforward to replicate some of its behaviour step-by-step. The special
feature of induct is that it handles rules whose conclusion is of the shape "?P ?x ?y", which would normally be too general for
unification to consistently do what you want. Unfortunately, if you take either your lemma or the one from the library and compose
it with the assumption "n >= 4" as a single step, this fixes "?n" to "n", and you no longer have a standard-shape induction lemma,
so the induct mechanism won't do the right thing with it. This might be why you're falling back to quite primitive mechanisms.

If you do want to do every step yourself, I'd recommend you use "where" to pin the variables in your rule rather than OF/THEN to
combine it with other steps. Don't misunderstand me, unification is super handy, and OF/THEN are really useful, but usually in
cases where the unification is constrained and will necessarily do what you want. For instance, this might be useful:

An intermediate option is to just set the lower bound in your rule ('s' in John's rephrasing of your rule). That variable appeared in
the premises but not the conclusion of the induction rule, so it was always a risk for going wrong. This seems to be a valid way
to start your proof:
proof (induct n rule: induction_from_start[where s="4"])

Finally, you can chain equalities or inequalities with the 'also have ...' mechanism in the Isar proof language. This is a bit specialised
but it is really useful when your goal is to prove an inequality. Using that mechanism would avoid the need for your box_le lemma.

I do sometimes end up needing to do transitivity manually in some cases. Theorems like order_le_less_trans can be useful.

It occurs to me that the steps of your box_le lemma aren't in the naming scheme, since you don't need a named rule to apply an
equality. You can single-step apply an equality rewrite with the subst method.

More broadly, once you know a sufficient set of mechanisms, you'll find that you can usually do things a step at a time if you need
to. Automation is useful too. I appreciate that induction is a bit of an exception.

As a comparative beginner, I'm almost certainly the wrong person to advise you on your more general problem, but it seems to me that your initial lemma isn't expressing the thing you wanted to express. It should probably be something more like this:

lemma induction_from_start:
fixes P:: "nat ⇒ bool"
fixes s::"nat"
assumes "P s"
assumes "⋀n. n > s ⟹ P (n - 1) ⟹ P n"
shows "⋀n. n ≥ s ⟹ P n"

i.e., you assume that for some fixed starting point s, P is true, and that inductive steps work for anything bigger than s. You've used "n" both for the starting point and for the induction variable, and I think that's not what you want.

You've also used subtraction, and that may have coerced things to be ints rather than nats or something, so a rewritten form would be:

lemma induction_from_start:
fixes P:: "nat ⇒ bool"
fixes s::"nat"
assumes "P s"
assumes "⋀n. n ≥ s ⟹ P (n) ⟹ P (Suc n)"
shows "⋀n. n ≥ s ⟹ P n"

which uses the Successor, which is what induction over the naturals works well on.

(highlight mine). The highlighted theorem in fact says exactly what you're trying to say in your lemma. It's in $ISABELLE_HOME/src/HOL/Nat.thy, which I found by typing

in my file and then command-clicking on nat_induct_at_least with my cursor (use ctrl-click on Windows), which then opened up the definition of the lemma for me to look at.

I hope this is of some help. I definitely know how it feels to struggle with this stuff.

On Wed, May 1, 2024 at 3:46 PM Roland Lutz <rlutz@hedmen.org<mailto:rlutz@hedmen.org>> wrote:
On Mon, 29 Apr 2024, Makarius wrote:

In the terminology of this section, what I want to do is close a branch by
composing with a fact (that isn't necessarily atomic).

What I'm trying to do, on a meta-level, is learn how to prove things in
Isabelle. Despite having spent quite some time with Isabelle now, I still
find myself struggling to do even simple things.

In my previous question, I've been trying to prove by induction that 2ⁿ ≤
n! for n ≥ 4:

While that works, it took me a long time to figure out, and I'm not too
happy about the result (in particular, about the initial proof method and
the two separate helper lemmata).

From a conceptual point of view, I really miss composability: the ability
to break complex things down into an equivalent combination of more
elementary building blocks.

Email Gateway (May 02 2024 at 10:34):

From: Lawrence Paulson <lp15@cam.ac.uk>
I would never belittle the difficulty of getting even simple proofs out of an ITP. There are any number of pitfalls, and trying to prove something is particularly frustrating when it is obvious.

I tackled this problem (using that wonderful induction rule nat_induct_at_least, which I hadn't heard of) and got the following:

theorem fact_outgrows_powers_of_two:
shows "n ≥ 4 ⟹ 2 ^ n ≤ (fact n::nat)"
proof (induct n rule: nat_induct_at_least)
case base
then show ?case
by (auto simp: eval_nat_numeral)
next
case (Suc n)
with Suc_le_D show ?case
by (fastforce simp add: eval_nat_numeral)
qed

There are two fine points to note. First I am using the built-in factorial (fact), which is overloaded over numeric types, so the type constraint is necessary. And two, rewriting by eval_nat_numeral transforms numerals into Suc-form, which you need here. The lemma Suc_le_D what suggested by sledgehammer.

Email Gateway (May 02 2024 at 10:35):

From: Lawrence Paulson <lp15@cam.ac.uk>
In this case I'm really surprised if sledgehammer cannot figure it out. That really is precisely what it is for.
Larry

Email Gateway (May 04 2024 at 17:20):

From: Lawrence Paulson <lp15@cam.ac.uk>
Quite a few users, especially newbies, want to use Isabelle to explore proofs at a low level, basically in terms of individual rule applications. Isabelle is not designed for this application. It’s worth bearing in mind that proofs of even trivial facts can be enormous if broken down in that way.

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Meta-implication in a premise

Email Gateway (Apr 28 2024 at 19:14):