Laurent Théry (Apr 06 2023 at 14:48): 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.
We needed to add some extra Proper instances, and there was some discussion here
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
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?
Paolo Giarrusso (Apr 07 2023 at 18:59): 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]. *)
I think I have code better than in the link...
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
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
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.
Laurent Théry (Apr 08 2023 at 06:57):ok if @Gregory Malecha gives his ok, I will make a PR with his code.
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"
Laurent Théry (Apr 08 2023 at 08:14):Why mathcomp? I was thinking to do a PR for Coq.
Karl Palmskog (Apr 08 2023 at 08:16):OK, but same story there, only different relicensing (to LGPL-2.1-only)
Paolo Giarrusso (Apr 08 2023 at 08:31):@Karl Palmskog absolutely
Last updated: Oct 13 2024 at 01:02 UTC