<commit_before>------------------------------------------------------------------------------
-- Natural numbers properties using Agsy
------------------------------------------------------------------------------

module Agsy.Nat where

open import Data.Nat

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

------------------------------------------------------------------------------

+-assoc : ∀ m n o → m + n + o ≡ m + (n + o)  -- via Agsy {-c}
+-assoc zero    n o = refl
+-assoc (suc m) n o = cong suc (+-assoc m n o)

x+Sy≡S[x+y] : ∀ m n → m + suc n ≡ suc (m + n)  -- via Agsy {-c}
x+Sy≡S[x+y] zero    n = refl
x+Sy≡S[x+y] (suc m) n = cong suc (x+Sy≡S[x+y] m n)

0+x≡x+0 : ∀ x → 0 + x ≡ x + 0  -- via Agsy {-c}
0+x≡x+0 zero    = refl
0+x≡x+0 (suc n) = cong suc (0+x≡x+0 n)

+-comm : ∀ m n → m + n ≡ n + m  -- via Agsy {-c -m}
+-comm zero    n = 0+x≡x+0 n
+-comm (suc m) n =
  begin
    suc (m + n) ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m) ≡⟨ sym (x+Sy≡S[x+y] n m) ⟩
    n + suc m
  ∎<commit_msg>Modified an Agsy proof (it is more similar to the PA proof).<commit_after>------------------------------------------------------------------------------
-- Natural numbers properties using Agsy
------------------------------------------------------------------------------

module Agsy.Nat where

open import Data.Nat

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

------------------------------------------------------------------------------

+-rightIdentity : ∀ n → n + zero ≡ n  -- via Agsy {-c}
+-rightIdentity zero    = refl
+-rightIdentity (suc n) = cong suc (+-rightIdentity n)

+-assoc : ∀ m n o → m + n + o ≡ m + (n + o)  -- via Agsy {-c}
+-assoc zero    n o = refl
+-assoc (suc m) n o = cong suc (+-assoc m n o)

x+Sy≡S[x+y] : ∀ m n → m + suc n ≡ suc (m + n)  -- via Agsy {-c}
x+Sy≡S[x+y] zero    n = refl
x+Sy≡S[x+y] (suc m) n = cong suc (x+Sy≡S[x+y] m n)

+-comm : ∀ m n → m + n ≡ n + m  -- via Agsy {-c -m}
+-comm zero    n = sym (+-rightIdentity n)
+-comm (suc m) n =
  begin
    suc (m + n) ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m) ≡⟨ sym (x+Sy≡S[x+y] n m) ⟩
    n + suc m
  ∎
{'fraction_non_alphanumeric': 0.3658878504672897, 'fraction_numerical': 0.005607476635514018, 'mean_word_length': 1.195897435897436, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 7, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3901926', 'n_tokens_mistral': 846, 'n_tokens_neox': 814, 'n_words': 302}