Stream: math-comp users

Topic: from telescopes to packaged structures

Christian Doczkal (Jul 16 2020 at 19:15):

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

Cyril Cohen (Jul 17 2020 at 20:00):

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?

Christian Doczkal (Jul 17 2020 at 20:12):

Well, it could be a subType except for:

1. the predicate with denoting special elements is not a boolean predicate. It is phrased as an equivalence of the underlying setoid.
2. 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.

Cyril Cohen (Jul 17 2020 at 20:16):

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

Christian Doczkal (Jul 17 2020 at 20:19):

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.

Christian Doczkal (Jul 17 2020 at 20:26):

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:

Enrico Tassi (Jul 17 2020 at 20:27):

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.

Cyril Cohen (Jul 17 2020 at 20:29):

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

Christian Doczkal (Jul 17 2020 at 20:32):

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

Cyril Cohen (Jul 17 2020 at 20:55):

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

Cyril Cohen (Jul 17 2020 at 20:55):

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

Christian Doczkal (Jul 18 2020 at 08:41):

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

Christian Doczkal (Jul 20 2020 at 15:57):

@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: Oct 13 2024 at 01:02 UTC