Announcement: amc-prove

Posted on September 25, 2019
Word count: 331

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 PQP \to Q in the logic.
  • Product types P * Q, corresponding to PQP \land Q in the logic.
  • Sum types P + Q, corresponding to PQP \lor Q in the logic
  • tt and ff correspond to \top and \bot respectively
  • The propositional bi-implication type P <-> Q stands for P    QP \iff Q and is interpreted as PQQPP \to Q \land Q \to P

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 (PQ)RS(P \lor Q) \land R \to S by (PQ)RS(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 ¬¬(P¬P)\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
  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
% 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
  fun b -> b
? P -> Q -> P
  fun a b -> a
? Q -> P -> P
  fun a b -> b
? (P -> Q) * P -> Q
  fun (h, x) -> h x
? P * Q -> P
  fun (z, a) -> z
? P * Q -> Q
  fun (z, a) -> a
? P -> Q -> P * Q
  fun b c -> (b, c)
? P -> P + Q
  fun y -> L y
? Q -> P + Q
  fun y -> R y
? (P -> R) -> (Q -> R) -> P + Q -> R
  fun g f -> function
  | (L y) -> g y
  | (R c) -> f c
? not (P * not P)
  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)
(* 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)
  | (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.↩︎