<commit_before>module Syntactic.Changes where

-- TERMS that operate on CHANGES
--
-- This module defines terms that correspond to the basic change
-- operations, as well as some other helper terms.

open import Syntactic.Types
open import Syntactic.Contexts Type
open import Syntactic.Terms.Total

open import Changes

_and_ : ∀ {Γ} → Term Γ bool → Term Γ bool → Term Γ bool
a and b = if a b false

!_ : ∀ {Γ} → Term Γ bool → Term Γ bool
! x = if x false true

-- Term xor
_xor-term_ : ∀ {Γ} → Term Γ bool → Term Γ bool → Term Γ bool
a xor-term b = if a (! b) b

diff-term : ∀ {τ Γ} → Term Γ τ → Term Γ τ → Term Γ (Δ-Type τ)

-- XXX: to finish this, we just need to call lift-term, like in
-- derive-term. Should be easy, just a bit boring.
-- Other problem: in fact, Δ t is not the nil change of t, in this context. That's a problem.
apply-pure-term : ∀ {τ Γ} → Term Γ (Δ-Type τ ⇒ τ ⇒ τ)
apply-pure-term {bool} = abs (abs (var this xor-term var (that this)))

apply-pure-term {τ₁ ⇒ τ₂} {Γ} =
-- λdf. λf.  λx.            apply          (          df                       x          (x ⊖ x))                             (     f                x        )
   abs (abs (abs (app (app apply-pure-term (app (app (var (that (that this))) (var this)) (diff-term (var this) (var this)))) (app (var (that this)) (var this)))))
--abs (abs (abs (app (app apply-compose-term (app (var (that (that this))) (var this))) (app (var (that this)) (var this)))))


apply-term : ∀ {τ Γ} → Term Γ (Δ-Type τ) → Term Γ τ → Term Γ τ
apply-term {τ ⇒ τ₁} = λ df f → app (app apply-pure-term df) f
apply-term {bool} = _xor-term_

diff-term {τ ⇒ τ₁} =
  λ f₁ f₂ →
  -- The following can be written as:
  -- * Using Unicode symbols for change operations:
  -- λ x dx. (f1 (dx ⊕ x)) ⊝ (f2 x)
  -- * In lambda calculus with names:
  --λx.  λdx. diff           (     f₁                   (apply      dx         x))                 (f₂                        x)
  -- * As a deBrujin-encoded term in Agda:
    abs (abs (diff-term {τ₁} (app (weaken ≼-in-body f₁) (apply-term (var this) (var (that this)))) (app (weaken ≼-in-body f₂) (var (that this)))))
  where
    ≼-in-body = drop (Δ-Type τ) • (drop τ • ≼-refl)

diff-term {bool} = _xor-term_

-- Derived CONGRUENCE RULES
module _ where
  open import Denotational.Equivalence

  _≈-and_ : ∀ {Γ} {t₁ t₂ t₃ t₄ : Term Γ bool} →
    t₁ ≈ t₂ → t₃ ≈ t₄ → (t₁ and t₃) ≈ (t₂ and t₄)
  _≈-and_ ≈₁ ≈₂ = ≈-if ≈₁ ≈₂ ≈-false

  ≈-!_ : ∀ {Γ} {t₁ t₂ : Term Γ bool} →
    t₁ ≈ t₂ → ! t₁ ≈ ! t₂
  ≈-!_ ≈₁ = ≈-if ≈₁ ≈-false ≈-true

  _≈-xor-term_ : ∀ {Γ} {t₁ t₂ t₃ t₄ : Term Γ bool} →
    t₁ ≈ t₂ → t₃ ≈ t₄ → (t₁ xor-term t₃) ≈ (t₂ xor-term t₄)
  _≈-xor-term_ ≈₁ ≈₂ = ≈-if ≈₁ (≈-! ≈₂) ≈₂
<commit_msg>Prove congruence for diff-term and apply-term.<commit_after>module Syntactic.Changes where

-- TERMS that operate on CHANGES
--
-- This module defines terms that correspond to the basic change
-- operations, as well as some other helper terms.

open import Syntactic.Types
open import Syntactic.Contexts Type
open import Syntactic.Terms.Total

open import Changes

_and_ : ∀ {Γ} → Term Γ bool → Term Γ bool → Term Γ bool
a and b = if a b false

!_ : ∀ {Γ} → Term Γ bool → Term Γ bool
! x = if x false true

-- Term xor
_xor-term_ : ∀ {Γ} → Term Γ bool → Term Γ bool → Term Γ bool
a xor-term b = if a (! b) b

diff-term : ∀ {τ Γ} → Term Γ τ → Term Γ τ → Term Γ (Δ-Type τ)

-- XXX: to finish this, we just need to call lift-term, like in
-- derive-term. Should be easy, just a bit boring.
-- Other problem: in fact, Δ t is not the nil change of t, in this context. That's a problem.
apply-pure-term : ∀ {τ Γ} → Term Γ (Δ-Type τ ⇒ τ ⇒ τ)
apply-pure-term {bool} = abs (abs (var this xor-term var (that this)))

apply-pure-term {τ₁ ⇒ τ₂} {Γ} =
-- λdf. λf.  λx.            apply          (          df                       x          (x ⊖ x))                             (     f                x        )
   abs (abs (abs (app (app apply-pure-term (app (app (var (that (that this))) (var this)) (diff-term (var this) (var this)))) (app (var (that this)) (var this)))))
--abs (abs (abs (app (app apply-compose-term (app (var (that (that this))) (var this))) (app (var (that this)) (var this)))))


apply-term : ∀ {τ Γ} → Term Γ (Δ-Type τ) → Term Γ τ → Term Γ τ
apply-term {τ ⇒ τ₁} = λ df f → app (app apply-pure-term df) f
apply-term {bool} = _xor-term_

diff-term {τ ⇒ τ₁} =
  λ f₁ f₂ →
  -- The following can be written as:
  -- * Using Unicode symbols for change operations:
  -- λ x dx. (f1 (dx ⊕ x)) ⊝ (f2 x)
  -- * In lambda calculus with names:
  --λx.  λdx. diff           (     f₁                   (apply      dx         x))                 (f₂                        x)
  -- * As a deBrujin-encoded term in Agda:
    abs (abs (diff-term {τ₁} (app (weaken ≼-in-body f₁) (apply-term (var this) (var (that this)))) (app (weaken ≼-in-body f₂) (var (that this)))))
  where
    ≼-in-body = drop (Δ-Type τ) • (drop τ • ≼-refl)

diff-term {bool} = _xor-term_

-- Derived CONGRUENCE RULES
module _ where
  open import Denotational.Equivalence

  _≈-and_ : ∀ {Γ} {t₁ t₂ t₃ t₄ : Term Γ bool} →
    t₁ ≈ t₂ → t₃ ≈ t₄ → (t₁ and t₃) ≈ (t₂ and t₄)
  _≈-and_ ≈₁ ≈₂ = ≈-if ≈₁ ≈₂ ≈-false

  ≈-!_ : ∀ {Γ} {t₁ t₂ : Term Γ bool} →
    t₁ ≈ t₂ → ! t₁ ≈ ! t₂
  ≈-!_ ≈₁ = ≈-if ≈₁ ≈-false ≈-true

  _≈-xor-term_ : ∀ {Γ} {t₁ t₂ t₃ t₄ : Term Γ bool} →
    t₁ ≈ t₂ → t₃ ≈ t₄ → (t₁ xor-term t₃) ≈ (t₂ xor-term t₄)
  _≈-xor-term_ ≈₁ ≈₂ = ≈-if ≈₁ (≈-! ≈₂) ≈₂

  ≈-diff-term : ∀ {τ Γ} {t₁ t₂ t₃ t₄ : Term Γ τ} →
    t₁ ≈ t₂ → t₃ ≈ t₄ → diff-term t₁ t₃ ≈ diff-term t₂ t₄
  ≈-diff-term {τ₁ ⇒ τ₂} ≈₁ ≈₂ =
    ≈-abs (≈-abs
      (≈-diff-term
        (≈-app (≈-weaken Γ″ ≈₁) ≈-refl)
        (≈-app (≈-weaken Γ″ ≈₂) ≈-refl)))
    where
      Γ″ = drop (Δ-Type τ₁) • (drop τ₁ • ≼-refl)
  ≈-diff-term {bool} ≈₁ ≈₂ = ≈₁ ≈-xor-term ≈₂

  ≈-apply-term : ∀ {τ Γ} {t₁ t₂ : Term Γ (Δ-Type τ)} {t₃ t₄ : Term Γ τ} →
    t₁ ≈ t₂ → t₃ ≈ t₄ → apply-term t₁ t₃ ≈ apply-term t₂ t₄
  ≈-apply-term {τ₁ ⇒ τ₂} ≈₁ ≈₂ = ≈-app (≈-app ≈-refl ≈₁) ≈₂
  ≈-apply-term {bool} ≈₁ ≈₂ = ≈₁ ≈-xor-term ≈₂

{'fraction_non_alphanumeric': 0.16043046357615895, 'fraction_numerical': 0.0006622516556291391, 'mean_word_length': 2.031108881083793, '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': 16, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3789617', 'n_tokens_mistral': 2704, 'n_tokens_neox': 2746, 'n_words': 1023}