multiset_solver cannot even solve trivial goals

I am not sure what goals multiset_solver is supposed to be able to handle, but so far it has solved zero of the goals I tried it on. Here is a rather simple example that only requires reasoning up to A/C:

  net_phys, net_ghost : gmultiset val
  m : val
-----------------------------------------
{[m]} ⊎ net_ghost ∖ {[m]} ⊎ net_phys = net_ghost ∖ {[m]} ⊎ (net_phys ⊎ {[m]})

changed the description

Hm in a minimal example it can solve this goal, but in my main proof it is unable to do so...

This is the goal it fails to solve:

  @eq (@gmultiset val val_eq_dec val_countable)
    (@disj_union (@gmultiset val val_eq_dec val_countable)
       (@gmultiset_disj_union val val_eq_dec val_countable)
       (@disj_union (@gmultiset val val_eq_dec val_countable)
          (@gmultiset_disj_union val val_eq_dec val_countable)
          (@singleton val (@gmultiset val val_eq_dec val_countable)
             (@gmultiset_singleton val val_eq_dec val_countable) m)
          (@difference (@gmultiset val val_eq_dec val_countable)
             (@gmultiset_difference val val_eq_dec val_countable) net_ghost
             (@singleton val (@gmultiset val val_eq_dec val_countable)
                (@gmultiset_singleton val val_eq_dec val_countable) m))) net_phys)
    (@disj_union (@gmultiset val val_eq_dec val_countable)
       (@gmultiset_disj_union val val_eq_dec val_countable)
       (@difference (@gmultiset val val_eq_dec val_countable)
          (@gmultiset_difference val val_eq_dec val_countable) net_ghost
          (@singleton val (@gmultiset val val_eq_dec val_countable)
             (@gmultiset_singleton val val_eq_dec val_countable) m))
       (@disj_union (@gmultiset val val_eq_dec val_countable)
          (@gmultiset_disj_union val val_eq_dec val_countable) net_phys
          (@singleton val (ucmra_car (@gmultisetUR val val_eq_dec val_countable))
             (@gmultiset_singleton val val_eq_dec val_countable) m)))

And this is the one it solves fine:

  @eq (@gmultiset val val_eq_dec val_countable)
    (@disj_union (@gmultiset val val_eq_dec val_countable)
       (@gmultiset_disj_union val val_eq_dec val_countable)
       (@disj_union (@gmultiset val val_eq_dec val_countable)
          (@gmultiset_disj_union val val_eq_dec val_countable)
          (@singleton val (@gmultiset val val_eq_dec val_countable)
             (@gmultiset_singleton val val_eq_dec val_countable) m)
          (@difference (@gmultiset val val_eq_dec val_countable)
             (@gmultiset_difference val val_eq_dec val_countable) net_ghost
             (@singleton val (@gmultiset val val_eq_dec val_countable)
                (@gmultiset_singleton val val_eq_dec val_countable) m))) net_phys)
    (@disj_union (@gmultiset val val_eq_dec val_countable)
       (@gmultiset_disj_union val val_eq_dec val_countable)
       (@difference (@gmultiset val val_eq_dec val_countable)
          (@gmultiset_difference val val_eq_dec val_countable) net_ghost
          (@singleton val (@gmultiset val val_eq_dec val_countable)
             (@gmultiset_singleton val val_eq_dec val_countable) m))
       (@disj_union (@gmultiset val val_eq_dec val_countable)
          (@gmultiset_disj_union val val_eq_dec val_countable) net_phys
          (@singleton val (@gmultiset val val_eq_dec val_countable)
             (@gmultiset_singleton val val_eq_dec val_countable) m)))

The former has some ucmra_car (@gmultisetUR val val_eq_dec val_countable), maybe that is the problem?

The lemma in which this happens is

  Lemma recv_elimdiff (net_phys net_ghost : gmultiset val) (m : val) :
    own γgdiff (● net_ghost ⋅ ◯ net_phys) -∗ own γgdiff (◯ {[ m ]}) ==∗
    ⌜m ∈ net_ghost⌝ ∗ own γgdiff (● (net_ghost ∖ {[ m ]}) ⋅ ◯ net_phys).

Adding type ascription solves the problem. Looks like the map and set singleton notations are basically unusable without type ascription, but in the most subtle ways?

I am not sure if this is related to Ralf's example, but here is an example that exhibits two problems:

• multiset_solver fails to prove a simple statement;
• two distinct relations on multisets are printed ⊆, which is confusing.

Lemma test `{Countable A} (x : A) (X : gmultiset A) :
  x ∈ X → {[x]} ⊆ X.
Proof.
  intros Hx.
  (* [multiset_solver] fails: *)
  Fail multiset_solver.
  (* OK, let's try this: *)
  rewrite -> elem_of_subseteq_singleton in Hx.
  (* We now have a hypothesis {[x]} ⊆ X and the goal is {[x]} ⊆ X,
     yet they are not the same, even though they are printed in
     the same way: *)
  Fail assumption.
  (* The hypothesis uses [set_subseteq], whereas the goal uses
     [gmultiset_subseteq]. These are two distinct relations,
     and the implication is indeed false. *)
Abort.

@fpottier the second problem you mention has a separate issue at #87 (closed)

The first problem is caused by the fact that ∈ is out of scope for multiset_solver. That should probably be documented better somewhere... (Or we should improve multiset_solver to remove that restriction).

Noted, thanks for your replies!

mentioned in merge request !231 (merged)

Closing the original problem as "wontfix" since this is a Coq unification bug; working around it in std++ would be non-trivial.

@fpottier's example is handled by !231 (merged).

closed