# Zulip Chat Archive

## 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 _,
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 (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.swap`

s, which should only work on `decidable_eq`

types. 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 `def`

s 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

`def`

s 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

`def`

s 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