Stream: Coq users

Topic: Reasoning about domains of partial functions


view this post on Zulip 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).

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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”.

view this post on Zulip 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.

view this post on Zulip 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, ...

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Christian Doczkal (Jun 27 2021 at 17:38):

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

view this post on Zulip 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. :)

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Bas Spitters (Jun 28 2021 at 06:02):

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

view this post on Zulip 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. :)

view this post on Zulip Ignat Insarov (Jun 28 2021 at 14:43):

The code looks so nice…

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 03 2021 at 21:47):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jan 28 2023 at 05:02 UTC