Created
November 23, 2025 07:12
-
-
Save SekiT/0c2e453afe707c05b8f8ed5c5b193b3f to your computer and use it in GitHub Desktop.
This file contains hidden or 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
| module BiNat | |
| import Data.Vect | |
| %default total | |
| public export | |
| data BiNat : Type where | |
| I : BiNat | |
| N0 : BiNat -> BiNat | |
| N1 : BiNat -> BiNat | |
| public export | |
| Uninhabited (I = N0 _) where | |
| uninhabited Refl impossible | |
| public export | |
| Uninhabited (N0 _ = I) where | |
| uninhabited Refl impossible | |
| public export | |
| Uninhabited (I = N1 _) where | |
| uninhabited Refl impossible | |
| public export | |
| Uninhabited (N1 _ = I) where | |
| uninhabited Refl impossible | |
| public export | |
| Uninhabited (N0 _ = N1 _) where | |
| uninhabited Refl impossible | |
| public export | |
| Uninhabited (N1 _ = N0 _) where | |
| uninhabited Refl impossible | |
| public export | |
| Eq BiNat where | |
| I == I = True | |
| I == (N0 n) = False | |
| I == (N1 n) = False | |
| (N0 m) == I = False | |
| (N0 m) == (N0 n) = m == n | |
| (N0 m) == (N1 n) = False | |
| (N1 m) == I = False | |
| (N1 m) == (N0 n) = False | |
| (N1 m) == (N1 n) = m == n | |
| public export | |
| Ord BiNat where | |
| compare I I = EQ | |
| compare I _ = LT | |
| compare (N0 m) I = GT | |
| compare (N0 m) (N0 n) = compare m n | |
| compare (N0 m) (N1 n) = case compare m n of | |
| LT => LT | |
| EQ => LT | |
| GT => GT | |
| compare (N1 m) I = GT | |
| compare (N1 m) (N0 n) = case compare m n of | |
| LT => LT | |
| EQ => GT | |
| GT => GT | |
| compare (N1 m) (N1 n) = compare m n | |
| public export | |
| data LTE : (m, n: BiNat) -> Type where | |
| LTEI : LTE I n | |
| LTERefl : (n : BiNat) -> LTE n n | |
| LTETail00 : {m, n : BiNat} -> LTE m n -> LTE (N0 m) (N0 n) | |
| LTETail01 : {m, n : BiNat} -> LTE m n -> LTE (N0 m) (N1 n) | |
| LTETail10 : {m, n : BiNat} -> LTE m n -> Not (m = n) -> LTE (N1 m) (N0 n) | |
| LTETail11 : {m, n : BiNat} -> LTE m n -> LTE (N1 m) (N1 n) | |
| public export | |
| Uninhabited (LTE (N0 _) I) where | |
| uninhabited LTEI impossible | |
| uninhabited (LTERefl _) impossible | |
| uninhabited (LTETail00 lte) impossible | |
| uninhabited (LTETail01 lte) impossible | |
| uninhabited (LTETail10 lte notEq) impossible | |
| uninhabited (LTETail11 lte) impossible | |
| public export | |
| Uninhabited (LTE (N1 _) I) where | |
| uninhabited LTEI impossible | |
| uninhabited (LTERefl _) impossible | |
| uninhabited (LTETail00 lte) impossible | |
| uninhabited (LTETail01 lte) impossible | |
| uninhabited (LTETail10 lte notEq) impossible | |
| uninhabited (LTETail11 lte) impossible | |
| lteAntisynmetric : {a, b : BiNat} -> LTE a b -> LTE b a -> a = b | |
| lteAntisynmetric (LTERefl _) _ = Refl | |
| lteAntisynmetric _ (LTERefl _) = Refl | |
| lteAntisynmetric {a = I} {b = I} LTEI LTEI = Refl | |
| lteAntisynmetric {a = I} {b = N0 b} LTEI lteBA = absurd (uninhabited lteBA) | |
| lteAntisynmetric {a = I} {b = N1 b} LTEI lteBA = absurd (uninhabited lteBA) | |
| lteAntisynmetric {a = N0 a} {b = I} lteAB LTEI = absurd (uninhabited lteAB) | |
| lteAntisynmetric {a = N0 a} {b = N0 b} (LTETail00 lteAB) (LTETail00 lteBA) = rewrite lteAntisynmetric lteAB lteBA in Refl | |
| lteAntisynmetric {a = N0 a} {b = N1 b} (LTETail01 lteAB) (LTETail10 lteBA notEq) = absurd (notEq (lteAntisynmetric lteBA lteAB)) | |
| lteAntisynmetric {a = N1 a} {b = I} lteAB LTEI = absurd (uninhabited lteAB) | |
| lteAntisynmetric {a = N1 a} {b = N0 b} (LTETail10 lteAB notEq) (LTETail01 lteBA) = absurd (notEq (lteAntisynmetric lteAB lteBA)) | |
| lteAntisynmetric {a = N1 a} {b = N1 b} (LTETail11 lteAB) (LTETail11 lteBA) = rewrite lteAntisynmetric lteAB lteBA in Refl | |
| lteTransitive : {a, b, c : BiNat} -> LTE a b -> LTE b c -> LTE a c | |
| lteTransitive {a = I} LTEI _ = LTEI | |
| lteTransitive {a} {b = a} {c} (LTERefl _) lteBC = lteBC | |
| lteTransitive {a = N0 a} {b = N0 b} {c = N0 b} (LTETail00 lteAB) (LTERefl _) = LTETail00 lteAB | |
| lteTransitive {a = N0 a} {b = N0 b} {c = N0 c} (LTETail00 lteAB) (LTETail00 lteBC) = LTETail00 (lteTransitive lteAB lteBC) | |
| lteTransitive {a = N0 a} {b = N0 b} {c = N1 c} (LTETail00 lteAB) (LTETail01 lteBC) = LTETail01 (lteTransitive lteAB lteBC) | |
| lteTransitive {a = N0 a} {b = N1 b} {c = N1 b} (LTETail01 lteAB) (LTERefl _) = LTETail01 lteAB | |
| lteTransitive {a = N0 a} {b = N1 b} {c = N0 c} (LTETail01 lteAB) (LTETail10 lteBC notEq) = LTETail00 (lteTransitive lteAB lteBC) | |
| lteTransitive {a = N0 a} {b = N1 b} {c = N1 c} (LTETail01 lteAB) (LTETail11 lteBC) = LTETail01 (lteTransitive lteAB lteBC) | |
| lteTransitive {a = N1 a} {b = N0 b} {c = N0 b} (LTETail10 lteAB notEq) (LTERefl (N0 _)) = LTETail10 lteAB notEq | |
| lteTransitive {a = N1 a} {b = N0 b} {c = N0 c} (LTETail10 lteAB notEq) (LTETail00 lteBC) = | |
| let acNotEq = \eq => notEq (lteAntisynmetric lteAB (replace {p = \x => LTE b x} (sym eq) lteBC)) in | |
| LTETail10 (lteTransitive lteAB lteBC) acNotEq | |
| lteTransitive {a = N1 a} {b = N0 b} {c = N1 c} (LTETail10 lteAB notEq) (LTETail01 lteBC) = LTETail11 (lteTransitive lteAB lteBC) | |
| lteTransitive {a = N1 a} {b = N1 b} {c = N0 c} (LTETail11 lteAB) (LTETail10 lteBC notEq) = | |
| let acNotEq = \eq => notEq (lteAntisynmetric lteBC (replace {p = \x => LTE x b} eq lteAB)) in | |
| LTETail10 (lteTransitive lteAB lteBC) acNotEq | |
| lteTransitive {a = N1 a} {b = N1 b} {c = N1 b} (LTETail11 lteAB) (LTERefl _) = LTETail11 lteAB | |
| lteTransitive {a = N1 a} {b = N1 b} {c = N1 c} (LTETail11 lteAB) (LTETail11 lteBC) = LTETail11 (lteTransitive lteAB lteBC) | |
| data LT : BiNat -> BiNat -> Type where | |
| LTC : {m, n : BiNat} -> LTE m n -> Not (m = n) -> LT m n | |
| ltTransitive : {a, b, c : BiNat} -> LT a b -> LT b c -> LT a c | |
| ltTransitive {a} {b} {c} (LTC lteAB notEqAB) (LTC lteBC notEqBC) = | |
| let lteAC = lteTransitive lteAB lteBC in | |
| let notEqAC = \eq => notEqAB (lteAntisynmetric lteAB (replace {p = \x => LTE b x} eq lteBC)) in | |
| LTC lteAC (\eq => notEqAC (sym eq)) | |
| public export | |
| succ : BiNat -> BiNat | |
| succ I = N0 I | |
| succ (N0 n) = N1 n | |
| succ (N1 n) = N0 (succ n) | |
| public export | |
| pred : BiNat -> BiNat | |
| pred I = I | |
| pred (N0 I) = I | |
| pred (N0 (N0 n)) = N1 (pred (N0 n)) | |
| pred (N0 (N1 n)) = N1 (N0 n) | |
| pred (N1 n) = N0 n | |
| succNotI : (n : BiNat) -> Not (succ n = I) | |
| succNotI I prf impossible | |
| succNotI (N0 n) prf impossible | |
| succNotI (N1 n) prf impossible | |
| succNotEq : (n : BiNat) -> Not (n = succ n) | |
| succNotEq I prf impossible | |
| succNotEq (N0 n) prf impossible | |
| succNotEq (N1 n) prf impossible | |
| N0Injective : (m, n : BiNat) -> N0 m = N0 n -> m = n | |
| N0Injective m n prf = case prf of Refl => Refl | |
| N1Injective : (m, n : BiNat) -> N1 m = N1 n -> m = n | |
| N1Injective m n prf = case prf of Refl => Refl | |
| succInjective : (m, n : BiNat) -> succ m = succ n -> m = n | |
| succInjective I I Refl = Refl | |
| succInjective I (N0 n) prf impossible | |
| succInjective I (N1 n) prf = absurd $ succNotI n (sym $ N0Injective I (succ n) prf) | |
| succInjective (N0 m) I prf impossible | |
| succInjective (N0 m) (N0 n) prf = rewrite N1Injective m n prf in Refl | |
| succInjective (N0 m) (N1 n) prf impossible | |
| succInjective (N1 m) I prf = absurd $ succNotI m (N0Injective (succ m) I prf) | |
| succInjective (N1 m) (N0 n) prf impossible | |
| succInjective (N1 m) (N1 n) prf = rewrite succInjective m n (N0Injective (succ m) (succ n) prf) in Refl | |
| predOfSucc : (n : BiNat) -> pred (succ n) = n | |
| predOfSucc I = Refl | |
| predOfSucc (N0 n) = Refl | |
| predOfSucc (N1 I) = Refl | |
| predOfSucc (N1 (N0 n)) = Refl | |
| predOfSucc (N1 (N1 I)) = Refl | |
| predOfSucc (N1 (N1 (N0 n))) = Refl | |
| predOfSucc (N1 (N1 (N1 n))) = rewrite predOfSucc (N1 n) in Refl | |
| succOfPred : (n : BiNat) -> Not (n = I) -> succ (pred n) = n | |
| succOfPred I notI = absurd (notI Refl) | |
| succOfPred (N0 I) _ = Refl | |
| succOfPred (N0 (N0 n)) _ = rewrite succOfPred (N0 n) uninhabited in Refl | |
| succOfPred (N0 (N1 n)) _ = Refl | |
| succOfPred (N1 n) _ = Refl | |
| public export | |
| plus : BiNat -> BiNat -> BiNat | |
| plus I n = succ n | |
| plus (N0 m) I = N1 m | |
| plus (N0 m) (N0 n) = N0 (plus m n) | |
| plus (N0 m) (N1 n) = N1 (plus m n) | |
| plus (N1 m) I = N0 (succ m) | |
| plus (N1 m) (N0 n) = N1 (plus m n) | |
| plus (N1 m) (N1 n) = N0 (succ (plus m n)) | |
| plusCommutes : (m, n : BiNat) -> plus m n = plus n m | |
| plusCommutes I I = Refl | |
| plusCommutes I (N0 n) = Refl | |
| plusCommutes I (N1 n) = Refl | |
| plusCommutes (N0 m) I = Refl | |
| plusCommutes (N0 m) (N0 n) = rewrite plusCommutes m n in Refl | |
| plusCommutes (N0 m) (N1 n) = rewrite plusCommutes m n in Refl | |
| plusCommutes (N1 m) I = Refl | |
| plusCommutes (N1 m) (N0 n) = rewrite plusCommutes m n in Refl | |
| plusCommutes (N1 m) (N1 n) = rewrite plusCommutes m n in Refl | |
| plusISucc : (n : BiNat) -> plus n I = succ n | |
| plusISucc n = rewrite plusCommutes I n in Refl | |
| plusBySucc : (m, n : BiNat) -> plus m (succ n) = succ (plus m n) | |
| plusBySucc I n = Refl | |
| plusBySucc (N0 m) I = rewrite plusISucc m in Refl | |
| plusBySucc (N0 m) (N0 n) = Refl | |
| plusBySucc (N0 m) (N1 n) = rewrite plusBySucc m n in Refl | |
| plusBySucc (N1 m) I = rewrite plusISucc m in Refl | |
| plusBySucc (N1 m) (N0 n) = Refl | |
| plusBySucc (N1 m) (N1 n) = rewrite plusBySucc m n in Refl | |
| n0IsDouble : (n : BiNat) -> N0 n = plus n n | |
| n0IsDouble I = Refl | |
| n0IsDouble (N0 n) = rewrite n0IsDouble n in Refl | |
| n0IsDouble (N1 n) = rewrite sym $ n0IsDouble n in Refl | |
| plusAssociative : (a, b, c : BiNat) -> plus (plus a b) c = plus a (plus b c) | |
| plusAssociative I b c = | |
| rewrite plusCommutes (succ b) c in | |
| rewrite plusCommutes b c in | |
| plusBySucc c b | |
| plusAssociative (N0 a) b c = | |
| rewrite n0IsDouble a in | |
| rewrite plusAssociative a a b in | |
| rewrite plusAssociative a (plus a b) c in | |
| rewrite plusAssociative a a (plus b c) in | |
| rewrite plusAssociative a b c in Refl | |
| plusAssociative (N1 a) b c = | |
| rewrite plusCommutes (N1 a) b in | |
| rewrite plusBySucc b (N0 a) in | |
| rewrite plusCommutes (succ (plus b (N0 a))) c in | |
| rewrite plusBySucc c (plus b (N0 a)) in | |
| rewrite plusCommutes (N1 a) (plus b c) in | |
| rewrite plusBySucc (plus b c) (N0 a) in | |
| rewrite plusCommutes b c in | |
| rewrite n0IsDouble a in | |
| rewrite plusCommutes b (plus a a) in | |
| rewrite plusAssociative a a b in | |
| rewrite plusCommutes c (plus a (plus a b)) in | |
| rewrite plusCommutes (plus c b) (plus a a) in | |
| rewrite plusCommutes c b in | |
| rewrite plusAssociative a a (plus b c) in | |
| rewrite sym $ plusAssociative a b c in | |
| rewrite plusAssociative a (plus a b) c in Refl | |
| composeFunctions : {T : BiNat -> Type} -> | |
| ((k : BiNat) -> T k -> T (succ k)) -> | |
| (m, n : BiNat) -> T m -> T (plus m n) | |
| composeFunctions f m I pm = rewrite plusISucc m in f m pm | |
| composeFunctions f m (N0 n) pm = | |
| rewrite n0IsDouble n in | |
| rewrite sym $ plusAssociative m n n in | |
| let pmn = composeFunctions f m n pm in | |
| composeFunctions f (plus m n) n pmn | |
| composeFunctions f m (N1 n) pm = | |
| rewrite plusBySucc m (N0 n) in | |
| rewrite n0IsDouble n in | |
| rewrite sym $ plusAssociative m n n in | |
| let pmn = composeFunctions f m n pm in | |
| let pmnn = composeFunctions f (plus m n) n pmn in | |
| f (plus (plus m n) n) pmnn | |
| public export | |
| induction : {P : BiNat -> Type} -> | |
| P I -> | |
| ((n : BiNat) -> P n -> P (succ n)) -> | |
| (n : BiNat) -> P n | |
| induction pI pSucc I = pI | |
| induction pI pSucc (N0 n) = | |
| rewrite n0IsDouble n in | |
| composeFunctions pSucc n n (induction pI pSucc n) | |
| induction pI pSucc (N1 n) = | |
| let l1 = composeFunctions pSucc n n (induction pI pSucc n) in | |
| let l2 = replace {p = P} (sym $ n0IsDouble n) l1 in | |
| pSucc (N0 n) l2 | |
| lteFromLt : {m, n : BiNat} -> LT m n -> LTE m n | |
| lteFromLt (LTC lte notEq) = lte | |
| ltSucc : (n : BiNat) -> LT n (succ n) | |
| ltSucc I = LTC LTEI (\eq => absurd (uninhabited eq)) | |
| ltSucc (N0 n) = LTC (LTETail01 (LTERefl n)) uninhabited | |
| ltSucc (N1 n) = LTC (LTETail10 (lteFromLt (ltSucc n)) (succNotEq n)) uninhabited | |
| plusLt : (m, n : BiNat) -> LT m (plus m n) | |
| plusLt m I = rewrite plusISucc m in ltSucc m | |
| plusLt m (N0 n) = | |
| rewrite n0IsDouble n in | |
| rewrite sym $ plusAssociative m n n in | |
| ltTransitive (plusLt m n) (plusLt (plus m n) n) | |
| plusLt m (N1 n) = | |
| rewrite plusBySucc m (N0 n) in | |
| rewrite n0IsDouble n in | |
| rewrite sym $ plusAssociative m n n in | |
| let l1 = ltTransitive (plusLt m n) (plusLt (plus m n) n) in | |
| ltTransitive l1 (ltSucc _) | |
| succPlusLeft : (m, n : BiNat) -> succ (plus m n) = plus (succ m) n | |
| succPlusLeft m n = | |
| rewrite plusCommutes (succ m) n in | |
| rewrite plusBySucc n m in | |
| rewrite plusCommutes m n in Refl | |
| complement : (m, n : BiNat) -> LT m n -> (k : BiNat ** plus m k = n) | |
| complement = induction | |
| {P = \m => (n : BiNat) -> LT m n -> (k : BiNat ** plus m k = n)} | |
| (\n => \(LTC _ notEq) => (pred n ** rewrite succOfPred n (\x => notEq (sym x)) in Refl)) | |
| $ \m, pm, n, lt => | |
| let lt2 = ltTransitive (ltSucc m) lt in | |
| let (k ** eq) = pm n lt2 in | |
| case k of | |
| I => case lt of LTC _ notEq => absurd (notEq (replace {p = \x => x = n} (plusISucc m) eq)) | |
| N0 I => | |
| let eq2 = replace {p = \x => x = n} (plusBySucc m I) eq in | |
| let eq3 = replace {p = \x => x = n} (succPlusLeft m I) eq2 in | |
| (I ** eq3) | |
| N0 (N0 k2) => | |
| let eq2 = replace {p = \x => plus m x = n} (sym $ succOfPred (N0 (N0 k2)) uninhabited) eq in | |
| let eq3 = replace {p = \x => x = n} (plusBySucc m (N1 (pred (N0 k2)))) eq2 in | |
| let eq4 = replace {p = \x => x = n} (succPlusLeft m (N1 (pred (N0 k2)))) eq3 in | |
| (N1 (pred (N0 k2)) ** eq4) | |
| N0 (N1 k2) => | |
| let eq2 = replace {p = \x => x = n} (plusBySucc m (N1 (N0 k2))) eq in | |
| let eq3 = replace {p = \x => x = n} (succPlusLeft m (N1 (N0 k2))) eq2 in | |
| (N1 (N0 k2) ** eq3) | |
| N1 k2 => | |
| let eq2 = replace {p = \x => x = n} (plusBySucc m (N0 k2)) eq in | |
| let eq3 = replace {p = \x => x = n} (succPlusLeft m (N0 k2)) eq2 in | |
| (N0 k2 ** eq3) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment