two proofs suggested for `Data.List.Membership.Setoid.Properties`

[mechvel]

I suggest the following two proofs for standard library (probably for Data.List.Membership.Setoid.Properties). These are is over S : Setoid _ _.

any∈sym :  ∀ {xs ys} → Any (_∈ ys) xs → Any (_∈ xs) ys
any∈sym {xs} {ys} any-xs∈ys =
  let (x , x∈xs , x∈ys) = find {P = (_∈ ys)} any-xs∈ys
  in
  lose {P = (_∈ xs)} (∈-resp-≈ S) x∈ys x∈xs

all∉sym :  ∀ {xs ys} → All (_∉ ys) xs → All (_∉ xs) ys
all∉sym {xs} {ys} all-xs∉ys =
                  ¬Any⇒All¬ ys (¬any-xs∈ys ∘ any∈sym)
  where
  ¬any-xs∈ys =  All¬⇒¬Any all-xs∉ys

I do not set dashes, for example, write any∈sym rather than any-∈-sym. Because (1) this makes the proof texts shorter, (2) the symbols like ∈, ∉, *, _≈_, ... denote operators and are distinguished themselves inside a word. But if the team insists, let them set dashes.

[jamesmckinna]

The first lemma, purely concerning Any, has the direct proof as above, but may also be given, perhaps more indirectly, by appeal to Data.List.Relation.Unary.Any.Properties.swap, noting that symmetry of equality _≈_ implies that flip _≈_ is extensionally the same as _≈_ (UPDATED: the implicit argument {R = flip _≈_} to Any.swap is in fact superfluous):

any∈sym :  ∀ {xs ys} → Any (_∈ ys) xs → Any (_∈ xs) ys
any∈sym p = Any.swap (Any.map (Any.map sym) p)

The second lemma, as observed, follows easily by (iterated) contraposition UPDATED but, unfortunately, placing it with the first under Data.List.Membership.Setoid.Properties creates a dependency cycle with Data.List.Relation.Unary.All.Properties, arising from the import of Data.List.Membership.Setoid.Properties in Data.List.Relation.Unary.All.Properties in order to be able to define cartesianProductWith and cartesianProduct...

So, how best to break that cycle?

• place the second lemma under Data.List.Relation.Unary.All.Properties instead?
• lift out a restricted fragment (essentially this section) to Data.List.Membership.Setoid.Properties.Core?

PR #2465 takes the second course of action.

[mechvel]

Thank you. I see. Let the team decide about this.