How to prove the type of form (a | b) in agda?
In thoughts:
In Agda, is it possible to define a data type that has equations?
I have been playing around 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 provide an opportunity to get around this. However, you can define an abbreviation for the Int type above, which can 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 proven is this:
idempotent : (n : Int) -> normalize n \== normalize (normalize n)
When expanding cases, you get for example
idempotent (P n) = ?
The target of the hole is the type
(normalize (P n) | normalize n) \== normalize (normalize (P n) | normalize n)
And I have not seen this "|" and dont know how to create a proof of the type associated with them. The proof must match the pattern, for example
idempotent (P n) with inspect (normalize n)
... (S m) with-\== = ?
... m with-\== = ?
But here the hole for the second case still has "|" in that. So I'm a little confused.
-------- EDIT ---------------
It would be helpful to prove a simpler statement:
normLemma : (n m : NZ) -> normalize n \== P m -> normalize (S n) \== m
The proof on paper is pretty simple. Assuming the normalization n = P m, consider
normalize (S n) = case normalize n of
P k -> k
x -> S x
But the normalization n is assumed to be P m, so we normalize (S n) = k. Then k = m, since the normalization is n = P m = P k, which implies m = k. Thus, we normalize (S n) = m.
source to share
User Vitus suggested the use of conventional 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 get the desired result:
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))
those. only members of the type S (S ... (S Z)...
and P (P ... (P Z)...)
are in normal form.
And the proofs are simple enough:
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
source to share
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
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 extended version normalize (S (S m))
. Therefore, we can rewrite the context a bit:
Goal: normalize (S (S m)) ≡ S (S m)
————————————————————————————————————————————————————————————
p : normalize n ≡ S m
m : Int
n : Int
Because of the function definition normalize
normalize (S n) with normalize n
... | P m = m
... | m = S m
normalize (S n) ≡ S (normalize n)
if normalize n
does not contain P
s.
If we have an equation of the type normalize n ≡ S m
, then it is m
already normalized and does not contain P
s. But if it m
does not contain P
s, therefore and normalize m
. So we have normalize (S m) ≡ S (normalize m)
.
Let us prove a slightly 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
indicates that if m
does not contain P
s, this is true:
normalize (S (S ... (S m)...)) ≡ S (S ... (S (normalize m))...)
Here's the 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
Goal: normalize (Z ‵add‵ i) ≡ Z ‵add‵ i
————————————————————————————————————————————————————————————
i : ℕ
.w : Reveal .Data.Unit.Core.hide normalize n is Z
n : Int
those. normalize (S (S ... (S Z)...)) ≡ S (S ... (S Z)...)
... We can easily prove this:
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
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 briefly normalize (S (m ‵add‵ i)) ≡ S (m ‵add‵ i)
. Therefore, 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
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 the dual of normalize-S
and is of 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 having a type normalize (S m) ≡ S m
: normalize-S (S m) (normalize-P n q 0) i
. This expression is of exactly the type we want. Therefore 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
Problem with these holes: Agda does not see what normalize-S (S m) _ _
completes as it is S m
not syntactically less S n
. It is possible, however, to convince Agda by using informed recursion.
With all this, we can easily prove the theorem idempotent
:
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 two versions, with {-# TERMINATING #-}
and without pragma.
EDIT
idempotent
just
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
source to share