I'm having fun formalizing some calculus book "for humans", which, of course, is using partial functions.

And I got a question - what's the best way to formalize and reason about domains of composite functions and stuff, for example, (sqrt(x) + tan(x))/(x+1). It seems like something easy for humans but not so easy to formalize in a way that's comfortable to use (for me, who's having brain fog right now).

Basically, I'm asking if the bicycle is already invented.

For now I'm using the set theoretic (?) definition of function, because that's used in the book.

```
Structure function A B := {
graph: set (A * B);
function_property: ∀ x y1 y2, graph (x, y1) → graph (x, y2) → y1 = y2
}.
```

Then partial analogue of `Rdiv`

has type of `function (R * R) R`

, for example.

Nit: The above didn’t render well — you want the 3 backticks on their own line, while for inline code you want a single backtick.

two common approaches are indeed functional relations (`A -> B -> Prop`

with the restriction you describe), and function in the `option`

monad (like `A -> B -> option C`

). The latter works well for computable functions, but most functions on reals don’t just “terminate”.

“common approaches” in general, never looked at formalizations of calculus. For composing functions of `function A B`

type, I wonder if you could follows Haskell’s notation for the Arrow typeclass — assuming that `function`

is indeed a valid instance.

There are a number of possibilities. It mostly depedents on which library you are using: math-comp analysis, coquelicot, corn/math-classes, ...

Is there defined Arrow typeclass in Coq, in some library somewhere? I tried to find but wasn't successful.

Not that I'm aware (my idea was to build such a thing), but you should probably ignore me and listen to @Bas Spitters. I wouldn't have spoken :grinning:

Both the relational and the `option`

variant have the drawback that it is very painful to write composite expression. Often it is preferably to just extend functions to the full argument type (i.e., define the quare root of negative real/rational numbers to be 0). Of course, many lemmas will still need side conditions ensuring that the arguments are within the domain on which the function is normally defined.

The prime example is subtraction on `nat`

, which satisfies `n - m = 0`

whenever `n <= m`

.

I know about normal practice in formalisations, I'm just exploring how to do it in the wrong (the painful) way.

Thank you, anyway. :)

Lessness said:

I know about normal practice in formalisations, I'm just exploring how to do it in the wrong (the painful) way.

Okay, that was not clear to me after reading your question. In that case, it might be a good idea to document your experience with whichever route you choose, so that it can serve as a warning to others :grinning_face_with_smiling_eyes:

Paolo Giarrusso said:

For composing functions of

`function A B`

type, I wonder if you could follow Haskell’s notation for the Arrow typeclass — assuming that`function`

is indeed a valid instance.

I believe that it is a valid instance, and it's very promising idea, actually . Thank you! :)

Will probably post about progress tomorrow.

You mean Arrows as in haskell/category theory? I don't think I've seen one.

https://gist.github.com/LessnessRandomness/2d0dc97fc348213e9c6626ca10ef06f7 - there's what I managed to achieve for now.

It looks promising for me, yay. :)

The code looks so nice…

I'll continue to play the devils advocate and point to what looks to be the weak spot to me: writing down expressions that involve several functions (i.e. your `combination`

). So my challenge would be to prove any (nontrivial) identity between (partial) functions in a way such that it is clear from the statement what the identity is. (Which is crucial in order to be able to use `Search`

to find the result).

https://gist.github.com/LessnessRandomness/1361447aebb18e80c52a6fcafa1440b4

I changed functional relation approach to the `A -> option B`

approach.

At the end, in the `Experimenting`

section I defined simple datatype `formula_of_one_variable`

for simple expressions of one variable, made some notations for it and defined transformation that makes it into `function`

. Then defined some notion of nontransitive equivalence (??) for partial functions and proved simple theorem that `x / x == 1`

.

Making the same thing but for many variable formulas will take some thinking, at least for me.

https://gist.github.com/LessnessRandomness/d82cd6597af4241aa14f96dd8f58aed8 - now I have partial multivariate functions in (almost) the same way.

I proved that `(x + y) * (x - y) / (x + y) == x - y`

as an example. Still thinking about notations, as one can see... in the place of `x`

and `y`

I have `var _ 0`

and `var _ 1`

, etc.

In that experiment, formula n ~= formula 0, right? Did you mean to enforce a match between n and the "number of free variables"?

you're encoding a simplified version of de Bruijn indexes from lambda calculus, but you could probably just use variable names, and a map instead of tuple n in transform.

Luckily for you, your language doesn't have anonymous functions/lambdas/... yet, so you don't need the complexities of lambda calculus.

Yes, formula n <> formula 0.

If there's `var i`

in the formula with `i`

bigger than `n`

then `nth_of_tuple`

returns `None`

and transformation returns, for example, function `λ _ : R * R * R, None`

.

Interesting. But it seems the types are still isomorphic. You're basically using a phantom type.

TIL what a phantom type is, cool. :) Yes, I agree now that `formula n`

is isomorphic to `formula 0`

.

This is probably more like math question... anyway, is it possible to prove theorem `function_limit_if_function_eq`

without hypothesis `subset (domain f2) (domain f1)`

? It seems obvious to me but I'm not successful.

If there's some counterexample or maybe you can find some error in definitions (it's possible, too), I will be grateful.

```
Require Import Reals Lra Field Classical IndefiniteDescription Utf8 Lia.
Open Scope R.
Set Implicit Arguments.
Definition set A := A → Prop.
Definition empty_set A: set A := λ x, False.
Definition full_set A: set A := λ x, True.
Definition union {A} (X Y: set A): set A := λ a, X a ∨ Y a.
Definition intersection {A} (X Y: set A): set A := λ a, X a ∧ Y a.
Definition difference {A} (X Y: set A): set A := λ a, X a ∧ ¬ Y a.
Definition disjoint {A} (X Y: set A): Prop := intersection X Y = @empty_set A.
Definition subset {A} (X Y: set A): Prop := ∀ x, X x → Y x.
Definition function A B := A → option B.
Notation "a ~> b" := (function a b) (at level 90, right associativity).
Definition domain {A B} (f: A ~> B): set A := λ x, ∃ y, f x = Some y.
Definition apply_function A B (f: A ~> B) x (H: domain f x): B.
Proof.
unfold domain in H. apply constructive_indefinite_description in H.
destruct H. exact x0.
Defined.
Inductive extendedR :=
| finite: forall (x: R), extendedR
| positive_infinity: extendedR
| negative_infinity: extendedR.
Definition epsilon := { eps: R | eps > 0 }.
Definition epsilon_proj1 (e: epsilon) := proj1_sig e.
Coercion epsilon_proj1: epsilon >-> R.
Definition neighbourhood (x: extendedR) (e: epsilon): set R :=
match x with
| finite a => λ i, a - e < i < a + e
| positive_infinity => λ i, / e < i
| negative_infinity => λ i, i < - / e
end.
Definition sequence A := nat → A.
Definition limit (s: sequence R) (A: extendedR) :=
∀ (eps: epsilon), ∃ n, ∀ m, (m > n)%nat → neighbourhood A eps (s m).
Definition function_limit (f: R ~> R) (x0 a: extendedR) :=
∀ (eps: epsilon), ∃ (delta: epsilon), ∀ (x: R) (H: domain f x),
neighbourhood x0 delta x → neighbourhood a eps (apply_function H).
Definition function_eq A B (f1 f2: A ~> B) := ∀ x, domain f1 x → domain f2 x → f1 x = f2 x.
Theorem function_limit_if_function_eq (f1 f2: R ~> R) (H: function_eq f1 f2) (x a: extendedR):
subset (domain f2) (domain f1) → function_limit f1 x a → function_limit f2 x a.
Proof.
intros. unfold function_limit in *. intros. destruct (H1 eps) as [delta H2].
exists delta. intros. pose proof (H0 _ H3). pose proof (H2 _ H5 H4).
assert (apply_function H3 = apply_function H5).
{ unfold function_eq in H. unfold apply_function.
repeat destruct constructive_indefinite_description.
pose proof (H x0 H5 H3). congruence. }
rewrite H7. auto.
Qed.
```

This is probably more like math question... anyway, is it possible to prove theorem `function_limit_if_function_eq`

without hypothesis `subset (domain f2) (domain f1)`

? It seems obvious to me but I'm not successful.

If there's some counterexample or maybe you can find some error in definitions (it's possible, too), I will be grateful.

```
Require Import Reals Lra Field Classical IndefiniteDescription Utf8 Lia.
Open Scope R.
Set Implicit Arguments.
Definition set A := A → Prop.
Definition empty_set A: set A := λ x, False.
Definition full_set A: set A := λ x, True.
Definition union {A} (X Y: set A): set A := λ a, X a ∨ Y a.
Definition intersection {A} (X Y: set A): set A := λ a, X a ∧ Y a.
Definition difference {A} (X Y: set A): set A := λ a, X a ∧ ¬ Y a.
Definition disjoint {A} (X Y: set A): Prop := intersection X Y = @empty_set A.
Definition subset {A} (X Y: set A): Prop := ∀ x, X x → Y x.
Definition function A B := A → option B.
Notation "a ~> b" := (function a b) (at level 90, right associativity).
Definition domain {A B} (f: A ~> B): set A := λ x, ∃ y, f x = Some y.
Definition apply_function A B (f: A ~> B) x (H: domain f x): B.
Proof.
unfold domain in H. apply constructive_indefinite_description in H.
destruct H. exact x0.
Defined.
Inductive extendedR :=
| finite: forall (x: R), extendedR
| positive_infinity: extendedR
| negative_infinity: extendedR.
Definition epsilon := { eps: R | eps > 0 }.
Definition epsilon_proj1 (e: epsilon) := proj1_sig e.
Coercion epsilon_proj1: epsilon >-> R.
Definition neighbourhood (x: extendedR) (e: epsilon): set R :=
match x with
| finite a => λ i, a - e < i < a + e
| positive_infinity => λ i, / e < i
| negative_infinity => λ i, i < - / e
end.
Definition sequence A := nat → A.
Definition limit (s: sequence R) (A: extendedR) :=
∀ (eps: epsilon), ∃ n, ∀ m, (m > n)%nat → neighbourhood A eps (s m).
Definition function_limit (f: R ~> R) (x0 a: extendedR) :=
∀ (eps: epsilon), ∃ (delta: epsilon), ∀ (x: R) (H: domain f x),
neighbourhood x0 delta x → neighbourhood a eps (apply_function H).
Definition function_eq A B (f1 f2: A ~> B) := ∀ x, domain f1 x → domain f2 x → f1 x = f2 x.
Theorem function_limit_if_function_eq (f1 f2: R ~> R) (H: function_eq f1 f2) (x a: extendedR):
subset (domain f2) (domain f1) → function_limit f1 x a → function_limit f2 x a.
Proof.
intros. unfold function_limit in *. intros. destruct (H1 eps) as [delta H2].
exists delta. intros. pose proof (H0 _ H3). pose proof (H2 _ H5 H4).
assert (apply_function H3 = apply_function H5).
{ unfold function_eq in H. unfold apply_function.
repeat destruct constructive_indefinite_description.
pose proof (H x0 H5 H3). congruence. }
rewrite H7. auto.
Qed.
```

I think your definition of `function_eq f1 f2`

, i.e.`domain f1 x → domain f2 x → f1 x = f2 x`

is too weak to remove the hypothesis about domains. Suppose f1 and f2 have completely disjoint domain: they would be `function_eq`

-equal but have no reason to share limits.

Last updated: Jan 28 2023 at 05:02 UTC