Predicative Arithmetic

PredArith.agda

module PredArith where

data void : Set where

abort : {A : Set} → void → A
abort ()

postulate
  ι : Set

data _==_ : ι → ι → Set where
  refl : {a : ι} → a == a

data _∨_ (A : Set) (B : Set) : Set where
  inl : A → A ∨ B
  inr : B → A ∨ B

record _⇔_ (A : Set) (B : Set) : Set where
  field
   ⇔fore : A → B
   ⇔back : B → A
open _⇔_

record ex (P : ι → Set) : Set where
  constructor exwit
  field
    w : ι
    p : P w

∃-syntax = ex
infix 5 ∃-syntax
syntax ∃-syntax (λ x → Bx) = ∃ x , Bx

¬ : Set → Set
¬ A = A → void

_≠_ : ι → ι → Set
x ≠ y = ¬ (x == y)

infix 10 _==_
infix 6 _∨_
infix 5 _⇔_
infix 10 _≠_
infix 30 _*_
infix 20 _+_
infix 10 _≤_

conv : {a b : ι} (P : ι → Set) → a == b → P a → P b
conv P refl q = q

==trans : {a b c : ι} → a == b → b == c → a == c
==trans refl refl = refl

==sym : {a b : ι} → a == b → b == a
==sym refl = refl

postulate
  O : ι
  S : ι → ι
  _+_ : ι → ι → ι
  _*_ : ι → ι → ι
  a3,1 : {x : ι} → S x ≠ O
  a3,2 : {x y : ι} → S x == S y → x == y
  a3,3 : {x : ι} → x + O == x
  a3,4 : {x y : ι} → x + (S y) == S (x + y)
  a3,5 : {x : ι} → x * O == O
  a3,6 : {x y : ι} → x * (S y) == x * y + x
  aR : (x : ι) → x == O ∨ (∃ y , S y == x)

cong : {a b : ι} (f : ι → ι) → a == b → f a == f b
cong f refl = refl

P : ι → ι
P x with aR x
P x | inl t = O
P x | inr (exwit w p) = w

postulate
  a3,8 : {x y z : ι} → (x + y) + z == x + (y + z)
  a3,9 : {x y z : ι} → x * (y + z) == x * y + x * z
  a3,10 : {x y z : ι} → (x * y) * z == x * (y * z)
  a3,11 : {x y : ι} → x + y == y + x
  a3,12 : {x y : ι} → x * y == y * x

_≤_ : ι → ι → Set
x ≤ y = ∃ z , x + z == y

thm4,2a : {x : ι} → O ≤ x
thm4,2a {x} = exwit x (==trans a3,11 a3,3)

thm4,2b : {x : ι} → x ≤ x
thm4,2b = exwit O a3,3

thm4,2c : {x : ι} → x ≤ S x
thm4,2c = exwit (S O) (==trans a3,4 (cong S a3,3))

succ-pred-lemma : {x y : ι} → (S y == x) →  x == S (P x)
succ-pred-lemma {x} q with aR x
succ-pred-lemma {x} q | inl refl = abort (a3,1 q)
succ-pred-lemma {x} q | inr (exwit w p) = ==sym p

thm4,3 : {x : ι} → x ≤ O → x == O
thm4,3 (exwit w p)     with aR w
thm4,3 (exwit w p)     | inl refl = ==trans (==sym a3,3) p
thm4,3 {x} (exwit z p) | inr (exwit y p₁) = abort (a3,1 lemma) where
   lemma : S (x + P z) == O
   lemma = ==trans (==sym a3,4) (conv (λ z → x + z == O) (succ-pred-lemma p₁) p)

thm4,4 : {x y : ι} → y ≤ S x ⇔ y ≤ x ∨ y == S x
thm4,4 = record { ⇔fore = fore ; ⇔back = back } where
  fore : {x y : ι} → y ≤ S x → y ≤ x ∨ y == S x
  fore         (exwit z p)  with aR z
  fore         (exwit .O p) | inl refl = inr (==trans (==sym a3,3) p)
  fore {x} {y} (exwit z p)  | inr (exwit w p₁) = inl (exwit w (a3,2 (==trans (==sym a3,4) step))) where
    step : (y + S w) == S x
    step = conv (λ z → y + z == S x) (==sym p₁) p
  back : {x y : ι} → y ≤ x ∨ y == S x → y ≤ S x
  back (inl (exwit z p)) = exwit (S z) (==trans a3,4 (cong S p))
  back (inr refl) = thm4,2b

thm4,5 : {x y z : ι} → x ≤ y → y ≤ z → x ≤ z
thm4,5 (exwit w refl) (exwit w' refl) = exwit (w + w') (==sym a3,8)

-- thm4,6 : {x : ι} → P x ≤ x
-- thm4,6 = {!!}

thm4,7 : {x y z : ι} → x ≤ y → z + x ≤ z + y
thm4,7 (exwit u p) = exwit u (==trans a3,8 (cong (λ w → _ + w) p))

-- thm4,8 : {x y z : ι} → x ≤ y → z * x ≤ z * y
-- thm4,8 = {!!}

postulate
  C : ι → Set

C¹ : ι → Set
C¹ x = {y : ι} → y ≤ x → C y

C² : ι → Set
C² x = {y : ι} → C¹ y → C¹ (y + x)

C³ : ι → Set
C³ x = {y : ι} → C² y → C² (y * x)

module REL (c0 : C O) (cs : {x : ι} → C x → C (S x)) where
  d1 : {x : ι} → C¹ x → C x
  d1 pc1 = pc1 thm4,2b

  d2 : C¹ O
  d2 le = conv C (==sym (thm4,3 le)) c0

  d3 : {x : ι} → C¹ x → C¹ (S x)
  d3 pc1 le with (thm4,4 .⇔fore le)
  d3 pc1 le | inl le' = pc1 le'
  d3 pc1 le | inr t = conv C (==sym t) (cs (d1 pc1))

  d4 : {x u : ι} → C¹ x → u ≤ x → C¹ u
  d4 pc1 le1 le2 = pc1 (thm4,5 le2 le1)

  d5 : {x : ι} → C² x → C¹ x
  d5 pc2 = conv C¹ (==trans a3,11 a3,3) (pc2 d2)

  d6 : C² O
  d6 pc1 ple = pc1 (conv (λ w → _ ≤ w) a3,3 ple)

  d7 : {x : ι} → C² x → C² (S x)
  d7 pc2 pc1 = conv C¹ (==sym a3,4) (d3 (pc2 pc1))

  d8 : {x u : ι} → C² x → u ≤ x → C² u
  d8 pc2 ple pc1 = d4 (pc2 pc1) (thm4,7 ple)

  d9 : {x₁ x₂ : ι} → C² x₁ → C² x₂ → C² (x₁ + x₂)
  d9 pc2₁ pc2₂ pc1 = conv C¹ a3,8 (pc2₂ (pc2₁ pc1))