feat(order/pilex): lexicographic ordering on pi types (#1157)

* feat(order/pilex): lexicographic ordering on pi types

* fix instance name

* fix instance name properly

* Update basic.lean

* remove unnecessary import

Author: ChrisHughes24

src/order/basic.lean

@@ -11,6 +11,10 @@ open function
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w} {r : α → α → Prop}
 
+protected noncomputable def classical.decidable_linear_order [I : linear_order α] :
+  decidable_linear_order α :=
+{ decidable_le := classical.dec_rel _, ..I }
+
 theorem ge_of_eq [preorder α] {a b : α} : a = b → a ≥ b :=
 λ h, h ▸ le_refl a
 

src/order/pilex.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2019 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes
+-/
+
+import algebra.order_functions tactic.tauto algebra.pi_instances
+
+variables {ι : Type*} {β : ι → Type*} (r : ι → ι → Prop)
+  (s : Π {i}, β i → β i → Prop)
+
+def pi.lex (x y : Π i, β i) : Prop :=
+∃ i, (∀ j, r j i → x j = y j) ∧ s (x i) (y i)
+
+def pilex (α : Type*) (β : α → Type*) : Type* := Π a, β a
+
+instance [has_lt ι] [∀ a, has_lt (β a)] : has_lt (pilex ι β) :=
+{ lt := pi.lex (<) (λ _, (<)) }
+
+set_option eqn_compiler.zeta true
+
+instance [linear_order ι] [∀ a, partial_order (β a)] : partial_order (pilex ι β) :=
+let I : decidable_linear_order ι := classical.decidable_linear_order in
+have lt_not_symm : ∀ {x y : pilex ι β}, ¬ (x < y ∧ y < x),
+  from λ x y ⟨⟨i, hi⟩, ⟨j, hj⟩⟩, begin
+      rcases lt_trichotomy i j with hij | hij | hji,
+      { exact lt_irrefl (x i) (by simpa [hj.1 _ hij] using hi.2) },
+      { exact not_le_of_gt hj.2 (hij ▸ le_of_lt hi.2) },
+      { exact lt_irrefl (x j) (by simpa [hi.1 _ hji] using hj.2) },
+    end,
+{ le := λ x y, x < y ∨ x = y,
+  le_refl := λ _, or.inr rfl,
+  le_antisymm := λ x y hxy hyx,
+    hxy.elim (λ hxy, hyx.elim (λ hyx, false.elim (lt_not_symm ⟨hxy, hyx⟩)) eq.symm) id,
+  le_trans :=
+    λ x y z hxy hyz,
+    hxy.elim
+      (λ ⟨i, hi⟩, hyz.elim
+        (λ ⟨j, hj⟩, or.inl
+          ⟨by exactI min i j, by resetI; exact
+            λ k hk, by rw [hi.1 _ (lt_min_iff.1 hk).1, hj.1 _ (lt_min_iff.1 hk).2],
+            by resetI; exact (le_total i j).elim
+              (λ hij, by rw [min_eq_left hij];
+                exact lt_of_lt_of_le hi.2
+                  ((lt_or_eq_of_le hij).elim (λ h, le_of_eq (hj.1 _ h))
+                    (λ h, h.symm ▸ le_of_lt hj.2)))
+              (λ hji, by rw [min_eq_right hji];
+                exact lt_of_le_of_lt
+                  ((lt_or_eq_of_le hji).elim (λ h, le_of_eq (hi.1 _ h))
+                    (λ h, h.symm ▸ le_of_lt hi.2))
+                  hj.2)⟩)
+        (λ hyz, hyz ▸ hxy))
+      (λ hxy, hxy.symm ▸ hyz),
+  lt_iff_le_not_le := λ x y, show x < y ↔ (x < y ∨ x = y) ∧ ¬ (y < x ∨ y = x),
+    from ⟨λ ⟨i, hi⟩, ⟨or.inl ⟨i, hi⟩,
+        λ h, h.elim (λ ⟨j, hj⟩, begin
+            rcases lt_trichotomy i j with hij | hij | hji,
+            { exact lt_irrefl (x i) (by simpa [hj.1 _ hij] using hi.2) },
+            { exact not_le_of_gt hj.2 (hij ▸ le_of_lt hi.2) },
+            { exact lt_irrefl (x j) (by simpa [hi.1 _ hji] using hj.2) },
+          end)
+        (λ hyx, lt_irrefl (x i) (by simpa [hyx] using hi.2))⟩, by tauto⟩,
+  ..pilex.has_lt }
+
+instance [linear_order ι] (wf : well_founded ((<) : ι → ι → Prop)) [∀ a, linear_order (β a)] :
+  linear_order (pilex ι β) :=
+{ le_total := λ x y, by classical; exact
+    or_iff_not_imp_left.2 (λ hxy, begin
+      have := not_or_distrib.1 hxy,
+      let i : ι := well_founded.min wf _
+        (set.ne_empty_iff_exists_mem.2 (classical.not_forall.1 (this.2 ∘ funext))),
+      have hjiyx : ∀ j < i, y j = x j,
+      { assume j,
+        rw [eq_comm, ← not_imp_not],
+        exact λ h, well_founded.not_lt_min wf _ _ h },
+      refine or.inl ⟨i, hjiyx, _⟩,
+      { refine lt_of_not_ge (λ hyx, _),
+        exact this.1 ⟨i, (λ j hj, (hjiyx j hj).symm),
+          lt_of_le_of_ne hyx (well_founded.min_mem _ {i | x i ≠ y i} _)⟩ }
+    end),
+  ..pilex.partial_order }
+
+instance [linear_order ι] [∀ a, ordered_comm_group (β a)] : ordered_comm_group (pilex ι β) :=
+{ add_le_add_left := λ x y hxy z,
+    hxy.elim
+      (λ ⟨i, hi⟩,
+        or.inl ⟨i, λ j hji, show z j + x j = z j + y j, by rw [hi.1 j hji],
+          add_lt_add_left hi.2 _⟩)
+      (λ hxy, hxy ▸ le_refl _),
+  add_lt_add_left := λ x y ⟨i, hi⟩ z,
+    ⟨i, λ j hji, show z j + x j = z j + y j, by rw [hi.1 j hji],
+      add_lt_add_left hi.2 _⟩,
+  ..pilex.partial_order,
+  ..pi.add_comm_group }