Skip to content

Instantly share code, notes, and snippets.

@ice1000

ice1000/N-add-comm-lf.agda

Last active April 23, 2024 02:53
Show Gist options
  • Save ice1000/e82aaaf53ba95aba7f68079907ed0479 to your computer and use it in GitHub Desktop.
Save ice1000/e82aaaf53ba95aba7f68079907ed0479 to your computer and use it in GitHub Desktop.
Download ZIP
Purely axiomatic proof of +-comm on nat in extensional type theory
Raw
N-add-comm-lf.agda
variable
A B : Set
postulate
Eq : A → A → Set
refl : (a : A) → Eq a a
rw : {x y : A} → Eq x y → (B : A → Set) → B x → B y
-- UIP missing but not needed
N : Set
Z : N
S : N → N
N-rec : (P : N → Set) → P Z → ((n : N) → P n → P (S n)) → (x : N) → P x
N-β-1 : (P : N → Set) → {a : P Z} → {b : (n : N) → P n → P (S n)} → Eq (N-rec P a b Z) a
N-β-2 : (P : N → Set) → {a : P Z} → {b : (n : N) → P n → P (S n)} → (m : N) → Eq (N-rec P a b (S m)) (b m (N-rec P a b m))
sym : {x y : A} → Eq x y → Eq y x
sym = λ z → rw z (λ z → Eq z _) (refl _)
trans : {x y z : A} → Eq x y → Eq y z → Eq x z
trans = λ z w → rw w (Eq _) z
cong : (f : A → B) → {x y : A} → Eq x y → Eq (f x) (f y)
cong f = λ z → rw z (λ w → Eq (f _) (f w)) (refl (f _))
module Version2 where
postulate
N-add : N → N → N
N-add-0 : (a : N) → Eq (N-add a Z) a
N-add-S : (a b : N) → Eq (N-add a (S b)) (S (N-add a b))
N-add-0' : (a : N) → Eq (N-add Z a) a
N-add-S' : (a b : N) → Eq (N-add (S a) b) (S (N-add a b))
N-add-comm : (a b : N) → Eq (N-add a b) (N-add b a)
N-add-comm a b = N-rec (λ x → Eq (N-add x b) (N-add b x))
(trans (N-add-0' b) (sym (N-add-0 b)))
(λ n x → trans (N-add-S' n b) (trans (cong S x) (sym (N-add-S b n)))) a
N-add-assoc : (a b c : N) → Eq (N-add a (N-add b c)) (N-add (N-add a b) c)
N-add-assoc a b c = N-rec (λ x → Eq (N-add x (N-add b c)) (N-add (N-add x b) c))
(trans (N-add-0' (N-add b c)) (sym (cong add-c (N-add-0' b))))
(λ n x → trans (N-add-S' n (N-add b c))
(trans (trans (cong S x) (sym (N-add-S' (N-add n b) c)))
(cong add-c (sym (N-add-S' n b))))) a
where add-c = λ x → N-add x c
module Version1 where
N-add : N → N → N
N-add a b = N-rec (λ _ → N) a (λ _ → S) b
N-add-comm : (a b : N) → Eq (N-add a b) (N-add b a)
N-add-comm a b = N-rec (λ a' → Eq (N-add a' b) (N-add b a'))
(trans (id1 b) (sym (jeq2 b)))
(λ n p → trans (id2 n b) (trans (cong S p) (sym (jeq1 b n)))) a
where
P = λ (_ : N) → N
jeq1 : ∀ a b → Eq (N-add a (S b)) (S (N-add a b))
jeq1 a b = N-β-2 P b
jeq2 : ∀ b → Eq (N-add b Z) b
jeq2 b = N-β-1 P
id1-lem : ∀ n → Eq (N-add Z n) n → Eq (N-add Z (S n)) (S n)
id1-lem n p = rw (sym (jeq1 Z n)) (λ x → Eq x (S n)) (cong S p)
id1 : ∀ b → Eq (N-add Z b) b
id1 b = N-rec (λ b' → Eq (N-add Z b') b') (jeq2 Z) id1-lem b
jeq3 : ∀ a → Eq (N-add (S a) Z) (S (N-add a Z))
jeq3 a = trans (jeq2 (S a)) (cong S (sym (jeq2 a)))
id2 : ∀ a b → Eq (N-add (S a) b) (S (N-add a b))
id2 a b = N-rec (λ b' → Eq (N-add (S a) b') (S (N-add a b')))
(jeq3 a) (λ n q → trans (jeq1 (S a) n) (cong S (trans q (sym (jeq1 a n))))) b
chase-2023-11-19 : (a : N) → Eq (N-add (S a) Z) (S (N-add a Z))
chase-2023-11-19 = λ a → rw (sym (N-β-1 P))
(λ x → Eq (N-rec P (S a) (λ _ → S) Z) (S x)) (N-β-1 P)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment