2019-06-25 14:16:6 (GMT)
Simon and I started a discussion on the proof checker in private. We decided to move it here, in case other people are also interested:
Alexander Bentkamp: Hi Simon,
I've been playing with the proof checker, trying to add support for extensionality reasoning. My approach is to trust the implementation of the extensionality axiom (i.e. setting its proof to Proof.Step.trivial), but to reduce all other extensionality-based reasoning to that axiom.
For example, for the ho_ext_pos rule that derives f = g from f z = g z, the parents of the proof are the premise f z = g zwith the substitution z ↦ diff f g and the extensionality axiom x (diff x y) ≠ y (diff x y) ⋁ x = y with the substitution x ↦ f, y ↦ g. No changes to the proof checker are necessary.
In cases with Skolems, the situation is a bit more complicated. For example, the neg_ext rule derives f sk ≠ g sk from f ≠ g. Here, the extensionality axiom x (diff x y) ≠ y (diff x y) ⋁ x = y with the substitution x ↦ f, y ↦ g is not enough. The proof checker needs in addition the equation sk = diff f g. So, what I need is a mechanism in the proof checker to introduce "definitions" for Skolem symbols. The checker should make sure that only one definition is given per symbol and that the defined symbols do not occur in the original problem.
I saw that there is already something called "definition" in the proof checker and in the Skolem module. What is that intended to do? Can I use that?
Cheers,
Alex
Simon Cruanes: I haven't looked in a while, so let me go back to you on this. But from a high level perspective, if you can add sk = diff x y as a kind of side condition, the proof checker's congruence closure should be happy, so it seems like a good path. This could also allow CNF steps to be checked (by equating skolems to Hilbert ε terms, possibly.)
Alexander Bentkamp:
I haven't looked in a while, so let me go back to you on this. But from a high level perspective, if you can add sk = diff x y as a kind of side condition, the proof checker's congruence closure should be happy, so it seems like a good path.
Ok, then I will further experiment with this.
This could also allow CNF steps to be checked (by equating skolems to Hilbert ε terms, possibly.)
I have also been wondering about this, but it seems to me that the Skolems are not the only problem when attempting to verify the CNF trafo. Since we have only a ground prover, already a transformation like ∀x. P a ∧ Q x into P a ∧ ∀x. Q x cannot be proved with the current prover.
Simon Cruanes: Ah, didn't think about miniscoping, good call. Anyway proof checking doesn't have to be all-or-nothing.
Side notes:
- this discussion could go in the #zipperposition stream :)
- the proof checker admits, if I remember correctly, callbacks to add more equalities (intended for β reduction initially).
Alexander Bentkamp:
the proof checker admits, if I remember correctly, callbacks to add more equalities (intended for β reduction initially).
Don't know which method you mean, but of course I can easily add proof parents whose proof is Proof.Step.trivial. But I would like a mechanism that allows only one definition for each constant, and only for constants that are not in the original problem. Maybe I'll add a field on ID.Attr_skolem for the term represented by the Skolem. The LLProver could then generate an equation from that if necessary.
2019-06-25 14:46:31 (GMT)
I mean that you can add, into LLProver, a Rule.t that looks for subterms of the form (λx. t) u and adds (λx. t) u = u[x\t] to the tableau's branch.
2019-06-25 14:53:28 (GMT)
Ah, I see. Yes, that will be useful once I've added the information on the ID objects.
2019-06-25 14:56:3 (GMT)
There's a system for tagging proof steps with "theories" (to know whether the checker can actually check them) but it's very under-used right now.
I've been thinking for years of adding a basic Simplex solver to check LRA proofs, but given how rarely useful it is…
Otoh a mechanism for checking HO things would help y'all with your proofs, I believe :slight_smile:
2019-06-25 14:59:49 (GMT)
Except for extensionality, It seems to work nicely for HO already.
2019-06-25 15:10:57 (GMT)
You can display the low level proofs, btw (--dot-llproof <file> --check). We can discuss more about the checker in july :)
2019-06-25 16:42:18 (GMT)
Alexander Bentkamp: Except for extensionality, It seems to work nicely for HO already.
Actually, we might still have problems with boolean reasoning. I haven't tested that.
2019-06-25 17:31:28 (GMT)
I don't remember, but it should be doable to have a Tableau rule to split on x=true \oplus x=false for boolean subterm x, at least (for Avatar).
Overall the llprover doesn't do nearly as much as it eventually should. We should have rules for AC symbols (add t = norm_AC(t) to the CC whenever these differ), β reduction, eta-equivalence, extensionality, booleans, arith…
2019-06-25 19:32:59 (GMT)
but I tried some examples for beta/eta-equivalence and it seems to do that.
2019-06-25 19:45:33 (GMT)
ahhh I think it's done directly in LLTerm during conversion from normal terms. It's nice but not really sufficient in general (if you have a term f a, and later you assert f = λx. u, need to β reduce during proof search).
2019-06-25 19:47:2 (GMT)
My longer term plan is to use sidekick instead: a small functorized SMT solver that uses mSAT and should be more scalable than the basic tableau prover in LLProver.
It's not really ready yet, though.
2019-06-26 8:27:11 (GMT)
if you have a term f a, and later you assert f = λx. u, need to β reduce during proof search
But which kind of proof step would need this kind of reasoning? I can't think of any.
2019-06-26 13:24:44 (GMT)
But which kind of proof step would need this kind of reasoning? I can't think of any.
If you had a combined superposition + β reduction inference. I'm not saying it's necessary right now.