# a-conjecture-of-mine

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

```commit ff512183d5897c369c0366bb77e4077a0db0057e
Author: Pablo Escobar Gaviria <gark.garcia@protonmail.com>
Date:   Fri, 14 Feb 2020 21:28:14 -0200

Diffstat:
M.gitignore | 1-
D.stack-work/install/x86_64-linux-nopie/ghc-8.0.2/8.0.2/pkgdb/package.cache | 0
MC++/main.cpp | 2+-
DExtra/brainfuck/main.bf | 22----------------------
AIdris/Main.idr | 58++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

5 files changed, 59 insertions(+), 24 deletions(-)
```
```diff --git a/.gitignore b/.gitignore
@@ -12,4 +12,3 @@ build
*.hi
Latex
Cuda
-Idris
diff --git a/.stack-work/install/x86_64-linux-nopie/ghc-8.0.2/8.0.2/pkgdb/package.cache b/.stack-work/install/x86_64-linux-nopie/ghc-8.0.2/8.0.2/pkgdb/package.cache
Binary files differ.
diff --git a/C++/main.cpp b/C++/main.cpp
@@ -4,7 +4,7 @@
#include <map>
#include <vector>
-#include <charconv>
+//#include <charconv>

#define SUCCESS 0
#define FAIL 1
diff --git a/Extra/brainfuck/main.bf b/Extra/brainfuck/main.bf
@@ -1,22 +0,0 @@
-[This script 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 interger.]
-
-[The value of `a` is stored in `#1`]
-[The value of `b` is stored in `#2`]
-[The value of `c` is stored in `#3`]
-[The adress `#4` is used as a temporara variable]
->[
-    Copy the value of `a` to `b`
-    >>>[-]
-    <<[-]
-    <[>+>>+<<<-]
-    >>>[<<<+>>>-]
-
-    [
-       I give up
-    ]
-    -
-]
-
diff --git a/Idris/Main.idr b/Idris/Main.idr
@@ -0,0 +1,58 @@
+-- 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
+
+data Every : (Nat -> Type) -> Nat -> Type  where
+    Base :  {P : Nat -> Type} -> Every P Z
+    Succ :  (n : Nat)
+         -> {P : Nat -> Type}
+         -> Every P n
+         -> P (S n)
+         -> Every P (S n)
+
+head' : List a -> Maybe a
+head' (x :: _) = Just x
+
+readDec : String -> List (Nat, String)
+
+main : IO Int
+main = do
+    args <- getArgs
+
+        Just [(max, "")] =>
+            if counter' max then exitFailure else exitSuccess
+        _ =>
+            exitInvalidInput
+
+-- Calculates the sum of the digits of `n`.
+sumDigits : Nat -> Int
+sumDigits = sumDigitsTail 0
+    where
+        sumDigitsTail : Int -> Nat -> Int
+        sumDigitsTail acc Z = acc
+        sumDegitsTail acc n = sumDigitsTail (acc + fromEnum n `mod` 10)
+                                            (n `div` 10)
+
+diff : Nat -> Nat -> Int
+diff a b = (sumDigits (a + b) - sumDigits a - sumDigits b) `mod` 9
+
+-- TODO: Prove this
+test : Nat -> Nat -> diff a b = 0
+test = ?test
+
+iter : (a : Nat) -> Every (test a) a
+iter Z = Base (test a)
+iter (S b) = Succ n (test b) (iter b) (test a b)
+
+conjecture : (max : Nat) -> Every iter max
+conjecture Z = Base iter
+conjecture (S a) = Succ a iter (conjecture a) (iter a)
+
```