Zulip Chat Archive

Stream: lean4

Topic: Annoying LCNF errors

Uranus Testing (Sep 28 2022 at 16:02):

After updating Lean I started getting aΒ bunch of strange errors from the codegen (because problem disappears if I mark vect.subst as a theorem). Here’s MWE of such one:

namespace MWE

universe u v w

inductive Id {A : Type u} : A β†’ A β†’ Type u
| refl {a : A} : Id a a

attribute [eliminator] Id.casesOn

infix:50 (priority := high) " = " => Id

inductive Unit : Type u
| star : Unit

attribute [eliminator] Unit.casesOn

notation "𝟏" => Unit
notation "β˜…" => Unit.star
notation "β„•" => Nat

def vect (A : Type u) : β„• β†’ Type u
| Nat.zero   => 𝟏
| Nat.succ n => A Γ— vect A n

def vect.const {A : Type u} (a : A) : βˆ€ n, vect A n
| Nat.zero   => β˜…
| Nat.succ n => (a, const a n)

def vect.map {A : Type u} {B : Type v} (f : A β†’ B) :
  βˆ€ {n : β„•}, vect A n β†’ vect B n
| Nat.zero   => Ξ» _ => β˜…
| Nat.succ n => Ξ» v => (f v.1, map f v.2)

def transport {A : Type u} (B : A β†’ Type v) {a b : A} (p : a = b) : B a β†’ B b :=
by { induction p; apply id }

/-
type mismatch at LCNF application
  map f _x.12
argument f has type
  B β†’ A
but is expected to have type
  A β†’ A
-/
def vect.subst {A B : Type u} (p : A = B) (f : B β†’ A) {n : β„•} (v : vect A n) :
  vect.map f (transport (vect · n) p v) = vect.map (f ∘ transport id p) v :=
by { induction p; apply Id.refl }

James Gallicchio (Sep 28 2022 at 16:33):

I think these bugs are being reported on GitHub, see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/LCNF.20local.20context.20contains.20unused.20local.20variable.20declaratio/near/301102923

Mario Carneiro (Sep 28 2022 at 19:22):

@Leonardo de Moura Someone found a "mixing types and data" issue :)

Leonardo de Moura (Sep 28 2022 at 21:28):

I will take a look.

Leonardo de Moura (Sep 28 2022 at 22:40):

Pushed a fix for this issue. Great example for the test suite. Thanks for posting it.

Uranus Testing (Sep 29 2022 at 12:03):

It seems that’s not all. Even after fix this definition still reports a weird error:

type mismatch at LCNF application
  contrRespectsEquiv _x.5 _x.8
argument _x.5 has type
  (_ : (_ : B) Γ— lcErased = lcErased β†’ (_ : B) Γ— lcErased = lcErased) Γ—
    ((_ : (_ : B) Γ— lcErased = lcErased β†’ (_ : B) Γ— lcErased = lcErased) Γ—
        ((_ : B) Γ— lcErased = lcErased β†’ lcErased = lcErased)) Γ—
      (_ : (_ : B) Γ— lcErased = lcErased β†’ (_ : B) Γ— lcErased = lcErased) Γ—
        ((_ : B) Γ— lcErased = lcErased β†’ lcErased = lcErased)
but is expected to have type
  (_ : Sigma (Types.Id lcErased) β†’ (_ : B) Γ— lcErased = lcErased) Γ—
    ((_ : (_ : B) Γ— lcErased = lcErased β†’ Sigma (Types.Id lcErased)) Γ—
        (Sigma (Types.Id lcErased) β†’ lcErased = lcErased)) Γ—
      (_ : (_ : B) Γ— lcErased = lcErased β†’ Sigma (Types.Id lcErased)) Γ—
        ((_ : B) Γ— lcErased = lcErased β†’ lcErased = lcErased)

Here’s another MWE:

namespace MWE

universe u v w

inductive Id {A : Type u} : A β†’ A β†’ Type u
| refl {a : A} : Id a a

attribute [eliminator] Id.casesOn

infix:50 (priority := high) " = " => Id

def contr (A : Type u) := Ξ£ (a : A), βˆ€ b, a = b

def singl {A : Type u} (a : A) :=
Ξ£ b, a = b

def Corr (A : Type u) (B : Type v) :=
Ξ£ (R : A β†’ B β†’ Type w), (βˆ€ a, contr (Ξ£ b, R a b)) Γ— (βˆ€ b, contr (Ξ£ a, R a b))

def Homotopy {A : Type u} {B : A β†’ Type v} (f g : βˆ€ x, B x) :=
βˆ€ (x : A), f x = g x
infix:80 " ~ " => Homotopy

def isQinv {A : Type u} {B : Type v} (f : A β†’ B) (g : B β†’ A) :=
(f ∘ g ~ id) Γ— (g ∘ f ~ id)

def Qinv {A : Type u} {B : Type v} (f : A β†’ B) :=
Ξ£ (g : B β†’ A), isQinv f g

def Qinv.eqv (A : Type u) (B : Type v) :=
Ξ£ (f : A β†’ B), Qinv f

def linv {A : Type u} {B : Type v} (f : A β†’ B) :=
Ξ£ (g : B β†’ A), g ∘ f ~ id

def rinv {A : Type u} {B : Type v} (f : A β†’ B) :=
Ξ£ (g : B β†’ A), f ∘ g ~ id

def biinv {A : Type u} {B : Type v} (f : A β†’ B) :=
linv f Γ— rinv f

def Equiv (A : Type u) (B : Type v) : Type (max u v) :=
Ξ£ (f : A β†’ B), biinv f
infix:25 " ≃ " => Equiv

axiom ax₁ {A : Type u} {B : Type v} : A ≃ B β†’ contr A β†’ contr B
axiom axβ‚‚ {A : Type v} {B : Type u} (f g : A β†’ B) : (Ξ£ x, f x = g x) ≃ (Ξ£ x, g x = f x)
axiom axβ‚„ {A : Type u} {B : Type v} (w : Qinv.eqv A B) (b : B) : contr (Ξ£ a, b = w.1 a)
axiom ax₃ {A : Type u} (a : A) : contr (singl a)

def corrOfQinv {A : Type u} {B : Type v} : Qinv.eqv A B β†’ Corr A B :=
by { intro w; exists (Ξ» a b => b = w.1 a); apply Prod.mk <;> intro x;
     apply ax₁; apply axβ‚‚; apply ax₃; apply axβ‚„ }

Uranus Testing (Sep 29 2022 at 12:07):

It’s interesting also that if we replace last definition (corrOfQinv) with theorem, it will report other error:

application type mismatch
  ?m.23082 = Sigma.fst w a
argument
  Sigma.fst w a
has type
  B : Type v
but is expected to have type
  ?m.23103 a b : Type u_1

Leonardo de Moura (Sep 29 2022 at 13:25):

I will take a look.

Leonardo de Moura (Sep 29 2022 at 18:07):

Pushed a fix for the LCNF error.

Leonardo de Moura (Sep 29 2022 at 18:07):

I have added the example to the test suite.

Uranus Testing (Oct 02 2022 at 13:29):

These (new) errors seem to be related to the previous:

namespace MWE

inductive Id {A : Type u} : A β†’ A β†’ Type u
| refl {a : A} : Id a a

attribute [eliminator] Id.casesOn

infix:50 (priority := high) " = " => Id

def symm {A : Type u} {a b : A} (p : a = b) : b = a :=
by { induction p; exact Id.refl }

def transportconst {A B : Type u} : A = B β†’ A β†’ B :=
by { intros p x; induction p; exact x }

def transportconstInv {A B : Type u} (e : A = B) : B β†’ A :=
transportconst (symm e)

/-
type mismatch at LCNF application
  Id.refl
argument x has type
  B
but is expected to have type
  A
-/
def transportconstOverInv {A B : Type u} (p : A = B) :
  βˆ€ x, transportconst (symm p) x = transportconstInv p x :=
by { intro x; apply Id.refl }

/-
type mismatch at `MWE.transportconstInv'`, value has type
  (A B : Type u) β†’ A = B β†’ B β†’ B
but is expected to have type
  {A B : Type u} β†’ A = B β†’ B β†’ A
-/
def transportconstInv' {A B : Type u} : A = B β†’ B β†’ A :=
transportconst ∘ symm

Leonardo de Moura (Oct 02 2022 at 15:16):

Pushed a fix for this one. https://github.com/leanprover/lean4/commit/31d59e337bc2baf021f8025b9d18b37648359585

Uranus Testing (Oct 03 2022 at 12:51):

It’s strange, but the following isn’t working now, while previous example works.

namespace MWE

inductive Id {A : Type u} : A β†’ A β†’ Type u
| refl {a : A} : Id a a

attribute [eliminator] Id.casesOn

infix:50 (priority := high) " = " => Id

def symm {A : Type u} {a b : A} (p : a = b) : b = a :=
by { induction p; exact Id.refl }

def transport {A : Type u} (B : A β†’ Type v) {a b : A} (p : a = b) : B a β†’ B b :=
by { induction p; exact id }

def transportconst {A B : Type u} : A = B β†’ A β†’ B :=
transport id

def transportconstInv {A B : Type u} (e : A = B) : B β†’ A :=
transportconst (symm e)

def transportconstOverInv {A B : Type u} (p : A = B) :
  βˆ€ x, transportconst (symm p) x = transportconstInv p x :=
by { intro x; apply Id.refl }

def transportconstInv' {A B : Type u} : A = B β†’ B β†’ A :=
transportconst ∘ symm

Leonardo de Moura (Oct 03 2022 at 13:28):

I will take a look.

Leonardo de Moura (Oct 03 2022 at 16:50):

Pushed a fix for this one. https://github.com/leanprover/lean4/commit/fed7ff27e83173a9e2817002095c6bb55abd5ef4

Uranus Testing (Oct 09 2022 at 15:02):

Fresh problems:

namespace MWE

inductive Id {A : Type u} : A β†’ A β†’ Type u
| refl {a : A} : Id a a

attribute [eliminator] Id.casesOn

infix:50 (priority := high) " = " => Id

def symm {A : Type u} {a b : A} (p : a = b) : b = a :=
by { induction p; exact Id.refl }

def map {A : Type u} {B : Type v} {a b : A} (f : A β†’ B) (p : a = b) : f a = f b :=
by { induction p; apply Id.refl }

def transport {A : Type u} (B : A β†’ Type v) {a b : A} (p : a = b) : B a β†’ B b :=
by { induction p; exact id }

def boolToUniverse : Bool β†’ Type
| true  => Unit
| false => Empty

def ffNeqTt : false = true β†’ Empty :=
Ξ» p => transport boolToUniverse (symm p) ()

def isZero : Nat β†’ Bool
| Nat.zero   => true
| Nat.succ _ => false

/-
type mismatch at LCNF application
  ffNeqTt h
argument h has type
  Id Nat lcErased lcErased
but is expected to have type
  Id Bool lcErased lcErased
-/
def succNeqZero (n : Nat) : Nat.succ n = 0 β†’ Empty :=
Ξ» h => ffNeqTt (map isZero h)

Leonardo de Moura (Oct 09 2022 at 19:29):

Pushed a fix for this one. https://github.com/leanprover/lean4/commit/cc09afc5e14dc032f17e3d1d40e3121832a924be

Last updated: Dec 20 2023 at 11:08 UTC