From 70bd95d931a8764590b4e66be020e37574fbdfa9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 9 Aug 2015 22:46:28 -0700
Subject: [PATCH] feat(library/data/list): show that (sort R l1 = sort R l2)
 when R is a decidable total order and l1 is a permutation of l2

---
 library/data/list/sort.lean   | 24 +++++++++++++++++++++--
 library/data/list/sorted.lean | 37 ++++++++++++++++++++++++++++++++++-
 2 files changed, 58 insertions(+), 3 deletions(-)

diff --git a/library/data/list/sort.lean b/library/data/list/sort.lean
index db8733c330..81981b32e4 100644
--- a/library/data/list/sort.lean
+++ b/library/data/list/sort.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 
 Naive sort for lists
 -/
-import data.list.comb data.list.set data.list.perm data.list.sorted logic.connectives
+import data.list.comb data.list.set data.list.perm data.list.sorted logic.connectives algebra.order
 
 namespace list
 open decidable nat
@@ -161,7 +161,27 @@ lemma strongly_sorted_sort_aux : ∀ {n : nat} {l : list A} (h : length l = n),
       show R m x,         from of_mem_of_all this `all l (R m)`),
   strongly_sorted.step hall ss
 
-lemma strongly_sorted_sort (to : total R) (tr : transitive R) (rf : reflexive R) (l : list A) : strongly_sorted R (sort R l) :=
+variable {R}
+
+lemma strongly_sorted_sort_core (to : total R) (tr : transitive R) (rf : reflexive R) (l : list A) : strongly_sorted R (sort R l) :=
 @strongly_sorted_sort_aux _ _ _ _ to tr rf (length l) l rfl
 
+lemma sort_eq_of_perm_core {l₁ l₂ : list A} (to : total R) (tr : transitive R) (rf : reflexive R) (asy : anti_symmetric R) (h : l₁ ~ l₂) : sort R l₁ = sort R l₂ :=
+have s₁ : sorted R (sort R l₁),  from sorted_of_strongly_sorted (strongly_sorted_sort_core to tr rf l₁),
+have s₂ : sorted R (sort R l₂),  from sorted_of_strongly_sorted (strongly_sorted_sort_core to tr rf l₂),
+have p  : sort R l₁ ~ sort R l₂, from calc
+  sort R l₁ ~ l₁        : sort_perm
+    ...     ~ l₂        : h
+    ...     ~ sort R l₂ : sort_perm,
+eq_of_sorted_of_perm tr asy p s₁ s₂
+
+section
+open algebra
+omit decR
+lemma strongly_sorted_sort [ord : decidable_linear_order A] (l : list A) : strongly_sorted has_le.le (sort has_le.le l) :=
+strongly_sorted_sort_core le.total (@le.trans A ord) le.refl l
+
+lemma sort_eq_of_perm {l₁ l₂ : list A} [ord : decidable_linear_order A] (h : l₁ ~ l₂) : sort has_le.le l₁ = sort has_le.le l₂ :=
+sort_eq_of_perm_core le.total (@le.trans A ord) le.refl (@le.antisymm A ord) h
+end
 end list
diff --git a/library/data/list/sorted.lean b/library/data/list/sorted.lean
index dc13438d80..112222f229 100644
--- a/library/data/list/sorted.lean
+++ b/library/data/list/sorted.lean
@@ -3,7 +3,7 @@ Copyright (c) 2015 Leonardo de Moura. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import data.list.comb
+import data.list.comb data.list.perm
 
 namespace list
 variable {A : Type}
@@ -94,4 +94,39 @@ theorem strongly_sorted_of_sorted_of_transitive (trans : transitive R) : ∀ {l}
   have strongly_sorted R l, from strongly_sorted_of_sorted_of_transitive this,
   have all l (R a),         from sorted_extends trans h,
   strongly_sorted.step `all l (R a)` `strongly_sorted R l`
+
+open perm
+
+lemma eq_of_sorted_of_perm (tr : transitive R) (anti : anti_symmetric R) : ∀ {l₁ l₂ : list A}, l₁ ~ l₂ → sorted R l₁ → sorted R l₂ → l₁ = l₂
+| []       []       h₁ h₂ h₃ := rfl
+| (a₁::l₁) []       h₁ h₂ h₃ := absurd (perm.symm h₁) !not_perm_nil_cons
+| []       (a₂::l₂) h₁ h₂ h₃ := absurd h₁ !not_perm_nil_cons
+| (a::l₁)  l₂       h₁ h₂ h₃ :=
+  have aux : ∀ {t}, l₂ = a::t → a::l₁ = l₂, from
+    take t, suppose l₂ = a::t,
+    have   l₁ ~ t,      by rewrite [this at h₁]; apply perm_cons_inv h₁,
+    have   sorted R l₁, from and.right (sorted_inv h₂),
+    have   sorted R t,  by rewrite [`l₂ = a::t` at h₃]; exact and.right (sorted_inv h₃),
+    assert l₁ = t,      from eq_of_sorted_of_perm `l₁ ~ t` `sorted R l₁` `sorted R t`,
+    show a :: l₁ = l₂,  by rewrite [`l₂ = a::t`, this],
+  have   a ∈ l₂,                       from mem_perm h₁ !mem_cons,
+  obtain s t (e₁ : l₂ = s ++ (a::t)),  from mem_split this,
+  begin
+    cases s with b s,
+    { have l₂ = a::t, by exact e₁,
+      exact aux this },
+    { have e₁   : l₂ = b::(s++(a::t)), by exact e₁,
+      have b ∈ l₂,                by rewrite e₁; apply mem_cons,
+      have hall₂ : all (s++(a::t)) (R b), begin rewrite [e₁ at h₃], apply sorted_extends tr h₃ end,
+      have a ∈ s++(a::t),         from mem_append_right _ !mem_cons,
+      have R b a,                 from of_mem_of_all this hall₂,
+      have b ∈ a::l₁,             from mem_perm (perm.symm h₁) `b ∈ l₂`,
+      have hall₁ : all l₁ (R a),  from sorted_extends tr h₂,
+      apply or.elim (eq_or_mem_of_mem_cons `b ∈ a::l₁`),
+        suppose b = a,  by rewrite this at e₁; exact aux e₁,
+        suppose b ∈ l₁,
+          have   R a b, from of_mem_of_all this hall₁,
+          assert b = a, from anti `R b a` `R a b`,
+          by rewrite this at e₁; exact aux e₁ }
+  end
 end list