Andrey Klaus (Nov 14 2021 at 21:28): 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 => ->.
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: Dec 06 2023 at 13:01 UTC