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.

>> This is currently just for HOL, but I could do something similar for Z too.
> Certainly this would be a useful facility for HOL users but I could only make 
> use of a Z version.
> Regards,
> Phil
> P.S.  The above formal text is UTF8 encoded!  Hopefully that is not a problem 
> these days.  It would be useful to know if any mail systems aren't displaying 
> it properly.

It looks good to me.  I must get round to some more work on Unicode and UTF-8 
for ProofPower.

Thanks for the input.



Proofpower mailing list

Reply via email to