Ssreflect Users Discussion List

[Georges Gonthier <>]

  There’s a low-tech solution to your problem: parametrize your semigroup structure by a list of booleans, one for each property. The obvious

downside is that you’ll need to declare a bool list variable alongside sg (and possibly other boolean variables if you’re skipping properties).

  There’s probably a high-tech solution using nested structures, but I’d have to think it over (depends on whether you want to unify constraints,

for example).

 

Georges

 

 

---

From: Arthur Azevedo de Amorim [mailto:]
Sent: 16 June 2009 21:35
To: Laurence Rideau
Cc:
Subject: Re: [Fwd: Re: Automatic proofs of is_true]

 

Thanks for your answers, but I think that I haven't expressed myself correctly. I will try to explain the problem without getting into too much detail.

In our development, we have a type for semigroups and another type that enumerates some basic semigroup properties, e.g. HasIdentity, IsCommutative, HasAnnihilator and so on. We have also defined a semantics for each of these constants, which is a function with type property -> semigroup -> Prop. The reason for doing this is that we can compute symbolically which properties are valid for some semigroups.

I wanted to be able to write a generic algebra library for these structures. The problem is that the structures we work with can have many different combinations of properties, making it unpractical to write a coerent hierarchy of algebraic structures such as that of ssralg. However, in one part of our code we enrich the type of semigroups with a list of properties and a proof that that list contains only properties that are valid for that semigroup. I thought that it would be possible to use that to specify on which kind of structure each lemma works, something like this:

Section sg.

Variable sg : semigroup (HasIdentity :: IsCommutative :: nil).

Lemma l1 : ...
Lemma l2 : ...

End sg.

And then, later use one of those lemmas transparently with another structure that has more properties, such as a
semigroup (HasIdentity :: IsCommutative :: IsCancelative :: nil).

Therefore, I thought that if something similar existed in ssr, I would be able to adapt it to this case. That's why I asked if we could get "transparent" coercions in that case. The notation suggestion seems pretty satisfatory!

Cheers

On Tue, Jun 16, 2009 at 5:50 PM, Laurence Rideau <> wrote:

my answer to Arthur (forgot to reply "All"...sorry)
laurence


Arthur Azevedo de Amorim wrote:

Hello everyone,

is there a way in plain ssr to cast between I_n and I_m when (n <= m) is convertible to true without mentioning explicitly its proof, e.g, when using a value of I_3 in a context that asks for an I_5 without calling widen_ord and passing it (refl_equal _)?

Thanks in advance.

--
Arthur Azevedo de Amorim

Hello Arthur,
the lift function (of type  forall m n : nat, 'I_m -> 'I_(m + n)) from fintype.v should answer your question.
cheers
laurence

--
Arthur Azevedo de Amorim