## Stream: math-comp analysis

### Topic: using near

#### Marie Kerjean (Nov 25 2020 at 20:31):

Is there a lemma stating`forall e, 0< e -> x \is_near (nbhs 0)) -> `|x| < e` in a normed vector space ?

#### Cyril Cohen (Nov 25 2020 at 22:44):

Marie Kerjean said:

Is there a lemma stating`forall e, 0< e -> x \is_near (nbhs 0)) -> `|x| < e` in a normed vector space ?

No, I think it is missing, but it should definitely be added! (the proof should be a one-liner)

#### Cyril Cohen (Nov 25 2020 at 22:50):

``````Lemma nbhs0_lt  (R : numFieldType) (V : normedModType R) e :
0 < e -> \forall x \near (nbhs (0 : V)), `|x| < e.
Proof.
move=> e_gt0; apply/nbhs_ballP; exists e => // x.
by rewrite -ball_normE /= sub0r normrN.
Qed.
``````

#### Marie Kerjean (Nov 26 2020 at 10:53):

Another question on the use of near. After discharging

``````e : (R[i])^o
_Hyp_ : e \is_near (nbhs (nbhs' 0))
``````

I get a locked goal :

``````locked_with near_key (forall x0 : (R[i])^o, x0 \is_near (nbhs (nbhs' 0)) -> `|x0| <r)
``````

I cannot apply the previous lemmas and rewriting through `rewrite locked_withE` gets me at strange places (where there are mismatches on `@default_arrow_filter` types) . Any insight about what I should do ? Is that because of the use of `nbhs'`?

#### Cyril Cohen (Nov 26 2020 at 11:01):

which tactic / line of tactics did you use to get the `locked_with` (you are now supposed to get there)

#### Marie Kerjean (Nov 26 2020 at 11:11):

I have a goal `|e| <r` on which I use the tactic `near: e`.

#### Marie Kerjean (Nov 27 2020 at 08:57):

Is the tactic correct ? Could the fact that `locked_with` is appearing be a consequence of a bad join/type structure on `R[i]` ?

#### Cyril Cohen (Nov 27 2020 at 08:59):

can you point me to a branch where this happens?

#### Cyril Cohen (Nov 27 2020 at 12:01):

I will take a look

#### Cyril Cohen (Nov 27 2020 at 12:30):

So, here is the explanation:

#### Cyril Cohen (Nov 27 2020 at 12:31):

there seems to a bug in `near:`, the call to `near: e` should have failed with error message : `impossible to infer r that does not depend on e, you might want to generalize r (as in move: r e) or introduce r before using near=> e`.

#### Cyril Cohen (Nov 27 2020 at 12:31):

you could then do `move: r r0; near: e`, but I expect you will fail...

#### Cyril Cohen (Nov 27 2020 at 12:34):

I do not understand how this proof though ....

#### Marie Kerjean (Nov 27 2020 at 12:53):

So I shouldn' t use `near: e` on a goal containing free variables triggering constraints on `e` ?

#### Marie Kerjean (Nov 27 2020 at 12:54):

Cyril Cohen said:

I do not understand how this proof though ....

I'm not sure In understand your comment.

#### Cyril Cohen (Nov 27 2020 at 13:01):

Marie Kerjean said:

Cyril Cohen said:

I do not understand how this proof though ....

I'm not sure In understand your comment.

I do not understand ~how~ this proof ~works~ though ....

#### Cyril Cohen (Nov 27 2020 at 13:02):

Marie Kerjean said:

So I shouldn' t use `near: e` on a goal containing free variables triggering constraints on `e` ?

Sure, you cannot say a `e` should be bigger/smaller than a quantity that depends on `e`... that would be a circular dependency and it is forbidden.

#### Marie Kerjean (Nov 27 2020 at 13:03):

of course, thanks !

Last updated: Feb 05 2023 at 06:28 UTC