Re: [isabelle] Uniqueness quantification



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.

On 26/07/12 22:39, John Munroe wrote:
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

On Thu, Jul 26, 2012 at 3:26 AM, Thomas Sewell
<Thomas.Sewell at nicta.com.au>  wrote:
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.


On 26/07/12 00:20, John Munroe wrote:
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








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.