feat(computability/primrec): list definitions are primrec

Author: digama0

data/computability/primrec.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 ℕ

data/denumerable.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

data/encodable.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

data/list/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 -/
 

data/nat/basic.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

data/nat/pairing.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
 

order/order_iso.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] },