Stream: Hierarchy Builder devs & users

Topic: Checking whether some type is some instance


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

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 14:51):

In which notation scope are you?

view this post on Zulip Laurent Théry (Apr 01 2021 at 14:52):

I am doing CoqWs_demo.v

view this post on Zulip Enrico Tassi (Apr 01 2021 at 14:53):

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 14:56):

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

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 14:57):

What does Set Prinnting All show?

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

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

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

view this post on Zulip Cyril Cohen (Apr 01 2021 at 15:02):

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

view this post on Zulip Laurent Théry (Apr 01 2021 at 15:03):

I have the instances but not the ring structure

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

view this post on Zulip Cyril Cohen (Apr 01 2021 at 15:03):

The ring instance is obtained automatically from semiring and group

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:03):

for which Laurent has an instance

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:04):

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

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:05):

Can you please try Laurent?

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:06):

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:06):

With the ring structure, this has a solution

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:06):

without, it does not

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:06):

(he removed the structure)

view this post on Zulip Cyril Cohen (Apr 01 2021 at 15:06):

How?

view this post on Zulip Cyril Cohen (Apr 01 2021 at 15:07):

Ah ok I get it now!!!

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:07):

with (* ... *) ;-)

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:07):

Or at least, this is my understanding

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:07):

In any case, you should split the thread again

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

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:10):

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

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

view this post on Zulip Cyril Cohen (Apr 01 2021 at 15:12):

That's what Enrico said :laughter_tears:

view this post on Zulip Cyril Cohen (Apr 01 2021 at 15:12):

I'm just 10min late

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:12):

Maybe this one is more clear

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:13):

This is what I mean by abstract

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:14):

Also Ring.on Z should work

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

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:22):

I hope it works even without the :> Z

view this post on Zulip Laurent Théry (Apr 01 2021 at 15:22):

without it does not know the ring

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:23):

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:24):

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:24):

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:25):

While Check does not have this requirement

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:26):

Maybe Program Lemma ;-)

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:26):

(I don't think it works)

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:36):

IIRC S.on X = S.clone X _

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 15:39):

I guess A and B must be convertible in general

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

view this post on Zulip Cyril Cohen (Apr 01 2021 at 15:53):

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

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