Stream: Beginner Questions

Topic: Defining abstract Frechet derivative

view this post on Zulip Alex Hyman (Nov 26 2025 at 16:01):

Why does the simple lemma shown not follow immediately from chain_rule. There's some weird type theoretic thing going on, but I'm not sure why:

(*abstract Frechet derivative operator*)
consts D :: "('u ⇒ 'v) ⇒ 'u ⇒ ('u ⇒ 'v)"


locale differentiation =
  assumes chain_rule:
    "⋀(f::'a⇒'b) (g::'b⇒'c) (x::'a). D (g ∘ f) x = (D g (f x)) ∘ (D f x)"

begin
lemma "(λ x . (D (g ∘ f) x)) = (λ x . (D g (f x)) ∘ (D f x))"
  using chain_rule by blast

end

view this post on Zulip Mathias Fleury (Nov 26 2025 at 16:02):

lemma "(λ x . (D (g ∘ f) x)) = (λ x . (D g (f x)) ∘ (D f x))" for f::"'a⇒'b" and g :: "'b⇒'c"
  using chain_rule[of g f] by blast

view this post on Zulip Mathias Fleury (Nov 26 2025 at 16:02):

if you specify the types it works

view this post on Zulip Mathias Fleury (Nov 26 2025 at 16:03):

The issue is that 'a, 'b, and 'c fixed by the locale but the typing give a more general type

view this post on Zulip Mathias Fleury (Nov 26 2025 at 16:04):

The "weird type theoretic thing" is that that locale do not allow to say forall 'a, 'b, 'c, we have

view this post on Zulip Alex Hyman (Nov 26 2025 at 16:05):

Ok I see. Never knew about this "for" notation so thank you!
Is there a way to refactor this code so that I don't need to explicitly give types every time?

view this post on Zulip Mathias Fleury (Nov 26 2025 at 16:09):

Depends on your application, you could add some abbreviation of D:

abbreviation Da where
  ‹Da ≡ (D :: ('a ⇒ 'c) ⇒ 'a ⇒ 'a ⇒ 'c)›

abbreviation Db where
  ‹Db ≡ (D:: ('b ⇒ 'c) ⇒ 'b ⇒ 'b ⇒ 'c)›

lemma "(λ x . (Da (g ∘ f) x)) = (λ x . (Db g (f x)) ∘ (D f x))"
  using chain_rule[of g f] by blast

view this post on Zulip Mathias Fleury (Nov 26 2025 at 16:10):

or if you always work with f and g, you could just fix them in the locale

view this post on Zulip Mathias Fleury (Nov 26 2025 at 16:11):

locale differentiation =
  fixes f::"'a⇒'b" and g::"'b⇒'c"
  assumes chain_rule:
    "⋀(f::'a⇒'b) (g::'b⇒'c) (x::'a). D (g ∘ f) x = (D g (f x)) ∘ (D f x)"

begin

lemma "(λ x . (D (g ∘ f) x)) = (λ x . (D g (f x)) ∘ (D f x))"
  using chain_rule[of g f] by blast

end

or probably better, a context:

locale differentiation =
  assumes chain_rule:
    "⋀(f::'a⇒'b) (g::'b⇒'c) (x::'a). D (g ∘ f) x = (D g (f x)) ∘ (D f x)"

begin
context
fixes f::"'a⇒'b" and g::"'b⇒'c"
begin
lemma "(λ x . (D (g ∘ f) x)) = (λ x . (D g (f x)) ∘ (D f x))"
  using chain_rule[of g f] by blast


lemma "(λ x . (D (g ∘ f) x)) = (λ x . (D g (f x)) ∘ (D f x))"
  using chain_rule[of g f] by blast

lemma "(λ x . (D (g ∘ f) x)) = (λ x . (D g (f x)) ∘ (D f x))"
  using chain_rule[of g f] by blast
end
end

Last updated: Dec 08 2025 at 08:34 UTC