难以在 Idris 中应用证明答案

【问题标题】：Difficulty applying a proof in Idris难以在 Idris 中应用证明
【发布时间】：2017-09-11 20:38:54
【问题描述】：

我正在尝试证明我定义的数据类型之一的属性，如下所示：

reverseProof' : (inputBlock : Block iType iSize iInputs)
          -> (ind : Fin rSize)
          -> (rInputs : Vect rSize Ty)
          -> (receiveBlock : Block rType rSize rInputs)
          -> (prf : index ind rInputs = iType)
          -> (newInsert : MaybeBlockty iType)
          -> (HVect (replaceAt ind (MaybeBlockty iType) (map MaybeBlockty rInputs))) 
          ->  (HVect (map MaybeBlockty rInputs))

为了证明这一点，我试图使用一个较早证明的事实：

replaceAtProof' : (xs : Vect n a) 
           -> (i : Fin n)
           -> (f : a -> b) 
           -> ((index i xs) = x) 
           -> (replaceAt i (f x) (map f xs)) = (map f xs)

我希望简单地尝试重写 reverseAtProof' 中的适当表达式可以实现这一点，但是当尝试如下重写时：

reverseProof' inputBlock ind rInputs receiveBlock prf newInsert x = rewrite replaceAtProof' rInputs ind MaybeBlockty prf in x

我得到如下错误：

When checking right hand side of reverseProof' with expected type HVect (map MaybeBlockty rInputs)

rewriting replaceAt ind
          (Maybe (len : Nat ** tyList : Vect len Ty ** Block iType len tyList))
          (Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map MaybeBlockty rInputs) 

to 

           Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map MaybeBlockty rInputs 

did not change type HVect (Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map MaybeBlockty rInputs)

我读到这个错误说它无法应用尝试的重写，因为它无法在x 中找到指定的模式。这似乎是因为编译器减少了

的定义

MaybeBlockty iType

成为

Maybe (len : Nat ** tyList : Vect len Ty ** Block iType len tyList)

：按照MaybeBlockty的定义编辑

我有什么方法可以防止这种情况发生，以便应用给定的重写，还是我误读了给定的错误？

【问题讨论】：

您能否将代码粘贴到要点中以查看发生了什么？

标签： idris theorem-proving

【解决方案1】：

rewrite 使用提供的从左到右的相等来更改目标的类型。由于您需要它来适应 x 的类型，看起来您的重写应该朝相反的方向发展：尝试 rewrite sym $ replaceAtProof' rInputs ind MaybeBlockty prf in x

【讨论】：

谢谢！这确实是问题所在。我误解了他们申请的顺序。