CODEWITHSUNDEEP
idristheorem-proving
proverIdr
proverIdr

Reputation: 13

Difficulty applying a proof in Idris

I am attempting to prove a property over one of my defined data types as follows: 

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))

In attempting to prove this I am trying to use an earlier proved fact that:

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)

I was hoping that simply attempting to rewrite the appropriate expression in reverseAtProof' would achieve this, however when attempting to rewrite as follows:

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

I get the error as below:

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)

I read this error as saying that it could not apply the attempted rewrite as it could not find the specified pattern within x. This would appear to be because the compiler reduces the definition of 

MaybeBlockty iType

to be

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

:EDIT as is the definition of MaybeBlockty

Is there any way for me to prevent this from occurring so that the given rewrite will apply, or am I misreading the given error?

Upvotes: 1

Views: 137

Answers (1)

Alexander Gryzlov
Alexander Gryzlov

Reputation: 933

rewrite changes the type of the goal using the provided equality going from the left to the right. Since you need it to fit the type of x, it looks like your rewrite should go in the opposite direction: try rewrite sym $ replaceAtProof' rInputs ind MaybeBlockty prf in x

Upvotes: 2

Related Questions