Zulip Chat Archive

I'm stuck on something probably really stupid: --> isn't available after From mathcomp.analysis Require Import topology sequences.

From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.analysis Require Import topology sequences.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Scope ring_scope.

Section First.

Variable RR: realFieldType.

Variable r: RR.

Lemma geom_infty: (r > 1) -> (geometric 1 r) --> +oo.
Proof.

Qed.

End First.

Reynald Affeldt (Sep 22 2022 at 23:58):

This notation is in the scope classical_set_scope. This can be observed by looking at its definition in topology.v.

Reynald Affeldt (Sep 23 2022 at 00:10):

so maybe Require Import classical_sets and open scope, but then you may also need Require Import normedtype and Import numFieldNormedType.Exports to type check the --> +oo notation.

Julien Puydt (Sep 23 2022 at 14:31):

Ah, that's better, but I'm still not there yet: now geometric 1 r and +oo and --> are recognized, but the types don't match!

From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.analysis Require Import normedtype topology sequences.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Scope classical_set_scope.
Open Scope ring_scope.

Section First.

Variable RR: realFieldType.

Variable r: RR.

Lemma geom_infty: (r > 1) -> (geometric 1 r) --> +oo.
Proof.

Qed.

End First.

abab9579 (Sep 23 2022 at 19:51):

Julien Puydt (Sep 24 2022 at 07:17):

What do you mean by "requires realType"? As far as I understand, that's what I have and the error message isn't about +oo but about geometric:

In environment
RR : realFieldType
r : RR
The term "Phantom (RR) ^nat (geometric 1 r)" has type
 "phantom (sequence (GRing.Field.sort (Num.RealField.fieldType RR)))
    (@geometric (Num.RealField.fieldType RR)
       (GRing.one (GRing.Field.ringType (Num.RealField.fieldType RR))) r)"
while it is expected to have type "phantom (@Filtered.sort ?X ?fX) ?x".

abab9579 (Sep 24 2022 at 07:37):

I mean it should be RR: realType not RR: realFieldType. realFieldType does not even have filteredtype struture, so you cannot use topological reasoning like --> +oo.

Julien Puydt (Sep 26 2022 at 06:49):

@abab9579 Changing to RR: realType means I also have to require import reals, but doesn't solve the problem. I posted my whole file to show the problem ; if you have a solution, can you also post it in full?

Cyril Cohen (Sep 26 2022 at 08:37):

As @Reynald Affeldt pointed out there were a few missing imports (namelyclassical_sets and numFieldNormedType.Exports) to make it work:

From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp Require Import boolp classical_sets.
From mathcomp Require Import normedtype topology sequences.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Scope classical_set_scope.
Open Scope ring_scope.

Import numFieldNormedType.Exports.

Section First.

Variable RR: realFieldType.

Variable r: RR.

Lemma geom_infty: (r > 1) -> (geometric 1 r) --> +oo.
Proof.
Qed.

End First.

Stream: math-comp analysis

Topic: Unknown notation --> ?

Julien Puydt (Sep 22 2022 at 12:24):