## Stream: Beginner Questions

### Topic: ✔ symmetric rule in inductively defined predicates

#### Chengsong Tan (Aug 20 2021 at 12:47):

It seems that symmetric rule in inductively defined predicates causes difficulty for proving
certain arguments make it evaluate to False.
If we define an inductive datatype called `tfoo`:
```datatype tfoo = TZERO | TONE | TSEQ tfoo tfoo ```
Then we can define an inductive predicate that
determines whether two terms of the type `tfoo`
are "similar":

``````inductive tsimilar :: "tfoo ⇒ tfoo ⇒ bool"
where
"tsimilar TZERO TZERO"
(*|  "tsimilar t1 t2 ⟹ tsimilar t2 t1"*)
| "tsimilar TONE TONE"
| "⟦tsimilar t1 t2; tsimilar t3 t4 ⟧ ⟹ tsimilar (TSEQ t1 t3) (TSEQ t2 t4)"
``````

And showing that two concrete instances of type `tfoo`
are not similar is quite straightforward:

``````lemma notsimilar : assumes "tsimilar TZERO TONE"
shows "False"
using assms
apply(erule_tac tsimilar.cases)
apply simp
apply simp
by fastforce
``````

The problem arises once you add (uncomment)
the symmetric rule:
``` "tsimilar t1 t2 ⟹ tsimilar t2 t1" ```
This causes automation to fail.
The reason why is probably because sledgehammer/....
tries to apply the symmetric rule back and forth, creating
an infinite loop.
Apparently` tsimilar TZERO TONE` should
always evaluate to false, as the inductive definition
defines the minimal set closed under the rules,
so how can we make this obvious again to Isabelle?

#### Manuel Eberl (Aug 20 2021 at 12:52):

I think the real problem here is that when you add that new rule, your statement is simply not strong enough to be provable by direct induction.

#### Manuel Eberl (Aug 20 2021 at 12:53):

You get `tsimilar TONE TZERO ⟹ False` as one of the cases and that's not provable without another induction.

#### Manuel Eberl (Aug 20 2021 at 12:55):

The obvious solution is to just prove something stronger, e.g.:

``````lemma "tsimilar x y ⟹ x = y"
by (induction rule: tsimilar.induct) auto
``````

#### Chengsong Tan (Aug 20 2021 at 13:56):

Manuel Eberl said:

I think the real problem here is that when you add that new rule, your statement is simply not strong enough to be provable by direct induction.

Thank you!
How about when the relation is slightly more complicated that this lemma
doesn't hold?

``````lemma "tsimilar x y ⟹ x = y"
``````

If I change the relation to include those
that are slightly different:

``````datatype tfoo = TZERO | TONE nat | TSEQ tfoo tfoo

inductive tsimilar :: "tfoo ⇒ tfoo ⇒ bool"
where
"tsimilar TZERO TZERO"
|  "tsimilar t1 t2 ⟹ tsimilar t2 t1"
| "tsimilar (TONE i)  (TONE j)"
| "⟦tsimilar t1 t2; tsimilar t3 t4 ⟧ ⟹ tsimilar (TSEQ t1 t3) (TSEQ t2 t4)"

lemma notsimilar : assumes "tsimilar TZERO (TONE i)"
``````

Then how can I prove the lemma notsimilar?

#### Chengsong Tan (Aug 20 2021 at 13:59):

The reason I came up with this question was that
I defined a predicate where two instances which are
semantically equal but syntactically different
are deemed similar. It would be nice
to be able to prove certain instances of them
are not similar because there is no induction rule
to derive the similarity.

#### Manuel Eberl (Aug 20 2021 at 14:03):

Well, first of all, your `tsimilar` would be symmetric even without that additional explicit symmetry rule. So I suggest removing it to make things easier, and then prove it from the remaining ones by induction.

#### Manuel Eberl (Aug 20 2021 at 14:04):

You could even define this by recursion instead of an `inductive`, that might also make things easier.

#### Manuel Eberl (Aug 20 2021 at 14:06):

Otherwise, I guess you will have to strengthen your goal in such a way that it survives the induction, i.e. in particular in a way that makes it symmetric in `x` and `y`, e.g.:

``````lemma notsimilar:
assumes "tsimilar x y" "∃c. x = TZERO ∧ y = TONE c ∨ x = TONE c ∧ y = TZERO"
shows False
using assms by (induction rule: tsimilar.induct) auto
``````

#### Manuel Eberl (Aug 20 2021 at 14:07):

But if you can get rid of the symmetry rule in the `inductive`, I would. It only complicates things.

#### Chengsong Tan (Aug 20 2021 at 14:31):

Manuel Eberl said:

Otherwise, I guess you will have to strengthen your goal in such a way that it survives the induction, i.e. in particular in a way that makes it symmetric in `x` and `y`, e.g.:

``````lemma notsimilar:
assumes "tsimilar x y" "∃c. x = TZERO ∧ y = TONE c ∨ x = TONE c ∧ y = TZERO"
shows False
using assms by (induction rule: tsimilar.induct) auto
``````

Thanks a lot!
How do you come up with such strengthening methods (is it
more on an ad-hoc basis or is there a general rule of thumb), and
can you elaborate a bit more about
what do you mean by "survive the induction" (for example a
formal definition)?

For me an intuitive and naive reason to think that there should
be a method to prove

``````lemma notsimilar : assumes "tsimilar TZERO (TONE i)"
``````

is that we know that from rules like these

``````  "tsimilar TZERO TZERO"
``````

you can never derive a similarity between instances
that breaks the "hierarchy", and therefore

``````tsimilar TZERO (TONE i)
tsimilar TZERO (TSEQ t1 t2)
tsimilar (TONE i) (TSEQ t1 t2)
``````

are always false.

#### Chengsong Tan (Aug 20 2021 at 14:32):

From your example I came up with another strengthening
lemma that is like the below:

``````lemma hierachy_maintained:
assumes "tsimilar x y" "∃c t1 t2.
x = TZERO ∧ y = TONE c ∨ x = TONE c ∧ y = TZERO
∨  x = TONE c ∧ y = TSEQ t1 t2 ∨  x = TSEQ t1 t2 ∧ y = TONE c
∨  x = TZERO ∧ y = TSEQ t1 t2 ∨  x = TSEQ t1 t2 ∧ y = TZERO"
shows False
using assms
apply(induction rule: tsimilar.induct)
apply fastforce
apply fastforce
apply fastforce
apply fastforce
done
``````

#### Manuel Eberl (Aug 20 2021 at 14:38):

Chengsong Tan said:

For me an intuitive and naive reason to think that there should
be a method to prove

``````lemma notsimilar : assumes "tsimilar TZERO (TONE i)"
``````

is that we know that from rules like these

``````  "tsimilar TZERO TZERO"
``````

you can never derive a similarity between instances
that breaks the "hierarchy", and therefore

``````tsimilar TZERO (TONE i)
tsimilar TZERO (TSEQ t1 t2)
tsimilar (TONE i) (TSEQ t1 t2)
``````

are always false.

Yeah but the problem is that due to your symmetry rule, you could also have `tsimilar TZERO (TONE x)` from `tsimilar (TONE x) TZERO`, so if you do try to disprove it, you have to disprove both of them simultaneously.

#### Chengsong Tan (Aug 20 2021 at 14:38):

Chengsong Tan said:

From your example I came up with another strengthening
lemma that is like the below:

``````lemma hierachy_maintained:
assumes "tsimilar x y" "∃c t1 t2.
x = TZERO ∧ y = TONE c ∨ x = TONE c ∧ y = TZERO
∨  x = TONE c ∧ y = TSEQ t1 t2 ∨  x = TSEQ t1 t2 ∧ y = TONE c
∨  x = TZERO ∧ y = TSEQ t1 t2 ∨  x = TSEQ t1 t2 ∧ y = TZERO"
shows False
using assms
apply(induction rule: tsimilar.induct)
apply fastforce
apply fastforce
apply fastforce
apply fastforce
done
``````

For me the summary of doing a strengthening of a lemma about inductive definitions,
is to

``````1. add existential quantifiers rather than using free variables
2. try to prove/disprove together a bunch of things if they are interderivable
``````

#### Manuel Eberl (Aug 20 2021 at 14:38):

I don't think there's any general method for finding out how to generalise things sufficiently. It's just intuition and experience.

#### Manuel Eberl (Aug 20 2021 at 14:39):

By "survive the induction" I mean that your statement must be strong enough so that you can actually apply the induction hypothesis in the induction step.

#### Manuel Eberl (Aug 20 2021 at 14:41):

A classic example is the tail-recursive list reversal function:

``````fun itrev :: "'a list ⇒ 'a list ⇒ 'a list" where
"itrev acc [] = acc"
| "itrev acc (x # xs) = itrev (x # acc) xs"
``````

If you try to prove `itrev [] xs = rev xs` by induction directly, you will run into a problem in the induction step because your induction hypothesis will tell you that `itrev [] xs = rev xs` (i.e. where `acc = []`), but in the induction step, you will have `acc = [x]` so you cannot apply the induction hypothesis.

#### Manuel Eberl (Aug 20 2021 at 14:42):

The trick is then to try to generalise the `[]` and prove something about `itrev acc xs` in general, namely `itrev acc xs = rev xs @ acc`.

#### Manuel Eberl (Aug 20 2021 at 14:43):

But, let me stress again, in the above case, the real solution is to remove the symmetry rule. You don't need it, and it just makes the proofs harder.

#### Chengsong Tan (Aug 20 2021 at 14:48):

Manuel Eberl said:

But, let me stress again, in the above case, the real solution is to remove the symmetry rule. You don't need it, and it just makes the proofs harder.

Of course this example is contrived, but I feel like
in more complicated cases where you can't get
rid of a rule that tricks Isabelle into loops the technique shown
here can be really useful.

#### Manuel Eberl (Aug 20 2021 at 14:52):

I still don't see where Isabelle "looped" here.

#### Chengsong Tan (Aug 20 2021 at 15:03):

Manuel Eberl said:

I still don't see where Isabelle "looped" here.

The automatic prover tries to
say that there is no rule leading to the term

``````tsimilar TZERO (TONE i)
``````

(which we abbreviate as `t`)
being true

by finding out
that

``````tsimilar TZERO TZERO
``````

can't lead to the `t`,
and

``````tsimilar (TONE i) (TONE j)
``````

can't lead to `t`,
and .......... so forth
Until it finds the rule

``````tsimilar t1 t2 ==> tsimilar t2 t1
``````

it says umm, if we unify t1 with
TONE i and t2 with TZERO,
then the fact `t'`

``````tsimilar t1 t2
``````

``````tsimilar TZERO (TONE i)
``````

How to get `t'`?
Well by rule

``````tsimilar t1 t2 ==> tsimilar t2 t1
``````

again, which requires `t''`,
which requires `t'''`,
..............
that's where the loop (I think) happens.
Is there a misunderstanding here?

Since the inductive definition means the minimal set that
is closed under the rules, if the prover checked all rules
and found out that none can lead to the desired relation of instances,
it proved the fact that `P x1.... xn` is false. In our example here it got stuck in the last rule,
not being able to disprove possibility of deriving the result.

#### Manuel Eberl (Aug 20 2021 at 15:05):

Pretty sure it has a limited search depth for `intro` rules though, so I don't think there should be any infinite loop.

#### Manuel Eberl (Aug 20 2021 at 15:05):

Infinite loops can happen with the simplifier sometimes, but the intro rules of an `inductive` are not declared as `simp` rules.

#### Manuel Eberl (Aug 20 2021 at 15:06):

I don't think I saw any looping behaviour when I tried your example before either.

#### Chengsong Tan (Aug 20 2021 at 15:08):

Manuel Eberl said:

I don't think I saw any looping behaviour when I tried your example before either.

Ah my bad, shouldn't use the terminology loop, but just stuck and gave up?

#### Manuel Eberl (Aug 20 2021 at 15:13):

Sure, yes, at some point most methods will just give up.

#### Notification Bot (Aug 20 2021 at 15:59):

Chengsong Tan has marked this topic as resolved.

Last updated: Sep 25 2022 at 23:25 UTC