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?

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.

You get `tsimilar TONE TZERO ⟹ False`

as one of the cases and that's not provable without another induction.

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

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

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?

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.

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.

You could even define this by recursion instead of an `inductive`

, that might also make things easier.

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
```

But if you can get rid of the symmetry rule in the `inductive`

, I would. It only complicates things.

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.

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
```

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 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
```

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

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.

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.

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`

.

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.

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.

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

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.

Pretty sure it has a limited search depth for `intro`

rules though, so I don't think there should be any infinite loop.

Infinite loops can happen with the simplifier sometimes, but the intro rules of an `inductive`

are not declared as `simp`

rules.

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

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?

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

Chengsong Tan has marked this topic as resolved.

Last updated: Jun 20 2024 at 12:31 UTC