What's going on with Prod?

Stream: new members

[Jakub Nowak]

I've run into such two errors, and I'm pretty bamboozled about what's going on.

inductive VecOrd : Type 1 where
| zero : VecOrd
| succ : VecOrd → VecOrd

inductive VecType : Type where
| zero : VecType
| succ : VecType

def VecOrd.type : VecOrd → VecType
| .zero => .zero
| .succ .. => .succ

/--
error: stuck at solving universe constraint
  1 =?= max 1 ?u.588
while trying to unify
  Type : Type 1
with
  Sort (max 1 ?u.588) : Type (max 1 ?u.588)

-/
#guard_msgs in
def VecT (m : Type → Type) (α : Type) (ord : VecOrd) : Type :=
  (type : VecType) × (_ : ord.type = type) ×' ((match type, ord with
    | .zero, .zero => Unit
    | .succ, .succ o => α × m (VecT m α o)
  ) : Type)

inductive VecOrd : Type 1 where
| zero : VecOrd
| succ : VecOrd → VecOrd

inductive VecType : Type where
| zero : VecType
| succ : VecType

def VecOrd.type : VecOrd → VecType
| .zero => .zero
| .succ .. => .succ

def VecT (m : Type → Type) (α : Type) (ord : VecOrd) : Type :=
  (type : VecType) × (_ : ord.type = type) ×' Unit × ((match type, ord with
    | .zero, .zero => Unit
    | .succ, .succ o => α × m (VecT m α o)
  ) : Type)

/--
error: Invalid `⟨...⟩` notation: The expected type `VecT m α VecOrd.zero` is not an inductive type

Note: This notation can only be used when the expected type is an inductive type with a single constructor
-/
#guard_msgs in
def VecT.none : VecT m α .zero :=
  ⟨.zero, sorry, (), ()⟩

The second one is weird, because this works perfectly fine:

inductive VecOrd : Type 1 where
| zero : VecOrd

inductive VecType : Type where
| zero : VecType

def VecOrd.type : VecOrd → VecType
| .zero => .zero

def VecT (m : Type → Type) (α : Type) (ord : VecOrd) : Type :=
  (type : VecType) × (_ : ord.type = type) ×' Unit × ((match type, ord with
    | .zero, .zero => Unit
  ) : Type)

def VecT.none : VecT m α .zero :=
  ⟨.zero, sorry, (), ()⟩

[Anthony Wang]

(Bad suggestion, please ignore)

[Anthony Wang]

(deleted)

[Aaron Liu]

Anthony Wang said:

For your first error, it type-checks if you use → instead of ×' (which often leads to complicated universe level constraints):

But → and ×' are not the same, they're not even isomorphic

[Aaron Liu]

it works if you add a by exact

inductive VecOrd : Type 1 where
| zero : VecOrd
| succ : VecOrd → VecOrd

inductive VecType : Type where
| zero : VecType
| succ : VecType

def VecOrd.type : VecOrd → VecType
| .zero => .zero
| .succ .. => .succ

def VecT (m : Type → Type) (α : Type) (ord : VecOrd) : Type :=
  (type : VecType) × (_ : ord.type = type) ×' ((by exact match type, ord with
    | .zero, .zero => Unit
    | .succ, .succ o => α × m (VecT m α o)
  ) : Type)

[Aaron Liu]

the second one seems to be smart unfolding's fault

inductive VecOrd : Type 1 where
| zero : VecOrd
| succ : VecOrd → VecOrd

inductive VecType : Type where
| zero : VecType
| succ : VecType

def VecOrd.type : VecOrd → VecType
| .zero => .zero
| .succ .. => .succ

def VecT (m : Type → Type) (α : Type) (ord : VecOrd) : Type :=
  (type : VecType) × (_ : ord.type = type) ×' Unit × ((match type, ord with
    | .zero, .zero => Unit
    | .succ, .succ o => α × m (VecT m α o)
  ) : Type)

set_option smartUnfolding false in
def VecT.none {m α} : VecT m α .zero :=
  ⟨.zero, rfl, (), ()⟩

[Jakub Nowak]

Huh, thanks. Though, I still have no idea what's happening. Why by exact .. helps? Should I report any of these as an issue?

[Jakub Nowak]

I don't know what smartUnfolding does, but this option sounds like something useful that I shouldn't just turn off. Maybe it's possible to write the definition differently, so there's no need to turn it off?

[Jakub Nowak]

I've tried this, and in this case, not even turning off smartUnfolding helps.

inductive VecOrd : Type 1 where
| zero : VecOrd
| succ : VecOrd → VecOrd

inductive VecType : Type where
| zero : VecType
| succ : VecType

def VecOrd.type : VecOrd → VecType
| .zero => .zero
| .succ .. => .succ

mutual

def VecTTyped (m : Type → Type) (α : Type) (ord : VecOrd) {type : VecType} (_ : ord.type = type) : Type :=
match type, ord with
| .zero, .zero => Unit
| .succ, .succ o => α × m (VecT m α o)

def VecT (m : Type → Type) (α : Type) (ord : VecOrd) : Type :=
  (type : VecType) × (h : ord.type = type) ×' VecTTyped m α ord h

end

/--
error: Invalid `⟨...⟩` notation: The expected type `VecT m α VecOrd.zero` is not an inductive type

Note: This notation can only be used when the expected type is an inductive type with a single constructor
-/
#guard_msgs in
def VecT.none {m α} : VecT m α .zero :=
  ⟨.zero, rfl, ()⟩

[Aaron Liu]

Jakub Nowak said:

I've tried this, and in this case, not even turning off smartUnfolding helps.

In this case it's used well-founded recursion so there's no way to unfold it definitionally it's irreducible

[Jakub Nowak]

In the latter case, it seems like with mutual, function is no longer defeq with it's body.

[Aaron Liu]

yeah that's correct

[Aaron Liu]

it's not directly because of the mutual recursion

[Aaron Liu]

it's because you made it mutual, the calls are not decreasing in the same way, so it used a different strategy to show termination

[Aaron Liu]

and that strategy is well-founded recursion and functions defined with well founded recursion are never defeq to their body

[Jakub Nowak]

It seems like even with structural recursion function isn't defeq with body.

import Lean

inductive VecOrd : Type 1 where
| zero : VecOrd
| succ : VecOrd → VecOrd

inductive VecType : Type where
| zero : VecType
| succ : VecType

def VecOrd.type : VecOrd → VecType
| .zero => .zero
| .succ .. => .succ

def VecT (m : Type → Type) (α : Type) (ord : VecOrd) : Type :=
  (type : VecType) × (_ : ord.type = type) ×' Unit × ((match type, ord with
    | .zero, .zero => Unit
    | .succ, .succ o => α × m (VecT m α o)
  ) : Type)
termination_by structural ord

/--
error: Tactic `rfl` failed: The left-hand side
  VecT m α ord
is not definitionally equal to the right-hand side
  (type : VecType) ×
    (x : ord.type = type) ×'
      Unit ×
        match type, ord, x with
        | VecType.zero, VecOrd.zero, x => Unit
        | VecType.succ, o.succ, x => α × m (VecT m α o)

m : Type → Type
α : Type
ord : VecOrd
⊢ VecT m α ord =
    ((type : VecType) ×
      (x : ord.type = type) ×'
        Unit ×
          match type, ord, x with
          | VecType.zero, VecOrd.zero, x => Unit
          | VecType.succ, o.succ, x => α × m (VecT m α o))
-/
#guard_msgs in
theorem VecT.eq_def' : VecT m α ord = ((type : VecType) × (_ : ord.type = type) ×' Unit × ((match type, ord with
    | .zero, .zero => Unit
    | .succ, .succ o => α × m (VecT m α o)
  ) : Type)) := by
  rfl

[Aaron Liu]

I think you have to case on ord

[Jakub Nowak]

Aaron Liu said:

I think you have to case on ord

Doesn't help.

inductive VecOrd : Type 1 where
| zero : VecOrd
| succ : VecOrd → VecOrd

inductive VecType : Type where
| zero : VecType
| succ : VecType

def VecOrd.type : VecOrd → VecType
| .zero => .zero
| .succ .. => .succ

def VecT (m : Type → Type) (α : Type) (ord : VecOrd) : Type :=
  (type : VecType) × (_ : ord.type = type) ×' Unit × ((match type, ord with
    | .zero, .zero => Unit
    | .succ, .succ o => α × m (VecT m α o)
  ) : Type)
termination_by structural ord

theorem VecT.eq_def' : VecT m α ord = ((type : VecType) × (_ : ord.type = type) ×' Unit × ((match type, ord with
    | .zero, .zero => Unit
    | .succ, .succ o => α × m (VecT m α o)
  ) : Type)) := by
  cases ord
  · rfl
  · rfl

[Aaron Liu]

and maybe also turn off smart unfolding?

[Jakub Nowak]

Aaron Liu said:

and maybe also turn off smart unfolding?

Still doesn't work.

[Jakub Nowak]

Does smartUnfolding changes what is defeq and what isn't?

[Aaron Liu]

hmm weird

[Aaron Liu]

oh it's a naturality diamond I think

[Aaron Liu]

yeah and it also fails to prove the equation automatically

[Aaron Liu]

I think this is a bug maybe?

[Jakub Nowak]

Hm, should I post it on #lean4 , or directly on Github issues?

[Jakub Nowak]

I've tried debugging and reading Lean's code a little, but with my little knowledge of the internals I didn't make any progress at understanding why it's failing.

[Jakub Nowak]

Here's manual proof, maybe that can help in pinpointing the problem:

inductive VecOrd : Type 1 where
| zero : VecOrd
| succ : VecOrd → VecOrd

inductive VecType : Type where
| zero : VecType
| succ : VecType

def VecOrd.type : VecOrd → VecType
| .zero => .zero
| .succ .. => .succ

def VecT (m : Type → Type) (α : Type) (ord : VecOrd) : Type :=
  (type : VecType) × (_ : ord.type = type) ×' Unit × ((match type, ord with
    | .zero, .zero => Unit
    | .succ, .succ o => α × m (VecT m α o)
  ) : Type)

set_option pp.notation false

theorem VecT.eq_def' : VecT m α ord = ((type : VecType) × (_ : ord.type = type) ×' Unit × ((match type, ord with
    | .zero, .zero => Unit
    | .succ, .succ o => α × m (VecT m α o)
  ) : Type)) := by
  cases ord
  · conv => lhs; delta VecT
    simp only
    congr
    funext type
    congr
    funext h
    congr
    split
    · rfl
    · grind only
  · conv => lhs; delta VecT
    simp only
    congr
    funext type
    congr
    funext h
    congr
    split
    · grind only
    . congr
      conv => rhs; delta VecT
      grind only

[Niklas Halonen]

I'm not sure how termination_by structural ord works/should work, but I don't think it can get rid of well-founded recursion as the inner match is inside the sigma over the Eq. Anyways it looks like the following works (with termination_by ord and gives your eq_def':

inductive VecOrd : Type 1 where
| zero : VecOrd
| succ : VecOrd → VecOrd

inductive VecType : Type where
| zero : VecType
| succ : VecType

def VecOrd.type : VecOrd → VecType
| .zero => .zero
| .succ .. => .succ

def VecT (m : Type → Type) (α : Type) (ord : VecOrd) : Type :=
  (type : VecType) × (_ : ord.type = type) ×' Unit × ((match type, ord with
    | .zero, .zero => Unit
    | .succ, .succ o => α × m (VecT m α o)
  ) : Type)
termination_by ord


/-
@[irreducible] def VecT : (Type → Type) → Type → VecOrd → Type :=
fun m α =>
  VecT._proof_1.fix fun ord a =>
    (type : VecType) ×
      (x : ord.type = type) ×'
        Unit ×
          (match (motive :=
              (type : VecType) →
                (ord : VecOrd) →
                  ord.type = type → ((y : VecOrd) → (invImage (fun x => x) sizeOfWFRel).1 y ord → Type) → Type)
              type, ord, x with
            | VecType.zero, VecOrd.zero, x => fun x => Unit
            | VecType.succ, o.succ, x => fun x => α × m (x o ⋯))
            a
-/
#print VecT

/-
∀ (m : Type → Type) (α : Type) (ord : VecOrd),
  VecT m α ord =
    ((type : VecType) ×
      (x : ord.type = type) ×'
        Unit ×
          match type, ord, x with
          | VecType.zero, VecOrd.zero, x => Unit
          | VecType.succ, o.succ, x => α × m (VecT m α o))
-/
#check VecT.eq_def

theorem VecT.eq_def' : VecT m α ord = ((type : VecType) × (_ : ord.type = type) ×' Unit × ((match type, ord with
    | .zero, .zero => Unit
    | .succ, .succ o => α × m (VecT m α o)
  ) : Type)) := eq_def _ _ _

Tested on 4.24.0 and 4.26.0-rc2

[Aaron Liu]

but unfortunately you lose defeqs

[Kyle Miller]

I haven't seen anyone mention that structural recursion isn't able to generate equation lemmas. That could be indicating a significant problem. Plus, if it could generate the equation lemma, any eq_def lemma would be already proved.

import Lean

inductive VecOrd : Type 1 where
| zero : VecOrd
| succ : VecOrd → VecOrd

inductive VecType : Type where
| zero : VecType
| succ : VecType

def VecOrd.type : VecOrd → VecType
| .zero => .zero
| .succ .. => .succ

def VecT (m : Type → Type) (α : Type) (ord : VecOrd) : Type :=
  Sigma.{0,0} fun type : VecType =>
    PSigma.{0,1} fun _ : ord.type = type =>
      match type, ord with
      | .zero, .zero => Unit
      | .succ, .succ o => α × m (VecT m α o)

#print VecT.eq_1
/-
Failed to realize constant VecT.eq_1:
  failed to generate equational theorem for `VecT`
    no progress at goal

m : Type → Type
α : Type
ord : VecOrd
r : VecOrd.below ord := (VecOrd.brecOn.go ord fun ord f =>
    (type : VecType) ×
      (x : ord.type = type) ×'
        (match (motive := (type : VecType) → (ord : VecOrd) → ord.type = type → VecOrd.below ord → Type) type, ord,
            x with
          | VecType.zero, VecOrd.zero, x => fun x => Unit
          | VecType.succ, o.succ, x => fun x => α × m x.1)
          f).2
⊢ ((type : VecType) ×
    (x : ord.type = type) ×'
      (match (motive :=
          (type : VecType) →
            (ord : VecOrd) → ord.type = type → VecOrd.rec PUnit (fun a a_ih => Type ×' a_ih) ord → Type)
          type, ord, x with
        | VecType.zero, VecOrd.zero, x => fun x => Unit
        | VecType.succ, o.succ, x => fun x => α × m x.1)
        r) =
  ((type : VecType) ×
    (x : ord.type = type) ×'
      match type, ord, x with
      | VecType.zero, VecOrd.zero, x => Unit
      | VecType.succ, o.succ, x => α × m (VecT m α o))
-/

(I also haven't seen anyone mention that it's Sigma, not Prod.)