This PR makes it harder to create "fake" theorems about definitions that
are stubbed-out with `sorry` by ensuring that each `sorry` is not
definitionally equal to any other. For example, this now fails:
```lean
example : (sorry : Nat) = sorry := rfl -- fails
```
However, this still succeeds, since the `sorry` is a single
indeterminate `Nat`:
```lean
def f (n : Nat) : Nat := sorry
example : f 0 = f 1 := rfl -- succeeds
```
One can be more careful by putting parameters to the right of the colon:
```lean
def f : (n : Nat) → Nat := sorry
example : f 0 = f 1 := rfl -- fails
```
Most sources of synthetic sorries (recall: a sorry that originates from
the elaborator) are now unique, except for elaboration errors, since
making these unique tends to cause a confusing cascade of errors. In
general, however, such sorries are labeled. This enables "go to
definition" on `sorry` in the Infoview, which brings you to its origin.
The option `set_option pp.sorrySource true` causes the pretty printer to
show source position information on sorries.
**Details:**
* Adds `Lean.Meta.mkLabeledSorry`, which creates a sorry that is labeled
with its source position. For example, `(sorry : Nat)` might elaborate
to
```
sorryAx (Lean.Name → Nat) false
`lean.foo.12.8.12.13.8.13._sorry._@.lean.foo._hyg.153
```
It can either be made unique (like the above) or merely labeled. Labeled
sorries use an encoding that does not impact defeq:
```
sorryAx (Unit → Nat) false (Function.const Lean.Name ()
`lean.foo.14.7.13.7.13.69._sorry._@.lean.foo._hyg.174)
```
* Makes the `sorry` term, the `sorry` tactic, and every elaboration
failure create labeled sorries. Most are unique sorries, but some
elaboration errors are labeled sorries.
* Renames `OmissionInfo` to `DelabTermInfo` and adds configuration
options to control LSP interactions. One field is a source position to
use for "go to definition". This is used to implement "go to definition"
on labeled sorries.
* Makes hovering over a labeled `sorry` show something friendlier than
that full `sorryAx` expression. Instead, the first hover shows the
simplified ``sorry `«lean.foo:48:11»``. Hovering over that hover shows
the full `sorryAx`. Setting `set_option pp.sorrySource true` makes
`sorry` always start with printing with this source position
information.
* Removes `Lean.Meta.mkSyntheticSorry` in favor of `Lean.Meta.mkSorry`
and `Lean.Meta.mkLabeledSorry`.
* Changes `sorryAx` so that the `synthetic` argument is no longer
optional.
* Gives `addPPExplicitToExposeDiff` awareness of labeled sorries. It can
set `pp.sorrySource` when source positions differ.
* Modifies the delaborator framework so that delaborators can set Info
themselves without it being overwritten.
Incidentally closes#4972.
Inspired by [this Zulip
thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Is.20a.20.60definition_wanted.60.20keyword.20possible.3F/near/477260277).
This PR adds `Nat` theorems for distributing `>>>` over bitwise
operations, paralleling those of `BitVec`.
This enables closing goals like the following using `simp`:
```lean
example (n : Nat) : (n <<< 2 ||| 3) >>> 2 = n := by simp [Nat.shiftRight_or_distrib]
```
It might be nice for these theorems to be `simp` lemmas, but they are
not currently in order to be consistent with the existing `BitVec` and
`div_two` theorems.
This PR makes all message constructors handle pretty printer errors.
Prior to this change, pretty printer errors in messages were not
uniformly handled. In core, some printers capture their errors (e.g.,
`ppExprWithInfos` and `ppTerm` ) and some do not (e.g., `ppGoal` and
`ppSignature`) propagate them to whatever serializes the message (e.g.,
the frontend).
To resolve this inconsistency and uniformly handle errors, the signature
for `ofLazy` now uses `BaseIO`. As such, all printers been adapted to
capture any errors within them and print similar messages to
`ppExprWithInfos` and `ppTerm` on such errors.
This PR adjusts the way the pretty printer unresolves names. It used to
make use of all `export`s when pretty printing, but now it only uses
`export`s that put names into parent namespaces (heuristic: these are
"API exports" that are intended by the library author), rather than
"horizontal exports" that put the names into an unrelated namespace,
which the dot notation feature in #6189 now incentivizes.
Closes the already closed#2524
This PR adds `BitVec.[toFin|getMsbD]_setWidth` and
`[getMsb|msb]_signExtend` as well as `ofInt_toInt`.
Also correct renamed the misnamed theorem for
`signExtend_eq_setWidth_of_msb_false`.
---------
Co-authored-by: Siddharth <siddu.druid@gmail.com>
This PR adds docstrings to `Expr.hasLooseBVars` and `Expr.hasLooseBVar`,
to clarify the difference between these functions, and to document that
the former traverses the expression, while the latter is constant-time,
using cached information.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR removes the deprecated aliases `Int.div := Int.tdiv` and
`Int.mod := Int.tmod`. Later we will rename `Int.ediv` to `Int.div` and
`Int.emod` to `Int.mod`.
This PR removes unnecessary parameters from the funcion induction
principles. This is a breaking change; broken code can typically be adjusted
simply by passing fewer parameters.
Part 2, adjusting after stage0 update.
Closes#6320
This PR removes unnecessary parameters from the funcion induction
principles. This is a breaking change; broken code can typically be adjusted
simply by passing fewer parameters.
Part 1, before stage0 update.
Closes#6320
This PR adds `protected` to `Fin.cast` and `BitVec.cast`, to avoid
confusion with `_root_.cast`. These should mostly be used via
dot-notation in any case.
This PR upstreams the `ToLevel` typeclass from mathlib and uses it to
fix the existing `ToExpr` instances so that they are truly universe
polymorphic (previously it generated malformed expressions when the
universe level was nonzero). We improve on the mathlib definition of
`ToLevel` to ensure the class always lives in `Type`, irrespective of
the universe parameter.
This implements part one of the plan to upstream a derive handler for
`ToExpr`, as discussed in #5906 and #5909.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
This PR adds lemmas simplifying `for` loops over `Option` into
`Option.pelim`, giving parity with lemmas simplifying `for` loops of
`List` into `List.fold`.
This PR removes an unused import in the time library that can yield to
import cycles when building stuff that gets imported by `Std.Internal`
but also wants to import `Std.Time`.
This PR adds `BitVec.[toInt|toFin]_concat` and moves a couple of
theorems into the concat section, as `BitVec.msb_concat` is needed for
the `toInt_concat` proof.
We also add `Bool.toInt`.
This PR adds theorems characterizing the value of the unsigned shift
right of a bitvector in terms of its 2s complement interpretation as an
integer.
Unsigned shift right by at least one bit makes the value of the
bitvector less than or equal to `2^(w-1)`,
makes the interpretation of the bitvector `Int` and `Nat` agree.
In the case when `n = 0`, then the shift right value equals the integer
interpretation.
```lean
theorem toInt_ushiftRight_eq_ite {x : BitVec w} {n : Nat} :
(x >>> n).toInt = if n = 0 then x.toInt else x.toNat >>> n
```
```lean
theorem toFin_uShiftRight {x : BitVec w} {n : Nat} :
(x >>> n).toFin = x.toFin / (Fin.ofNat' (2^w) (2^n))
```
---------
Co-authored-by: Harun Khan <harun19@stanford.edu>
Co-authored-by: Tobias Grosser <github@grosser.es>
This PR changes the implementation of `HashMap.toList`, so the ordering
agrees with `HashMap.toArray`.
Currently there are no verification lemmas about `HashMap.toList`, so no
contract is being broken yet!
This PR moves `IO.Channel` and `IO.Mutex` from `Init` to `Std.Sync` and
renames them to `Std.Channel` and `Std.Mutex`.
Note that the original files are retained and the deprecation is written
manually as we cannot import `Std` from `Init` so this is the only way
to deprecate without a hard breaking change. In particular we do not yet
move `Std.Queue` from `Init` to `Std` both because it needs to be
retained for this deprecation to work but also because it is already
within the `Std` namespace and as such we cannot maintain two copies of
the file at once. After the deprecation period is finished `Std.Queue`
will find a new home in `Std.Data.Queue`.
