type argument conversion

Stream: lean4

[Anders Christiansen Sørby]

I'm trying to write a recursive function that returns a dependent type with a constraint, but this constraint changes from the recursion so I want to raise/cast it to the top level constraint Prop. How do I do this?

-- is this the best way to assign a variable in a type expression btw?
variable (bound : Bound := ⟨m, m+n, le_left_cancel⟩)

def progression (n m : Nat) : List <| BNat bound :=
  match n with
  | 0 => []
  | Nat.succ ns =>
    let ms := Nat.succ m;
    let ob : Bound := ⟨ms, ms+ns, le_left_cancel⟩;
    { val := m, isLe := sorry, isGe := sorry : BNat bound }
    :: (progression ns ms).map (λ b : BNat ob =>
      let h : (ob.max ≤ m+n) := by sorry;
      BNat.raise b (max := m+n) h : BNat bound
    )

The checker doesn't understand that BNat.raise returns the same bound. Why can't it do this? Is there a way to hint it about it? A Decide instance? Unification hints?

[James Gallicchio]

I'm not sure if there's a better way, but you can always manually specify the motive by using Nat.rec instead of a recursive definition. I think lean4's equation compiler needs some tuning still?

[Gabriel Ebner]

First of all, please post a #mwe.

[Gabriel Ebner]

-- is this the best way to assign a variable in a type expression btw?
variable (bound : Bound := ⟨m, m+n, le_left_cancel⟩)

This is the syntax for default arguments, not for let-bindings. The := just means that the value will be used if you call progression n m, but you can still provide a different one using progression ⟨...⟩ n m, so you can't assume that it's equal to the default one.

[Gabriel Ebner]

If you look in the term goal at BNat.raise b .. then you should also see that there are two m's. The m in the default argument is a different one than the m argument to progression.

[Gabriel Ebner]

What you probably want is the following:

def progression (n m : Nat) : let bound := ⟨m, m+n, le_left_cancel⟩; List <| BNat bound :=

[Gabriel Ebner]

I'd just write:

def progression (n m : Nat) : List (BNat ⟨m, m+n, le_left_cancel⟩) :=

[Anders Christiansen Sørby]

Thanks. Will post #mwe next time. I didn't know let expressions were allowed inside type expressions.