Zulip Chat Archive

Stream: new members

Topic: induction with hypothesis with tuple (Prod)

Z. Wu (Nov 03 2023 at 05:53):

In the proof of t1, induction in t1 fails to induct on the hypothesis of prop R (k, v) (w, r) and I have to use a single variable for (k, v) and (w, r) to make it go through, as shown in t2. Is there a way that allows me to carry (k, v) over in the induction in t1 as if it is a single variable?

inductive prop {α: Type} (R: α  α  Prop):  α  α  Prop where
| refl : (a:α), prop R a a
| trans: a b c, R a b  prop R b c  prop R a c

theorem t1 {α: Type} (R: α × α -> α × α -> Prop) (k v w r: α): prop R (k, v) (w, r) -> True := by
  intro h
  induction h -- failed
  -- index in target's type is not a variable (consider using the `cases` tactic instead)
  --  (k, v)

theorem t2 {α: Type} (R: α × α -> α × α -> Prop) (k v w r: α) kv wr: kv = (k, v) -> wr = (w, r) -> prop R kv wr -> True := by
  intro hkv hwr h -- or
  induction h -- ok

Last updated: Dec 20 2023 at 11:08 UTC