Idris2中expanded_shape函数调用无法在类型内归约的问题

我希望lemma4中的expanded_shape (DimSame Scalar p)能够归约，从而使用Refl完成证明，但尝试时出现以下错误：

Error: While processing right hand side of lemma4. Can't solve constraint between: [p] and expanded_shape (DimSame Scalar p).

完整代码 #

import Data.Vect
import Data.Nat

%default total

Shape : Nat -> Type
Shape n = Vect n Nat

data Array : Type -> Shape n -> Type where
    FromElem : e -> Array e []
    FromVec : Vect n (Array e s) -> Array e (n::s) 

data Broadcastable : Shape n1 -> Shape n2 -> Type where
    Scalar : Broadcastable [] []
    Dim1Left : {s1, s2: Shape n} -> Broadcastable s1 s2 -> (r: Nat) -> Broadcastable (1::s1) (r::s2)
    DimSame : {s1, s2: Shape n} -> Broadcastable s1 s2 -> (p: Nat) -> Broadcastable (p::s1) (p::s2)
    AppendLeft: {s1, s2: Shape n} -> Broadcastable s1 s2 -> (v: Vect nv Nat) -> Broadcastable (v ++ s1) s2
    Reflect : Broadcastable s1 s2 -> Broadcastable s2 s1

prf : Broadcastable [4, 8, 9, 1] [1, 4]
prf = ?hole 

max_comm : (a, b : Nat) -> maximum a b = maximum b a
max_comm Z Z = Refl
max_comm Z (S b) = Refl
max_comm (S a) Z = Refl 
max_comm (S a) (S b) = cong S (max_comm a b)

maxSame : (a: Nat) -> maximum a a = a
maxSame Z = Refl
maxSame (S a) = cong S (maxSame a) 

maxSucc : (n: Nat) -> (maximum (S n) n) = S n
maxSucc Z = Refl
maxSucc (S n) = cong S (maxSucc n) 

succInjective : {a: Nat} -> {b: Nat} -> S a = S b -> a = b
succInjective prf = cong pred prf

maxIDK : (a: Nat) -> (b: Nat) -> maximum a b = a -> maximum (S a) b = S a
maxIDK a Z prf = Refl
maxIDK (S a) (S b) prf = cong S (maxIDK a b (succInjective prf)) 
maxIDK Z b prf = rewrite prf in Refl

max_plus_b : (a, b : Nat) -> maximum (a + b) b = a + b
max_plus_b Z b = maxSame b 
max_plus_b (S a) b = (maxIDK (a + b) b (max_plus_b a b)) 


lemma : (nv, n2 : Nat) -> plus nv (maximum n2 n2) = maximum (plus nv n2) n2
lemma nv n2 = rewrite (max_plus_b nv n2) in (rewrite (maxSame n2) in Refl) 

expanded_shape : {s1: Shape n1} -> {s2: Shape n2} -> Broadcastable s1 s2 -> Shape (maximum n1 n2)
expanded_shape Scalar = []
expanded_shape (Dim1Left b r) = r::(expanded_shape b)
expanded_shape (DimSame b p) = p::(expanded_shape b)
expanded_shape (Reflect b) = rewrite (max_comm n1 n2) in (expanded_shape b)
expanded_shape (AppendLeft {nv} b v) = rewrite sym (lemma nv n2) in (v ++ expanded_shape b)

lemma4 : (p: Nat) -> expanded_shape (DimSame Scalar p) = [p] 
lemma4 p = ?lemma4_rhs

尝试的改写 #

我还尝试了以下写法，但遇到相同错误：

expanded_shape_scalar_nil : expanded_shape Scalar = []
expanded_shape_scalar_nil = Refl

lemma4 : (p: Nat) -> expanded_shape (DimSame Scalar p) = [p]
lemma4 p =
  rewrite expanded_shape_scalar_nil in Refl

内容的提问来源于stack exchange，提问作者Belphegor