feat(pfun/recursion): unbounded recursion

src/data/nat/up.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2020 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Simon Hudon
+-/
+import data.nat.basic
+
+/-!
+# `nat.up`
+
+`nat.up p`, with `p` a predicate on `ℕ`, is a subtype of `ℕ` that contains value
+`n` if no value below `n` (excluding `n`) satisfies `p`.
+
+This allows us to prove `>` is well-founded when `∃ i, p i`. This helps implement
+searches on `ℕ`, starting at `0` and with an unknown upper-bound.
+
+-/
+
+namespace nat
+
+@[reducible]
+def up (p : ℕ → Prop) : Type := { i : ℕ // (∀ j < i, ¬ p j) }
+
+namespace up
+
+variable {p : ℕ → Prop}
+
+protected def lt (p) : up p → up p → Prop := λ x y, x.1 > y.1
+
+instance : has_lt (up p) :=
+{ lt := λ x y, x.1 > y.1 }
+
+protected def wf : Exists p → well_founded (up.lt p)
+| ⟨x,h⟩ :=
+have h : (<) = measure (λ y : nat.up p, x - y.val),
+  by { ext, dsimp [measure,inv_image],
+       rw nat.sub_lt_sub_left_iff, refl,
+       by_contradiction h', revert h,
+       apply x_1.property _ (lt_of_not_ge h'), },
+cast (congr_arg _ h.symm) (measure_wf _)
+
+def zero : nat.up p := ⟨ 0, λ j h, false.elim (nat.not_lt_zero _ h) ⟩
+
+def succ (x : nat.up p) (h : ¬ p x.val) : nat.up p :=
+⟨x.val.succ, by { intros j h', rw nat.lt_succ_iff_lt_or_eq at h',
+                  cases h', apply x.property _ h', subst j, apply h } ⟩
+
+section find
+
+variables [decidable_pred p] (h : Exists p)
+
+def find_aux : nat.up p → nat.up p :=
+well_founded.fix (up.wf h) $ λ x f,
+if h : p x.val then x
+  else f (x.succ h) $ nat.lt_succ_self _
+
+def find : ℕ := (find_aux h up.zero).val
+
+lemma p_find : p (find h) :=
+let P := (λ x : nat.up p, p (find_aux h x).val) in
+suffices ∀ x, P x, from this _,
+assume x,
+well_founded.induction (nat.up.wf h) _ $ λ y ih,
+by { dsimp [P], rw [find_aux,well_founded.fix_eq],
+     by_cases h' : (p y); simp *,
+     apply ih, apply nat.lt_succ_self, }
+
+lemma find_least_solution (i : ℕ) (h' : i < find h) : ¬ p i :=
+subtype.property (find_aux h nat.up.zero) _ h'
+
+end find
+
+end up
+end nat

src/data/pfun.lean

@@ -44,6 +44,7 @@ theorem dom_iff_mem : ∀ {o : roption α}, o.dom ↔ ∃y, y ∈ o
 theorem get_mem {o : roption α} (h) : get o h ∈ o := ⟨_, rfl⟩
 
 /-- `roption` extensionality -/
+@[ext]
 theorem ext {o p : roption α} (H : ∀ a, a ∈ o ↔ a ∈ p) : o = p :=
 ext' ⟨λ h, ((H _).1 ⟨h, rfl⟩).fst,
      λ h, ((H _).2 ⟨h, rfl⟩).fst⟩ $
@@ -94,6 +95,16 @@ begin
   { rintro ⟨x, rfl⟩, apply some_ne_none }
 end
 
+lemma eq_none_or_eq_some (o : roption α) : o = none ∨ ∃ x, o = some x :=
+begin
+  classical,
+  by_cases h : o.dom,
+  { rw dom_iff_mem at h, right,
+    apply exists_imp_exists _ h,
+    simp [eq_some_iff] },
+  { rw eq_none_iff', exact or.inl h },
+end
+
 @[simp] lemma some_inj {a b : α} : roption.some a = some b ↔ a = b :=
 function.injective.eq_iff (λ a b h, congr_fun (eq_of_heq (roption.mk.inj h).2) trivial)
 
@@ -172,6 +183,26 @@ by haveI := classical.dec; exact
 ⟨λ o, to_option o, of_option, λ o, of_to_option o,
  λ o, eq.trans (by dsimp; congr) (to_of_option o)⟩
 
+instance : order_bot (roption α) :=
+{ le := λ x y, ∀ i, i ∈ x → i ∈ y,
+  le_refl := λ x y, id,
+  le_trans := λ x y z f g i, g _ ∘ f _,
+  le_antisymm := λ x y f g, roption.ext $ λ z, ⟨f _, g _⟩,
+  bot := none,
+  bot_le := by { introv x, rintro ⟨⟨_⟩,_⟩, } }
+
+lemma le_total_of_le_of_le {x y : roption α} (z : roption α) (hx : x ≤ z) (hy : y ≤ z) :
+  x ≤ y ∨ y ≤ x :=
+begin
+  rcases roption.eq_none_or_eq_some x with h | ⟨b, h₀⟩,
+  { rw h, left, apply order_bot.bot_le _ },
+  right, intros b' h₁,
+  rw roption.eq_some_iff at h₀,
+  replace hx := hx _ h₀, replace hy := hy _ h₁,
+  replace hx := roption.mem_unique hx hy, subst hx,
+  exact h₀
+end
+
 /-- `assert p f` is a bind-like operation which appends an additional condition
   `p` to the domain and uses `f` to produce the value. -/
 def assert (p : Prop) (f : p → roption α) : roption α :=
@@ -210,6 +241,23 @@ theorem mem_assert {p : Prop} {f : p → roption α}
 ⟨match a with _, ⟨h, rfl⟩ := ⟨_, ⟨_, rfl⟩⟩ end,
  λ ⟨a, h⟩, mem_assert _ h⟩
 
+lemma assert_pos {p : Prop} {f : p → roption α} (h : p) :
+  assert p f = f h :=
+begin
+  dsimp [assert],
+  cases h' : f h, simp [h',h],
+  apply function.hfunext,
+  { simp only [h,h',exists_prop_of_true] },
+  { cc }
+end
+
+lemma assert_neg {p : Prop} {f : p → roption α} (h : ¬ p) :
+  assert p f = none :=
+begin
+  dsimp [assert,none], congr, simp [h],
+  apply function.hfunext, simp [h], cc,
+end
+
 theorem mem_bind {f : roption α} {g : α → roption β} :
   ∀ {a b}, a ∈ f → b ∈ g a → b ∈ f.bind g
 | _ _ ⟨h, rfl⟩ ⟨h₂, rfl⟩ := ⟨⟨h, h₂⟩, rfl⟩
@@ -273,6 +321,15 @@ by rw [bind_some_eq_map]; simp [map_id']
 @[simp] theorem bind_eq_bind {α β} (f : roption α) (g : α → roption β) :
   f >>= g = f.bind g := rfl
 
+lemma bind_le {α} (x : roption α) (f : α → roption β) (y : roption β) :
+  x >>= f ≤ y ↔ (∀ a, a ∈ x → f a ≤ y) :=
+begin
+  split; intro h,
+  { intros a h' b, replace h := h b, simp at h, apply h _ h' },
+  { intros b h', simp at h', rcases h' with ⟨a,h₀,h₁⟩,
+    apply h _ h₀ _ h₁ },
+end
+
 instance : monad_fail roption :=
 { fail := λ_ _, none, ..roption.monad }