Zulip Chat Archive

Stream: general

Topic: a whole new error


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 06:26):

use a local notation

view this post on Zulip Mario Carneiro (Apr 21 2018 at 06:26):

what did you write to get that?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 06:30):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 06:32):

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

view this post on Zulip 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,
    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

view this post on Zulip Kenny Lau (Apr 21 2018 at 07:08):

thanksssss

view this post on Zulip Kenny Lau (Apr 21 2018 at 07:11):

and I just realized that I only have two interface theorems

view this post on Zulip Kenny Lau (Apr 21 2018 at 07:11):

and I don't have to change the rest

view this post on Zulip Kenny Lau (Apr 21 2018 at 07:11):

which is again a testimony of the theory of interface


Last updated: May 11 2021 at 23:11 UTC