feat(computability/primrec): add traditional primrec definition

This shows that the pairing function with its square roots does not give any additional power.

Author: digama0

data/computability/primrec.lean

@@ -267,16 +267,26 @@ def encode_subtype : {a : α // P a} → nat
 
 include decP
 def decode_subtype (v : nat) : option {a : α // P a} :=
-match decode α v with
-| some a := if h : P a then some ⟨a, h⟩ else none
-| none   := none
-end
+(decode α v).bind $ λ a,
+if h : P a then some ⟨a, h⟩ else none
 
 instance subtype : encodable {a : α // P a} :=
 ⟨encode_subtype, decode_subtype,
  λ ⟨v, h⟩, by simp [encode_subtype, decode_subtype, encodek, h]⟩
 end subtype
 
+instance fin (n) : encodable (fin n) :=
+of_equiv _ (equiv.fin_equiv_subtype _)
+
+instance vector [encodable α] {n} : encodable (vector α n) :=
+encodable.subtype
+
+instance fin_arrow [encodable α] {n} : encodable (fin n → α) :=
+of_equiv _ (equiv.vector_equiv_fin _ _).symm
+
+instance array [encodable α] {n} : encodable (array n α) :=
+of_equiv _ (equiv.array_equiv_fin _ _)
+
 instance int : encodable ℤ :=
 of_equiv _ equiv.int_equiv_nat
 

data/encodable.lean

@@ -8,8 +8,8 @@ We say two types are equivalent if they are isomorphic.
 
 Two equivalent types have the same cardinality.
 -/
-import data.prod data.nat.pairing logic.function tactic data.set.lattice
-import algebra.group
+import data.prod data.nat.pairing logic.function tactic.basic
+import data.set.lattice algebra.group data.vector2
 open function
 
 universes u v w
@@ -449,6 +449,21 @@ def list_equiv_of_equiv {α β : Type*} : α ≃ β → list α ≃ list β
   by refine ⟨list.map f, list.map g, λ x, _, λ x, _⟩;
      simp [id_of_left_inverse l, id_of_right_inverse r]
 
+def fin_equiv_subtype (n : ℕ) : fin n ≃ {m // m < n} :=
+⟨λ x, ⟨x.1, x.2⟩, λ x, ⟨x.1, x.2⟩, λ ⟨a, b⟩, rfl,λ ⟨a, b⟩, rfl⟩
+
+def vector_equiv_fin (α : Type*) (n : ℕ) : vector α n ≃ (fin n → α) :=
+⟨vector.nth, vector.of_fn, vector.of_fn_nth, λ f, funext $ vector.nth_of_fn f⟩
+
+def d_array_equiv_fin (n : ℕ) (α : fin n → Type*) : d_array n α ≃ (Π i, α i) :=
+⟨d_array.read, d_array.mk, λ ⟨f⟩, rfl, λ f, rfl⟩
+
+def array_equiv_fin (n : ℕ) (α : Type*) : array n α ≃ (fin n → α) :=
+d_array_equiv_fin _ _
+
+def vector_equiv_array (α : Type*) (n : ℕ) : vector α n ≃ array n α :=
+(vector_equiv_fin _ _).trans (array_equiv_fin _ _).symm
+
 def decidable_eq_of_equiv [h : decidable_eq α] : α ≃ β → decidable_eq β
 | ⟨f, g, l, r⟩ b₁ b₂ :=
   match h (g b₁) (g b₂) with

data/equiv.lean

@@ -51,3 +51,18 @@ i.succ_rec H0 Hs
   {C : ∀ n, fin n → Sort*} {H0 Hs} {n} (i : fin n) :
   @fin.succ_rec_on (succ n) i.succ C H0 Hs = Hs n i (fin.succ_rec_on i H0 Hs) :=
 by cases i; refl
+
+@[elab_as_eliminator] def fin.cases {n} {C : fin (succ n) → Sort*}
+  (H0 : C 0) (Hs : ∀ i : fin n, C (i.succ)) :
+  ∀ (i : fin (succ n)), C i
+| ⟨0, h⟩ := H0
+| ⟨succ i, h⟩ := Hs ⟨i, lt_of_succ_lt_succ h⟩
+
+@[simp] theorem fin.cases_zero
+  {n} {C : fin (succ n) → Sort*} {H0 Hs} :
+  @fin.cases n C H0 Hs 0 = H0 := rfl
+
+@[simp] theorem fin.cases_succ
+  {n} {C : fin (succ n) → Sort*} {H0 Hs} (i : fin n) :
+  @fin.cases n C H0 Hs i.succ = Hs i :=
+by cases i; refl

data/fin.lean

@@ -8,7 +8,7 @@ Basic properties of lists.
 import tactic.interactive tactic.mk_iff_of_inductive_prop tactic.split_ifs
   logic.basic logic.function
   algebra.group
-  data.nat.basic data.option data.bool data.prod data.sigma
+  data.nat.basic data.option data.bool data.prod data.sigma data.fin
 open function nat
 
 namespace list
@@ -411,16 +411,23 @@ by subst l₁
 
 /- head and tail -/
 
-@[simp] theorem head_cons [h : inhabited α] (a : α) (l : list α) : head (a::l) = a := rfl
+@[simp] def head' : list α → option α
+| []       := none
+| (a :: l) := some a
+
+theorem head_eq_head' [inhabited α] (l : list α) : head l = (head' l).iget :=
+by cases l; refl
+
+@[simp] theorem head_cons [inhabited α] (a : α) (l : list α) : head (a::l) = a := rfl
 
 @[simp] theorem tail_nil : tail (@nil α) = [] := rfl
 
 @[simp] theorem tail_cons (a : α) (l : list α) : tail (a::l) = l := rfl
 
-@[simp] theorem head_append [h : inhabited α] (t : list α) {s : list α} (h : s ≠ []) : head (s ++ t) = head s :=
+@[simp] theorem head_append [inhabited α] (t : list α) {s : list α} (h : s ≠ []) : head (s ++ t) = head s :=
 by {induction s, contradiction, simp}
 
-theorem cons_head_tail [h : inhabited α] {l : list α} (h : l ≠ []) : (head l)::(tail l) = l :=
+theorem cons_head_tail [inhabited α] {l : list α} (h : l ≠ []) : (head l)::(tail l) = l :=
 by {induction l, contradiction, simp}
 
 /- map -/
@@ -2289,6 +2296,69 @@ theorem length_sigma (l₁ : list α) (l₂ : Π a, list (σ a)) :
 by induction l₁ with x l₁ IH; simp *
 end
 
+/- of_fn -/
+def of_fn_aux {n} (f : fin n → α) : ∀ m, m ≤ n → list α → list α
+| 0        h l := l
+| (succ m) h l := of_fn_aux m (le_of_lt h) (f ⟨m, h⟩ :: l)
+
+def of_fn {n} (f : fin n → α) : list α :=
+of_fn_aux f n (le_refl _) []
+
+theorem length_of_fn_aux {n} (f : fin n → α) :
+  ∀ m h l, length (of_fn_aux f m h l) = length l + m
+| 0        h l := rfl
+| (succ m) h l := (length_of_fn_aux m _ _).trans (succ_add _ _)
+
+theorem length_of_fn {n} (f : fin n → α) : length (of_fn f) = n :=
+(length_of_fn_aux f _ _ _).trans (zero_add _)
+
+def of_fn_nth_val {n} (f : fin n → α) (i : ℕ) : option α :=
+if h : _ then some (f ⟨i, h⟩) else none
+
+theorem nth_of_fn_aux {n} (f : fin n → α) (i) :
+  ∀ m h l,
+    (∀ i, nth l i = of_fn_nth_val f (i + m)) →
+     nth (of_fn_aux f m h l) i = of_fn_nth_val f i
+| 0        h l H := H i
+| (succ m) h l H := nth_of_fn_aux m _ _ begin
+  intro j, cases j with j,
+  { simp [of_fn_nth_val, show m < n, from h], refl },
+  { simp [H, succ_add, -add_comm] }
+end
+
+@[simp] theorem nth_of_fn {n} (f : fin n → α) (i) :
+  nth (of_fn f) i = of_fn_nth_val f i :=
+nth_of_fn_aux f _ _ _ _ $ λ i,
+by simp [of_fn_nth_val, not_lt.2 (le_add_right n i)]
+
+theorem nth_le_of_fn {n} (f : fin n → α) (i : fin n) :
+  nth_le (of_fn f) i.1 ((length_of_fn f).symm ▸ i.2) = f i :=
+option.some.inj $ by rw [← nth_le_nth];
+  simp [of_fn_nth_val, i.2]; cases i; refl
+
+theorem array_eq_of_fn {n} (a : array n α) : a.to_list = of_fn a.read :=
+suffices ∀ {m h l}, d_array.rev_iterate_aux a
+  (λ i, cons) m h l = of_fn_aux (d_array.read a) m h l, from this,
+begin
+  intros, induction m with m IH generalizing l, {refl},
+  simp [d_array.rev_iterate_aux, of_fn_aux, IH]
+end
+
+theorem of_fn_zero (f : fin 0 → α) : of_fn f = [] := rfl
+
+theorem of_fn_succ {n} (f : fin (succ n) → α) :
+  of_fn f = f 0 :: of_fn (λ i, f i.succ) :=
+suffices ∀ {m h l}, of_fn_aux f (succ m) (succ_le_succ h) l =
+  f 0 :: of_fn_aux (λ i, f i.succ) m h l, from this,
+begin
+  intros, induction m with m IH generalizing l, {refl},
+  rw [of_fn_aux, IH], refl
+end
+
+theorem of_fn_nth_le : ∀ l : list α, of_fn (λ i, nth_le l i.1 i.2) = l
+| [] := rfl
+| (a::l) := by rw of_fn_succ; congr; simp; exact of_fn_nth_le l
+
 /- disjoint -/
 section disjoint
 

data/list/basic.lean

@@ -150,6 +150,10 @@ theorem sqrt_eq_zero {n : ℕ} : sqrt n = 0 ↔ n = 0 :=
   by rw [h]; exact dec_trivial,
  λ e, e.symm ▸ rfl⟩
 
+theorem eq_sqrt {n q} : q = sqrt n ↔ q*q ≤ n ∧ n < (q+1)*(q+1) :=
+⟨λ e, e.symm ▸ sqrt_is_sqrt n,
+ λ ⟨h₁, h₂⟩, le_antisymm (le_sqrt.2 h₁) (le_of_lt_succ $ sqrt_lt.2 h₂)⟩
+
 theorem le_three_of_sqrt_eq_one {n : ℕ} (h : sqrt n = 1) : n ≤ 3 :=
 le_of_lt_succ $ (@sqrt_lt n 2).1 $
 by rw [h]; exact dec_trivial
@@ -170,4 +174,10 @@ le_antisymm
 theorem sqrt_eq (n : ℕ) : sqrt (n*n) = n :=
 sqrt_add_eq n (zero_le _)
 
+theorem sqrt_succ_le_succ_sqrt (n : ℕ) : sqrt n.succ ≤ n.sqrt.succ :=
+le_of_lt_succ $ sqrt_lt.2 $ lt_succ_of_le $ succ_le_succ $
+le_trans (sqrt_le_add n) $ add_le_add_right
+  (by refine add_le_add
+    (mul_le_mul_right _ _) _; exact le_add_right _ 2) _
+
 end nat

data/nat/sqrt.lean

@@ -687,8 +687,7 @@ theorem image_union (f : α → β) (s t : set α) :
   f '' (s ∪ t) = f '' s ∪ f '' t :=
 by finish [set_eq_def, iff_def, mem_image_eq]
 
-@[simp] theorem image_empty (f : α → β) : f '' ∅ = ∅ :=
-by finish [set_eq_def, mem_image_eq]
+@[simp] theorem image_empty (f : α → β) : f '' ∅ = ∅ := ext $ by simp
 
 theorem image_inter_on {f : α → β} {s t : set α} (h : ∀x∈t, ∀y∈s, f x = f y → x = y) :
   f '' s ∩ f '' t = f '' (s ∩ t) :=
@@ -718,8 +717,7 @@ begin
   intro x, split; { intro e, subst e, simp }
 end
 
-theorem image_id (s : set α) : id '' s = s :=
-by finish [set_eq_def, iff_def, mem_image_eq]
+@[simp] theorem image_id (s : set α) : id '' s = s := ext $ by simp
 
 theorem compl_compl_image (S : set (set α)) :
   compl '' (compl '' S) = S :=

data/set/basic.lean

@@ -72,6 +72,15 @@ end psigma
 section subtype
 variables {α : Sort*} {β : α → Prop}
 
+protected lemma subtype.eq' : ∀ {a1 a2 : {x // β x}}, a1.val = a2.val → a1 = a2
+| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl
+
+lemma subtype.ext {a1 a2 : {x // β x}} : a1 = a2 ↔ a1.val = a2.val :=
+⟨congr_arg _, subtype.eq'⟩
+
+theorem subtype.val_injective : function.injective (@subtype.val _ β) :=
+λ a b, subtype.eq'
+
 @[simp] theorem subtype.coe_eta {α : Type*} {β : α → Prop}
  (a : {a // β a}) (h : β a) : subtype.mk ↑a h = a := subtype.eta _ _
 

data/sigma/basic.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2018 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+
+Additional theorems about the `vector` type.
+-/
+import data.vector data.list.basic data.sigma
+
+namespace vector
+variables {α : Type*} {n : ℕ}
+
+attribute [simp] head_cons tail_cons
+
+instance [inhabited α] : inhabited (vector α n) :=
+⟨of_fn (λ _, default α)⟩
+
+theorem to_list_injective : function.injective (@to_list α n) :=
+subtype.val_injective
+
+@[simp] theorem to_list_of_fn : ∀ {n} (f : fin n → α), to_list (of_fn f) = list.of_fn f
+| 0     f := rfl
+| (n+1) f := by rw [of_fn, list.of_fn_succ, to_list_cons, to_list_of_fn]
+
+theorem mk_to_list :
+  ∀ (v : vector α n) h, (⟨to_list v, h⟩ : vector α n) = v
+| ⟨l, h₁⟩ h₂ := rfl
+
+theorem nth_eq_nth_le : ∀ (v : vector α n) (i),
+  nth v i = v.to_list.nth_le i.1 (by rw to_list_length; exact i.2)
+| ⟨l, h⟩ i := rfl
+
+@[simp] theorem nth_of_fn {n} (f : fin n → α) (i) : nth (of_fn f) i = f i :=
+by rw [nth_eq_nth_le, ← list.nth_le_of_fn f];
+   congr; apply to_list_of_fn
+
+@[simp] theorem of_fn_nth (v : vector α n) : of_fn (nth v) = v :=
+begin
+  rcases v with ⟨l, rfl⟩,
+  apply to_list_injective,
+  change nth ⟨l, eq.refl _⟩ with λ i, nth ⟨l, rfl⟩ i,
+  simp [nth, list.of_fn_nth_le]
+end
+
+@[simp] theorem nth_tail : ∀ (v : vector α n.succ) (i : fin n),
+  nth (tail v) i = nth v i.succ
+| ⟨a::l, e⟩ ⟨i, h⟩ := by simp [nth_eq_nth_le]; refl
+
+@[simp] theorem tail_of_fn {n : ℕ} (f : fin n.succ → α) :
+  tail (of_fn f) = of_fn (λ i, f i.succ) :=
+(of_fn_nth _).symm.trans $ by congr; funext i; simp
+
+theorem head'_to_list : ∀ (v : vector α n.succ),
+  (to_list v).head' = some (head v)
+| ⟨a::l, e⟩ := rfl
+
+@[simp] theorem nth_zero : ∀ (v : vector α n.succ), nth v 0 = head v
+| ⟨a::l, e⟩ := rfl
+
+@[simp] theorem head_of_fn
+  {n : ℕ} (f : fin n.succ → α) : head (of_fn f) = f 0 :=
+by rw [← nth_zero, nth_of_fn]
+
+@[simp] theorem nth_cons_zero
+  (a : α) (v : vector α n) : nth (a :: v) 0 = a :=
+by simp [nth_zero]
+
+@[simp] theorem nth_cons_succ
+  (a : α) (v : vector α n) (i : fin n) : nth (a :: v) i.succ = nth v i :=
+by rw [← nth_tail, tail_cons]
+
+end vector

data/vector2.lean

@@ -65,7 +65,7 @@ protected def of_not_nonempty {α : Sort u} {β : Sort v} (hα : ¬ nonempty α)
 ⟨λa, (hα ⟨a⟩).elim, assume a, (hα ⟨a⟩).elim⟩
 
 def subtype {α} (p : α → Prop) : subtype p ↪ α :=
-⟨subtype.val, λ a b, subtype.eq⟩
+⟨subtype.val, λ _ _, subtype.eq'⟩
 
 /-- Restrict the codomain of an embedding. -/
 def cod_restrict {α β} (p : set β) (f : α ↪ β) (H : ∀ a, f a ∈ p) : α ↪ p :=