難度在伊德里斯

我試圖在我的定義的數據類型中的一種證明屬性如下應用證明：難度在伊德里斯

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

的定義是有沒有辦法對我來說，防止這種發生這種情況，以便重寫將會生效，還是我誤解了給定的錯誤？

來源

2017-09-11 proverIdr

你可以粘貼代碼的要點，以查看發生了什麼？ –

rewrite使用提供的從左到右的等式來更改目標的類型。既然你需要它來適應x的類型，它看起來像你的重寫應該是在相反的方向：嘗試rewrite sym $ replaceAtProof' rInputs ind MaybeBlockty prf in x

來源

2017-09-11 22:49:05

謝謝！那確實是問題所在。我誤解了他們申請的順序。 – proverIdr

難度在伊德里斯

回答

相關問題