Announcement: amc-prove

Posted on September 25, 2019

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

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 \((P \lor Q) \land R \to S\) by \((P \lor Q) \to R \to S\) (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 \(\neg\neg(P \lor \neg{}P)\), 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.
?

Usage sample

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.


  1. 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.↩︎