Stream: Coq users

Topic: aac-tactics, fset automation, universes

Philipp G. Haselwarter (Nov 08 2021 at 09:59):

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?

Karl Palmskog (Nov 08 2021 at 10:03):

@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

Philipp G. Haselwarter (Nov 08 2021 at 10:16):

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

Arthur Azevedo de Amorim (Nov 08 2021 at 15:09):

@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 fsubsetso 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.

Philipp G. Haselwarter (Nov 08 2021 at 16:14):

Thanks for the workaround Arthur. Still seems like a shortcoming of aac_normalize.
Are you aware of other automation for fset?

Arthur Azevedo de Amorim (Nov 08 2021 at 18:56):

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

Bas Spitters (Nov 09 2021 at 11:48):

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.

Kazuhiko Sakaguchi (Nov 09 2021 at 13:26):

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.

Karl Palmskog (Nov 09 2021 at 13:29):

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

Kazuhiko Sakaguchi (Nov 09 2021 at 13:30):

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

Bas Spitters (Nov 09 2021 at 13:52):

@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?

Bas Spitters (Nov 17 2021 at 14:56):

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

Kazuhiko Sakaguchi (Nov 19 2021 at 12:55):

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

Bas Spitters (Nov 19 2021 at 14:44):

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

Evgeniy Moiseenko (Nov 21 2021 at 10:20):

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.

Kazuhiko Sakaguchi (Nov 22 2021 at 16:29):

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

Kazuhiko Sakaguchi (Feb 10 2022 at 03:40):

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 01 2023 at 19:01 UTC