Skip to content

Instantly share code, notes, and snippets.

@flickyfrans

flickyfrans/another one

Last active August 29, 2015 14:08
Show Gist options
  • Save flickyfrans/f2c7d5413b3657a94950 to your computer and use it in GitHub Desktop.
Save flickyfrans/f2c7d5413b3657a94950 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
another one
-- This is related to http://stackoverflow.com/questions/26615082/how-does-one-prove-a-type-of-the-form-a-b-in-agda
open import Function
open import Relation.Binary.PropositionalEquality
data Int : Set where
Z : Int
S : Int -> Int
P : Int -> Int
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
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))
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
idempotent : ∀ n -> normalize (normalize n) ≡ normalize n
idempotent = idempotent' ∘ normalForm
Raw
idempotent-normalize
open import Relation.Binary.PropositionalEquality
open import Data.Nat
data Int : Set where
Z : Int
S : Int -> Int
P : Int -> Int
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
_‵add‵_ : Int -> ℕ -> Int
n ‵add‵ 0 = n
n ‵add‵ (suc i) = S (n ‵add‵ i)
_‵sub‵_ : Int -> ℕ -> Int
n ‵sub‵ 0 = n
n ‵sub‵ (suc i) = P (n ‵sub‵ 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)
inj-sub : ∀ n i -> P n ‵sub‵ i ≡ P (n ‵sub‵ i)
inj-sub n 0 = refl
inj-sub n (suc i) = cong P (inj-sub n i)
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
normalize-sub : ∀ i -> normalize (Z ‵sub‵ i) ≡ Z ‵sub‵ i
normalize-sub 0 = refl
normalize-sub (suc i) rewrite normalize-sub i with i
... | 0 = refl
... | suc _ = refl
{-# TERMINATING #-}
mutual
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-add i
normalize-S (S n) refl i | S m | [ q ] rewrite inj-add m i = normalize-S n q (suc i)
normalize-S (S n) refl i | P (S m) | [ q ] = normalize-S (S m) (normalize-P n q 0) i
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 (S m) (normalize-S n q 0) i
normalize-S (P n) () i | P _ | _
normalize-P : ∀ n {m} -> normalize n ≡ P m -> ∀ i -> normalize (m ‵sub‵ i) ≡ m ‵sub‵ i
normalize-P Z () i
normalize-P (S n) p i with normalize n | inspect normalize n
normalize-P (S n) () i | Z | _
normalize-P (S n) () i | S _ | _
normalize-P (S n) refl i | P (P m) | [ q ] = normalize-P (P m) (normalize-P n q 0) i
normalize-P (P n) p i with normalize n | inspect normalize n
normalize-P (P n) refl i | Z | _ = normalize-sub i
normalize-P (P n) refl i | S (P m) | [ q ] = normalize-P (P m) (normalize-S n q 0) i
normalize-P (P n) refl i | P m | [ q ] rewrite inj-sub m i = normalize-P n q (suc i)
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
Raw
terminating idempotent-normalize
open import Function
open import Relation.Binary.PropositionalEquality
open import Induction.WellFounded as WF
open import Data.Product
open import Data.Nat hiding (_<_)
open import Data.Nat.Properties
data Int : Set where
Z : Int
S : Int -> Int
P : Int -> Int
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
_‵add‵_ : Int -> ℕ -> Int
n ‵add‵ 0 = n
n ‵add‵ (suc i) = S (n ‵add‵ i)
_‵sub‵_ : Int -> ℕ -> Int
n ‵sub‵ 0 = n
n ‵sub‵ (suc i) = P (n ‵sub‵ 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)
inj-sub : ∀ n i -> P n ‵sub‵ i ≡ P (n ‵sub‵ i)
inj-sub n 0 = refl
inj-sub n (suc i) = cong P (inj-sub n i)
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
normalize-sub : ∀ i -> normalize (Z ‵sub‵ i) ≡ Z ‵sub‵ i
normalize-sub 0 = refl
normalize-sub (suc i) rewrite normalize-sub i with i
... | 0 = refl
... | suc _ = refl
length-Int : Int -> ℕ
length-Int Z = 0
length-Int (S n) = suc (length-Int n)
length-Int (P n) = suc (length-Int n)
_<_ : Int -> Int -> Set
_<_ = _<′_ on length-Int
<-well-founded : Well-founded _<_
<-well-founded = well-founded length-Int <-well-founded-ℕ where
open Inverse-image
open import Induction.Nat renaming (<-well-founded to <-well-founded-ℕ)
module _ {ℓ} where
open WF.All <-well-founded ℓ public renaming (wfRec to <-rec)
suc-≤′ : ∀ {n m} -> suc n ≤′ m -> n ≤′ m
suc-≤′ ≤′-refl = ≤′-step ≤′-refl
suc-≤′ (≤′-step n+m≤′p) = ≤′-step (suc-≤′ n+m≤′p)
mutual
norm-S-< : ∀ {m} n -> normalize n ≡ S m -> m < n
norm-S-< Z ()
norm-S-< (S n) p with normalize n | inspect normalize n
norm-S-< (S n) refl | Z | _ = s≤′s z≤′n
norm-S-< (S n) refl | S _ | [ q ] = s≤′s (norm-S-< n q)
norm-S-< (S n) refl | P ._ | [ q ] = ≤′-step (suc-≤′ (norm-P-< n q))
norm-S-< (P n) p with normalize n | inspect normalize n
norm-S-< (P n) () | Z | _
norm-S-< (P n) refl | S ._ | [ q ] = ≤′-step (suc-≤′ (norm-S-< n q))
norm-S-< (P n) () | P _ | _
norm-P-< : ∀ {m} n -> normalize n ≡ P m -> m < n
norm-P-< Z ()
norm-P-< (S n) p with normalize n | inspect normalize n
norm-P-< (S n) () | Z | _
norm-P-< (S n) () | S _ | _
norm-P-< (S n) refl | P ._ | [ q ] = ≤′-step (suc-≤′ (norm-P-< n q))
norm-P-< (P n) p with normalize n | inspect normalize n
norm-P-< (P n) refl | Z | _ = s≤′s z≤′n
norm-P-< (P n) refl | S ._ | [ q ] = ≤′-step (suc-≤′ (norm-S-< n q))
norm-P-< (P n) refl | P _ | [ q ] = s≤′s (norm-P-< n q)
normalized = <-rec _ go where
mutual
go : ∀ n -> (∀ p -> p < n -> _) -> (∀ {m} -> normalize n ≡ S m -> ∀ i -> _)
× (∀ {m} -> normalize n ≡ P m -> ∀ i -> _)
go n rec = go-S n rec , go-P n rec
go-S : ∀ n -> (∀ p -> p < n -> _) ->
∀ {m} -> normalize n ≡ S m -> ∀ i -> normalize (m ‵add‵ i) ≡ m ‵add‵ i
go-S Z rec () i
go-S (S n) rec p i with normalize n | inspect normalize n
go-S (S n) rec refl i | Z | _ = normalize-add i
go-S (S n) rec refl i | S m | [ q ] rewrite inj-add m i =
proj₁ (rec n ≤′-refl) q (suc i)
go-S (S n) rec refl i | P (S m) | [ q ] =
proj₁ (rec (S m) (≤′-step (norm-P-< n q))) (proj₂ (rec n ≤′-refl) q 0) i
go-S (P n) rec p i with normalize n | inspect normalize n
go-S (P n) rec () i | Z | _
go-S (P n) rec refl i | S (S m) | [ q ] =
proj₁ (rec (S m) (≤′-step (norm-S-< n q))) (proj₁ (rec n ≤′-refl) q 0) i
go-S (P n) rec () i | P _ | _
go-P : ∀ n -> (∀ p -> p < n -> _) ->
∀ {m} -> normalize n ≡ P m -> ∀ i -> normalize (m ‵sub‵ i) ≡ m ‵sub‵ i
go-P Z rec ()
go-P (S n) rec p i with normalize n | inspect normalize n
go-P (S n) rec () i | Z | _
go-P (S n) rec refl i | P (P m) | [ q ] =
proj₂ (rec (P m) (≤′-step (norm-P-< n q))) (proj₂ (rec n ≤′-refl) q 0) i
go-P (S n) rec () i | S _ | _
go-P (P n) rec p i with normalize n | inspect normalize n
go-P (P n) rec refl i | Z | _ = normalize-sub i
go-P (P n) rec refl i | S (P m) | [ q ] =
proj₂ (rec (P m) (≤′-step (norm-S-< n q))) (proj₁ (rec n ≤′-refl) q 0) i
go-P (P n) rec refl i | P m | [ q ] rewrite inj-sub m i =
proj₂ (rec n ≤′-refl) q (suc i)
idempotent : (n : Int) -> normalize (normalize n) ≡ normalize n
idempotent n with normalize n | inspect normalize n
... | Z | _ = refl
... | S _ | [ p ] = proj₁ (normalized n) p 1
... | P _ | [ p ] = proj₂ (normalized n) p 1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment