Not quite; the idea is more
to have
Structure semigroup
(sg_plist : list bool) :=
…
sg_valid : foldr and True (sieve sg_plist (sem_props sg_op))
}
where sem_props is a list of standard
properties of a semigroup. If the first one is has_unit, and the
second on commutativity, then you would
quantify over a semigroup with a unit with
Variables (sgp : seq bool) (sg :
semigroup (true :: sgp)).
and a commutative one with
Variables (sgu : bool) (sgp : seq
bool) (sg : semigroup (sgu :: true :: sgp)).
The bool lists simply unify pointwise; implied
properties should be precomputed when structures are constructed.
It’s possible to compute boolean
sequence patterns from symbol lists; you’ll still need a supply of bool
variables, though.
Georges
From:
Arthur Azevedo de Amorim [mailto:]
Sent: 17 June 2009 14:12
To: Georges
Gonthier
Cc: Laurence Rideau;
Subject: Re: [Fwd: Re: Automatic
proofs of is_true]
I think that this
actually might be related to what we have already. Our structure looks
something like this:
Structure semigroup : Type :=
sg_carrier : Type;
sg_op : bin_op sg_carrier;
sg_assoc : associative sg_op;
sg_plist : list sg_prop;
sg_valid : forall p, has p sg_plist -> prop_sem p sg_op sg_assoc
}.
So we enrich this base type with the property list as a type parameter that
expresses that at least some properties (IsCommutative and HasIdentity in the
example above) are present in the property list sg_plist. Actually, the
semigroup type in the previous message is called psemigroup, an annotated
version defined on top of the one I've defined here. Giving the list sg_plist
when building an instance is not too cumbersome because the whole list is
inferred by a function. Is this close to what you meant, Georges?
Anyway, even with the list of boolean values, wouldn't it still be necessary to
give (refl_equal true) explicitly in order to show that one list implies the
other one and thus be able to coerce between the two types?
On Wed, Jun 17, 2009 at 12:32 PM, Georges
Gonthier <>
wrote:
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
--
Arthur Azevedo de Amorim
