Andrey Klaus (Nov 15 2021 at 15:09): Andrey Klaus (Nov 15 2021 at 15:09):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.
Andrey Klaus (Nov 15 2021 at 15:18):(deleted)
Pierre Roux (Nov 15 2021 at 15:35):Locate "=i" should enable you to see the underlying equality (no magic in there)
Christian Doczkal (Nov 15 2021 at 16:38):I'm a bit puzzled by the type of build_set, is it really using two different "base" types T1 and T2?
Christian Doczkal (Nov 15 2021 at 16:41):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 eqType structure.
Christian Doczkal (Nov 15 2021 at 16:45):For seq, this is set up in seq.v
Andrey Klaus (Nov 16 2021 at 06:59):@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