Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Pointwise function changes #14

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Improve abstraction a bit
  • Loading branch information
Blaisorblade committed Sep 7, 2016
commit 92ffe6615fa0ad448dc33553060a940805bec401
40 changes: 22 additions & 18 deletions Base/Change/AltFunctionChanges.agda
Original file line number Diff line number Diff line change
@@ -11,6 +11,8 @@ open import Base.Ascription
open import Base.HetEqExtra
open import Base.Change.Algebra

-- Define an alternative change structure on functions based on pointwise changes. Both functions and changes carry a derivative with them.

module AltFunctionChanges ℓ (A B : Set ℓ) {{CA : ChangeAlgebra ℓ A}} {{CB : ChangeAlgebra ℓ B}} where
open ≅-Reasoning

@@ -46,43 +48,45 @@ module AltFunctionChanges ℓ (A B : Set ℓ) {{CA : ChangeAlgebra ℓ A}} {{CB
IsDerivative-deriv-f⊕df : (f : A → B) → (df : RawChangeP f) → IsDerivative (f raw⊕ df) (deriv-f⊕df f df)
IsDerivative-deriv-f⊕df f df a da = update-diff (f (a ⊞ da) ⊞ df (a ⊞ da)) (f a ⊞ df a)

FChange : FunBaseT → Set ℓ
FChange (f₀ , f₀′ , IsDerivative-f₀-f₀′) =
FChange : (A → B) → Set ℓ
FChange₀ f₀ =
Σ[ df ∈ RawChangeP f₀ ] (
let f₁ = f₀ raw⊕ df
in Σ[ f₁′ ∈ RawChange f₁ ] IsDerivative f₁ f₁′)

FChange : FunBaseT → Set ℓ
FChange (f₀ , f₀′ , IsDerivative-f₀-f₀′) = FChange₀ f₀

_⊕_ : (f : FunBaseT) → FChange f → FunBaseT
(f₀ , f₀′ , IsDerivative-f₀-f₀′) ⊕ (df , f₁′ , IsDerivative-f₁-f₁′) =
let f₁ = f₀ raw⊕ df
in (f₁ , f₁′ , IsDerivative-f₁-f₁′)

transport-base-f : ∀ {f₀ f₁ : A → B} (eq : f₁ ≅ f₀) (f₀′ : RawChange f₀) (IsDerivative-f₀-f₀′ : IsDerivative f₀ f₀′) →
-- Lemmas to transport across the f₁ ≅ f₀ equality.
transport-base-f₀ : ∀ {f₀ f₁ : A → B} (eq : f₁ ≅ f₀) (f₀′ : RawChange f₀) (IsDerivative-f₀-f₀′ : IsDerivative f₀ f₀′) →
Σ[ f₁′ ∈ RawChange f₁ ] (IsDerivative f₁ f₁′)
transport-base-f refl f₀′ IsDerivative-f₀-f₀′ = f₀′ , IsDerivative-f₀-f₀′
transport-base-f₀ refl f₀′ IsDerivative-f₀-f₀′ = f₀′ , IsDerivative-f₀-f₀′

transport-base-f : ∀ {f₀ g₀ : A → B} df →
let g₁ = f₀ raw⊕ df
in (eq : g₁ ≅ g₀) (g₀′ : RawChange g₀) (IsDerivative-g₀-g₀′ : IsDerivative g₀ g₀′) → FChange₀ f₀
transport-base-f df eq g₀′ IsDerivative-g₀-g₀′ = df , transport-base-f₀ eq g₀′ IsDerivative-g₀-g₀′

transport-base-f-eq : ∀ {f₀ f₁ : A → B} (eq : f₁ ≅ f₀) (f₀′ : RawChange f₀) (IsDerivative-f₀-f₀′ : IsDerivative f₀ f₀′) →
(f₁ , transport-base-f eq f₀′ IsDerivative-f₀-f₀′) P.≡ (f₀ , f₀′ , IsDerivative-f₀-f₀′)
transport-base-f-eq : ∀ {f₀ f₁ : A → B}
(eq : f₁ ≅ f₀) (f₀′ : RawChange f₀) (IsDerivative-f₀-f₀′ : IsDerivative f₀ f₀′) →
(f₁ , transport-base-f₀ eq f₀′ IsDerivative-f₀-f₀′) P.≡ (f₀ , f₀′ , IsDerivative-f₀-f₀′)
transport-base-f-eq refl f₀′ IsDerivative-f₀-f₀′ = P.refl

f-nil : (f : FunBaseT) → FChange f
f-nil (f₀ , f₀′ , IsDerivative-f₀-f₀′) =
let
df = rawnil f₀
f₁ = f₀ raw⊕ df
f₁≅f₀ = raw-update-nil f₀
in df , transport-base-f f₁≅f₀ f₀′ IsDerivative-f₀-f₀′
transport-base-f (rawnil f₀) (raw-update-nil f₀) f₀′ IsDerivative-f₀-f₀′

f-update-nil : ∀ fstr → (fstr ⊕ f-nil fstr) P.≡ fstr
f-update-nil (f₀ , f₀′ , IsDerivative-f₀-f₀′) = transport-base-f-eq (raw-update-nil f₀) f₀′ IsDerivative-f₀-f₀′
f-update-nil (f₀ , f₀′ , IsDerivative-f₀-f₀′) =
transport-base-f-eq (raw-update-nil f₀) f₀′ IsDerivative-f₀-f₀′

_⊝_ : (g f : FunBaseT) → FChange f
_⊝_ (g₀ , g₀′ , IsDerivative-g₀-g₀′) (f₀ , f₀′ , IsDerivative-f₀-f₀′) =
let
df = g₀ raw⊝ f₀
g₁ = f₀ raw⊕ df
g₁≅g₀ = raw-update-diff f₀ g₀
in df , transport-base-f g₁≅g₀ g₀′ IsDerivative-g₀-g₀′
_⊝_ (g₀ , g₀′ , IsDerivative-g₀-g₀′) (f₀ , f₀′ , IsDerivative-f₀-f₀′) = transport-base-f (g₀ raw⊝ f₀) (raw-update-diff f₀ g₀) g₀′ IsDerivative-g₀-g₀′

f-update-diff : ∀ gstr fstr → fstr ⊕ (gstr ⊝ fstr) P.≡ gstr
f-update-diff (g₀ , g₀′ , IsDerivative-g₀-g₀′) (f₀ , f₀′ , IsDerivative-f₀-f₀′) = transport-base-f-eq (raw-update-diff f₀ g₀) g₀′ IsDerivative-g₀-g₀′