open import Level
open import Data.Nat hiding (_/_)
open import Data.Nat.Properties
open import Data.Sum
open import Data.Unit
open import Data.Empty
open import Relation.Binary
open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Product
open import Relation.Binary.Structures
open import Data.Fin hiding (_+_ ; _<_ ; _≤_)
open import Function
open ≡-Reasoning renaming (begin_ to ≡begin_ ; _∎ to _≡∎)
open import Eser.Card
open import Eser.Equivalences.Notation
open import Eser.Equivalences.Properties
open import Eser.Aux
open import Eser.Signature
open import Eser.Examples.Integers.Definitions
open import Eser.Examples.Integers.DirectEncProperties
module Eser.Examples.Integers.NFLeq where
open import Eser.Signature.EnumOrderingProperties {fin 0} {fin 1} ℤSig
using (giveArgBigger)
opaque
unfolding ℤ'≃C
infix 4 _<w_
_<w_ : Rel C 0ℓ
_<w_ (w , t) (w' , t') = w < w'
𝟎 : C
𝟎 = (1 , mk-nullary Fin.zero)
𝐒 : C → C
𝐒 (wₐ , a) = (wₐ + 1 , giveArg (mk-multiary Fin.zero) a)
𝐏 : C → C
𝐏 (wₐ , a) = (wₐ + 2 , giveArg (mk-multiary $ Fin.suc Fin.zero) a)
getSP : Fin 2 → ℤ' → ℤ'
getSP Fin.zero = S
getSP (Fin.suc Fin.zero) = P
get𝐒𝐏 : Fin 2 → C → C
get𝐒𝐏 Fin.zero = 𝐒
get𝐒𝐏 (Fin.suc Fin.zero) = 𝐏
get𝐒𝐏-lemma
: (wₐ : ℕ)
→ (a : OT wₐ 0)
→ (c : Fin 2)
→ (proj₁ $ get𝐒𝐏 c (wₐ , a)) ≡ wₐ + (ℕ.suc $ cardToℕ c)
get𝐒𝐏-lemma wₐ a (Fin.zero) = refl
get𝐒𝐏-lemma wₐ a (Fin.suc Fin.zero) = refl
𝐒-monotone : (t t' : C) → t <w t' → 𝐒 t <w 𝐒 t'
𝐒-monotone t t' t<wt' = +-monoˡ-< 1 t<wt'
𝐏-monotone : (t t' : C) → t <w t' → 𝐏 t <w 𝐏 t'
𝐏-monotone t t' t<wt' = +-monoˡ-< 2 t<wt'
<w-trans : (t₁ t₂ t₃ : C) → t₁ <w t₂ → t₂ <w t₃ → t₁ <w t₃
<w-trans t₁ t₂ t₃ H K = <-trans H K
𝐒-<w-intro : (t : C) → t <w 𝐒 t
𝐒-<w-intro (wₜ , t) = n<n+1 wₜ
𝐒-<w-increasing : (t t' : C) → t <w t' → t <w 𝐒 t'
𝐒-<w-increasing t t' H = <w-trans t (𝐒 t) (𝐒 t') (𝐒-<w-intro t)
(𝐒-monotone t t' H)
𝐏-<w-intro : (t : C) → t <w 𝐏 t
𝐏-<w-intro (wₜ , t) = n<n+Sm wₜ 1
𝐏-<w-increasing : (t t' : C) → t <w t' → t <w 𝐏 t'
𝐏-<w-increasing t t' H = <w-trans t (𝐏 t) (𝐏 t') (𝐏-<w-intro t)
(𝐏-monotone t t' H)
f-pos-fixpoint
: (z : ℤ')
→ f (S z) ≡ S z
→ IsZero z ⊎ IsPos z
f-pos-fixpoint z H = caseDistinction z Sz-is-clean
where
Sz-is-clean : IsClean (S z)
Sz-is-clean = subst (λ y → IsClean y) H (f-cleans $ S z)
caseDistinction : (z : ℤ') → IsClean (S z) → IsZero z ⊎ IsPos z
caseDistinction O (inj₂ (inj₁ x)) = inj₁ tt
caseDistinction (S O) (inj₂ (inj₁ x)) = inj₂ tt
caseDistinction (S (S z)) (inj₂ (inj₁ x)) = inj₂ x
z-must-be-Pz'
: (z : ℤ')
→ (f (S z) ≢ S z)
→ f z ≡ z
→ Σ[ z' ∈ ℤ' ](z ≡ P z')
z-must-be-Pz' O H _ = ⊥-elim (H refl)
z-must-be-Pz' (S z) fSSz≢SSz fSz≡Sz = ⊥-elim $ fSSz≢SSz fSSz≡SSz
where
SSz-clean : IsClean $ S (S z)
SSz-clean = subst (λ y → IsClean y) (fSz≡Sz) (f-cleans $ S z)
fSSz≡SSz : (f $ S $ S z) ≡ (S $ S z)
fSSz≡SSz = f-fixes-on-clean-inp (S (S z)) SSz-clean
z-must-be-Pz' (P z) _ _ = (z , refl)
z-must-be-Sz'
: (z : ℤ')
→ (f (P z) ≢ P z)
→ f z ≡ z
→ Σ[ z' ∈ ℤ' ](z ≡ S z')
z-must-be-Sz' O H _ = ⊥-elim (H refl)
z-must-be-Sz' (P z) fPPz≢PPz fPz≡Pz = ⊥-elim $ fPPz≢PPz fPPz≡PPz
where
PPz-clean : IsClean $ P (P z)
PPz-clean = subst (λ y → IsClean y) (fPz≡Pz) (f-cleans $ P z)
fPPz≡PPz : (f $ P $ P z) ≡ (P $ P z)
fPPz≡PPz = f-fixes-on-clean-inp (P (P z)) PPz-clean
z-must-be-Sz' (S z) _ _ = (z , refl)
f-weight-decr
: (z : ℤ')
→ f z ≢ z
→ ψ (f z) <w ψ z
f-weight-decr O fz≢z = ⊥-elim $ fz≢z refl
f-weight-decr (S z) fSz≢Sz = case-Sz ((f z) ℤ'≟ z)
where
case-Sz : Dec (f z ≡ z) → (ψ $ f $ S z) <w ψ (S z)
case-Sz-fz≢z
: (f z ≢ z)
→ (z' : ℤ')
→ (f z ≡ z')
→ (ψ $ f $ S z) <w ψ (S z)
case-Sz-fz≡z : f z ≡ z → (ψ $ f $ S z) <w ψ (S z)
case-Sz (yes fz≡z) = case-Sz-fz≡z fz≡z
case-Sz (no fz≢z) = case-Sz-fz≢z fz≢z (f z) refl
case-Sz-fz≡z fz≡z = H₄
where
z' : ℤ'
z' = proj₁ $ z-must-be-Pz' z fSz≢Sz fz≡z
z≡Pz' : z ≡ P z'
z≡Pz' = proj₂ $ z-must-be-Pz' z fSz≢Sz fz≡z
H₁ : ψ z' <w ψ (P z')
H₁ = 𝐏-<w-intro (ψ z')
H₂ : ψ z' <w ψ (S (P z') )
H₂ = 𝐒-<w-increasing (ψ z') (ψ (P z')) H₁
K : z' ≡ f (S z)
K = ≡begin
z'
≡⟨⟩
(f-Sz $ P z')
≡⟨ cong f-Sz $ sym $ trans fz≡z z≡Pz' ⟩
(f-Sz $ f z)
≡⟨⟩
f (S z)
≡∎
H₃ : ψ z' <w ψ (S z)
H₃ = subst (λ y → ψ z' <w ψ (S y)) (sym z≡Pz') H₂
H₄ : ψ (f (S z)) <w ψ (S z)
H₄ = subst (λ y → ψ y <w ψ (S z)) K H₃
case-Sz-fz≢z H O p = subst (λ y → (ψ $ f-Sz $ y) <w ψ (S z)) (sym p)
$ 𝐒-monotone (ψ O) (ψ z) IH
where
IH : ψ O <w ψ z
IH = subst (λ y → ψ y <w ψ z) p $ f-weight-decr z H
case-Sz-fz≢z H (S z') p = subst (λ y → (ψ $ y) <w (ψ $ S z)) H₂ H₁
where
IH : ψ (S z') <w ψ z
IH = subst (λ y → ψ y <w ψ z) p $ f-weight-decr z H
H₁ : (ψ $ S $ S z') <w (ψ $ S z)
H₁ = 𝐒-monotone (ψ $ S z') (ψ z) IH
H₂ : S (S z') ≡ f (S z)
H₂ = cong f-Sz $ sym p
case-Sz-fz≢z H (P z') p = ans
where
IH : ψ (P z') <w ψ z
IH = subst (λ y → ψ y <w ψ z) p $ f-weight-decr z H
K : ψ z' <w ψ (S z)
K = <w-trans (ψ z') (ψ $ P z') (ψ $ S z)
(𝐏-<w-intro (ψ z'))
(<w-trans (ψ $ P z') (ψ z) (ψ $ S z) IH (𝐒-<w-intro (ψ z)))
ans : (ψ $ f $ S z) <w (ψ $ S z)
ans = subst (λ y → (ψ $ f-Sz y) <w (ψ $ S z)) (sym p) K
f-weight-decr (P z) fPz≢Pz = case-Pz ((f z) ℤ'≟ z)
where
case-Pz : Dec (f z ≡ z) → (ψ $ f $ P z) <w ψ (P z)
case-Pz-fz≢z
: (f z ≢ z)
→ (z' : ℤ')
→ (f z ≡ z')
→ (ψ $ f $ P z) <w ψ (P z)
case-Pz-fz≡z : f z ≡ z → (ψ $ f $ P z) <w ψ (P z)
case-Pz (yes fz≡z) = case-Pz-fz≡z fz≡z
case-Pz (no fz≢z) = case-Pz-fz≢z fz≢z (f z) refl
case-Pz-fz≡z fz≡z = H₄
where
z' : ℤ'
z' = proj₁ $ z-must-be-Sz' z fPz≢Pz fz≡z
z≡Sz' : z ≡ S z'
z≡Sz' = proj₂ $ z-must-be-Sz' z fPz≢Pz fz≡z
H₁ : ψ z' <w ψ (S z')
H₁ = 𝐒-<w-intro (ψ z')
H₂ : ψ z' <w ψ (P (S z') )
H₂ = 𝐏-<w-increasing (ψ z') (ψ (S z')) H₁
K : z' ≡ f (P z)
K = ≡begin
z'
≡⟨⟩
(f-Pz $ S z')
≡⟨ cong f-Pz $ sym $ trans fz≡z z≡Sz' ⟩
(f-Pz $ f z)
≡⟨⟩
f (P z)
≡∎
H₃ : ψ z' <w ψ (P z)
H₃ = subst (λ y → ψ z' <w ψ (P y)) (sym z≡Sz') H₂
H₄ : ψ (f (P z)) <w ψ (P z)
H₄ = subst (λ y → ψ y <w ψ (P z)) K H₃
case-Pz-fz≢z H O p = subst (λ y → (ψ $ f-Pz $ y) <w ψ (P z)) (sym p)
$ 𝐏-monotone (ψ O) (ψ z) IH
where
IH : ψ O <w ψ z
IH = subst (λ y → ψ y <w ψ z) p $ f-weight-decr z H
case-Pz-fz≢z H (P z') p = subst (λ y → (ψ $ y) <w (ψ $ P z)) H₂ H₁
where
IH : ψ (P z') <w ψ z
IH = subst (λ y → ψ y <w ψ z) p $ f-weight-decr z H
H₁ : (ψ $ P $ P z') <w (ψ $ P z)
H₁ = 𝐏-monotone (ψ $ P z') (ψ z) IH
H₂ : P (P z') ≡ f (P z)
H₂ = cong f-Pz $ sym p
case-Pz-fz≢z H (S z') p = ans
where
IH : ψ (S z') <w ψ z
IH = subst (λ y → ψ y <w ψ z) p $ f-weight-decr z H
K : ψ z' <w ψ (P z)
K = <w-trans (ψ z') (ψ $ S z') (ψ $ P z)
(𝐒-<w-intro (ψ z'))
(<w-trans (ψ $ S z') (ψ z) (ψ $ P z) IH (𝐏-<w-intro (ψ z)))
ans : (ψ $ f $ P z) <w (ψ $ P z)
ans = subst (λ y → (ψ $ f-Pz y) <w (ψ $ P z)) (sym p) K
nf'-weight-decr
: (t : C)
→ nf' t ≢ t
→ nf' t <w t
nf'-weight-decr t H = subst (λ y → nf' t <w y) (ψ∘ψ⁻¹≈id t) H''
where
z : ℤ'
z = ψ⁻¹ t
H' : f z ≢ z
H' p = H (subst (λ y → (ψ ∘ f) z ≡ y) (ψ∘ψ⁻¹≈id t) (cong ψ p))
H'' : nf' t <w ψ (ψ⁻¹ t)
H'' = f-weight-decr (ψ⁻¹ t) H'
open import Eser.Signature.EnumOrderingProperties {fin 0} {fin 1} ℤSig
using (smallerWeightSmallerIdx)
nf-leq : (n : ℕ) → nf n Data.Nat.≤ n
nf-leq n = nf-leq-sublemma (nf n Data.Nat.≟ n)
where
nf-leq-sublemma : Dec (nf n ≡ n) → nf n ≤ n
nf-leq-sublemma (yes p) = ≡→≤ p
nf-leq-sublemma (no nfn≢n) = <⇒≤ ans
where
wₐ : ℕ
wₐ = proj₁ $ nf' $ φ⁻¹ n
a : ClosedTerms {fin 1} {fin 2} ℤSig wₐ
a = proj₂ $ nf' $ φ⁻¹ n
wₓ : ℕ
wₓ = proj₁ $ φ⁻¹ n
x : ClosedTerms {fin 1} {fin 2} ℤSig wₓ
x = proj₂ $ φ⁻¹ n
nfn≢φφ⁻¹n : nf n ≢ (φ ∘ φ⁻¹) n
nfn≢φφ⁻¹n nfn≡φφ⁻¹n = nfn≢n H
where
H : nf n ≡ n
H = subst (λ y → nf n ≡ y) (φ∘φ⁻¹≈id n) nfn≡φφ⁻¹n
nf'φ⁻¹n≢φ⁻¹n : (nf' $ φ⁻¹ n) ≢ (φ⁻¹ n)
nf'φ⁻¹n≢φ⁻¹n p = H $ cong φ p
where
H : (φ ∘ nf' ∘ φ⁻¹) n ≢ (φ ∘ φ⁻¹) n
H = nfn≢φφ⁻¹n
nf'n<φφ⁻¹n : nf n < (φ ∘ φ⁻¹) n
nf'n<φφ⁻¹n = smallerWeightSmallerIdx {wₐ} {wₓ} a x
(nf'-weight-decr (φ⁻¹ n) nf'φ⁻¹n≢φ⁻¹n)
ans : nf n < n
ans = subst (λ y → nf n < y) (φ∘φ⁻¹≈id n) nf'n<φφ⁻¹n