Stream: math-comp users

Topic: completeNormedModType of matrix


view this post on Zulip Xiaoquan Xu (Feb 23 2024 at 12:40):

I found that matrix 'M[R](m.+1,n.+1) can already pass the Check for completeType and NormedModType R, but it fails the Check for completeNormedModType R. So why this happens? Btw, is there any manual approaches to declare a type that inherits from two base classes without any mixin like this?

From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.analysis Require Import reals topology normedtype.

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

Import Order Order.Theory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.

Local Open Scope ring_scope.

Section Debug.

Variables (R: realType).

Variables (m n: nat).

Check 'M[R]_(m.+1, n.+1): completeType.
Check 'M[R]_(m.+1, n.+1): normedModType R.
Check 'M[R]_(m.+1, n.+1): completePseudoMetricType R.
Check 'M[R]_(m.+1, n.+1): pseudoMetricType R.

(*Why this fails*)
Fail Check 'M[R]_(m.+1, n.+1): completeNormedModType R.

End Debug.

view this post on Zulip Notification Bot (Feb 23 2024 at 12:41):

Xiaoquan Xu has marked this topic as resolved.

view this post on Zulip Notification Bot (Feb 23 2024 at 12:41):

Xiaoquan Xu has marked this topic as unresolved.

view this post on Zulip Xiaoquan Xu (Feb 23 2024 at 13:23):

I temporarily solved the problem with the following Canonical command, but still cannot understand why it can't be automatically recognized.

Canonical mx_comp := CompleteNormedModule.Pack
  (CompleteNormedModule.Class
  (PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R 'M[R]_(m.+1, n.+1)
  (@mx_normZ _ _ _))
  (Uniform_isComplete.Build 'M[R]_(m.+1, n.+1) (@mx_complete _ _ _))
  ).

 Check 'M[R]_(m.+1, n.+1): completeNormedModType R.

view this post on Zulip Cyril Cohen (Feb 26 2024 at 12:20):

This looks like a missing join.

view this post on Zulip Li Zhou (Feb 26 2024 at 18:31):

But a similar thing works for (R : realType) itself.
Following is the code in normedtype.v:

HB.instance Definition _ (R : realType) := Uniform_isComplete.Build R^o
  (@R_complete R). (* todo : delete *)

HB.instance Definition _ (R : realType) := Complete.copy R
  [the completeType of R^o].
(* new *)

These are already sufficient to make Check R : completeNormedModType R pass.


Last updated: Jul 25 2024 at 17:02 UTC