METATHEOREM: Use duality to see if any of the outstanding unknown implications can be resolved

[teorth]

Use the duality theorem https://teorth.github.io/equational_theories/blueprint/sect0002.html#duality to see if any of the unresolved implications (see #173) can be proven.

If the duality theorem is not yet formalized in Lean, one could output any such proven implications as a list of conjectures. If the duality theorem is formalized (see #122 for progress), then this could be output as a list of theorems instead.

Eventually, checking for duality reductions could be made part of the CI in #171.

[goens]

claim

[nomeata]

Do we really want to apply the duality theorem to all concrete proofs, roughly doubling the fact of ground truth theorems that Lean has to go through? Or would it suffice to consider duality as another way of “implied truth”, like transitivity?

[teorth]

I think once the duality theorem is formalized, in such a way that one could in principle automatically generate a proof of a dual implication from the proof of an implication, one can use duality as a source of implicit truth rather than explicit truth, i.e., update the transitivity tools to incorporate duality. A quicker but weaker alternative is to output the dual statements as conjectures rather than theorems; one could do that initially and deal with the updating of transitivity tooling later.

[goens]

I had understood it to be "implied", too (as a "metatheorem"). I'm working on it in #285 where I have the metatheorem (implies_op) so far. The problem is that we still haven't formalized the relationship between the "deep" and "shallow" versions (e.g. MagmaLaw end [Magma G] : @Eq G), so we can't yet apply implies_op to e.g. the implications in Subgraph.lean

[teorth]

Yeah, #36, #143, and #147 should eventually let one directly dualize shallow equivalences in Lean (and possibly #186 may end up being relevant as well), but we are still some ways from putting all that together. However, we should eventually get to the point where every implicit implication can be converted automatically (if desired) into an explicit Lean-proven implication, but we would not want to do this in the main Lean files as this would make compile times explode.

Ideally, the transitive closure code, once upgraded to also incorporate duality, should also be able to output, for a given implied implication or anti-implication, a human readable derivation of that statement from the explicit implications. Something like:

0. EquationX => EquationY is implicitly true. Proof:

1. EquationX' => EquationZ' (explicitly proven in [give Lean code reference])

2. EquationX => EquationZ (dual of 1)

3. EquationZ => EquationY (explicitly proven in [give Lean code reference])

4. EquationX => EquationY (combine 2 and 3), as desired.

or something like that. But that's a longer term goal, I can add it as an issue once this one is completed. In the even longer term, code could be provided to automatically convert this human-readable proof of an implication to a Lean-compilable proof.

[goens]

That sounds reasonable. Maybe we can start by merging #285 (changed it from draft to ready PR now), which proves the metatheorem itself, and add the transitive closure computations in a different PR, ideally once #36 lands as it would make things easier and someone is working on it now.

[teorth]

Is thre anything left to do here? Our transitive closure algorithm already incorporates duality, and we already have implies_iff_dual, as well as equivalences between laws and equations.

[goens]

sorry, I should have unclaimed this a while ago! I was distracted with other stuff. For completeness, formally adding the duality in Lean for all equations was missing, but this was just closed by @digama0 on #769