# Axiomatic proofs of natural addition properties, in Idris

I'm a seasoned programmer in a variety of languages (including Haskell and some ML dialects), but i'm a complete dilettante when it comes to formal logic. I've very briefly looked at Coq, and now i'm trying to dabble in theorem proving with Idris.

In particular, before trying to use the interactive elaborator, I'd like to understand how to create simple proofs, because I had a hard time following the elaborator section of the tutorial. So, I've written the following program, that typechecks successfully:

total
project : a = b -> S a = S b
project Refl = Refl

total
sym : a = b -> b = a
sym Refl = Refl

total
transitive : a = b -> b = c -> a = c
transitive Refl Refl = Refl

total
plus_assoc : (a: Nat) -> (b: Nat) -> (c: Nat) -> a+(b+c) = (a+b)+c
plus_assoc Z     b c = Refl
plus_assoc (S a) b c = project (plus_assoc a b c)

total
plus_succ_commute : (n: Nat) -> (m: Nat) -> S n + m = n + S m
plus_succ_commute Z     m = Refl
plus_succ_commute (S n) m = project (plus_succ_commute n m)

total
plus_commutes : (n: Nat) -> (m: Nat) -> n + m = m + n
plus_commutes Z     Z     = Refl
plus_commutes Z     (S m) = project (plus_commutes Z m)
plus_commutes (S n) m     = transitive (project (plus_commutes n m)) (plus_succ_commute m n)

I'd appreciate advice on how to make things cleaner, and in particular:

• At first, I tried to write a direct proof for plus_commutes that would not involve plus_succ_commute, but alas, to no avail.

• In the second clause of plus_assoc, I tried to get rid of my definition of project by writing

plus_assoc (S a) b c = let Refl = plus_assoc a b c in Refl

Which seems to me as just substituting the definition of project into the original clause, but fails with a type error:

Type mismatch between
plus (plus a b) c = plus (plus a b) c (Type of Refl)
and
a + (b + c) = a + b + c (Expected type)

Specifically:
Type mismatch between
plus (plus a b) c
and
plus a (plus b c)

Can anyone offer insight as to why inlining this definition breaks the proof ? perhaps I ought to pass some implicits to constraint the type of the subexpression ?