On Mon, Nov 4, 2019 at 3:22 PM Giovanni Mascellani <[email protected]> wrote:
> [DAW, sorry for double sending, this is meant for the mailing list] > > Il 04/11/19 18:52, David A. Wheeler ha scritto: > > There's no way to know for certain without trying, but I expect that > > an automated tool could simplify a number of these expressions. The > > result might be a smaller monster. > > Looking quickly at the proof, it seems that a substantial amount of > steps apply either mergeconj or selconj. The first is used to merge > together two lists of conjuncts in the antecedent of a ND clause, and > the second to select one of the conjuncts in the antecedent of a ND > clause. Currently the Metamath proof synthesisation algorithm is forced > to represent ND clauses invariably in this form: > > ( ( ph /\ ( ps /\ ( ch /\ T. ) ) ) -> th ) > > although in line of principle much more freedom could be use to > represent the antecedent. When to lists are merged they won't be in this > form, so mergeconj has to be repeatedly called to fix it. Also, ND > manipulation lemmata, which are called by the proof generated by my > code, expect conjuncts to be removed from the antecedent to appear in > the first (outermost) place(s). Therefore repeated application of > selconj is required to fix the shape of the antecedent before applying > some ND steps. > > Probably many such calls could be saved by allowing more freedom in how > the antecedent is represented. mergeconj could be dropped altogether and > fewer selconj applications might be required if the antecedent is > shallower. Unfortunately, this means complicating the code, because the > conjunct selection process needs to accept any tree of conjuncts instead > of a rigid right-associated list. > > Alternatively I could try to follow the idea of Mario's style for ND. In > that case selecting conjuncts becomes free, because selecting hypotheses > in Metamath is already free. The problem I see is that some ND steps, > like ex (implication introduction) require a reified inference operator > (i.e., an implication), that is not available with Mario's style. It is > available with mine, though, which is the reason I am using it. > Maybe you could bring me up to speed on the details here, but as I see it, implication introduction is 'ex'. It is important for this that conjuncts be stored as a *left* associated list, possibly beginning with a T. if that makes things easier. Whenever you change the context, there is a cost associated with pulling any lemmas into the new context (including hypotheses) via adantr; you can either compute these lazily or precompute them and drop any that you don't end up needing. If you are finding subproofs in the manner of a tableau calculus (working backwards from the goal), this will not be a problem, but if you are reasoning forward and taking context unions all the time, one inefficiency that you can end up with is that a subproof Gamma |- ph is derived, and then it is used to prove two other subproofs Delta1 |- ps and Delta2 |- ch, where Delta1 and Delta2 are incomparable strict supersets of Gamma. In this case, if you turn it into an ND proof, you will end up replaying the steps Delta1 |- ph and Delta2 |- ph, and some sharing is lost. I don't know how problematic this is, but if you look for shared subproofs you can in principle determine that Gamma |- ph is shared, and so prove Gamma |- ph directly and then do a context change (syl*anc) step to get to Delta1 |- ph and Delta2 |- ph. Another frequently used lemma is csbcom2fi, which applies an explicit > substitution to another one. Substitutions are frequently used in ND > proofs, for example in quantifier introduction and elimination. Also, > when I convert a FOF predicate or functor to Metamath, I represent it > using one substitution for each of its arguments. For example, ph(x, y) > is represented as > > [. x / w ]. [. y / z ]. ph > > where w and z are two fresh variables chosen for ph. While this is an option, I think it would be much simpler in a set.mm based system to use x R y for representing binary relations without additional variables getting in the way. In a real FOL system, you would have a sort for terms and a constant for each primitive relation; set.mm only has the e. relation but you can use that as a prototypical relation on set.mm foundations. Using wff variables has the disadvantage that the binding variables become explicit, which complicates proofs with lots of unnecessary NF stuff. (Actually it doesn't need to, because you should be assuming that w and z are disjoint from everything other than ph.) > Furthermore, I > assume that w and z are the only free variables in ph. A similar thing > happens for functors, where in addition I also assume that it can be > proved that they are sets. > I formalize this requirement in MM0: it is not that w and z are the only free variables in ph, but rather that any free variables other than w and z are not mentioned anywhere in the theorem or proof (they are "parameters" to ph). In metamath that means putting a $d between w , z and all variables in the statement. > This is necessary because there is mismatch between Metamath and > standard FOFs: in FOFs arguments are explicit and order-based, while in > Metamath they are implicit and name-based. As a result, it is not easy > in Metamath to distinguish the two FOFs ph(x,y) and ph(y,x), and even > less ph(x,y) and ph(A(y),y), unless one resorts to the trick I am using. > If we stipulate that the arguments to ph are internally called w and z > and the argument to A is internally called u, then we can write: > > [. y / w ]. [. x / z ]. ph > [. [_ y / u ]_ A / w ]. [. y / z ]. ph > > and everything is fine, except for the readability of the notation and > the fact that we have to commute a lot of explicit substitutions. > Yes, I dealt with the same problem in peano.mm0. Originally I just had wffs and variables, but without a "class" like type it quickly becomes difficult to deal with all the "deferred binding" variables involved in relations. If you are okay with an axiomatic term constructor, you can just declare P(x,y), but if you want P to be a metavariable you need a sort for it. (Things become even more complicated if you want a sort for n-ary predicates but the universe of discourse doesn't support pairing...) Mario -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSu0ObTt0D9dQte%2BpO0Z%2BQHq9_pzuDvBQOxspQucAkQg5w%40mail.gmail.com.
