Nonsensical type mismatch

Stream: new members

[Kuba]

I am getting a weird application type mismatch message, where both the actual and expected type are the same:

application type mismatch
  Eq.subst (Eq.symm (tmp13 x xs m)) (tmp10 xs (x :: bs) m (Nat.lt_of_succ_lt_succ h))
argument
  tmp10 xs (x :: bs) m (Nat.lt_of_succ_lt_succ h)
has type
  List.get (List.reverseAux xs (x :: bs))
      { val := List.length xs - 1 - m,
        isLt := (_ : List.length xs - 1 - m < List.length (List.reverseAux xs (x :: bs))) } =
    List.get xs { val := m, isLt := (_ : m < List.length xs) } : Prop
but is expected to have type
  List.get (List.reverseAux xs (x :: bs))
      { val := List.length xs - 1 - m,
        isLt := (_ : List.length xs - 1 - m < List.length (List.reverseAux xs (x :: bs))) } =
    List.get xs { val := m, isLt := (_ : m < List.length xs) } : Prop

Here is the relevant code snippet:

theorem tmp10.{u} {α : Type u} : ∀ as bs : List α, ∀ n : Nat,  (h : n < as.length) →
  (List.reverseAux as bs).get ⟨as.length - 1 - n,
      Nat.lt_of_lt_of_le (tmp3 as.length n (tmp9 n as.length h)) (tmp7 as bs)⟩ =
    as.get ⟨n, h⟩ :=
λ as bs => λ n => λ h =>
  match as, n with
  | x :: xs, Nat.succ m => (Eq.subst
      (motive := λ y => (List.reverseAux xs (x :: bs) ).get ⟨y, _⟩ = xs.get ⟨m, _⟩)
      (Eq.symm (tmp13 x xs m))
      (tmp10 xs (x :: bs) m (Nat.lt_of_succ_lt_succ h)))
  | [], _ => ()

What I am trying to prove is List.reverse_aux2 which is already part of Mathlib, but I wanted to have a go myself as an exercise. Therefore this question is not about how to prove the theorem, but how to interpret the weird error message.

[Kevin Buzzard]

can you post a #mwe ? The code above doesn't run. Put by convert in front of your proof to get more detailed information about the part that Lean is stuck on.

[Kuba]

Sorry, here is all you should need (no imports required, I only used stuff that is part of Init):

theorem tmp1 : ∀ n : Nat, n > 0 → n - 1 < n :=
λ _ => λ h => Nat.sub_lt h (Nat.zero_lt_succ 0)

theorem tmp2 : ∀ n m k : Nat, n < m → n - k < m :=
λ n _ k => λ h => Nat.lt_of_le_of_lt (Nat.sub_le n k) h

theorem tmp3 : ∀ n m : Nat, 0 < n → n - 1 - m < n :=
λ n m => λ h => tmp2 (n - 1) n m (tmp1 n h)

theorem tmp6.{u} {α : Type u} :
  ∀ as bs : List α, (List.reverseAux as bs).length = as.length + bs.length :=
λ as bs =>
  match as with
  | [] => Eq.symm (Nat.zero_add bs.length)
  | a :: as =>
    Eq.trans (tmp6 as (a :: bs)) (
      Eq.trans (Nat.add_succ as.length bs.length) (
        Eq.symm (Nat.succ_add as.length bs.length)))

theorem tmp7.{u} {α : Type u} : ∀ as bs : List α,
  as.length <= (List.reverseAux as bs).length :=
λ as bs => Eq.subst (Eq.symm (tmp6 as bs)) (Nat.le_add_right as.length bs.length)

theorem tmp9 : ∀ m n : Nat, m < n → n > 0 :=
λ m _ => λ h => Nat.lt_of_le_of_lt (Nat.zero_le m) h

theorem tmp14 : ∀ n m k : Nat, n - m - k = n - k - m :=
λ n m k => Eq.trans
  (Eq.subst (motive := λ x => n - m - k = n - x)
    (Nat.add_comm m k) (Nat.sub_sub n m k))
  (Eq.symm (Nat.sub_sub n k m))

theorem tmp13.{u} {α : Type u} : ∀ a : α, ∀ as : List α, ∀ n : Nat,
  (a :: as).length - 1 - (Nat.succ n) = as.length - 1 - n :=
λ a => λ as => λ n => Eq.trans
  (Eq.subst (motive := λ x => (a::as).length - 1 - (Nat.succ n) = x - 1)
    (Nat.succ_sub_succ as.length n) (tmp14 (a :: as).length 1 (Nat.succ n)))
  (tmp14 as.length n 1)

theorem tmp10.{u} {α : Type u} : ∀ as bs : List α, ∀ n : Nat,  (h : n < as.length) →
  (List.reverseAux as bs).get ⟨as.length - 1 - n,
      Nat.lt_of_lt_of_le (tmp3 as.length n (tmp9 n as.length h)) (tmp7 as bs)⟩ =
    as.get ⟨n, h⟩ :=
λ as bs => λ n => λ h =>
  match as, n with
  | x :: xs, Nat.succ m => (Eq.subst
      (motive := λ y => (List.reverseAux xs (x :: bs) ).get ⟨y, _⟩ = xs.get ⟨m, _⟩)
      (Eq.symm (tmp13 x xs m))
      (tmp10 xs (x :: bs) m (Nat.lt_of_succ_lt_succ h)))
  | [], _ => ()

[Kuba]

I tried using the convert tactic. Since 'convert' is part of Mathlib, I cloned and tried building it on my machine (not sure whether that was successful). However, I can't import it into the file that contains my failing code, I get: unknown package 'Mathlib'.

[Alex J. Best]

You shouldn't manually clone mathlib, rather you need to add a dependency on mathlib inside your lakefile.lean by adding the lines

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

just before the default target

[Alex J. Best]

Then run lake update, lake exe cache get

[Kuba]

Thank you for the help with importing Mathlib, it works now.

I inserted by convert before the proof and this is what I got (code+infoview contents in the comments):

import Mathlib.Tactic.Convert

theorem tmp1 : ∀ n : Nat, n > 0 → n - 1 < n :=
λ _ => λ h => Nat.sub_lt h (Nat.zero_lt_succ 0)

theorem tmp2 : ∀ n m k : Nat, n < m → n - k < m :=
λ n _ k => λ h => Nat.lt_of_le_of_lt (Nat.sub_le n k) h

theorem tmp3 : ∀ n m : Nat, 0 < n → n - 1 - m < n :=
λ n m => λ h => tmp2 (n - 1) n m (tmp1 n h)

theorem tmp6.{u} {α : Type u} :
  ∀ as bs : List α, (List.reverseAux as bs).length = as.length + bs.length :=
λ as bs =>
  match as with
  | [] => Eq.symm (Nat.zero_add bs.length)
  | a :: as =>
    Eq.trans (tmp6 as (a :: bs)) (
      Eq.trans (Nat.add_succ as.length bs.length) (
        Eq.symm (Nat.succ_add as.length bs.length)))

theorem tmp7.{u} {α : Type u} : ∀ as bs : List α,
  as.length <= (List.reverseAux as bs).length :=
λ as bs => Eq.subst (Eq.symm (tmp6 as bs)) (Nat.le_add_right as.length bs.length)

theorem tmp9 : ∀ m n : Nat, m < n → n > 0 :=
λ m _ => λ h => Nat.lt_of_le_of_lt (Nat.zero_le m) h

theorem tmp14 : ∀ n m k : Nat, n - m - k = n - k - m :=
λ n m k => Eq.trans
  (Eq.subst (motive := λ x => n - m - k = n - x)
    (Nat.add_comm m k) (Nat.sub_sub n m k))
  (Eq.symm (Nat.sub_sub n k m))

theorem tmp13.{u} {α : Type u} : ∀ a : α, ∀ as : List α, ∀ n : Nat,
  (a :: as).length - 1 - (Nat.succ n) = as.length - 1 - n :=
λ a => λ as => λ n => Eq.trans
  (Eq.subst (motive := λ x => (a::as).length - 1 - (Nat.succ n) = x - 1)
    (Nat.succ_sub_succ as.length n) (tmp14 (a :: as).length 1 (Nat.succ n)))
  (tmp14 as.length n 1)

theorem tmp10.{u} {α : Type u} : ∀ as bs : List α, ∀ n : Nat,  (h : n < as.length) →
  (List.reverseAux as bs).get ⟨as.length - 1 - n,
      Nat.lt_of_lt_of_le (tmp3 as.length n (tmp9 n as.length h)) (tmp7 as bs)⟩ =
    as.get ⟨n, h⟩ := by convert
λ as bs => λ n => λ h =>
  match as, n with
  | x :: xs, Nat.succ m => (Eq.subst
      (motive := λ y => (List.reverseAux xs (x :: bs) ).get ⟨y, _⟩ = xs.get ⟨m, _⟩)
      (Eq.symm (tmp13 x xs m))
      (tmp10 xs (x :: bs) m (Nat.lt_of_succ_lt_succ h)))
  | [], _ => ()
/-
α : Type u
⊢ ∀ (as bs : List α) (n : Nat) (h : n < List.length as),
  List.get (List.reverseAux as bs)
      { val := List.length as - 1 - n, isLt := (_ : List.length as - 1 - n < List.length (List.reverseAux as bs)) } =
    List.get as { val := n, isLt := h }
-/
/-
application type mismatch
  Nat.lt_of_succ_lt_succ h
argument
  h
has type
  ?m.1775 : Sort ?u.1766
but is expected to have type
  Nat.succ m < Nat.succ (List.length xs) : Prop
-/
/-
unknown free variable '_uniq.1808'
-/
/-
type mistmatch, alternative has type
  (fun y =>
      List.get (List.reverseAux xs (x :: bs))
          { val := y, isLt := (_ : y < List.length (List.reverseAux xs (x :: bs))) } =
        List.get xs { val := m, isLt := (_ : m < List.length xs) })
    (List.length (x :: xs) - 1 - Nat.succ m) : Prop
but is expected to have type
  ?m.1576 (x :: xs) bs (Nat.succ m) h : Sort ?u.1547
-/

which is not that helpful.

[Kyle Miller]

"_uniq.1808" points to a bug somewhere (maybe the convert tactic? maybe from some interaction between convert and match?)

[Kuba]

Do you mean a bug in my code, or in the Mathlib?

[Kyle Miller]

mathlib or Lean

[Kyle Miller]

though it could be your code too

[Kyle Miller]

Why is the second case of the match ()? That's Unit, but it looks like the goal is an equality

[Kuba]

It is just a stub, I have not done the other cases yet.

[Kyle Miller]

You'd better put sorry rather than something that's type incorrect then

[Kuba]

Here is a corrected version:

import Mathlib.Tactic.Convert

theorem tmp1 : ∀ n : Nat, n > 0 → n - 1 < n :=
λ _ => λ h => Nat.sub_lt h (Nat.zero_lt_succ 0)

theorem tmp2 : ∀ n m k : Nat, n < m → n - k < m :=
λ n _ k => λ h => Nat.lt_of_le_of_lt (Nat.sub_le n k) h

theorem tmp3 : ∀ n m : Nat, 0 < n → n - 1 - m < n :=
λ n m => λ h => tmp2 (n - 1) n m (tmp1 n h)

theorem tmp6.{u} {α : Type u} :
  ∀ as bs : List α, (List.reverseAux as bs).length = as.length + bs.length :=
λ as bs =>
  match as with
  | [] => Eq.symm (Nat.zero_add bs.length)
  | a :: as =>
    Eq.trans (tmp6 as (a :: bs)) (
      Eq.trans (Nat.add_succ as.length bs.length) (
        Eq.symm (Nat.succ_add as.length bs.length)))

theorem tmp7.{u} {α : Type u} : ∀ as bs : List α,
  as.length <= (List.reverseAux as bs).length :=
λ as bs => Eq.subst (Eq.symm (tmp6 as bs)) (Nat.le_add_right as.length bs.length)

theorem tmp9 : ∀ m n : Nat, m < n → n > 0 :=
λ m _ => λ h => Nat.lt_of_le_of_lt (Nat.zero_le m) h

theorem tmp14 : ∀ n m k : Nat, n - m - k = n - k - m :=
λ n m k => Eq.trans
  (Eq.subst (motive := λ x => n - m - k = n - x)
    (Nat.add_comm m k) (Nat.sub_sub n m k))
  (Eq.symm (Nat.sub_sub n k m))

theorem tmp13.{u} {α : Type u} : ∀ a : α, ∀ as : List α, ∀ n : Nat,
  (a :: as).length - 1 - (Nat.succ n) = as.length - 1 - n :=
λ a => λ as => λ n => Eq.trans
  (Eq.subst (motive := λ x => (a::as).length - 1 - (Nat.succ n) = x - 1)
    (Nat.succ_sub_succ as.length n) (tmp14 (a :: as).length 1 (Nat.succ n)))
  (tmp14 as.length n 1)

theorem tmp10.{u} {α : Type u} : ∀ as bs : List α, ∀ n : Nat,  (h : n < as.length) →
  (List.reverseAux as bs).get ⟨as.length - 1 - n,
      Nat.lt_of_lt_of_le (tmp3 as.length n (tmp9 n as.length h)) (tmp7 as bs)⟩ =
    as.get ⟨n, h⟩ :=
λ as bs => λ n => λ h => by convert
  match as, n with
  | x :: xs, Nat.succ m => (Eq.subst
      (motive := λ y => (List.reverseAux xs (x :: bs) ).get ⟨y, _⟩ = xs.get ⟨m, _⟩)
      (Eq.symm (tmp13 x xs m))
      (tmp10 xs (x :: bs) m (Nat.lt_of_succ_lt_succ h)))
  | _, _ => sorry
/-

-/
/-
application type mismatch
  Nat.lt_of_succ_lt_succ h
argument
  h
has type
  n < List.length as : Prop
but is expected to have type
  Nat.succ m < Nat.succ (List.length xs) : Prop
-/
/-
unknown free variable '_uniq.1850'
-/
/-
type mistmatch, alternative has type
  (fun y =>
      List.get (List.reverseAux xs (x :: bs))
          { val := y, isLt := (_ : y < List.length (List.reverseAux xs (x :: bs))) } =
        List.get xs { val := m, isLt := (_ : m < List.length xs) })
    (List.length (x :: xs) - 1 - Nat.succ m) : Prop
but is expected to have type
  ?m.1806 h : Prop
-/

[Kuba]

The tactic state changed to No goals and the first message looks more helpful now. But you still have the _uniq thingy.