Email Gateway (Aug 19 2022 at 07:54): Email Gateway (Aug 19 2022 at 07:54):From: John Munroe <munddr@gmail.com>
Hi,
I'm trying to prove a lemma containing a uniqueness quantification:
axiomatization
p1 :: "nat => bool" and
p2 :: "nat => bool" and
p3 :: "nat => bool"
where
ax1: "p1 x == ~p2 x & ~p3 x" and
ax2: "p2 x == ~p1 x & ~p3 x" and
ax3: "p3 x == ~p1 x & ~p2 x"
lemma lem: "EX! p:{p1,p2,p3}. p q"
using ax1 ax2 ax3
apply auto
but unfortunately no proof is found. Don't ax1, ax2 and ax3 together
imply that for all values, there's one and only one predicate that is
true?
I must be missing something here...
Thanks a lot for your time.
John
Email Gateway (Aug 19 2022 at 07:54):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
I can prove your lemma a bit like this:
axiomatization
p1 :: "nat => bool" and
p2 :: "nat => bool" and
p3 :: "nat => bool"
where
ax1: "p1 x == ~p2 x & ~p3 x" and
ax2: "p2 x == ~p1 x & ~p3 x" and
ax3: "p3 x == ~p1 x & ~p2 x"
lemma lem: "EX! p:{p1,p2,p3}. p q"
apply simp
apply (simp add: conj_disj_distribR cong: conj_cong)
apply (metis ax1 ax2 ax3)
done
Let me say a little about how I knew to do that.
Firstly, introducing ax1 ax2 or ax3 as assumptions will loop the
simplifier. It will take them as rewrite rules and apply them to each
other, and they're directed towards their complex ends. I could
introduce them safely the other way around, e.g.
lemma lem: "EX! p:{p1,p2,p3}. p q"
using ax1[symmetric] ax2[symmetric] ax3[symmetric]
apply simp
apply (simp add: conj_disj_distribR cong: conj_cong)
apply metis
done
The syntax "EX! p: S. P p" is an abbreviation for "EX! p. p : S --> P
p". The first simp statement reveals this by reducing "p : {p1, p2, p3}"
to "p = p1 | p = p2 | p = p3". If you are using an old enough version of
Isabelle, the syntax comes with a constant Bex1, which should be
unfolded in the first line with (simp add Bex1_def) to get to the same
state.
Secondly, I wanted to avoid the (very general) application "p q" in your
term where "p" is a quantified variable (an intrinsically higher-order
expression). If we move this statement together with the three different
equalities, and supply the "conj_cong" congruence rule (which allows the
left-hand side of conjunctions to be used to rewrite their right hand
sides in the simplifier) then the applications are of the three specific
predicates p1 p2 and p3. The equalities are still higher-order, but for
some reason metis can solve the problem already (mirabile dictu).
The quantifiers can be removed more completely with "apply (simp add:
conj_disj_distribR Ex1_def all_conj_distrib ex_disj_distrib)", from
which point it is even more clear that metis should be able to solve the
problem. Maybe.
Yours,
Thomas.
Email Gateway (Aug 19 2022 at 07:56):From: John Munroe <munddr@gmail.com>
Hi Thomas,
Thanks so much for your detailed explanation.
I've tried your suggestion and it works! However, I've tried extending
the model to 5 predicates:
axiomatization
p1 :: "nat => bool" and
p2 :: "nat => bool" and
p3 :: "nat => bool" and
p4 :: "nat => bool" and
p5 :: "nat => bool"
where
ax1: "p1 x == ~p2 x & ~p3 x & ~p4 x & ~p5 x" and
ax2: "p2 x == ~p1 x & ~p3 x & ~p4 x & ~p5 x" and
ax3: "p3 x == ~p1 x & ~p2 x & ~p4 x & ~p5 x" and
ax4: "p4 x == ~p1 x & ~p2 x & ~p3 x & ~p5 x" and
ax5: "p5 x == ~p1 x & ~p2 x & ~p3 x & ~p4 x"
and
metis loops at:
lemma lem: "EX! p:{p1,p2,p3,p4,p5}. p q"
using ax1[symmetric] ax2[symmetric] ax3[symmetric] ax4[symmetric]
ax5[symmetric]
apply simp
apply (simp add: conj_disj_distribR Ex1_def all_conj_distrib ex_disj_distrib)
apply metis
Do you know why it's fine for a smaller number of predicates, e.g., 3,
but not when there are 5? Do you happen to know how to simplify the
goal further?
Thanks a lot for your time.
John
Email Gateway (Aug 19 2022 at 07:57):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
I fiddled around with it a bit, and discovered that applying clarsimp
before metis may solve the problem.
I have no idea why this might be. I tried case decomposition but all I
discovered was that some combination of disjCI and conjE, which
clarsimp/clarify apply, was helping metis. It makes no sense to me that
(elim conjE, metis) can solve some problems which metis can't, but it
seems to be the case.
I suppose I should ask the obvious: these equalities on predicates seem
a bit strange. The "p1 = p2" possibilities all over the place are
complicating things. Do you want the property "p q" to hold for exactly
one of the 5 expressions p1, p2, ... or for exactly one of the
values, of which there might be less than 5? Note that "EX! p : {p1,
p2, p3, p4, p5}. p q" would be true if "p1 q" and "p2 q" but "p1 = p2"
(although that's impossible in this case).
Here is a slightly stronger formulation which can be solved by auto:
lemmas axs = ax1 ax2 ax3 ax4 ax5
lemma lem: "length (filter (%p. p q) [p1, p2, p3, p4, p5]) = 1"
using axs[symmetric]
by auto
This helper rule might also be helpful:
lemma ex_unique_from_length:
"length (filter P xs) = 1 ==> (EX! x : set xs. P x)"
apply (induct xs)
apply (auto simp add: filter_empty_conv split: split_if_asm)
done
lemmas lem2 = ex_unique_from_length[OF lem, unfolded set.simps]
Yours,
Thomas.
Email Gateway (Aug 19 2022 at 07:58):From: John Munroe <munddr@gmail.com>
Thanks again for your help.
I suppose I should ask the obvious: these equalities on predicates seem a
bit strange. The "p1 = p2" possibilities all over the place are complicating
things. Do you want the property "p q" to hold for exactly one of the 5
expressions p1, p2, ... or for exactly one of the values, of which there
might be less than 5? Note that "EX! p : {p1, p2, p3, p4, p5}. p q" would be
true if "p1 q" and "p2 q" but "p1 = p2" (although that's impossible in this
case).
I indeed want "p q" to hold for exactly one of the 5 expressions, i.e.
only one of the 5 predicates returns true for all arguments.
Applying clarify/clarsimp seems to work indeed. However, if I change
the type of the predicates from "nat => bool" to "(nat*nat) => bool",
the proof breaks. Do you know why the input type of the predicates
affects the proof?
Here is a slightly stronger formulation which can be solved by auto:
lemmas axs = ax1 ax2 ax3 ax4 ax5
lemma lem: "length (filter (%p. p q) [p1, p2, p3, p4, p5]) = 1"
using axs[symmetric]
by autoThis helper rule might also be helpful:
lemma ex_unique_from_length:
"length (filter P xs) = 1 ==> (EX! x : set xs. P x)"
Right, but how come the reverse doesn't hold? If there's exactly one
of the predicates returning true, then isn't the length of the
filtered list one?
Thanks again.
John
Email Gateway (Aug 19 2022 at 07:58):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
I indeed want "p q" to hold for exactly one of the 5 expressions, i.e.
only one of the 5 predicates returns true for all arguments.Applying clarify/clarsimp seems to work indeed. However, if I change
the type of the predicates from "nat => bool" to "(nat*nat) => bool",
the proof breaks. Do you know why the input type of the predicates
affects the proof?
No particularly good ideas here, except that things are becoming more
complicated.
Right, but how come the reverse doesn't hold? If there's exactly one
of the predicates returning true, then isn't the length of the
filtered list one?
No. To phrase what I said before in different language again, the
cardinality of the set you've been talking about "{p1, p2, p3, p4, p5}"
isn't necessarily 5. If "p1 = p2" then there are less than 5 unique
elements of the set "{p1, p2, p3, p4, p5}".
To rephrase this once more: if you add a p6 to your axiomatization with
the axiom ax6: "p6 = p5", then the equivalent lemma is still provable:
lemma lem: "EX! p:{p1,p2,p3,p4,p5, p6}. p q"
apply (simp add: conj_disj_distribR Ex1_def all_conj_distrib
ex_disj_distrib)
apply clarsimp
apply (metis axs)
done
The reason this is provable is because "{p1, p2, p3, p4, p5, p6} = {p1,
p2, p3, p4, p5}", so it's really just the same as the 5 example.
Yours,
Thomas.
Email Gateway (Aug 19 2022 at 07:59):From: Tjark Weber <webertj@in.tum.de>
No. Try
lemma length_from_ex_unique:
"(EX! x : set xs. P x) ==> length (filter P xs) = 1"
nitpick
Best regards,
Tjark
Last updated: Nov 21 2024 at 12:39 UTC