Relation is Ayclical

Stream: new members

[Andrew Souther]

Hello, I'm very new, so I hope this question makes sense. I'm thinking about a binary relation R on type σ. I'm interested in this definition from a social choice theory textbook:

A relation R is said to be acyclical if for all finite sequences {x₁ , . . . , xₖ} from X it is not the case that x₁ R x₂ ∧ x₂ R x₂ ∧ . . . ∧ xₖ₋₁ R xₖ and xₖ R x₁.

Here is my best attempt in Lean:

variables {σ: Type}

def is_acyclical (R : σ → σ → Prop) : Prop :=
    ∀ (S : list σ), ¬ ( R (list.nth S S.length) (list.nth S 1)
    ∧ ∀ k : ℕ, k < S.length →  R (list.nth S k) (list.nth S k+1) )

But this gives me an error, where all the terms (list.nth _ _) are type option σ, instead of type σ. Should I try to define a finite sequence in a different way? I'm still struggling to navigate mathlib. Thanks!

I guess it's also worth asking: has anyone else worked on Social Choice Theory in Lean?

[Johan Commelin]

Welcome @Andrew Souther! I don't think anybody has been doing social choice theory in lean. (It's the first time I hear about it.)

[Johan Commelin]

Note that there is list.nth_le which avoids the option _

[Johan Commelin]

Another option would be to use vector instead of list, to make the length into an explicit natural number, so you would get something like
\forall n, (S : vector \sigma n), ...

[Heather Macbeth]

Another option: you could let S be of type zmod n → σ (i.e., a function from integers-mod-n to σ), and then you can state your result in terms of S k and S (k + 1) without needing a special case for the end term (since the last "+ 1" wraps around to 0).

[Reid Barton]

Another way to express it is using docs#relation.trans_gen: say there is no x with trans_gen R x x

[Johan Commelin]

Welcome to the world of design decisions :grinning:

[Andrew Souther]

A lot to play with, thank you! I'll be be back if I have trouble.

[Reid Barton]

but wait! there's also docs#list.chain :upside_down:

[Reid Barton]

If σ is finite it's also equivalent to wellfoundedness

[Andrew Souther]

trans_gen seems like a really concise solution. I'd like to make sure I understand it though.
I think that ¬(∃ x : σ, trans_gen R x x) roughly means "There is no x, such that the transitive closure of R contains xRx."

Does that sound right? I'll try to put this definition to use. If it's too hard to work with, I'll tinker more with lists and vectors and zmod. Thanks again!

[Kevin Buzzard]

The definition you quoted -- presumably k>=1 is part of the assumptions? Assuming it is, ¬(∃ x : σ, trans_gen R x x) looks good to me. If you wanted practice you could formalise Heather's definition too (assuming n>=1 there) and prove it's equivalent.

[Andrew Souther]

Yes, I think it's fair to say k>=1, but I'm not 100% sure based on the language in the textbook. I will try that proof for practice!

[Reid Barton]

Right, if it's k>=2 instead, then the trans_gen approach isn't as convenient