There is a nice equality
mem_undup : forall (T : eqType) (s : seq T), undup s =i s. Quite useful thing that it can be used as rewrite rule like
rewrite mem_undup. Essentially, this mean that every member which is in
s is also in
undup s and vise versa. I would like to build my own equality like
mem_undup. I have function
build_set : seq T1 -> seq T2. And I would like to have lemma
mem_build_undup s : build_set s i= build_set (undup s). I would like to use it for rewriting as mem_undup. Can I have it? What is better to see as an example. I tryed to see mem_undup, but I'm not sure I see how it works. It looks like it should be some kind of coersion because undup s and s are just of type
seq T, but
=i waits for some more complicated type.
Locate "=i" should enable you to see the underlying equality (no magic in there)
I'm a bit puzzled by the type of
build_set, is it really using two different "base" types
In any event,
A =i B expands to
eq_mem (mem A) (mem B) where
mem : forall (T : Type) (pT : predType T), pT -> mem_pred T
So it requires that the objects on the LHS and RHS can be seen as (boolean) predicates over some type, as is the case for
seq T when
T has an
seq, this is set up in seq.v
@Pierre Roux , @Christian Doczkal , thank you very much for the hints. After trying to believe that there is no magic there and checking the hints given by Christian I was able to find that my T2 is not eqType. I think that is why I have problems with this thing.
@Christian Doczkal , as for T1 T2, build_set builds seq from some another seq that is why types are different.
Last updated: Feb 08 2023 at 04:04 UTC