**Update** June 18, 2015: swapped conjunction and disjunction in first set of bullets. (thanks @FouriersTrick!)

**Update** June 17, 2015: My Idris code was incorrect. See the section after the **Closing** to hear how I went wrong.

This year, I’m attending the Oregon Programming Languages Summer School OPLSS. The program brings together students and teachers towards better understanding programming languages foundations. In short, it’s a whole lot of proof, category, and type theory, and their connections.

I’ve been taking advantage of the study time to get a firm grasp of dependently typed languages. In order to better understand the lectures, I’ve been trying to mechanize proofs of some of the theorems that have been shared. It also helps me to see tools based on these theories in action.

This blog post will show four simple proofs in three different languages. The proofs are:

- The distributive property of logical conjunction (and, ∧)
- The distributive property of logical disjunction (or, ∨)

For illustration, an example of an algebra that has a distributive property, is say, multiplication over addition within the integers:

The languages I’ll be using to demonstrate these proofs are:

Agda, after some false starts, was the most fun language for me to use. In part, this is because of the Haskell-like syntax. The emacs support for using the language as a theorem prover was also great. Case-splits, context information, type information, and automatic refinement were all great.

Here’s what all that looks like:

- The text edit buffer, with a single metavariable
`?`

- After pressing
`Ctrl-c Ctrl-l`

to load the buffer into Agda, the`?`

is replaced by a goal`{ }0`

:

- The context buffer at that same time:

- The context buffer after pressing
`Ctrl-c ,`

```
Goal: And .a .b
————————————————————————————————————————————————————————————
x : .b
a₁ : .a
.c : Set
.b : Set
.a : Set
```

Now, here’s the full proof:

```
module Proof where
data Or {a b} (A : Set a) (B : Set b) : Set1 where
Inl : A -> Or A B
Inr : B -> Or A B
data And {a b} (A : Set a) (B : Set b) : Set1 where
AndIntro : A -> B -> And A B
and_dist_over_or : {a b c : Set} -> And a (Or b c) -> Or (And a b) (And a c)
and_dist_over_or (AndIntro a₁ (Inl x)) = Inl (AndIntro a₁ x)
and_dist_over_or (AndIntro a₁ (Inr x)) = Inr (AndIntro a₁ x)
and_dist_over_or' : {a b c : Set} -> Or (And a b) (And a c) -> And a (Or b c)
and_dist_over_or' (Inl (AndIntro x x₁)) = AndIntro x (Inl x₁)
and_dist_over_or' (Inr (AndIntro x x₁)) = AndIntro x (Inr x₁)
or_dist_over_and : {a b c : Set} -> And (Or a b) (Or a c) -> Or a (And b c)
or_dist_over_and (AndIntro (Inl x) (Inl y)) = Inl x
or_dist_over_and (AndIntro (Inl x) (Inr y)) = Inl x
or_dist_over_and (AndIntro (Inr x) (Inl y)) = Inl y
or_dist_over_and (AndIntro (Inr x) (Inr y)) = Inr (AndIntro x y)
or_dist_over_and' : {a b c : Set} -> Or a (And b c) -> And (Or a b) (Or a c)
or_dist_over_and' (Inl x) = AndIntro (Inl x) (Inl x)
or_dist_over_and' (Inr (AndIntro x y)) = AndIntro (Inr x) (Inr y)
```

The `And`

and `Or`

data types were introduced to represent conjunction and disjunction.

A few things were notable to me:

As per type theory, the implementations themselves served as witnesses that such types could be constructed. That I could fill in an implementation is a proof, in that sense.

The type

`Set1`

exists in a universe a level above that of standard types,`Set`

. This makes sense, given that both`And`

and`Or`

are higher-kinded.The lack of a

`case`

construct in Agda made for a bit of duplicationI felt I could trust Agda throughout, as it caught me making mistakes when produing

`Inl`

or`Inr`

in some proofs.

Coq feels very different from Agda and Idris. The first difference is that its syntax is far more verbose, preferring to introduce `Theorems`

, `Definitions`

, and `Lemmas`

as alternative function definition forms. Data types were introduced with `Inductive`

, as far as I’ve seen, and all universal quantification `forall`

was explicit. It leans far closer to a proof assistant than a programming language, though it has enough support to be used to program functionally.

The emacs support for using Coq as a proof assistant was great. I used ProofGeneral, and in particular, the ProofGeneral-4.3pre150313 (development) release along with emacs-24.5.

A few key-binding:

`Ctrl-c Ctrl-b`

loads an emacs buffer into`coqtop`

`Ctrl-c Ctrl-c`

interrupts`coqtop`

; useful if it hangs`Ctrl-c ctrl-r`

retracts a buffer

Three buffers are open while working with ProofGeneral and Coq:

- Editing buffer
- coqtop response buffer
- (Proof) Goals buffer

This is an incomplete proof:

```
Theorem and_distributes : forall a b c : Prop,
(a /\ (b \/ c)) -> ((a /\ b) \/ (a /\ c)).
Proof.
intros.
destruct H as [HA [HB | HC]].
Case "L". left. split. apply HA. apply HB.
Case "R". right. split. apply HA.
```

After loading the editing buffer, the goal buffer shows:

```
1 subgoal, subgoal 1 (ID 52)
Case := "R" : String.string
a, b, c : Prop
HA : a
HC : c
============================
c
```

It’s really nice to know what the type of everything in the environment is, as well as what’s left in the goal. Most proofs I worked through involved clearing the bottom line, essentially showing that all these reductions make the left and right side of an implication reduce to `id`

, the identity function.

As most type theory indicates, `Equality`

is an interesting thing.

Here’s the proofs I completed in Coq:

```
(** Ignore from here ... **)
Ltac move_to_top x :=
match reverse goal with
| H : _ |- _ => try move x after H
end.
Tactic Notation "assert_eq" ident(x) constr(v) :=
let H := fresh in
assert (x = v) as H by reflexivity;
clear H.
Tactic Notation "Case_aux" ident(x) constr(name) :=
first [
set (x := name); move_to_top x
| assert_eq x name; move_to_top x
| fail 1 "because we are working on a different case"
].
Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
(**
... to here. That was all sugar to add the Case documentation
construct.
**)
Inductive and (P Q : Prop) : Prop := conj : P -> Q ->
(and P Q). Notation "P /\ Q" := (and P Q) : type_scope.
Inductive or (P Q : Prop) : Prop :=
| or_introl : P -> or P Q
| or_intror : Q -> or P Q.
Notation "P \/ Q" := (or P Q) : type_scope.
Theorem and_distributes : forall a b c : Prop,
(a /\ (b \/ c)) -> ((a /\ b) \/ (a /\ c)).
Proof.
intros.
destruct H as [HA [HB | HC]].
Case "L". left. split. apply HA. apply HB.
Case "R". right. split. apply HA. apply HC.
Qed.
Theorem or_distributes : forall a b c : Prop,
(a \/ (b /\ c)) -> ((a \/ b) /\ (a \/ c)).
Proof.
intros a b c. intros A.
destruct A as [A' | [BB BC]].
Case "left". split.
SCase "left". left. apply A'.
SCase "right". left. apply A'.
Case "right". split.
SCase "left". right. apply BB.
SCase "left". right. apply BC.
Qed.
Theorem or_distributes' : forall a b c : Prop,
((a \/ b) /\ (a \/ c)) -> (a \/ (b /\ c)).
Proof.
intros a b c. intros MAIN.
destruct MAIN as [[BA | BB] [CA | CC]].
Case "left1". left. apply BA.
SCase "left". left. apply BA.
Case "left2". left. apply CA.
SCase "right". right. split. apply BB. apply CC.
Qed.
```

Notably, for me:

- A distinct
`Notation`

directive for giving sugared syntax for arbitrary data types `Notation`

plays well with the tactics system, e.g.,`destruct`

and`split`

- Structuring proof scripts isn’t pretty. It’s an art, to be honest.
- The
`Case`

and`SCase`

constructs were introduced to add some readability; they’re not proof relevant. - The proving process was very much trial and error for me.
- Part of the challenge was learning the appropriate tactics
- The other part was applying them in the right order

Because of the challenge of working with Coq, I’m not very confident I could always find a proof of a thing if one existed. I attribute that largely to my inexperience working with Coq and provers like it. There’s much overlap with the functional languages I’ve worked with before, but the proof script portion wasn’t intuitive to me.

I was excited to play with Idris again. There’ve been several illustrative talks over the past year showing how one might use Idris in practice, covering such things as length-indexed vectors to safe printfs.

Agda and Idris share a lot in common. The Idris emacs mode also works with metavariables, marked with a `?`

. You can hover over a metavariable turned goal to learn what’s left to satisfy its proof.

I initially attempted writing proofs in Idris using proof tactics. I wanted to see how this mapped to my experience working in Coq. After finding some documentation on this, and giving it a try, I was left feeling discouraged. It wasn’t clear how to approach proofs in Idris using a tactical approach. My understanding is that the language wasn’t designed to work that way. That’s okay!

I then proceeded to write functional, constructive proofs. This went much more smoothly. Here’s the final outcome:

```
module Basics
%default total
data Or a b = Inl a | Inr b
data And a b = AndIntro a b
and_distributes_over_or : And a (Or b c) -> Or (And a b) (And a c)
and_distributes_over_or (AndIntro a x) =
case x of
Inl l => Inl (AndIntro a l)
Inr r => Inr (AndIntro a r)
and_distributes_over_or' : Or (And a b) (And a c) -> And a (Or b c)
and_distributes_over_or' x =
case x of
Inl (AndIntro a b) => AndIntro a (Inl b)
Inr (AndIntro a c) => AndIntro a (Inr c)
or_distributes_over_and : Or a (And b c) -> And (Or a b) (Or a c)
or_distributes_over_and x =
case x of
Inl l => AndIntro (Inl l) (Inl l)
Inr (AndIntro b c) => AndIntro (Inr b) (Inr c)
or_distributes_over_and' : And (Or a b) (Or a c) -> Or a (And b c)
or_distributes_over_and' (AndIntro ab ac) =
case ab of
Inl l => Inl l
Inr r => case ac of
Inl l' => Inl l'
Inr r' => Inr (AndIntro r r')
```

Notably:

- Idris needed fewer type annotations that Agda
- Idris had support for case statements
`%default total`

was needed at the start to enforce totality

Idris was a joy to work with!

I most enjoyed working with Agda. I think it most closely maps to my current mental model for doing proofs. I hope to work through CS410 to better understand how to work with Agda.

I look forward to working more with Coq in the near term. I’m particularly motivated by the existence of Software Foundations and CIS500.

I really liked working with Idris. I like it as much as Agda I think. The ability to leverage a `case`

to reduce repetition makes me very happy.

It’s still a bit early for me to say for sure what applications of these proofs would be. However, I suspect that much like parametricity tells us that certain definitions are correct by construction, I suspect that a suite of proofs could be use in place of tests to verify that modules continue to satisfy their desired behavior in the face of change.

These proofs might be over the structure of those modules, rather than over logical connectives, but I’m pretty excited that type systems are getting to the point where we can express and guarantee a lot with types!

In an earlier release of this post, I shared an incorrect Idris proof and attributed the error to the Idris unification engine. Here’s the original code:

```
module Basics
%default total
-- HERE'S MY ERROR
data Or a b = Inl a | Inr a
-- HERE'S My ERROR
data And a b = AndIntro a b
and_distributes_over_or : And a (Or b c) -> Or (And a b) (And a c)
and_distributes_over_or (AndIntro a x) =
case x of
Inl l => Inl (AndIntro a l)
Inr r => Inr (AndIntro a r)
and_distributes_over_or' : Or (And a b) (And a c) -> And a (Or b c)
and_distributes_over_or' x =
case x of
Inl (AndIntro a b) => AndIntro a (Inl b)
Inr (AndIntro a c) => AndIntro a (Inr c)
or_distributes_over_and : Or a (And b c) -> And (Or a b) (Or a c)
or_distributes_over_and x =
case x of
Inl l => AndIntro (Inl l) (Inr l)
Inr r => AndIntro (Inr r) (Inr r)
or_distributes_over_and' : And (Or a b) (Or a c) -> Or a (And b c)
or_distributes_over_and' (AndIntro ab ac) =
case ab of
Inl l => Inl l
Inr r => Inr r
```

Thanks greatly to Edwin Brady tweet for figuring this out! <3