I'm trying to get some simple automation for reasoning about finite sets (using @Arthur Azevedo de Amorim 's `extructures`

). My idea for a first attempt was to use `aac-tactics`

to normalise expressions modulo associativity, commutativity, and idempotency of unions and intersections and use a hint database for the rest.

Here's what I have so far https://gist.github.com/haselwarter/811f2e480359f4eb6b3d364de61c02c2

I was surprised to see that `aac_normalise`

failed when I tried to use it to simplify the goal

```
fsubset (fset [:: a; b])
(O :|: (fset [:: a; b] :|: fset [:: c])
:|: (O :|: (fset [:: a; b] :|: fset [:: c])))
```

The aac laws for `fset`

hold strictly (i.e. wrt. typal equality); in this case AAC should be able to rewrite in any subexpression.

When I manually pulled out the equation I wanted to simplify along via `replace`

, `aac_reflexivity`

succeeded. But when I tried to `Qed.`

I got another error

```
which should be coercible to "Type@{AAC_tactics.AAC.271}".
```

@Karl Palmskog , can you tell what's going on here? Am I barking up the wrong tree altogether? Abusing `aac_tactics`

?

@Philipp G. Haselwarter I may be the maintainer, but my insights into the implementation of aac-tactics are very shallow. Maybe you can create a small self-contained example and report as an issue on GitHub? Then we can ping more aac-tactics-knowledgeable people such as Fabian Kunze and Damien Pous

Sounds good, I wanted to ask here first in case this was some well-known / obvious issue.

@Philipp G. Haselwarter `@fsubset T`

has type `{fset T} -> {fset T} -> bool`

, so your goal actually looks like this:

```
is_true (@fsubset T lhs rhs)
```

where `is_true`

is an SSReflect coercion that converts booleans to propositions. This seems to be the reason why `aac_normalize`

is getting confused. If we wrap `fsubset`

so that it returns a proposition, the tactic succeeds:

```
Definition fsubset' X Y : Prop :=
@fsubset T X Y.
Context {H : Proper ((fsubset') ==> (fsubset') ==> (fsubset')) (@fsetU T)}.
Instance X : Proper ((fsubset') ==> (fsubset') ==> (fsubset')) (@fsetU T) := H.
Goal Goal_subset.
unfold Goal_subset.
fold O.
rewrite -[is_true (fsubset _ _)]/(fsubset' _ _).
aac_normalise.
rewrite /fsubset'.
info_eauto using introTF, orP, fsubsetxx, fsubsetU.
Qed.
```

Thanks for the workaround Arthur. Still seems like a shortcoming of `aac_normalize`

.

Are you aware of other automation for `fset`

?

@Philipp G. Haselwarter There isn't any automation for `fset`

in extructures, unfortunately. SSReflect has great generic lemmas for rewriting with commutativity and associativity (https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrAC.v), which do work with `fset`

. But they are not automated, and they do not support reasoning with idempotency.

The `std++`

library has its own extensional implementation of finite sets, and it has a `set_solver`

tactic for discharging goals like that. It works quite well. However, using `std++`

together with the other SSReflect libraries is not that easy -- they were designed separately as replacements for the Coq standard library.

Thanks @Arthur Azevedo de Amorim

An alternative would be to make a simplified version of https://github.com/math-comp/algebra-tactics by @Kazuhiko Sakaguchi and @Cyril Cohen . In fact, in this case, fset forms a distributive lattice and thus a ring, so we might even be able to use the ring tactic directly.

I'd imagine making automation for idempotent rings would be straightforward.

I guess the problem is that purely syntactic reification procedures do not work for MathComp style (overloaded or polymorphic) operators. This is one of the issues I addressed in Algebra Tactics by using conversion in reification.

maybe this is something that should be added to aac-tactics documentation then, and we just point to `ssrAC`

and Algebra Tactics for MathComp, I don't see any specific MathComp support in aac-tactics forthcoming...

I think there is a plan to implement a reflexive tactic for the theory of finite sets. I personally wish to have reflexive tactics for several classes of ordered sets (including distributive lattices), which I don't know how to do yet. (I don't have time to do that right now anyway.)

@Kazuhiko Sakaguchi who has that plan ?

Won't the ring tactic already give you most of what you need for a tactic for distributive lattices?

@Kazuhiko Sakaguchi how hard would it be to provide a dressed down version of the ring tactic for communtative semigroups (i.e. AC-rewriting).

Correct me if I'm wrong. I think:

- It should be easy to implement tactics for weaker structures such as monoids, semirings, and groups, although I personally never reimplemented the decision procedure part of the ring/field tactics (I just reused ones in the standard library).
- But any of them is not really a practical tool to reason about lattices. A lattice is not necessarily equipped with the identity elements (bottom and top). The ring tactic and other similar ones do not know about idempotence, and are incomplete with respect to assumptions (in the case of the ring tactic, they are restricted to monomial equalities).

@Kazuhiko Sakaguchi Yes, I had the same impression.

Indeed, finite sets do not have a top element, so it is a slightly weaker algebraic structure.

Note there is also `lattice`

tactic in `relation-algebra`

library. Though I do not know on what algorithm it is based.

Yet I used it in my projects and it is able to solve some simple equalities/inequalities over lattices.

Besides that, by quick googling, I found this paper, that also looks relevant.

In general, I'm also very interested in mathcomp-compatible tactic to solve lattice theory.

@Evgeniy Moiseenko That TFP paper looks interesting, although it does not seem to support distributivity. Thanks for the pointer.

I wrote a paper about Algebra Tactics. If you learn Coq-Elpi and also have a reflexive decision procedure, you would be able to apply this technique to fsets. The crucial part is Section 3, but Section 4 might also be useful to deal with images and preimages. https://arxiv.org/abs/2202.04330

Last updated: Oct 13 2024 at 01:02 UTC