43 lines
1.1 KiB
Idris
43 lines
1.1 KiB
Idris
module HomeworkEleven
|
|
%default total
|
|
|
|
data Move = Up | Rgt | Seq Move Move | Rev Move
|
|
|
|
Vec : Type
|
|
Vec = (Int, Int)
|
|
|
|
add : Vec -> Vec -> Vec
|
|
add (x1, y1) (x2, y2) = (x1+x2, y1+y2)
|
|
|
|
neg : Vec -> Vec
|
|
neg (x1, y1) = (negate x1, negate y1)
|
|
|
|
sem : Move -> Vec
|
|
sem Up = (0, 1)
|
|
sem Rgt = (1, 0)
|
|
sem (Seq s1 s2) = sem s1 `add` sem s2
|
|
sem (Rev s1) = neg $ sem s1
|
|
|
|
data Final : Move -> Vec -> Type where
|
|
FUp : Final Up (0, 1)
|
|
FRgt : Final Rgt (1, 0)
|
|
FSeq : Final s1 v1 -> Final s2 v2 -> Final (Seq s1 s2) (v1 `add` v2)
|
|
FRev : Final s v -> Final (Rev s) (neg v)
|
|
|
|
finalEx : Final ((Up `Seq` Up) `Seq` Rgt) (1, 2)
|
|
finalEx = (FUp `FSeq` FUp) `FSeq` FRgt
|
|
|
|
finalSem : Final s v -> sem s = v
|
|
finalSem FUp = Refl
|
|
finalSem FRgt = Refl
|
|
finalSem (FRev f) with (finalSem f) | Refl = Refl
|
|
finalSem (FSeq f1 f2) with (finalSem f1, finalSem f2) | (Refl, Refl) = Refl
|
|
|
|
semFinal : sem s = v -> Final s v
|
|
semFinal {s=Up} Refl = FUp
|
|
semFinal {s=Rgt} Refl = FRgt
|
|
semFinal {s=Rev s1} Refl with (sem s1) proof p1
|
|
| _ = FRev (semFinal (sym p1))
|
|
semFinal {s=Seq s1 s2} Refl with (sem s1, sem s2) proof p
|
|
| (_, _) = let Refl = p in FSeq (semFinal Refl) (semFinal Refl)
|