Struggling with rewrite tactic in Idris

Question

I'm going through Terry Tao's real analysis textbook, which builds up fundamental mathematics from the natural numbers up. By formalizing as many of the proofs as possible, I hope to familiarize myself with both Idris and dependent types.

I have defined the following datatype:

data GE: Nat -> Nat -> Type where
    Ge : (n: Nat) -> (m: Nat) -> GE n (n + m)

to represent the proposition that one natural number is greater than or equal to another.

I'm currently struggling to prove reflexivity of this relation, i.e. to construct the proof with signature

geRefl : GE n n

My first attempt was to simply try geRefl {n} = Ge n Z, but this has type Ge n (add n Z). To get this to unify with the desired signature, we obviously have to perform some kind of rewrite, presumably involving the lemma

plusZeroRightNeutral : (left : Nat) -> left + fromInteger 0 = left

My best attempt is the following:

geRefl : GE n n                                                                 
geRefl {n} = x                                                                  
    where x : GE n (n + Z)                                                      
          x = rewrite plusZeroRightNeutral n in Ge n Z 

but this does not typecheck.

Can you please give a correct proof of this theorem, and explain the reasoning behind it?

Aleris

It would be much easier to make it GE : (m : Nat) -> (n : Nat) -> GE n (m + n) instead. Then geRefl = GE Z. – Izaak

@Izaak I considered this, but it made other things harder. – Aleris

Answer 1

The first problem is superficial: you are trying to apply the rewriting at the wrong place. If you have x : GE n (n + Z), then you'll have to rewrite its type if you want to use it as the definition of geRefl : GE n n, so you'd have to write

geRefl : GE n n
geRefl {n} = rewrite plusZeroRightNeutral n in x

But that still won't work. The real problem is you only want to rewrite a part of the type GE n n: if you just rewrite it using n + 0 = n, you'd get GE (n + 0) (n + 0), which you still can't prove using Ge n 0 : GE n (n + 0).

What you need to do is use the fact that if a = b, then x : GE n a can be turned into x' : GE n b. This is exactly what the replace function in the standard library provides:

replace : (x = y) -> P x -> P y

Using this, by setting P = GE n, and using Ge n 0 : GE n (n + 0), we can write geRefl as

geRefl {n} = replace {P = GE n} (plusZeroRightNeutral n) (Ge n 0)

(note that Idris is perfectly able to infer the implicit parameter P, so it works without that, but I think in this case it makes it clearer what is happening)

Cup