# Zulip Chat Archive

## Stream: new members

### Topic: Type mismatch at application 2

#### Gareth Ma (Jan 20 2023 at 07:24):

Hi, I am getting cryptic error messages :tear: Here is my code:

```
have frac_pos : ∀ n : ℕ, 0 < 1 / (n + 1),
{
intro n,
have : 0 < n + 1,
{ linarith, },
exact div_pos zero_lt_one this,
},
```

Very simple, just prove `0 < n + 1`

, then `zero_lt_one`

gives `0 < 1`

, and them combined gives `0 < 1 / (n + 1)`

using `div_pos`

. Great!

... No, it gives the following error message:

```
type mismatch at application
div_pos zero_lt_one this
term
this
has type
0 < n + 1
but is expected to have type
0 < ?m_3
Additional information:
.../src/grhkm.lean:82:10: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
type mismatch, term
div_pos ?m_5 ?m_6
has type
0 < ?m_3 / ?m_4
but is expected to have type
0 < 1 / (n + 1)
```

I can't seem to understand the message. It seems to fail to match `?m_3`

with `(n + 1)`

? Can someone explain what is happening and how I should fix it?

#### Martin Dvořák (Jan 20 2023 at 07:34):

The problem is that your statement does not hold. For example `1 / 2 = 0`

in natural numbers.

#### Gareth Ma (Jan 20 2023 at 07:37):

Oh... How do I make it so that it treats `1 / (n + 1)`

as a real number? I tried `↑1 / (n + 1)`

but it doesn't seem to work

#### Riccardo Brasca (Jan 20 2023 at 07:37):

The way to write the (usual) `1/(n+1)`

in Lean is `(1 : ℚ)/(1+n)`

.

#### Riccardo Brasca (Jan 20 2023 at 07:38):

Replace `ℚ`

by `ℝ`

if you want real numbers.

#### Martin Dvořák (Jan 20 2023 at 07:38):

FYI, this code works:

```
have frac_pos : ∀ x : ℚ, 0 < x → 0 < 1 / (x + 1),
{
intros,
have : 0 < x + 1,
{ linarith, },
rwa one_div_pos,
},
```

#### Riccardo Brasca (Jan 20 2023 at 07:39):

If you want to know why `1/0 = 0`

you can have a look here.

#### Gareth Ma (Jan 20 2023 at 07:41):

I see, that is useful, thank you so much.

#### Martin Dvořák (Jan 20 2023 at 07:42):

This also works:

```
lemma frac_pos : ∀ n : ℕ, 0 < (1 : ℚ) / (n + 1) :=
begin
intro,
rw one_div_pos,
exact nat.cast_add_one_pos n,
end
```

#### Riccardo Brasca (Jan 20 2023 at 07:42):

`↑1 / (n + 1)`

is "morally" correct, in the sense we need a coercion, but how can Lean read your mind and guess that the `↑`

means "coercion to real numbers" (maybe you want coercion to `ℤ`

)? Indeed, `1 : ℝ`

is exactly the same as `(↑1 : ℝ)`

, allowing Lean to understand where you want to send `1`

.

#### Riccardo Brasca (Jan 20 2023 at 07:43):

Once `1`

is understood to be a real number, Lean understands that it needs to use a coercion also for the denominator, so it inserts it automatically.

#### Martin Dvořák (Jan 20 2023 at 07:44):

Shorter:

```
lemma frac_pos (n : ℕ) : 0 < (1 : ℚ) / (n + 1) :=
nat.one_div_pos_of_nat
```

#### Ben Nale (Feb 02 2023 at 11:53):

Hi, I have some`a : Nat → Type`

and I want to show `x : a (m+n) = y : a (n+m)`

(with some additional info on x and y) but it's not letting me state the equality due to type mismatch. :smiling_face_with_tear: How do I tell Lean `m+n = n+m`

is obvious?

#### Johan Commelin (Feb 02 2023 at 11:57):

That's a tiny example of a tough problem. And it usually indicates that you are trying to fight dependent type theory.

#### Johan Commelin (Feb 02 2023 at 11:57):

There are solutions, but they are a pain to work with. So probably you want to take a step back and approach the task that brought you in this position in a slightly different way.

#### Arthur Paulino (Feb 02 2023 at 12:08):

`m+n = n+m`

with `m n : Nat`

is `Nat.add_comm`

. Can you paste a #mwe of what you're trying to do?

#### Ben Nale (Feb 02 2023 at 12:24):

```
def BitVec (w : Nat) := Fin (2^w)
def bbT (bs : List Bool) : BitVec bs.length := --converts a boolean list to a number via binary representation to base 10)
def to_bool (x : BitVec w) : List Bool := --inverse map of to_bool
List.range w |>.map (to_bit x)
theorem eq_to_bool (x : BitVec w) : x = bbT (to_bool x) :=
```

the last theorem is where the error occurs. It says ```
type mismatch
bbT (to_bool x)
has type
BitVec (List.length (to_bool x)) : Type
but is expected to have type
BitVec w : Type
```

#### Reid Barton (Feb 02 2023 at 12:32):

The simplest thing to do in this situation is just assert that `x.val = (bbT (to_bool x)).val`

#### Reid Barton (Feb 02 2023 at 12:33):

But in turn, the question is what are you using `eq_to_bool`

for

#### Ben Nale (Feb 02 2023 at 12:49):

To prove alot of other things. For example

x<y implies either the first digit of x is less than the first digit of y or else the second or...

I figured doing induction on boolean lists would be easier than say induction on x but not sure if there's a better way to go about proving this.

Last updated: Dec 20 2023 at 11:08 UTC