On 29/03/12 16:59, Rob Arthan wrote:

On 29 Mar 2012, at 15:02, Phil Clayton wrote:

On 27/03/12 08:36, Rob Arthan wrote:

On 25 Mar 2012, at 12:31, Phil Clayton wrote:

On 24/03/12 09:32, Rob Arthan wrote:
The scripts for the ProofPower mathematical case studies have a
little tool called "check_thms" which does a quality assurance
check on the the theorems in a theory. It checks against:

a) Theorems with free variables. Typically this means you forgot an
outer universal quantifier. Later on you will be puzzled when tools
like the rewriting tools think you don't want the free variables to
be instantiated.

b) Theorems with variables bound by logical quantifiers (universal,
existential and unique existential) that are not used in the body
of the abstraction. This happens for various reasons (often hand in
hand with (a)). It is misleading for the reader and can be
confusing when you try to use the theorem.

It outputs a little report on any problems it finds.

I am considering putting a bug-fixed and documented version of
check_thms in the next working release of ProofPower. Any comments
or suggestions for other things to check for would be welcome.

I am wondering about a stronger version of check b for individual
conjuncts of a theorem. In the past, I have found that e.g.
rewriting can be awkward when an equational conjunct of a theorem
does not mention a universally quantified variable (that is
mentioned by other conjuncts). I think the issue was when the
unmentioned variable was quantified over a non-maximal set, so this
is probably most relevant to Z. For example, given

│ _ ^ _ : ℤ × ℕ → ℤ
├──────
│ ∀ i : ℤ; j : ℕ ⦁ i ^ 0 = 1 ∧ i ^ (j + 1) = i * i ^ j

I think rewriting with the base case requires manual intervention to
provide a value for j,

Indeed. ∀ i : ℤ; j : X ⦁ i ^ 0 = 1 amounts to a convoluted way of
saying "either X is empty or ∀ i : ℤ ^ 0 = 1".

so the following would be preferable:

├──────
│ ∀ i : ℤ ⦁ i ^ 0 = 1 ∧ (∀ j : ℕ ⦁ i ^ (j + 1) = i * i ^ j)


I expect that this sort of check would be dependent on the current
proof context (perhaps making use of canonicalization support) so
may not be desirable as part of the same utility.

I think a simple heuristic would work. I think is reasonable to say
that in a predicate of the form:

∀ ... x : X | P ⦁ Q1 ∧ Q2 ∧ ...

If there is an i such that x doesn't appear free in P or Qi, then
report a possible problem. There are many cases (e.g., law of
transivity) where a theorem has an implication with an antecedent
that contains variables that are not in the succedent, but it is a
reasonable style rule in Z not to disguise such an implication by
burying the antecedent in an implication.

That sounds reasonable to me.

There is also the possibility of a schema declaration in the
quantification which presents various options. For e.g. a schema
reference:

∀ S; ... | P ⦁ Q1 ∧ Q2 ∧ ...

would it make sense for the heuristic warn if there is an i such that
frees(P) ∪ frees (Qi) does not mention any variable bound by S?

Yes that makes sense.

Also, for a horizontal schema declaration, there is the question of
whether to destruct it, i.e. expand out its contents, or treat it like
any other schema.

Do you mean a declaration in a quantifier of the form [Declaration |
Predicate]?

Yes.


Do you use that idiom much?

No. (Although I am generating Z systematically which can result in a horizontal schema, I can't foresee any need to quantify such a horizontal schema in a theorem.)


I can't see the point, so I don't have any views on how to handle it.

I don't have any views either but thought I would mention it in case anyone did.

Regards,

Phil

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to