Zulip Chat Archive

Stream: new members

Topic: How do I unfold match in the following example?

Z. Wu (Nov 07 2023 at 09:39):

In the following code, it is obvious that the example holds because we only care about the first element in the tuple returned by the match. But it seems like simp won't go through in this scenario. If I induction ht, then it works fine, which makes sense.

But if match has many more terms, it would be a nightmare because I have to invoke induction on each of the term. Is there a tactic that goes through in this scenario?

inductive Seqx {α: Type} : α -> Type where
| cons (s s': α): Seqx s' -> Seqx s

example {α: Type} (s s': α) (ht: Seqx s): s = (match s, ht with | sm, Seqx.cons _ q sn => (sm, q)).1  := by
  -- induction ht automagically works

Last updated: Dec 20 2023 at 11:08 UTC