experiments

src/data/list/bag_inter.lean

@@ -0,0 +1,53 @@
+import data.list.basic
+import tactic.chain
+import tactic.auto_cases
+import tactic.tidy
+import tactic.squeeze
+
+open list
+open nat
+
+variables {α : Type*} [decidable_eq α]
+
+local attribute [simp] min_succ_succ count_cons erase_cons count_erase
+
+lemma foo {a : α} {L : list α} (h : a ∈ L) (n : ℕ) : succ (min n (pred (count a L))) = min (succ n) (count a L) :=
+begin
+  rw ←nat.min_succ_succ,
+  rw nat.succ_pred_eq_of_pos,
+  exact count_pos.2 h
+end
+
+open tactic
+
+@[simp] theorem count_bag_inter' {a : α} :
+  ∀ {l₁ l₂ : list α}, count a (l₁.bag_inter l₂) = min (count a l₁) (count a l₂)
+| []         l₂ := by simp
+| l₁         [] := by simp
+| (h₁ :: l₁) (h₂ :: l₂) :=
+begin
+  simp only [list.bag_inter],
+  dsimp at *,
+  tactic.tidy.simp_non_aux,
+  split_ifs,
+  tactic.tidy.simp_non_aux,
+  split_ifs,
+  refl,
+  simp,
+  split_ifs,
+  { tidy? },
+  { tidy? },
+  -- tidy?,
+
+  rw foo h,
+
+  rw decidable.not_or_iff_and_not at h,
+  have w : a ∉ l₂ := h.right,
+  rw count_eq_zero_of_not_mem w,
+  simp,
+  -- sorry,
+  -- sorry,
+end
+-- using_well_founded
+-- { rel_tac := λ _ _, tactic.apply_instance,
+--   dec_tac := tactic.target >>= tactic.trace >> tactic.assumption, }

src/data/list/basic.lean

@@ -733,7 +733,7 @@ begin
   induction l with b l ih,
   { exact iff_of_true rfl (not_mem_nil _) },
   simp only [length, mem_cons_iff, index_of_cons], split_ifs,
-  { exact iff_of_false (by rintro ⟨⟩) (λ H, H $ or.inl h) },
+  { exact iff_of_false (by rintro ⟨⟩) (λ H, H $ or.inl rfl) },
   { simp only [h, false_or], rw ← ih, exact succ_inj' }
 end
 
@@ -2734,6 +2734,18 @@ theorem map_foldl_erase [decidable_eq β] {f : α → β} (finj : injective f) {
 by induction l₂ generalizing l₁; [refl,
 simp only [foldl_cons, map_erase finj, *]]
 
+lemma count_erase {a b : α} : ∀ (s : list α), count a (s.erase b) = if a = b then pred (count a s) else count a s
+| [] := by simp
+| (x :: xs) :=
+begin
+  rw erase_cons,
+  -- split_ifs with h₁ h₂,
+  -- replace h₁ := h₁.symm,
+  -- subst h₁, -- subst could try harder ...
+  -- rw h₂,
+  -- simp,
+end
+
 @[simp] theorem count_erase_self (a : α) : ∀ (s : list α), count a (list.erase s a) = pred (count a s)
 | [] := by simp
 | (h :: t) :=

src/tactic/auto_cases.lean

@@ -12,6 +12,8 @@ meta def auto_cases_at (h : expr) : tactic string :=
 do t' ← infer_type h,
   t' ← whnf t',
   let use_cases := match t' with
+  | `(false)     := tt
+  | `(true)      := tt
   | `(empty)     := tt
   | `(pempty)    := tt
   | `(unit)      := tt
@@ -35,7 +37,8 @@ do t' ← infer_type h,
     match t' with
     -- `cases` can be dangerous on `eq` and `quot`, producing mysterious errors during type checking.
     -- instead we attempt `induction`
-    | `(eq _ _)        := do induction h, pp ← pp h, return ("induction " ++ pp.to_string)
+    | `(eq _ _)        := (do subst h,     pp ← pp h, return ("induction " ++ pp.to_string)) <|>
+                          (do induction h, pp ← pp h, return ("induction " ++ pp.to_string))
     | `(quot _)        := do induction h, pp ← pp h, return ("induction " ++ pp.to_string)
     | _                := failed
     end

src/tactic/split_ifs.lean

@@ -36,7 +36,7 @@ hs ← at_.get_locals, hs.mmap' (λ h, simp_hyp sls [] h cfg discharger >> skip)
 when at_.include_goal (simp_target sls [] cfg discharger)
 
 meta def split_if1 (c : expr) (n : name) (at_ : loc) : tactic unit :=
-by_cases c n; reduce_ifs_at at_
+by_cases c n; try (do e ← get_local n, subst e); reduce_ifs_at at_
 
 private meta def get_next_name (names : ref (list name)) : tactic name := do
 ns ← read_ref names,
@@ -84,4 +84,4 @@ tactic.split_ifs names at_
 
 end interactive
 
-end tactic
+end tactic

src/tactic/tidy.lean

@@ -39,17 +39,31 @@ do ng ← num_goals,
      "tactic.ext1 [] {new_goals := tactic.new_goals.all}"
    else "ext1"
 
+/-- `simp at *`, except we don't simplify hypotheses generated by the equation compiler. -/
+meta def simp_non_aux : tactic unit :=
+do ctx ← local_context,
+   let ctx := ctx.filter $ λ e, ¬ e.is_aux_decl,
+   let ctx := none :: (ctx.map $ λ e, some e.local_pp_name),
+   tactic.interactive.simp none ff [] [] (interactive.loc.ns ctx)
+
+/-- Same as `subst_vars`, but fails if it does not find a successful `subst`. -/
+meta def any_subst : tactic unit :=
+do ctx ← local_context,
+   ctx.any_of $ λ e, subst e
+
 meta def default_tactics : list (tactic string) :=
 [ reflexivity                                 >> pure "refl",
   `[exact dec_trivial]                        >> pure "exact dec_trivial",
   propositional_goal >> assumption            >> pure "assumption",
   ext1_wrapper,
   intros1                                     >>= λ ns, pure ("intros " ++ (" ".intercalate (ns.map (λ e, e.to_string)))),
+  any_subst                                   >> pure "any_subst",
   auto_cases,
   `[apply_auto_param]                         >> pure "apply_auto_param",
   `[dsimp at *]                               >> pure "dsimp at *",
-  `[simp at *]                                >> pure "simp at *",
+  simp_non_aux                                >> pure "simp at *",
   fsplit                                      >> pure "fsplit",
+  `[split_ifs]                                >> pure "split_ifs",
   injections_and_clear                        >> pure "injections_and_clear",
   propositional_goal >> (`[solve_by_elim])    >> pure "solve_by_elim",
   `[unfold_aux]                               >> pure "unfold_aux",

test/split_ifs.lean

@@ -15,4 +15,12 @@ example (p q : Prop) [decidable p] [decidable q] :
 by split_ifs; simp *
 
 example : true :=
-by success_if_fail { split_ifs }; trivial
+by success_if_fail { split_ifs }; trivial
+
+example (n : ℕ) : if n = 3 then n = 3 else true :=
+begin
+  split_ifs,
+  guard_target (3 = 3),
+  refl,
+  trivial
+end