## Stream: general

### Topic: decidable_eq problem

#### Heather Macbeth (Jan 12 2021 at 23:24):

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 _,
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 (Jan 12 2021 at 23:24):

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 (Jan 12 2021 at 23:31):

Do you have to have open_locale classical at the top?

#### Yakov Pechersky (Jan 12 2021 at 23:32):

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

#### Yakov Pechersky (Jan 12 2021 at 23:33):

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 (Jan 12 2021 at 23:34):

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

#### Heather Macbeth (Jan 12 2021 at 23:35):

Yup, requiring decidable_eq for orthonormal seems to work!

#### Heather Macbeth (Jan 12 2021 at 23:36):

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 (Jan 12 2021 at 23:37):

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 (Jan 12 2021 at 23:37):

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

#### Yakov Pechersky (Jan 12 2021 at 23:38):

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 (Jan 12 2021 at 23:39):

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 (Jan 12 2021 at 23:40):

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 (Jan 12 2021 at 23:41):

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 (Jan 12 2021 at 23:44):

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 (Jan 12 2021 at 23:58):

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

#### Yakov Pechersky (Jan 13 2021 at 00:00):

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

#### Yakov Pechersky (Jan 13 2021 at 00:01):

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

#### Yakov Pechersky (Jan 13 2021 at 00:02):

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 (Jan 13 2021 at 00:04):

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 (Jan 13 2021 at 00:08):

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 (Jan 13 2021 at 00:09):

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 (Jan 13 2021 at 00:16):

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 (Jan 13 2021 at 00:21):

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 (Jan 13 2021 at 01:17):

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

#### Heather Macbeth (Jan 13 2021 at 01:25):

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 (Jan 13 2021 at 02:03):

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

#### Anne Baanen (Jan 13 2021 at 10:02):

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.

Last updated: May 13 2021 at 23:16 UTC