amc-prove is a smallish tool to automatically prove (some) sentences of constructive quantifier-free1 first-order logic using the Amulet compiler’s capability to suggest replacements for typed holes.
In addition to printing whether or not it could determine the truthiness of the sentence,
amc-prove will also report the smallest proof term it could compute of that type.
What works right now
- Function types
P -> Q, corresponding to in the logic.
- Product types
P * Q, corresponding to in the logic.
- Sum types
P + Q, corresponding to in the logic
ffcorrespond to and respectively
- The propositional bi-implication type
P <-> Qstands for and is interpreted as
What is fiddly right now
Amulet will not attempt to pattern match on a sum type nested inside a product type. Concretely, this means having to replace by (currying).
amc-prove’s support for negation and quantifiers is incredibly fiddly. There is a canonical empty type,
ff, but the negation connective
not P expands to
P -> forall 'a. 'a, since empty types aren’t properly supported. As a concrete example, take the double-negation of the law of excluded middle , which holds constructively.
If you enter the direct translation of that sentence as a type,
amc-prove will report that it couldn’t find a solution. However, by using
P -> ff instead of
not P, a solution is found.
? not (not (P + not P)) probably not. ? ((P + (P -> forall 'a. 'a)) -> forall 'a. 'a) -> forall 'a. 'a probably not. ? ((P + (P -> ff)) -> ff) -> ff yes. fun f -> f (R (fun b -> f (L b)))
How to get it
amc-prove is bundled with the rest of the Amulet compiler on Github. You’ll need Stack to build. I recommend building with
stack build --fast since the compiler is rather large and
amc-prove does not benefit much from GHC’s optimisations.
% git clone https://github.com/tmpim/amc-prove.git % cd amc-prove % stack build --fast % stack run amc-prove Welcome to amc-prove. ?
Here’s a small demonstration of everything that works.
? P -> P yes. fun b -> b ? P -> Q -> P yes. fun a b -> a ? Q -> P -> P yes. fun a b -> b ? (P -> Q) * P -> Q yes. fun (h, x) -> h x ? P * Q -> P yes. fun (z, a) -> z ? P * Q -> Q yes. fun (z, a) -> a ? P -> Q -> P * Q yes. fun b c -> (b, c) ? P -> P + Q yes. fun y -> L y ? Q -> P + Q yes. fun y -> R y ? (P -> R) -> (Q -> R) -> P + Q -> R yes. fun g f -> function | (L y) -> g y | (R c) -> f c ? not (P * not P) yes. Not (fun (a, (Not h)) -> h a) (* Note: Only one implication of DeMorgan's second law holds constructively *) ? not (P + Q) <-> (not P) * (not Q) yes. (* Note: I have a marvellous term to prove this proposition, but unfortunately it is too large to fit in this margin. *) ? (not P) + (not Q) -> not (P * Q) yes. function | (L (Not f)) -> Not (fun (a, b) -> f a) | (R (Not g)) -> Not (fun (y, z) -> g z)
You can find the proof term I redacted from DeMorgan’s first law here.
Technically, amc-prove “supports” the entire Amulet type system, which includes things like type-classes and rank-N types (it’s equal in expressive power to System F). However, the hole-filling logic is meant to aid the programmer while she codes, not exhaustively search for a solution, so it was written to fail early and fail fast instead of spending unbounded time searching for a solution that might not be there.↩︎