## Stream: Coq users

### Topic: Reasoning about domains of partial functions

#### Lessness (Jun 26 2021 at 18:31):

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).

#### Lessness (Jun 26 2021 at 18:38):

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.

#### Paolo Giarrusso (Jun 27 2021 at 01:33):

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.

#### Paolo Giarrusso (Jun 27 2021 at 01:39):

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”.

#### Paolo Giarrusso (Jun 27 2021 at 01:42):

“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.

#### Bas Spitters (Jun 27 2021 at 10:04):

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

#### Lessness (Jun 27 2021 at 17:32):

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

#### Paolo Giarrusso (Jun 27 2021 at 17:36):

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:

#### Christian Doczkal (Jun 27 2021 at 17:36):

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.

#### Christian Doczkal (Jun 27 2021 at 17:38):

The prime example is subtraction on `nat`, which satisfies `n - m = 0` whenever `n <= m`.

#### Lessness (Jun 27 2021 at 18:11):

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

Thank you, anyway. :)

#### Christian Doczkal (Jun 27 2021 at 18:19):

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:

#### Lessness (Jun 27 2021 at 21:13):

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.

#### Bas Spitters (Jun 28 2021 at 06:02):

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

#### Lessness (Jun 28 2021 at 10:56):

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

It looks promising for me, yay. :)

#### Ignat Insarov (Jun 28 2021 at 14:43):

The code looks so nice…

#### Christian Doczkal (Jun 28 2021 at 17:32):

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).

#### Lessness (Jul 01 2021 at 01:10):

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.

#### Lessness (Jul 03 2021 at 19:57):

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.

#### Paolo Giarrusso (Jul 03 2021 at 21:31):

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

#### Paolo Giarrusso (Jul 03 2021 at 21:32):

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.

#### Paolo Giarrusso (Jul 03 2021 at 21:35):

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

#### Lessness (Jul 03 2021 at 21:42):

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`.

#### Paolo Giarrusso (Jul 03 2021 at 21:47):

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

#### Lessness (Jul 03 2021 at 21:52):

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

#### Lessness (Jul 12 2021 at 13:18):

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.
``````

#### Lessness (Jul 12 2021 at 13:19):

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.
``````

#### Pierre Courtieu (Jul 12 2021 at 13:26):

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: Jun 18 2024 at 20:02 UTC