Zulip Chat Archive

Stream: mathlib4

Topic: !4#3225

Jeremy Tan (Apr 02 2023 at 12:27):

!4#3225 I need help with the calc part of the first theorem, it's too golfed

Jeremy Tan (Apr 02 2023 at 12:28):

rw [finSuccEquiv_apply]
    calc
      _ = eval _ p := _
      _ = 0 := h _
    · intro i
      exact Fin.cases (eval x q) x i
    apply induction_on p
    · intro r

Jeremy Tan (Apr 02 2023 at 12:29):

I already figured out what goes in eval _ p, but then Lean can't figure out the third underscore (the proof of that step)

Yaël Dillies (Apr 02 2023 at 12:29):

Isn't it because it's the

    · intro i
      exact Fin.cases (eval x q) x i

Jeremy Tan (Apr 02 2023 at 12:30):

I also observe that in mathlib3 extra goals are generated in the calc proof, but here I'm not sure how the rest of the proof links up with the second and last step in the calc

Jeremy Tan (Apr 02 2023 at 12:34):

No, this doesn't work:

    calc
      _ = eval (fun i => Fin.cases (eval x q) x i) p := by exact Fin.cases (eval x q) x i
      _ = 0 := by apply h _
    apply induction_on p
    · intro r

This is the mathlib3 proof for comparison:

    calc _ = eval _ p : _
       ... = 0 : h _,
    { intro i, exact fin.cases (eval x q) x i },
    apply induction_on p,
    { intro r,
      simp only [eval_C, polynomial.eval_C, ring_hom.coe_comp, eval₂_hom_C], },
    { intros, simp only [*, ring_hom.map_add, polynomial.eval_add] },
    { intros φ i hφ, simp only [*, eval_X, polynomial.eval_mul, ring_hom.map_mul, eval₂_hom_X'],
      congr' 1,
      by_cases hi : i = 0,
      { subst hi, simp only [polynomial.eval_X, fin.cases_zero] },
      { rw [← fin.succ_pred i hi], simp only [eval_X, polynomial.eval_C, fin.cases_succ] } },
    { apply_instance, },

Jeremy Tan (Apr 02 2023 at 12:35):

eval (fun i => Fin.cases (eval x q) x i) p is correct by the way (found by prodding in mathlib3)

Yaël Dillies (Apr 02 2023 at 12:35):

~~... because you didn't translate the intro i?~~ because you're filling in the wrong hole

Jeremy Tan (Apr 02 2023 at 12:36):

_ = eval (fun i => Fin.cases (eval x q) x i) p := by intro i; exact Fin.cases (eval x q) x i fails:
tactic 'introN' failed, insufficient number of binders

Yaël Dillies (Apr 02 2023 at 12:41):

Is the problem not just that mathlib4's calc doesn't generate goals for placeholders but instead asks you to fill them in straight away?

    apply induction_on p,
    { intro r,
      simp only [eval_C, polynomial.eval_C, ring_hom.coe_comp, eval₂_hom_C], },
    { intros, simp only [*, ring_hom.map_add, polynomial.eval_add] },
    { intros φ i hφ, simp only [*, eval_X, polynomial.eval_mul, ring_hom.map_mul, eval₂_hom_X'],
      congr' 1,
      by_cases hi : i = 0,
      { subst hi, simp only [polynomial.eval_X, fin.cases_zero] },
      { rw [← fin.succ_pred i hi], simp only [eval_X, polynomial.eval_C, fin.cases_succ] } },
    { apply_instance, },