On 29 Mar 2012, at 17:52, Phil Clayton wrote: >> On 29 Mar 2012, at 15:02, Phil Clayton wrote: >> >>>>> ... >>>>> 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
I tried this and it seems to give too many false positives - there is no harm in the above if the Qi are equations, and X is a set that will be automatically proved equal to the universe of its type. In that case, the unnecessary quantification over x makes no difference when the theorem is used as a rewrite rule and often makes the theorem easier to read (e.g., see z_minus_thm). As I can't think of a good general solution, I may just implement a hook so you can add in your own checks to the ones that always make sense. (In cases like the above, it is easy to write something that will detect the cases of interest, without having to handle the "general case"). Regards, Rob.
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
