Zulip Chat Archive

Stream: new members

Topic: Problem with induction hypothesis/generalization

Marcus Rossel (Jan 10 2022 at 10:43):

Ok, I've got another one which is a bit more complicated:

inductive E
structure D where es : Nat  E
inductive C
structure B where cs : Nat  List C
structure A where bs : Nat  B

def CEquivE : C  E  Prop := sorry

def makeE {a : A} {b : B} (hb :  i, a.bs i = b) {c : C} {i} (hc : c  b.cs i) : E := sorry

example (a : A) (b : B) (hb :  i, a.bs i = b) (i : Nat) :
  List.forall₂ CEquivE (b.cs i) ((b.cs i).attach.map (makeE hb ·.property)) := by
  generalize b.cs i = x

Here I can't generalize, because tactic 'generalize' failed, result is not type correct.
Simply trying induction b.cs i has the same problem.

I'm guessing it has something to do with the fact that I'm using attach on b.cs i, but I don't know how to resolve the issue.

Last updated: Dec 20 2023 at 11:08 UTC