Stream: Beginner Questions

Topic: symmetric rule in inductively defined predicates


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

Thanks again for your helpful advice.

view this post on Zulip Manuel Eberl (Aug 20 2021 at 14:52):

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

view this post on Zulip 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

leads to

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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (Aug 20 2021 at 15:06):

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

view this post on Zulip 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?

view this post on Zulip Manuel Eberl (Aug 20 2021 at 15:13):

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


Last updated: Jul 15 2022 at 23:21 UTC