2
\$\begingroup\$

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 ?

\$\endgroup\$

1 Answer 1

0
\$\begingroup\$

Inlining the second clause fails because you're shadowing Refl.

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

just reduces to

plus_assoc (S a) b c = plus_assoc a b c

\$\endgroup\$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.