How does one prove a type of the form (a | b) in agda?

Question

In thinking about:

In Agda is it possible to define a datatype that has equations?

I was playing with the following datatype:

data Int : Set where
    Z : Int
    S : Int -> Int
    P : Int -> Int

The above is a poor definition of Integers, and the answers in the above give a way around this. However, one can define a reduction on the above Int type that might be useful.

normalize : Int -> Int
normalize Z = Z
normalize (S n) with normalize n
... | P m = m
... | m = S m
normalize (P n) with normalize n
... | S m = m
... | m = P m

The thing that needs to be proved is:

idempotent : (n : Int) -> normalize n \== normalize (normalize n)

When you expand the cases out, you get for example

idempotent (P n) = ? 

The goal for the hole has type

(normalize (P n) | normalize n) \== normalize (normalize (P n) | normalize n)

And I haven't seen this "|" before, nor do I know how to produce a proof of a type involving them. The proof needs to pattern match,for example,

idempotent (P n) with inspect (normalize n)
... (S m) with-\== = ?
... m with-\== = ?

But here the hole for the second case still has a "|" in it. So I am a bit confused.

-------- EDIT ---------------

It would be helpful to prove a simpler statement:

normLemma : (n m : NZ) -> normalize n \== P m -> normalize (S n) \== m

The "on paper" proof is rather straightforward. Assuming normalize n = P m, consider

normalize (S n) = case normalize n of
  P k -> k
  x -> S x

But normalize n is assumed to be P m, hence normalize (S n) = k. Then k = m, since normalize n = P m = P k which implies m = k. Thus normalize (S n) = m.

Answer 1

User Vitus proposed to use normal forms.

If we have these two functions:

normalForm : ∀ n -> NormalForm (normalize n)
idempotent' : ∀ {n} -> NormalForm n -> normalize n ≡ n

then we can easily compose them to obtain the result we need:

idempotent : ∀ n -> normalize (normalize n) ≡ normalize n
idempotent = idempotent' ∘ normalForm

Here is the definition of normal forms:

data NormalForm : Int -> Set where
  NZ  : NormalForm Z
  NSZ : NormalForm (S Z)
  NPZ : NormalForm (P Z)
  NSS : ∀ {n} -> NormalForm (S n) -> NormalForm (S (S n))
  NPP : ∀ {n} -> NormalForm (P n) -> NormalForm (P (P n))

I.e. only terms like S (S ... (S Z)... and P (P ... (P Z)...) are in the normal form.

And proofs are rather straightforward:

normalForm : ∀ n -> NormalForm (normalize n)
normalForm  Z    = NZ
normalForm (S n) with normalize n | normalForm n
... | Z    | nf     = NSZ
... | S  _ | nf     = NSS nf
... | P ._ | NPZ    = NZ
... | P ._ | NPP nf = nf
normalForm (P n) with normalize n | normalForm n
... | Z    | nf     = NPZ
... | S ._ | NSZ    = NZ
... | S ._ | NSS nf = nf
... | P  _ | nf     = NPP nf

idempotent' : ∀ {n} -> NormalForm n -> normalize n ≡ n
idempotent'  NZ     = refl
idempotent'  NSZ    = refl
idempotent'  NPZ    = refl
idempotent' (NSS p) rewrite idempotent' p = refl
idempotent' (NPP p) rewrite idempotent' p = refl

The whole code: https://gist.github.com/flickyfrans/f2c7d5413b3657a94950#file-another-one

Answer 2

idempotent : (n : Int) -> normalize (normalize n) ≡ normalize n
idempotent  Z    = refl
idempotent (S n) with normalize n | inspect normalize n
... | Z   |   _   = refl
... | S m | [ p ] = {!!}
... | P m | [ p ] = {!!}

Context in the first hole is

Goal: (normalize (S (S m)) | (normalize (S m) | normalize m)) ≡
      S (S m)
————————————————————————————————————————————————————————————
p : normalize n ≡ S m
m : Int
n : Int

(normalize (S (S m)) | (normalize (S m) | normalize m)) ≡ S (S m) is just an expanded version of normalize (S (S m)). So we can rewrite the context a bit:

Goal: normalize (S (S m)) ≡ S (S m)
————————————————————————————————————————————————————————————
p : normalize n ≡ S m
m : Int
n : Int

Due to the definition of the normalize function

normalize (S n) with normalize n
... | P m = m
... | m = S m

normalize (S n) ≡ S (normalize n), if normalize n doesn't contain Ps.

If we have an equation like normalize n ≡ S m, than m is already normalized and doesn't contain Ps. But if m doesn't contain Ps, so and normalize m. So we have normalize (S m) ≡ S (normalize m).

Let's prove a little more general lemma:

normalize-S : ∀ n {m} -> normalize n ≡ S m -> ∀ i -> normalize (m ‵add‵ i) ≡ m ‵add‵ i

where ‵add‵ is

_‵add‵_ : Int -> ℕ -> Int
n ‵add‵  0      = n
n ‵add‵ (suc i) = S (n ‵add‵ i)

normalize-S states, that if m doesn't contain Ps, than this holds:

normalize (S (S ... (S m)...)) ≡ S (S ... (S (normalize m))...)

Here is a proof:

  normalize-S : ∀ n {m} -> normalize n ≡ S m -> ∀ i -> normalize (m ‵add‵ i) ≡ m ‵add‵ i
  normalize-S  Z    ()    i
  normalize-S (S n) p     i with normalize n | inspect normalize n
  normalize-S (S n) refl  i | Z       |   _   = {!!}
  normalize-S (S n) refl  i | S m     | [ q ] = {!!}
  normalize-S (S n) refl  i | P (S m) | [ q ] = {!!}
  normalize-S (P n) p     i with normalize n | inspect normalize n
  normalize-S (P n) ()    i | Z       |   _     
  normalize-S (P n) refl  i | S (S m) | [ q ] = {!!}
  normalize-S (P n) ()    i | P _     |   _

Context in the first hole is

Goal: normalize (Z ‵add‵ i) ≡ Z ‵add‵ i
————————————————————————————————————————————————————————————
i  : ℕ
.w : Reveal .Data.Unit.Core.hide normalize n is Z
n  : Int

I.e. normalize (S (S ... (S Z)...)) ≡ S (S ... (S Z)...). We can easily prove it:

normalize-add : ∀ i -> normalize (Z ‵add‵ i) ≡ Z ‵add‵ i
normalize-add  0      = refl
normalize-add (suc i) rewrite normalize-add i with i
... | 0     = refl
... | suc _ = refl

So we can fill the first hole with normalize-add i.

Context in the second hole is

Goal: normalize (S m ‵add‵ i) ≡ S m ‵add‵ i
————————————————————————————————————————————————————————————
i : ℕ
q : .Data.Unit.Core.reveal (.Data.Unit.Core.hide normalize n) ≡ S m
m : Int
n : Int

While normalize-S n q (suc i) has this type:

(normalize (S (m ‵add‵ i)) | normalize (m ‵add‵ i)) ≡ S (m ‵add‵ i)

Or, shortly, normalize (S (m ‵add‵ i)) ≡ S (m ‵add‵ i). So we need to replace S m ‵add‵ i with S (m ‵add‵ i):

inj-add : ∀ n i -> S n ‵add‵ i ≡ S (n ‵add‵ i)
inj-add n  0      = refl
inj-add n (suc i) = cong S (inj-add n i)

And now we can write

  normalize-S (S n) refl  i | S m | [ q ] rewrite inj-add m i = normalize-S n q (suc i)

Context in the third hole is

Goal: normalize (m ‵add‵ i) ≡ m ‵add‵ i
————————————————————————————————————————————————————————————
i : ℕ
q : .Data.Unit.Core.reveal (.Data.Unit.Core.hide normalize n) ≡
    P (S m)
m : Int
n : Int

normalize-P n q 0 gives us normalize (S m) ≡ S m where normalize-P is dual of normalize-S and has this type:

  normalize-P : ∀ n {m} -> normalize n ≡ P m -> ∀ i -> normalize (m ‵sub‵ i) ≡ m ‵sub‵ i

We can apply normalize-S to something, that has type normalize (S m) ≡ S m: normalize-S (S m) (normalize-P n q 0) i. This expression has precisely the type we want. So we can write

  normalize-S (S n) refl  i | P (S m) | [ q ] = normalize-S (S m) (normalize-P n q 0) i

The fourth hole is similar to the third:

  normalize-S (P n) refl  i | S (S m) | [ q ] = normalize-S (S m) (normalize-S n q 0) i

There is a problem with this holes: Agda doesn't see, that normalize-S (S m) _ _ terminates, since S m is not syntactically smaller than S n. It's possible however to convience Agda by using well-founded recursion.

Having all this stuff we can easily proof the idempotent theorem:

idempotent : (n : Int) -> normalize (normalize n) ≡ normalize n
idempotent  Z    = refl
idempotent (S n) with normalize n | inspect normalize n
... | Z   |   _   = refl
... | S m | [ p ] = normalize-S n p 2
... | P m | [ p ] = normalize-P n p 0
idempotent (P n) with normalize n | inspect normalize n
... | Z   |   _   = refl
... | S m | [ p ] = normalize-S n p 0
... | P m | [ p ] = normalize-P n p 2

Here is the code: https://gist.github.com/flickyfrans/f2c7d5413b3657a94950 There are both versions: with the {-# TERMINATING #-} pragma and without.

EDIT

idempotent is simply

idempotent : ∀ n -> normalize (normalize n) ≡ normalize n
idempotent n with normalize n | inspect normalize n
... | Z   |   _   = refl
... | S _ | [ p ] = normalize-S n p 1
... | P _ | [ p ] = normalize-P n p 1