remove unused declarations

src/data/pfun/fix.lean

@@ -19,7 +19,7 @@ open roption nat nat.up
 
 variables {β : α → Type*} (f : (Π a, roption $ β a) → (Π a, roption $ β a))
 
-def succ' (i : α → ℕ) (x : α) : ℕ := (i x).succ
+-- def succ' (i : α → ℕ) (x : α) : ℕ := (i x).succ
 
 def approx : stream $ Π a, roption $ β a
 | 0 := ⊥
@@ -123,21 +123,21 @@ begin
     cases hh _ _ h' }
 end
 
-lemma approx_eq {i j : ℕ} {a : α} (hi : (approx f i a).dom) (hj : (approx f j a).dom) :
-  approx f i a = approx f j a :=
-begin
-  simp [dom_iff_mem] at hi hj,
-  cases hi with b hi, cases hj with b' hj,
-  have : b' = b,
-  { wlog hij : i ≤ j := le_total i j using [i j b b',j i b' b],
-    apply mem_unique hj, apply approx_mono hf hij _ _ hi, },
-  subst b',
-  ext y, split; intro hy,
-  rename hi hh, rename hj hi, rename hh hj,
-  all_goals
-  { have := mem_unique hy hj, subst this,
-    exact hi }
-end
+-- lemma approx_eq {i j : ℕ} {a : α} (hi : (approx f i a).dom) (hj : (approx f j a).dom) :
+--   approx f i a = approx f j a :=
+-- begin
+--   simp [dom_iff_mem] at hi hj,
+--   cases hi with b hi, cases hj with b' hj,
+--   have : b' = b,
+--   { wlog hij : i ≤ j := le_total i j using [i j b b',j i b' b],
+--     apply mem_unique hj, apply approx_mono hf hij _ _ hi, },
+--   subst b',
+--   ext y, split; intro hy,
+--   rename hi hh, rename hj hi, rename hh hj,
+--   all_goals
+--   { have := mem_unique hy hj, subst this,
+--     exact hi }
+-- end
 
 noncomputable def approx_chain : chain (Π a, roption $ β a) :=
 begin
@@ -192,6 +192,7 @@ begin
     intros y x, revert y, simp, apply max_fix hf },
 end
 
+@[main_declaration]
 lemma fix_le {X : Π a, roption $ β a} (hX : f X ≤ X) : fix f ≤ X :=
 begin
   rw fix_eq_Sup hf,
@@ -244,6 +245,7 @@ show to_unit f x ≤ to_unit f y,
 def to_unit_cont (f : roption α → roption α) : Π hc : continuous' f, continuous (to_unit f) (to_unit_mono f hc.fst)
 | ⟨hm,hc⟩ := by { intro c, ext : 1, dsimp [to_unit,complete_partial_order.Sup], erw [hc _,chain.map_comp], refl }
 
+@[main_declaration]
 noncomputable instance : lawful_fix (roption α) :=
 ⟨ λ f hc, by { dsimp [fix],
               conv { to_lhs, rw [pi.fix_eq (to_unit_cont f hc)] }, refl } ⟩

src/order/complete_partial_order.lean

@@ -6,6 +6,7 @@ Helpful for a small-scale domain theory, see
 import data.pfun
 import data.stream.basic
 import tactic.wlog
+import tactic.find_unused
 
 universes u v
 
@@ -64,28 +65,18 @@ instance : has_mem α (chain α) :=
 
 @[simp] lemma mem_mk (x : α) (s : stream α) (h) : x ∈ chain.mk s h ↔ x ∈ s := iff.refl _
 
-def nth (i : ℕ) (c : chain α) : α := c.elems.nth i
-
-@[simp] lemma nth_mk (i : ℕ) (s : stream α) (h) : (chain.mk s h).nth i = s.nth i := rfl
-
 variables (c c' : chain α)
-  (f : α → β) (hf : monotone f)
-  {g : β → γ} (hg : monotone g)
+variables (f : α → β) (hf : monotone f)
+variables {g : β → γ} (hg : monotone g)
 
 instance : has_le (chain α) :=
 { le := λ x y, ∀ a, a ∈ x → ∃ b ∈ y, a ≤ b  }
 
-@[ext]
-lemma ext (h : ∀ i, c.nth i = c'.nth i) : c = c' :=
-by cases c; cases c'; congr; ext; apply h
-
 def map : chain β :=
 ⟨c.elems.map f, stream.monotone_map hf c.mono ⟩
 
 variables {f}
 
-@[simp] lemma elems_map (c : chain α) : (c.map f hf).elems = c.elems.map f := rfl
-
 lemma mem_map (x : α) : x ∈ c → f x ∈ chain.map c f hf :=
 stream.mem_map _
 
@@ -95,29 +86,6 @@ stream.exists_of_mem_map
 lemma mem_map_iff {b : β} : b ∈ c.map f hf ↔ ∃ a, a ∈ c ∧ f a = b :=
 ⟨ exists_of_mem_map _ _, λ h, by { rcases h with ⟨w,h,h'⟩, subst b, apply mem_map c hf _ h, } ⟩
 
-lemma chain_map_le (c' : chain β) (h : ∀ a, a ∈ c → f a ∈ c') : chain.map c f hf ≤ c' :=
-begin
-  intros b hb,
-  rcases exists_of_mem_map _ hf hb with ⟨a,h₀,h₁⟩,
-  subst b, existsi [f a,h _ h₀], refl
-end
-
-lemma le_chain_map (c' : chain β) (h : ∀ b, b ∈ c' → ∃ a, b ≤ f a ∧ a ∈ c) : c' ≤ chain.map c f hf :=
-begin
-  intros b hb,
-  replace h := h _ hb, rcases h with ⟨a,h₀,h₁⟩,
-  exact ⟨f a,mem_map _ hf _ h₁,h₀⟩
-end
-
-lemma map_le_map {g : α → β} (hg : monotone g) (h : ∀ a ∈ c, f a ≤ g a) : c.map f hf ≤ c.map g hg :=
-begin
-  intros a ha,
-  replace ha := exists_of_mem_map _ _ ha,
-  rcases ha with ⟨a',ha₀,ha₁⟩,
-  existsi [g a', mem_map _ hg _ ha₀],
-  rw ← ha₁, apply h _ ha₀,
-end
-
 lemma map_id : c.map id (monotone_id) = c :=
 by cases c; refl
 
@@ -150,9 +118,11 @@ variables [complete_partial_order α]
 
 export order_bot (bot_le)
 
+@[main_declaration]
 lemma le_Sup_of_le {c : chain α} {x y : α} (h : x ≤ y) (hy : y ∈ c) : x ≤ Sup c :=
 le_trans h (le_Sup c y hy)
 
+@[main_declaration]
 lemma Sup_total {c : chain α} {x : α} (h : ∀y∈c, y ≤ x ∨ x ≤ y) : Sup c ≤ x ∨ x ≤ Sup c :=
 classical.by_cases
   (assume : ∀y ∈ c, y ≤ x, or.inl (Sup_le _ _ this))
@@ -163,11 +133,13 @@ classical.by_cases
     have x ≤ y, from (h y hy).resolve_left hyx,
     or.inr $ le_Sup_of_le this hy)
 
+@[main_declaration]
 lemma Sup_le_Sup_of_le {c₀ c₁ : chain α} (h : c₀ ≤ c₁) : Sup c₀ ≤ Sup c₁ :=
 Sup_le _ _ $
 λ y hy, Exists.rec_on (h y hy) $
 λ x ⟨hx,hxy⟩, le_trans hxy $ le_Sup _ _ hx
 
+@[main_declaration]
 lemma Sup_le_iff (c : chain α) (x : α) : Sup c ≤ x ↔ (∀ y ∈ c, y ≤ x) :=
 begin
   split; intros,
@@ -223,6 +195,7 @@ have a' : some (classical.some this) ∈ c, from classical.some_spec this,
 calc roption.Sup c = some (classical.some this) : dif_pos this
                ... = some a : congr_arg _ (eq_of_chain a' h)
 
+@[main_declaration]
 lemma Sup_eq_none {c : chain (roption α)} (h : ¬∃a, some a ∈ c) : roption.Sup c = none :=
 dif_neg h
 
@@ -271,9 +244,9 @@ variables [∀a, partial_order (β a)]
 lemma monotone_apply (a : α) : monotone (λf:Πa, β a, f a) :=
 assume f g hfg, hfg a
 
-lemma monotone_lambda {γ : Type*} [partial_order γ] {m : γ → Πa, β a}
-  (hm : ∀a, monotone (λc, m c a)) : monotone m :=
-assume f g h a, hm a h
+-- lemma monotone_lambda {γ : Type*} [partial_order γ] {m : γ → Πa, β a}
+--   (hm : ∀a, monotone (λc, m c a)) : monotone m :=
+-- assume f g h a, hm a h
 
 end monotone
 
@@ -323,6 +296,7 @@ instance : partial_order (set α) :=
   le_trans    := assume a b c hab hbc x hx, hbc $ hab $ hx,
   le_antisymm := assume a b hab hba, ext $ assume x, ⟨@hab x, @hba x⟩ }
 
+@[main_declaration]
 instance : complete_partial_order (set α) :=
 { Sup    := λc, ⋃ i, c.elems i,
   Sup_le := assume ⟨c, _⟩ s hs x, by simp [stream.mem_def] at ⊢ hs; intros i hx; apply hs _ i rfl hx,

test/general_recursion.lean

@@ -1,6 +1,7 @@
 import tactic.norm_num
 import tactic.linarith
 import tactic.omega
+import tactic.find_unused
 import data.pfun.fix
 import data.nat.basic
 
@@ -25,6 +26,7 @@ pi.continuous_ext easy.intl
        (λ (x_1 : ℕ), id (cont_const' (pure x))))
 
 -- automation coming soon
+@[main_declaration]
 theorem easy.equations.eqn_1 (x y : ℕ) : easy x y = pure x :=
 by rw [easy, lawful_fix.fix_eq easy.cont]; refl
 
@@ -56,6 +58,7 @@ pi.continuous_ext div.intl
                (cont_const' (pure x)))))
 
 -- automation coming soon
+@[main_declaration]
 theorem div.equations.eqn_1 (x y : ℕ) : div x y = if y ≤ x ∧ y > 0 then div (x - y) y else pure x :=
 by conv_lhs { rw [div, lawful_fix.fix_eq div.cont] }; refl
 
@@ -103,10 +106,12 @@ theorem tree_map.cont : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), con
                             (λ (x_1 : tree β), cont_const' (pure (node (f x_x) x x_1)))))))))
 
 -- automation coming soon
+@[main_declaration]
 theorem tree_map.equations.eqn_1 {α : Type u_1} {β : Type u_2} (f : α → β) : tree_map f nil = pure nil :=
 by rw [tree_map,lawful_fix.fix_eq (tree_map.cont f)]; refl
 
 -- automation coming soon
+@[main_declaration]
 theorem tree_map.equations.eqn_2 {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) (t₀ t₁ : tree α) :
   tree_map f (node x t₀ t₁) = tree_map f t₀ >>= λ (tt₀ : tree β), tree_map f t₁ >>= λ (tt₁ : tree β), pure (node (f x) tt₀ tt₁) :=
 by conv_lhs { rw [tree_map,lawful_fix.fix_eq (tree_map.cont f)] }; refl
@@ -137,11 +142,13 @@ theorem tree_map'.cont : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), co
                  (pi.continuous_congr (λ (v : tree α) (x : tree α → roption (tree β)), x v) x_a_1 cont_id'))))
 
 -- automation coming soon
+@[main_declaration]
 theorem tree_map'.equations.eqn_1 {α : Type u_1} {β : Type u_2} (f : α → β) :
   tree_map' f nil = pure nil :=
 by rw [tree_map',lawful_fix.fix_eq (tree_map'.cont f)]; refl
 
 -- automation coming soon
+@[main_declaration]
 theorem tree_map'.equations.eqn_2 {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) (t₀ t₁ : tree α) :
   tree_map' f (node x t₀ t₁) = node (f x) <$> tree_map' f t₀ <*> tree_map' f t₁ :=
 by conv_lhs { rw [tree_map',lawful_fix.fix_eq (tree_map'.cont f)] }; refl
@@ -172,6 +179,7 @@ pi.continuous_ext f91.intl
                 (λ (x_1 : ℕ), pi.continuous_congr (λ (v : ℕ) (g : ℕ → roption ℕ), g v) x_1 cont_id')))))
 .
 -- automation coming soon
+@[main_declaration]
 theorem f91.equations.eqn_1 (n : ℕ) : f91 n = ite (n > 100) (pure (n - 10)) (f91 (n + 11) >>= f91) :=
 by conv_lhs { rw [f91, lawful_fix.fix_eq f91.cont] }; refl
 
@@ -200,6 +208,7 @@ def f91' (n : ℕ) : ℕ := (f91 n).get (f91_dom n)
 #eval f91' 109
 -- 99
 
+@[main_declaration]
 lemma f91_spec' (n : ℕ) : f91' n = if n > 100 then n - 10 else 91 :=
 begin
   suffices : (∃ n', n' ∈ f91 n ∧ n' = if n > 100 then n - 10 else 91),