<commit_before>------------------------------------------------------------------------------
-- Arithmetic properties (using induction on the LTC natural numbers)
------------------------------------------------------------------------------

module LTC.Data.Nat.PropertiesByInduction where

open import LTC.Minimal

open import LTC.Data.Nat

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

-- Usually our proofs use pattern matching instead of the induction
-- principle associated with the LTC natural numbers. The following
-- example shows a proof using it.
+-assoc : {m n o : D} → N m → N n → N o → (m + n) + o ≡ m + (n + o)
+-assoc {m} {n} {o} Nm Nn No = indN P P0 iStep Nm
  where
    P : D → Set
    P i = i + n + o ≡ i + (n + o)

    postulate
      P0 : zero + n + o ≡ zero + (n + o)
    {-# ATP prove P0 #-} -- We use the ATP systems to prove the base case.

    postulate
      iStep : {i : D} → N i →
              i + n + o ≡ i + (n + o) → -- IH.
              succ i + n + o ≡ succ i + (n + o)
    {-# ATP prove iStep #-} -- We use the ATP systems to prove the
                            -- induction step.<commit_msg>Added an example.<commit_after>------------------------------------------------------------------------------
-- Arithmetic properties (using induction on the LTC natural numbers)
------------------------------------------------------------------------------

module LTC.Data.Nat.PropertiesByInduction where

open import LTC.Minimal

open import LTC.Data.Nat

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

-- Usually our proofs use pattern matching instead of the induction
-- principle associated with the LTC natural numbers. The following
-- example shows a proof using it.

-- Proof without use definitions
+-assocND : {m n o : D} → N m → N n → N o → m + n + o ≡ m + (n + o)
+-assocND {n = n} {o} Nm _ _ = indN P P0 iStep Nm
  where
    P : D → Set
    P i = i + n + o ≡ i + (n + o)

    postulate
      P0 : zero + n + o ≡ zero + (n + o)
    {-# ATP prove P0 #-} -- We use the ATP systems to prove the base case.

    postulate
      iStep : {i : D} → N i →
              i + n + o ≡ i + (n + o) → -- IH.
              succ i + n + o ≡ succ i + (n + o)
    {-# ATP prove iStep #-} -- We use the ATP systems to prove the
                            -- induction step.

-- Proof using definitions
+-assocD : {m n o : D} → N m → N n → N o → m + n + o ≡ m + (n + o)
+-assocD {n = n} {o} Nm _ _ = indN P P0 iStep Nm
  where
    P : D → Set
    P i = i + n + o ≡ i + (n + o)
    {-# ATP definition P #-}

    postulate
      P0 : P zero
    {-# ATP prove P0 #-} -- We use the ATP systems to prove the base case.

    postulate
      iStep : {i : D} → N i → P i → P (succ i)
    {-# ATP prove iStep #-} -- We use the ATP systems to prove the
                            -- induction step.
{'fraction_non_alphanumeric': 0.26428818843089713, 'fraction_numerical': 0.0031174229303775544, 'mean_word_length': 1.1345158906134516, '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': 13, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4111526', 'n_tokens_mistral': 893, 'n_tokens_neox': 846, 'n_words': 405}