Idris proof with RHS as function definition

Question

I'm trying to get my head around some simple proofs by trying to prove the equivalence of a computational method of computing triangular numbers to the closed form of them. So far, all I've managed to achieve is this:

total 
tn_eval : (n : Nat) -> Nat
tn_eval Z = Z
tn_eval (S k)  = (S k) + tn_eval k

total 
tn_closed : (n: Nat) -> Nat
tn_closed Z = Z
tn_closed (S k) = div ((S k) * ((S k) - 1)) 2

total 
tn_closed_proof : (n : Nat) -> (tn_closed n) = (tn_eval n)
tn_closed_proof Z = ?strange_hole
tn_closed_proof (S k) = ?more_difficult_hole

However, I've got stuck as to what the possible definition of ?strange_hole should be. Inspecting the type gives:

Idris: Type of strange_hole
--------------------------------------
strange_hole : tn_closed 0 = 0

Which (as I understand it) is literally the definition of tn_closed Z, so, this should be provable simply using Refl, as tn_closed 0 is definitionally equivalent to 0.

However, this isn't right, as when I try this, I get a type error:

When checking right hand side of tn_closed_proof with expected type
        tn_closed 0 = tn_eval 0

Type mismatch between
        0 = 0 (Type of Refl)
and
        tn_closed 0 = 0 (Expected type)

Specifically:
        Type mismatch between
                0
        and
                tn_closed 0

Along with the totality warning:

Arith.tn_closed is possibly not total due to: Prelude.Nat.Nat implementation of Prelude.Interfaces.Integral

I feel like the latter might be the reason for the former, but aside from that I'm totally stuck! As I understood it, tn_closed 0 and 0 were by definition equivalent, so any proof requiring tn_closed 0 = 0 should be trivial, or provable with Refl, but it would seem that I'm wrong...

AdamHarries AdamHarries · Accepted Answer · 2019-10-01T22:36:32

As soon as I asked the question, I managed to solve it!

As far as I understand it, the issue lay in the definition of tn_closed, specifically:

tn_closed (S k) = div ((S k) * ((S k) - 1)) 2

This definition meant that Idris (for some reason) didn't understand that the division was total. Replacing this definition with the following:

tn_closed (S k) = divNatNZ ((S k) * ((S k) - 1)) 2 SIsNotZ

Gave the much more approachable hole:

Idris: Type of hole
--------------------------------------
hole : 0 = 0

This is fairly simple to solve with Refl!

Idris proof with RHS as function definition

1 Answers