Beginner Notes on proofs in Idris

I’m not very bright, but even I was able to get a bit comfortable with proofs. Here are my notes on actually using the Idris type system to prove things. Next time I’ll write about how I think proofs fit practically in software development after exploring minikanren last year and compare them both to traditional unit testing. I’m still a noob at this, so those experienced might want to avert their eyes. My goal here is to have a place online where some common questions about the forms and practices of proofs in Idris are documented in a more explanatory style, which will be Ok (maybe even better) with the amateur things presented.

Some things I don’t feel are well explained, or aren’t emphasized enough:

The type of a proof is (a = b), and yes single equals really is what might be thought of as a type-level constructor in Idris. This part took me a lot of mind bending to really get in my head, even though I had been writing (a : Nat) -> Type for equalities, it hadn’t really settled.

I now imagine that in the background there’s an OpEq : Type -> Type -> Type floating around and that the type of (a = b) is really syntactic sugar for some OpEq a b, because it helps me imagine what’s happening in way that fits my mental model.

The type of wrong proofs is (a = b) -> Void, which is weird, and kind of builtin. The truth is it could just as easily be some type (a ≠ b), unicode notwitstanding but instead it’s a function type (a = b) -> Void. About midway through learning the prover, I was struct by the idea that I might be able to extract the (a = b) part and use it to rewrite wrong assertions into provably wrong assertions. I wrote the type level code to do it (YOLO!), but Idris will not force such code to be sound, because that isn’t its convention.

Idris’ prover has special handling for things like (2 = S (S (S a))) so that “Refl impossible” understands why you want a function from some (a = b) -> Void when (a = b) is unsound. You’re not only doing your own computation on types, but it can feel like you are. This is not the only way to get an (a = b) -> Void, but it’s the only way that allows Idris to check your work.

The proper way to write a proof that something is trivially untrue is:

thisIsNotTrue : {a : Nat} -> (S (S a) = 1) -> Void
thisIsNotTrue   Refl         Refl             impossible

I feel that it isn’t explained well what this does, so I used formatting to make more sense of it.

Arguments in { .. } are implied arguments in Idris. You can specify their value as Refl when you don’t need the value in a proof. The implied argument doesn’t need to appear anywhere else, but you can’t do anything with it if it doesn’t appear in the (a = b) type you’re reasoning about. That it’s implied means you don’t have to (and can’t by curried application) specify it yourself when you use thisIsNotTrue in a DecEq No or to prove that something else is untrue.

One reason to not use implied arguments in this way is if you want to rewrite subexpressions in different ways using the same rule more naturally.

There are times Idris itself rewrites (or can rewrite) things and it can be very confusing. Especially, proofs that come down to comparing natural numbers can be weird because Idris can rewrite the left side of plus.

Case example:

testPlusA0 : (n : Nat) -> n = plus n 0 
testPlusA0 Z = Refl 
testPlusA0 (S k) = 
 let rec = testPlusA0 {n=k} in 
 rewrite rec in Refl
plusS1Eq2 : (n : Nat) -> plus n (S Z) = S n
plusS1Eq2 Z = Refl
plusS1Eq2 (S a) =
  let rec = plusS1Eq2 {n=a} in
  rewrite rec in Refl
add2NEqNP2 : (n : Nat) -> (a : Nat) -> S (plus n a) = plus n (S a) 
add2NEqNP2 Z Z = Refl 
add2NEqNP2 Z (S a) = Refl 
add2NEqNP2 n Z = 
 rewrite sym (testPlusA0 n) in 
 rewrite (plusS1Eq2 n) in Refl 
 
add2NEqNP2 (S n) (S a) =
  rewrite (add2NEqNP2 n (S a)) in
  Refl
fourSBackIn : (a : Nat) -> (S (S (S (S (plus (plus a a) (plus a a))))) = plus (plus (S a) (S a)) (plus (S a) (S a))) 
fourSBackIn Z = Refl 
fourSBackIn (S a) = 
 rewrite sym (add2NEqNP2 a a) in 
 rewrite sym (add2NEqNP2 a (S a)) in 
 rewrite sym (add2NEqNP2 a a) in 
 rewrite sym (add2NEqNP2 (plus a a) (S (plus a a))) in 
 rewrite sym (add2NEqNP2 (plus a a) (plus a a)) in 
 rewrite sym (add2NEqNP2 (plus a a) (S (S (S (plus a a))))) in 
 rewrite sym (add2NEqNP2 (plus a a) (S (S (plus a a)))) in 
 rewrite sym (add2NEqNP2 (plus a a) (S (plus a a))) in 
 rewrite sym (add2NEqNP2 (plus a a) (plus a a)) in 
 ?fourSBackInProof

Can you really replace ?fourSBackInProof with Refl ? Yes. Idris rewrites plus down the left side only and can make inferences about it:

Bin.fourSBackInProof : (\replaced => 
 S (S (S (S (S (S (S (S (plus (plus a a) (plus a a))))))))) = 
 S (S (S (S (S (S (S replaced))))))) (S (plus (plus a a) (plus a a)))

Note that I didn’t rewrite any of the left terms of the plus applications … Idris freely moves the S on that side. It bothered me that there’s a stray S in replaced clause but I couldn’t figure out a single way to get Idris to rewrite all the Ss in the hole function :-). Most of the time the prover requires you to take it through every step, but this one case is different. There may be others, so use and pay attention to holes after rewriting.

But … what does rewrite actually do?

It changes any type that has (a = b) in it if part of one side precisely matches either the left or right part of the (a = b) type given to rewrite, depending on whether it’s applied with sym or not. It’s a bit of a fuzzy “precisely” because Idris can rewrite certain narrow things (like the Ss in the left side of plus). Importantly, this changes the goal of the proof from below while actual computations try to reach the proof from above.

 ?haveToProveSomethingComplicated -- You are here
 ... -- ? unknown steps 
 ...
 ...
 (complicated = goal) -- What we want
rewrite makes the goal simpler:
 rewrite (simpler = complicated) in
 ?haveToProveSomethingSimpler 
 ...
 ...
 -- (simpler = goal)
 --  ^-- rewrite (simpler = complicated) moved the goal UP
 -- (complicated = goal)
rewrite again:
 ?haveToProveSomethingComplicated
 rewrite (simpler = complicated) in
 rewrite (trivial = simpler) in
 ?verifyHoleIsTrivial
 ...
 -- (trivial = goal)
 -- ^-- rewrite made it better again
 -- (simpler = goal)
 -- (complicated = goal)
finally:
 rewrite (simpler = complicated) in
 rewrite (trivial = simpler) in
 Refl -- We snatch the goal my moving down toward it

Like this

a2Pa4 : (a : Nat) -> Dec (2 = a) -> Dec (4 = plus a a) 
a2Pa4 (S (S Z)) _ = Yes Refl 
a2Pa4 a (Yes r) = 
 rewrite r in 
 rewrite sym r in Yes Refl 
a2Pa4 Z (No contra) = No fourIsNotZero 
a2Pa4 (S Z) _ = No fourIsNotTwo 
a2Pa4 (S (S (S a))) (No contra) = 
 rewrite sym (add2NEqNP2 a (S (S a))) in -- Rewrite moves the goal
 rewrite sym (add2NEqNP2 a (S a)) in     -- closer so it'll be in
 rewrite sym (add2NEqNP2 a a) in         -- reach ...
 No fourIsNotAPlus6                      -- And we pounce from above

The proper type of “implies” relationships is Dec (a = b). You can write

(n : Nat) -> Dec (n = 0) -> Dec (S (S n) = 2)

When you want to prove that a certain thing implies another thing depending on variable values, and

(n : Nat) -> (S (S (plus n n) = plus (S n) (S n))

When the proposition is true for all n.

You can use (a = b) from Dec (a = b) in with clauses and in case expressions. The prover is totally fine understanding case expressions, actually, however watch out for the No case, because it may not give you any more power.

Consider:

twoTimesAIsZeroIfAIs : (a : Nat) -> Dec (a = 0) -> Dec (plus a a = 0) 
twoTimesAIsZeroIfAIs a (Yes prf) = rewrite prf in Yes Refl 
twoTimesAIsZeroIfAIs Z _ = Yes Refl 
twoTimesAIsZeroIfAIs (S a) (No contra) = 
 rewrite sym (add2NEqNP2 a a) in 
 No $ \prf => 
 sNotZ {a=S (plus a a)} prf

I had to prove the No case separately, not using the contra argument to No, which is actually pretty common.

Exploring the No case. Holes are your friend.

This was explained to me by a patient person on reddit.

The No case of Dec is a weird beast to look at: it’s type is something like:

No ((a = b) -> Void) -- O_o

If you’re used to thinking of data constructors carrying values, this doesn’t feel great, but in this case, the type constructor just has the type of things that are proofs that other things are inconsistent :-O

So how do you use this?

If you’re proving that something implies something else, then you have to provide a function(?)… Let me write it like this:

twoTimesAIsZeroIfAIs : (a : Nat) -> Dec (a = 0) -> Dec (plus a a = 0) 
twoTimesAIsZeroIfAIs a (Yes prf) = rewrite prf in Yes Refl 
twoTimesAIsZeroIfAIs Z _ = Yes Refl 
twoTimesAIsZeroIfAIs (S a) (No contra) =
 let nofun prf = sNotZ {a=S (plus a a)} prf in
 rewrite sym (add2NEqNP2 a a) in 
 No nofun

So nofun is a function of …

(S (S (plus a a)) = 0) -> Void

In the abstract, this proof is completed when the argument contra to No is given an argument of type (S (S (plus a a)) = 0) and yields a Void result. Any function that has an argument of type (S (S (plus a a)) = 0) and a result of Void can fill this role, and since part of this has an (a = b) type, it can be rewritten to make it something easier to fill.

It’s weird to think of rewriting the argument type of a function, but these types don’t have runtime values. It’s ok. Eat some soup.

Sometimes the “contra” argument to no is what you want (it is a function yielding Void after all), and can be used either directly or as an argument to another proof that proves some implication (rw : Dec (a = b)) -> Dec (c = d) when rw = No contra.

plusA1EqPlusB1 : (a : Nat) -> (b : Nat) -> Dec (a = b) -> Dec (plus a 1 = plus b 1) 
plusA1EqPlusB1 a b (Yes prf) = 
 rewrite prf in Yes Refl 
plusA1EqPlusB1 a b (No contra) = 
 let re = plusA0EqPlusB0 a b (decEq (plus a 1) (plus b 1)) in 
 rewrite plusS1Eq2 a in 
 rewrite plusS1Eq2 b in 
 saEqSb2 a b (No contra)

Don’t pre-prove subgoals.

Many times I made functions representing subgoals and proved them, only to realize that I couldn’t easily get from the subgoal to the main one, or that it overlapped something I had an easier proof for later. In the event of a cabin pressure change, always prove your own goal before securing your subgoals!

-- Imagine that I have't written plusS1Eq2 yet:
plusS1Eq2 : (n : Nat) -> plus n (S Z) = S n
plusS1Eq2 n = ?plusS1Eq2Proof -- Idris just assumes this works :-)
plusA1EqPlusB1 : (a : Nat) -> (b : Nat) -> Dec (a = b) -> Dec (plus a 1 = plus b 1) 
plusA1EqPlusB1 a b (Yes prf) = 
 rewrite prf in Yes Refl 
plusA1EqPlusB1 a b (No contra) = 
 let re = plusA0EqPlusB0 a b (decEq (plus a 1) (plus b 1)) in 
 rewrite plusS1Eq2 a in 
 rewrite plusS1Eq2 b in 
 saEqSb2 a b (No contra)

This allows you to ensure that plusS1Eq2 will be useful to you before you go to the trouble of proving it, and Idris will assume it’s right when checking other stuff. Idris will dutifully keep track of these skipped proofs so you can come back to them.

Finally, for practical purposes, you can just cheat:

You know part of it is true and don’t want to be bothered with a hole at the moment. I present, the con-arty method: The life changing magic of just cheating:

plusS1Eq2 : (n : Nat) -> plus n (S Z) = S n 
plusS1Eq2 n = rewrite sym (assert_total (plusS1Eq2 n)) in Refl

I’ve stated plusS1Eq2 as an axiom, effectively. This could be useful if you want to start proving things at a higher level without needing to convince Idris that other stuff is sound yet. You can always replace it with a hole later to continue working on it.