Fighting rewriting tactics in Idris

Question

I am experiencing a real Terry Tao analysis tutorial that bases fundamental mathematics on natural numbers. Making as much evidence as possible, I hope to get acquainted with Idris and dependent types.

I defined the following data type:

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

to present a statement that one natural number is greater than or equal to another.

I am currently trying to prove the reflexivity of this relationship, i.e. build evidence with signature

 geRefl : GE nn 

My first attempt was to simply try geRefl {n} = Ge n Z , but this is of type Ge n (add n Z) . In order to achieve unification with the desired signature, we obviously must carry out some correspondence, presumably including the lemma

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

My best attempt is as follows:

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

but it does not look.

Could you give a correct proof of this theorem and explain the reasons for this?

Answer 1

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

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

But it still won’t work. The real problem is that you only want to rewrite a part like GE nn : if you just rewrite it with n + 0 = n , you will get GE (n + 0) (n + 0) , which you still cannot use using Ge n 0 : GE n (n + 0) .

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

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

Using this, 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 quite capable of inferring the implicit parameter P , so it works without it, but I think in this case it clarifies what happens)