Stream: math-comp users

Topic: Code review - new user


view this post on Zulip Fernando Chu (Apr 05 2023 at 19:10):

Hello, I've been learning about math-comp and wanted to implement issue 619 a as a challenge. My code is the following

Lemma subset_cons2 s1 s2 x:
  s1 \subset s2 -> x::s1 \subset x::s2.
Proof.
move/subsetP=> ss1s2; apply/subsetP => y H; rewrite in_cons in H; rewrite in_cons.
apply/orP; case/orP: H.
- by move => p; left; apply p.
- by move => p; right; apply: ss1s2.
Qed.

However there are many things that could be improved. I thought that I could apply in_cons directly in H in the 4th line, by apply/subsetP => y /in_cons-H but it's not working. There is also some repetition as I'm using twice the same lemma, both with in_cons and orP.

I'd appreciate any constructive criticism to improve this code.

view this post on Zulip Laurent Théry (Apr 05 2023 at 21:09):

Lemma subset_cons2 s1 s2 (x : T) :
  s1 \subset s2 -> x :: s1 \subset x :: s2.
Proof.
move/subsetP=> ss1s2; apply/subsetP => y.
rewrite !inE.
case: eqP => //= _.
apply: ss1s2.
Qed.

view this post on Zulip Fernando Chu (Apr 06 2023 at 14:12):

Thank you!


Last updated: Jul 15 2024 at 21:02 UTC