Stream: math-comp users

Topic: under tactic with setoid rewrite


view this post on Zulip Laurent Théry (Apr 06 2023 at 14:48):

Hi,
is the under tactic supposed to work with setoid? I've been trying this

From mathcomp Require Import all_ssreflect.
Require Import Setoid.

Goal forall (A  B : Prop), A /\ B -> B /\ A.
by move=> A B H; rewrite and_comm.
Qed.

Lemma all_equiv A (P Q : A -> Prop) :
  (forall a, P a <-> Q a) -> (forall a, P a) <-> (forall a, Q a).
Proof. by move=> H; split=> H1 a; rewrite ?H // -H. Qed.

Goal forall (A  B : nat -> Prop), (forall x, A x /\ B x) -> (forall x, B x /\ A x).
move=> A B H.
under all_equiv do rewrite and_comm.

view this post on Zulip Paolo Giarrusso (Apr 06 2023 at 17:41):

We needed to add some extra Proper instances, and there was some discussion here

view this post on Zulip Paolo Giarrusso (Apr 06 2023 at 17:41):

They seemed to work, but I don't think anybody was confident they wouldn't cause performance problems

view this post on Zulip Laurent Théry (Apr 07 2023 at 07:30):

Paolo Giarrusso said:

We needed to add some extra Proper instances, and there was some discussion here

where?

view this post on Zulip Paolo Giarrusso (Apr 07 2023 at 18:59):

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.60Proper.20.2E.2E.2E.20.28Under_rel.20.2E.2E.2E.29.60

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

Great it works! I would like to make a PR but it is not clear to me where this new instance should be put.
I though about ssrunder.v but this comment scared me :

(*
 This preserves the following feature: we can use [Setoid] without
 requiring [ssreflect] and use [ssreflect] without requiring [Setoid]. *)

view this post on Zulip Paolo Giarrusso (Apr 07 2023 at 21:50):

I think I have code better than in the link...

view this post on Zulip Paolo Giarrusso (Apr 07 2023 at 21:52):

This is the latest version https://github.com/bedrocksystems/BRiCk/blob/master/theories/prelude/under_rel_proper.v

view this post on Zulip Paolo Giarrusso (Apr 07 2023 at 21:55):

Beware the bedrock license isn't compatible with math-comp's, I expect we'll relicense it but this needs an okay from @Gregory Malecha

view this post on Zulip Paolo Giarrusso (Apr 07 2023 at 21:58):

It sounds like the right place for these tactics should eventually be https://github.com/coq/coq/blob/d8db2fd7e6df24d56160651d570603d935dac170/theories/ssr/ssrsetoid.v.

view this post on Zulip Laurent Théry (Apr 08 2023 at 06:57):

ok if @Gregory Malecha gives his ok, I will make a PR with his code.

view this post on Zulip Karl Palmskog (Apr 08 2023 at 07:57):

the code is currently licensed under the usual Affero GPL-like license. This is a really cumbersome license to abide by. I hope "giving OK" means "relicensing under MathComp's license"

view this post on Zulip Laurent Théry (Apr 08 2023 at 08:14):

Why mathcomp? I was thinking to do a PR for Coq.

view this post on Zulip Karl Palmskog (Apr 08 2023 at 08:16):

OK, but same story there, only different relicensing (to LGPL-2.1-only)

view this post on Zulip Paolo Giarrusso (Apr 08 2023 at 08:31):

@Karl Palmskog absolutely


Last updated: Jul 25 2024 at 16:02 UTC