From 6a2c00045a27976e400471331b09f89426033f18 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 7 Sep 2016 17:20:57 +0200 Subject: [PATCH 1/7] First version of alternative function changes --- Base/Change/AltFunctionChanges.agda | 221 ++++++++++++++++++++++++++++ Base/HetEqExtra.agda | 19 +++ Postulate/Extensionality.agda | 4 + 3 files changed, 244 insertions(+) create mode 100644 Base/Change/AltFunctionChanges.agda create mode 100644 Base/HetEqExtra.agda diff --git a/Base/Change/AltFunctionChanges.agda b/Base/Change/AltFunctionChanges.agda new file mode 100644 index 0000000..e08d356 --- /dev/null +++ b/Base/Change/AltFunctionChanges.agda @@ -0,0 +1,221 @@ +module Base.Change.AltFunctionChanges where + +open import Data.Product +open import Function +import Relation.Binary.PropositionalEquality as P +open import Relation.Binary.HeterogeneousEquality as H +open import Postulate.Extensionality +open import Level + +open import Base.Ascription +open import Base.HetEqExtra +open import Base.Change.Algebra + +module AltFunctionChanges ℓ (A B : Set ℓ) {{CA : ChangeAlgebra ℓ A}} {{CB : ChangeAlgebra ℓ B}} where + open ≅-Reasoning + + RawChangeP : (f : A → B) → Set ℓ + RawChangeP f = (a : A) → Δ (f a) + + FunBaseT : Set ℓ + FunBaseT = Σ[ f ∈ (A → B) ] Σ[ f′ ∈ RawChange f ] IsDerivative f f′ + + _raw⊕_ : (f : A → B) → (df : RawChangeP f) → (A → B) + f raw⊕ df = λ a → f a ⊞ df a + + _raw⊝_ : (g f : A → B) → RawChangeP f + g raw⊝ f = λ a → g a ⊟ f a + + rawnil : (f : A → B) → RawChangeP f + rawnil f = λ a → nil (f a) + + raw-update-nil : ∀ f → f raw⊕ (rawnil f) ≅ f + raw-update-nil f = hext (λ a → update-nil (f a)) + raw-update-diff : ∀ f g → f raw⊕ (g raw⊝ f) ≅ g + raw-update-diff f g = hext (λ a → update-diff (g a) (f a)) + + deriv-f⊕df : ∀ (f : A → B) (df : RawChangeP f) → RawChange (f raw⊕ df) + deriv-f⊕df f df = λ a da → f (a ⊞ da) ⊞ df (a ⊞ da) ⊟ (f a ⊞ df a) + -- Instead of ` f (a ⊞ da) ` we could/should use` f a ⊞ f′ a da `, + -- but we'd need to invoke the right equivalence for the expression to typecheck. + -- XXX: that derivative is very non-incremental. + -- Alternatives: + -- 1. (invert df x) andThen (f' x dx) andThen (df (x ⊞ dx)) + -- 2. include a derivative in the function change as well. That would limit the point though. + + 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₀′) = + Σ[ df ∈ RawChangeP f₀ ] ( + let f₁ = f₀ raw⊕ df + in Σ[ f₁′ ∈ RawChange f₁ ] IsDerivative f₁ 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₁′) + + f-nil-eq : ∀ (f₀ : A → B) (f₀′ : RawChange f₀) (IsDerivative-f₀-f₀′ : IsDerivative f₀ f₀′) → + Σ[ nil-f₀ ∈ RawChangeP f₀ ] ( + let f₁ = f₀ raw⊕ nil-f₀ + in Σ[ f₁′ ∈ RawChange f₁ ] Σ[ IsDerivative-f₁-f₁′ ∈ IsDerivative f₁ f₁′ ] (f₁ ≅ f₀ × f₁′ ≅ f₀′ × IsDerivative-f₁-f₁′ ≅ IsDerivative-f₀-f₀′)) + + f-nil-eq f₀ f₀′ IsDerivative-f₀-f₀′ = df , f₁′ , IsDerivative-f₁-f₁′ , f₁≅f₀ , f₁′≅f₀′ , IsDerivative-f₁-f₁′≅IsDerivative-f₀-f₀′ + where + df = rawnil f₀ + f₁ = f₀ raw⊕ df + f₁≅f₀ = raw-update-nil f₀ + f₀≅f₁ = sym f₁≅f₀ + + f₁′ = subst RawChange f₀≅f₁ f₀′ + + f₁′≅f₀′ = subst-removable RawChange f₀≅f₁ f₀′ + f₀′≅f₁′ = sym f₁′≅f₀′ + + IsDerivative-f₁-f₁′ = hsubst₂ IsDerivative f₀≅f₁ f₀′≅f₁′ IsDerivative-f₀-f₀′ + IsDerivative-f₁-f₁′≅IsDerivative-f₀-f₀′ = hsubst₂-removable IsDerivative f₀≅f₁ f₀′≅f₁′ IsDerivative-f₀-f₀′ + + f-nil : (f : FunBaseT) → FChange f + f-nil (f₀ , f₀′ , IsDerivative-f₀-f₀′) = + let (df , f₁′ , IsDerivative-f₁-f₁′ , _ ) = f-nil-eq f₀ f₀′ IsDerivative-f₀-f₀′ + in df , f₁′ , IsDerivative-f₁-f₁′ + + f-update-nil : ∀ fstr → (fstr ⊕ f-nil fstr) P.≡ fstr + f-update-nil (f₀ , f₀′ , IsDerivative-f₀-f₀′) = + let (df , f₁′ , IsDerivative-f₁-f₁′ , f₁≅f₀ , f₁′≅f₀′ , IsDerivative-f₁-f₁′≅IsDerivative-f₀-f₀′ ) = f-nil-eq f₀ f₀′ IsDerivative-f₀-f₀′ + in ≅-to-≡ (cong₃ (λ x y z → as' FunBaseT (x , y , z)) f₁≅f₀ f₁′≅f₀′ IsDerivative-f₁-f₁′≅IsDerivative-f₀-f₀′) + + f-diff-eq : + ∀ (f₀ : A → B) (f₀′ : RawChange f₀) (IsDerivative-f₀-f₀′ : IsDerivative f₀ f₀′) → + (g₀ : A → B) (g₀′ : RawChange g₀) (IsDerivative-g₀-g₀′ : IsDerivative g₀ g₀′) → + Σ[ df ∈ RawChangeP f₀ ] ( + let g₁ = f₀ raw⊕ (g₀ raw⊝ f₀) + in Σ[ g₁′ ∈ RawChange g₁ ] Σ[ IsDerivative-g₁-g₁′ ∈ IsDerivative g₁ g₁′ ] (g₁ ≅ g₀ × g₁′ ≅ g₀′ × IsDerivative-g₁-g₁′ ≅ IsDerivative-g₀-g₀′)) + f-diff-eq f₀ f₀′ IsDerivative-f₀-f₀′ g₀ g₀′ IsDerivative-g₀-g₀′ + = df , g₁′ , IsDerivative-g₁-g₁′ , g₁≅g₀ , g₁′≅g₀′ , IsDerivative-g₁-g₁′≅IsDerivative-g₀-g₀′ + where + df = g₀ raw⊝ f₀ + g₁ = f₀ raw⊕ (g₀ raw⊝ f₀) + g₁≅g₀ = raw-update-diff f₀ g₀ + g₀≅g₁ = sym g₁≅g₀ + + g₁′ = subst RawChange g₀≅g₁ g₀′ + g₁′≅g₀′ = subst-removable RawChange g₀≅g₁ g₀′ + g₀′≅g₁′ = sym g₁′≅g₀′ + IsDerivative-g₁-g₁′ = hsubst₂ IsDerivative g₀≅g₁ g₀′≅g₁′ IsDerivative-g₀-g₀′ + IsDerivative-g₁-g₁′≅IsDerivative-g₀-g₀′ = hsubst₂-removable IsDerivative g₀≅g₁ g₀′≅g₁′ IsDerivative-g₀-g₀′ + + _⊝_ : (g f : FunBaseT) → FChange f + _⊝_ (g₀ , g₀′ , IsDerivative-g₀-g₀′) (f₀ , f₀′ , IsDerivative-f₀-f₀′) = + let (df , g₁′ , IsDerivative-g₁-g₁′ , _) = f-diff-eq f₀ f₀′ IsDerivative-f₀-f₀′ g₀ g₀′ IsDerivative-g₀-g₀′ + in df , g₁′ , IsDerivative-g₁-g₁′ + + -- _⊝_ : (g f : FunBaseT) → FChange f + -- _⊝_ (g , g′ , IsDerivative-g-g′) (f , f′ , IsDerivative-f-f′) + -- = g⊝f + -- , cast-g′ + -- , hsubst₂ (IsDerivative {{CA}} {{CB}}) g≅f-raw⊕-g⊝f g′≅cast-g′ IsDerivative-g-g′ + -- where + -- g⊝f = g raw⊝ f + -- g≅f-raw⊕-g⊝f : g ≅ f raw⊕ g⊝f + -- g≅f-raw⊕-g⊝f = sym (raw-update-diff f g) + + -- cast-g′ = subst RawChange g≅f-raw⊕-g⊝f g′ + + -- g′≅cast-g′ : g′ ≅ cast-g′ + -- g′≅cast-g′ = sym (subst-removable RawChange g≅f-raw⊕-g⊝f g′) + + f-update-diff : ∀ gstr fstr → fstr ⊕ (gstr ⊝ fstr) P.≡ gstr + f-update-diff (g₀ , g₀′ , IsDerivative-g₀-g₀′) (f₀ , f₀′ , IsDerivative-f₀-f₀′) = + let (df , g₁′ , IsDerivative-g₁-g₁′ , g₁≅g₀ , g₁′≅g₀′ , IsDerivative-g₁-g₁′≅IsDerivative-g₀-g₀′ ) = f-diff-eq f₀ f₀′ IsDerivative-f₀-f₀′ g₀ g₀′ IsDerivative-g₀-g₀′ + in ≅-to-≡ (cong₃ (λ x y z → as' FunBaseT (x , y , z)) g₁≅g₀ g₁′≅g₀′ IsDerivative-g₁-g₁′≅IsDerivative-g₀-g₀′) + + changeAlgebra : ChangeAlgebra ℓ FunBaseT + changeAlgebra = record + { Change = FChange + ; update = _⊕_ + ; diff = _⊝_ + ; nil = f-nil + ; isChangeAlgebra = record { update-diff = f-update-diff ; update-nil = f-update-nil } + } + -- f-diff : (g f : FunBaseT) → FChange f + -- f-diff (g , g′ , IsDerivative-g-g′) (f , f′ , IsDerivative-f-f′) = λ a → g a ⊟ f a + + +-- FChange : FunBaseT → Set ℓ +-- FChange (f , f′ , IsDerivative-f-f′) = RawChangeP f + +-- _⊕_ : (f : FunBaseT) → FChange f → FunBaseT +-- (f , f′ , IsDerivative-f-f′) ⊕ df = +-- ( f raw⊕ df +-- , ( deriv-f⊕df f df +-- , IsDerivative-deriv-f⊕df f df +-- ) +-- ) +-- f-nil : (f : FunBaseT) → FChange f +-- f-nil (f , f′ , IsDerivative-f-f′) a = nil (f a) + +-- f-diff : (g f : FunBaseT) → FChange f +-- f-diff (g , g′ , IsDerivative-g-g′) (f , f′ , IsDerivative-f-f′) = λ a → g a ⊟ f a + +-- -- f-update-nil fstr₀@(f₀ , f′₀ , IsDerivative-f-f′₀) with ext (λ a → sym (update-nil (f₀ a))) +-- -- f-update-nil fstr₀@(f₀ , f′₀ , IsDerivative-f-f′₀) | refl = {!!} +-- -- gives: +-- {- +-- With clause pattern fstr₀@(f₀ , f′₀ , IsDerivative-f-f′₀) is not an +-- instance of its parent pattern +-- (_,_ f₀ (_,_ f′₀ IsDerivative-f-f′₀)) +-- -} + +-- f-update-nil : ∀ fstr → (fstr ⊕ f-nil fstr) ≡ fstr +-- f-update-nil fstr₀@(f₀ , f′₀ , IsDerivative-f-f′₀) = {!!} +-- where + +-- nil-fstr = f-nil fstr₀ + +-- fstr₁ : FunBaseT +-- fstr₁ = fstr₀ ⊕ f-nil fstr₀ + +-- f₁ : A → B +-- f′₁ : RawChange f₁ +-- IsDerivative-f-f′₁ : IsDerivative f₁ f′₁ + +-- f₁ = proj₁ fstr₁ +-- f′₁ = proj₁ (proj₂ fstr₁) +-- IsDerivative-f-f′₁ = proj₂ (proj₂ fstr₁) +-- --(f₁ , f′₁ , IsDerivative-f-f′₁) = fstr₀ ⊕ f-nil fstr₀ + +-- f≡f : f₁ ≡ f₀ +-- f≡f = raw-update-nil f₀ + +-- -- f′₁′ : RawChange f₀ +-- -- f′₁′ = subst RawChange (sym f≡f) f′₁ + +-- -- -- f′₁≡f′₁′ : ∀ a → f′₁ a ≡ f′₁′ a +-- -- -- f′₁≡f′₁′ a = ? + +-- -- f′≡f′a : ∀ a → f′₁′ a ≡ f′₀ a +-- -- f′≡f′a a = {!!} + +-- -- f′≡f′ : f′₀ ≡ f′₁′ +-- -- f′≡f′ = ext f′≡f′a + +-- -- -- IsDer≡ : IsDerivative-f-f′₁ ≡ IsDerivative-f-f′₀ +-- -- -- IsDer≡ = ? + +-- f-update-diff : ∀ gstr fstr → fstr ⊕ (f-diff gstr fstr) ≡ gstr +-- f-update-diff (f , f′ , IsDerivative-f-f′) (g , g′ , IsDerivative-g-g′) = {!!} +-- where +-- fg : f raw⊕ (g raw⊝ f) ≡ g +-- fg = raw-update-diff f g + +-- changeAlgebra : ChangeAlgebra ℓ FunBaseT +-- changeAlgebra = record +-- { Change = FChange +-- ; update = _⊕_ +-- ; diff = f-diff +-- ; nil = f-nil +-- ; isChangeAlgebra = record { update-diff = f-update-diff ; update-nil = f-update-nil } +-- } diff --git a/Base/HetEqExtra.agda b/Base/HetEqExtra.agda new file mode 100644 index 0000000..5d3a5c3 --- /dev/null +++ b/Base/HetEqExtra.agda @@ -0,0 +1,19 @@ +module Base.HetEqExtra where + +open import Relation.Binary.HeterogeneousEquality + +-- More dependent variant of subst₂ from Relation.Binary.HeterogeneousEquality, see e.g. +-- http://stackoverflow.com/a/24255198/53974 +hsubst₂ : ∀ {a b p} {A : Set a} {B : A → Set b} (P : (a : A) → (B a) → Set p) → + ∀ {x₁ x₂ y₁ y₂} → x₁ ≅ x₂ → y₁ ≅ y₂ → P x₁ y₁ → P x₂ y₂ +hsubst₂ P refl refl p = p + +-- subst-removable for hsubst₂ +hsubst₂-removable : ∀ {a b p} {A : Set a} {B : A → Set b} (P : (a : A) → (B a) → Set p) → + ∀ {x₁ x₂ y₁ y₂} (≅₁ : x₁ ≅ x₂) (≅₂ : y₁ ≅ y₂) p → hsubst₂ P ≅₁ ≅₂ p ≅ p +hsubst₂-removable P refl refl p = refl + +cong₃ : ∀ {a b c d} {A : Set a} {B : A → Set b} {C : ∀ x → B x → Set c} {D : ∀ x y → C x y → Set d} + {x y u v z w} + (f : (x : A) (y : B x) → (z : C x y) → D x y z) → x ≅ y → u ≅ v → z ≅ w → f x u z ≅ f y v w +cong₃ f refl refl refl = refl diff --git a/Postulate/Extensionality.agda b/Postulate/Extensionality.agda index 5606926..a16dcfe 100644 --- a/Postulate/Extensionality.agda +++ b/Postulate/Extensionality.agda @@ -11,6 +11,7 @@ module Postulate.Extensionality where open import Relation.Binary.PropositionalEquality +import Relation.Binary.HeterogeneousEquality as H postulate ext : ∀ {a b} → Extensionality a b @@ -25,3 +26,6 @@ ext³ : ∀ ((a : A) (b : B a) (c : C a b) → f a b c ≡ g a b c) → f ≡ g ext³ fabc=gabc = ext (λ a → ext (λ b → ext (λ c → fabc=gabc a b c))) + +hext : ∀ {a b} → {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f H.≅ g +hext f≡g = H.≡-to-≅ (ext f≡g) From 48a80fe35c42bbdf7561b7577742189db3c7443c Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 7 Sep 2016 17:56:00 +0200 Subject: [PATCH 2/7] Delete dead code --- Base/Change/AltFunctionChanges.agda | 96 +---------------------------- 1 file changed, 2 insertions(+), 94 deletions(-) diff --git a/Base/Change/AltFunctionChanges.agda b/Base/Change/AltFunctionChanges.agda index e08d356..6adf034 100644 --- a/Base/Change/AltFunctionChanges.agda +++ b/Base/Change/AltFunctionChanges.agda @@ -57,6 +57,8 @@ module AltFunctionChanges ℓ (A B : Set ℓ) {{CA : ChangeAlgebra ℓ A}} {{CB let f₁ = f₀ raw⊕ df in (f₁ , f₁′ , IsDerivative-f₁-f₁′) + -- Produce a complete change, together with the needed correctness proofs. + -- Most of these proofs are already needed for the implementation; defining this lemma avoids duplicating them. f-nil-eq : ∀ (f₀ : A → B) (f₀′ : RawChange f₀) (IsDerivative-f₀-f₀′ : IsDerivative f₀ f₀′) → Σ[ nil-f₀ ∈ RawChangeP f₀ ] ( let f₁ = f₀ raw⊕ nil-f₀ @@ -112,21 +114,6 @@ module AltFunctionChanges ℓ (A B : Set ℓ) {{CA : ChangeAlgebra ℓ A}} {{CB let (df , g₁′ , IsDerivative-g₁-g₁′ , _) = f-diff-eq f₀ f₀′ IsDerivative-f₀-f₀′ g₀ g₀′ IsDerivative-g₀-g₀′ in df , g₁′ , IsDerivative-g₁-g₁′ - -- _⊝_ : (g f : FunBaseT) → FChange f - -- _⊝_ (g , g′ , IsDerivative-g-g′) (f , f′ , IsDerivative-f-f′) - -- = g⊝f - -- , cast-g′ - -- , hsubst₂ (IsDerivative {{CA}} {{CB}}) g≅f-raw⊕-g⊝f g′≅cast-g′ IsDerivative-g-g′ - -- where - -- g⊝f = g raw⊝ f - -- g≅f-raw⊕-g⊝f : g ≅ f raw⊕ g⊝f - -- g≅f-raw⊕-g⊝f = sym (raw-update-diff f g) - - -- cast-g′ = subst RawChange g≅f-raw⊕-g⊝f g′ - - -- g′≅cast-g′ : g′ ≅ cast-g′ - -- g′≅cast-g′ = sym (subst-removable RawChange g≅f-raw⊕-g⊝f g′) - f-update-diff : ∀ gstr fstr → fstr ⊕ (gstr ⊝ fstr) P.≡ gstr f-update-diff (g₀ , g₀′ , IsDerivative-g₀-g₀′) (f₀ , f₀′ , IsDerivative-f₀-f₀′) = let (df , g₁′ , IsDerivative-g₁-g₁′ , g₁≅g₀ , g₁′≅g₀′ , IsDerivative-g₁-g₁′≅IsDerivative-g₀-g₀′ ) = f-diff-eq f₀ f₀′ IsDerivative-f₀-f₀′ g₀ g₀′ IsDerivative-g₀-g₀′ @@ -140,82 +127,3 @@ module AltFunctionChanges ℓ (A B : Set ℓ) {{CA : ChangeAlgebra ℓ A}} {{CB ; nil = f-nil ; isChangeAlgebra = record { update-diff = f-update-diff ; update-nil = f-update-nil } } - -- f-diff : (g f : FunBaseT) → FChange f - -- f-diff (g , g′ , IsDerivative-g-g′) (f , f′ , IsDerivative-f-f′) = λ a → g a ⊟ f a - - --- FChange : FunBaseT → Set ℓ --- FChange (f , f′ , IsDerivative-f-f′) = RawChangeP f - --- _⊕_ : (f : FunBaseT) → FChange f → FunBaseT --- (f , f′ , IsDerivative-f-f′) ⊕ df = --- ( f raw⊕ df --- , ( deriv-f⊕df f df --- , IsDerivative-deriv-f⊕df f df --- ) --- ) --- f-nil : (f : FunBaseT) → FChange f --- f-nil (f , f′ , IsDerivative-f-f′) a = nil (f a) - --- f-diff : (g f : FunBaseT) → FChange f --- f-diff (g , g′ , IsDerivative-g-g′) (f , f′ , IsDerivative-f-f′) = λ a → g a ⊟ f a - --- -- f-update-nil fstr₀@(f₀ , f′₀ , IsDerivative-f-f′₀) with ext (λ a → sym (update-nil (f₀ a))) --- -- f-update-nil fstr₀@(f₀ , f′₀ , IsDerivative-f-f′₀) | refl = {!!} --- -- gives: --- {- --- With clause pattern fstr₀@(f₀ , f′₀ , IsDerivative-f-f′₀) is not an --- instance of its parent pattern --- (_,_ f₀ (_,_ f′₀ IsDerivative-f-f′₀)) --- -} - --- f-update-nil : ∀ fstr → (fstr ⊕ f-nil fstr) ≡ fstr --- f-update-nil fstr₀@(f₀ , f′₀ , IsDerivative-f-f′₀) = {!!} --- where - --- nil-fstr = f-nil fstr₀ - --- fstr₁ : FunBaseT --- fstr₁ = fstr₀ ⊕ f-nil fstr₀ - --- f₁ : A → B --- f′₁ : RawChange f₁ --- IsDerivative-f-f′₁ : IsDerivative f₁ f′₁ - --- f₁ = proj₁ fstr₁ --- f′₁ = proj₁ (proj₂ fstr₁) --- IsDerivative-f-f′₁ = proj₂ (proj₂ fstr₁) --- --(f₁ , f′₁ , IsDerivative-f-f′₁) = fstr₀ ⊕ f-nil fstr₀ - --- f≡f : f₁ ≡ f₀ --- f≡f = raw-update-nil f₀ - --- -- f′₁′ : RawChange f₀ --- -- f′₁′ = subst RawChange (sym f≡f) f′₁ - --- -- -- f′₁≡f′₁′ : ∀ a → f′₁ a ≡ f′₁′ a --- -- -- f′₁≡f′₁′ a = ? - --- -- f′≡f′a : ∀ a → f′₁′ a ≡ f′₀ a --- -- f′≡f′a a = {!!} - --- -- f′≡f′ : f′₀ ≡ f′₁′ --- -- f′≡f′ = ext f′≡f′a - --- -- -- IsDer≡ : IsDerivative-f-f′₁ ≡ IsDerivative-f-f′₀ --- -- -- IsDer≡ = ? - --- f-update-diff : ∀ gstr fstr → fstr ⊕ (f-diff gstr fstr) ≡ gstr --- f-update-diff (f , f′ , IsDerivative-f-f′) (g , g′ , IsDerivative-g-g′) = {!!} --- where --- fg : f raw⊕ (g raw⊝ f) ≡ g --- fg = raw-update-diff f g - --- changeAlgebra : ChangeAlgebra ℓ FunBaseT --- changeAlgebra = record --- { Change = FChange --- ; update = _⊕_ --- ; diff = f-diff --- ; nil = f-nil --- ; isChangeAlgebra = record { update-diff = f-update-diff ; update-nil = f-update-nil } --- } From 3b7573d130da694c2426b8624a9b8e679bfaf679 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 7 Sep 2016 18:56:44 +0200 Subject: [PATCH 3/7] Abstract away the hsubst boilerplate --- Base/Change/AltFunctionChanges.agda | 68 ++++++++--------------------- 1 file changed, 18 insertions(+), 50 deletions(-) diff --git a/Base/Change/AltFunctionChanges.agda b/Base/Change/AltFunctionChanges.agda index 6adf034..a055e4d 100644 --- a/Base/Change/AltFunctionChanges.agda +++ b/Base/Change/AltFunctionChanges.agda @@ -57,67 +57,35 @@ module AltFunctionChanges ℓ (A B : Set ℓ) {{CA : ChangeAlgebra ℓ A}} {{CB let f₁ = f₀ raw⊕ df in (f₁ , f₁′ , IsDerivative-f₁-f₁′) - -- Produce a complete change, together with the needed correctness proofs. - -- Most of these proofs are already needed for the implementation; defining this lemma avoids duplicating them. - f-nil-eq : ∀ (f₀ : A → B) (f₀′ : RawChange f₀) (IsDerivative-f₀-f₀′ : IsDerivative f₀ f₀′) → - Σ[ nil-f₀ ∈ RawChangeP f₀ ] ( - let f₁ = f₀ raw⊕ nil-f₀ - in Σ[ f₁′ ∈ RawChange f₁ ] Σ[ IsDerivative-f₁-f₁′ ∈ IsDerivative f₁ f₁′ ] (f₁ ≅ f₀ × f₁′ ≅ f₀′ × IsDerivative-f₁-f₁′ ≅ IsDerivative-f₀-f₀′)) - - f-nil-eq f₀ f₀′ IsDerivative-f₀-f₀′ = df , f₁′ , IsDerivative-f₁-f₁′ , f₁≅f₀ , f₁′≅f₀′ , IsDerivative-f₁-f₁′≅IsDerivative-f₀-f₀′ - where - df = rawnil f₀ - f₁ = f₀ raw⊕ df - f₁≅f₀ = raw-update-nil f₀ - f₀≅f₁ = sym f₁≅f₀ - - f₁′ = subst RawChange f₀≅f₁ f₀′ + 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₀′ - f₁′≅f₀′ = subst-removable RawChange f₀≅f₁ f₀′ - f₀′≅f₁′ = sym f₁′≅f₀′ - - IsDerivative-f₁-f₁′ = hsubst₂ IsDerivative f₀≅f₁ f₀′≅f₁′ IsDerivative-f₀-f₀′ - IsDerivative-f₁-f₁′≅IsDerivative-f₀-f₀′ = hsubst₂-removable IsDerivative f₀≅f₁ 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 , f₁′ , IsDerivative-f₁-f₁′ , _ ) = f-nil-eq f₀ f₀′ IsDerivative-f₀-f₀′ - in df , 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₀′ f-update-nil : ∀ fstr → (fstr ⊕ f-nil fstr) P.≡ fstr - f-update-nil (f₀ , f₀′ , IsDerivative-f₀-f₀′) = - let (df , f₁′ , IsDerivative-f₁-f₁′ , f₁≅f₀ , f₁′≅f₀′ , IsDerivative-f₁-f₁′≅IsDerivative-f₀-f₀′ ) = f-nil-eq f₀ f₀′ IsDerivative-f₀-f₀′ - in ≅-to-≡ (cong₃ (λ x y z → as' FunBaseT (x , y , z)) f₁≅f₀ f₁′≅f₀′ IsDerivative-f₁-f₁′≅IsDerivative-f₀-f₀′) - - f-diff-eq : - ∀ (f₀ : A → B) (f₀′ : RawChange f₀) (IsDerivative-f₀-f₀′ : IsDerivative f₀ f₀′) → - (g₀ : A → B) (g₀′ : RawChange g₀) (IsDerivative-g₀-g₀′ : IsDerivative g₀ g₀′) → - Σ[ df ∈ RawChangeP f₀ ] ( - let g₁ = f₀ raw⊕ (g₀ raw⊝ f₀) - in Σ[ g₁′ ∈ RawChange g₁ ] Σ[ IsDerivative-g₁-g₁′ ∈ IsDerivative g₁ g₁′ ] (g₁ ≅ g₀ × g₁′ ≅ g₀′ × IsDerivative-g₁-g₁′ ≅ IsDerivative-g₀-g₀′)) - f-diff-eq f₀ f₀′ IsDerivative-f₀-f₀′ g₀ g₀′ IsDerivative-g₀-g₀′ - = df , g₁′ , IsDerivative-g₁-g₁′ , g₁≅g₀ , g₁′≅g₀′ , IsDerivative-g₁-g₁′≅IsDerivative-g₀-g₀′ - where - df = g₀ raw⊝ f₀ - g₁ = f₀ raw⊕ (g₀ raw⊝ f₀) - g₁≅g₀ = raw-update-diff f₀ g₀ - g₀≅g₁ = sym g₁≅g₀ - - g₁′ = subst RawChange g₀≅g₁ g₀′ - g₁′≅g₀′ = subst-removable RawChange g₀≅g₁ g₀′ - g₀′≅g₁′ = sym g₁′≅g₀′ - IsDerivative-g₁-g₁′ = hsubst₂ IsDerivative g₀≅g₁ g₀′≅g₁′ IsDerivative-g₀-g₀′ - IsDerivative-g₁-g₁′≅IsDerivative-g₀-g₀′ = hsubst₂-removable IsDerivative g₀≅g₁ g₀′≅g₁′ IsDerivative-g₀-g₀′ + 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₁′ , IsDerivative-g₁-g₁′ , _) = f-diff-eq f₀ f₀′ IsDerivative-f₀-f₀′ g₀ g₀′ IsDerivative-g₀-g₀′ - in df , g₁′ , IsDerivative-g₁-g₁′ + 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₀′ f-update-diff : ∀ gstr fstr → fstr ⊕ (gstr ⊝ fstr) P.≡ gstr - f-update-diff (g₀ , g₀′ , IsDerivative-g₀-g₀′) (f₀ , f₀′ , IsDerivative-f₀-f₀′) = - let (df , g₁′ , IsDerivative-g₁-g₁′ , g₁≅g₀ , g₁′≅g₀′ , IsDerivative-g₁-g₁′≅IsDerivative-g₀-g₀′ ) = f-diff-eq f₀ f₀′ IsDerivative-f₀-f₀′ g₀ g₀′ IsDerivative-g₀-g₀′ - in ≅-to-≡ (cong₃ (λ x y z → as' FunBaseT (x , y , z)) g₁≅g₀ g₁′≅g₀′ IsDerivative-g₁-g₁′≅IsDerivative-g₀-g₀′) + 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₀′ changeAlgebra : ChangeAlgebra ℓ FunBaseT changeAlgebra = record From 92ffe6615fa0ad448dc33553060a940805bec401 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 7 Sep 2016 18:59:23 +0200 Subject: [PATCH 4/7] Improve abstraction a bit --- Base/Change/AltFunctionChanges.agda | 40 ++++++++++++++++------------- 1 file changed, 22 insertions(+), 18 deletions(-) diff --git a/Base/Change/AltFunctionChanges.agda b/Base/Change/AltFunctionChanges.agda index a055e4d..032360d 100644 --- a/Base/Change/AltFunctionChanges.agda +++ b/Base/Change/AltFunctionChanges.agda @@ -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₀′ From af5372f1afeebda56a7cc5fdc1deb8a0fbf1ec79 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 7 Sep 2016 19:01:30 +0200 Subject: [PATCH 5/7] Improve module name --- .../{AltFunctionChanges.agda => PointwiseFunctionChanges.agda} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename Base/Change/{AltFunctionChanges.agda => PointwiseFunctionChanges.agda} (98%) diff --git a/Base/Change/AltFunctionChanges.agda b/Base/Change/PointwiseFunctionChanges.agda similarity index 98% rename from Base/Change/AltFunctionChanges.agda rename to Base/Change/PointwiseFunctionChanges.agda index 032360d..4a6fe50 100644 --- a/Base/Change/AltFunctionChanges.agda +++ b/Base/Change/PointwiseFunctionChanges.agda @@ -1,4 +1,4 @@ -module Base.Change.AltFunctionChanges where +module Base.Change.PointwiseFunctionChanges where open import Data.Product open import Function From 264e58642cbd2ffb4d264b04d722f0032b061b95 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 7 Sep 2016 19:28:06 +0200 Subject: [PATCH 6/7] Further simplifications - Introduce `Derivative` for the pair of a function change and prove that it's a derivative. Using it saves lots of clutter. - Rationalize argument names in transport lemmas. - Stop using heterogeneous equality, at least now it's unneeded. --- Base/Change/Algebra.agda | 3 + Base/Change/PointwiseFunctionChanges.agda | 72 ++++++++++------------- 2 files changed, 34 insertions(+), 41 deletions(-) diff --git a/Base/Change/Algebra.agda b/Base/Change/Algebra.agda index 78bf2bb..3014a1b 100644 --- a/Base/Change/Algebra.agda +++ b/Base/Change/Algebra.agda @@ -256,6 +256,9 @@ module GroupChanges module FunctionChanges {a} {b} {c} {d} (A : Set a) (B : Set b) {{CA : ChangeAlgebra c A}} {{CB : ChangeAlgebra d B}} where + Derivative : (A → B) → Set (a ⊔ b ⊔ c ⊔ d) + Derivative f = Σ[ f′ ∈ RawChange f ] IsDerivative f f′ + -- This corresponds to Definition 2.6 in the paper. record FunctionChange (f : A → B) : Set (a ⊔ b ⊔ c ⊔ d) where field diff --git a/Base/Change/PointwiseFunctionChanges.agda b/Base/Change/PointwiseFunctionChanges.agda index 4a6fe50..2c32988 100644 --- a/Base/Change/PointwiseFunctionChanges.agda +++ b/Base/Change/PointwiseFunctionChanges.agda @@ -2,8 +2,7 @@ module Base.Change.PointwiseFunctionChanges where open import Data.Product open import Function -import Relation.Binary.PropositionalEquality as P -open import Relation.Binary.HeterogeneousEquality as H +open import Relation.Binary.PropositionalEquality open import Postulate.Extensionality open import Level @@ -14,13 +13,13 @@ 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 + open FunctionChanges A B {{CA}} {{CB}} using (Derivative) RawChangeP : (f : A → B) → Set ℓ RawChangeP f = (a : A) → Δ (f a) FunBaseT : Set ℓ - FunBaseT = Σ[ f ∈ (A → B) ] Σ[ f′ ∈ RawChange f ] IsDerivative f f′ + FunBaseT = Σ[ f ∈ (A → B) ] Derivative f _raw⊕_ : (f : A → B) → (df : RawChangeP f) → (A → B) f raw⊕ df = λ a → f a ⊞ df a @@ -31,13 +30,16 @@ module AltFunctionChanges ℓ (A B : Set ℓ) {{CA : ChangeAlgebra ℓ A}} {{CB rawnil : (f : A → B) → RawChangeP f rawnil f = λ a → nil (f a) - raw-update-nil : ∀ f → f raw⊕ (rawnil f) ≅ f - raw-update-nil f = hext (λ a → update-nil (f a)) - raw-update-diff : ∀ f g → f raw⊕ (g raw⊝ f) ≅ g - raw-update-diff f g = hext (λ a → update-diff (g a) (f a)) + raw-update-nil : ∀ f → f raw⊕ (rawnil f) ≡ f + raw-update-nil f = ext (λ a → update-nil (f a)) + raw-update-diff : ∀ f g → f raw⊕ (g raw⊝ f) ≡ g + raw-update-diff f g = ext (λ a → update-diff (g a) (f a)) - deriv-f⊕df : ∀ (f : A → B) (df : RawChangeP f) → RawChange (f raw⊕ df) - deriv-f⊕df f df = λ a da → f (a ⊞ da) ⊞ df (a ⊞ da) ⊟ (f a ⊞ df a) + Derivative-f⊕df : ∀ (f : A → B) (df : RawChangeP f) → Derivative (f raw⊕ df) + Derivative-f⊕df f df + = ( (λ a da → f (a ⊞ da) ⊞ df (a ⊞ da) ⊟ (f a ⊞ df a)) + , (λ a da → update-diff (f (a ⊞ da) ⊞ df (a ⊞ da)) (f a ⊞ df a)) + ) -- Instead of ` f (a ⊞ da) ` we could/should use` f a ⊞ f′ a da `, -- but we'd need to invoke the right equivalence for the expression to typecheck. -- XXX: that derivative is very non-incremental. @@ -45,51 +47,39 @@ module AltFunctionChanges ℓ (A B : Set ℓ) {{CA : ChangeAlgebra ℓ A}} {{CB -- 1. (invert df x) andThen (f' x dx) andThen (df (x ⊞ dx)) -- 2. include a derivative in the function change as well. That would limit the point though. - 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₀ : (A → B) → Set ℓ - FChange₀ f₀ = - Σ[ df ∈ RawChangeP f₀ ] ( - let f₁ = f₀ raw⊕ df - in Σ[ f₁′ ∈ RawChange f₁ ] IsDerivative f₁ f₁′) + FChange₀ f₀ = Σ[ df ∈ RawChangeP f₀ ] Derivative (f₀ raw⊕ df) FChange : FunBaseT → Set ℓ - FChange (f₀ , f₀′ , IsDerivative-f₀-f₀′) = FChange₀ f₀ + FChange (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₁′) + (f₀ , _f₀′) ⊕ (df , f₁′) = (f₀ raw⊕ df , 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₀′ + -- Lemmas to transport across the f₁ᵇ ≅ f₁ᵃ equality. + transport-derivative-to-equiv-base : ∀ {f₁ᵃ f₁ᵇ} (eq : f₁ᵇ ≡ f₁ᵃ) → Derivative f₁ᵃ → Derivative f₁ᵇ + transport-derivative-to-equiv-base refl 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 : ∀ {f₀ f₁} df → Derivative f₁ → (f₀ raw⊕ df ≡ f₁) → FChange₀ f₀ + transport-base-f df f₁′ eq = df , transport-derivative-to-equiv-base eq f₁′ + -- Implementation note: transport-base-f can't pattern match on eq because of a unification failure. + -- Hence we called the generalized transport-derivative-to-equiv-base, where the problem disappears. - 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 + transport-base-f-eq : ∀ {f₁ᵃ f₁ᵇ} (eq : f₁ᵇ ≡ f₁ᵃ) (f₁′ : Derivative f₁ᵃ) → + (f₁ᵇ , transport-derivative-to-equiv-base eq f₁′) ≡ (f₁ᵃ , f₁′) + transport-base-f-eq refl f₁′ = refl f-nil : (f : FunBaseT) → FChange f - f-nil (f₀ , f₀′ , IsDerivative-f₀-f₀′) = - transport-base-f (rawnil f₀) (raw-update-nil f₀) f₀′ IsDerivative-f₀-f₀′ + f-nil (f , f′) = transport-base-f (rawnil f) f′ (raw-update-nil 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 : ∀ fstr → (fstr ⊕ f-nil fstr) ≡ fstr + f-update-nil (f , f′) = transport-base-f-eq (raw-update-nil f) f′ _⊝_ : (g f : FunBaseT) → FChange f - _⊝_ (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₀′ + _⊝_ (g , g′) (f , _f′) = transport-base-f (g raw⊝ f) g′ (raw-update-diff f 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₀′ + f-update-diff : ∀ gstr fstr → fstr ⊕ (gstr ⊝ fstr) ≡ gstr + f-update-diff (g , g′) (f , _f′) = transport-base-f-eq (raw-update-diff f g) g′ changeAlgebra : ChangeAlgebra ℓ FunBaseT changeAlgebra = record From c2b1e17d951a5c1fc3556300163d939c8ffaeea1 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 7 Sep 2016 20:31:42 +0200 Subject: [PATCH 7/7] Use sections also for RawChange/IsDerivative --- Base/Change/Algebra.agda | 84 ++++++++++++++++++++-------------------- 1 file changed, 41 insertions(+), 43 deletions(-) diff --git a/Base/Change/Algebra.agda b/Base/Change/Algebra.agda index 3014a1b..87fbf74 100644 --- a/Base/Change/Algebra.agda +++ b/Base/Change/Algebra.agda @@ -145,49 +145,6 @@ syntax update′ x v dv = v ⊞₍ x ₎ dv diff′ = Family.diff syntax diff′ x u v = u ⊟₍ x ₎ v --- Derivatives --- =========== --- --- This corresponds to Def. 2.4 in the paper. - -RawChange : ∀ {a b c d} {A : Set a} {B : Set b} → - {{CA : ChangeAlgebra c A}} → - {{CB : ChangeAlgebra d B}} → - (f : A → B) → - Set (a ⊔ c ⊔ d) -RawChange f = ∀ a (da : Δ a) → Δ (f a) - -IsDerivative : ∀ {a b c d} {A : Set a} {B : Set b} → - {{CA : ChangeAlgebra c A}} → - {{CB : ChangeAlgebra d B}} → - (f : A → B) → - (df : RawChange f) → - Set (a ⊔ b ⊔ c) -IsDerivative f df = ∀ a da → f a ⊞ df a da ≡ f (a ⊞ da) - --- This is a variant of IsDerivative for change algebra families. -RawChange₍_,_₎ : ∀ {a b p q c d} {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} → - {{CP : ChangeAlgebraFamily c P}} → - {{CQ : ChangeAlgebraFamily d Q}} → - (x : A) → - (y : B) → - (f : P x → Q y) → Set (c ⊔ d ⊔ p) -RawChange₍_,_₎ x y f = ∀ px (dpx : Δ₍_₎ x px) → Δ₍_₎ y (f px) - -IsDerivative₍_,_₎ : ∀ {a b p q c d} {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} → - {{CP : ChangeAlgebraFamily c P}} → - {{CQ : ChangeAlgebraFamily d Q}} → - (x : A) → - (y : B) → - (f : P x → Q y) → - (df : RawChange₍_,_₎ x y f) → - Set (p ⊔ q ⊔ c) -IsDerivative₍_,_₎ {P = P} {{CP}} {{CQ}} x y f df = IsDerivative {{change-algebra₍ _ ₎}} {{change-algebra₍ _ ₎}} f df where - CPx = change-algebra₍_₎ {{CP}} x - CQy = change-algebra₍_₎ {{CQ}} y - --- Lemma 2.5 appears in Base.Change.Equivalence. - -- Abelian Groups Induce Change Algebras -- ===================================== -- @@ -253,6 +210,47 @@ module GroupChanges -- arguments, and provides a changeAlgebra for (A → B). The proofs -- are by equational reasoning using 2.1e for A and B. +module _ {a} {b} {c} {d} {A : Set a} {B : Set b} {{CA : ChangeAlgebra c A}} {{CB : ChangeAlgebra d B}} + where + -- Derivatives + -- =========== + -- + -- This corresponds to Def. 2.4 in the paper. + + RawChange : + (f : A → B) → + Set (a ⊔ c ⊔ d) + RawChange f = ∀ a (da : Δ a) → Δ (f a) + + IsDerivative : + (f : A → B) → + (df : RawChange f) → + Set (a ⊔ b ⊔ c) + IsDerivative f df = ∀ a da → f a ⊞ df a da ≡ f (a ⊞ da) + +module _ {a b p q c d} {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} + {{CP : ChangeAlgebraFamily c P}} {{CQ : ChangeAlgebraFamily d Q}} + where + + -- This is a variant of IsDerivative for change algebra families. + RawChange₍_,_₎ : + (x : A) → + (y : B) → + (f : P x → Q y) → Set (c ⊔ d ⊔ p) + RawChange₍_,_₎ x y f = ∀ px (dpx : Δ₍_₎ x px) → Δ₍_₎ y (f px) + + IsDerivative₍_,_₎ : + (x : A) → + (y : B) → + (f : P x → Q y) → + (df : RawChange₍_,_₎ x y f) → + Set (p ⊔ q ⊔ c) + IsDerivative₍_,_₎ x y f df = IsDerivative {{change-algebra₍ _ ₎}} {{change-algebra₍ _ ₎}} f df where + CPx = change-algebra₍_₎ {{CP}} x + CQy = change-algebra₍_₎ {{CQ}} y + + -- Lemma 2.5 appears in Base.Change.Equivalence. + module FunctionChanges {a} {b} {c} {d} (A : Set a) (B : Set b) {{CA : ChangeAlgebra c A}} {{CB : ChangeAlgebra d B}} where