Define basic well-formedness of LFunc/Factory and prove WF of Boogie Factory

[aqjune-aws]

Description of changes:

This patch

• defines very basic well-formedness of LFunc and Factory, which include a desirable property previously written in a comment
• Prove that Factory.addFactoryFunc and Factory.addFactory preserves well-formedness
• Prove that Boogie's Factory is well-formed.

The motivation of this patch is somewhat in a similar context to adding conformance testing to Boogie operations. Since Boogie has many operations, there can be hidden bugs and I wanted to confirm whether these are good.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[shigoel]

Oof! What's going on here? Can you trace why we need this?

Also, I'd rather have set_option ... in directly above the offending construct to localize these settings.

[aqjune-aws]

I think it is from the tactics used for proving LFuncWf.concreteEval_argmatch, but was not crystal clear. Used set_option .. in.

[shigoel]

Hmm, maybe it's grind?

[aqjune-aws]

Maybe, but actually my impression was that it was a sequence of expensive tactics that made it eventually overflow.
If fully unrolled, the proof structure will be "take the first element of the Factory list, prove WF of the LFunc, take second element, prove WF of it, take third, ....". Since there are quite a few functions in Factory, the depth becomes quite deep but still affordable by Lean I guess.

And then here comes my theory: ideally, the expensive tactics like simp or grind are supposed to work at the "leaves" of the proof tree, avoiding multiplying the depth of the proof tree by a large constant. But my hypothesis is that this might not always the case in practice because for example discharging subgoal i might resolve hidden metavariables that will be used at subgoal i+1, making the size of the final subgoal state super large. So, the size of the sub-proof term increases as i increases, making the tactics more expensive too.

But this is indeed a conjecture. Actually, a preferred direction in the Lean world might be to define a custom computable decision procedure, prove that once the decision procedure is correct then the property holds, and use that (as the new Decidable instance in this patch did :). It did not immediately apply to this LFuncWf.concreteEval_argmatch because it is not decidable, but I am guessing that if using partial functions are allowed for Decidable then this could be resolved. But I haven't dived further, but this would be necessary if there are even more functions added to Factory.

[shigoel]

Thanks for the explanation and your theory!