n + 1 = n + 8 + 8 - 3 - 3 - 3 - 3 - 3

Stream: new members

[Francis Southern]

Sorry if I'm being silly, but why doesn't exact match these:

invalid type ascription, term has type
  P (n + 8 + 8 - 3 - 3 - 3 - 3 - 3)
but is expected to have type
  P (n + 1)

?

[Eric Rodriguez]

that is weird... example {n : ℕ} : n + 8 + 8 -3-3-3-3-3 = n + 1 := rfl does work. is there maybe some weird instances messing things up? what happens if you set pp.all to true? (set_option pp.all true)

[Francis Southern]

invalid type ascription, term has type
  P
    (@has_sub.sub.{0} int int.has_sub
       (@has_sub.sub.{0} int int.has_sub
          (@has_sub.sub.{0} int int.has_sub
             (@has_sub.sub.{0} int int.has_sub
                (@has_sub.sub.{0} int int.has_sub
                   (@has_add.add.{0} int int.has_add
                      (@has_add.add.{0} int int.has_add n
                         (@bit0.{0} int int.has_add
                            (@bit0.{0} int int.has_add (@bit0.{0} int int.has_add (@has_one.one.{0} int int.has_one)))))
                      (@bit0.{0} int int.has_add
                         (@bit0.{0} int int.has_add (@bit0.{0} int int.has_add (@has_one.one.{0} int int.has_one)))))
                   (@bit1.{0} int int.has_one int.has_add (@has_one.one.{0} int int.has_one)))
                (@bit1.{0} int int.has_one int.has_add (@has_one.one.{0} int int.has_one)))
             (@bit1.{0} int int.has_one int.has_add (@has_one.one.{0} int int.has_one)))
          (@bit1.{0} int int.has_one int.has_add (@has_one.one.{0} int int.has_one)))
       (@bit1.{0} int int.has_one int.has_add (@has_one.one.{0} int int.has_one)))
but is expected to have type
  P (@has_add.add.{0} int int.has_add n (@has_one.one.{0} int int.has_one))

I'm doing the M40001 problem sheet from 2019, if that means anything to you.

[Yaël Dillies]

Ah, rfl won't work because it's in ℤ.

[Yaël Dillies]

It has to case on whether any on those involved numbers is negative.

[Yakov Pechersky]

The tactic to use here is norm_num

[Kevin Buzzard]

The problem would have been spotted sooner if the OP had provided a #mwe :-)

[Francis Southern]

Sorry, I suppose I need to get over the embarrassment of showing my work!
Here's the whole code:

lemma question_5_1 (P : ℤ → Prop) (h8 : ∀ n, P n → P (n + 8))
                                  (h3 : ∀ n, P n → P (n - 3))
                                  (p0 : P 0) :
(∀ n, P n -> P (n + 1)) ∧ (∀ n, P n -> P (n - 1)) :=
begin
  split,
  intros n pn,
  have z := ((h3 (n + 8 + 8 - 3 - 3 - 3 - 3)) ((h3 (n + 8 + 8 - 3 - 3 - 3)) ((h3 (n + 8 + 8 - 3 - 3)) ((h3 (n + 8 + 8 - 3)) ((h3 (n + 8 + 8)) ((h8 (n + 8)) ((h8 n) pn))))))),

end

But trying norm_num just gives me unknown identifier 'norm_num' and I couldn't find it in the reference manual either..

[Ruben Van de Velde]

import tactic.norm_num

[Ruben Van de Velde]

It doesn't work here, though. This does:

import tactic.ring
lemma question_5_1 (P : ℤ → Prop) (h8 : ∀ n, P n → P (n + 8))
                                  (h3 : ∀ n, P n → P (n - 3))
                                  (p0 : P 0) :
(∀ n, P n -> P (n + 1)) ∧ (∀ n, P n -> P (n - 1)) :=
begin
  split,
  { intros n pn,
    have z := ((h3 (n + 8 + 8 - 3 - 3 - 3 - 3)) ((h3 (n + 8 + 8 - 3 - 3 - 3)) ((h3 (n + 8 + 8 - 3 - 3)) ((h3 (n + 8 + 8 - 3)) ((h3 (n + 8 + 8)) ((h8 (n + 8)) ((h8 n) pn))))))),
    convert z using 1,
    ring },
  sorry,
end

[Francis Southern]

Hmm, that code gives me the following error:

type mismatch at application
  tactic.istep 151 4 151 4 229 ring
term
  ring
has type
  Type ? → Type ? : Type (?+1)
but is expected to have type
  tactic ?m_1 : Type ?

[Yaël Dillies]

Did you import ring?

[Francis Southern]

Erm, no. Why didn't it give me the unknown identifier error this time? Is there another ring that gets shadowed?
Anyway, it works now. Thank you everyone. :-)

[Yaël Dillies]

because it assumed it was docs#ring :wink:

[Ruben Van de Velde]

Yeah, that's one of the cases where the error is... somewhat bemusing

[Yakov Pechersky]

import tactic.norm_num

lemma question_5_1 (P : ℤ → Prop) (h8 : ∀ n, P n → P (n + 8))
                                  (h3 : ∀ n, P n → P (n - 3))
                                  (p0 : P 0) :
(∀ n, P n -> P (n + 1)) ∧ (∀ n, P n -> P (n - 1)) :=
begin
  split,
  { intros n pn,
    have z := ((h3 (n + 8 + 8 - 3 - 3 - 3 - 3)) ((h3 (n + 8 + 8 - 3 - 3 - 3)) ((h3 (n + 8 + 8 - 3 - 3)) ((h3 (n + 8 + 8 - 3)) ((h3 (n + 8 + 8)) ((h8 (n + 8)) ((h8 n) pn))))))),
    convert z using 1,
    norm_num [add_assoc, int.add_sub_assoc] },
  sorry,
end

[Yakov Pechersky]

The way to get norm_num to work is to get all the numeric terms together.

[Miles Carmack]

Hello