From 92feaf95b750c04c3d1967beb0de00f137f8f29b Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Fri, 18 May 2018 01:13:44 -0400
Subject: [PATCH] feat(computability/primrec): list definitions are primrec

---
 data/computability/primrec.lean | 313 +++++++++++++++++++++++++++-----
 data/denumerable.lean           |  13 ++
 data/encodable.lean             |  28 +++
 data/list/basic.lean            |   4 +
 data/nat/basic.lean             |  30 +--
 data/nat/pairing.lean           |  15 +-
 order/order_iso.lean            |   3 +-
 set_theory/ordinal.lean         |  16 +-
 8 files changed, 352 insertions(+), 70 deletions(-)

diff --git a/data/computability/primrec.lean b/data/computability/primrec.lean
index ace5e4d05da19..f1c18d17dbe14 100644
--- a/data/computability/primrec.lean
+++ b/data/computability/primrec.lean
@@ -184,7 +184,7 @@ protected theorem id : primrec (@id α) :=
 
 theorem comp {α β γ} [primcodable α] [primcodable β] [primcodable γ]
   {f : β → γ} {g : α → β} (hf : primrec f) (hg : primrec g) :
-  primrec (f ∘ g) :=
+  primrec (λ a, f (g a)) :=
 ((cases1 0 (hf.comp $ pred.comp hg)).comp (primcodable.prim α)).of_eq $
 λ n, begin
   simp; cases decode α n, {refl},
@@ -206,6 +206,9 @@ theorem of_nat_iff {α β} [denumerable α] [primcodable β]
   {f : α → β} : primrec f ↔ primrec (λ n, f (of_nat α n)) :=
 dom_denumerable.trans $ nat_iff.symm.trans encode_iff
 
+protected theorem of_nat (α) [denumerable α] : primrec (of_nat α) :=
+of_nat_iff.1 primrec.id
+
 theorem option_some_iff {f : α → σ} : primrec (λ a, some (f a)) ↔ primrec f :=
 ⟨λ h, encode_iff.1 $ pred.comp $ encode_iff.2 h, option_some.comp⟩
 
@@ -240,7 +243,7 @@ theorem fst {α β} [primcodable α] [primcodable β] :
 λ n, begin
   simp,
   cases decode α n.unpair.1; simp, {refl},
-  dsimp [option.bind, (∘)],
+  dsimp [option.bind],
   cases decode β n.unpair.2; simp, {refl},
   refl
 end
@@ -253,7 +256,7 @@ theorem snd {α β} [primcodable α] [primcodable β] :
 λ n, begin
   simp,
   cases decode α n.unpair.1; simp, {refl},
-  dsimp [option.bind, (∘)],
+  dsimp [option.bind],
   cases decode β n.unpair.2; simp, {refl},
   refl
 end
@@ -270,10 +273,10 @@ theorem unpair : primrec nat.unpair :=
 suffices primrec (λ n, (n ₗ, n ᵣ)), by simpa,
 pair (nat_iff.2 nat.primrec.left) (nat_iff.2 nat.primrec.right)
 
-theorem list_nth : ∀ (l : list α), primrec l.nth
+theorem list_nth₁ : ∀ (l : list α), primrec l.nth
 | []     := dom_denumerable.2 zero
 | (a::l) := dom_denumerable.2 $
-  (cases1 (encode a).succ $ dom_denumerable.1 $ list_nth l).of_eq $
+  (cases1 (encode a).succ $ dom_denumerable.1 $ list_nth₁ l).of_eq $
   λ n, by cases n; simp
 
 end primrec
@@ -318,7 +321,7 @@ theorem mkpair : primrec₂ nat.mkpair :=
 by simp [primrec₂, primrec, option.bind]; constructor
 
 theorem unpaired {f : ℕ → ℕ → α} : primrec (nat.unpaired f) ↔ primrec₂ f :=
-⟨λ h, by simpa [(∘)] using h.comp mkpair,
+⟨λ h, by simpa using h.comp mkpair,
  λ h, h.comp primrec.unpair⟩
 
 theorem unpaired' {f : ℕ → ℕ → ℕ} : nat.primrec (nat.unpaired f) ↔ primrec₂ f :=
@@ -420,6 +423,9 @@ namespace primrec
 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {σ : Type*}
 variables [primcodable α] [primcodable β] [primcodable γ] [primcodable δ] [primcodable σ]
 
+theorem to₂ {f : α × β → σ} (hf : primrec f) : primrec₂ (λ a b, f (a, b)) :=
+hf.of_eq $ λ ⟨a, b⟩, rfl
+
 theorem nat_elim {f : α → β} {g : α → ℕ × β → β}
   (hf : primrec f) (hg : primrec₂ g) :
   primrec₂ (λ a (n : ℕ), n.elim (f a) (λ n IH, g a (n, IH))) :=
@@ -433,9 +439,9 @@ primrec₂.nat_iff.2 $ ((nat.primrec.cases nat.primrec.zero $
 λ n, begin
   simp,
   cases decode α n.unpair.1 with a, {refl},
-  simp [(∘), encodek, option.map, option.bind],
+  simp [encodek, option.map, option.bind],
   symmetry,
-  induction n.unpair.2 with m; simp [(∘), encodek, option.bind],
+  induction n.unpair.2 with m; simp [encodek, option.bind],
   simp [ih],
   repeat {simp [encodek, option.map, option.bind]}
 end
@@ -445,7 +451,7 @@ theorem nat_elim' {f : α → ℕ} {g : α → β} {h : α → ℕ × β → β}
   primrec (λ a, (f a).elim (g a) (λ n IH, h a (n, IH))) :=
 (nat_elim hg hh).comp primrec.id hf
 
-theorem nat_elim1 {f : ℕ → α → α} (a : α) (hf : primrec₂ f) :
+theorem nat_elim₁ {f : ℕ → α → α} (a : α) (hf : primrec₂ f) :
   primrec (nat.elim a f) :=
 nat_elim' primrec.id (const a) $ comp₂ hf primrec₂.right
 
@@ -460,10 +466,16 @@ theorem nat_cases {f : α → ℕ} {g : α → β} {h : α → ℕ → β}
   primrec (λ a, (f a).cases (g a) (h a)) :=
 (nat_cases' hg hh).comp primrec.id hf
 
-theorem nat_cases1 {f : ℕ → α} (a : α) (hf : primrec f) :
+theorem nat_cases₁ {f : ℕ → α} (a : α) (hf : primrec f) :
   primrec (nat.cases a f) :=
 nat_cases primrec.id (const a) (comp₂ hf primrec₂.right)
 
+theorem nat_iterate {f : α → ℕ} {g : α → β} {h : α → β → β}
+  (hf : primrec f) (hg : primrec g) (hh : primrec₂ h) :
+  primrec (λ a, (h a)^[f a] (g a)) :=
+(nat_elim' hf hg (hh.comp₂ primrec₂.left $ snd.comp₂ primrec₂.right)).of_eq $
+λ a, by induction f a; simp [*, -nat.iterate_succ, nat.iterate_succ']
+
 theorem option_cases {o : α → option β} {f : α → σ} {g : α → β → σ}
   (ho : primrec o) (hf : primrec f) (hg : primrec₂ g) :
   @primrec _ σ _ _ (λ a, option.cases_on (o a) (f a) (g a)) :=
@@ -471,7 +483,7 @@ encode_iff.1 $
 (nat_cases (encode_iff.2 ho) (encode_iff.2 hf) $
   pred.comp₂ $ primrec₂.encode_iff.2 $
   (primrec₂.nat_iff'.1 hg).comp₂
-    ((@primrec.encode α _).comp₂ primrec₂.left)
+    ((@primrec.encode α _).comp fst).to₂
     primrec₂.right).of_eq $
 λ a, begin
   cases o a with b; simp [encodek]; refl
@@ -483,16 +495,16 @@ theorem option_bind {f : α → option β} {g : α → β → option σ}
 (option_cases hf (const none) hg).of_eq $
 λ a, by cases f a; refl
 
-theorem option_bind1 {f : α → option σ} (hf : primrec f) :
+theorem option_bind₁ {f : α → option σ} (hf : primrec f) :
   primrec (λ o, option.bind o f) :=
-option_bind primrec.id (hf.comp₂ primrec₂.right)
+option_bind primrec.id (hf.comp snd).to₂
 
 theorem option_map {f : α → option β} {g : α → β → σ}
   (hf : primrec f) (hg : primrec₂ g) : primrec (λ a, (f a).map (g a)) :=
 option_bind hf (option_some.comp₂ hg)
 
-theorem option_map1 {f : α → σ} (hf : primrec f) : primrec (option.map f) :=
-option_map primrec.id (hf.comp₂ primrec₂.right)
+theorem option_map₁ {f : α → σ} (hf : primrec f) : primrec (option.map f) :=
+option_map primrec.id (hf.comp snd).to₂
 
 theorem option_iget [inhabited α] : primrec (@option.iget α _) :=
 (option_cases primrec.id (const $ default α) primrec₂.right).of_eq $
@@ -501,9 +513,9 @@ theorem option_iget [inhabited α] : primrec (@option.iget α _) :=
 theorem bind_decode_iff {f : α → β → option σ} : primrec₂ (λ a n,
   (decode β n).bind (f a)) ↔ primrec₂ f :=
 ⟨λ h, by simpa [encodek] using
-   h.comp primrec₂.left ((@primrec.encode β _).comp primrec₂.right),
+   h.comp fst ((@primrec.encode β _).comp snd),
  λ h, option_bind (primrec.decode.comp snd) $
-   h.comp (fst.comp primrec₂.left) primrec₂.right⟩
+   h.comp (fst.comp fst) snd⟩
 
 theorem map_decode_iff {f : α → β → σ} : primrec₂ (λ a n,
   (decode β n).map (f a)) ↔ primrec₂ f :=
@@ -521,7 +533,7 @@ primrec₂.unpaired'.1 nat.primrec.mul
 theorem cond {c : α → bool} {f : α → σ} {g : α → σ}
   (hc : primrec c) (hf : primrec f) (hg : primrec g) :
   primrec (λ a, cond (c a) (f a) (g a)) :=
-(nat_cases (encode_iff.2 hc) hg (hf.comp₂ primrec₂.left)).of_eq $
+(nat_cases (encode_iff.2 hc) hg (hf.comp fst).to₂).of_eq $
 λ a, by cases c a; refl
 
 theorem ite {c : α → Prop} [decidable_pred c] {f : α → σ} {g : α → σ}
@@ -529,11 +541,8 @@ theorem ite {c : α → Prop} [decidable_pred c] {f : α → σ} {g : α → σ}
   primrec (λ a, if c a then f a else g a) :=
 by simpa using cond hc hf hg
 
-theorem list_inth [inhabited α] (l : list α) : primrec l.inth :=
-option_iget.comp (list_nth _)
-
 theorem nat_le : primrec_rel ((≤) : ℕ → ℕ → Prop) :=
-(nat_cases nat_sub (const tt) (primrec₂.const ff)).of_eq $
+(nat_cases nat_sub (const tt) (const ff).to₂).of_eq $
 λ p, begin
   dsimp [function.swap],
   cases e : p.1 - p.2 with n,
@@ -580,33 +589,31 @@ have primrec_rel (λ a b : ℕ, a = b), from
   (primrec.encode.comp₂ primrec₂.right)).of_eq $
 λ a b, encode_injective.eq_iff.symm
 
-theorem list_find_index {p : α → β → Prop}
+theorem list_find_index₁ {p : α → β → Prop}
   [∀ a b, decidable (p a b)] (hp : primrec_rel p) :
   ∀ (l : list β), primrec (λ a, l.find_index (p a))
 | [] := const 0
 | (a::l) := ite (hp.comp primrec.id (const a)) (const 0)
-  (succ.comp (list_find_index l))
+  (succ.comp (list_find_index₁ l))
 
-theorem list_index_of [decidable_eq α] (l : list α) :
-  primrec (λ a, l.index_of a) := list_find_index primrec.eq l
+theorem list_index_of₁ [decidable_eq α] (l : list α) :
+  primrec (λ a, l.index_of a) := list_find_index₁ primrec.eq l
 
 theorem dom_fintype [fintype α] (f : α → σ) : primrec f :=
 let ⟨l, nd, m⟩ := fintype.exists_univ_list α in
 option_some_iff.1 $ begin
   haveI := decidable_eq_of_encodable α,
-  refine ((list_nth (l.map f)).comp (list_index_of l)).of_eq (λ a, _),
-  simp [(∘)],
+  refine ((list_nth₁ (l.map f)).comp (list_index_of₁ l)).of_eq (λ a, _),
+  simp,
   rw [list.nth_le_nth (list.index_of_lt_length.2 (m _)),
       list.index_of_nth_le]; refl
 end
 
 theorem nat_bodd_div2 : primrec nat.bodd_div2 :=
 (nat_elim' primrec.id (const (ff, 0))
-  (primrec.comp₂
-    ((cond fst
+  (((cond fst
       (pair (const ff) (succ.comp snd))
-      (pair (const tt) snd)).comp snd)
-    primrec₂.right)).of_eq $
+      (pair (const tt) snd)).comp snd).comp snd).to₂).of_eq $
 λ n, begin
   simp [-nat.bodd_div2_eq], symmetry,
   induction n with n IH, {refl},
@@ -639,9 +646,7 @@ nat_elim' fst (const (0, 0)) $
   ((ite ((@primrec.eq ℕ _ _).comp (succ.comp $ snd.comp snd) fst)
       (pair (succ.comp $ fst.comp snd) (const 0))
       (pair (fst.comp snd) (succ.comp $ snd.comp snd)))
-    .comp₂ (primrec₂.pair.comp₂
-    (snd.comp₂ primrec₂.left)
-    (snd.comp₂ primrec₂.right))),
+    .comp (pair (snd.comp fst) (snd.comp snd))).to₂,
 suffices ∀ k n, (n / k, n % k) = f (n, k),
 from hf.of_eq $ λ ⟨m, n⟩, by simp [this],
 λ k n, begin
@@ -671,6 +676,76 @@ theorem nat_mod : primrec₂ ((%) : ℕ → ℕ → ℕ) := snd.comp₂ nat_div_
 
 end primrec
 
+section
+variables {α : Type*} {β : Type*} {σ : Type*}
+variables [primcodable α] [primcodable β] [primcodable σ]
+
+variable (H : nat.primrec (λ n, encodable.encode (decode (list β) n)))
+include H
+open primrec
+
+private def prim : primcodable (list β) := ⟨H⟩
+
+private lemma list_cases'
+  {f : α → list β} {g : α → σ} {h : α → β × list β → σ}
+  (hf : by haveI := prim H; exact primrec f) (hg : primrec g)
+  (hh : by haveI := prim H; exact primrec₂ h) :
+  @primrec _ σ _ _ (λ a, list.cases_on (f a) (g a) (λ b l, h a (b, l))) :=
+by letI := prim H; exact
+have @primrec _ (option σ) _ _ (λ a,
+  (decode (option (list β × β)) (encode (f a))).map
+  (λ o, option.cases_on o (g a) (λ p, h a (p.2, p.1)))), from
+((@map_decode_iff _ (option (list β × β)) _ _ _ _ _).2 $
+    to₂ $ option_cases snd (hg.comp fst)
+  (hh.comp₂ (fst.comp₂ primrec₂.left)
+    (primrec.comp₂ (pair snd fst) primrec₂.right)))
+    .comp primrec.id (encode_iff.2 hf),
+option_some_iff.1 $ this.of_eq $
+λ a, by cases f a with b l; simp [encodek]; refl
+
+private lemma list_foldl'
+  {f : α → list β} {g : α → σ} {h : α → σ × β → σ}
+  (hf : by haveI := prim H; exact primrec f) (hg : primrec g)
+  (hh : by haveI := prim H; exact primrec₂ h) :
+  primrec (λ a, (f a).foldl (λ s b, h a (s, b)) (g a)) :=
+by letI := prim H; exact
+let G (a : α) (IH : σ × list β) : σ × list β :=
+  list.cases_on IH.2 IH (λ b l, (h a (IH.1, b), l)) in
+let F (a : α) (n : ℕ) := nat.iterate (G a) n (g a, f a) in
+have primrec (λ a, (F a (encode (f a))).1), from
+fst.comp $ nat_iterate (encode_iff.2 hf) (pair hg hf) $
+  list_cases' H (snd.comp snd) snd $ to₂ $ pair
+    (hh.comp (fst.comp fst) $
+      pair ((fst.comp snd).comp fst) (fst.comp snd))
+    (snd.comp snd),
+this.of_eq $ λ a, begin
+  have : ∀ n, F a n =
+    ((list.take n (f a)).foldl (λ s b, h a (s, b)) (g a),
+      list.drop n (f a)),
+  { intro, simp [F],
+    generalize : f a = l, generalize : g a = x,
+    induction n with n IH generalizing l x, {refl},
+    simp, cases l with b l; simp [IH] },
+  rw [this, list.take_all_of_ge (length_le_encode _)]
+end
+
+private lemma list_cons' : by haveI := prim H; exact primrec₂ (@list.cons β) :=
+by letI := prim H; exact
+encode_iff.1 (succ.comp $
+primrec₂.mkpair.comp (encode_iff.2 snd) (encode_iff.2 fst))
+
+private lemma list_reverse' : by haveI := prim H; exact
+  primrec (@list.reverse β) :=
+by letI := prim H; exact
+(list_foldl' H primrec.id (const []) $ to₂ $
+   ((list_cons' H).comp snd fst).comp snd).of_eq
+(suffices ∀ l r, list.reverse_core l r =
+  list.foldl (λ (s : list β) (b : β), b :: s) r l,
+from λ l, this l [],
+λ l, by induction l; simp [*, list.reverse_core])
+
+end
+
 namespace primcodable
 variables {α : Type*} {β : Type*}
 variables [primcodable α] [primcodable β]
@@ -679,12 +754,10 @@ open primrec
 instance sum : primcodable (α ⊕ β) :=
 ⟨primrec.nat_iff.1 $
 (encode_iff.2 (cond nat_bodd
-  (((@primrec.decode β _).comp nat_div2).option_map $
-     nat_bit.comp₂ (primrec₂.const tt)
-       (primrec.encode.comp₂ primrec₂.right))
-  (((@primrec.decode α _).comp nat_div2).option_map $
-     nat_bit.comp₂ (primrec₂.const ff)
-       (primrec.encode.comp₂ primrec₂.right)))).of_eq $
+  (((@primrec.decode β _).comp nat_div2).option_map $ to₂ $
+     nat_bit.comp (const tt) (primrec.encode.comp snd))
+  (((@primrec.decode α _).comp nat_div2).option_map $ to₂ $
+     nat_bit.comp (const ff) (primrec.encode.comp snd)))).of_eq $
 λ n, show encode (decode_sum n) = _, begin
   simp [decode_sum],
   cases nat.bodd n; simp [decode_sum],
@@ -692,4 +765,160 @@ instance sum : primcodable (α ⊕ β) :=
   { cases decode β n.div2; refl }
 end⟩
 
-end primcodable
\ No newline at end of file
+instance list : primcodable (list α) := ⟨
+by letI H := primcodable.prim (list ℕ); exact
+have primrec₂ (λ (a : α) (o : option (list ℕ)),
+  o.map (list.cons (encode a))), from
+option_map snd $
+  (list_cons' H).comp ((@primrec.encode α _).comp (fst.comp fst)) snd,
+have primrec (λ n, (of_nat (list ℕ) n).reverse.foldl
+  (λ o m, (decode α m).bind (λ a, o.map (list.cons (encode a))))
+   (some [])), from
+list_foldl' H
+  ((list_reverse' H).comp (primrec.of_nat (list ℕ)))
+  (const (some []))
+  (primrec.comp₂ (bind_decode_iff.2 $ primrec₂.swap this) primrec₂.right),
+nat_iff.1 $ (encode_iff.2 this).of_eq $ λ n, begin
+  rw list.foldl_reverse,
+  apply nat.case_strong_induction_on n, {refl},
+  intros n IH, simp,
+  cases decode α n.unpair.2 with a, {refl},
+  simp [option.bind, has_seq.seq],
+  suffices : ∀ o (p : option (list ℕ)) (_ : encode o = encode p),
+    encode (option.map (list.cons a) o) =
+    encode (option.map (list.cons (encode a)) p),
+  from this _ _ (IH _ (nat.unpair_le n)),
+  intros o p IH,
+  cases o; cases p; injection IH with h,
+  exact congr_arg (λ k, -(k, encode a)-.succ.succ) h
+end⟩
+
+end primcodable
+
+namespace primrec
+variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {σ : Type*}
+variables [primcodable α] [primcodable β] [primcodable γ] [primcodable δ] [primcodable σ]
+
+theorem sum_inl : primrec (@sum.inl α β) :=
+encode_iff.1 $ nat_bit0.comp primrec.encode
+
+theorem sum_inr : primrec (@sum.inr α β) :=
+encode_iff.1 $ nat_bit1.comp primrec.encode
+
+theorem sum_cases
+  {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ}
+  (hf : primrec f) (hg : primrec₂ g) (hh : primrec₂ h) :
+  @primrec _ σ _ _ (λ a, sum.cases_on (f a) (g a) (h a)) :=
+option_some_iff.1 $
+(cond (nat_bodd.comp $ encode_iff.2 hf)
+  (option_map (primrec.decode.comp $ nat_div2.comp $ encode_iff.2 hf) hh)
+  (option_map (primrec.decode.comp $ nat_div2.comp $ encode_iff.2 hf) hg)).of_eq $
+λ a, by cases f a with b c;
+  simp [nat.div2_bit, nat.bodd_bit, encodek]; refl
+
+theorem list_cons : primrec₂ (@list.cons α) :=
+list_cons' (primcodable.prim _)
+
+theorem list_cases
+  {f : α → list β} {g : α → σ} {h : α → β × list β → σ} :
+  primrec f → primrec g → primrec₂ h →
+  @primrec _ σ _ _ (λ a, list.cases_on (f a) (g a) (λ b l, h a (b, l))) :=
+list_cases' (primcodable.prim _)
+
+theorem list_foldl
+  {f : α → list β} {g : α → σ} {h : α → σ × β → σ} :
+  primrec f → primrec g → primrec₂ h →
+  primrec (λ a, (f a).foldl (λ s b, h a (s, b)) (g a)) :=
+list_foldl' (primcodable.prim _)
+
+theorem list_reverse : primrec (@list.reverse α) :=
+list_reverse' (primcodable.prim _)
+
+theorem list_foldr
+  {f : α → list β} {g : α → σ} {h : α → β × σ → σ}
+  (hf : primrec f) (hg : primrec g) (hh : primrec₂ h) :
+  primrec (λ a, (f a).foldr (λ b s, h a (b, s)) (g a)) :=
+(list_foldl (list_reverse.comp hf) hg $ to₂ $
+  hh.comp fst $ (pair snd fst).comp snd).of_eq $
+λ a, by simp [list.foldl_reverse]
+
+theorem list_rec
+  {f : α → list β} {g : α → σ} {h : α → β × list β × σ → σ}
+  (hf : primrec f) (hg : primrec g) (hh : primrec₂ h) :
+  @primrec _ σ _ _ (λ a,
+    list.rec_on (f a) (g a) (λ b l IH, h a (b, l, IH))) :=
+let F (a : α) := (f a).foldr
+  (λ (b : β) (s : list β × σ), (b :: s.1, h a (b, s))) ([], g a) in
+have primrec F, from
+list_foldr hf (pair (const []) hg) $ to₂ $
+  pair ((list_cons.comp fst (fst.comp snd)).comp snd) hh,
+(snd.comp this).of_eq $ λ a, begin
+  suffices : F a = (f a,
+    list.rec_on (f a) (g a) (λ b l IH, h a (b, l, IH))), {rw this},
+  simp [F], induction f a with b l IH; simp *
+end
+
+theorem list_nth : primrec₂ (@list.nth α) :=
+let F (l : list α) (n : ℕ) :=
+l.foldl (λ (s : ℕ ⊕ α) (a : α),
+  sum.cases_on s
+    (@nat.cases (ℕ ⊕ α) (sum.inr a) sum.inl) sum.inr)
+  (sum.inl n) in
+have hF : primrec₂ F, from
+list_foldl fst (sum_inl.comp snd) ((sum_cases fst
+  (nat_cases snd
+    (sum_inr.comp $ snd.comp fst)
+    (sum_inl.comp snd).to₂).to₂
+  (sum_inr.comp snd).to₂).comp snd).to₂,
+have @primrec _ (option α) _ _ (λ p : list α × ℕ,
+  sum.cases_on (F p.1 p.2) (λ _, none) some), from
+sum_cases hF (const none).to₂ (option_some.comp snd).to₂,
+this.to₂.of_eq $ λ l n, begin
+  dsimp, symmetry,
+  induction l with a l IH generalizing n, {refl},
+  cases n with n,
+  { rw [(_ : F (a :: l) 0 = sum.inr a)], {refl},
+    clear IH, dsimp [F],
+    induction l with b l IH; simp * },
+  { apply IH }
+end
+
+theorem list_inth [inhabited α] : primrec₂ (@list.inth α _) :=
+option_iget.comp₂ list_nth
+
+theorem list_append : primrec₂ ((++) : list α → list α → list α) :=
+(list_foldr fst snd $ to₂ $ comp (@list_cons α _) snd).to₂.of_eq $
+λ l₁ l₂, by induction l₁; simp *
+
+theorem list_map
+  {f : α → list β} {g : α → β → σ}
+  (hf : primrec f) (hg : primrec₂ g) :
+  primrec (λ a, (f a).map (g a)) :=
+(list_foldr hf (const []) $ to₂ $ list_cons.comp
+  (hg.comp fst (fst.comp snd)) (snd.comp snd)).of_eq $
+λ a, by induction f a; simp *
+
+theorem list_join : primrec (@list.join α) :=
+(list_foldr primrec.id (const []) $ to₂ $
+  comp (@list_append α _) snd).of_eq $
+λ l, by dsimp; induction l; simp *
+
+theorem list_length : primrec (@list.length α) :=
+(list_foldr (@primrec.id (list α) _) (const 0) $ to₂ $
+  (succ.comp $ snd.comp snd).to₂).of_eq $
+λ l, by dsimp; induction l; simp [*, -add_comm]
+
+theorem list_find_index {f : α → list β} {p : α → β → Prop}
+  [∀ a b, decidable (p a b)]
+  (hf : primrec f) (hp : primrec_rel p) :
+  primrec (λ a, (f a).find_index (p a)) :=
+(list_foldr hf (const 0) $ to₂ $
+  ite (hp.comp fst $ fst.comp snd) (const 0)
+    (succ.comp $ snd.comp snd)).of_eq $
+λ a, eq.symm $ by dsimp; induction f a with b l;
+  [refl, { simp [*, list.find_index], congr }]
+
+theorem list_index_of [decidable_eq α] : primrec₂ (@list.index_of α _) :=
+to₂ $ list_find_index snd $ primrec.eq.comp₂ (fst.comp fst).to₂ snd.to₂
+
+end primrec
\ No newline at end of file
diff --git a/data/denumerable.lean b/data/denumerable.lean
index 898f8181476c4..d3ee925f5fc86 100644
--- a/data/denumerable.lean
+++ b/data/denumerable.lean
@@ -117,6 +117,19 @@ end
 
 instance denumerable_list : denumerable (list α) := ⟨denumerable_list_aux⟩
 
+@[simp] theorem list_of_nat_zero : of_nat (list α) 0 = [] := rfl
+
+@[simp] theorem list_of_nat_succ (v : ℕ) :
+  of_nat (list α) (succ v) =
+  of_nat α v.unpair.2 :: of_nat (list α) v.unpair.1 :=
+of_nat_of_decode $ show decode_list (succ v) = _,
+begin
+  cases e : unpair v with v₂ v₁,
+  simp [decode_list, e],
+  rw [show decode_list v₂ = decode (list α) v₂,
+      from rfl, decode_eq_of_nat]; refl
+end
+
 section multiset
 
 def lower : list ℕ → ℕ → list ℕ
diff --git a/data/encodable.lean b/data/encodable.lean
index 2ec255f58b974..047bac29429b6 100644
--- a/data/encodable.lean
+++ b/data/encodable.lean
@@ -93,6 +93,14 @@ instance sum : encodable (α ⊕ β) :=
 ⟨encode_sum, decode_sum, λ s,
   by cases s; simp [encode_sum, decode_sum];
      rw [bodd_bit, div2_bit, decode_sum, encodek]; refl⟩
+
+@[simp] theorem encode_inl (a : α) :
+  @encode (α ⊕ β) _ (sum.inl a) = bit ff (encode a) := rfl
+@[simp] theorem encode_inr (b : β) :
+  @encode (α ⊕ β) _ (sum.inr b) = bit tt (encode b) := rfl
+@[simp] theorem decode_sum_val (n : ℕ) :
+  decode (α ⊕ β) n = decode_sum n := rfl
+
 end sum
 
 instance bool : encodable bool :=
@@ -173,6 +181,26 @@ def decode_list : ℕ → option (list α)
 instance list : encodable (list α) :=
 ⟨encode_list, decode_list, λ l,
   by induction l with a l IH; simp [encode_list, decode_list, unpair_mkpair, encodek, *]⟩
+
+@[simp] theorem encode_list_nil : encode (@nil α) = 0 := rfl
+@[simp] theorem encode_list_cons (a : α) (l : list α) :
+  encode (a :: l) = succ (mkpair (encode l) (encode a)) := rfl
+
+@[simp] theorem decode_list_zero : decode (list α) 0 = some [] := rfl
+
+@[simp] theorem decode_list_succ (v : ℕ) :
+  decode (list α) (succ v) =
+  (::) <$> decode α v.unpair.2 <*> decode (list α) v.unpair.1 :=
+show decode_list (succ v) = _, begin
+  cases e : unpair v with v₂ v₁,
+  simp [decode_list, e], refl
+end
+
+theorem length_le_encode : ∀ (l : list α), length l ≤ encode l
+| [] := zero_le _
+| (a :: l) := succ_le_succ $
+  le_trans (length_le_encode l) (le_mkpair_left _ _)
+
 end list
 
 section finset
diff --git a/data/list/basic.lean b/data/list/basic.lean
index eb1f4cc2718d1..93fdc1bc99596 100644
--- a/data/list/basic.lean
+++ b/data/list/basic.lean
@@ -862,6 +862,10 @@ theorem take_take : ∀ (n m) (l : list α), take n (take m l) = take (min n m)
 | (succ n)  (succ m) nil    := by simp
 | (succ n)  (succ m) (a::l) := by simp [min_succ_succ, take_take]
 
+@[simp] theorem drop_nil : ∀ n, drop n [] = ([] : list α)
+| 0     := rfl
+| (n+1) := rfl
+
 theorem drop_eq_nth_le_cons : ∀ {n} {l : list α} h,
   drop n l = nth_le l n h :: drop (n+1) l
 | 0     (a::l) h := rfl
diff --git a/data/nat/basic.lean b/data/nat/basic.lean
index 4fa464d4d78b9..771ac73c6f1d9 100644
--- a/data/nat/basic.lean
+++ b/data/nat/basic.lean
@@ -373,19 +373,23 @@ by rw [← nat.add_sub_cancel' h, pow_add]; apply dvd_mul_right
 @[simp] theorem bodd_div2_eq (n : ℕ) : bodd_div2 n = (bodd n, div2 n) :=
 by unfold bodd div2; cases bodd_div2 n; refl
 
-/- foldl & foldr -/
-
-/-- `foldl op n a` is the `n`-times iterate of `op` on `a`. -/
-@[simp] def foldl {α : Sort*} (op : α → α) : ℕ → α → α
- | 0        a := a
- | (succ k) a := foldl k (op a)
-
-/-- `foldr op n a` is the `n`-times iterate of `op` on `a`.
-  It is provably the same as `foldl` but has different
-  definitional equalities. -/
-@[simp] def foldr {α : Sort*} (op : α → α) (a : α) : ℕ → α
- | 0        := a
- | (succ k) := op (foldr k)
+/- iterate -/
+
+section
+variables {α : Sort*} (op : α → α)
+
+@[simp] theorem iterate_zero (a : α) : op^[0] a = a := rfl
+
+@[simp] theorem iterate_succ (n : ℕ) (a : α) : op^[succ n] a = (op^[n]) (op a) := rfl
+
+theorem iterate_add : ∀ (m n : ℕ) (a : α), op^[m + n] a = (op^[m]) (op^[n] a)
+| m 0 a := rfl
+| m (succ n) a := iterate_add m n _
+
+theorem iterate_succ' (n : ℕ) (a : α) : op^[succ n] a = op (op^[n] a) :=
+by rw [← one_add, iterate_add]; refl
+
+end
 
 /- size and shift -/
 
diff --git a/data/nat/pairing.lean b/data/nat/pairing.lean
index 31851e2e073f2..a82a78629c88a 100644
--- a/data/nat/pairing.lean
+++ b/data/nat/pairing.lean
@@ -11,15 +11,15 @@ open prod decidable
 namespace nat
 
 /-- Pairing function for the natural numbers. -/
-def mkpair (a b : nat) : nat :=
+def mkpair (a b : ℕ) : ℕ :=
 if a < b then b*b + a else a*a + a + b
 
 /-- Unpairing function for the natural numbers. -/
-def unpair (n : nat) : nat × nat :=
+def unpair (n : ℕ) : ℕ × ℕ :=
 let s := sqrt n in
 if n - s*s < s then (n - s*s, s) else (s, n - s*s - s)
 
-@[simp] theorem mkpair_unpair (n : nat) : mkpair (unpair n).1 (unpair n).2 = n :=
+@[simp] theorem mkpair_unpair (n : ℕ) : mkpair (unpair n).1 (unpair n).2 = n :=
 let s := sqrt n in begin
   dsimp [unpair], change sqrt n with s,
   have sm : s * s + (n - s * s) = n := nat.add_sub_cancel' (sqrt_le _),
@@ -35,7 +35,7 @@ end
 theorem mkpair_unpair' {n a b} (H : unpair n = (a, b)) : mkpair a b = n :=
 by simpa [H] using mkpair_unpair n
 
-@[simp] theorem unpair_mkpair (a b : nat) : unpair (mkpair a b) = (a, b) :=
+@[simp] theorem unpair_mkpair (a b : ℕ) : unpair (mkpair a b) = (a, b) :=
 begin
   by_cases a < b; simp [h, mkpair],
   { show unpair (a + b * b) = (a, b),
@@ -55,7 +55,7 @@ begin
         nat.add_sub_cancel, nat.add_sub_cancel_left] }
 end
 
-theorem unpair_lt {n : nat} (n1 : n ≥ 1) : (unpair n).1 < n :=
+theorem unpair_lt {n : ℕ} (n1 : n ≥ 1) : (unpair n).1 < n :=
 let s := sqrt n in begin
   simp [unpair], change sqrt n with s,
   by_cases h : n - s * s < s; simp [h],
@@ -65,8 +65,11 @@ let s := sqrt n in begin
     exact lt_of_le_of_lt h (nat.sub_lt_self n1 (mul_pos s0 s0)) }
 end
 
-theorem unpair_le : ∀ (n : nat), (unpair n).1 ≤ n
+theorem unpair_le : ∀ (n : ℕ), (unpair n).1 ≤ n
 | 0     := dec_trivial
 | (n+1) := le_of_lt (unpair_lt (nat.succ_pos _))
 
+theorem le_mkpair_left (a b : ℕ) : a ≤ mkpair a b :=
+by simpa using unpair_le (mkpair a b)
+
 end nat
diff --git a/order/order_iso.lean b/order/order_iso.lean
index 653408e02c2ca..b513bc1f63a71 100644
--- a/order/order_iso.lean
+++ b/order/order_iso.lean
@@ -154,7 +154,8 @@ theorem well_founded_iff_no_descending_seq [is_strict_order α r] : well_founded
     show ∀ x : {a // ¬ acc r a}, ∃ y : {a // ¬ acc r a}, r y.1 x.1,
     from λ ⟨x, h⟩, classical.by_contradiction $ λ hn, h $
       ⟨_, λ y h, classical.by_contradiction $ λ na, hn ⟨⟨y, na⟩, h⟩⟩ in
-  N ⟨nat_gt (λ n, (n.foldr f ⟨a, na⟩).1) $ λ n, h _⟩⟩⟩
+  N ⟨nat_gt (λ n, (f^[n] ⟨a, na⟩).1) $ λ n,
+    by rw nat.iterate_succ'; apply h⟩⟩⟩
 
 end order_embedding
 
diff --git a/set_theory/ordinal.lean b/set_theory/ordinal.lean
index 30999842d2ecd..7d700fbbdf107 100644
--- a/set_theory/ordinal.lean
+++ b/set_theory/ordinal.lean
@@ -2556,20 +2556,20 @@ by rw [list.sorted, list.pairwise_map]; exact CNF_pairwise b o
 /-- The next fixed point function, the least fixed point of the
   normal function `f` above `a`. -/
 def nfp (f : ordinal → ordinal) (a : ordinal) :=
-sup (λ n : ℕ, n.foldr f a)
+sup (λ n : ℕ, f^[n] a)
 
-theorem foldr_le_nfp (f a n) : nat.foldr f a n ≤ nfp f a :=
+theorem iterate_le_nfp (f a n) : f^[n] a ≤ nfp f a :=
 le_sup _ n
 
 theorem le_nfp_self (f a) : a ≤ nfp f a :=
-foldr_le_nfp f a 0
+iterate_le_nfp f a 0
 
 theorem is_normal.lt_nfp {f} (H : is_normal f) {a b} :
   f b < nfp f a ↔ b < nfp f a :=
 lt_sup.trans $ iff.trans
   (by exact
    ⟨λ ⟨n, h⟩, ⟨n, lt_of_le_of_lt (H.le_self _) h⟩,
-    λ ⟨n, h⟩, ⟨n+1, H.lt_iff.2 h⟩⟩)
+    λ ⟨n, h⟩, ⟨n+1, by rw nat.iterate_succ'; exact H.lt_iff.2 h⟩⟩)
   lt_sup.symm
 
 theorem is_normal.nfp_le {f} (H : is_normal f) {a b} :
@@ -2579,8 +2579,8 @@ le_iff_le_iff_lt_iff_lt.2 H.lt_nfp
 theorem is_normal.nfp_le_fp {f} (H : is_normal f) {a b}
   (ab : a ≤ b) (h : f b ≤ b) : nfp f a ≤ b :=
 sup_le.2 $ λ i, begin
-  induction i with i IH, {exact ab},
-  exact le_trans (H.le_iff.2 IH) h
+  induction i with i IH generalizing a, {exact ab},
+  exact IH (le_trans (H.le_iff.2 ab) h),
 end
 
 theorem is_normal.nfp_fp {f} (H : is_normal f) (a) : f (nfp f a) = nfp f a :=
@@ -2589,13 +2589,13 @@ begin
   cases le_or_lt (f a) a with aa aa,
   { rwa le_antisymm (H.nfp_le_fp (le_refl _) aa) (le_nfp_self _ _) },
   rcases zero_or_succ_or_limit (nfp f a) with e|⟨b, e⟩|l,
-  { refine @le_trans _ _ _ (f a) _ (H.le_iff.2 _) (foldr_le_nfp f a 1),
+  { refine @le_trans _ _ _ (f a) _ (H.le_iff.2 _) (iterate_le_nfp f a 1),
     simp [e, zero_le] },
   { have : f b < nfp f a := H.lt_nfp.2 (by simp [e, lt_succ_self]),
     rw [e, lt_succ] at this,
     have ab : a ≤ b,
     { rw [← lt_succ, ← e],
-      exact lt_of_lt_of_le aa (foldr_le_nfp f a 1) },
+      exact lt_of_lt_of_le aa (iterate_le_nfp f a 1) },
     refine le_trans (H.le_iff.2 (H.nfp_le_fp ab this))
       (le_trans this (le_of_lt _)),
     simp [e, lt_succ_self] },