decidable_eq problem

Stream: general

[Heather Macbeth]

I would like some help fixing an error. Apologies for the length, this was a little hard to minimize.

import analysis.normed_space.inner_product

open_locale classical

variables (𝕜 : Type*) {E : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 E]

local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y

/-- Example with no errors -/
example (k : ℕ) {i j : fin (k + 1)} (h : ¬i = 0) (h' : ¬j = 0) :
  ite (i = j) (1:𝕜) 0 = ite (i.pred h = j.pred h') 1 0 :=
begin
  refine if_congr _ rfl rfl, -- no errors here

end


/-- build up to the (apparent) same goal state, with error -/

instance submodule_inner_product_space {W : submodule 𝕜 E} : inner_product_space 𝕜 W :=
{ inner             := λ x y, ⟪(x:E), ↑y⟫,
  conj_sym          := λ _ _, inner_conj_sym _ _ ,
  nonneg_im         := λ _, inner_self_nonneg_im,
  norm_sq_eq_inner  := λ _, norm_sq_eq_inner _,
  add_left          := λ _ _ _ , inner_add_left,
  smul_left         := λ _ _ _, inner_smul_left,
  ..submodule.normed_space W }

def orthonormal {ι : Type*} (v : ι → E) : Prop :=
∀ i j, ⟪v i, v j⟫ = if i = j then (1:𝕜) else (0:𝕜)

example [finite_dimensional 𝕜 E] {k : ℕ} (hk : finite_dimensional.findim 𝕜 E = k + 1)
  {x : E} (hx : ∥x∥ = 1) {w : fin k → (𝕜 ∙ x)ᗮ} (hw : orthonormal 𝕜 w) :
  orthonormal 𝕜 (λ i : fin (k + 1), if h : i = 0 then x else coe (w (i.pred h))) :=
begin
  intros i j,
  by_cases h : i = 0, { sorry },
  by_cases h' : j = 0, { sorry },
  convert hw (i.pred h) (j.pred h') using 1, { sorry },
  refine if_congr _ rfl rfl, -- error here

end

[Heather Macbeth]

The error is

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  subtype.decidable_eq i j
inferred
  classical.prop_decidable (i = j)

[Yakov Pechersky]

Do you have to have open_locale classical at the top?

[Yakov Pechersky]

Your orthonormal doesn't require decidable_eq on the {ι : Type*}

[Yakov Pechersky]

I would just require that, which will make the if then else happy, and then rely in other things to choose whether to use a type which is truly decidable_eq like fin n, or conjure up such an instance with classical.

[Yakov Pechersky]

Those suggestions are without actually trying it, I might be wrong.

[Heather Macbeth]

Yup, requiring decidable_eq for orthonormal seems to work!

[Heather Macbeth]

Yakov Pechersky said:

Do you have to have open_locale classical at the top?

Is this a problem? I thought that in mathlib it was supposed to be safe to make everything classical everywhere :)

[Yakov Pechersky]

In any case, whenever you do an ite (a = b), you're making the claim you can actually decide that. And what happens downstream is that fin n knows it can supply decidable_eq from the fact that nat is decidable_eq and fin is a subtype.

[Yakov Pechersky]

And borks, because it's not the more general and not computable classical.prop_decidable

[Yakov Pechersky]

We ran into this problem recently with equiv.swaps, which should only work on decidable_eqtypes. So some lemmas about them were stated with classical instead of just general variables ... [decidable_eq ...]

[Yakov Pechersky]

Because later on, proving concrete specialized lemmas over fin or option ι or what have you hits the same issue you're hitting now.

[Yakov Pechersky]

Someone that understand this better than me can comment -- but should defs state explicitly the decidable_eq constraints, and downstream, uses of the def can satisfy that with classical?

[Heather Macbeth]

Yakov Pechersky said:

Someone that understand this better than me can comment -- but should defs state explicitly the decidable_eq constraints, and downstream, uses of the def can satisfy that with classical?

If this is correct, it seems like a useful rule of thumb.

[Yakov Pechersky]

For your (λ i : fin (k + 1), if h : i = 0 then x else coe (w (i.pred h))) you might prefer fin.cases _ _ i

[Heather Macbeth]

Could you indicate the specific syntax? I had a quick look but didn't see how to use it.

[Yakov Pechersky]

fin.cases x (λ j, coe (w j)) i

[Yakov Pechersky]

So no need to juggle hypotheses about positivity or pred. And the simp lemmas for fin.cases are clean.

[Yakov Pechersky]

Otherwise, you'd be proving things about how ite i.succ = 0 is always false by having to introduce the relevant inequality, then i.succ.pred = i etc etc

[Heather Macbeth]

Yakov Pechersky said:

Otherwise, you'd be proving things about how ite i.succ = 0 is always false by having to introduce the relevant inequality, then i.succ.pred = i etc etc

Hmm, I didn't need to do anything like this in my proof, maybe it's a slightly different situation.

[Yakov Pechersky]

With fin (n + 1) it's either casing on if it is 0 or positive (I like rcases eq_or_lt_of_le (fin.zero_le i)) or casing on if it is 0 or the i.succ for some i : fin n.

[Kevin Buzzard]

Isn't there some rule of thumb about when to use decidable_eq, which I've never managed to internalise because it's "not mathematics"?

[Heather Macbeth]

Yakov Pechersky said:

With fin (n + 1) it's either casing on if it is 0 or positive (I like rcases eq_or_lt_of_le (fin.zero_le i)) or casing on if it is 0 or the i.succ for some i : fin n.

I suppose the former is closer to the style of the proof I was writing. I hadn't found it awkward, but let me experiment with fin.cases. The syntax you suggested gives an error, any ideas?

type mismatch at application
  fin.cases x
term
  x
has type
  E : Type u_2
but is expected to have type
  ?m_1 0 : Sort ?

This is for my original code, modified to have

  orthonormal 𝕜 (fin.cases x (λ j, coe (w j))) :=

as line 34.

[Heather Macbeth]

Yakov Pechersky said:

With fin (n + 1) it's either casing on if it is 0 or positive (I like rcases eq_or_lt_of_le (fin.zero_le i)) or casing on if it is 0 or the i.succ for some i : fin n.

More precisely, my proof before was casing using by_cases h : i = 0, and in the second (nonzero) case working with i.pred h.

[Yakov Pechersky]

For fin.cases, you'll still need the 'fun i, fin.cases _ _ i'. I think your way is great and clear.

[Heather Macbeth]

Hmm, with the modification

  orthonormal 𝕜 (λ i, (fin.cases x (λ j, coe (w j)) i)) :=

I get a different error,

invalid 'fin.cases' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables
  ?m_1

[Yakov Pechersky]

Well then, I guess the ite is the best choice :-)

[Anne Baanen]

Heather Macbeth said:

Yakov Pechersky said:

Someone that understand this better than me can comment -- but should defs state explicitly the decidable_eq constraints, and downstream, uses of the def can satisfy that with classical?

If this is correct, it seems like a useful rule of thumb.

This is more or less the design rule I follow: classical is for internal use only. Therefore, unfolding a definition or applying a lemma should not introduce classical. So not only definitions, but also lemma statements, should avoid the use of classical.

In practice, I declare variables [deι : decidable_eq ι] if I need decidability. Since named parameters won't get included in the hypotheses if they are not used in a definition or lemma statement, there should be no complaints from the classical linter.