From f2df67053f161eba75c74afadf8bd970588488d9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 2 May 2018 12:36:31 -0700
Subject: [PATCH] feat(library/init/data/dlist): add dlist back without tactic
 framework dependency

---
 library/init/data/dlist.lean      | 52 +++++++++++++++++++++++++++++++
 library/init/data/list/basic.lean |  9 ++++++
 2 files changed, 61 insertions(+)
 create mode 100644 library/init/data/dlist.lean

diff --git a/library/init/data/dlist.lean b/library/init/data/dlist.lean
new file mode 100644
index 0000000000..caa36642c6
--- /dev/null
+++ b/library/init/data/dlist.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.data.list.basic init.function
+universes u
+/--
+A difference list is a function that, given a list, returns the original
+contents of the difference list prepended to the given list.
+This structure supports `O(1)` `append` and `concat` operations on lists, making it
+useful for append-heavy uses such as logging and pretty printing.
+-/
+structure dlist (α : Type u) :=
+(apply     : list α → list α)
+(invariant : ∀ l, apply l = apply [] ++ l)
+
+namespace dlist
+variables {α : Type u}
+open list
+
+def of_list (l : list α) : dlist α :=
+⟨append l, λ t, (append_nil l).symm ▸ rfl⟩
+
+def empty : dlist α :=
+⟨id, λ t, rfl⟩
+
+def to_list : dlist α → list α
+| ⟨f, h⟩ := f []
+
+def singleton : α → dlist α
+| a := ⟨λ t, a :: t, λ t, rfl⟩
+
+def cons : α → dlist α → dlist α
+| a ⟨f, h⟩ := ⟨λ t, a :: f t, λ t,
+               show a :: f t = a :: (f [] ++ t), from h t ▸ rfl⟩
+
+def append : dlist α → dlist α → dlist α
+| ⟨f, h₁⟩ ⟨g, h₂⟩ := ⟨f ∘ g, λ t,
+                      show f (g t) = (f (g [])) ++ t, from
+                      (h₁ (g [])).symm ▸ (append_assoc (f []) (g []) t).symm ▸ h₂ t ▸ h₁ (g t) ▸ rfl⟩
+
+def push : dlist α → α → dlist α
+| ⟨f, h⟩ a := ⟨λ t, f (a :: t), λ t, (h (a::t)).symm ▸ (h [a]).symm ▸ (append_assoc (f []) [a] t).symm ▸ rfl⟩
+
+
+
+instance : has_append (dlist α) :=
+⟨dlist.append⟩
+
+end dlist
diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean
index 8f8235ab8c..883065f990 100644
--- a/library/init/data/list/basic.lean
+++ b/library/init/data/list/basic.lean
@@ -40,6 +40,15 @@ list.has_dec_eq
 instance : has_append (list α) :=
 ⟨list.append⟩
 
+theorem append_nil : ∀ (l : list α), l ++ [] = l
+| []      := rfl
+| (a::as) := show a :: (as ++ []) = a :: as, from (append_nil as).symm ▸ rfl
+
+theorem append_assoc : ∀ (l₁ l₂ l₃ : list α), (l₁ ++ l₂) ++ l₃ = l₁ ++ (l₂ ++ l₃)
+| []      l₁ l₂ := rfl
+| (a::as) l₁ l₂ := show a :: (as ++ l₁ ++ l₂) = a :: (as ++ (l₁ ++ l₂)), from
+                   append_assoc as l₁ l₂ ▸ rfl
+
 protected def mem : α → list α → Prop
 | a []       := false
 | a (b :: l) := a = b ∨ mem a l