Stream: Beginner Questions

Topic: Proving lemma with definite description

Lekhani Ray (Jul 28 2022 at 19:59):

Hello!

I am trying to prove a lemma for plus with definite description

lemma (in th8a) th8_a: "∀f. q f ⟶ plus = f"
  apply(simp add: th8_a_2 plus_def)

Isabelle cannot seem to recognize anything after this

Supporting context:

locale th8a = th1 +
  assumes
    "((∀x . p zero ∧ (∀x. p x ⟶ p (suc x))) ⟶ (∀x. p x))"
begin
definition
 plus where plus_def: "plus = (THE f. ∀ x y. f x zero = x ∧ f x (suc y) = suc (f x y))"
definition
 times where "times = (THE g. ∀ x y. g x zero = zero ∧ g x (suc y) = plus (g x y) x)"
end

fun (in th8a) q :: "('a ⇒ 'a ⇒ 'a) ⇒ bool"
  where
"q f = (∀ x y. (f x zero = x ∧ f x (suc y) = suc (f x y)))"

lemma (in th8a) th8_a_2: "plus = (THE f. q f)"
  apply(simp add: plus_def)
  done

Any pointers on how to move forward with lemma th8_a_2?

Mathias Fleury (Jul 29 2022 at 05:03):

You probably need theI

Mathias Fleury (Jul 29 2022 at 05:04):

But typically proofs on choice are very painful.

Manuel Eberl (Jul 29 2022 at 12:43):

My personal approach is:

1. hide the operator behind a definition (using definition on toplevel or define in an Isar proof)
2. prove unique exists (with the ∃! operator)
3. use the introduction rules for the operator (my favourite ones are theI', the1_equality, and someI_ex) to prove the properties that you expect
4. never unfold the definition of the operator again; just work with the derived properties

That involves a little bit of boilerplate once, but it is fairly pain free.

Mathias Fleury (Jul 29 2022 at 12:48):

The boilerplate part is what I called »painful«

Manuel Eberl (Jul 29 2022 at 12:52):

There's also the specification command, but it's a bit old-fashioned and only works on the toplevel. One could perhaps write a more modern version of that at some point…

Manuel Eberl (Jul 29 2022 at 12:53):

In an Isar proof, you can often also get away just using obtain (possibly combined with an application of the axiom of choice, which e.g. metis does very well automatically) instead of using SOME.

Lekhani Ray (Aug 03 2022 at 18:23):

Manuel Eberl said:

My personal approach is:

1. hide the operator behind a definition (using definition on toplevel or define in an Isar proof)
2. prove unique exists (with the ∃! operator)
3. use the introduction rules for the operator (my favourite ones are theI', the1_equality, and someI_ex) to prove the properties that you expect
4. never unfold the definition of the operator again; just work with the derived properties

That involves a little bit of boilerplate once, but it is fairly pain free.

Thank you both @Manuel Eberl and @Mathias Fleury for your comments.

With respect to point 2:
I have started with

lemma (in th8a) th8_a2: "∃! f. q f"
  apply(rule theI' the1_equality someI_ex)
apply(simp add: th8_a_2)
  apply auto

where th8_a_2 is

lemma (in th8a) th8_a_2: "plus = (THE f. q f)"
  apply(simp add: plus_def)
  done

Questions:

1. Does the order of the applications matter? [eg. If I switch the order of theI', the1_equality etc)
2. With every application of auto, the subgoals keep on increasing. What may be the reason?
3. Is the expression in the lemma the correct expression?

Thank you!

Lawrence Paulson (Aug 16 2022 at 09:47):

The rule method attempts the rules in the order given, from left to right. Put the most specific rules at the beginning.

The auto method is designed to do all of its work in one call. With rare exceptions, a second application of auto with the same arguments should fail.

Last updated: Apr 20 2024 at 08:16 UTC