Dependent type casting problem

Stream: new members

[GraceHopper]

Hello everyone,
we are new to Lean and are stuck at one point in our project for the university. We are writing a library for working with SessionTypes and want to translate this paper from Agda into Lean. However, we are encountering a problem with recursion in Chapter 4, specifically with the implementation of a stack. You probably don't need to read the paper, since we believe that our problem stems from not knowing exactly how typecasts work in Lean. The stack contains pairs of indexed types (SessionType n, Cmd A n S), where S must be typed with the same n. If we now want to implement push as described in xy, we can cast SessionType n to SessionType n+1.

However, when casting the Cmd, we somehow get stuck with its SessionType. Can you help us with this?

Many thanks in advance,

Anne, Jakob, Marlon.

These are the definitions you might need to understand:

inductive SessionType : Nat -> Type where

inductive Cmd (A: Type): Nat → SessionType n → Type where -- A is an ApplicationState

def opposite {n : Nat} (i : Fin n) : Fin n :=
  ⟨n - 1 - i.val, by omega⟩

def toN {n : Nat} (i : Fin n) : Nat := i.val

def CmdStack (n : Nat) (A : Type) : Type :=
  (i : Fin n) → Σ S : SessionType (toN (opposite i)), Cmd A (toN (opposite i)) S

And this is the push method we are stuck at:

def push {A : Type} {n : Nat} {S : SessionType n} (old_stack : CmdStack n A) (cmd : Cmd A n S) : CmdStack (n+1) A
| ⟨i + 1, p⟩ =>

    let fin_i: Fin (n) := ⟨i, by omega⟩
    let ⟨old_S, old_cmd⟩ := old_stack fin_i

    -- Proof, that the Indices are equal
    let h : toN (opposite ⟨i + 1, p⟩) = toN (opposite fin_i) := by
      simp [toN, opposite, fin_i]
      omega

    let old_S_casted := Eq.mp (by rw [h]) old_S

    let sess : SessionType (toN (opposite ⟨i + 1, p⟩)) := old_S_casted

    let old_cmd_casted := Eq.mp (by sorry) old_cmd -- by rw[h] didn't work here

    let cmd: Cmd A (toN (opposite ⟨i + 1, p⟩)) sess := by
        simp[h]
        simp[sess]

        exact old_cmd_casted

    ⟨sess, cmd⟩

| ⟨0, p ⟩ =>
    ⟨S, cmd⟩

[Marcus Rossel]

Does this work for you?

inductive SessionType : Nat → Type where

inductive Cmd (A : Type): Nat → SessionType n → Type where -- A is an ApplicationState

def Fin.opposite (i : Fin n) : Fin n :=
  ⟨n - 1 - i, by omega⟩

def CmdStack (n : Nat) (A : Type) : Type :=
  (i : Fin n) → Σ S : SessionType i.opposite, Cmd A i.opposite S

def push {S : SessionType n} (oldStack : CmdStack n A) (cmd : Cmd A n S) : CmdStack (n + 1) A
  | 0 => ⟨S, cmd⟩
  | ⟨i + 1, p⟩ =>
    let i : Fin n := ⟨i, by omega⟩
    let j := Fin.opposite ⟨i + 1, p⟩
    let ⟨oldSess, oldCmd⟩ := oldStack i
    have h₁ : (i.opposite : Nat) = j := by grind [Fin.opposite]
    let sess := h₁ ▸ oldSess
    have h₂ : Cmd A ↑i.opposite oldSess = Cmd A ↑j sess := by grind
    let cmd := h₂ ▸ oldCmd
    ⟨sess, cmd⟩

[Aaron Liu]

why do you want to cast?

[GraceHopper]

Aaron Liu schrieb:

why do you want to cast?

We stumbled upon something similar and thought that this might help tbh

[GraceHopper]

Nice, thank you @Marcus Rossel , this seems to work.