Stream: math-comp users

Topic: ✔ how to work with `mem`?

Andrey Klaus (Nov 14 2021 at 21:28):

I have predicate incl defined as

Definition incl (T : eqType) (vrs' vrs : seq T) := all (fun x => has (pred1 x) vrs) vrs'.

Now I would like to define it as

Definition incl (T : eqType) (vrs' vrs : seq T) := all (mem vrs) vrs'.

because it looks nicer to me (thanks to @Christian Doczkal for the hint).

The question.
When this lemma is defined using has I can use rewrite has_pred1 mem_undup like it is shown below

Lemma incl_undup (T : eqType) (vrs vrs' : seq T) : incl vrs (undup (vrs ++ vrs')).
  move => vrs vrs';  rewrite /incl; apply/allP => t.

 T : eqType
  vrs, vrs' : seq T
  t : T
  ============================
  t \in vrs -> has (pred1 t) (undup (vrs ++ vrs'))

(* now rewrite *)
rewrite has_pred1 mem_undup mem_cat.

When it is defined with mem, I'm a bit stuck with rewrite step at this moment

  T : eqType
  vrs, vrs' : seq T
  t : T
  ============================
  t \in vrs -> mem (undup (vrs ++ vrs')) t

So, how to work with mem in this case?

Christian Doczkal (Nov 14 2021 at 21:37):

It is often a good idea to simplify (using /=). In this case mem _ _ simplifies to _ \in _ and you can finish your proof with:

by rewrite /= mem_undup mem_cat => ->.

Andrey Klaus (Nov 14 2021 at 21:40):

Great thanks!

Notification Bot (Nov 14 2021 at 21:40):

Andrey Klaus has marked this topic as resolved.

Notification Bot (Nov 15 2021 at 07:49):

Andrey Klaus has marked this topic as unresolved.

Notification Bot (Nov 15 2021 at 07:50):

Andrey Klaus has marked this topic as resolved.

Last updated: Apr 19 2024 at 23:02 UTC