2120883307
@Kha I had some unexpected surprises, but it is a good change.
Here is the summary.
1- We could get rid of `a %ₙ b` and `ModN` class. We can use `HMod`
instead. It was a positive surprise since I didn't remember we had
this `ModN` class.
2- Coercions are never used in heterogeneous operators. This is
expected since `a * b` is now notation for `HMul.hMul a b`, and
`a` and `b` may have different types. I manually added instances such
as `HMul Nat Int Int`. However, I did not try to add generic instances
such as
```
instance [Coe a b] [Mul b] : HMul a b b where
hMul x y := mul (coe x) y
```
I will try later.
3- Give `h : cs.size > 0`, I got a type error at
```
let idx : Fin cs.size := ⟨cs.size - 1, Nat.predLt h⟩
```
`Nat.predLt h` has type `Nat.pred cs.size < cs.size`
However, `Nat.pred cs.size` doesn't unify with `cs.size - 1`.
The problem is that we can't synthesize the `HSub` instance until
we apply the default instances.
It worked before because `isDefEq` would force the pending TC
problem `Sub Nat` to be resolved, and after that we would be able
to reduce `cs.size - 1` and establish that it is definitionally
equal to `Nat.pred cs.size`.
I considered two possible workarounds
a) `let idx : Fin cs.size := ⟨cs.size - (1:Nat), Nat.predLt h⟩`
b) `let idx : Fin cs.size := ⟨cs.size - 1, by exact Nat.predLt h⟩`
The first one works because we are not providing enough information
for synthesizing the `HSub` instance. The second works because it
postpones the elaboration of `Nat.predLt h`. The default instances
will be applied before we start applying tactics.
4- The `.` notation is affected too. For example, `(x + 1).toUInt8`
doesn't work since we don't know the type of `x+1` until we apply
default instances. I fixed it by using `(x + (1:Nat)).toUInt8`.
Another possible fix is `Nat.toUInt8 (x + 1)`.
Similarly, `(x+1).fold ...` doesn't work.
5- The following code failed to be elaborated
```
indent (push s!"{ss'}\n") (some (0 - Format.getIndent (← getOptions)))
```
It was working before, but it relied on how the expected type is
propagated. The elaborator process
```
some (0 - Format.getIndent (← getOptions))
```
with expected type `(Option Int)`. So, the `-` is interpreted as
`Int.sub` although `Format.getIndent (← getOptions)` has type `Nat`.
In the new `HSub`, the expected type doesn't really influence TC
resolution since it is an `outparam`. So, we failed with the error
failed to synthesize `HSub Nat Nat Int`.
One possible fix was to add the instance `HSub Nat Nat Int` with
`Int.sub`, but I used the following fix
```
some ((0 : Int) - Format.getIndent (← getOptions))
```
which makes it clear that we want the `Int.sub` operator instead of
`Nat.sub`.
220 lines
5.5 KiB
Text
220 lines
5.5 KiB
Text
/-
|
|
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Jeremy Avigad, Leonardo de Moura
|
|
|
|
The integers, with addition, multiplication, and subtraction.
|
|
-/
|
|
prelude
|
|
import Init.Data.Nat.Basic
|
|
import Init.Data.List
|
|
import Init.Data.Repr
|
|
import Init.Data.ToString.Basic
|
|
open Nat
|
|
|
|
/- the Type, coercions, and notation -/
|
|
|
|
inductive Int : Type where
|
|
| ofNat : Nat → Int
|
|
| negSucc : Nat → Int
|
|
|
|
attribute [extern "lean_nat_to_int"] Int.ofNat
|
|
attribute [extern "lean_int_neg_succ_of_nat"] Int.negSucc
|
|
|
|
instance : Coe Nat Int := ⟨Int.ofNat⟩
|
|
|
|
namespace Int
|
|
instance : Inhabited Int := ⟨ofNat 0⟩
|
|
|
|
def negOfNat : Nat → Int
|
|
| 0 => 0
|
|
| succ m => negSucc m
|
|
|
|
set_option bootstrap.gen_matcher_code false in
|
|
@[extern "lean_int_neg"]
|
|
protected def neg (n : @& Int) : Int :=
|
|
match n with
|
|
| ofNat n => negOfNat n
|
|
| negSucc n => succ n
|
|
|
|
def subNatNat (m n : Nat) : Int :=
|
|
match (n - m : Nat) with
|
|
| 0 => ofNat (m - n) -- m ≥ n
|
|
| (succ k) => negSucc k
|
|
|
|
set_option bootstrap.gen_matcher_code false in
|
|
@[extern "lean_int_add"]
|
|
protected def add (m n : @& Int) : Int :=
|
|
match m, n with
|
|
| ofNat m, ofNat n => ofNat (m + n)
|
|
| ofNat m, negSucc n => subNatNat m (succ n)
|
|
| negSucc m, ofNat n => subNatNat n (succ m)
|
|
| negSucc m, negSucc n => negSucc (succ (m + n))
|
|
|
|
set_option bootstrap.gen_matcher_code false in
|
|
@[extern "lean_int_mul"]
|
|
protected def mul (m n : @& Int) : Int :=
|
|
match m, n with
|
|
| ofNat m, ofNat n => ofNat (m * n)
|
|
| ofNat m, negSucc n => negOfNat (m * succ n)
|
|
| negSucc m, ofNat n => negOfNat (succ m * n)
|
|
| negSucc m, negSucc n => ofNat (succ m * succ n)
|
|
|
|
instance : Neg Int where
|
|
neg := Int.neg
|
|
instance : Add Int where
|
|
add := Int.add
|
|
instance : Mul Int where
|
|
mul := Int.mul
|
|
|
|
instance : HAdd Int Nat Int where
|
|
hAdd a b := Int.add a b
|
|
instance : HAdd Nat Int Int where
|
|
hAdd a b := Int.add a b
|
|
|
|
instance : HMul Int Nat Int where
|
|
hMul a b := Int.mul a b
|
|
instance : HMul Nat Int Int where
|
|
hMul a b := Int.mul a b
|
|
|
|
@[extern "lean_int_sub"]
|
|
protected def sub (m n : @& Int) : Int :=
|
|
m + (- n)
|
|
|
|
instance : Sub Int where
|
|
sub := Int.sub
|
|
|
|
instance : HSub Int Nat Int where
|
|
hSub a b := Int.sub a b
|
|
instance : HSub Nat Int Int where
|
|
hSub a b := Int.sub a b
|
|
|
|
inductive NonNeg : Int → Prop where
|
|
| mk (n : Nat) : NonNeg (ofNat n)
|
|
|
|
protected def LessEq (a b : Int) : Prop := NonNeg (b - a)
|
|
|
|
instance : HasLessEq Int where
|
|
LessEq := Int.LessEq
|
|
|
|
protected def Less (a b : Int) : Prop := (a + 1) ≤ b
|
|
|
|
instance : HasLess Int where
|
|
Less := Int.Less
|
|
|
|
set_option bootstrap.gen_matcher_code false in
|
|
@[extern "lean_int_dec_eq"]
|
|
protected def decEq (a b : @& Int) : Decidable (a = b) :=
|
|
match a, b with
|
|
| ofNat a, ofNat b => match decEq a b with
|
|
| isTrue h => isTrue <| h ▸ rfl
|
|
| isFalse h => isFalse <| fun h' => Int.noConfusion h' (fun h' => absurd h' h)
|
|
| negSucc a, negSucc b => match decEq a b with
|
|
| isTrue h => isTrue <| h ▸ rfl
|
|
| isFalse h => isFalse <| fun h' => Int.noConfusion h' (fun h' => absurd h' h)
|
|
| ofNat a, negSucc b => isFalse <| fun h => Int.noConfusion h
|
|
| negSucc a, ofNat b => isFalse <| fun h => Int.noConfusion h
|
|
|
|
instance : DecidableEq Int := Int.decEq
|
|
|
|
set_option bootstrap.gen_matcher_code false in
|
|
@[extern "lean_int_dec_nonneg"]
|
|
private def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
|
|
match m with
|
|
| ofNat m => isTrue <| NonNeg.mk m
|
|
| negSucc m => isFalse <| fun h => nomatch h
|
|
|
|
@[extern "lean_int_dec_le"]
|
|
instance decLe (a b : @& Int) : Decidable (a ≤ b) :=
|
|
decNonneg _
|
|
|
|
@[extern "lean_int_dec_lt"]
|
|
instance decLt (a b : @& Int) : Decidable (a < b) :=
|
|
decNonneg _
|
|
|
|
set_option bootstrap.gen_matcher_code false in
|
|
@[extern "lean_nat_abs"]
|
|
def natAbs (m : @& Int) : Nat :=
|
|
match m with
|
|
| ofNat m => m
|
|
| negSucc m => m.succ
|
|
|
|
protected def repr : Int → String
|
|
| ofNat m => Nat.repr m
|
|
| negSucc m => "-" ++ Nat.repr (succ m)
|
|
|
|
instance : Repr Int where
|
|
repr := Int.repr
|
|
|
|
instance : ToString Int where
|
|
toString := Int.repr
|
|
|
|
instance : OfNat Int n where
|
|
ofNat := Int.ofNat n
|
|
|
|
@[extern "lean_int_div"]
|
|
def div : (@& Int) → (@& Int) → Int
|
|
| ofNat m, ofNat n => ofNat (m / n)
|
|
| ofNat m, negSucc n => -ofNat (m / succ n)
|
|
| negSucc m, ofNat n => -ofNat (succ m / n)
|
|
| negSucc m, negSucc n => ofNat (succ m / succ n)
|
|
|
|
@[extern "lean_int_mod"]
|
|
def mod : (@& Int) → (@& Int) → Int
|
|
| ofNat m, ofNat n => ofNat (m % n)
|
|
| ofNat m, negSucc n => ofNat (m % succ n)
|
|
| negSucc m, ofNat n => -ofNat (succ m % n)
|
|
| negSucc m, negSucc n => -ofNat (succ m % succ n)
|
|
|
|
instance : Div Int where
|
|
div := Int.div
|
|
|
|
instance : Mod Int where
|
|
mod := Int.mod
|
|
|
|
instance : HDiv Int Nat Int where
|
|
hDiv a b := Int.div a b
|
|
instance : HDiv Nat Int Int where
|
|
hDiv a b := Int.div a b
|
|
|
|
instance : HMod Int Nat Int where
|
|
hMod a b := Int.mod a b
|
|
instance : HMod Nat Int Int where
|
|
hMod a b := Int.mod a b
|
|
|
|
def toNat : Int → Nat
|
|
| ofNat n => n
|
|
| negSucc n => 0
|
|
|
|
def natMod (m n : Int) : Nat := (m % n).toNat
|
|
|
|
protected def Int.pow (m : Int) : Nat → Int
|
|
| 0 => 1
|
|
| succ n => Int.pow m n * m
|
|
|
|
instance : HPow Int Nat Int where
|
|
hPow := Int.pow
|
|
|
|
end Int
|
|
|
|
namespace String
|
|
|
|
def toInt? (s : String) : Option Int :=
|
|
if s.get 0 = '-' then do
|
|
let v ← (s.toSubstring.drop 1).toNat?;
|
|
pure <| - Int.ofNat v
|
|
else
|
|
Int.ofNat <$> s.toNat?
|
|
|
|
def isInt (s : String) : Bool :=
|
|
if s.get 0 = '-' then
|
|
(s.toSubstring.drop 1).isNat
|
|
else
|
|
s.isNat
|
|
|
|
def toInt! (s : String) : Int :=
|
|
match s.toInt? with
|
|
| some v => v
|
|
| none => panic! "Int expected"
|
|
|
|
end String
|