## Stream: Beginner Questions

### Topic: Difference between = and ≡

#### Benedikt Ahrens (Mar 17 2021 at 19:54):

Hi everyone,

I am (re)learning Isabelle right now, and I have a question regarding the difference between = and ≡, and their uses in Isabelle/HOL.
Specifically, in the (allegedly outdated) Isabelle Tutorial, it says that ≡ should be used for constant definitions (see Section 2.7.2 Constant Definitions), and the following example is given:

``````definition nand :: gate where "nand A B ≡ ¬(A ∧ B)"
``````

In the more recent "Concrete Semantics" (Section 2.3.2 Definitions), definitions are said to use =, and the following example is given:

``````definition sq :: "nat ⇒ nat" where
"sq n = n ∗ n"
``````

It is furthermore said that abbreviations (Section 2.3.3) should use ≡.

My first idea was that maybe ≡ is a meta-theoretic notion, and behaves to = like ==> behaves to -->. But this is somewhat refuted by the fact that the following works (for a suitable definition of lists etc):

``````lemma "append_list xs [] ≡ xs"
apply (induction xs)
apply (auto)
done
``````

where the ≡ is used within a HOL statement (if I understand correctly). Here, interestingly, after the induction the subgoals are stated using = instead of ≡:

``````goal (2 subgoals):
1. append_list [] [] = []
2. ⋀x1 xs. append_list xs [] = xs ⟹ append_list (x1 # xs) [] = x1 # xs
``````

I would be grateful for any pointers to an explanation of = and ≡.

#### Manuel Eberl (Mar 17 2021 at 19:57):

No, you were right. `≡` is just the meta-logical equivalent of `=`. There is no real reason to use it as an Isabelle ‘user’, much less than using e.g. `⟹` (which does have its uses). This is probably explained somewhere in the Isabelle/Isar reference manual (isar-ref), but as I said, it's not really something you have to know about as a user.

I think the only case in which is might crop up is that the `abbreviation` command insists on a specification with `≡`, not `=` (and will complain otherwise).

#### Manuel Eberl (Mar 17 2021 at 19:59):

Referring to ‘where the ≡ is used within a HOL statement (if I understand correctly)’: where is the HOL statement there? Because no, you cannot write `≡` as a HOL statement, since `≡` returns a `prop` (the type of propositions, which you normally do not see as a HOL user and which you cannot use inside HOL terms).

#### Benedikt Ahrens (Mar 17 2021 at 20:01):

@Manuel Eberl : Thanks a lot for your response. Re using ≡ in HOL statements: I thought my lemma statement above was a HOL statement, since it is in quotes. Am I misunderstanding the quotes then?

#### Manuel Eberl (Mar 17 2021 at 20:02):

The fact that the `≡` becomes a `=` suddenly is probably some quirk of the `induction` method. I think it turns meta-logical connectives into their object-logical ones because that is required to use the induction rule (which is specified in terms of HOL predicates, not meta-logical ones). This mainly concerns `⋀` and `⟹`, but the HOL-ification probably also happens to convert your `≡`.

#### Manuel Eberl (Mar 17 2021 at 20:06):

Benedikt Ahrens said:

Manuel Eberl : Thanks a lot for your response. Re using ≡ in HOL statements: I thought my lemma statement above was a HOL statement, since it is in quotes. Am I misunderstanding the quotes then?

Yes! The quotes distinguish outer syntax from inner syntax. The inner syntax is what you use to specify terms and types. The outer syntax is what you use to interact with the system.

If you take a look at Isabelle/Pure (`~~/src/Pure/Pure.thy`), you will see lots if Isabelle/Pure statements inside quotes as well. In Isabelle/Pure, you have a type `prop` of propositions and some built-in connectives like `⟹`, `⋀`, and `≡`.

HOL then axiomatises a `bool` type that can be converted to `prop` using the function `Trueprop :: bool ⇒ prop`. Whenever you write down a proposition in HOL (i.e. `bool`-valued), Isabelle implicitly wraps a `Trueprop` around it and hides it from you. HOL also has object-level equivalents to all the meta-level equivalents from Pure, and you can convert between the two in both directions as long as the thing you're looking at is of HOL (i.e. not `prop`. You can only reason about `prop` directly in Isabelle/Pure).

#### Manuel Eberl (Mar 17 2021 at 20:07):

Disclaimer: I'm not really an expert on Isabelle/Pure, so some details of what I said might be a bit off. But I'm fairly certain that it's a good enough ‘working knowledge’ for the average Isabelle user.

#### Benedikt Ahrens (Mar 17 2021 at 20:14):

Thanks a lot, that has clarified a lot for me!

Last updated: Aug 13 2022 at 05:18 UTC