Formalization of "chain of or"

Stream: maths

[Esteban Martínez Vañó]

Hi everyone.

I have the following definitions to have a way to talk about disjuntions of arbitrary many formulas indexed by the natural numbers:

def ORn' (P : ℕ → Prop) (N : ℕ): ℕ → Prop
  | 0 => P N
  | n + 1 => P (N - (n + 1)) ∨ ORn' P N n

def ORn (P: ℕ → Prop) : ℕ → Prop := fun n ↦ ORn' P n n

I've done it in this way to ensure that when entering any particular natural number, for example, n=4, one gets by reflexivity:

example (P: ℕ → Prop): ORn P 4 ↔ P 0 ∨ P 1 ∨ P 2 ∨ P 3 ∨ P 4 := by
  rfl

In that way, one can use it with "rcases" because the order of the disjunctions is the "correct" one, but I'd also like to prove that the recursion can be "reversed", that is the following theorem:

theorem aux (n : ℕ) (P: ℕ → Prop) : ORn P n ∨ P (n + 1) ↔ ORn P (n + 1)

Any idea of how to proceed?

[Violeta Hernández]

Your definition can be simplified quite a bit if you're willing to have associativity the other way around

def ORn (P : ℕ → Prop) : ℕ → Prop
  | 0 => P 0
  | n + 1 => ORn P n ∨ P (n + 1)

example (P: ℕ → Prop): ORn P 4 ↔ (((P 0 ∨ P 1) ∨ P 2) ∨ P 3) ∨ P 4 := by
  rfl

[Violeta Hernández]

Then your aux theorem should be definitional

[Edward van de Meent]

i don't know what you need this for, but perhaps it might be easier to simply use ∃ n, P n (or something along those lines)

[Edward van de Meent]

perhaps even using a ∈ Set.Iic 4 clause

[Violeta Hernández]

If you really don't want those parentheses, you can also do

def ORn (P : ℕ → Prop) : ℕ → Prop
  | 0 => P 0
  | n + 1 => P 0 ∨ ORn (P ∘ Nat.succ) n

example (P: ℕ → Prop): ORn P 4 ↔ P 0 ∨ P 1 ∨ P 2 ∨ P 3 ∨ P 4 := by
  rfl

[Violeta Hernández]

In both cases you get rid of the awkward auxiliary definition (and natural subtraction), and you can reason in terms of induction directly

[Violeta Hernández]

Edward van de Meent said:

perhaps even using a ∈ Set.Iic 4 clause

Or even better, Finset.Iic 4

[Adam Topaz]

Another option is to use lists of props with folds, maps, and ranges.

[Adam Topaz]

These building blocks can recover essentially all the recursive approaches mentioned above

[Violeta Hernández]

Yeah, I think trying to come up with these n-ary functions via recursion is somewhat of an antipattern. We used to do this for some stuff in the ZFC file, but #16398 shows that it's actually way simpler to just use Fin n instead.

[Esteban Martínez Vañó]

Violeta Hernández ha dicho:

If you really don't want those parentheses, you can also do

def ORn (P : ℕ → Prop) : ℕ → Prop
  | 0 => P 0
  | n + 1 => P 0 ∨ ORn (P ∘ Nat.succ) n

example (P: ℕ → Prop): ORn P 4 ↔ P 0 ∨ P 1 ∨ P 2 ∨ P 3 ∨ P 4 := by
  rfl

This has worked for me. Thanks!

But, as you all are saying that it is more simple to use Fin, I'll explain what I wanted to do with the definition and see if you can tell me if it can be done with Fin.

In some proofs I have staments of the form (i : ℕ ) < 5 and I want to do a proof by cases with cases i=0, i=1, ... , i= 4. By definining my "ORn" (well, Violeta's ORn) I have proven

theorem aux {x : ℕ} (n : ℕ) (h: 0 < n):  x < n ↔ ORn (fun k ↦ x = k) (n - 1)

And so, using this theorem I can rewrite (i : ℕ ) < 5 so that it is a chain of disjuntions where I can use the rcases tactic.

Can this be done with Fin?

[Daniel Weber]

In Mathlib there are fin_cases and interval_cases

[Esteban Martínez Vañó]

Daniel Weber ha dicho:

In Mathlib there are fin_cases and interval_cases

Thanks! I didn't know those tactics!

[Eric Wieser]

I don't see it mentioned above, but \exists i : Fin n, P i works well for your use-case give docs#Fin.exists_fin_succ