<commit_before>open import Base

open import Nat

module Evens where

data Even : ℕ → Type where
  0even : Even 0
  _+2even : {n : ℕ} → Even n → Even (succ (succ n))

4even : Even 4
4even = (0even +2even) +2even

open import Logic

1odd : Even 1 → False
1odd ()

module n|n+1even where
  P = λ n → (Even n) ⊕ (Even (succ n))

  step : {n : ℕ} → P n → P (succ n)
  step (ι₁ p) = ι₂(p +2even)
  step (ι₂ p) = ι₁(p)

  thm : (n : ℕ) → P n
  thm 0 = ι₁ 0even
  thm (succ n) = step (thm n)

value : {n : ℕ} → Even n → ℕ
value 0even = 0
value (p +2even) = succ (succ (value p))

half : (n : ℕ) → Even n → ℕ
half .0 0even = 0
half (succ (succ n)) (p +2even) = succ (half n p) 

-- wrong = half 2 0even

double : ℕ → Σ ℕ Even
double 0 = [ 0 , 0even ]
double (succ n) = [ succ (succ (proj₁(double n))) , (proj₂ (double n) +2even) ]

halfdouble : ℕ → ℕ
halfdouble n = half (proj₁ (double n)) (proj₂ (double n))
<commit_msg>collatz function<commit_after>open import Base

open import Nat

module Evens where

data Even : ℕ → Type where
  0even : Even 0
  _+2even : {n : ℕ} → Even n → Even (succ (succ n))

4even : Even 4
4even = (0even +2even) +2even

open import Logic

1odd : Even 1 → False
1odd ()

module n|n+1even where
  P = λ n → (Even n) ⊕ (Even (succ n))

  step : {n : ℕ} → P n → P (succ n)
  step (ι₁ p) = ι₂(p +2even)
  step (ι₂ p) = ι₁(p)

  thm : (n : ℕ) → P n
  thm 0 = ι₁ 0even
  thm (succ n) = step (thm n)

value : {n : ℕ} → Even n → ℕ
value 0even = 0
value (p +2even) = succ (succ (value p))

evenValue : {n : ℕ} → (pf : Even n) → Even (value pf)
evenValue 0even = 0even
evenValue (pf +2even) = evenValue pf +2even

half : (n : ℕ) → Even n → ℕ
half .0 0even = 0
half (succ (succ n)) (p +2even) = succ (half n p) 

-- wrong = half 2 0even

double : ℕ → Σ ℕ Even
double 0 = [ 0 , 0even ]
double (succ n) = [ succ (succ (proj₁(double n))) , (proj₂ (double n) +2even) ]

halfdouble : ℕ → ℕ
halfdouble n = half (proj₁ (double n)) (proj₂ (double n))

module Collatz where
  open n|n+1even

  fn : {n : ℕ} → P n → ℕ
  fn (ι₁ x) = half (value x) (evenValue x)
  fn (ι₂ (x +2even)) = succ (half (value x) (evenValue x) + (value x))
{'fraction_non_alphanumeric': 0.1516431924882629, 'fraction_numerical': 0.03004694835680751, 'mean_word_length': 2.7716814159292036, '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': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4397604', 'n_tokens_mistral': 1055, 'n_tokens_neox': 967, 'n_words': 396}