Reasoning about domains of partial functions · Coq users

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

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.

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

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

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

Lessness (Jun 28 2021 at 10:56):

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

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

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

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