Checking whether some type is some instance · Hierarchy Builder devs & users

Stream: Hierarchy Builder devs & users

Topic: Checking whether some type is some instance

Laurent Théry (Apr 01 2021 at 14:50):

Just I was doing the example about ring and somewhere it says

(* Now Z is recognized as a Ring *)
Goal forall x : Z, x * - (1 + x) = 0 + 1.

but actually this d oes not need to have ring forZ. So I was searching as a way to check that Z is recognized as a ring

Enrico Tassi (Apr 01 2021 at 14:50):

Coq-Elpi can only support abbreviations, that is Notation ident args := term. They have the same "power" of the other notations, in the sense that you can define all the phantom magic stuff, but are much much simpler to build. So you will have to use Coq to attach to that ident a more fancy notation.

Enrico Tassi (Apr 01 2021 at 14:51):

In which notation scope are you?

Laurent Théry (Apr 01 2021 at 14:52):

I am doing CoqWs_demo.v

Enrico Tassi (Apr 01 2021 at 14:53):

That file define notations for *, +... for the ring operations. Did you open Z_scope?

Enrico Tassi (Apr 01 2021 at 14:56):

I mean, Set Printing All should show mul Z_canonical_Ring x ...

Laurent Théry (Apr 01 2021 at 14:57):

nop the file does not mention any scope. https://github.com/math-comp/hierarchy-builder/blob/master/examples/Coq2020_material/CoqWS_demo.v

Enrico Tassi (Apr 01 2021 at 14:57):

What does Set Prinnting All show?

Laurent Théry (Apr 01 2021 at 14:59):

I have commented the ring declaration and it still works. I get

@eq (SemiRing.sort Z_canonical_SemiRing)
  (@mul Z_canonical_SemiRing x
     (@opp Z_canonical_AbelianGrp
        (@add (SemiRing_to_CMonoid Z_canonical_SemiRing) (@one Z_canonical_SemiRing) x)))
  (@add (SemiRing_to_CMonoid Z_canonical_SemiRing)
     (@zero (SemiRing_to_CMonoid Z_canonical_SemiRing)) (@one Z_canonical_SemiRing))```

Cyril Cohen (Apr 01 2021 at 15:02):

The notations are declared earlier in the file in the empty scope (thus taking precedence over Z_scope)

Enrico Tassi (Apr 01 2021 at 15:02):

Yes, because all the operations you use are already there (in the group or semiring) and I guess that unification is smart/lucky enough.
If you remove : Z on the variables, you should get an error, since there will be no known structure with all the operations you use.

Cyril Cohen (Apr 01 2021 at 15:02):

I do not understand how you can get this line working without the instances...

Laurent Théry (Apr 01 2021 at 15:03):

I have the instances but not the ring structure

Enrico Tassi (Apr 01 2021 at 15:03):

I think the magic is that SemiRingsort Z_canonical_SemiRing = AbelianGrp.sort ? is solved by unfolding the LHS and finding Z.

Cyril Cohen (Apr 01 2021 at 15:03):

The ring instance is obtained automatically from semiring and group

Enrico Tassi (Apr 01 2021 at 15:03):

for which Laurent has an instance

Enrico Tassi (Apr 01 2021 at 15:04):

what he lacks is the join, and he needs it only for an unknown type

Enrico Tassi (Apr 01 2021 at 15:05):

If you remove Z_canonical_SemiRing from the previous equation, then you really need to compute the pullback (you need the join struture)

Enrico Tassi (Apr 01 2021 at 15:05):

Can you please try Laurent?

Enrico Tassi (Apr 01 2021 at 15:06):

Goal forall x : _, x * - (1 + x) = 0 + 1.

Enrico Tassi (Apr 01 2021 at 15:06):

With the ring structure, this has a solution

Enrico Tassi (Apr 01 2021 at 15:06):

without, it does not

Cyril Cohen (Apr 01 2021 at 15:06):

@Laurent Théry to check the existence of the instance you can use

Check [the Ring.type of Z : Type].

Enrico Tassi (Apr 01 2021 at 15:06):

(he removed the structure)

Cyril Cohen (Apr 01 2021 at 15:06):

How?

Cyril Cohen (Apr 01 2021 at 15:07):

Ah ok I get it now!!!

Enrico Tassi (Apr 01 2021 at 15:07):

with (* ... *) ;-)

Enrico Tassi (Apr 01 2021 at 15:07):

Or at least, this is my understanding

Enrico Tassi (Apr 01 2021 at 15:07):

In any case, you should split the thread again

Laurent Théry (Apr 01 2021 at 15:07):

I am a bit puzzled what I understood is that Z now works as a kind of join between SemiRIng and Abelian so that is why your example works even if there is not the Ring Structure. Correct?

Cyril Cohen (Apr 01 2021 at 15:09):

I think that, as Enrico explained, the join does not need to exist because the structure is concrete and the unification unfold sort projections to find it...

Enrico Tassi (Apr 01 2021 at 15:10):

yes, you happen to have a concrete join, but not an abstract one.

Cyril Cohen (Apr 01 2021 at 15:11):

for example

Check forall x, x * - (1 + x) = 0 + 1.

will succeed only if you have the Ring structure

Cyril Cohen (Apr 01 2021 at 15:12):

That's what Enrico said :laughter_tears:

Cyril Cohen (Apr 01 2021 at 15:12):

I'm just 10min late

Laurent Théry (Apr 01 2021 at 15:12):

So to come back to my initial question I wanted to have a quick way to check when a concrete stuff can be seen as a structure

Enrico Tassi (Apr 01 2021 at 15:12):

Maybe this one is more clear

Enrico Tassi (Apr 01 2021 at 15:12):

You cannot write this forall r : S, x : S.sort r, x * - .... if you don't have a proper S

Enrico Tassi (Apr 01 2021 at 15:13):

This is what I mean by abstract

Cyril Cohen (Apr 01 2021 at 15:13):

Cyril Cohen said:

Laurent Théry to check the existence of the instance you can use
Check [the Ring.type of Z : Type].

@Laurent Théry is this what you were looking for? Checking whether some structure is instanciated on some type?

Enrico Tassi (Apr 01 2021 at 15:14):

Also Ring.on Z should work

Cyril Cohen (Apr 01 2021 at 15:14):

(Initially you wrote So I was searching as a way to check that Z is recognized as a ring)

Laurent Théry (Apr 01 2021 at 15:21):

Sorry about the confusion. So without the ring forall x : Z, x * - (1 + x) = 0 + 1. works but with the ring now forall x, x * - (1 + x) = 0 + 1 :>Z. works.
But yes Ring.on _ and `[the Ring.type of : _[ is what I was searching. Thanks

Enrico Tassi (Apr 01 2021 at 15:22):

I hope it works even without the :> Z

Laurent Théry (Apr 01 2021 at 15:22):

without it does not know the ring

Enrico Tassi (Apr 01 2021 at 15:23):

Goal will not work, but Check will, this is what I meant, sorry for the confusion

Enrico Tassi (Apr 01 2021 at 15:24):

I'm afraid I misunderstood the problem by reading Check and not Goal

Enrico Tassi (Apr 01 2021 at 15:24):

So yes, Goal needs to find a ring instance because the statement cannot contain unresolved evars

Enrico Tassi (Apr 01 2021 at 15:25):

While Check does not have this requirement

Laurent Théry (Apr 01 2021 at 15:25):

Yes, I had the same problem before on the file. I found it disturbing that Lemma and Checkdoes not behave the same.

Enrico Tassi (Apr 01 2021 at 15:26):

Maybe Program Lemma ;-)

Enrico Tassi (Apr 01 2021 at 15:26):

(I don't think it works)

Laurent Théry (Apr 01 2021 at 15:35):

Just to really understand in the file ssralg in the port. You have

Notation "[ 'zmodType' 'of' T 'for' cT ]" := (@Zmodule.clone T cT)
  (at level 0, format "[ 'zmodType'  'of'  T  'for'  cT ]") : form_scope.
Notation "[ 'zmodType' 'of' T ]" :=  (@Zmodule.clone T _)
  (at level 0, format "[ 'zmodType'  'of'  T ]") : form_scope.
``` .
So it is not cmpletly equivalent to `Zmodule.on` or `[the Zmodule.type ..]`

Enrico Tassi (Apr 01 2021 at 15:36):

IIRC S.on X = S.clone X _

Enrico Tassi (Apr 01 2021 at 15:38):

My understanding is that clone A B infers on A and uses the infrred to build a structure on B, if you don't give B I guess unification picks A.

Enrico Tassi (Apr 01 2021 at 15:39):

I guess A and B must be convertible in general

Cyril Cohen (Apr 01 2021 at 15:53):

Enrico Tassi said:

IIRC S.on X = S.clone X _

Nop... S.on X = S.copy X _

Cyril Cohen (Apr 01 2021 at 15:53):

S.clone T T' has type S.type and simulate the old clone

Cyril Cohen (Apr 01 2021 at 15:56):

The difference between [zmodType of T] and [the zmodType of T] is that the former will fail if the canonical instance on T is abstract (no Pack constructor) as in fun T : zmodType => [zmodType of T] (the cloning is "deep"), while the latter will just pick it...

Last updated: May 28 2023 at 18:29 UTC