Type mismatch at application 2

Stream: new members

[Gareth Ma]

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]

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

[Gareth Ma]

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]

The way to write the (usual) 1/(n+1) in Lean is (1 : ℚ)/(1+n).

[Riccardo Brasca]

Replace ℚ by ℝ if you want real numbers.

[Martin Dvořák]

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]

If you want to know why 1/0 = 0 you can have a look here.

[Gareth Ma]

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

[Martin Dvořák]

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]

↑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]

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]

Shorter:

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

[Ben Nale]

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]

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

[Johan Commelin]

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]

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]

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]

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

[Reid Barton]

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

[Ben Nale]

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.