The Coq mailing list

[Katherine Ye <kye AT princeton.edu>]

Hi all,

I'm using multisets as the type of an environment. (I'm using this library: https://coq.inria.fr/library/Coq.Sets.Multiset.html) I want to be able to rewrite in a sequent using multiset equivalence, like this:
 

H1: m1 == m2 (where "==" is multiset equivalence)
Goal: m1 |- Top
(rewrite using H1 in goal)
New goal: m2 |- Top


But I can't seem to get it to work.
 
Here's what I have:

Require Import LinearLogic. (* written by me *)
Require Import Setoid.

Definition emptyBag := EmptyBag LinProp.

(* multiset equivalence, to allow setoid rewrites on multisets *)

(* meq = all elements in the set have the  same multiplicity *)
Add Parametric Relation A : (multiset A) (@meq A)
 reflexivity proved by (@meq_refl A)
 symmetry proved by (@meq_sym A)
 transitivity proved by (@meq_trans A)
 as meq_rel.

Add Parametric Morphism A : (@eq (multiset A)) with
  signature (@meq A) ==> (@meq A) ==> (Basics.flip Basics.impl)
      as eq_mor.
Proof.               

(* note this is actually not true, it's here just as a minimal test *) Admitted.

(* again, not true, but the rewriting works *)
Lemma setoid_rewrite_test : forall {A : Type} (s1: multiset A),
                              meq s1 (EmptyBag A) ->
                              s1 = EmptyBag A.
Proof.
  intros. setoid_rewrite H. reflexivity.
Qed.

(* now extending it to LinProof, which I defined

LinProof is basically "env |- some single linear prop" *)

Check LinProof. (* : env -> LinProp -> Prop *)

                 
Add Morphism LinProof with
  signature (@meq LinProp) ==> eqLinProp ==> (Basics.flip Basics.impl)
      as seq_mor.
Proof. 

(* this should be true *)
Admitted.

Lemma setoid_rewrite_test_sequent : forall (s: multiset LinProp),
                              meq s emptyBag ->
                                   s |- Top.
Proof.
  intros.
  setoid_rewrite H. (* Trying to rewrite s in goal gives an error *)


Here's the error I'm getting:


Toplevel input, characters 0-16:
Error:
Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting constraints.
Unable to satisfy the following constraints:
EVARS:
 ?130==[s H |- Morphisms.ProperProxy ?128 Top] (internal placeholder)
 ?129==[s H (do_subrelation:=Morphisms.do_subrelation)
         |- Morphisms.Proper
              (meq (A:=LinProp) ==> ?128 ==> Basics.flip Basics.impl)
              LinProof] (internal placeholder)
 ?128==[s H |- relation LinProp] (internal placeholder).

Any help would be appreciated. Other suggestions about ways to represent the environment, which is a set that can contain the same element multiple times, are also welcome. (I considered Ensembles and ListSet, but they were missing things. Maybe lists with permutations?)

Thanks!

Best,

Katherine