Declare relation symmetric under permutations of variables

Stream: general

[Quinn Culver]

Is there a standard way to say in LEAN that a relation is invariant under permutations of its variables?

For example I have collinear below, and often find myself proving something is not collinear using lemma noncollinear but with the variables in an order different from what I need. So, for example, I'll have proved ¬ collinear L p₀ p₁ p₂ but the goal is ¬ collinear L p₁ p₀ p₂. I know I could unpack and repack the definition of collinear, but my hope is that LEAN/mathlib already does this.

import combinatorics.configuration
open configuration.projective_plane

open classical

universe u

variables {P L : Type u} [has_mem P L] [configuration.projective_plane P L]
variables {P} (L)
def collinear (p₀ p₁ p₂ : P) : Prop := ∃ l : L, p₀ ∈ l ∧ p₁ ∈ l ∧ p₂ ∈ l

lemma noncollinear (p₀ p₁ p₂ : P) (l₀ : L) (i₀₀ : p₀ ∉ l₀) (i₁₀ : p₁ ∈ l₀) (i₂₀ : p₂ ∈ l₀) (hp₁p₂ : p₁ ≠ p₂) : ¬ collinear L p₀ p₁ p₂ :=  sorry

[Eric Wieser]

I suspect it doesn't directly work for the projective case, but you could look at how the API for docs#collinear is designed in mathlib

[Eric Wieser]

Note that it's defined on a set of points rather than three points

[Alex J. Best]

That said if your goals are literal permutions of the logical connectives of things you know tactic#tauto should solve it for you

[Quinn Culver]

Thanks. Am I right that tauto won't work if the logical connectives are "hidden behind" a definition, (collinear in this case)? E.g. I have hypothesis ¬ collinear L p₀ p₁ p₂ but the goal is ¬ collinear L p₁ p₀ p₂.

[Eric Wieser]

Yes, it won't work

[Eric Wieser]

But you can write a lemma that says collinear L p q r ↔ collinear L q r p and prove that by unfolding then using tauto.

[Junyan Xu]

or you might just do := ⟨λ ⟨l, hp, hq, hr⟩, ⟨l, hq, hr, hp⟩, λ ⟨l, hq, hr, hp⟩, ⟨l, hp, hq, hr⟩⟩