{-# 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