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.
Regards,
Rob.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
