infer_type decl.value different from decl.type

Stream: metaprogramming / tactics

[Xavier Martinet]

Hi,

Sometimes I have noticed that the proof term type (as inferred by tactic.infer_type) is different from the type of a given theorem. Not by a lot, but still.

I have a hard time finding a minimal working example, so this is some real-life thing I have stumbled upon:

import order.bounds data.nat.modeq

theorem myth :
  is_least { x : ℕ+ | 30 * x ≡ 42 [MOD 47] } 39 :=
begin
  fsplit,
  norm_num,
  dec_trivial!,
  rintro ⟨n, hn⟩,
  simp,
  intros h,
  apply int.coe_nat_le.1,
  norm_cast,
  norm_num,
  contrapose! h,
  dec_trivial!,
end

meta def check_decl_type (decl_nm : name) : tactic bool := do
  env ← tactic.get_env,
  decl ← env.get decl_nm,
  decl_ty ← tactic.infer_type decl.value,
  pure $ expr.alpha_eqv decl.type decl_ty

#eval tactic.trace $ check_decl_type `myth
-- ff

[Reid Barton]

Without more information that's not very surprising, for example the type of a theorem could be a specialization of the inferred type of its proof.

[Reid Barton]

Wait, I think that's wrong. But it's definitely true that the inferred type of the proof will often not be alpha-equivalent to the theorem statement. For example in lemma x : 1 + 1 = 2 := rfl the inferred type of the proof will be either 1 + 1 = 1 + 1 or 2 = 2.

[Xavier Martinet]

Please forgive my ignorance but: how is it possible? the type of lemma x has to be the same as the one of its proof term, hasn't it?

in your example, basically the elaborator fills out the blanks by lemma x : 1 + 1 = 2 := @rfl.{1} nat (has_add.add.{0} nat nat.has_add (has_one.one.{0} nat nat.has_one) (has_one.one.{0} nat nat.has_one))

so it really does lemma x : 1 + 1 = 2 := <rfl "1+1">, so to speak. Hence I understand why 1 + 1 = 1 + 1, but not why the right hand side can be recasted as a 2

[Reid Barton]

The types are definitionally equal, but not alpha equivalent

[Reid Barton]

there is a rule that says that if x : t and t is definitionally equal to t', then x : t' also

[Reid Barton]

and there are a whole bunch of definitional equality rules between types (or terms) that are not alpha-equivalent; for instance replacing something by its definition

[Xavier Martinet]

Alright, thanks! I didn't know about this "definitional equality" concept. So in your example, I suppose that somewhere 2 is defined as 1+1, and the typechecker is able to reduce all constants to their definition and compare able to able, correct?

[Kevin Buzzard]

Section 3.7 of the reference manual talks about definitional equality, and I just wrote a far more informal explanation about it in my course notes