Stream: new members

Topic: Relation is Ayclical

Andrew Souther (Nov 25 2020 at 17:00):

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 (Nov 25 2020 at 17:02):

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 (Nov 25 2020 at 17:03):

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

Johan Commelin (Nov 25 2020 at 17:05):

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 (Nov 25 2020 at 17:15):

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 (Nov 25 2020 at 17:17):

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

Johan Commelin (Nov 25 2020 at 17:20):

Welcome to the world of design decisions :grinning:

Andrew Souther (Nov 25 2020 at 17:23):

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

Reid Barton (Nov 25 2020 at 17:24):

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

Reid Barton (Nov 25 2020 at 17:26):

If σ is finite it's also equivalent to wellfoundedness

Andrew Souther (Nov 25 2020 at 18:31):

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 (Nov 25 2020 at 18:38):

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 (Nov 25 2020 at 19:01):

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 (Nov 25 2020 at 19:02):

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

Last updated: May 15 2021 at 23:13 UTC