Compiler Explorer

Source code

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MonoLocalBinds #-}

import Data.Kind(Type)

-- I want to axiomatically state that type "Nat" (natural numbers) exists
data Nat :: Type where

-- Then I want to axiomatically state that "z" (zero) of type "Nat" exists
type family Z :: Nat

-- Same for "n" (next)
type family N :: Nat -> Nat

-- Then I want to axiomatically state induction axiom. Namely:
-- if some property "p" holds for "z" and for every "x" we have "p x -> p (n x)",
-- then "p" holds for all "x"
ind :: (forall (p :: Nat -> Type).

-- If "p" holds for "z" ...
  p Z ->

-- and for every "x" we have "p x -> p (n x)", ...
  (forall (x :: Nat). p x -> p (N x)) ->

-- then "p" holds for all "x"
  (forall (x :: Nat). p x)
  )
ind = undefined

-- Equality
data Equal :: Nat -> Nat -> Type where

-- Axioms of equality

refl :: Equal a a
refl = undefined

sym :: Equal a b -> Equal b a
sym = undefined

trans :: Equal a b -> Equal b c -> Equal a c
trans = undefined

subst :: forall (p :: Nat -> Type) (a :: Nat) (b :: Nat). Equal a b -> p a -> p b
subst = undefined

-- Now let's prove subst2 using subst (both facts should be obvious)
subst2 :: forall (c :: Nat -> Nat) (a :: Nat) (b :: Nat). Equal a b -> Equal (c a) (c b)

-- We will need this type
data Lam1 (a::Nat) (c::Nat -> Nat) (x::Nat) = MkLam1 { unLam1 :: Equal (c a) (c x) }

-- Now the proof
subst2 x = let {
    fact1 :: Equal (c a) (c a) = refl;
} in unLam1 (subst @(Lam1 a c) x (MkLam1 fact1))

type family Add :: Nat -> Nat -> Nat

addz :: Equal (Add x Z) x
addz = undefined

addn :: Equal (Add x (N y)) (N (Add x y))
addn = undefined

addz2 :: Equal (Add Z x) x

data Lam2 (x :: Nat) = MkLam2 { unLam2 :: Equal (Add Z x) x }

addz2 = let {
    fact1 :: Equal (Add Z Z) Z = addz;
    fact2 :: forall xx. Equal (Add Z xx) xx -> Equal (Add Z (N xx)) (N xx);
    fact2 premise = let {
        fact3 :: Equal (Add Z (N xx)) (N (Add Z xx)) = addn;
        fact4 :: Equal (N (Add Z xx)) (N xx) = subst2 @N premise;
    } in trans fact3 fact4;
    fact5 :: forall xx. Lam2 xx -> Lam2 (N xx);
    fact5 = MkLam2 . fact2 . unLam2;
} in unLam2 (ind @Lam2 (MkLam2 fact1) fact5)

main = return ()