Sec8_1_eqproof.idr

module Part2.Sec8_1_eqproof
import Data.Vect

%default total 

{- 
Returns proof that num1 and num2 are equal 

data (=) : a -> b -> Type where
     Refl : x = x 
cong : {func : a -> b} -> x = y -> func x = func y
-}
checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (num1 = num2)
checkEqNat Z Z = Just Refl
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Nothing => Nothing
                              Just prf => Just (cong prf)

{-
Notes: if the last line in defintion of exactLength is changed to
Just prf => ?hole

idris repl:
*Part2/Sec8_1_eqproof> :t hole
  a : Type
  m : Nat
  len : Nat
  prf : len = m
  input : Vect m a
--------------------------------------
hole : Maybe (Vect len a)


When last line is replaced with:
Just prf => Just input 
causes compiler error:

./Part2/Sec8_1_eqproof.idr:34:49-58:
   |
34 |                                     Just prf => Just input
   |                                                 ~~~~~~~~~~
When checking right hand side of Part2.Sec8_1_eqproof.case block in exactLength at ./Part2/Sec8_1_eqproof.idr:32:14-29 with expected type
        Maybe (Vect len a)

When checking argument x to constructor Prelude.Maybe.Just:
        Type mismatch between
                Vect m a (Type of input)
        and
                Vect len a (Expected type)
        
        Specifically:
                Type mismatch between
                        m
                and
                        len

Just prf => ?hole -- Just input

Using rewrite syntax from section 8.2 fixes the problem.
But order of len and m is important
`checkEqNat m len` would not work! (equational profs are not automatically symmetric -
sym function in 8.2)

TODO, also using Dec (section 8.3) fixes the problem, why?
This code compiles fine:

exactLength {m} len input = case decEq m len of
         Yes Refl => Just input
         No contra => Nothing
-}
exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a) 
exactLength {m} len input 
      = case checkEqNat len m of
                                    Nothing => Nothing
                                    Just prf => rewrite prf in Just input  -- syntax from 8.2

{- 
`exactLength` implementation in the book (repeated below) does not need `rewrite` syntax.
Maybe because it keeps nat value in scope (look at SameNat constructor) and is Nat sepecific. 
The need to have evidence of type/value being checked in scope seems to be important.
This relates to some of my Haskell experience (see F2 type family and solutions to example 1 and 2). 
-}

data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where
     SameNat : (num : Nat) -> EqNat num num

{- nicely generated by Idris by case splitting on third variable (eq) -}
sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS j j (SameNat j) = SameNat (S j)

checkEqNat1 : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat1 Z Z = Just (SameNat Z)
checkEqNat1 Z (S k) = Nothing
checkEqNat1 (S k) Z = Nothing
checkEqNat1 (S k) (S j) = case checkEqNat1 k j of
                              Nothing => Nothing
                              Just eq => Just (sameS _ _ eq)


{- The proof of equality allows this type of method to typecheck and
 rewrite statement is not used. -}
exactLength1 : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a) 
exactLength1 {m} len input 
      = case checkEqNat1 m len of
                                    Nothing => Nothing
                                    Just (SameNat len) => Just input

{- exercise 1, (x :) is just a function  -}
same_cons : {xs : List a} -> {ys : List a} ->
                      xs = ys -> x :: xs = x :: ys
same_cons prf = cong prf


{- exercise 2, knowing that x's are indentical, this theorem reduces to same_cons -}
same_lists : {xs : List a} -> {ys : List a} ->
                      x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl = same_cons

{- exercise 3, 4 -}
data ThreeEqual : a -> b -> c -> Type where
  Refl3 : ThreeEqual a a a

{- Idris knows that all 3 a's are the same, interstingly no need for cong -}
allSameS : (x, y, z : Nat) -> ThreeEqual x y z -> ThreeEqual (S x) (S y) (S z)
allSameS a a a Refl3 = Refl3