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]? Do you use that idiom much? I can't see the point, so I don't have
any views on how to handle it.
Regards,
Rob.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
