a-conjecture-of-mine

An exercise on polyglossy: the same problem solved on multiple languages

git clone: git://git.pablopie.xyz/a-conjecture-of-mine
Log
Files
Refs

Commit: 1554a98150bf64df0e10dadd4f991f17925d31f5
Parent: 81a611cfe7ffa7a6499e18eb8961645378a76527
Author: Pablo Escobar Gaviria <gark.garcia@protonmail.com>
Date: Sun, 2 Feb 2020 08:25:03 -0200

Removed the Idris implementation from the repo, sice it is far from complete.

Diffstat

3 files changed, 0 insertions, 222 deletions

Status	File Name	N° Changes	Insertions	Deletions
Deleted	Idris/Data/Map.ibc	0	0	0
Deleted	Idris/Data/Map.idr	149	0	149
Deleted	Idris/Main.idr	73	0	73

diff --git a/Idris/Data/Map.ibc b/Idris/Data/Map.ibc
Binary files differ.

diff --git a/Idris/Data/Map.idr b/Idris/Data/Map.idr
@@ -1,149 +0,0 @@
-module Data.Map
-
-public export
-data Map k a = Bin Nat k a (Map k a) (Map k a)
-             | Tip
-
-implementation Sized (Map k a) where
-  size (Bin s _ _ _ _) = s
-  size Tip = 0
-
-ratio : Nat
-ratio = 2
-
-delta : Nat
-delta = 3
-
-raise : String -> Map k v
-raise _ = ?undefined
-
--- | /O(1)/. The empty map.
-public export
-empty : Map k a
-empty = Tip
-
--- | /O(1)/. A map with a single element.
---
--- > singleton 1 'a'        == fromList [(1, 'a')]
--- > size (singleton 1 'a') == 1
-public export
-singleton : k -> a -> Map k a
-singleton k x = Bin 1 k x Tip Tip
-
--- balanceL is called when left subtree might have been inserted to or when
--- right subtree might have been deleted from.
-balanceL : k -> a -> Map k a -> Map k a -> Map k a
-balanceL k x l r = 
-  case r of
-    Tip =>
-      case l of
-        Tip => Bin 1 k x Tip Tip
-        (Bin _ _ _ Tip Tip) => Bin 2 k x l Tip
-        (Bin _ lk lx Tip (Bin _ lrk lrx _ _)) => Bin 3 lrk lrx (Bin 1 lk lx Tip Tip) (Bin 1 k x Tip Tip)
-        (Bin _ lk lx ll@(Bin _ _ _ _ _) Tip) => Bin 3 lk lx ll (Bin 1 k x Tip Tip)
-        (Bin ls lk lx ll@(Bin lls _ _ _ _) lr@(Bin lrs lrk lrx lrl lrr)) =>
-          if lrs < ratio*lls 
-            then Bin (1+ls) lk lx ll (Bin (1+lrs) k x lr Tip)
-            else Bin (1+ls) lrk lrx (Bin (1+lls+size lrl) lk lx ll lrl) (Bin (1+size lrr) k x lrr Tip)
-
-    (Bin rs _ _ _ _) =>
-      case l of
-        Tip => Bin (1+rs) k x Tip r
-        (Bin ls lk lx ll lr) =>
-          if ls > delta*rs
-            then case (ll, lr) of
-              (Bin lls _ _ _ _, Bin lrs lrk lrx lrl lrr) =>
-                if lrs < ratio*lls
-                  then Bin (1+ls+rs) lk lx ll (Bin (1+rs+lrs) k x lr r)
-                  else Bin (1+ls+rs) lrk lrx (Bin (1+lls+size lrl) lk lx ll lrl) (Bin (1+rs+size lrr) k x lrr r)
-              (_, _) => raise "Failure in Data.Map.balanceL"
-            else Bin (1+ls+rs) k x l r
-
--- balanceR is called when right subtree might have been inserted to or when
--- left subtree might have been deleted from.
-balanceR : k -> a -> Map k a -> Map k a -> Map k a
-balanceR k x l r =
-  case l of
-    Tip =>
-      case r of
-        Tip => Bin 1 k x Tip Tip
-        (Bin _ _ _ Tip Tip) => Bin 2 k x Tip r
-        (Bin _ rk rx Tip rr@(Bin _ _ _ _ _)) => Bin 3 rk rx (Bin 1 k x Tip Tip) rr
-        (Bin _ rk rx (Bin _ rlk rlx _ _) Tip) => Bin 3 rlk rlx (Bin 1 k x Tip Tip) (Bin 1 rk rx Tip Tip)
-        (Bin rs rk rx rl@(Bin rls rlk rlx rll rlr) rr@(Bin rrs _ _ _ _)) =>
-          if rls < ratio*rrs
-            then Bin (1+rs) rk rx (Bin (1+rls) k x Tip rl) rr
-            else Bin (1+rs) rlk rlx (Bin (1+size rll) k x Tip rll) (Bin (1+rrs+size rlr) rk rx rlr rr)
-    (Bin ls _ _ _ _) =>
-      case r of
-        Tip => Bin (1+ls) k x l Tip
-        (Bin rs rk rx rl rr) =>
-          if rs > delta*ls
-            then case (rl, rr) of
-              (Bin rls rlk rlx rll rlr, Bin rrs _ _ _ _) =>
-                if  rls < ratio*rrs 
-                  then Bin (1+ls+rs) rk rx (Bin (1+ls+rls) k x l rl) rr
-                  else Bin (1+ls+rs) rlk rlx (Bin (1+ls+size rll) k x l rll) (Bin (1+rrs+size rlr) rk rx rlr rr)
-              (_, _) => raise "Failure in Data.Map.balanceR"
-            else Bin (1+ls+rs) k x l r
-
-
--- | /O(log n)/. Insert a new key and value in the map.
--- If the key is already present in the map, the associated value is
--- replaced with the supplied value. 'insert' is equivalent to
--- @'insertWith' 'const'@.
---
--- > insert 5 'x' (fromList [(5,'a'), (3,'b')]) == fromList [(3, 'b'), (5, 'x')]
--- > insert 7 'x' (fromList [(5,'a'), (3,'b')]) == fromList [(3, 'b'), (5, 'a'), (7, 'x')]
--- > insert 5 'x' empty                         == singleton 5 'x'
---
--- See Map.Internal.Note: Type of local 'go' function
-public export
-insert : Ord k => k -> a -> Map k a -> Map k a
-insert = go where
-  go : Ord k => k -> a -> Map k a -> Map k a
-  go kx x Tip = singleton kx x
-  go kx x (Bin sz ky y l r) =
-    case compare kx ky of
-      LT => balanceL ky y (go kx x l) r
-      GT => balanceR ky y l (go kx x r)
-      EQ => Bin sz kx x l r
-
--- | /O(log n)/. Lookup the value at a key in the map.
---
--- The function will return the corresponding value as @('Just' value)@,
--- or 'Nothing' if the key isn't in the map.
---
--- An example of using @lookup@:
---
--- > import Prelude hiding (lookup)
--- > import Data.Map
--- >
--- > employeeDept = fromList([("John","Sales"), ("Bob","IT")])
--- > deptCountry = fromList([("IT","USA"), ("Sales","France")])
--- > countryCurrency = fromList([("USA", "Dollar"), ("France", "Euro")])
--- >
--- > employeeCurrency : String -> Maybe String
--- > employeeCurrency name = do
--- >     dept <- lookup name employeeDept
--- >     country <- lookup dept deptCountry
--- >     lookup country countryCurrency
--- >
--- > main = do
--- >     putStrLn $ "John's currency: " ++ (show (employeeCurrency "John"))
--- >     putStrLn $ "Pete's currency: " ++ (show (employeeCurrency "Pete"))
---
--- The output of this program:
---
--- >   John's currency: Just "Euro"
--- >   Pete's currency: Nothing
-public export
-lookup : Ord k => k -> Map k a -> Maybe a
-lookup = go where
-  go _ Tip = Nothing
-  go k (Bin _ kx x l r) =
-    case compare k kx of
-      LT => go k l
-      GT => go k r
-      EQ => Just x
-

diff --git a/Idris/Main.idr b/Idris/Main.idr
@@ -1,73 +0,0 @@
--- The following program is a simple test for the following conjecture:
-
--- Let S: N -> N be the sum of the digits of a positive integer.
--- For all A and B in N, S(A + B) = S(A) + S(B) - 9k, where k is an integer.
-
-module Main
-
-import System
-
-main : IO Int
-main = do
-    args <- getArgs
-        
-    case readDec <$> head' args of
-      Just [(max, "")] =>
-        if counter' max then exitFailure else exitSuccess
-      _ => exitInvalidInput
-      
-    where
-      head' : List a -> Maybe a
-      head' [] = Nothing
-      head' xs = Just (head xs)
-
--- Calculates the sum of the digits of `n`.
-sum' : Nat -> Int
-sum' n
-     | n < 10 = fromEnum n
-     | otherwise = fromEnum (n `mod` 10) + sum' (n `div` 10)
-
--- Returns `Just updated` if the if the conjecture holds for pair, where
--- `updated` is an updated versions of the sums cache provided by `sums`.
--- Otherwise returns `Nothing`.
-test' : Map Nat Int -> (Nat, Nat) -> Maybe (Map Nat Int)
-test' sums pair =
-    case diff sums pair of
-        Left updated =>
-            test' updated pair
-
-        Right dif =>
-            if dif `mod` 9 == 0 then Just sums else Nothing
-
--- Given a cache of the image of `sum'`, attemps to lookup `sum' a`, `sum' b`
--- and `sum' $ a + b`.
--- If the lookup succeeds, returns `Right (sum' (a + b) - sum' a - sum' a)`.
--- Otherwise inserts the value that caused the failure to `sums` and returns
--- `Left sums`.
-diff : Map Nat Int -> (Nat, Nat) -> Either (Map Nat Int) Int
-diff sums (a, b) = do
-    sa  <- lookupOrInsert a
-    sb  <- lookupOrInsert b
-    sab <- lookupOrInsert $ a + b
-
-    return $ sab - sa - sb
-    where lookupOrInsert x =
-            case Data.Map.lookup x sums of
-                Just sx => Right sx
-                
-                Nothing => Left (insert x (sum' x) sums)
-
--- Checks if there is any counterexample in
--- [(a, b) | a <- [0..max], b <- [a..max]].
---
--- Returns `True` if a counter example was found.
--- Otherwise returns `False`.
-counter' : Nat -> Bool
-counter' max =
-    case foldM test' empty [(a, b) | a <- [0..max], b <- [a..max]] of
-        Nothing => True
-        Just _  => False
-
-exitInvalidInput : IO Int
-exitInvalidInput = exitWith $ ExitFailure 2
-