Stream: math-comp users

Topic: how to create =i equality


view this post on Zulip 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.

view this post on Zulip Andrey Klaus (Nov 15 2021 at 15:18):

(deleted)

view this post on Zulip Pierre Roux (Nov 15 2021 at 15:35):

Locate "=i" should enable you to see the underlying equality (no magic in there)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Christian Doczkal (Nov 15 2021 at 16:45):

For seq, this is set up in seq.v

view this post on Zulip 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