From d6eae3265c9fdc15031d7ffff79aa81255b09eeb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= <johannes.hoelzl@gmx.de>
Date: Tue, 7 Mar 2017 20:02:53 -0500
Subject: [PATCH] feat(library/data/dlist): setup transfer for dlist

---
 library/data/dlist.lean         | 53 +++++++++++++++++++++++++++++++++
 library/init/meta/transfer.lean | 11 ++++---
 library/init/relator.lean       |  3 ++
 3 files changed, 61 insertions(+), 6 deletions(-)

diff --git a/library/data/dlist.lean b/library/data/dlist.lean
index cf1d9fc3b3..c9efafe42e 100644
--- a/library/data/dlist.lean
+++ b/library/data/dlist.lean
@@ -85,4 +85,57 @@ by cases l; rsimp
 lemma to_list_concat (x : α) (l : dlist α) : to_list (concat x l) = to_list l ++ [x] :=
 by cases l; simp; rsimp
 
+section transfer
+
+protected def rel_dlist_list (d : dlist α) (l : list α) : Prop :=
+to_list d = l
+
+instance bi_total_rel_dlist_list : @relator.bi_total (dlist α) (list α) dlist.rel_dlist_list :=
+⟨take d, ⟨to_list d, rfl⟩, take l, ⟨of_list l, to_list_of_list l⟩⟩
+
+protected lemma rel_eq :
+  (dlist.rel_dlist_list ⇒ dlist.rel_dlist_list ⇒ iff) (@eq (dlist α)) eq
+| l₁ ._ rfl l₂ ._ rfl := ⟨congr_arg to_list,
+  suppose to_list l₁ = to_list l₂,
+  have of_list (to_list l₁) = of_list (to_list l₂), from congr_arg of_list this,
+  by simp [of_list_to_list] at this; assumption⟩
+
+protected lemma rel_empty : dlist.rel_dlist_list (@empty α) [] :=
+to_list_empty
+
+protected lemma rel_singleton : (@eq α ⇒ dlist.rel_dlist_list) (λx, singleton x) (λx, [x])
+| ._ x rfl := to_list_singleton x
+
+protected lemma rel_append :
+  (dlist.rel_dlist_list ⇒ dlist.rel_dlist_list ⇒ dlist.rel_dlist_list) (λ(x y : dlist α), x ++ y) (λx y, x ++ y)
+| l₁ ._ rfl l₂ ._ rfl := to_list_append l₁ l₂
+
+protected lemma rel_cons :
+  (@eq α ⇒ dlist.rel_dlist_list ⇒ dlist.rel_dlist_list) cons (λx y, x :: y)
+| x ._ rfl l ._ rfl := to_list_cons x l
+
+protected lemma rel_concat :
+  (@eq α ⇒ dlist.rel_dlist_list ⇒ dlist.rel_dlist_list) concat (λx y, y ++ [x])
+| x ._ rfl l ._ rfl := to_list_concat x l
+
+protected meta def transfer : tactic unit := do
+  transfer.transfer [`relator.rel_forall_of_total, `dlist.rel_eq, `dlist.rel_empty,
+    `dlist.rel_singleton, `dlist.rel_append, `dlist.rel_cons, `dlist.rel_concat]
+
+example : ∀(a b c : dlist α), a ++ (b ++ c) = (a ++ b) ++ c :=
+begin
+  dlist.transfer,
+  intros,
+  simp
+end
+
+example : ∀(a : α), singleton a ++ empty = singleton a :=
+begin
+  dlist.transfer,
+  intros,
+  simp
+end
+
+end transfer
+
 end dlist
diff --git a/library/init/meta/transfer.lean b/library/init/meta/transfer.lean
index 06a2377287..699df48186 100644
--- a/library/init/meta/transfer.lean
+++ b/library/init/meta/transfer.lean
@@ -83,7 +83,7 @@ private meta def mark_occurences (e : expr) : list expr → list (expr × bool)
 | (h :: t) := let xs := mark_occurences t in
   (h, occurs h e || any xs (λ⟨e, oc⟩, oc && occurs h e)) :: xs
 
-private meta def analyse_rule (pr : expr) : tactic rule_data := do
+private meta def analyse_rule (u' : list name) (pr : expr) : tactic rule_data := do
   t ← infer_type pr,
   (params, app (app r f) g) ← mk_local_pis t,
   (arg_rels, R) ← get_lift_fun r,
@@ -93,8 +93,7 @@ private meta def analyse_rule (pr : expr) : tactic rule_data := do
   p       ← head_beta (app_of_list f a_vars),
   p_data  ← return $ mark_occurences (app R p) params,
   p_vars  ← return $ list.map prod.fst (list.filter (λx, ↑x.2) p_data),
-  u'      ← return $ collect_univ_params t,
-  u       ← return $ collect_univ_params (app R p),
+  u       ← return $ collect_univ_params (app R p) ∩ u',
   pat     ← mk_pattern (fmap level.param u) (p_vars ++ a_vars) (app R p) (fmap level.param u) (p_vars ++ a_vars),
   return $ rule_data.mk pr (list.remove_all u' u) p_data u args pat g
 
@@ -102,8 +101,8 @@ private meta def analyse_decls : list name → tactic (list rule_data) :=
   monad.mapm (λn, do
     d ← get_decl n,
     c ← return d^.univ_params^.length,
-    l ← monad.for (range c) (λ_, level.param <$> mk_fresh_name),
-    analyse_rule (const n l))
+    ls ← monad.for (range c) (λ_, mk_fresh_name),
+    analyse_rule ls (const n (ls^.map level.param)))
 
 private meta def split_params_args : list (expr × bool) → list expr → list (expr × option expr) × list expr
 | ((lc, tt) :: ps) (e :: es) := let (ps', es') := split_params_args ps es in ((lc, some e) :: ps', es')
@@ -154,7 +153,7 @@ meta def compute_transfer : list rule_data → list expr → expr → tactic (ex
       b ← mk_local_def (("b" ++ to_string n) : string) arg^.out_type,
       R ← mk_local_def (("R" ++ to_string n) : string) (arg^.relation a b),
       return ((a, b), (R, [a, b, R]))) >>= (return ∘ prod.map unzip unzip ∘ unzip),
-    rds'      ← monad.for R_vars analyse_rule,
+    rds'      ← monad.for R_vars (analyse_rule []),
 
     -- Transfer argument
     a           ← return $ i e,
diff --git a/library/init/relator.lean b/library/init/relator.lean
index 2f12fe34f5..806bf5fa9b 100644
--- a/library/init/relator.lean
+++ b/library/init/relator.lean
@@ -67,4 +67,7 @@ take p q h r s l, imp_congr h l
 lemma rel_not : (iff ⇒ iff) not not :=
 take p q h, not_congr h
 
+instance bi_total_eq {α : Type u₁} : relator.bi_total (@eq α) :=
+⟨take a, ⟨a, rfl⟩, take a, ⟨a, rfl⟩⟩
+
 end relator