{-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE ExplicitNamespaces #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} module Data.Type.Natural.Lemma.Presburger where import Data.Type.Equality import Data.Type.Natural.Core import Data.Void plusEqZeroL :: SNat n -> SNat m -> n + m :~: 0 -> n :~: 0 plusEqZeroL :: SNat n -> SNat m -> ((n + m) :~: 0) -> n :~: 0 plusEqZeroL SNat n _ SNat m _ (n + m) :~: 0 Refl = n :~: 0 forall k (a :: k). a :~: a Refl plusEqZeroR :: SNat n -> SNat m -> n + m :~: 0 -> m :~: 0 plusEqZeroR :: SNat n -> SNat m -> ((n + m) :~: 0) -> m :~: 0 plusEqZeroR SNat n _ SNat m _ (n + m) :~: 0 Refl = m :~: 0 forall k (a :: k). a :~: a Refl succNonCyclic :: SNat n -> Succ n :~: 0 -> Void succNonCyclic :: SNat n -> (Succ n :~: 0) -> Void succNonCyclic SNat n Zero Succ n :~: 0 r = case Succ n :~: 0 r of succNonCyclic (Succ SNat n1 n) Succ n :~: 0 Refl = SNat n1 -> (Succ n1 :~: 0) -> Void forall (n :: Nat). SNat n -> (Succ n :~: 0) -> Void succNonCyclic SNat n1 n Succ n1 :~: 0 forall k (a :: k). a :~: a Refl