ordering unique elements

Stream: new members

[Evan Lohn]

I want to prove that some unique elements of fin N satisfying some property have an "ordered version" of those elements also each satisfying the property. Is this the best way to go about doing so? Would love any feedback (even on style)!

import data.fin.basic

variables (N: ℕ)

lemma not_lt_neq_gt {a b: fin N} (h1: ¬(a < b)) (h2: a ≠ b): b < a :=
begin
  rw not_lt at h1,
  exact or.resolve_left (eq_or_lt_of_le h1) (ne.symm h2),
end

lemma find_ordered {a b c: fin N} {pred: (fin N) → Prop} (hab: a ≠ b) (hac: a ≠ c) (hbc: b ≠ c) (hprops: pred a ∧ pred b ∧ pred c):
∃ d e f, d < e ∧ e < f ∧ pred d ∧ pred e ∧ pred f :=
begin
  by_cases haltb : a < b; by_cases hbltc : b < c,
  exact ⟨ a, b, c, haltb, hbltc, hprops⟩,
  by_cases haltc : a < c,
  exact ⟨a, c, b, haltc, not_lt_neq_gt _ hbltc hbc, hprops.1, hprops.2.2, hprops.2.1⟩,
  exact ⟨c, a, b, not_lt_neq_gt _ haltc hac, haltb, hprops.2.2, hprops.1, hprops.2.1⟩,
  by_cases haltc : a < c,
  exact ⟨b, a, c, not_lt_neq_gt _ haltb hab, haltc, hprops.2.1, hprops.1, hprops.2.2⟩,
  exact ⟨b, c, a, hbltc, not_lt_neq_gt _ haltc hac, hprops.2.1, hprops.2.2, hprops.1⟩,
  exact ⟨c, b, a, not_lt_neq_gt _ hbltc hbc, not_lt_neq_gt _ haltb hab, hprops.2.2, hprops.2.1, hprops.1⟩,
end

[Yakov Pechersky]

import data.fin.basic
import data.list.sort

variables (N: ℕ)

lemma find_ordered {a b c: fin N} {pred: (fin N) → Prop} (hab: a ≠ b) (hac: a ≠ c) (hbc: b ≠ c) (hprops: pred a ∧ pred b ∧ pred c):
∃ d e f, d < e ∧ e < f ∧ pred d ∧ pred e ∧ pred f :=
begin
  set l : list (fin N) := list.merge_sort (≤) [a, b, c] with hl,
  have hperm : [a, b, c] ~ l := (list.perm_merge_sort _ _).symm,
  have hn : l.nodup,
  { suffices : [a, b, c].nodup,
    { rw hl,
      exact (hperm.nodup_iff).mp this },
    simp [hab, hac, hbc] },
  have hp : ∀ (x ∈ l), pred x,
  { simp [hperm.symm.mem_iff, hprops] },
  refine ⟨l.nth_le 0 _, l.nth_le 1 _, l.nth_le 2 _, _, _, _, _, _⟩,
  any_goals { simp },
  any_goals { refine lt_of_le_of_ne _ _,
    { refine list.sorted.rel_nth_le_of_lt (list.sorted_merge_sort _ _) _ _ _,
      simp },
    { simp [ne.def, hn.nth_le_inj_iff] } },
  any_goals { exact hp _ (list.nth_le_mem _ _ _) }
end

[Yakov Pechersky]

number of lines is more. but the logic is much simpler I think. I would also ask, why do you need to have three explicit elements as such? Why can't you work on the {a, b, c} : finset (fin N) or [a, b, c]?

[Evan Lohn]

Thanks for your response! I wasn't sure whether it was easier/better to use a finset or list, is that what people typically use for this type of thing? would that make the proof any simpler?

[Kyle Miller]

Depending on what you're doing, you might consider holding onto the elements as a 3-element finset. There's a quick proof from your hypotheses that there's such a finset, and then it's possible to use that conclusion to obtain the conclusion of find_ordered, if you need it.

import data.fin.basic
import data.finset
import tactic

variables (N: ℕ)

lemma find_finset {a b c : fin N} {pred : fin N → Prop} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hprops : pred a ∧ pred b ∧ pred c) :
  ∃ (s : finset (fin N)), s.card = 3 ∧ ∀ x ∈ s, pred x :=
⟨{a, b, c}, by simp [hab, hac, hbc, hprops]⟩

lemma find_ordered {pred : fin N → Prop} (h : ∃ (s : finset (fin N)), s.card = 3 ∧ ∀ x ∈ s, pred x) :
  ∃ d e f, d < e ∧ e < f ∧ pred d ∧ pred e ∧ pred f :=
begin
  obtain ⟨s, hc, hp⟩ := h,
  have h : _ = s.card := finset.length_sort (≤),
  have hsort := s.sort_sorted (≤),
  have hnd := s.sort_nodup (≤),
  simp_rw [← finset.mem_sort (≤)] at hp,
  generalize_hyp hs : s.sort (≤) = l at h hp hsort hnd,
  rw hc at h,
  cases l with d l, by norm_num at h,
  cases l with e l, by norm_num at h,
  cases l with f l, by norm_num at h,
  simp only [add_assoc, list.length, add_left_eq_self] at h,
  replace h := list.eq_nil_of_length_eq_zero h,
  subst h,
  simp only [not_or_distrib, list.nodup_cons, list.mem_cons_iff, list.mem_singleton,
    list.not_mem_nil, not_false_iff, list.nodup_nil, and_true, list.sorted_cons, forall_eq_or_imp,
    forall_eq, list.sorted_singleton] at hsort hnd,
  use [d, e, f, (ne.le_iff_lt hnd.1.1).mp hsort.1.1, (ne.le_iff_lt hnd.2).mp hsort.2],
  simp [hp],
end

[Kyle Miller]

Here's some style feedback in the form of a restyled version of your original code:

import data.fin.basic

variables (N : ℕ)

lemma not_lt_neq_gt {α : Type*} [linear_order α] {a b : α} (h1 : ¬ a < b) (h2 : a ≠ b) : b < a :=
or.resolve_left (le_of_not_gt h1).eq_or_lt h2.symm

lemma find_ordered {a b c : fin N} {pred : fin N → Prop}
  (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (ha : pred a) (hb : pred b) (hc : pred c) :
  ∃ d e f, d < e ∧ e < f ∧ pred d ∧ pred e ∧ pred f :=
begin
  by_cases haltb : a < b; by_cases hbltc : b < c,
  { exact ⟨a, b, c, haltb, hbltc, ha, hb, hc⟩ },
  { by_cases haltc : a < c,
    { exact ⟨a, c, b, haltc, not_lt_neq_gt hbltc hbc, ha, hc, hb⟩ },
    { exact ⟨c, a, b, not_lt_neq_gt haltc hac, haltb, hc, ha, hb⟩ } },
  { by_cases haltc : a < c,
    { exact ⟨b, a, c, not_lt_neq_gt haltb hab, haltc, hb, ha, hc⟩ },
    { exact ⟨b, c, a, hbltc, not_lt_neq_gt haltc hac, hb, hc, ha⟩ } },
  { exact ⟨c, b, a, not_lt_neq_gt hbltc hbc, not_lt_neq_gt haltb hab, hc, hb, ha⟩ },
end

If I remember all the changes:

• spaces before colons
• using curly braces to show proof structure
• split conjunctions when given as arguments
• using dot notation in the first lemma (and turning it into a one-liner since it's "trivial")
• indentation in the lemma statement

[Kyle Miller]

A somewhat less tedious version of the second lemma is this:

lemma find_ordered {a b c : fin N} {pred : fin N → Prop}
  (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (ha : pred a) (hb : pred b) (hc : pred c) :
  ∃ d e f, d < e ∧ e < f ∧ pred d ∧ pred e ∧ pred f :=
begin
  by_cases haltb : a < b; by_cases hbltc : b < c,
  { use [a, b, c], simp [*] },
  { by_cases haltc : a < c,
    { use [a, c, b], simp [*, not_lt_neq_gt] },
    { use [c, a, b], simp [*, not_lt_neq_gt] } },
  { by_cases haltc : a < c,
    { use [b, a, c], simp [*, not_lt_neq_gt] },
    { use [b, c, a], simp [*, not_lt_neq_gt] } },
  { use [c, b, a], simp [*, not_lt_neq_gt] },
end

This way it makes it a bit clearer that you're implementing a sorting network, I think.

[Eric Rodriguez]

can't wlog do this?