Re: [isabelle] I need a meta-or



On 7/29/2013 3:23 PM, Makarius wrote:
If there's a &&&, then it seems there should be the complete suite of basic meta operators

In principle you could define all the standard connectives of Isabelle/HOL in Isabelle/Pure as well, but what is the point?

Makarius,

For myself, the point has become more general. Having meta-connectives would now be a result of being able to define functions using "prop", such as "prop => prop", "prop => prop => prop", etc., and have the functions coexist nicely with Trueprop coercion just like meta-implication does, that is, not having to annotate the variables with PROP, and Trueprop not trying to coerce when it's not supposed to.

For me, the general point is to do formalizations about other logics within HOL, and be able to keep those formalizations respectably separate from the object-logic functions, definitions, axioms, etc., until I intentionally want to mix the (mostly) meta-logic with the object-logic.

I don't know that it has to be about formalizing other logics. If you had an Isar definition and Isar abbreviation command that allowed a person to define functions using prop, and the functions behaved nicely like ==>, then people would find a use for those commands.

I now have the perfect function to make my point, which is not the meta-or I asked for at first. The meta-or I initially wanted sort of fell under the "what is the point" category. Meta-or is "(!!R. (P ==> R) ==> (Q ==> R) ==> R)", so to make it practical to use, you would have to start defining a bunch of simp rules, and then you'd end up asking, "And why exactly am I duplicating all the simp rules that have been created for \<or>?"

My function now is, "((P ==> False) ==> Q)", which requires absolutely nothing additional to use. If I want to go total meta (other than bool variables), then I can replace False with "(!!P Q. P == Q::bool)", which would only require a simp rule to convert the meta-False back to False, since meta-False by itself can make simplification slower.

The purpose of Isabelle/Pure is to provide a framework for higher-order natural deduction, with declarative rule structure indicated by the connectives !! and ==> (i.e. Minimal Higher-order Logic). Anything beyond that is not really pure.

You're the authority, but my inclination is to say that a logic is defined by its axioms, so I'm inclined to say that any logic that is derived using only Pure is Pure. Even with a little bit of corruption, like having to use bool variables, I'd say it can be considered Pure, practically speaking. I'm just a novice here speaking.

You talk about Isabelle/Pure as a framework, but I don't see the problem with taking the framework to its limits, though there would have to be Isar commands to facilitate that, or ML templates that can be used to define "prop" based functions that behave like ==>.

My interest in this evolved due to sequents. The LHS of a sequent is a conjunction, which matches the use of ==> perfectly. The RHS of a sequent is a disjunction, so for the RHS, ==> by itself ceases to work.

I created some notation to sync up the turnstile with ==>, and I used \<or> to duplicate the RHS properties of the sequent.

I then plugged in a sequent derivation proof from Wikipedia with my notation. It happened to be that the second line of the proof and the conclusion of the proof were the same, because of the \<or>. Very uninspiring. A "what's the point" moment.

If there's a mistake, it's that you make it too easy to use ==>. If I know that ==> is of type (prop => prop => prop), and I can do:

   theorem "A ==> (B ==> C)"

It's only natural that I think I should be able to do:

   abbreviation imp2 :: "prop => prop => prop" (infixr "=+>" 15) where
      "imp2 P Q == (P ==> Q)"

   theorem "A =+> (B =+> C)"

But it doesn't work. I can finagle things to make it work, but it'll never work like that.

The good news is that my finagling led to something that's acceptable (with Lars' prior help).

I think there are lots of tangents to go off on for why a person might want to intentionally stay within the meta-logic. Part of it is catching the "meta-logic spirit". What other proof assistant has a meta-logic that a person can use?

Part of it is trying to figure out what in Isabelle/HOL is optimized for the meta-logic, and what's optimized for the object-logic. Overusing the meta-logic should at least teach me how to use the meta-logic, and formalizing something differently can sometimes help a person do old things better.

I do this:

   theorem "(A ==> False) ==> (~A)"
   using[[simp_trace]]
   apply(auto simp only:)
   done

The simp trace shows this:

   [1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
   (A ==> False) ==> ~A
   [1]Adding rewrite rule "??.unknown":
   A == True

I didn't give it any simp rules about True and False, but it knows how to use them. That tells me the simplifier is optimized for the object-logic, that and 15ms more for a proof if I use meta-False.

Consequently, I decide I should use "((P ==> False) ==> Q)" instead of "((P ==> (!!P Q. P == Q::bool)) ==> Q)", because in this case, the performance price for staying pure is probably too high, and False is not too much to accept. It's some lambda calculus and the HOL refl axiom.

I know that the logic engine really likes statements like "P ==> Q", so I'm trying to go through the exercise of seeing to what extent I can stay in the "==>" world. I don't think the logic engine is fond of things like "(!!R. (P ==> R) ==> (Q ==> R) ==> R)", but I'm pretty sure that it doesn't consider "((P ==> False) ==> Q)" to be much more of a burden than "P ==> Q". In fact, I think the logic engine loves "((P ==> False) ==> Q)", because it's easy, and different.

In a more perfect world, my function "((P ==> False) ==> Q)" would be of type "prop => prop => prop". It's okay that it's not. I'm happy to have found something that's simple, and that fits in the "==>" paradigm.

After your email I put a little more effort into creating the meta-versions of the standard connectives. I was trying to cut and paste from the HOL versions, but the HOL versions use lambda calculus, which wasn't working for me. Then I came up with the version for meta-False, which gave me meta-not, and then I cut and pasted for the meta-exists.

If the performance cost is too high to stay pure, then I don't want to use the meta-connectives. But my perfect example, "((P ==> False) ==> Q)", which I've used to make my point, is not a standard connective. It's also fast, and I need it, and I want it. I have it, too. Just not in a one-operator form.

Regards,
GB

notation ==> (infixr "|-" 4)

abbreviation mFalse :: "prop" ("mFalse") where
  "mFalse == (!!P Q. P == Q::bool)"

abbreviation (input) seqr :: "bool => bool => prop" (infixr "||" 9) where
  "seqr P Q == ((P ==> mFalse) ==> Q)"

abbreviation (input) seql :: "bool => prop => prop" (infixr "|||" 9) where
  "seql P Q == ((P ==> mFalse) ==> PROP Q)"

theorem mF_EQ_False:
  "mFalse == (Trueprop False)"
by(rule equal_intr_rule, metis, presburger)

(*3ms with False in abbreviation.
  18ms with meta-False used in abbreviation and no mF_EQ_False simp rule.
  3ms with meta-False used in abbreviation and simp rule mF_EQ_False.*)
theorem
  "   (A |- (~E ==> ~C ==> ~D ==> B))
  ==> (A |- (E ||| B ||| C || D))"
apply(auto simp only: mF_EQ_False)
done

theorem meta_not_EQ_not:
  "(P ==> (!!P Q. P == Q::bool)) == (Trueprop (~P))"
apply(simp only: mF_EQ_False not_def)
apply(rule equal_intr_rule)
by(auto)

theorem meta_exists_EQ_exists:
  "(!!Q. (!!x. P x ==> Q) ==> Q) == (Trueprop (? x. P x))"
apply(rule equal_intr_rule)
by(auto simp only:)




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