Word count: 331

`amc-prove`

is a smallish tool to automatically prove (some) sentences
of constructive quantifier-free^{1} 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 $P \to Q$ in the logic. - Product types
`P * Q`

, corresponding to $P \land Q$ in the logic. - Sum types
`P + Q`

, corresponding to $P \lor Q$ in the logic `tt`

and`ff`

correspond to $\top$ and $\bot$ respectively- The propositional bi-implication type
`P <-> Q`

stands for $P \iff Q$ and is interpreted as $P \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 $(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.

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