## Stream: general

### Topic: a whole new error

#### Kenny Lau (Apr 21 2018 at 06:25):

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 (Apr 21 2018 at 06:26):

use a local notation

#### Mario Carneiro (Apr 21 2018 at 06:26):

what did you write to get that?

#### Kenny Lau (Apr 21 2018 at 06:28):

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 (Apr 21 2018 at 06:30):

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

#### Kenny Lau (Apr 21 2018 at 06:32):

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

#### Mario Carneiro (Apr 21 2018 at 07:08):

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,
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

thanksssss

#### Kenny Lau (Apr 21 2018 at 07:11):

and I just realized that I only have two interface theorems

#### Kenny Lau (Apr 21 2018 at 07:11):

and I don't have to change the rest

#### Kenny Lau (Apr 21 2018 at 07:11):

which is again a testimony of the theory of interface

Last updated: Aug 03 2023 at 10:10 UTC