> The first line doesn’t look like a full expansion, because A gets multiplied by a sum of other variables. ...
Yes, you are right, that's a bug in my program. What actually has happened is that in the routine which is supposed to expand X and Y before expanding X x. Y by distributivity, I forgot to record the proofs for X = (expanded X) and Y = (expanded Y). So that's why some steps are missing and the proof starts with a strange line. It's funny that it unified at all! The correct proved statement is this: |- ( ( ( A + B ) x. ( A + B ) ) x. A ) = ( ( ( ( A x. A ) x. A ) + ( ( B x. A ) x. A ) ) + ( ( ( A x. B ) x. A ) + ( ( B x. B ) x. A ) ) ) I think I fixed the program, here's the correct proof <https://expln.github.io/lamp/dev/index.html?editorState=eyJzcmNzIjpbeyJ0eXAiOiJXZWIiLCJmaWxlTmFtZSI6IiIsInVybCI6Imh0dHBzOi8vdXMubWV0YW1hdGgub3JnL21ldGFtYXRoL3NldC5tbSIsInJlYWRJbnN0ciI6IlJlYWRBbGwiLCJsYWJlbCI6IiIsInJlc2V0TmVzdGluZ0xldmVsIjp0cnVlLCJhbGxMYWJlbHMiOltdfV0sImRlc2NyIjoiIiwidmFyc1RleHQiOiIiLCJkaXNqVGV4dCI6IiIsInN0bXRzIjpbeyJsYWJlbCI6InFlZC4xIiwidHlwIjoiZSIsImlzR29hbCI6ZmFsc2UsImlzQmttIjpmYWxzZSwiY29udCI6InwtIEEgZS4gQ0MiLCJqc3RmVGV4dCI6IiJ9LHsibGFiZWwiOiJxZWQuMiIsInR5cCI6ImUiLCJpc0dvYWwiOmZhbHNlLCJpc0JrbSI6ZmFsc2UsImNvbnQiOiJ8LSBCIGUuIENDIiwianN0ZlRleHQiOiIifSx7ImxhYmVsIjoiMSIsInR5cCI6InAiLCJpc0dvYWwiOmZhbHNlLCJpc0JrbSI6ZmFsc2UsImNvbnQiOiJ8LSAoIEEgKyBCICkgZS4gQ0MiLCJqc3RmVGV4dCI6InFlZC4xIHFlZC4yIDogYWRkY2xpIn0seyJsYWJlbCI6IjIiLCJ0eXAiOiJwIiwiaXNHb2FsIjpmYWxzZSwiaXNCa20iOmZhbHNlLCJjb250IjoifC0gKCAoIEEgKyBCICkgeC4gKCBBICsgQiApICkgPSAoICggKCBBICsgQiApIHguIEEgKSArICggKCBBICsgQiApIHguIEIgKSApIiwianN0ZlRleHQiOiIxIHFlZC4xIHFlZC4yIDogYWRkZGlpIn0seyJsYWJlbCI6IjMiLCJ0eXAiOiJwIiwiaXNHb2FsIjpmYWxzZSwiaXNCa20iOmZhbHNlLCJjb250IjoifC0gKCAoIEEgKyBCICkgeC4gQSApID0gKCAoIEEgeC4gQSApICsgKCBCIHguIEEgKSApIiwianN0ZlRleHQiOiJxZWQuMSBxZWQuMiBxZWQuMSA6IGFkZGRpcmkifSx7ImxhYmVsIjoiNCIsInR5cCI6InAiLCJpc0dvYWwiOmZhbHNlLCJpc0JrbSI6ZmFsc2UsImNvbnQiOiJ8LSAoICggQSArIEIgKSB4LiBCICkgPSAoICggQSB4LiBCICkgKyAoIEIgeC4gQiApICkiLCJqc3RmVGV4dCI6InFlZC4xIHFlZC4yIHFlZC4yIDogYWRkZGlyaSJ9LHsibGFiZWwiOiI1IiwidHlwIjoicCIsImlzR29hbCI6ZmFsc2UsImlzQmttIjpmYWxzZSwiY29udCI6InwtICggKCAoIEEgKyBCICkgeC4gQSApICsgKCAoIEEgKyBCICkgeC4gQiApICkgPSAoICggKCBBIHguIEEgKSArICggQiB4LiBBICkgKSArICggKCBBICsgQiApIHguIEIgKSApIiwianN0ZlRleHQiOiIzIDogb3ZlcTFpIn0seyJsYWJlbCI6IjYiLCJ0eXAiOiJwIiwiaXNHb2FsIjpmYWxzZSwiaXNCa20iOmZhbHNlLCJjb250IjoifC0gKCAoICggQSB4LiBBICkgKyAoIEIgeC4gQSApICkgKyAoICggQSArIEIgKSB4LiBCICkgKSA9ICggKCAoIEEgeC4gQSApICsgKCBCIHguIEEgKSApICsgKCAoIEEgeC4gQiApICsgKCBCIHguIEIgKSApICkiLCJqc3RmVGV4dCI6IjQgOiBvdmVxMmkifSx7ImxhYmVsIjoiNyIsInR5cCI6InAiLCJpc0dvYWwiOmZhbHNlLCJpc0JrbSI6ZmFsc2UsImNvbnQiOiJ8LSAoICggQSArIEIgKSB4LiAoIEEgKyBCICkgKSA9ICggKCAoIEEgeC4gQSApICsgKCBCIHguIEEgKSApICsgKCAoIEEgeC4gQiApICsgKCBCIHguIEIgKSApICkiLCJqc3RmVGV4dCI6IjIgNSA2IDogM2VxdHJpIn0seyJsYWJlbCI6IjgiLCJ0eXAiOiJwIiwiaXNHb2FsIjpmYWxzZSwiaXNCa20iOmZhbHNlLCJjb250IjoifC0gKCAoICggQSArIEIgKSB4LiAoIEEgKyBCICkgKSB4LiBBICkgPSAoICggKCAoIEEgeC4gQSApICsgKCBCIHguIEEgKSApICsgKCAoIEEgeC4gQiApICsgKCBCIHguIEIgKSApICkgeC4gQSApIiwianN0ZlRleHQiOiI3IDogb3ZlcTFpIn0seyJsYWJlbCI6IjkiLCJ0eXAiOiJwIiwiaXNHb2FsIjpmYWxzZSwiaXNCa20iOmZhbHNlLCJjb250IjoifC0gKCBBIHguIEEgKSBlLiBDQyIsImpzdGZUZXh0IjoicWVkLjEgcWVkLjEgOiBtdWxjbGkifSx7ImxhYmVsIjoiMTAiLCJ0eXAiOiJwIiwiaXNHb2FsIjpmYWxzZSwiaXNCa20iOmZhbHNlLCJjb250IjoifC0gKCBCIHguIEEgKSBlLiBDQyIsImpzdGZUZXh0IjoicWVkLjIgcWVkLjEgOiBtdWxjbGkifSx7ImxhYmVsIjoiMTEiLCJ0eXAiOiJwIiwiaXNHb2FsIjpmYWxzZSwiaXNCa20iOmZhbHNlLCJjb250IjoifC0gKCAoIEEgeC4gQSApICsgKCBCIHguIEEgKSApIGUuIENDIiwianN0ZlRleHQiOiI5IDEwIDogYWRkY2xpIn0seyJsYWJlbCI6IjEyIiwidHlwIjoicCIsImlzR29hbCI6ZmFsc2UsImlzQmttIjpmYWxzZSwiY29udCI6InwtICggQSB4LiBCICkgZS4gQ0MiLCJqc3RmVGV4dCI6InFlZC4xIHFlZC4yIDogbXVsY2xpIn0seyJsYWJlbCI6IjEzIiwidHlwIjoicCIsImlzR29hbCI6ZmFsc2UsImlzQmttIjpmYWxzZSwiY29udCI6InwtICggQiB4LiBCICkgZS4gQ0MiLCJqc3RmVGV4dCI6InFlZC4yIHFlZC4yIDogbXVsY2xpIn0seyJsYWJlbCI6IjE0IiwidHlwIjoicCIsImlzR29hbCI6ZmFsc2UsImlzQmttIjpmYWxzZSwiY29udCI6InwtICggKCBBIHguIEIgKSArICggQiB4LiBCICkgKSBlLiBDQyIsImpzdGZUZXh0IjoiMTIgMTMgOiBhZGRjbGkifSx7ImxhYmVsIjoiMTUiLCJ0eXAiOiJwIiwiaXNHb2FsIjpmYWxzZSwiaXNCa20iOmZhbHNlLCJjb250IjoifC0gKCAoICggKCBBIHguIEEgKSArICggQiB4LiBBICkgKSArICggKCBBIHguIEIgKSArICggQiB4LiBCICkgKSApIHguIEEgKSA9ICggKCAoICggQSB4LiBBICkgKyAoIEIgeC4gQSApICkgeC4gQSApICsgKCAoICggQSB4LiBCICkgKyAoIEIgeC4gQiApICkgeC4gQSApICkiLCJqc3RmVGV4dCI6IjExIDE0IHFlZC4xIDogYWRkZGlyaSJ9LHsibGFiZWwiOiIxNiIsInR5cCI6InAiLCJpc0dvYWwiOmZhbHNlLCJpc0JrbSI6ZmFsc2UsImNvbnQiOiJ8LSAoICggKCBBIHguIEEgKSArICggQiB4LiBBICkgKSB4LiBBICkgPSAoICggKCBBIHguIEEgKSB4LiBBICkgKyAoICggQiB4LiBBICkgeC4gQSApICkiLCJqc3RmVGV4dCI6IjkgMTAgcWVkLjEgOiBhZGRkaXJpIn0seyJsYWJlbCI6IjE3IiwidHlwIjoicCIsImlzR29hbCI6ZmFsc2UsImlzQmttIjpmYWxzZSwiY29udCI6InwtICggKCAoIEEgeC4gQiApICsgKCBCIHguIEIgKSApIHguIEEgKSA9ICggKCAoIEEgeC4gQiApIHguIEEgKSArICggKCBCIHguIEIgKSB4LiBBICkgKSIsImpzdGZUZXh0IjoiMTIgMTMgcWVkLjEgOiBhZGRkaXJpIn0seyJsYWJlbCI6IjE4IiwidHlwIjoicCIsImlzR29hbCI6ZmFsc2UsImlzQmttIjpmYWxzZSwiY29udCI6InwtICggKCAoICggQSB4LiBBICkgKyAoIEIgeC4gQSApICkgeC4gQSApICsgKCAoICggQSB4LiBCICkgKyAoIEIgeC4gQiApICkgeC4gQSApICkgPSAoICggKCAoIEEgeC4gQSApIHguIEEgKSArICggKCBCIHguIEEgKSB4LiBBICkgKSArICggKCAoIEEgeC4gQiApICsgKCBCIHguIEIgKSApIHguIEEgKSApIiwianN0ZlRleHQiOiIxNiA6IG92ZXExaSJ9LHsibGFiZWwiOiIxOSIsInR5cCI6InAiLCJpc0dvYWwiOmZhbHNlLCJpc0JrbSI6ZmFsc2UsImNvbnQiOiJ8LSAoICggKCAoIEEgeC4gQSApIHguIEEgKSArICggKCBCIHguIEEgKSB4LiBBICkgKSArICggKCAoIEEgeC4gQiApICsgKCBCIHguIEIgKSApIHguIEEgKSApID0gKCAoICggKCBBIHguIEEgKSB4LiBBICkgKyAoICggQiB4LiBBICkgeC4gQSApICkgKyAoICggKCBBIHguIEIgKSB4LiBBICkgKyAoICggQiB4LiBCICkgeC4gQSApICkgKSIsImpzdGZUZXh0IjoiMTcgOiBvdmVxMmkifSx7ImxhYmVsIjoiMjAiLCJ0eXAiOiJwIiwiaXNHb2FsIjpmYWxzZSwiaXNCa20iOmZhbHNlLCJjb250IjoifC0gKCAoICggKCBBIHguIEEgKSArICggQiB4LiBBICkgKSArICggKCBBIHguIEIgKSArICggQiB4LiBCICkgKSApIHguIEEgKSA9ICggKCAoICggQSB4LiBBICkgeC4gQSApICsgKCAoIEIgeC4gQSApIHguIEEgKSApICsgKCAoICggQSB4LiBCICkgeC4gQSApICsgKCAoIEIgeC4gQiApIHguIEEgKSApICkiLCJqc3RmVGV4dCI6IjE1IDE4IDE5IDogM2VxdHJpIn0seyJsYWJlbCI6InFlZCIsInR5cCI6InAiLCJpc0dvYWwiOnRydWUsImlzQmttIjpmYWxzZSwiY29udCI6InwtICggKCAoIEEgKyBCICkgeC4gKCBBICsgQiApICkgeC4gQSApID0gKCAoICggKCBBIHguIEEgKSB4LiBBICkgKyAoICggQiB4LiBBICkgeC4gQSApICkgKyAoICggKCBBIHguIEIgKSB4LiBBICkgKyAoICggQiB4LiBCICkgeC4gQSApICkgKSIsImpzdGZUZXh0IjoiOCAyMCA6IGVxdHJpIn1dfQ==> (I hope). > Intermediate variables become necessary for my tactics when there are also constants, for example, ( A x. ( ( 2 + 1 ) x. B ) ). I guess it's not entirely clear how to do that automatically, indeed. Say, if you have ( ( ( 3 x. 2 ) x. A ) x. B ), in some cases you would want to transform it into ( ( 6 x. A ) x. B ) and in other cases it's better to leave it as is. Ideally, you would want to be able to type |- X = Y and let the tactic figure out the rest :-) > However, from what I see, transformations.js uses trickier algorithms. As I understand it, there's an *arithEval* function which can parse metamath expressions like ( ( ; 3 1 + ; 9 0 ) x. 3 ) and evaluate them to a concrete integer (363 in this case). I don't think it's very tricky, but I haven't tried implementing something like that myself, so I might be underestimating it. -- 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/f6d09abf-00fe-49fa-a3f9-5700ebd9d3b5n%40googlegroups.com.
