Stream: Beginner Questions

Topic: Proving ==

Gergely Buday (Aug 01 2023 at 10:26):

Does it make sense to have the following goal?

lemma double_negation_equivalence: "A == (¬¬A)"

which results in

proof (prove)
goal (1 subgoal):
 1. A ≡ ¬ ¬ A

and the command proof is not able to deconstruct it to LHS ==> RHS and RHS ==> LHS, as it would do for

lemma j2: "A = (¬¬A)"
proof

whose proof state is

proof (state)
goal (2 subgoals):
 1. A ⟹ ¬ ¬ A
 2. ¬ ¬ A ⟹ A

Is the only place I can use ≡ in definitions, not goals?

Mathias Fleury (Aug 01 2023 at 11:14):

The only place where you need ≡ is in abbreviations

Mathias Fleury (Aug 01 2023 at 11:14):

Everywhere else = works

Mathias Fleury (Aug 01 2023 at 11:14):

(although it might have the wrong priority)

Wolfgang Jeltsch (Aug 01 2023 at 12:01):

You can use ≡ also in goals, but you have to be aware that it is the “low-level”, that is, meta-level, equality, the one of Isabelle/Pure, which comes with different pre-proved facts and different configurations of proof methods.

In your particular example, you can “cheat” by going from ≡ to = first:

lemma double_negation_equivalence:
  shows "A ≡ ¬ ¬ A"
proof (rule eq_reflection, standard)
  assume A
  then show "¬ ¬ A"
    by simp
next
  assume "¬ ¬ A"
  then show A
    by simp
qed

Wolfgang Jeltsch (Aug 01 2023 at 12:11):

Everywhere else = works (although it might have the wrong priority)

The priority of = is often unfortunate in equalities of booleans (for example in definitions), as = binds stronger than the typical logical connectives. However, in these situations you can use ⟷ instead, which is just an abbreviation of = restricted to bool and which has a lower priority than operators like ∧.

Gergely Buday (Aug 01 2023 at 12:13):

@Wolfgang Jeltsch yes at some point I had to write

lemma j2: "A = (¬¬A)"

without the parentheses it would not even parse.

Wolfgang Jeltsch (Aug 01 2023 at 12:14):

I would always use ⟷ in such cases, which is also what you would find in ordinary mathematical texts.

Wolfgang Jeltsch (Aug 01 2023 at 12:19):

By the way, I first tried to prove the above meta-level equality (A ≡ ¬ ¬ A) by boolean case distinction, trying to show it separately for False and True. However, this failed because the case_split fact, like probably all elimination rules in Isabelle/HOL, uses a conclusion that has type bool, while ≡ has result type prop. This is the type of propositions of Isabelle/Pure. Using bool for propositions in Isabelle/HOL works because there is an implicit conversion from bool to prop, but there is no conversion that would go in the other direction. So here is another reason why proving ≡-statements is hard: the pre-proved Isabelle/HOL facts you might want to use work with bool instead of prop.

I think, it’s best to adopt the following style:

• For implication, conjunction, and universal quantification use Isabelle/Pure operators whenever possible, because these work better with proof methods, for example.
• For equality, use the Isabelle/HOL operator whenever possible.

Last updated: Dec 21 2024 at 16:20 UTC