Could not deduce n~0 from the context n<=0

[int-index]

Since we're dealing with natural numbers, which are by definition non-negative, we must be able to conclude n~0 from n<=0. However, the following code does not compile:

natLeqZero :: (n <= 0) => n :~: 0
natLeqZero = Refl

[christiaanb]

EDIT: nvm the below, I misread.

~I don't think I can agree. I can only agree with:~

natEqZero :: (n <= 0, 0 <= n) => n :~: 0
natEqZero = Refl

[sheaf]

Here are some other facts about inequalities which I needed but the plugin couldn't handle:

lt1_is_Zero :: KnownNat n => (1 <=? n) :~: 'False -> (n :~: 0)
lt1_is_Zero _ = unsafeCoerce Refl

lte_transitive
  :: forall i j k
  .  ( KnownNat i, KnownNat j, KnownNat k, i <= j, j <= k )
  => ( i <=? k ) :~: 'True
lte_transitive = unsafeCoerce Refl

lemma1
  :: forall j n
  .  ( j <= n, 1 <= (n-j) )
  => ( CmpNat j n :~: LT )
lemma1 = unsafeCoerce Refl

lemma2
  :: forall j n
  .  ( j <= n, 1 <= (n-j) )
  => ( (j+1) <=? n ) :~: 'True
lemma2 = unsafeCoerce Refl

@christiaanb What's currently stopping the plugin from being able to handle deductions like these? I'd like to try enhancing the plugin to allow it to make these deductions; how would you recommend I go about it?

Edit: here's another one that doesn't work:

foo :: ( 4 <= n ) => Proxy n -> 3 `CmpNat` n :~: LT
foo _ = Refl

[christiaanb]

The solver for equalities and the solver for inequalities are disjoint (the plugin used to only deal with equalities)

The equality solver uses rewriting to reach a Sum-of-Product-like (not actual SOP because of exponentiation) normal form of the equations, and then does a simple syntactic equality check. Your first example, lt1_is_Zero requires more of an interval-arithmic based approach (we know that 0 <= n < 1) I guess... it might be possible to bolt it on top.

The inequality solver is also based on rewriting: it tries to rewrite given inequalities to the wanted inequality using some of the standard stuff we know about inequality: monotonicity of addition, transitivity, etc. So that means it can only solve a wanted inequality that merely need the proof of a single given inequality. Your examples all need two given inequalities, for which the stated approach doesn’t work. I never found the time or inspiration to build a more general solver.

One thing to note, people have asked me: “why not use an SMT solver to solve all these equations?” To which my answer is: when I started on the plugins I couldn’t find an SMT solver that can solve equations involving non-constant multiplications, let alone exponentiation. Perhaps they can these days, so that would be worthwhile to investigate. If you want to take a shot at writing a better inequality solver I’d be happy to walk you through the existing code during a telco/confcall. Just send me an email so we can set a date and time.

[amigalemming]

There are more type checker plugings that migth help: ghc-typelits-presburger and ghc-typelits-knownnat.