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:
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:
?Ctrl-c Ctrl-l to load the buffer into Agda, the ? is replaced by a goal { }0:Ctrl-c ,Goal: And .a .b
————————————————————————————————————————————————————————————
x : .b
a₁ : .a
.c : Set
.b : Set
.a : SetNow, 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 duplication
I 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 coqtopCtrl-c Ctrl-c interrupts coqtop; useful if it hangsCtrl-c ctrl-r retracts a bufferThree buffers are open while working with ProofGeneral and Coq:
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
============================
cIt’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:
Notation directive for giving sugared syntax for arbitrary data typesNotation plays well with the tactics system, e.g., destruct and splitCase and SCase constructs were introduced to add some readability; they’re not proof relevant.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:
%default total was needed at the start to enforce totalityIdris 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 rThanks greatly to Edwin Brady tweet for figuring this out! <3