<commit_before>------------------------------------------------------------------------------
-- The map-iterate property: A property using coinduction
------------------------------------------------------------------------------

-- The map-iterate property [1]:
-- map f (iterate f x) = iterate f (f · x)

-- [1] <NAME> and <NAME>. Proof methods for corecursive
-- programs. Fundamenta Informaticae, XX:1–14, 2005.

module FOTC.Program.MapIterate.MapIterateATP where

open import FOTC.Base

open import FOTC.Data.List
open import FOTC.Data.Stream.Equality

------------------------------------------------------------------------------
-- The map-iterate property.

≈-map-iterate : (f x : D) → map f (iterate f x) ≈ iterate f (f · x)
≈-map-iterate f x = ≈-gfp₂ R (λ {xs} {ys} → helper xs ys) (x , refl , refl)
  where
  postulate
    unfoldMap : ∀ f y →
                map f (iterate f y) ≡ f · y ∷ map f (iterate f (f · y))
  {-# ATP prove unfoldMap #-}

  postulate
    unfoldIterate : ∀ f y →
                    iterate f (f · y) ≡ f · y ∷ iterate f (f · (f · y))
  {-# ATP prove unfoldIterate #-}

  -- The relation R was based on the relation used by <NAME>
  -- and <NAME>. A Tutorial on [Co-]Inductive Types in
  -- Coq. May 1998 -- August 17, 2007.
  R : D → D → Set
  R xs ys = ∃ (λ y → xs ≡ map f (iterate f y) ∧ ys ≡ iterate f (f · y))

  helper : ∀ xs ys → R xs ys → ∃ λ x' → ∃ λ xs' → ∃ λ ys' →
             R xs' ys' ∧
             xs ≡ x' ∷ xs' ∧
             ys ≡ x' ∷ ys'
  helper xs ys h = f · y
                   , map f (iterate f (f · y))
                   , iterate f (f · (f · y))
                   , ((f · y) , refl , refl)
                   , trans xs≡map (unfoldMap f y)
                   , trans ys≡iterate (unfoldIterate f y)
    where
    y : D
    y = ∃-proj₁ h
<commit_msg>Cosmetic changes.<commit_after>------------------------------------------------------------------------------
-- The map-iterate property: A property using coinduction
------------------------------------------------------------------------------

-- The map-iterate property [1]:
-- map f (iterate f x) = iterate f (f · x)

-- [1] <NAME> and <NAME>. Proof methods for corecursive
-- programs. Fundamenta Informaticae, XX:1–14, 2005.

module FOTC.Program.MapIterate.MapIterateATP where

open import FOTC.Base

open import FOTC.Data.List
open import FOTC.Data.Stream.Equality

------------------------------------------------------------------------------
-- The map-iterate property.

≈-map-iterate : ∀ f x → map f (iterate f x) ≈ iterate f (f · x)
≈-map-iterate f x = ≈-gfp₂ R helper (x , refl , refl)
  where
  postulate
    unfoldMap : ∀ f y →
                map f (iterate f y) ≡ f · y ∷ map f (iterate f (f · y))
  {-# ATP prove unfoldMap #-}

  postulate
    unfoldIterate : ∀ f y →
                    iterate f (f · y) ≡ f · y ∷ iterate f (f · (f · y))
  {-# ATP prove unfoldIterate #-}

  -- The relation R was based on the relation used by <NAME>
  -- and <NAME>. A Tutorial on [Co-]Inductive Types in
  -- Coq. May 1998 -- August 17, 2007.
  R : D → D → Set
  R xs ys = ∃ λ y → xs ≡ map f (iterate f y) ∧ ys ≡ iterate f (f · y)

  helper : ∀ {xs ys} → R xs ys → ∃ λ x' → ∃ λ xs' → ∃ λ ys' →
           R xs' ys' ∧ xs ≡ x' ∷ xs' ∧ ys ≡ x' ∷ ys'
  helper {xs} {ys} h = f · y
                     , map f (iterate f (f · y))
                     , iterate f (f · (f · y))
                     , ((f · y) , refl , refl)
                     , trans xs≡map (unfoldMap f y)
                     , trans ys≡iterate (unfoldIterate f y)
    where
    y : D
    y = ∃-proj₁ h

{'fraction_non_alphanumeric': 0.25, 'fraction_numerical': 0.010579064587973273, 'mean_word_length': 1.2484355444305382, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 11, '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': '6880229', 'n_tokens_mistral': 1379, 'n_tokens_neox': 1193, 'n_words': 525}