a whole new error

Stream: general

[Kenny Lau]

invalid pattern, 'choice (frozen_name multiset.cons) (frozen_name list.cons)' is overloaded, and this kind of overloading is not currently supported in patterns

[Mario Carneiro]

use a local notation

[Mario Carneiro]

what did you write to get that?

[Kenny Lau]

theorem reduce.not : ∀ {L₁ L₂ L₃ : list (α × bool)} (x b), reduce L₁ = L₂ ++ (x, b) :: (x, bnot b) :: L₃ → false
| [] [] L3 _ _ H := by injections
| [] [hd] L3 _ _ H := by injections
| ((x,b)::hd1) L2 L3 _ _ H := by dsimp at H;
  exact match reduce hd1 with
  | [] := by dsimp at H
  | (x2,b2)::hd2 := _
  end

[Mario Carneiro]

does it help to use ((x2,b2)::hd2 : list _) instead?

[Kenny Lau]

well, it doesn't, but list.cons worked

[Mario Carneiro]

theorem reduce.not : ∀ (L₁ L₂ L₃ : list (α × bool)) (x b), reduce L₁ ≠ L₂ ++ (x, b) :: (x, bnot b) :: L₃
| [] L2 L3 _ _ := λ h, by simpa using (list.append_eq_nil.1 h.symm).2
| ((x,b)::L1) L2 L3 x' b' := begin
  dsimp [reduce],
  cases r : reduce L1,
  { dsimp [reduce], intro h,
    have := congr_arg list.length h,
    simp [-add_comm] at this,
    exact absurd this dec_trivial },
  cases hd with y c,
  by_cases x = y ∧ ¬b = c; simp [reduce, h]; intro H,
  { rw H at r,
    exact reduce.not L1 ((y,c)::L2) L3 x' b' r },
  rcases L2 with _|⟨a, L2⟩,
  { injections, substs x' y c b',
    refine h ⟨rfl, _⟩,
    cases b; exact dec_trivial },
  { refine reduce.not L1 L2 L3 x' b' _,
    injection H with _ H,
    rw [r, H], refl }
end

ah, I couldn't help myself

[Kenny Lau]

thanksssss

[Kenny Lau]

and I just realized that I only have two interface theorems

[Kenny Lau]

and I don't have to change the rest

[Kenny Lau]

which is again a testimony of the theory of interface