I am currently refactoring a development, trying to move from telescopes to packaged structures (using Hierarchy Builder). Until now we had the following telescope chain for some algebra modulo setoid equivalence: `Type < setoid < operations < axioms`

. The split between `operations`

and `axioms`

allows us to define notations for the the operations before specifying the axioms. This part was (easily) transferred to packaged structures using HB (i.e, one mixin each for `setoid`

, `operations`

, and `axioms`

).

Some parts of the existing proof single out elements satisfying a given property:

```
Record special (X : axioms) := Special { elem :> X ; _ : is_special elem}
```

Through the coercion from `special X`

to `X`

, one can state properties of special elements using the operations of the algebra and prove them using both their special properties and the generic properties of the algebra.

What is the easiest way to obtain the same behavior in the packaged approach? I would like to avoid defining another class, because this "sigma-type" would be the only instance. I tried defining three coercions from `special X`

to `axioms.sort`

, `operations.sort`

, and `setoid.sort`

. While this allows me to write down statements involving both operations and the underlying equivalence, this means that rewrite will treat multiple occurrences of some `a : special X`

as different, depending on whether it's an argument to an operation or to the equivalence (the coercions are convertible but not syntactically equal).

Hi @Christian Doczkal this looks a lot like a `subType`

(or perhaps the join of a `subType`

with `axioms`

) to me. Could you point me towards the relevant piece of code?

Well, it could be a `subType`

except for:

- the predicate with denoting
`special`

elements is not a boolean predicate. It is phrased as an equivalence of the underlying setoid. - I actually don't care whether the singled out elements form a subalgebra or not. In particular, I do not want to define new operations acting on those special elements. I would like special elements to be typed like normal ones - except that they satisfy their special property.

So basically, if every occurrence of`a : special X`

in a context requiring an object with a types of the shape`Setoid.sort _`

,`Ops.sort _`

, or`Axioms.sort _`

would trigger the insertion of the`elem`

projection and then trigger the structures defined for`X:Axioms.type`

, I would be entirely happy.

I am not sure what the problem is exactly... can you show me a piece of code with undesired behaviour?

After some trial, error, and frustration, I ended up turning the special elements into a class. This works pretty well, but it has the drawback that instead of `Implicit Type a b : special X`

and `Lemma foo a : _`

I need to write `Lemma foo (x : X) of is_special x : _`

On the other hand, this allows discovering "on the fly" that certain subexpressions are `special`

.

Cyril Cohen said:

I am not sure what the problem is exactly... can you show me a piece of code with undesired behaviour?

The code that didn't work has been replaced by code that does work, even if it needs type classes and a few manual casts. I could build minimal example, because I am interested in exploring other solutions. Though not tonight :upside_down:

We did chat in the afternoon. My understanding is that it is not a real subtype and it is not a real structure either (at least for some time)... so the TC thing may be OK, and eventually it can become a full instance.

Ok, so it may make sense it's not even part of a hierarchy...

Not it's not. In fact I do carve out the type of special elements because those form a commutative monoid that I need elsewhere. They also form a (somewhat degenerate) subalgebra, but that's neither interesting nor necessary. The condition for `special`

is literally that one of the operations of the algebra is the identity, causing two of the other operations to coincide. (One of them being commutative and the other one being associative.)

I would be so happy with a concrete example (whatever the style of the code)

even broken code, I just want to get a feel of the mathematical properties of `is_special`

Well, here is the code before trying to move from telescopes to packaged structures: pttdom.v. The "special" elements are those we call `test`

.

@Cyril Cohen And here is the same file on the branch that uses a HB-generated packaged hierarchy: pttdom.v.

As one can see, I define

```
Record test (X:pttdom) := Test{ elem_of :> X ; testP : is_test elem_of }
```

However, since `test`

is not part of the hierarchy, an element of type `a: test X`

applied to say `dom: forall s : Ops.type, s -> s`

, triggers the unification problem `test X =? Ops.sort ?x`

, which cannot be resolved, and also does not trigger the insertion of the `elem_of`

coercion. So I have to manually insert `elem_of`

in various places.

```
Lemma foo (X : pttdom) (a : test X) : dom (elem_of a) ≡ (elem_of a).
```

This isn't terrible, but slightly annoying, in particular when defining term normalization

Last updated: Jan 29 2023 at 19:02 UTC