Constructors for propositions?

[jkarni]

Currently Logic.Propositional doesn't have constructors - e.g.:

data And p q

So that if you want to manipulate proofs, you have to use the provided axioms. There are plenty of circumstances where pattern matching would make things nicer. E.g.:

replaceThird :: p -> (a && b && c) -> a && p && c
replaceThird p (a `And` b `And` c) = a `And` p `And` c

This becomes particularly important when you want to use domain-level proofs that do use constructors.

A quick look suggests all connectives could have such constructors (they'd just be the introduction rules). It seems to me you could still keep Proof, and that would allow erasing constructors and using the rest of the library as is. Would it make sense to send a PR with the constructors?

(Thanks for the great library and idea!)

[matt-noonan]

Hmm, I feel squeamish about this and I'm not entirely sure why. I guess because it involves manipulating the proof values directly, instead of underneath Proof? How would you apply your replaceThird function to a Proof (a && b && c) value? Or are you proposing to replace Proof p with p across the board?

Another possible point in the design space would be to keep Proof, but make it into a GADT with constructors for QED and the Logic.Propositional types, something like this:

data Proof (pf :: k) where
    QED :: Proof p
    AND :: Proof p -> Proof q -> Proof (p && q)
    OR_L :: Proof p -> Proof (p || q)
    OR_R :: Proof q -> Proof (p || q)
    ...

That would allow for pattern-matching, with the twist that every match would also have to have a QED case for when the property was just asserted by a library author, not proven. Ah, but is this a hitch in your proposal? After all, in your example the a && b && c might have been proven by fiat, instead of using the And constructor!

[jkarni]

My original thought was just exposing a proof :: a -> Proof a. But I know see that's kind of annoying on it's own, since you lose the ability to pattern match once you're inside Proof.

But it seems like Proof can be made into a monad, in which case you can still combine pattern matching and axioms (and so e.g. replaceThird x can just be fmapped over a Proof - and indeed, even just functor would be nice).

Anyhow see there's a decent amount of change involved in this, so please feel free to close this issue!