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`

for`Z`

. So I was searching as a way to check that Z is recognized as a ring

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.

In which notation scope are you?

I am doing `CoqWs_demo.v`

That file define notations for `*`

, `+`

... for the ring operations. Did you open Z_scope?

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

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

What does `Set Prinnting All`

show?

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))```
```

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

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.

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

I have the instances but not the ring structure

I think the magic is that `SemiRingsort Z_canonical_SemiRing = AbelianGrp.sort ?`

is solved by unfolding the LHS and finding Z.

The ring instance is obtained automatically from semiring and group

for which Laurent has an instance

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

If you remove `Z_canonical_SemiRing`

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

Can you please try Laurent?

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

With the ring structure, this has a solution

without, it does not

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

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

(he removed the structure)

How?

Ah ok I get it now!!!

with `(* ... *)`

;-)

Or at least, this is my understanding

In any case, you should split the thread again

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?

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...

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

for example

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

will succeed only if you have the Ring structure

That's what Enrico said :laughter_tears:

I'm just 10min late

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

Maybe this one is more clear

You cannot write this `forall r : S, x : S.sort r, x * - ....`

if you don't have a proper `S`

This is what I mean by abstract

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?

Also `Ring.on Z`

should work

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

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

I hope it works even without the `:> Z`

without it does not know the ring

`Goal`

will not work, but `Check`

will, this is what I meant, sorry for the confusion

I'm afraid I misunderstood the problem by reading `Check`

and not `Goal`

So yes, `Goal`

needs to find a ring *instance* because the statement cannot contain unresolved evars

While `Check`

does not have this requirement

Yes, I had the same problem before on the file. I found it disturbing that `Lemma`

and `Check`

does not behave the same.

Maybe `Program Lemma`

;-)

(I don't think it works)

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 ..]`
```

IIRC `S.on X = S.clone X _`

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`

.

I guess `A`

and `B`

must be convertible in general

Enrico Tassi said:

IIRC

`S.on X = S.clone X _`

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

`S.clone T T'`

has type `S.type`

and simulate the old clone

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