Last active
October 13, 2017 07:26
-
-
Save Axure/cb7db8f3ce7a6258bc896c2d86a1a199 to your computer and use it in GitHub Desktop.
Idris Question
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| %hide Prelude.Interfaces.(<=) | |
| data Peano : Type where | |
| O: Peano | |
| (++): Peano -> Peano | |
| total | |
| (+): Peano -> Peano -> Peano | |
| (+) O x = x | |
| (+) ((++)x) y = (++)(x + y) | |
| total | |
| unitRight: (x: Peano) -> x + O = x | |
| unitRight O = Refl | |
| unitRight ((++) x) = rewrite unitRight x in | |
| Refl | |
| data (<=): (x, y: Peano) -> Type where | |
| OLte: (x: Peano) -> O <= x | |
| SLte: x <= y -> ((++)x) <= ((++)y) | |
| total | |
| self: (x: Peano) -> x <= x | |
| self O = OLte O | |
| self ((++)n) = SLte (self n) | |
| total | |
| totalMinus: y <= x -> Peano | |
| totalMinus lteProof = case lteProof of | |
| (OLte x) => x | |
| (SLte prevProof) => totalMinus prevProof | |
| total | |
| onlyZero: x <= O -> x = O | |
| onlyZero lteProof = case lteProof of | |
| OLte O => Refl | |
| total | |
| getFirst: (x <= y) -> Peano | |
| getFirst OLte = O | |
| getFirst (SLte prevLteProof) = (++)(getFirst prevLteProof) | |
| total | |
| getSecond: (x <= y) -> Peano | |
| getSecond (OLte y) = y | |
| getSecond (SLte prevLteProof) = (++)(getSecond prevLteProof) | |
| total | |
| getSecondEq: (xLteY: x <= y) -> getSecond xLteY = y | |
| getSecondEq (OLte y) = Refl | |
| getSecondEq (SLte prevLteProof) = rewrite getSecondEq prevLteProof in Refl | |
| total | |
| subst: x = y -> y <= z -> x <= z | |
| subst xEqY yLteZ = rewrite xEqY in yLteZ | |
| total | |
| subst2: z = y -> x <= y -> x <= z | |
| subst2 yEqZ xLteY = rewrite yEqZ in xLteY | |
| total | |
| trans: x <= y -> y <= z -> x <= z | |
| trans (OLte yMinusX) yLteZ = | |
| let second = getSecond yLteZ | |
| secondEqZ = getSecondEq yLteZ | |
| in subst2 (sym secondEqZ) (OLte second) | |
| trans (SLte prevXY) (SLte prevYZ) = SLte (trans prevXY prevYZ) | |
| data Result target another = Yes target | No another | |
| total | |
| ten: Peano | |
| ten = (++)((++)((++)((++)((++)((++)((++)((++)((++)((++)(O)))))))))) | |
| total | |
| eleven: Peano | |
| eleven = (++)ten | |
| total | |
| hundred: Peano | |
| hundred = (++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)(O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | |
| total | |
| hundredOne: Peano | |
| hundredOne = (++)hundred | |
| total | |
| ninety: Peano | |
| ninety = (++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)((++)(O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | |
| total | |
| ninetyOne: Peano | |
| ninetyOne = (++)ninety | |
| total | |
| isLte: (x, y: Peano) -> Result (x <= y) ((++)y <= x) | |
| isLte O x = Yes (OLte x) | |
| isLte ((++)x) O = No (SLte (OLte x)) | |
| isLte ((++)x) ((++)y) = case isLte x y of | |
| No revLteProof => No (SLte revLteProof) | |
| Yes lteProof => Yes (SLte lteProof) | |
| total | |
| tenLteHundred: Main.ten <= Main.hundred | |
| tenLteHundred = SLte (SLte (SLte (SLte (SLte (SLte (SLte (SLte (SLte (SLte (OLte ninety)))))))))) | |
| total | |
| tenLteHundredOne: Main.ten <= Main.hundredOne | |
| tenLteHundredOne = SLte (SLte (SLte (SLte (SLte (SLte (SLte (SLte (SLte (SLte (OLte ninetyOne)))))))))) | |
| -- ======= Working proof ======== | |
| total | |
| f: Nat -> Nat | |
| f x = if x > 10 then 1 else 2 | |
| total | |
| proofOfF: x = 5 -> f x = 2 | |
| proofOfF eq = rewrite eq in Refl | |
| -- total | |
| mcCarthy: Peano -> Peano | |
| mcCarthy n = case n `isLte` Main.hundred of | |
| No hundredOneLteN => totalMinus (trans tenLteHundredOne hundredOneLteN) | |
| Yes lteProof => mcCarthy (mcCarthy (n + Main.eleven)) | |
| total | |
| literalCorrectness: (Main.(++))Main.ten = Main.eleven | |
| literalCorrectness= Refl | |
| mcCarthyIdentity2: (hundredOneLteX: Main.hundredOne <= x) -> mcCarthy x = totalMinus (trans Main.tenLteHundredOne hundredOneLteX) | |
| -- mcCarthyIdentity2 hndredOneLteX = Refl | |
| mcCarthyIdentity: n <= Main.hundred -> mcCarthy x = Main.ninetyOne | |
| -- mcCarthyIdentity nLteHundred = case getFirst nLteHundred of | |
| -- hundred => Refl |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment