Chengsong Tan (Aug 20 2021 at 12:47): 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
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
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
xandy, 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
Chengsong Tan said:
For me an intuitive and naive reason to think that there should
be a method to provelemma 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 thereforetsimilar 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
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.
Thanks again for your helpful advice.
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
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.
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: Dec 21 2024 at 16:20 UTC