## 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

.../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,
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 somea : 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