[ProofPower] Theorem QA

[Phil Clayton]

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