Compare commits

..

41 Commits

Author SHA1 Message Date
Leonardo de Moura
df2571286b chore: update stage0 2024-02-17 17:19:53 -08:00
Leonardo de Moura
b7dcd434fb chore: basic simprocs for String 2024-02-17 17:16:42 -08:00
Leonardo de Moura
80b10103a0 chore: simprocs for Eq 2024-02-17 16:29:29 -08:00
Leonardo de Moura
a0aea373a1 feat: simprocs for Char.val, default char, and Char.ofNatAux 2024-02-17 16:06:50 -08:00
Leonardo de Moura
7a8ff91d33 feat: simprocs for UInt??.ofNatCore and UInt??.toNat 2024-02-17 15:44:17 -08:00
Leonardo de Moura
3e5695e07e feat: simprocs for Char (#3382) 2024-02-17 20:36:51 +00:00
Leonardo de Moura
61a76a814f feat: delaborator for Char literals (#3381) 2024-02-17 12:19:40 -08:00
Arthur Adjedj
0c92d17792 fix: instantiate the types of inductives with the right parameters (#3246)
Closes #3242
2024-02-17 16:52:28 +00:00
Joachim Breitner
d536534c4d refactor: drop CasesOnApp, use MatcherApp (#3369)
in all uses of `CasesOnApp`, we treat `MatcherApp`s the same way,
dupliating a fair amount of relatively hairy code (and there is more to
come).

However, the `MatcherApp` abstraction is perfectly capable of
also representing `casesOn` applications, at least for the use cases
encountered so far.

So lets just (optionally) include `casesOn` applications when looking
for matchers,
and remove the `CasesOnApp` abstraction completely.
2024-02-17 15:25:32 +00:00
Leonardo de Moura
97e7e668d6 chore: pp.proofs.withType is now false by default (#3379)
`pp.proofs.withType := true` often produces too much noise in the info
view.
2024-02-17 15:09:24 +00:00
Sebastian Ullrich
dda88c9926 feat: infoview.maxTraceChildren (#3370)
Incrementally unveil trace children for excessively large nodes to
improve infoview rendering time, adjust particularly chatty
`simp.ground` trace to make use of it.
2024-02-17 14:04:46 +00:00
Leonardo de Moura
ef9a6bb839 fix: an equation lemma with autoParam arguments fails to rewrite (#3316)
closes #2243
2024-02-17 13:42:34 +00:00
Leonardo de Moura
baa9fe5932 fix: simp gets stuck on autoParam (#3315)
closes #2862
2024-02-17 13:42:19 +00:00
Leonardo de Moura
368326fb48 fix: simp fails when custom discharger makes no progress (#3317)
closes #2634
2024-02-17 13:42:04 +00:00
Leonardo de Moura
678797b67b fix: simp fails to discharge autoParam premises even when it can reduce them to True (#3314)
closes #3257
2024-02-17 13:41:48 +00:00
Mac Malone
496a8d578e fix: lake: open config trace as read-only first & avoid deadlock (#3254)
Lake previously opened the configuration trace as read-write even if it
does not update the configuration. This meant it failed if the trace was
read-only. With this change, it now first acquires a read-only handle
and then, if and only if it determines the need for a reconfigure, does
it re-open the file with a read-write handle. Also, this change fixes a
potential deadlock (Lake will error instead) and generally clarifies the
trace locking code.
2024-02-17 04:20:14 +00:00
Mac Malone
3fb7262fe0 fix: cloud release trace & lake build :release errors (#3248)
Fixes a bug with Lake cloud releases where a cloud release would produce
a different trace if the package was the root of the workspace versus a
dependency. Also, an explicit fetch of a cloud release (e.g., via `lake
build :release`) will now error out with a non-zero exit code if it
fails to find, download, and unpack a release.
2024-02-17 00:18:10 +00:00
Joe Hendrix
8f010a6115 fix: liasolver benchmark bug introduced by #3364 (#3372)
This fixes a rounded division/mod bug introduced by the change in
semantics from Int.div to Int.mod in #3364.
2024-02-16 23:39:26 +00:00
Joachim Breitner
089cd50d00 refactor: let MatcherApp.addArg? check if argument was refined (#3368)
Previously, `CasesOn.addArg?` would do that check inline, while
`MatcherApp.addArg?` would do it after the fact.

Now `MatcherApp.addArg?` uses the same idiom.

Also, makes both `addArg?` always fail if the argument was not refined.

The work on functional induction principles calls for more unification
between the handling of `CasesOnApp` and `MatcherApp`, so this is a step
in that direction.
2024-02-16 15:35:19 +00:00
Scott Morrison
18afefda96 chore: upstream basic statements about inequalities (#3366) 2024-02-16 05:42:38 +00:00
Joe Hendrix
06e21faecd chore: upstream Std.Data.Int.Init modules (#3364)
This is pretty big PR that upstreams all of Std.Data.Int.Init in one go.

So far lemmas have seen minimal changes needed to adapt to Lean core
environment.

---------

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
2024-02-16 03:58:23 +00:00
Scott Morrison
c9f27c36a0 chore: upstream false_or_by_contra tactic (#3363)
Changes the goal to `False`, retaining as much information as possible:

* If the goal is `False`, do nothing.
* If the goal is an implication or a function type, introduce the
argument and restart.
  (In particular, if the goal is `x ≠ y`, introduce `x = y`.)
* Otherwise, for a propositional goal `P`, replace it with `¬ ¬ P`
(attempting to find a `Decidable` instance, but otherwise falling back
to working classically)
  and introduce `¬ P`.
* For a non-propositional goal use `False.elim`.
2024-02-16 03:58:10 +00:00
Scott Morrison
c9cba33f57 chore: upstream Expr.nat? and int? for recognising 'normal form' numerals (#3360)
`nat?` checks if an expression is a "natural number in normal form",
i.e. of the form `OfNat n`, where `n` matches `.lit (.natVal n)` for
some `n`.
and if so returns `n`.
2024-02-16 03:31:22 +00:00
Scott Morrison
84bd563cff chore: upstream Std's material on Ord and Ordering (#3365) 2024-02-16 02:57:47 +00:00
Scott Morrison
73524e37ae chore: upstream exfalso (#3361) 2024-02-16 02:21:32 +00:00
Scott Morrison
229f16f421 chore: upstream MVarId.applyConst (#3362)
Helper function for applying a constant to the goal, with fresh universe
metavariables.
2024-02-16 02:08:47 +00:00
Scott Morrison
eaf44d74ae chore: upstream Option material from Std (#3356) 2024-02-16 02:05:18 +00:00
Scott Morrison
6fc3ea7790 chore: upstream Expr.getAppFnArgs (#3359)
This is a widely used helper function in Std/Mathlib when matching on
expressions.

I've reordered some definitions to keep things together. This
introduces:
```
/-- Return the function (name) and arguments of an application. -/
def getAppFnArgs (e : Expr) : Name × Array Expr :=
  withApp e λ e a => (e.constName, a)
```
and 
```
/-- If the expression is a constant, return that name. Otherwise return `Name.anonymous`. -/
def constName (e : Expr) : Name :=
  e.constName?.getD Name.anonymous
```
2024-02-16 01:51:59 +00:00
Scott Morrison
a4e27d3090 chore: upstream HashSet.merge (#3357) 2024-02-16 01:38:16 +00:00
Joe Hendrix
1d9074c524 chore: upstream NatCast and IntCast (#3347)
This upstreams NatCast and IntCast alone independent of norm_cast in
#3322.

This will allow more efficiently upstreaming parts of Std.Data.Int
relevant for omega.

---------

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
2024-02-16 00:54:22 +00:00
Kyle Miller
e29d75a961 feat: have pp.proofs use for omission (#3241)
By having the `pp.proofs` feature use `⋯` when omitting proofs, when
users copy/paste terms from the InfoView the elaborator can give an
error message explaining why the term cannot be elaborated.

Also adds `pp.proofs.threshold` option to allow users to pretty print
shallow proof terms. By default, only atomic proof terms are pretty
printed.

This adjustment was suggested in PR #3201, which added `⋯` and the
related `pp.deepTerms` option.
2024-02-15 21:49:41 +00:00
Kyle Miller
8aab74e65d fix: make withOverApp annotate the expression position and register TermInfo (#3327)
This makes it so that when `withOverApp` is handling overapplied
functions, the term produced by the supplied delaborator is hoverable in
the Infoview.
2024-02-15 17:40:54 +00:00
Sebastian Ullrich
4e58b428e9 doc: add Kyle Miller as delaborator code owner 2024-02-15 17:42:57 +01:00
Lean stage0 autoupdater
271ae5b8e5 chore: update stage0 2024-02-15 12:32:00 +00:00
Leonardo de Moura
a14bbbffb2 chore: add [ext] basic theorems, add test 2024-02-15 13:26:01 +01:00
Scott Morrison
5a95f91fae chore: update stage0 2024-02-15 13:26:01 +01:00
Scott Morrison
11727a415b chore: upstream ext
and_intros and subst_eqs are not builtin

clarify failure modes

Clarify docString of extCore

clarify

chore: builtin `subst_eqs` tactic

chore: builtin `ext`
2024-02-15 13:26:01 +01:00
Sebastian Ullrich
90a516de09 chore: avoid libleanshared symbol limit (#3346) 2024-02-15 11:39:44 +00:00
Scott Morrison
ae524d465f chore: a missing List lemma in Init (#3344) 2024-02-15 08:55:48 +00:00
Scott Morrison
9a3f0f1909 chore: upstream Std.Data.Array.Init.Lemmas (#3343) 2024-02-15 17:50:07 +11:00
Scott Morrison
fae5b2e87c chore: upstream Std.Data.List.Init.Lemmas (#3341) 2024-02-15 03:19:23 +00:00
335 changed files with 4456 additions and 846 deletions

View File

@@ -17,6 +17,7 @@
/src/Lean/Meta/Tactic/ @leodemoura
/src/Lean/Parser/ @Kha
/src/Lean/PrettyPrinter/ @Kha
/src/Lean/PrettyPrinter/Delaborator/ @kmill
/src/Lean/Server/ @mhuisi
/src/Lean/Widget/ @Vtec234
/src/runtime/io.cpp @joehendrix

View File

@@ -11,6 +11,13 @@ of each version.
v4.7.0 (development in progress)
---------
* When the `pp.proofs` is false, now omitted proofs use `⋯` rather than `_`,
which gives a more helpful error message when copied from the Infoview.
The `pp.proofs.threshold` option lets small proofs always be pretty printed.
[#3241](https://github.com/leanprover/lean4/pull/3241).
* `pp.proofs.withType` is now set to false by default to reduce noise in the info view.
v4.6.0
---------

View File

@@ -1932,6 +1932,18 @@ axiom ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b
end Lean
@[simp] theorem ge_iff_le [LE α] {x y : α} : x y y x := Iff.rfl
@[simp] theorem gt_iff_lt [LT α] {x y : α} : x > y y < x := Iff.rfl
theorem le_of_eq_of_le {a b c : α} [LE α] (h₁ : a = b) (h₂ : b c) : a c := h₁ h₂
theorem le_of_le_of_eq {a b c : α} [LE α] (h₁ : a b) (h₂ : b = c) : a c := h₂ h₁
theorem lt_of_eq_of_lt {a b c : α} [LT α] (h₁ : a = b) (h₂ : b < c) : a < c := h₁ h₂
theorem lt_of_lt_of_eq {a b c : α} [LT α] (h₁ : a < b) (h₂ : b = c) : a < c := h₂ h₁
namespace Std
variable {α : Sort u}

View File

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
prelude
import Init.Data.Basic
import Init.Data.Nat
import Init.Data.Cast
import Init.Data.Char
import Init.Data.String
import Init.Data.List

View File

@@ -11,3 +11,4 @@ import Init.Data.Array.InsertionSort
import Init.Data.Array.DecidableEq
import Init.Data.Array.Mem
import Init.Data.Array.BasicAux
import Init.Data.Array.Lemmas

View File

@@ -0,0 +1,187 @@
/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
prelude
import Init.Data.Nat
import Init.Data.List.Lemmas
import Init.Data.Fin.Basic
import Init.Data.Array.Mem
/-!
## Bootstrapping theorems about arrays
This file contains some theorems about `Array` and `List` needed for `Std.List.Basic`.
-/
namespace Array
attribute [simp] data_toArray uset
@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
@[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
theorem getElem_eq_data_get (a : Array α) (h : i < a.size) : a[i] = a.data.get i, h := by
by_cases i < a.size <;> (try simp [*]) <;> rfl
theorem foldlM_eq_foldlM_data.aux [Monad m]
(f : β α m β) (arr : Array α) (i j) (H : arr.size i + j) (b) :
foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.data.drop j).foldlM f b := by
unfold foldlM.loop
split; split
· cases Nat.not_le_of_gt _ (Nat.zero_add _ H)
· rename_i i; rw [Nat.succ_add] at H
simp [foldlM_eq_foldlM_data.aux f arr i (j+1) H]
rw (config := {occs := .pos [2]}) [ List.get_drop_eq_drop _ _ _]
rfl
· rw [List.drop_length_le (Nat.ge_of_not_lt _)]; rfl
theorem foldlM_eq_foldlM_data [Monad m]
(f : β α m β) (init : β) (arr : Array α) :
arr.foldlM f init = arr.data.foldlM f init := by
simp [foldlM, foldlM_eq_foldlM_data.aux]
theorem foldl_eq_foldl_data (f : β α β) (init : β) (arr : Array α) :
arr.foldl f init = arr.data.foldl f init :=
List.foldl_eq_foldlM .. foldlM_eq_foldlM_data ..
theorem foldrM_eq_reverse_foldlM_data.aux [Monad m]
(f : α β m β) (arr : Array α) (init : β) (i h) :
(arr.data.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f arr 0 i h init := by
unfold foldrM.fold
match i with
| 0 => simp [List.foldlM, List.take]
| i+1 => rw [ List.take_concat_get _ _ h]; simp [ (aux f arr · i)]; rfl
theorem foldrM_eq_reverse_foldlM_data [Monad m] (f : α β m β) (init : β) (arr : Array α) :
arr.foldrM f init = arr.data.reverse.foldlM (fun x y => f y x) init := by
have : arr = #[] 0 < arr.size :=
match arr with | [] => .inl rfl | a::l => .inr (Nat.zero_lt_succ _)
match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_
simp [foldrM, h, foldrM_eq_reverse_foldlM_data.aux, List.take_length]
theorem foldrM_eq_foldrM_data [Monad m]
(f : α β m β) (init : β) (arr : Array α) :
arr.foldrM f init = arr.data.foldrM f init := by
rw [foldrM_eq_reverse_foldlM_data, List.foldlM_reverse]
theorem foldr_eq_foldr_data (f : α β β) (init : β) (arr : Array α) :
arr.foldr f init = arr.data.foldr f init :=
List.foldr_eq_foldrM .. foldrM_eq_foldrM_data ..
@[simp] theorem push_data (arr : Array α) (a : α) : (arr.push a).data = arr.data ++ [a] := by
simp [push, List.concat_eq_append]
theorem foldrM_push [Monad m] (f : α β m β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
simp [foldrM_eq_reverse_foldlM_data, -size_push]
@[simp] theorem foldrM_push' [Monad m] (f : α β m β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldrM f init (start := arr.size + 1) = f a init >>= arr.foldrM f := by
simp [ foldrM_push]
theorem foldr_push (f : α β β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldr f init = arr.foldr f (f a init) := foldrM_push ..
@[simp] theorem foldr_push' (f : α β β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldr f init (start := arr.size + 1) = arr.foldr f (f a init) := foldrM_push' ..
@[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.data ++ l := by
simp [toListAppend, foldr_eq_foldr_data]
@[simp] theorem toList_eq (arr : Array α) : arr.toList = arr.data := by
simp [toList, foldr_eq_foldr_data]
/-- A more efficient version of `arr.toList.reverse`. -/
@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.data.reverse := by
rw [toListRev, foldl_eq_foldl_data, List.foldr_reverse, List.foldr_self]
theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
(a.push x)[i] = a[i] := by
simp only [push, getElem_eq_data_get, List.concat_eq_append, List.get_append_left, h]
@[simp] theorem get_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
simp only [push, getElem_eq_data_get, List.concat_eq_append]
rw [List.get_append_right] <;> simp [getElem_eq_data_get, Nat.zero_lt_one]
theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
(a.push x)[i] = if h : i < a.size then a[i] else x := by
by_cases h' : i < a.size
· simp [get_push_lt, h']
· simp at h
simp [get_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α m β) (arr : Array α) :
arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[] := by
rw [mapM, aux, foldlM_eq_foldlM_data]; rfl
where
aux (i r) :
mapM.map f arr i r = (arr.data.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
unfold mapM.map; split
· rw [ List.get_drop_eq_drop _ i _]
simp [aux (i+1), map_eq_pure_bind]; rfl
· rw [List.drop_length_le (Nat.ge_of_not_lt _)]; rfl
termination_by arr.size - i
@[simp] theorem map_data (f : α β) (arr : Array α) : (arr.map f).data = arr.data.map f := by
rw [map, mapM_eq_foldlM]
apply congrArg data (foldl_eq_foldl_data (fun bs a => push bs (f a)) #[] arr) |>.trans
have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = arr.data ++ l.map f := by
induction l generalizing arr <;> simp [*]
simp [H]
@[simp] theorem size_map (f : α β) (arr : Array α) : (arr.map f).size = arr.size := by
simp [size]
@[simp] theorem pop_data (arr : Array α) : arr.pop.data = arr.data.dropLast := rfl
@[simp] theorem append_eq_append (arr arr' : Array α) : arr.append arr' = arr ++ arr' := rfl
@[simp] theorem append_data (arr arr' : Array α) :
(arr ++ arr').data = arr.data ++ arr'.data := by
rw [ append_eq_append]; unfold Array.append
rw [foldl_eq_foldl_data]
induction arr'.data generalizing arr <;> simp [*]
@[simp] theorem appendList_eq_append
(arr : Array α) (l : List α) : arr.appendList l = arr ++ l := rfl
@[simp] theorem appendList_data (arr : Array α) (l : List α) :
(arr ++ l).data = arr.data ++ l := by
rw [ appendList_eq_append]; unfold Array.appendList
induction l generalizing arr <;> simp [*]
@[simp] theorem appendList_nil (arr : Array α) : arr ++ ([] : List α) = arr := Array.ext' (by simp)
@[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) :
arr ++ (a :: l) = arr.push a ++ l := Array.ext' (by simp)
theorem foldl_data_eq_bind (l : List α) (acc : Array β)
(F : Array β α Array β) (G : α List β)
(H : acc a, (F acc a).data = acc.data ++ G a) :
(l.foldl F acc).data = acc.data ++ l.bind G := by
induction l generalizing acc <;> simp [*, List.bind]
theorem foldl_data_eq_map (l : List α) (acc : Array β) (G : α β) :
(l.foldl (fun acc a => acc.push (G a)) acc).data = acc.data ++ l.map G := by
induction l generalizing acc <;> simp [*]
theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by simp
theorem anyM_eq_anyM_loop [Monad m] (p : α m Bool) (as : Array α) (start stop) :
anyM p as start stop = anyM.loop p as (min stop as.size) (Nat.min_le_right ..) start := by
simp only [anyM, Nat.min_def]; split <;> rfl
theorem anyM_stop_le_start [Monad m] (p : α m Bool) (as : Array α) (start stop)
(h : min stop as.size start) : anyM p as start stop = pure false := by
rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)]
theorem mem_def (a : α) (as : Array α) : a as a as.data :=
fun | .mk h => h, Array.Mem.mk

72
src/Init/Data/Cast.lean Normal file
View File

@@ -0,0 +1,72 @@
/-
Copyright (c) 2014 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Gabriel Ebner
-/
prelude
import Init.Coe
/-!
# `NatCast`
We introduce the typeclass `NatCast R` for a type `R` with a "canonical
homomorphism" `Nat → R`. The typeclass carries the data of the function,
but no required axioms.
This typeclass was introduced to support a uniform `simp` normal form
for such morphisms.
Without such a typeclass, we would have specific coercions such as
`Int.ofNat`, but also later the generic coercion from `Nat` into any
Mathlib semiring (including `Int`), and we would need to use `simp` to
move between them. However `simp` lemmas expressed using a non-normal
form on the LHS would then not fire.
Typically different instances of this class for the same target type `R`
are definitionally equal, and so differences in the instance do not
block `simp` or `rw`.
This logic also applies to `Int` and so we also introduce `IntCast` alongside
`Int.
## Note about coercions into arbitrary types:
Coercions such as `Nat.cast` that go from a concrete structure such as
`Nat` to an arbitrary type `R` should be set up as follows:
```lean
instance : CoeTail Nat R where coe := ...
instance : CoeHTCT Nat R where coe := ...
```
It needs to be `CoeTail` instead of `Coe` because otherwise type-class
inference would loop when constructing the transitive coercion `Nat →
Nat → Nat → ...`. Sometimes we also need to declare the `CoeHTCT`
instance if we need to shadow another coercion.
-/
/-- Type class for the canonical homomorphism `Nat → R`. -/
class NatCast (R : Type u) where
/-- The canonical map `Nat → R`. -/
protected natCast : Nat R
instance : NatCast Nat where natCast n := n
/--
Canonical homomorphism from `Nat` to a type `R`.
It contains just the function, with no axioms.
In practice, the target type will likely have a (semi)ring structure,
and this homomorphism should be a ring homomorphism.
The prototypical example is `Int.ofNat`.
This class and `IntCast` exist to allow different libraries with their own types that can be notated as natural numbers to have consistent `simp` normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with `NatCast` where possible. For instance, in Mathlib there will be such a homomorphism (and thus a `NatCast R` instance) whenever `R` is an additive monoid with a `1`.
-/
@[coe, reducible, match_pattern] protected def Nat.cast {R : Type u} [NatCast R] : Nat R :=
NatCast.natCast
-- see the notes about coercions into arbitrary types in the module doc-string
instance [NatCast R] : CoeTail Nat R where coe := Nat.cast
-- see the notes about coercions into arbitrary types in the module doc-string
instance [NatCast R] : CoeHTCT Nat R where coe := Nat.cast

View File

@@ -5,3 +5,9 @@ Authors: Leonardo de Moura
-/
prelude
import Init.Data.Int.Basic
import Init.Data.Int.Bitwise
import Init.Data.Int.DivMod
import Init.Data.Int.DivModLemmas
import Init.Data.Int.Gcd
import Init.Data.Int.Lemmas
import Init.Data.Int.Order

View File

@@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
The integers, with addition, multiplication, and subtraction.
-/
prelude
import Init.Coe
import Init.Data.Cast
import Init.Data.Nat.Div
import Init.Data.List.Basic
set_option linter.missingDocs true -- keep it documented
@@ -47,14 +47,35 @@ inductive Int : Type where
attribute [extern "lean_nat_to_int"] Int.ofNat
attribute [extern "lean_int_neg_succ_of_nat"] Int.negSucc
instance : Coe Nat Int := Int.ofNat
instance : NatCast Int where natCast n := Int.ofNat n
instance instOfNat : OfNat Int n where
ofNat := Int.ofNat n
namespace Int
/--
`-[n+1]` is suggestive notation for `negSucc n`, which is the second constructor of
`Int` for making strictly negative numbers by mapping `n : Nat` to `-(n + 1)`.
-/
scoped notation "-[" n "+1]" => negSucc n
instance : Inhabited Int := ofNat 0
@[simp] theorem default_eq_zero : default = (0 : Int) := rfl
protected theorem zero_ne_one : (0 : Int) 1 := nofun
/-! ## Coercions -/
@[simp] theorem ofNat_eq_coe : Int.ofNat n = Nat.cast n := rfl
@[simp] theorem ofNat_zero : ((0 : Nat) : Int) = 0 := rfl
@[simp] theorem ofNat_one : ((1 : Nat) : Int) = 1 := rfl
theorem ofNat_two : ((2 : Nat) : Int) = 2 := rfl
/-- Negation of a natural number. -/
def negOfNat : Nat Int
| 0 => 0
@@ -100,10 +121,10 @@ set_option bootstrap.genMatcherCode 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))
| ofNat m, ofNat n => ofNat (m + n)
| ofNat m, -[n +1] => subNatNat m (succ n)
| -[m +1], ofNat n => subNatNat n (succ m)
| -[m +1], -[n +1] => negSucc (succ (m + n))
instance : Add Int where
add := Int.add
@@ -121,10 +142,10 @@ set_option bootstrap.genMatcherCode 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)
| ofNat m, ofNat n => ofNat (m * n)
| ofNat m, -[n +1] => negOfNat (m * succ n)
| -[m +1], ofNat n => negOfNat (succ m * n)
| -[m +1], -[n +1] => ofNat (succ m * succ n)
instance : Mul Int where
mul := Int.mul
@@ -139,8 +160,7 @@ instance : Mul Int where
Implemented by efficient native code. -/
@[extern "lean_int_sub"]
protected def sub (m n : @& Int) : Int :=
m + (- n)
protected def sub (m n : @& Int) : Int := m + (- n)
instance : Sub Int where
sub := Int.sub
@@ -178,11 +198,11 @@ protected def decEq (a b : @& Int) : Decidable (a = b) :=
| 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
| ofNat _, -[_ +1] => isFalse <| fun h => Int.noConfusion h
| -[_ +1], ofNat _ => isFalse <| fun h => Int.noConfusion h
| -[a +1], -[b +1] => match decEq a b with
| isTrue h => isTrue <| h rfl
| isFalse h => isFalse <| fun h' => Int.noConfusion h' (fun h' => absurd h' h)
| ofNat _, negSucc _ => isFalse <| fun h => Int.noConfusion h
| negSucc _, ofNat _ => isFalse <| fun h => Int.noConfusion h
instance : DecidableEq Int := Int.decEq
@@ -199,8 +219,8 @@ set_option bootstrap.genMatcherCode 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 _ => isFalse <| fun h => nomatch h
| ofNat m => isTrue <| NonNeg.mk m
| -[_ +1] => isFalse <| fun h => nomatch h
/-- Decides whether `a ≤ b`.
@@ -241,85 +261,21 @@ set_option bootstrap.genMatcherCode false in
@[extern "lean_nat_abs"]
def natAbs (m : @& Int) : Nat :=
match m with
| ofNat m => m
| negSucc m => m.succ
| ofNat m => m
| -[m +1] => m.succ
/-- Integer division. This function uses the
[*"T-rounding"*][t-rounding] (**T**runcation-rounding) convention,
meaning that it rounds toward zero. Also note that division by zero
is defined to equal zero.
/-! ## sign -/
The relation between integer division and modulo is found in [the
`Int.mod_add_div` theorem in std][theo mod_add_div] which states
that `a % b + b * (a / b) = a`, unconditionally.
/--
Returns the "sign" of the integer as another integer: `1` for positive numbers,
`-1` for negative numbers, and `0` for `0`.
-/
def sign : Int Int
| Int.ofNat (succ _) => 1
| Int.ofNat 0 => 0
| -[_+1] => -1
[t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
[theo mod_add_div]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
Examples:
```
#eval (7 : Int) / (0 : Int) -- 0
#eval (0 : Int) / (7 : Int) -- 0
#eval (12 : Int) / (6 : Int) -- 2
#eval (12 : Int) / (-6 : Int) -- -2
#eval (-12 : Int) / (6 : Int) -- -2
#eval (-12 : Int) / (-6 : Int) -- 2
#eval (12 : Int) / (7 : Int) -- 1
#eval (12 : Int) / (-7 : Int) -- -1
#eval (-12 : Int) / (7 : Int) -- -1
#eval (-12 : Int) / (-7 : Int) -- 1
```
Implemented by efficient native code. -/
@[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)
instance : Div Int where
div := Int.div
/-- Integer modulo. This function uses the
[*"T-rounding"*][t-rounding] (**T**runcation-rounding) convention
to pair with `Int.div`, meaning that `a % b + b * (a / b) = a`
unconditionally (see [`Int.mod_add_div`][theo mod_add_div]). In
particular, `a % 0 = a`.
[t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
[theo mod_add_div]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
Examples:
```
#eval (7 : Int) % (0 : Int) -- 7
#eval (0 : Int) % (7 : Int) -- 0
#eval (12 : Int) % (6 : Int) -- 0
#eval (12 : Int) % (-6 : Int) -- 0
#eval (-12 : Int) % (6 : Int) -- 0
#eval (-12 : Int) % (-6 : Int) -- 0
#eval (12 : Int) % (7 : Int) -- 5
#eval (12 : Int) % (-7 : Int) -- 5
#eval (-12 : Int) % (7 : Int) -- 2
#eval (-12 : Int) % (-7 : Int) -- 2
```
Implemented by efficient native code. -/
@[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 : Mod Int where
mod := Int.mod
/-! ## Conversion -/
/-- Turns an integer into a natural number, negative numbers become
`0`.
@@ -334,6 +290,25 @@ def toNat : Int → Nat
| ofNat n => n
| negSucc _ => 0
/--
* If `n : Nat`, then `int.toNat' n = some n`
* If `n : Int` is negative, then `int.toNat' n = none`.
-/
def toNat' : Int Option Nat
| (n : Nat) => some n
| -[_+1] => none
/-! ## divisibility -/
/--
Divisibility of integers. `a b` (typed as `\|`) says that
there is some `c` such that `b = a * c`.
-/
instance : Dvd Int where
dvd a b := Exists (fun c => b = a * c)
/-! ## Powers -/
/-- Power of an integer to some natural number.
```
@@ -359,3 +334,27 @@ instance : Min Int := minOfLe
instance : Max Int := maxOfLe
end Int
/--
The canonical homomorphism `Int → R`.
In most use cases `R` will have a ring structure and this will be a ring homomorphism.
-/
class IntCast (R : Type u) where
/-- The canonical map `Int → R`. -/
protected intCast : Int R
instance : IntCast Int where intCast n := n
/--
Apply the canonical homomorphism from `Int` to a type `R` from an `IntCast R` instance.
In Mathlib there will be such a homomorphism whenever `R` is an additive group with a `1`.
-/
@[coe, reducible, match_pattern] protected def Int.cast {R : Type u} [IntCast R] : Int R :=
IntCast.intCast
-- see the notes about coercions into arbitrary types in the module doc-string
instance [IntCast R] : CoeTail Int R where coe := Int.cast
-- see the notes about coercions into arbitrary types in the module doc-string
instance [IntCast R] : CoeHTCT Int R where coe := Int.cast

View File

@@ -0,0 +1,50 @@
/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
prelude
import Init.Data.Int.Basic
import Init.Data.Nat.Bitwise
namespace Int
/-! ## bit operations -/
/--
Bitwise not
Interprets the integer as an infinite sequence of bits in two's complement
and complements each bit.
```
~~~(0:Int) = -1
~~~(1:Int) = -2
~~~(-1:Int) = 0
```
-/
protected def not : Int -> Int
| Int.ofNat n => Int.negSucc n
| Int.negSucc n => Int.ofNat n
instance : Complement Int := .not
/--
Bitwise shift right.
Conceptually, this treats the integer as an infinite sequence of bits in two's
complement and shifts the value to the right.
```lean
( 0b0111:Int) >>> 1 = 0b0011
( 0b1000:Int) >>> 1 = 0b0100
(-0b1000:Int) >>> 1 = -0b0100
(-0b0111:Int) >>> 1 = -0b0100
```
-/
protected def shiftRight : Int Nat Int
| Int.ofNat n, s => Int.ofNat (n >>> s)
| Int.negSucc n, s => Int.negSucc (n >>> s)
instance : HShiftRight Int Nat Int := .shiftRight
end Int

View File

@@ -0,0 +1,159 @@
/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Mario Carneiro
-/
prelude
import Init.Data.Int.Basic
open Nat
namespace Int
/-! ## Quotient and remainder
There are three main conventions for integer division,
referred here as the E, F, T rounding conventions.
All three pairs satisfy the identity `x % y + (x / y) * y = x` unconditionally,
and satisfy `x / 0 = 0` and `x % 0 = x`.
-/
/-! ### T-rounding division -/
/--
`div` uses the [*"T-rounding"*][t-rounding]
(**T**runcation-rounding) convention, meaning that it rounds toward
zero. Also note that division by zero is defined to equal zero.
The relation between integer division and modulo is found in
`Int.mod_add_div` which states that
`a % b + b * (a / b) = a`, unconditionally.
[t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862 [theo
mod_add_div]:
https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
Examples:
```
#eval (7 : Int) / (0 : Int) -- 0
#eval (0 : Int) / (7 : Int) -- 0
#eval (12 : Int) / (6 : Int) -- 2
#eval (12 : Int) / (-6 : Int) -- -2
#eval (-12 : Int) / (6 : Int) -- -2
#eval (-12 : Int) / (-6 : Int) -- 2
#eval (12 : Int) / (7 : Int) -- 1
#eval (12 : Int) / (-7 : Int) -- -1
#eval (-12 : Int) / (7 : Int) -- -1
#eval (-12 : Int) / (-7 : Int) -- 1
```
Implemented by efficient native code.
-/
@[extern "lean_int_div"]
def div : (@& Int) (@& Int) Int
| ofNat m, ofNat n => ofNat (m / n)
| ofNat m, -[n +1] => -ofNat (m / succ n)
| -[m +1], ofNat n => -ofNat (succ m / n)
| -[m +1], -[n +1] => ofNat (succ m / succ n)
/-- Integer modulo. This function uses the
[*"T-rounding"*][t-rounding] (**T**runcation-rounding) convention
to pair with `Int.div`, meaning that `a % b + b * (a / b) = a`
unconditionally (see [`Int.mod_add_div`][theo mod_add_div]). In
particular, `a % 0 = a`.
[t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
[theo mod_add_div]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
Examples:
```
#eval (7 : Int) % (0 : Int) -- 7
#eval (0 : Int) % (7 : Int) -- 0
#eval (12 : Int) % (6 : Int) -- 0
#eval (12 : Int) % (-6 : Int) -- 0
#eval (-12 : Int) % (6 : Int) -- 0
#eval (-12 : Int) % (-6 : Int) -- 0
#eval (12 : Int) % (7 : Int) -- 5
#eval (12 : Int) % (-7 : Int) -- 5
#eval (-12 : Int) % (7 : Int) -- 2
#eval (-12 : Int) % (-7 : Int) -- 2
```
Implemented by efficient native code. -/
@[extern "lean_int_mod"]
def mod : (@& Int) (@& Int) Int
| ofNat m, ofNat n => ofNat (m % n)
| ofNat m, -[n +1] => ofNat (m % succ n)
| -[m +1], ofNat n => -ofNat (succ m % n)
| -[m +1], -[n +1] => -ofNat (succ m % succ n)
/-! ### F-rounding division
This pair satisfies `fdiv x y = floor (x / y)`.
-/
/--
Integer division. This version of division uses the F-rounding convention
(flooring division), in which `Int.fdiv x y` satisfies `fdiv x y = floor (x / y)`
and `Int.fmod` is the unique function satisfying `fmod x y + (fdiv x y) * y = x`.
-/
def fdiv : Int Int Int
| 0, _ => 0
| ofNat m, ofNat n => ofNat (m / n)
| ofNat (succ m), -[n+1] => -[m / succ n +1]
| -[_+1], 0 => 0
| -[m+1], ofNat (succ n) => -[m / succ n +1]
| -[m+1], -[n+1] => ofNat (succ m / succ n)
/--
Integer modulus. This version of `Int.mod` uses the F-rounding convention
(flooring division), in which `Int.fdiv x y` satisfies `fdiv x y = floor (x / y)`
and `Int.fmod` is the unique function satisfying `fmod x y + (fdiv x y) * y = x`.
-/
def fmod : Int Int Int
| 0, _ => 0
| ofNat m, ofNat n => ofNat (m % n)
| ofNat (succ m), -[n+1] => subNatNat (m % succ n) n
| -[m+1], ofNat n => subNatNat n (succ (m % n))
| -[m+1], -[n+1] => -ofNat (succ m % succ n)
/-! ### E-rounding division
This pair satisfies `0 ≤ mod x y < natAbs y` for `y ≠ 0`.
-/
/--
Integer division. This version of `Int.div` uses the E-rounding convention
(euclidean division), in which `Int.emod x y` satisfies `0 ≤ mod x y < natAbs y` for `y ≠ 0`
and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
-/
def ediv : Int Int Int
| ofNat m, ofNat n => ofNat (m / n)
| ofNat m, -[n+1] => -ofNat (m / succ n)
| -[_+1], 0 => 0
| -[m+1], ofNat (succ n) => -[m / succ n +1]
| -[m+1], -[n+1] => ofNat (succ (m / succ n))
/--
Integer modulus. This version of `Int.mod` uses the E-rounding convention
(euclidean division), in which `Int.emod x y` satisfies `0 ≤ emod x y < natAbs y` for `y ≠ 0`
and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
-/
def emod : Int Int Int
| ofNat m, n => ofNat (m % natAbs n)
| -[m+1], n => subNatNat (natAbs n) (succ (m % natAbs n))
/--
The Div and Mod syntax uses ediv and emod for compatibility with SMTLIb and mathematical
reasoning tends to be easier.
-/
instance : Div Int where
div := Int.ediv
instance : Mod Int where
mod := Int.emod
end Int

View File

@@ -0,0 +1,347 @@
/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Mario Carneiro
-/
prelude
import Init.Data.Int.DivMod
import Init.Data.Int.Order
import Init.Data.Nat.Dvd
import Init.RCases
import Init.TacticsExtra
/-!
# Lemmas about integer division needed to bootstrap `omega`.
-/
open Nat (succ)
namespace Int
/-! ### `/` -/
@[simp] theorem ofNat_ediv (m n : Nat) : ((m / n) : Int) = m / n := rfl
@[simp] theorem zero_ediv : b : Int, 0 / b = 0
| ofNat _ => show ofNat _ = _ by simp
| -[_+1] => show -ofNat _ = _ by simp
@[simp] protected theorem ediv_zero : a : Int, a / 0 = 0
| ofNat _ => show ofNat _ = _ by simp
| -[_+1] => rfl
@[simp] protected theorem ediv_neg : a b : Int, a / (-b) = -(a / b)
| ofNat m, 0 => show ofNat (m / 0) = -(m / 0) by rw [Nat.div_zero]; rfl
| ofNat m, -[n+1] => (Int.neg_neg _).symm
| ofNat m, succ n | -[m+1], 0 | -[m+1], succ n | -[m+1], -[n+1] => rfl
protected theorem div_def (a b : Int) : a / b = Int.ediv a b := rfl
theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c 0) : (a + b * c) / c = a / c + b :=
suffices {{a b c : Int}}, 0 < c (a + b * c).ediv c = a.ediv c + b from
match Int.lt_trichotomy c 0 with
| Or.inl hlt => by
rw [ Int.neg_inj, Int.ediv_neg, Int.neg_add, Int.ediv_neg, Int.neg_mul_neg]
exact this (Int.neg_pos_of_neg hlt)
| Or.inr (Or.inl HEq) => absurd HEq H
| Or.inr (Or.inr hgt) => this hgt
suffices {k n : Nat} {a : Int}, (a + n * k.succ).ediv k.succ = a.ediv k.succ + n from
fun a b c H => match c, eq_succ_of_zero_lt H, b with
| _, _, rfl, ofNat _ => this
| _, k, rfl, -[n+1] => show (a - n.succ * k.succ).ediv k.succ = a.ediv k.succ - n.succ by
rw [ Int.add_sub_cancel (ediv ..), this, Int.sub_add_cancel]
fun {k n} => @fun
| ofNat m => congrArg ofNat <| Nat.add_mul_div_right _ _ k.succ_pos
| -[m+1] => by
show ((n * k.succ : Nat) - m.succ : Int).ediv k.succ = n - (m / k.succ + 1 : Nat)
if h : m < n * k.succ then
rw [ Int.ofNat_sub h, Int.ofNat_sub ((Nat.div_lt_iff_lt_mul k.succ_pos).2 h)]
apply congrArg ofNat
rw [Nat.mul_comm, Nat.mul_sub_div]; rwa [Nat.mul_comm]
else
have h := Nat.not_lt.1 h
have H {a b : Nat} (h : a b) : (a : Int) + -((b : Int) + 1) = -[b - a +1] := by
rw [negSucc_eq, Int.ofNat_sub h]
simp only [Int.sub_eq_add_neg, Int.neg_add, Int.neg_neg, Int.add_left_comm, Int.add_assoc]
show ediv ((n * succ k) + -((m : Int) + 1)) (succ k) = n + -((m / succ k) + 1 : Int)
rw [H h, H ((Nat.le_div_iff_mul_le k.succ_pos).2 h)]
apply congrArg negSucc
rw [Nat.mul_comm, Nat.sub_mul_div]; rwa [Nat.mul_comm]
theorem add_ediv_of_dvd_right {a b c : Int} (H : c b) : (a + b) / c = a / c + b / c :=
if h : c = 0 then by simp [h] else by
let k, hk := H
rw [hk, Int.mul_comm c k, Int.add_mul_ediv_right _ _ h,
Int.zero_add (k * c), Int.add_mul_ediv_right _ _ h, Int.zero_ediv, Int.zero_add]
theorem add_ediv_of_dvd_left {a b c : Int} (H : c a) : (a + b) / c = a / c + b / c := by
rw [Int.add_comm, Int.add_ediv_of_dvd_right H, Int.add_comm]
@[simp] theorem mul_ediv_cancel (a : Int) {b : Int} (H : b 0) : (a * b) / b = a := by
have := Int.add_mul_ediv_right 0 a H
rwa [Int.zero_add, Int.zero_ediv, Int.zero_add] at this
@[simp] theorem mul_ediv_cancel_left (b : Int) (H : a 0) : (a * b) / a = b :=
Int.mul_comm .. Int.mul_ediv_cancel _ H
theorem div_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : a / b 0 a 0 := by
rw [Int.div_def]
match b, h with
| Int.ofNat (b+1), _ =>
rcases a with a <;> simp [Int.ediv]
exact decide_eq_decide.mp rfl
/-! ### mod -/
theorem mod_def' (m n : Int) : m % n = emod m n := rfl
theorem ofNat_mod (m n : Nat) : ((m % n) : Int) = mod m n := rfl
theorem ofNat_mod_ofNat (m n : Nat) : (m % n : Int) = (m % n) := rfl
@[simp] theorem ofNat_emod (m n : Nat) : ((m % n) : Int) = m % n := rfl
@[simp] theorem zero_emod (b : Int) : 0 % b = 0 := by simp [mod_def', emod]
@[simp] theorem emod_zero : a : Int, a % 0 = a
| ofNat _ => congrArg ofNat <| Nat.mod_zero _
| -[_+1] => congrArg negSucc <| Nat.mod_zero _
theorem emod_add_ediv : a b : Int, a % b + b * (a / b) = a
| ofNat _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..
| ofNat m, -[n+1] => by
show (m % succ n + -(succ n) * -(m / succ n) : Int) = m
rw [Int.neg_mul_neg]; exact congrArg ofNat <| Nat.mod_add_div ..
| -[_+1], 0 => by rw [emod_zero]; rfl
| -[m+1], succ n => aux m n.succ
| -[m+1], -[n+1] => aux m n.succ
where
aux (m n : Nat) : n - (m % n + 1) - (n * (m / n) + n) = -[m+1] := by
rw [ ofNat_emod, ofNat_ediv, Int.sub_sub, negSucc_eq, Int.sub_sub n,
Int.neg_neg (_-_), Int.neg_sub, Int.sub_sub_self, Int.add_right_comm]
exact congrArg (fun x => -(ofNat x + 1)) (Nat.mod_add_div ..)
theorem ediv_add_emod (a b : Int) : b * (a / b) + a % b = a :=
(Int.add_comm ..).trans (emod_add_ediv ..)
theorem emod_def (a b : Int) : a % b = a - b * (a / b) := by
rw [ Int.add_sub_cancel (a % b), emod_add_ediv]
theorem emod_nonneg : (a : Int) {b : Int}, b 0 0 a % b
| ofNat _, _, _ => ofNat_zero_le _
| -[_+1], _, H => Int.sub_nonneg_of_le <| ofNat_le.2 <| Nat.mod_lt _ (natAbs_pos.2 H)
theorem emod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a % b < b :=
match a, b, eq_succ_of_zero_lt H with
| ofNat _, _, _, rfl => ofNat_lt.2 (Nat.mod_lt _ (Nat.succ_pos _))
| -[_+1], _, _, rfl => Int.sub_lt_self _ (ofNat_lt.2 <| Nat.succ_pos _)
theorem mul_ediv_self_le {x k : Int} (h : k 0) : k * (x / k) x :=
calc k * (x / k)
_ k * (x / k) + x % k := Int.le_add_of_nonneg_right (emod_nonneg x h)
_ = x := ediv_add_emod _ _
theorem lt_mul_ediv_self_add {x k : Int} (h : 0 < k) : x < k * (x / k) + k :=
calc x
_ = k * (x / k) + x % k := (ediv_add_emod _ _).symm
_ < k * (x / k) + k := Int.add_lt_add_left (emod_lt_of_pos x h) _
theorem emod_add_ediv' (m k : Int) : m % k + m / k * k = m := by
rw [Int.mul_comm]; apply emod_add_ediv
@[simp] theorem add_mul_emod_self {a b c : Int} : (a + b * c) % c = a % c :=
if cz : c = 0 then by
rw [cz, Int.mul_zero, Int.add_zero]
else by
rw [Int.emod_def, Int.emod_def, Int.add_mul_ediv_right _ _ cz, Int.add_comm _ b,
Int.mul_add, Int.mul_comm, Int.sub_sub, Int.add_sub_cancel]
@[simp] theorem add_mul_emod_self_left (a b c : Int) : (a + b * c) % b = a % b := by
rw [Int.mul_comm, Int.add_mul_emod_self]
@[simp] theorem add_emod_self {a b : Int} : (a + b) % b = a % b := by
have := add_mul_emod_self_left a b 1; rwa [Int.mul_one] at this
@[simp] theorem add_emod_self_left {a b : Int} : (a + b) % a = b % a := by
rw [Int.add_comm, Int.add_emod_self]
theorem neg_emod {a b : Int} : -a % b = (b - a) % b := by
rw [ add_emod_self_left]; rfl
@[simp] theorem emod_add_emod (m n k : Int) : (m % n + k) % n = (m + k) % n := by
have := (add_mul_emod_self_left (m % n + k) n (m / n)).symm
rwa [Int.add_right_comm, emod_add_ediv] at this
@[simp] theorem add_emod_emod (m n k : Int) : (m + n % k) % k = (m + n) % k := by
rw [Int.add_comm, emod_add_emod, Int.add_comm]
theorem add_emod (a b n : Int) : (a + b) % n = (a % n + b % n) % n := by
rw [add_emod_emod, emod_add_emod]
theorem add_emod_eq_add_emod_right {m n k : Int} (i : Int)
(H : m % n = k % n) : (m + i) % n = (k + i) % n := by
rw [ emod_add_emod, emod_add_emod k, H]
theorem emod_add_cancel_right {m n k : Int} (i) : (m + i) % n = (k + i) % n m % n = k % n :=
fun H => by
have := add_emod_eq_add_emod_right (-i) H
rwa [Int.add_neg_cancel_right, Int.add_neg_cancel_right] at this,
add_emod_eq_add_emod_right _
@[simp] theorem mul_emod_left (a b : Int) : (a * b) % b = 0 := by
rw [ Int.zero_add (a * b), Int.add_mul_emod_self, Int.zero_emod]
@[simp] theorem mul_emod_right (a b : Int) : (a * b) % a = 0 := by
rw [Int.mul_comm, mul_emod_left]
theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
conv => lhs; rw [
emod_add_ediv a n, emod_add_ediv' b n, Int.add_mul, Int.mul_add, Int.mul_add,
Int.mul_assoc, Int.mul_assoc, Int.mul_add n _ _, add_mul_emod_self_left,
Int.mul_assoc, add_mul_emod_self]
@[local simp] theorem emod_self {a : Int} : a % a = 0 := by
have := mul_emod_left 1 a; rwa [Int.one_mul] at this
@[simp] theorem emod_emod_of_dvd (n : Int) {m k : Int}
(h : m k) : (n % k) % m = n % m := by
conv => rhs; rw [ emod_add_ediv n k]
match k, h with
| _, t, rfl => rw [Int.mul_assoc, add_mul_emod_self_left]
@[simp] theorem emod_emod (a b : Int) : (a % b) % b = a % b := by
conv => rhs; rw [ emod_add_ediv a b, add_mul_emod_self_left]
theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by
apply (emod_add_cancel_right b).mp
rw [Int.sub_add_cancel, Int.add_emod_emod, Int.sub_add_cancel, emod_emod]
/-! ### properties of `/` and `%` -/
theorem mul_ediv_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : b * (a / b) = a := by
have := emod_add_ediv a b; rwa [H, Int.zero_add] at this
theorem ediv_mul_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : a / b * b = a := by
rw [Int.mul_comm, mul_ediv_cancel_of_emod_eq_zero H]
/-! ### dvd -/
protected theorem dvd_zero (n : Int) : n 0 := 0, (Int.mul_zero _).symm
protected theorem dvd_refl (n : Int) : n n := 1, (Int.mul_one _).symm
protected theorem one_dvd (n : Int) : 1 n := n, (Int.one_mul n).symm
protected theorem dvd_trans : {a b c : Int}, a b b c a c
| _, _, _, d, rfl, e, rfl => d * e, by rw [Int.mul_assoc]
@[simp] protected theorem zero_dvd {n : Int} : 0 n n = 0 :=
fun k, e => by rw [e, Int.zero_mul], fun h => h.symm Int.dvd_refl _
protected theorem neg_dvd {a b : Int} : -a b a b := by
constructor <;> exact fun k, e =>
-k, by simp [e, Int.neg_mul, Int.mul_neg, Int.neg_neg]
protected theorem dvd_neg {a b : Int} : a -b a b := by
constructor <;> exact fun k, e =>
-k, by simp [ e, Int.neg_mul, Int.mul_neg, Int.neg_neg]
protected theorem dvd_mul_right (a b : Int) : a a * b := _, rfl
protected theorem dvd_mul_left (a b : Int) : b a * b := _, Int.mul_comm ..
protected theorem dvd_add : {a b c : Int}, a b a c a b + c
| _, _, _, d, rfl, e, rfl => d + e, by rw [Int.mul_add]
protected theorem dvd_sub : {a b c : Int}, a b a c a b - c
| _, _, _, d, rfl, e, rfl => d - e, by rw [Int.mul_sub]
theorem ofNat_dvd {m n : Nat} : (m : Int) n m n := by
refine fun a, ae => ?_, fun k, e => k, by rw [e, Int.ofNat_mul]
match Int.le_total a 0 with
| .inl h =>
have := ae.symm Int.mul_nonpos_of_nonneg_of_nonpos (ofNat_zero_le _) h
rw [Nat.le_antisymm (ofNat_le.1 this) (Nat.zero_le _)]
apply Nat.dvd_zero
| .inr h => match a, eq_ofNat_of_zero_le h with
| _, k, rfl => exact k, Int.ofNat.inj ae
@[simp] theorem natAbs_dvd_natAbs {a b : Int} : natAbs a natAbs b a b := by
refine fun k, hk => ?_, fun k, hk => natAbs k, hk.symm natAbs_mul a k
rw [ natAbs_ofNat k, natAbs_mul, natAbs_eq_natAbs_iff] at hk
cases hk <;> subst b
· apply Int.dvd_mul_right
· rw [ Int.mul_neg]; apply Int.dvd_mul_right
theorem ofNat_dvd_left {n : Nat} {z : Int} : (n : Int) z n z.natAbs := by
rw [ natAbs_dvd_natAbs, natAbs_ofNat]
theorem dvd_of_emod_eq_zero {a b : Int} (H : b % a = 0) : a b :=
b / a, (mul_ediv_cancel_of_emod_eq_zero H).symm
theorem dvd_emod_sub_self {x : Int} {m : Nat} : (m : Int) x % m - x := by
apply dvd_of_emod_eq_zero
simp [sub_emod]
theorem emod_eq_zero_of_dvd : {a b : Int}, a b b % a = 0
| _, _, _, rfl => mul_emod_right ..
theorem dvd_iff_emod_eq_zero (a b : Int) : a b b % a = 0 :=
emod_eq_zero_of_dvd, dvd_of_emod_eq_zero
theorem emod_pos_of_not_dvd {a b : Int} (h : ¬ a b) : a = 0 0 < b % a := by
rw [dvd_iff_emod_eq_zero] at h
if w : a = 0 then simp_all
else exact Or.inr (Int.lt_iff_le_and_ne.mpr emod_nonneg b w, Ne.symm h)
instance decidableDvd : DecidableRel (α := Int) (· ·) := fun _ _ =>
decidable_of_decidable_of_iff (dvd_iff_emod_eq_zero ..).symm
protected theorem ediv_mul_cancel {a b : Int} (H : b a) : a / b * b = a :=
ediv_mul_cancel_of_emod_eq_zero (emod_eq_zero_of_dvd H)
protected theorem mul_ediv_cancel' {a b : Int} (H : a b) : a * (b / a) = b := by
rw [Int.mul_comm, Int.ediv_mul_cancel H]
protected theorem mul_ediv_assoc (a : Int) : {b c : Int}, c b (a * b) / c = a * (b / c)
| _, c, d, rfl =>
if cz : c = 0 then by simp [cz, Int.mul_zero] else by
rw [Int.mul_left_comm, Int.mul_ediv_cancel_left _ cz, Int.mul_ediv_cancel_left _ cz]
protected theorem mul_ediv_assoc' (b : Int) {a c : Int}
(h : c a) : (a * b) / c = a / c * b := by
rw [Int.mul_comm, Int.mul_ediv_assoc _ h, Int.mul_comm]
theorem neg_ediv_of_dvd : {a b : Int}, b a (-a) / b = -(a / b)
| _, b, c, rfl => by if bz : b = 0 then simp [bz] else
rw [Int.neg_mul_eq_mul_neg, Int.mul_ediv_cancel_left _ bz, Int.mul_ediv_cancel_left _ bz]
theorem sub_ediv_of_dvd (a : Int) {b c : Int}
(hcb : c b) : (a - b) / c = a / c - b / c := by
rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.add_ediv_of_dvd_right (Int.dvd_neg.2 hcb)]
congr; exact Int.neg_ediv_of_dvd hcb
/-!
# `bmod` ("balanced" mod)
We use balanced mod in the omega algorithm,
to make ±1 coefficients appear in equations without them.
-/
/--
Balanced mod, taking values in the range [- m/2, (m - 1)/2].
-/
def bmod (x : Int) (m : Nat) : Int :=
let r := x % m
if r < (m + 1) / 2 then
r
else
r - m
@[simp] theorem bmod_emod : bmod x m % m = x % m := by
dsimp [bmod]
split <;> simp [Int.sub_emod]

View File

@@ -0,0 +1,17 @@
/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
prelude
import Init.Data.Int.Basic
import Init.Data.Nat.Gcd
namespace Int
/-! ## gcd -/
/-- Computes the greatest common divisor of two integers, as a `Nat`. -/
def gcd (m n : Int) : Nat := m.natAbs.gcd n.natAbs
end Int

View File

@@ -0,0 +1,500 @@
/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
-/
prelude
import Init.Data.Int.Basic
import Init.Conv
import Init.PropLemmas
namespace Int
open Nat
/-! ## Definitions of basic functions -/
theorem subNatNat_of_sub_eq_zero {m n : Nat} (h : n - m = 0) : subNatNat m n = (m - n) := by
rw [subNatNat, h, ofNat_eq_coe]
theorem subNatNat_of_sub_eq_succ {m n k : Nat} (h : n - m = succ k) : subNatNat m n = -[k+1] := by
rw [subNatNat, h]
@[simp] protected theorem neg_zero : -(0:Int) = 0 := rfl
theorem ofNat_add (n m : Nat) : ((n + m) : Int) = n + m := rfl
theorem ofNat_mul (n m : Nat) : ((n * m) : Int) = n * m := rfl
theorem ofNat_succ (n : Nat) : (succ n : Int) = n + 1 := rfl
@[local simp] theorem neg_ofNat_zero : -((0 : Nat) : Int) = 0 := rfl
@[local simp] theorem neg_ofNat_succ (n : Nat) : -(succ n : Int) = -[n+1] := rfl
@[local simp] theorem neg_negSucc (n : Nat) : -(-[n+1]) = succ n := rfl
theorem negSucc_coe (n : Nat) : -[n+1] = -(n + 1) := rfl
theorem negOfNat_eq : negOfNat n = -ofNat n := rfl
/-! ## These are only for internal use -/
@[simp] theorem add_def {a b : Int} : Int.add a b = a + b := rfl
@[local simp] theorem ofNat_add_ofNat (m n : Nat) : (m + n : Int) = (m + n) := rfl
@[local simp] theorem ofNat_add_negSucc (m n : Nat) : m + -[n+1] = subNatNat m (succ n) := rfl
@[local simp] theorem negSucc_add_ofNat (m n : Nat) : -[m+1] + n = subNatNat n (succ m) := rfl
@[local simp] theorem negSucc_add_negSucc (m n : Nat) : -[m+1] + -[n+1] = -[succ (m + n) +1] := rfl
@[simp] theorem mul_def {a b : Int} : Int.mul a b = a * b := rfl
@[local simp] theorem ofNat_mul_ofNat (m n : Nat) : (m * n : Int) = (m * n) := rfl
@[local simp] theorem ofNat_mul_negSucc' (m n : Nat) : m * -[n+1] = negOfNat (m * succ n) := rfl
@[local simp] theorem negSucc_mul_ofNat' (m n : Nat) : -[m+1] * n = negOfNat (succ m * n) := rfl
@[local simp] theorem negSucc_mul_negSucc' (m n : Nat) :
-[m+1] * -[n+1] = ofNat (succ m * succ n) := rfl
/- ## some basic functions and properties -/
theorem ofNat_inj : ((m : Nat) : Int) = (n : Nat) m = n := ofNat.inj, congrArg _
theorem ofNat_eq_zero : ((n : Nat) : Int) = 0 n = 0 := ofNat_inj
theorem ofNat_ne_zero : ((n : Nat) : Int) 0 n 0 := not_congr ofNat_eq_zero
theorem negSucc_inj : negSucc m = negSucc n m = n := negSucc.inj, fun H => by simp [H]
theorem negSucc_eq (n : Nat) : -[n+1] = -((n : Int) + 1) := rfl
@[simp] theorem negSucc_ne_zero (n : Nat) : -[n+1] 0 := nofun
@[simp] theorem zero_ne_negSucc (n : Nat) : 0 -[n+1] := nofun
@[simp] theorem Nat.cast_ofNat_Int :
(Nat.cast (no_index (OfNat.ofNat n)) : Int) = OfNat.ofNat n := rfl
/- ## neg -/
@[simp] protected theorem neg_neg : a : Int, -(-a) = a
| 0 => rfl
| succ _ => rfl
| -[_+1] => rfl
protected theorem neg_inj {a b : Int} : -a = -b a = b :=
fun h => by rw [ Int.neg_neg a, Int.neg_neg b, h], congrArg _
@[simp] protected theorem neg_eq_zero : -a = 0 a = 0 := Int.neg_inj (b := 0)
protected theorem neg_ne_zero : -a 0 a 0 := not_congr Int.neg_eq_zero
protected theorem sub_eq_add_neg {a b : Int} : a - b = a + -b := rfl
theorem add_neg_one (i : Int) : i + -1 = i - 1 := rfl
/- ## basic properties of subNatNat -/
-- @[elabAsElim] -- TODO(Mario): unexpected eliminator resulting type
theorem subNatNat_elim (m n : Nat) (motive : Nat Nat Int Prop)
(hp : i n, motive (n + i) n i)
(hn : i m, motive m (m + i + 1) -[i+1]) :
motive m n (subNatNat m n) := by
unfold subNatNat
match h : n - m with
| 0 =>
have k, h := Nat.le.dest (Nat.le_of_sub_eq_zero h)
rw [h.symm, Nat.add_sub_cancel_left]; apply hp
| succ k =>
rw [Nat.sub_eq_iff_eq_add (Nat.le_of_lt (Nat.lt_of_sub_eq_succ h))] at h
rw [h, Nat.add_comm]; apply hn
theorem subNatNat_add_left : subNatNat (m + n) m = n := by
unfold subNatNat
rw [Nat.sub_eq_zero_of_le (Nat.le_add_right ..), Nat.add_sub_cancel_left, ofNat_eq_coe]
theorem subNatNat_add_right : subNatNat m (m + n + 1) = negSucc n := by
simp [subNatNat, Nat.add_assoc, Nat.add_sub_cancel_left]
theorem subNatNat_add_add (m n k : Nat) : subNatNat (m + k) (n + k) = subNatNat m n := by
apply subNatNat_elim m n (fun m n i => subNatNat (m + k) (n + k) = i)
focus
intro i j
rw [Nat.add_assoc, Nat.add_comm i k, Nat.add_assoc]
exact subNatNat_add_left
focus
intro i j
rw [Nat.add_assoc j i 1, Nat.add_comm j (i+1), Nat.add_assoc, Nat.add_comm (i+1) (j+k)]
exact subNatNat_add_right
theorem subNatNat_of_le {m n : Nat} (h : n m) : subNatNat m n = (m - n) :=
subNatNat_of_sub_eq_zero (Nat.sub_eq_zero_of_le h)
theorem subNatNat_of_lt {m n : Nat} (h : m < n) : subNatNat m n = -[pred (n - m) +1] :=
subNatNat_of_sub_eq_succ <| (Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)).symm
/- # Additive group properties -/
/- addition -/
protected theorem add_comm : a b : Int, a + b = b + a
| ofNat n, ofNat m => by simp [Nat.add_comm]
| ofNat _, -[_+1] => rfl
| -[_+1], ofNat _ => rfl
| -[_+1], -[_+1] => by simp [Nat.add_comm]
@[simp] protected theorem add_zero : a : Int, a + 0 = a
| ofNat _ => rfl
| -[_+1] => rfl
@[simp] protected theorem zero_add (a : Int) : 0 + a = a := Int.add_comm .. a.add_zero
theorem ofNat_add_negSucc_of_lt (h : m < n.succ) : ofNat m + -[n+1] = -[n - m+1] :=
show subNatNat .. = _ by simp [succ_sub (le_of_lt_succ h), subNatNat]
theorem subNatNat_sub (h : n m) (k : Nat) : subNatNat (m - n) k = subNatNat m (k + n) := by
rwa [ subNatNat_add_add _ _ n, Nat.sub_add_cancel]
theorem subNatNat_add (m n k : Nat) : subNatNat (m + n) k = m + subNatNat n k := by
cases n.lt_or_ge k with
| inl h' =>
simp [subNatNat_of_lt h', succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]
conv => lhs; rw [ Nat.sub_add_cancel (Nat.le_of_lt h')]
apply subNatNat_add_add
| inr h' => simp [subNatNat_of_le h',
subNatNat_of_le (Nat.le_trans h' (le_add_left ..)), Nat.add_sub_assoc h']
theorem subNatNat_add_negSucc (m n k : Nat) :
subNatNat m n + -[k+1] = subNatNat m (n + succ k) := by
have h := Nat.lt_or_ge m n
cases h with
| inr h' =>
rw [subNatNat_of_le h']
simp
rw [subNatNat_sub h', Nat.add_comm]
| inl h' =>
have h₂ : m < n + succ k := Nat.lt_of_lt_of_le h' (le_add_right _ _)
have h₃ : m n + k := le_of_succ_le_succ h₂
rw [subNatNat_of_lt h', subNatNat_of_lt h₂]
simp [Nat.add_comm]
rw [ add_succ, succ_pred_eq_of_pos (Nat.sub_pos_of_lt h'), add_succ, succ_sub h₃,
Nat.pred_succ]
rw [Nat.add_comm n, Nat.add_sub_assoc (Nat.le_of_lt h')]
protected theorem add_assoc : a b c : Int, a + b + c = a + (b + c)
| (m:Nat), (n:Nat), c => aux1 ..
| Nat.cast m, b, Nat.cast k => by
rw [Int.add_comm, aux1, Int.add_comm k, aux1, Int.add_comm b]
| a, (n:Nat), (k:Nat) => by
rw [Int.add_comm, Int.add_comm a, aux1, Int.add_comm a, Int.add_comm k]
| -[m+1], -[n+1], (k:Nat) => aux2 ..
| -[m+1], (n:Nat), -[k+1] => by
rw [Int.add_comm, aux2, Int.add_comm n, aux2, Int.add_comm -[m+1]]
| (m:Nat), -[n+1], -[k+1] => by
rw [Int.add_comm, Int.add_comm m, Int.add_comm m, aux2, Int.add_comm -[k+1]]
| -[m+1], -[n+1], -[k+1] => by
simp [add_succ, Nat.add_comm, Nat.add_left_comm, neg_ofNat_succ]
where
aux1 (m n : Nat) : c : Int, m + n + c = m + (n + c)
| (k:Nat) => by simp [Nat.add_assoc]
| -[k+1] => by simp [subNatNat_add]
aux2 (m n k : Nat) : -[m+1] + -[n+1] + k = -[m+1] + (-[n+1] + k) := by
simp [add_succ]
rw [Int.add_comm, subNatNat_add_negSucc]
simp [add_succ, succ_add, Nat.add_comm]
protected theorem add_left_comm (a b c : Int) : a + (b + c) = b + (a + c) := by
rw [ Int.add_assoc, Int.add_comm a, Int.add_assoc]
protected theorem add_right_comm (a b c : Int) : a + b + c = a + c + b := by
rw [Int.add_assoc, Int.add_comm b, Int.add_assoc]
/- ## negation -/
theorem subNatNat_self : n, subNatNat n n = 0
| 0 => rfl
| succ m => by rw [subNatNat_of_sub_eq_zero (Nat.sub_self ..), Nat.sub_self, ofNat_zero]
attribute [local simp] subNatNat_self
@[local simp] protected theorem add_left_neg : a : Int, -a + a = 0
| 0 => rfl
| succ m => by simp
| -[m+1] => by simp
@[local simp] protected theorem add_right_neg (a : Int) : a + -a = 0 := by
rw [Int.add_comm, Int.add_left_neg]
@[simp] protected theorem neg_eq_of_add_eq_zero {a b : Int} (h : a + b = 0) : -a = b := by
rw [ Int.add_zero (-a), h, Int.add_assoc, Int.add_left_neg, Int.zero_add]
protected theorem eq_neg_of_eq_neg {a b : Int} (h : a = -b) : b = -a := by
rw [h, Int.neg_neg]
protected theorem eq_neg_comm {a b : Int} : a = -b b = -a :=
Int.eq_neg_of_eq_neg, Int.eq_neg_of_eq_neg
protected theorem neg_eq_comm {a b : Int} : -a = b -b = a := by
rw [eq_comm, Int.eq_neg_comm, eq_comm]
protected theorem neg_add_cancel_left (a b : Int) : -a + (a + b) = b := by
rw [ Int.add_assoc, Int.add_left_neg, Int.zero_add]
protected theorem add_neg_cancel_left (a b : Int) : a + (-a + b) = b := by
rw [ Int.add_assoc, Int.add_right_neg, Int.zero_add]
protected theorem add_neg_cancel_right (a b : Int) : a + b + -b = a := by
rw [Int.add_assoc, Int.add_right_neg, Int.add_zero]
protected theorem neg_add_cancel_right (a b : Int) : a + -b + b = a := by
rw [Int.add_assoc, Int.add_left_neg, Int.add_zero]
protected theorem add_left_cancel {a b c : Int} (h : a + b = a + c) : b = c := by
have h₁ : -a + (a + b) = -a + (a + c) := by rw [h]
simp [ Int.add_assoc, Int.add_left_neg, Int.zero_add] at h₁; exact h₁
@[local simp] protected theorem neg_add {a b : Int} : -(a + b) = -a + -b := by
apply Int.add_left_cancel (a := a + b)
rw [Int.add_right_neg, Int.add_comm a, Int.add_assoc, Int.add_assoc b,
Int.add_right_neg, Int.add_zero, Int.add_right_neg]
/- ## subtraction -/
@[simp] theorem negSucc_sub_one (n : Nat) : -[n+1] - 1 = -[n + 1 +1] := rfl
@[simp] protected theorem sub_self (a : Int) : a - a = 0 := by
rw [Int.sub_eq_add_neg, Int.add_right_neg]
@[simp] protected theorem sub_zero (a : Int) : a - 0 = a := by simp [Int.sub_eq_add_neg]
@[simp] protected theorem zero_sub (a : Int) : 0 - a = -a := by simp [Int.sub_eq_add_neg]
protected theorem sub_eq_zero_of_eq {a b : Int} (h : a = b) : a - b = 0 := by
rw [h, Int.sub_self]
protected theorem eq_of_sub_eq_zero {a b : Int} (h : a - b = 0) : a = b := by
have : 0 + b = b := by rw [Int.zero_add]
have : a - b + b = b := by rwa [h]
rwa [Int.sub_eq_add_neg, Int.neg_add_cancel_right] at this
protected theorem sub_eq_zero {a b : Int} : a - b = 0 a = b :=
Int.eq_of_sub_eq_zero, Int.sub_eq_zero_of_eq
protected theorem sub_sub (a b c : Int) : a - b - c = a - (b + c) := by
simp [Int.sub_eq_add_neg, Int.add_assoc]
protected theorem neg_sub (a b : Int) : -(a - b) = b - a := by
simp [Int.sub_eq_add_neg, Int.add_comm]
protected theorem sub_sub_self (a b : Int) : a - (a - b) = b := by
simp [Int.sub_eq_add_neg, Int.add_assoc]
protected theorem sub_neg (a b : Int) : a - -b = a + b := by simp [Int.sub_eq_add_neg]
@[simp] protected theorem sub_add_cancel (a b : Int) : a - b + b = a :=
Int.neg_add_cancel_right a b
@[simp] protected theorem add_sub_cancel (a b : Int) : a + b - b = a :=
Int.add_neg_cancel_right a b
protected theorem add_sub_assoc (a b c : Int) : a + b - c = a + (b - c) := by
rw [Int.sub_eq_add_neg, Int.add_assoc, Int.sub_eq_add_neg]
theorem ofNat_sub (h : m n) : ((n - m : Nat) : Int) = n - m := by
match m with
| 0 => rfl
| succ m =>
show ofNat (n - succ m) = subNatNat n (succ m)
rw [subNatNat, Nat.sub_eq_zero_of_le h]
theorem negSucc_coe' (n : Nat) : -[n+1] = -n - 1 := by
rw [Int.sub_eq_add_neg, Int.neg_add]; rfl
protected theorem subNatNat_eq_coe {m n : Nat} : subNatNat m n = m - n := by
apply subNatNat_elim m n fun m n i => i = m - n
· intros i n
rw [Int.ofNat_add, Int.sub_eq_add_neg, Int.add_assoc, Int.add_left_comm,
Int.add_right_neg, Int.add_zero]
· intros i n
simp only [negSucc_coe, ofNat_add, Int.sub_eq_add_neg, Int.neg_add, Int.add_assoc]
rw [ @Int.sub_eq_add_neg n, ofNat_sub, Nat.sub_self, ofNat_zero, Int.zero_add]
apply Nat.le_refl
theorem toNat_sub (m n : Nat) : toNat (m - n) = m - n := by
rw [ Int.subNatNat_eq_coe]
refine subNatNat_elim m n (fun m n i => toNat i = m - n) (fun i n => ?_) (fun i n => ?_)
· exact (Nat.add_sub_cancel_left ..).symm
· dsimp; rw [Nat.add_assoc, Nat.sub_eq_zero_of_le (Nat.le_add_right ..)]; rfl
/- ## Ring properties -/
@[simp] theorem ofNat_mul_negSucc (m n : Nat) : (m : Int) * -[n+1] = -(m * succ n) := rfl
@[simp] theorem negSucc_mul_ofNat (m n : Nat) : -[m+1] * n = -(succ m * n) := rfl
@[simp] theorem negSucc_mul_negSucc (m n : Nat) : -[m+1] * -[n+1] = succ m * succ n := rfl
protected theorem mul_comm (a b : Int) : a * b = b * a := by
cases a <;> cases b <;> simp [Nat.mul_comm]
theorem ofNat_mul_negOfNat (m n : Nat) : (m : Nat) * negOfNat n = negOfNat (m * n) := by
cases n <;> rfl
theorem negOfNat_mul_ofNat (m n : Nat) : negOfNat m * (n : Nat) = negOfNat (m * n) := by
rw [Int.mul_comm]; simp [ofNat_mul_negOfNat, Nat.mul_comm]
theorem negSucc_mul_negOfNat (m n : Nat) : -[m+1] * negOfNat n = ofNat (succ m * n) := by
cases n <;> rfl
theorem negOfNat_mul_negSucc (m n : Nat) : negOfNat n * -[m+1] = ofNat (n * succ m) := by
rw [Int.mul_comm, negSucc_mul_negOfNat, Nat.mul_comm]
attribute [local simp] ofNat_mul_negOfNat negOfNat_mul_ofNat
negSucc_mul_negOfNat negOfNat_mul_negSucc
protected theorem mul_assoc (a b c : Int) : a * b * c = a * (b * c) := by
cases a <;> cases b <;> cases c <;> simp [Nat.mul_assoc]
protected theorem mul_left_comm (a b c : Int) : a * (b * c) = b * (a * c) := by
rw [ Int.mul_assoc, Int.mul_assoc, Int.mul_comm a]
protected theorem mul_right_comm (a b c : Int) : a * b * c = a * c * b := by
rw [Int.mul_assoc, Int.mul_assoc, Int.mul_comm b]
@[simp] protected theorem mul_zero (a : Int) : a * 0 = 0 := by cases a <;> rfl
@[simp] protected theorem zero_mul (a : Int) : 0 * a = 0 := Int.mul_comm .. a.mul_zero
theorem negOfNat_eq_subNatNat_zero (n) : negOfNat n = subNatNat 0 n := by cases n <;> rfl
theorem ofNat_mul_subNatNat (m n k : Nat) :
m * subNatNat n k = subNatNat (m * n) (m * k) := by
cases m with
| zero => simp [ofNat_zero, Int.zero_mul, Nat.zero_mul]
| succ m => cases n.lt_or_ge k with
| inl h =>
have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
simp [subNatNat_of_lt h, subNatNat_of_lt h']
rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), neg_ofNat_succ, Nat.mul_sub_left_distrib,
succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]; rfl
| inr h =>
have h' : succ m * k succ m * n := Nat.mul_le_mul_left _ h
simp [subNatNat_of_le h, subNatNat_of_le h', Nat.mul_sub_left_distrib]
theorem negOfNat_add (m n : Nat) : negOfNat m + negOfNat n = negOfNat (m + n) := by
cases m <;> cases n <;> simp [Nat.succ_add] <;> rfl
theorem negSucc_mul_subNatNat (m n k : Nat) :
-[m+1] * subNatNat n k = subNatNat (succ m * k) (succ m * n) := by
cases n.lt_or_ge k with
| inl h =>
have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
rw [subNatNat_of_lt h, subNatNat_of_le (Nat.le_of_lt h')]
simp [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), Nat.mul_sub_left_distrib]
| inr h => cases Nat.lt_or_ge k n with
| inl h' =>
have h₁ : succ m * n > succ m * k := Nat.mul_lt_mul_of_pos_left h' (Nat.succ_pos m)
rw [subNatNat_of_le h, subNatNat_of_lt h₁, negSucc_mul_ofNat,
Nat.mul_sub_left_distrib, succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁)]; rfl
| inr h' => rw [Nat.le_antisymm h h', subNatNat_self, subNatNat_self, Int.mul_zero]
attribute [local simp] ofNat_mul_subNatNat negOfNat_add negSucc_mul_subNatNat
protected theorem mul_add : a b c : Int, a * (b + c) = a * b + a * c
| (m:Nat), (n:Nat), (k:Nat) => by simp [Nat.left_distrib]
| (m:Nat), (n:Nat), -[k+1] => by
simp [negOfNat_eq_subNatNat_zero]; rw [ subNatNat_add]; rfl
| (m:Nat), -[n+1], (k:Nat) => by
simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, subNatNat_add]; rfl
| (m:Nat), -[n+1], -[k+1] => by simp; rw [ Nat.left_distrib, succ_add]; rfl
| -[m+1], (n:Nat), (k:Nat) => by simp [Nat.mul_comm]; rw [ Nat.right_distrib, Nat.mul_comm]
| -[m+1], (n:Nat), -[k+1] => by
simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, subNatNat_add]; rfl
| -[m+1], -[n+1], (k:Nat) => by simp [negOfNat_eq_subNatNat_zero]; rw [ subNatNat_add]; rfl
| -[m+1], -[n+1], -[k+1] => by simp; rw [ Nat.left_distrib, succ_add]; rfl
protected theorem add_mul (a b c : Int) : (a + b) * c = a * c + b * c := by
simp [Int.mul_comm, Int.mul_add]
protected theorem neg_mul_eq_neg_mul (a b : Int) : -(a * b) = -a * b :=
Int.neg_eq_of_add_eq_zero <| by rw [ Int.add_mul, Int.add_right_neg, Int.zero_mul]
protected theorem neg_mul_eq_mul_neg (a b : Int) : -(a * b) = a * -b :=
Int.neg_eq_of_add_eq_zero <| by rw [ Int.mul_add, Int.add_right_neg, Int.mul_zero]
@[local simp] protected theorem neg_mul (a b : Int) : -a * b = -(a * b) :=
(Int.neg_mul_eq_neg_mul a b).symm
@[local simp] protected theorem mul_neg (a b : Int) : a * -b = -(a * b) :=
(Int.neg_mul_eq_mul_neg a b).symm
protected theorem neg_mul_neg (a b : Int) : -a * -b = a * b := by simp
protected theorem neg_mul_comm (a b : Int) : -a * b = a * -b := by simp
protected theorem mul_sub (a b c : Int) : a * (b - c) = a * b - a * c := by
simp [Int.sub_eq_add_neg, Int.mul_add]
protected theorem sub_mul (a b c : Int) : (a - b) * c = a * c - b * c := by
simp [Int.sub_eq_add_neg, Int.add_mul]
@[simp] protected theorem one_mul : a : Int, 1 * a = a
| ofNat n => show ofNat (1 * n) = ofNat n by rw [Nat.one_mul]
| -[n+1] => show -[1 * n +1] = -[n+1] by rw [Nat.one_mul]
@[simp] protected theorem mul_one (a : Int) : a * 1 = a := by rw [Int.mul_comm, Int.one_mul]
protected theorem mul_neg_one (a : Int) : a * -1 = -a := by rw [Int.mul_neg, Int.mul_one]
protected theorem neg_eq_neg_one_mul : a : Int, -a = -1 * a
| 0 => rfl
| succ n => show _ = -[1 * n +1] by rw [Nat.one_mul]; rfl
| -[n+1] => show _ = ofNat _ by rw [Nat.one_mul]; rfl
protected theorem mul_eq_zero {a b : Int} : a * b = 0 a = 0 b = 0 := by
refine fun h => ?_, fun h => h.elim (by simp [·, Int.zero_mul]) (by simp [·, Int.mul_zero])
exact match a, b, h with
| .ofNat 0, _, _ => by simp
| _, .ofNat 0, _ => by simp
| .ofNat (a+1), .negSucc b, h => by cases h
protected theorem mul_ne_zero {a b : Int} (a0 : a 0) (b0 : b 0) : a * b 0 :=
Or.rec a0 b0 Int.mul_eq_zero.mp
protected theorem eq_of_mul_eq_mul_right {a b c : Int} (ha : a 0) (h : b * a = c * a) : b = c :=
have : (b - c) * a = 0 := by rwa [Int.sub_mul, Int.sub_eq_zero]
Int.sub_eq_zero.1 <| (Int.mul_eq_zero.mp this).resolve_right ha
protected theorem eq_of_mul_eq_mul_left {a b c : Int} (ha : a 0) (h : a * b = a * c) : b = c :=
have : a * b - a * c = 0 := Int.sub_eq_zero_of_eq h
have : a * (b - c) = 0 := by rw [Int.mul_sub, this]
have : b - c = 0 := (Int.mul_eq_zero.1 this).resolve_left ha
Int.eq_of_sub_eq_zero this
theorem mul_eq_mul_left_iff {a b c : Int} (h : c 0) : c * a = c * b a = b :=
Int.eq_of_mul_eq_mul_left h, fun w => congrArg (fun x => c * x) w
theorem mul_eq_mul_right_iff {a b c : Int} (h : c 0) : a * c = b * c a = b :=
Int.eq_of_mul_eq_mul_right h, fun w => congrArg (fun x => x * c) w
theorem eq_one_of_mul_eq_self_left {a b : Int} (Hpos : a 0) (H : b * a = a) : b = 1 :=
Int.eq_of_mul_eq_mul_right Hpos <| by rw [Int.one_mul, H]
theorem eq_one_of_mul_eq_self_right {a b : Int} (Hpos : b 0) (H : b * a = b) : a = 1 :=
Int.eq_of_mul_eq_mul_left Hpos <| by rw [Int.mul_one, H]
/-! NatCast lemmas -/
/-!
The following lemmas are later subsumed by e.g. `Nat.cast_add` and `Nat.cast_mul` in Mathlib
but it is convenient to have these earlier, for users who only need `Nat` and `Int`.
-/
theorem natCast_zero : ((0 : Nat) : Int) = (0 : Int) := rfl
theorem natCast_one : ((1 : Nat) : Int) = (1 : Int) := rfl
@[simp] theorem natCast_add (a b : Nat) : ((a + b : Nat) : Int) = (a : Int) + (b : Int) := by
-- Note this only works because of local simp attributes in this file,
-- so it still makes sense to tag the lemmas with `@[simp]`.
simp
@[simp] theorem natCast_mul (a b : Nat) : ((a * b : Nat) : Int) = (a : Int) * (b : Int) := by
simp
end Int

View File

@@ -0,0 +1,438 @@
/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
-/
prelude
import Init.Data.Int.Lemmas
import Init.ByCases
/-!
# Results about the order properties of the integers, and the integers as an ordered ring.
-/
open Nat
namespace Int
/-! ## Order properties of the integers -/
theorem nonneg_def {a : Int} : NonNeg a n : Nat, a = n :=
fun n => n, rfl, fun h => match a, h with | _, n, rfl => n
theorem NonNeg.elim {a : Int} : NonNeg a n : Nat, a = n := nonneg_def.1
theorem nonneg_or_nonneg_neg : (a : Int), NonNeg a NonNeg (-a)
| (_:Nat) => .inl _
| -[_+1] => .inr _
theorem le_def (a b : Int) : a b NonNeg (b - a) := .rfl
theorem lt_iff_add_one_le (a b : Int) : a < b a + 1 b := .rfl
theorem le.intro_sub {a b : Int} (n : Nat) (h : b - a = n) : a b := by
simp [le_def, h]; constructor
attribute [local simp] Int.add_left_neg Int.add_right_neg Int.neg_add
theorem le.intro {a b : Int} (n : Nat) (h : a + n = b) : a b :=
le.intro_sub n <| by rw [ h, Int.add_comm]; simp [Int.sub_eq_add_neg, Int.add_assoc]
theorem le.dest_sub {a b : Int} (h : a b) : n : Nat, b - a = n := nonneg_def.1 h
theorem le.dest {a b : Int} (h : a b) : n : Nat, a + n = b :=
let n, h₁ := le.dest_sub h
n, by rw [ h₁, Int.add_comm]; simp [Int.sub_eq_add_neg, Int.add_assoc]
protected theorem le_total (a b : Int) : a b b a :=
(nonneg_or_nonneg_neg (b - a)).imp_right fun H => by
rwa [show -(b - a) = a - b by simp [Int.add_comm, Int.sub_eq_add_neg]] at H
@[simp] theorem ofNat_le {m n : Nat} : (m : Int) n m n :=
fun h =>
let k, hk := le.dest h
Nat.le.intro <| Int.ofNat.inj <| (Int.ofNat_add m k).trans hk,
fun h =>
let k, (hk : m + k = n) := Nat.le.dest h
le.intro k (by rw [ hk]; rfl)
theorem ofNat_zero_le (n : Nat) : 0 (n : Int) := ofNat_le.2 n.zero_le
theorem eq_ofNat_of_zero_le {a : Int} (h : 0 a) : n : Nat, a = n := by
have t := le.dest_sub h; rwa [Int.sub_zero] at t
theorem eq_succ_of_zero_lt {a : Int} (h : 0 < a) : n : Nat, a = n.succ :=
let n, (h : (1 + n) = a) := le.dest h
n, by rw [Nat.add_comm] at h; exact h.symm
theorem lt_add_succ (a : Int) (n : Nat) : a < a + Nat.succ n :=
le.intro n <| by rw [Int.add_comm, Int.add_left_comm]; rfl
theorem lt.intro {a b : Int} {n : Nat} (h : a + Nat.succ n = b) : a < b :=
h lt_add_succ a n
theorem lt.dest {a b : Int} (h : a < b) : n : Nat, a + Nat.succ n = b :=
let n, h := le.dest h; n, by rwa [Int.add_comm, Int.add_left_comm] at h
@[simp] theorem ofNat_lt {n m : Nat} : (n : Int) < m n < m := by
rw [lt_iff_add_one_le, ofNat_succ, ofNat_le]; rfl
@[simp] theorem ofNat_pos {n : Nat} : 0 < (n : Int) 0 < n := ofNat_lt
theorem ofNat_nonneg (n : Nat) : 0 (n : Int) := _
theorem ofNat_succ_pos (n : Nat) : 0 < (succ n : Int) := ofNat_lt.2 <| Nat.succ_pos _
@[simp] protected theorem le_refl (a : Int) : a a :=
le.intro _ (Int.add_zero a)
protected theorem le_trans {a b c : Int} (h₁ : a b) (h₂ : b c) : a c :=
let n, hn := le.dest h₁; let m, hm := le.dest h₂
le.intro (n + m) <| by rw [ hm, hn, Int.add_assoc, ofNat_add]
protected theorem le_antisymm {a b : Int} (h₁ : a b) (h₂ : b a) : a = b := by
let n, hn := le.dest h₁; let m, hm := le.dest h₂
have := hn; rw [ hm, Int.add_assoc, ofNat_add] at this
have := Int.ofNat.inj <| Int.add_left_cancel <| this.trans (Int.add_zero _).symm
rw [ hn, Nat.eq_zero_of_add_eq_zero_left this, ofNat_zero, Int.add_zero a]
protected theorem lt_irrefl (a : Int) : ¬a < a := fun H =>
let n, hn := lt.dest H
have : (a+Nat.succ n) = a+0 := by
rw [hn, Int.add_zero]
have : Nat.succ n = 0 := Int.ofNat.inj (Int.add_left_cancel this)
show False from Nat.succ_ne_zero _ this
protected theorem ne_of_lt {a b : Int} (h : a < b) : a b := fun e => by
cases e; exact Int.lt_irrefl _ h
protected theorem ne_of_gt {a b : Int} (h : b < a) : a b := (Int.ne_of_lt h).symm
protected theorem le_of_lt {a b : Int} (h : a < b) : a b :=
let _, hn := lt.dest h; le.intro _ hn
protected theorem lt_iff_le_and_ne {a b : Int} : a < b a b a b := by
refine fun h => Int.le_of_lt h, Int.ne_of_lt h, fun aleb, aneb => ?_
let n, hn := le.dest aleb
have : n 0 := aneb.imp fun eq => by rw [ hn, eq, ofNat_zero, Int.add_zero]
apply lt.intro; rwa [ Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero this)] at hn
theorem lt_succ (a : Int) : a < a + 1 := Int.le_refl _
protected theorem zero_lt_one : (0 : Int) < 1 := _
protected theorem lt_iff_le_not_le {a b : Int} : a < b a b ¬b a := by
rw [Int.lt_iff_le_and_ne]
constructor <;> refine fun h, h' => h, h'.imp fun h' => ?_
· exact Int.le_antisymm h h'
· subst h'; apply Int.le_refl
protected theorem not_le {a b : Int} : ¬a b b < a :=
fun h => Int.lt_iff_le_not_le.2 (Int.le_total ..).resolve_right h, h,
fun h => (Int.lt_iff_le_not_le.1 h).2
protected theorem not_lt {a b : Int} : ¬a < b b a :=
by rw [ Int.not_le, Decidable.not_not]
protected theorem lt_trichotomy (a b : Int) : a < b a = b b < a :=
if eq : a = b then .inr <| .inl eq else
if le : a b then .inl <| Int.lt_iff_le_and_ne.2 le, eq else
.inr <| .inr <| Int.not_le.1 le
protected theorem ne_iff_lt_or_gt {a b : Int} : a b a < b b < a := by
constructor
· intro h
cases Int.lt_trichotomy a b
case inl lt => exact Or.inl lt
case inr h =>
cases h
case inl =>simp_all
case inr gt => exact Or.inr gt
· intro h
cases h
case inl lt => exact Int.ne_of_lt lt
case inr gt => exact Int.ne_of_gt gt
protected theorem lt_or_gt_of_ne {a b : Int} : a b a < b b < a:= Int.ne_iff_lt_or_gt.mp
protected theorem eq_iff_le_and_ge {x y : Int} : x = y x y y x := by
constructor
· simp_all
· intro h₁, h₂
exact Int.le_antisymm h₁ h₂
protected theorem lt_of_le_of_lt {a b c : Int} (h₁ : a b) (h₂ : b < c) : a < c :=
Int.not_le.1 fun h => Int.not_le.2 h₂ (Int.le_trans h h₁)
protected theorem lt_of_lt_of_le {a b c : Int} (h₁ : a < b) (h₂ : b c) : a < c :=
Int.not_le.1 fun h => Int.not_le.2 h₁ (Int.le_trans h₂ h)
protected theorem lt_trans {a b c : Int} (h₁ : a < b) (h₂ : b < c) : a < c :=
Int.lt_of_le_of_lt (Int.le_of_lt h₁) h₂
instance : Trans (α := Int) (· ·) (· ·) (· ·) := Int.le_trans
instance : Trans (α := Int) (· < ·) (· ·) (· < ·) := Int.lt_of_lt_of_le
instance : Trans (α := Int) (· ·) (· < ·) (· < ·) := Int.lt_of_le_of_lt
instance : Trans (α := Int) (· < ·) (· < ·) (· < ·) := Int.lt_trans
protected theorem min_def (n m : Int) : min n m = if n m then n else m := rfl
protected theorem max_def (n m : Int) : max n m = if n m then m else n := rfl
protected theorem min_comm (a b : Int) : min a b = min b a := by
simp [Int.min_def]
by_cases h₁ : a b <;> by_cases h₂ : b a <;> simp [h₁, h₂]
· exact Int.le_antisymm h₁ h₂
· cases not_or_intro h₁ h₂ <| Int.le_total ..
protected theorem min_le_right (a b : Int) : min a b b := by rw [Int.min_def]; split <;> simp [*]
protected theorem min_le_left (a b : Int) : min a b a := Int.min_comm .. Int.min_le_right ..
protected theorem le_min {a b c : Int} : a min b c a b a c :=
fun h => Int.le_trans h (Int.min_le_left ..), Int.le_trans h (Int.min_le_right ..),
fun h₁, h₂ => by rw [Int.min_def]; split <;> assumption
protected theorem max_comm (a b : Int) : max a b = max b a := by
simp only [Int.max_def]
by_cases h₁ : a b <;> by_cases h₂ : b a <;> simp [h₁, h₂]
· exact Int.le_antisymm h₂ h₁
· cases not_or_intro h₁ h₂ <| Int.le_total ..
protected theorem le_max_left (a b : Int) : a max a b := by rw [Int.max_def]; split <;> simp [*]
protected theorem le_max_right (a b : Int) : b max a b := Int.max_comm .. Int.le_max_left ..
protected theorem max_le {a b c : Int} : max a b c a c b c :=
fun h => Int.le_trans (Int.le_max_left ..) h, Int.le_trans (Int.le_max_right ..) h,
fun h₁, h₂ => by rw [Int.max_def]; split <;> assumption
theorem eq_natAbs_of_zero_le {a : Int} (h : 0 a) : a = natAbs a := by
let n, e := eq_ofNat_of_zero_le h
rw [e]; rfl
theorem le_natAbs {a : Int} : a natAbs a :=
match Int.le_total 0 a with
| .inl h => by rw [eq_natAbs_of_zero_le h]; apply Int.le_refl
| .inr h => Int.le_trans h (ofNat_zero_le _)
theorem negSucc_lt_zero (n : Nat) : -[n+1] < 0 :=
Int.not_le.1 fun h => let _, h := eq_ofNat_of_zero_le h; nomatch h
@[simp] theorem negSucc_not_nonneg (n : Nat) : 0 -[n+1] False := by
simp only [Int.not_le, iff_false]; exact Int.negSucc_lt_zero n
protected theorem add_le_add_left {a b : Int} (h : a b) (c : Int) : c + a c + b :=
let n, hn := le.dest h; le.intro n <| by rw [Int.add_assoc, hn]
protected theorem add_lt_add_left {a b : Int} (h : a < b) (c : Int) : c + a < c + b :=
Int.lt_iff_le_and_ne.2 Int.add_le_add_left (Int.le_of_lt h) _, fun heq =>
b.lt_irrefl <| by rwa [Int.add_left_cancel heq] at h
protected theorem add_le_add_right {a b : Int} (h : a b) (c : Int) : a + c b + c :=
Int.add_comm c a Int.add_comm c b Int.add_le_add_left h c
protected theorem add_lt_add_right {a b : Int} (h : a < b) (c : Int) : a + c < b + c :=
Int.add_comm c a Int.add_comm c b Int.add_lt_add_left h c
protected theorem le_of_add_le_add_left {a b c : Int} (h : a + b a + c) : b c := by
have : -a + (a + b) -a + (a + c) := Int.add_le_add_left h _
simp [Int.neg_add_cancel_left] at this
assumption
protected theorem le_of_add_le_add_right {a b c : Int} (h : a + b c + b) : a c :=
Int.le_of_add_le_add_left (a := b) <| by rwa [Int.add_comm b a, Int.add_comm b c]
protected theorem add_le_add_iff_left (a : Int) : a + b a + c b c :=
Int.le_of_add_le_add_left, (Int.add_le_add_left · _)
protected theorem add_le_add_iff_right (c : Int) : a + c b + c a b :=
Int.le_of_add_le_add_right, (Int.add_le_add_right · _)
protected theorem add_le_add {a b c d : Int} (h₁ : a b) (h₂ : c d) : a + c b + d :=
Int.le_trans (Int.add_le_add_right h₁ c) (Int.add_le_add_left h₂ b)
protected theorem le_add_of_nonneg_right {a b : Int} (h : 0 b) : a a + b := by
have : a + b a + 0 := Int.add_le_add_left h a
rwa [Int.add_zero] at this
protected theorem le_add_of_nonneg_left {a b : Int} (h : 0 b) : a b + a := by
have : 0 + a b + a := Int.add_le_add_right h a
rwa [Int.zero_add] at this
protected theorem neg_le_neg {a b : Int} (h : a b) : -b -a := by
have : 0 -a + b := Int.add_left_neg a Int.add_le_add_left h (-a)
have : 0 + -b -a + b + -b := Int.add_le_add_right this (-b)
rwa [Int.add_neg_cancel_right, Int.zero_add] at this
protected theorem le_of_neg_le_neg {a b : Int} (h : -b -a) : a b :=
suffices - -a - -b by simp [Int.neg_neg] at this; assumption
Int.neg_le_neg h
protected theorem neg_nonpos_of_nonneg {a : Int} (h : 0 a) : -a 0 := by
have : -a -0 := Int.neg_le_neg h
rwa [Int.neg_zero] at this
protected theorem neg_nonneg_of_nonpos {a : Int} (h : a 0) : 0 -a := by
have : -0 -a := Int.neg_le_neg h
rwa [Int.neg_zero] at this
protected theorem neg_lt_neg {a b : Int} (h : a < b) : -b < -a := by
have : 0 < -a + b := Int.add_left_neg a Int.add_lt_add_left h (-a)
have : 0 + -b < -a + b + -b := Int.add_lt_add_right this (-b)
rwa [Int.add_neg_cancel_right, Int.zero_add] at this
protected theorem neg_neg_of_pos {a : Int} (h : 0 < a) : -a < 0 := by
have : -a < -0 := Int.neg_lt_neg h
rwa [Int.neg_zero] at this
protected theorem neg_pos_of_neg {a : Int} (h : a < 0) : 0 < -a := by
have : -0 < -a := Int.neg_lt_neg h
rwa [Int.neg_zero] at this
protected theorem sub_nonneg_of_le {a b : Int} (h : b a) : 0 a - b := by
have h := Int.add_le_add_right h (-b)
rwa [Int.add_right_neg] at h
protected theorem le_of_sub_nonneg {a b : Int} (h : 0 a - b) : b a := by
have h := Int.add_le_add_right h b
rwa [Int.sub_add_cancel, Int.zero_add] at h
protected theorem sub_pos_of_lt {a b : Int} (h : b < a) : 0 < a - b := by
have h := Int.add_lt_add_right h (-b)
rwa [Int.add_right_neg] at h
protected theorem lt_of_sub_pos {a b : Int} (h : 0 < a - b) : b < a := by
have h := Int.add_lt_add_right h b
rwa [Int.sub_add_cancel, Int.zero_add] at h
protected theorem sub_left_le_of_le_add {a b c : Int} (h : a b + c) : a - b c := by
have h := Int.add_le_add_right h (-b)
rwa [Int.add_comm b c, Int.add_neg_cancel_right] at h
protected theorem sub_le_self (a : Int) {b : Int} (h : 0 b) : a - b a :=
calc a + -b
_ a + 0 := Int.add_le_add_left (Int.neg_nonpos_of_nonneg h) _
_ = a := by rw [Int.add_zero]
protected theorem sub_lt_self (a : Int) {b : Int} (h : 0 < b) : a - b < a :=
calc a + -b
_ < a + 0 := Int.add_lt_add_left (Int.neg_neg_of_pos h) _
_ = a := by rw [Int.add_zero]
theorem add_one_le_of_lt {a b : Int} (H : a < b) : a + 1 b := H
/- ### Order properties and multiplication -/
protected theorem mul_nonneg {a b : Int} (ha : 0 a) (hb : 0 b) : 0 a * b := by
let n, hn := eq_ofNat_of_zero_le ha
let m, hm := eq_ofNat_of_zero_le hb
rw [hn, hm, ofNat_mul]; apply ofNat_nonneg
protected theorem mul_pos {a b : Int} (ha : 0 < a) (hb : 0 < b) : 0 < a * b := by
let n, hn := eq_succ_of_zero_lt ha
let m, hm := eq_succ_of_zero_lt hb
rw [hn, hm, ofNat_mul]; apply ofNat_succ_pos
protected theorem mul_lt_mul_of_pos_left {a b c : Int}
(h₁ : a < b) (h₂ : 0 < c) : c * a < c * b := by
have : 0 < c * (b - a) := Int.mul_pos h₂ (Int.sub_pos_of_lt h₁)
rw [Int.mul_sub] at this
exact Int.lt_of_sub_pos this
protected theorem mul_lt_mul_of_pos_right {a b c : Int}
(h₁ : a < b) (h₂ : 0 < c) : a * c < b * c := by
have : 0 < b - a := Int.sub_pos_of_lt h₁
have : 0 < (b - a) * c := Int.mul_pos this h₂
rw [Int.sub_mul] at this
exact Int.lt_of_sub_pos this
protected theorem mul_le_mul_of_nonneg_left {a b c : Int}
(h₁ : a b) (h₂ : 0 c) : c * a c * b :=
if hba : b a then by
rw [Int.le_antisymm hba h₁]; apply Int.le_refl
else if hc0 : c 0 then by
simp [Int.le_antisymm hc0 h₂, Int.zero_mul]
else by
exact Int.le_of_lt <| Int.mul_lt_mul_of_pos_left
(Int.lt_iff_le_not_le.2 h₁, hba) (Int.lt_iff_le_not_le.2 h₂, hc0)
protected theorem mul_le_mul_of_nonneg_right {a b c : Int}
(h₁ : a b) (h₂ : 0 c) : a * c b * c := by
rw [Int.mul_comm, Int.mul_comm b]; exact Int.mul_le_mul_of_nonneg_left h₁ h₂
protected theorem mul_le_mul {a b c d : Int}
(hac : a c) (hbd : b d) (nn_b : 0 b) (nn_c : 0 c) : a * b c * d :=
Int.le_trans (Int.mul_le_mul_of_nonneg_right hac nn_b) (Int.mul_le_mul_of_nonneg_left hbd nn_c)
protected theorem mul_nonpos_of_nonneg_of_nonpos {a b : Int}
(ha : 0 a) (hb : b 0) : a * b 0 := by
have h : a * b a * 0 := Int.mul_le_mul_of_nonneg_left hb ha
rwa [Int.mul_zero] at h
protected theorem mul_nonpos_of_nonpos_of_nonneg {a b : Int}
(ha : a 0) (hb : 0 b) : a * b 0 := by
have h : a * b 0 * b := Int.mul_le_mul_of_nonneg_right ha hb
rwa [Int.zero_mul] at h
protected theorem mul_le_mul_of_nonpos_right {a b c : Int}
(h : b a) (hc : c 0) : a * c b * c :=
have : -c 0 := Int.neg_nonneg_of_nonpos hc
have : b * -c a * -c := Int.mul_le_mul_of_nonneg_right h this
Int.le_of_neg_le_neg <| by rwa [ Int.neg_mul_eq_mul_neg, Int.neg_mul_eq_mul_neg] at this
protected theorem mul_le_mul_of_nonpos_left {a b c : Int}
(ha : a 0) (h : c b) : a * b a * c := by
rw [Int.mul_comm a b, Int.mul_comm a c]
apply Int.mul_le_mul_of_nonpos_right h ha
/- ## natAbs -/
@[simp] theorem natAbs_ofNat (n : Nat) : natAbs n = n := rfl
@[simp] theorem natAbs_negSucc (n : Nat) : natAbs -[n+1] = n.succ := rfl
@[simp] theorem natAbs_zero : natAbs (0 : Int) = (0 : Nat) := rfl
@[simp] theorem natAbs_one : natAbs (1 : Int) = (1 : Nat) := rfl
@[simp] theorem natAbs_eq_zero : natAbs a = 0 a = 0 :=
fun H => match a with
| ofNat _ => congrArg ofNat H
| -[_+1] => absurd H (succ_ne_zero _),
fun e => e rfl
theorem natAbs_pos : 0 < natAbs a a 0 := by rw [Nat.pos_iff_ne_zero, Ne, natAbs_eq_zero]
@[simp] theorem natAbs_neg : (a : Int), natAbs (-a) = natAbs a
| 0 => rfl
| succ _ => rfl
| -[_+1] => rfl
theorem natAbs_eq : (a : Int), a = natAbs a a = -(natAbs a)
| ofNat _ => Or.inl rfl
| -[_+1] => Or.inr rfl
theorem natAbs_negOfNat (n : Nat) : natAbs (negOfNat n) = n := by
cases n <;> rfl
theorem natAbs_mul (a b : Int) : natAbs (a * b) = natAbs a * natAbs b := by
cases a <;> cases b <;>
simp only [ Int.mul_def, Int.mul, natAbs_negOfNat] <;> simp only [natAbs]
theorem natAbs_eq_natAbs_iff {a b : Int} : a.natAbs = b.natAbs a = b a = -b := by
constructor <;> intro h
· cases Int.natAbs_eq a with
| inl h₁ | inr h₁ =>
cases Int.natAbs_eq b with
| inl h₂ | inr h₂ => rw [h₁, h₂]; simp [h]
· cases h with (subst a; try rfl)
| inr h => rw [Int.natAbs_neg]
theorem natAbs_of_nonneg {a : Int} (H : 0 a) : (natAbs a : Int) = a :=
match a, eq_ofNat_of_zero_le H with
| _, _, rfl => rfl
theorem ofNat_natAbs_of_nonpos {a : Int} (H : a 0) : (natAbs a : Int) = -a := by
rw [ natAbs_neg, natAbs_of_nonneg (Int.neg_nonneg_of_nonpos H)]

View File

@@ -7,3 +7,4 @@ prelude
import Init.Data.List.Basic
import Init.Data.List.BasicAux
import Init.Data.List.Control
import Init.Data.List.Lemmas

View File

@@ -0,0 +1,630 @@
/-
Copyright (c) 2014 Parikshit Khanna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
-/
prelude
import Init.Data.List.BasicAux
import Init.Data.List.Control
import Init.PropLemmas
import Init.Control.Lawful
import Init.Hints
namespace List
open Nat
/-!
# Bootstrapping theorems for lists
These are theorems used in the definitions of `Std.Data.List.Basic` and tactics.
New theorems should be added to `Std.Data.List.Lemmas` if they are not needed by the bootstrap.
-/
attribute [simp] concat_eq_append append_assoc
@[simp] theorem get?_nil : @get? α [] n = none := rfl
@[simp] theorem get?_cons_zero : @get? α (a::l) 0 = some a := rfl
@[simp] theorem get?_cons_succ : @get? α (a::l) (n+1) = get? l n := rfl
@[simp] theorem get_cons_zero : get (a::l) (0 : Fin (l.length + 1)) = a := rfl
@[simp] theorem head?_nil : @head? α [] = none := rfl
@[simp] theorem head?_cons : @head? α (a::l) = some a := rfl
@[simp 1100] theorem headD_nil : @headD α [] d = d := rfl
@[simp 1100] theorem headD_cons : @headD α (a::l) d = a := rfl
@[simp] theorem head_cons : @head α (a::l) h = a := rfl
@[simp] theorem tail?_nil : @tail? α [] = none := rfl
@[simp] theorem tail?_cons : @tail? α (a::l) = some l := rfl
@[simp] theorem tail!_cons : @tail! α (a::l) = l := rfl
@[simp 1100] theorem tailD_nil : @tailD α [] l' = l' := rfl
@[simp 1100] theorem tailD_cons : @tailD α (a::l) l' = l := rfl
@[simp] theorem any_nil : [].any f = false := rfl
@[simp] theorem any_cons : (a::l).any f = (f a || l.any f) := rfl
@[simp] theorem all_nil : [].all f = true := rfl
@[simp] theorem all_cons : (a::l).all f = (f a && l.all f) := rfl
@[simp] theorem or_nil : [].or = false := rfl
@[simp] theorem or_cons : (a::l).or = (a || l.or) := rfl
@[simp] theorem and_nil : [].and = true := rfl
@[simp] theorem and_cons : (a::l).and = (a && l.and) := rfl
/-! ### length -/
theorem eq_nil_of_length_eq_zero (_ : length l = 0) : l = [] := match l with | [] => rfl
theorem ne_nil_of_length_eq_succ (_ : length l = succ n) : l [] := fun _ => nomatch l
theorem length_eq_zero : length l = 0 l = [] :=
eq_nil_of_length_eq_zero, fun h => h rfl
/-! ### mem -/
@[simp] theorem not_mem_nil (a : α) : ¬ a [] := nofun
@[simp] theorem mem_cons : a (b :: l) a = b a l :=
fun h => by cases h <;> simp [Membership.mem, *],
fun | Or.inl rfl => by constructor | Or.inr h => by constructor; assumption
theorem mem_cons_self (a : α) (l : List α) : a a :: l := .head ..
theorem mem_cons_of_mem (y : α) {a : α} {l : List α} : a l a y :: l := .tail _
theorem eq_nil_iff_forall_not_mem {l : List α} : l = [] a, a l := by
cases l <;> simp
/-! ### append -/
@[simp 1100] theorem singleton_append : [x] ++ l = x :: l := rfl
theorem append_inj :
{s₁ s₂ t₁ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ length s₁ = length s₂ s₁ = s₂ t₁ = t₂
| [], [], t₁, t₂, h, _ => rfl, h
| a :: s₁, b :: s₂, t₁, t₂, h, hl => by
simp [append_inj (cons.inj h).2 (Nat.succ.inj hl)] at h ; exact h
theorem append_inj_right (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length s₁ = length s₂) : t₁ = t₂ :=
(append_inj h hl).right
theorem append_inj_left (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length s₁ = length s₂) : s₁ = s₂ :=
(append_inj h hl).left
theorem append_inj' (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length t₁ = length t₂) : s₁ = s₂ t₁ = t₂ :=
append_inj h <| @Nat.add_right_cancel _ (length t₁) _ <| by
let hap := congrArg length h; simp only [length_append, hl] at hap; exact hap
theorem append_inj_right' (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length t₁ = length t₂) : t₁ = t₂ :=
(append_inj' h hl).right
theorem append_inj_left' (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length t₁ = length t₂) : s₁ = s₂ :=
(append_inj' h hl).left
theorem append_right_inj {t₁ t₂ : List α} (s) : s ++ t₁ = s ++ t₂ t₁ = t₂ :=
fun h => append_inj_right h rfl, congrArg _
theorem append_left_inj {s₁ s₂ : List α} (t) : s₁ ++ t = s₂ ++ t s₁ = s₂ :=
fun h => append_inj_left' h rfl, congrArg (· ++ _)
@[simp] theorem append_eq_nil : p ++ q = [] p = [] q = [] := by
cases p <;> simp
/-! ### map -/
@[simp] theorem map_nil {f : α β} : map f [] = [] := rfl
@[simp] theorem map_cons (f : α β) a l : map f (a :: l) = f a :: map f l := rfl
@[simp] theorem map_append (f : α β) : l₁ l₂, map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by
intro l₁; induction l₁ <;> intros <;> simp_all
@[simp] theorem map_id (l : List α) : map id l = l := by induction l <;> simp_all
@[simp] theorem map_id' (l : List α) : map (fun a => a) l = l := by induction l <;> simp_all
@[simp] theorem mem_map {f : α β} : {l : List α}, b l.map f a, a l f a = b
| [] => by simp
| _ :: l => by simp [mem_map (l := l), eq_comm (a := b)]
theorem mem_map_of_mem (f : α β) (h : a l) : f a map f l := mem_map.2 _, h, rfl
@[simp] theorem map_map (g : β γ) (f : α β) (l : List α) :
map g (map f l) = map (g f) l := by induction l <;> simp_all
/-! ### bind -/
@[simp] theorem nil_bind (f : α List β) : List.bind [] f = [] := by simp [join, List.bind]
@[simp] theorem cons_bind x xs (f : α List β) :
List.bind (x :: xs) f = f x ++ List.bind xs f := by simp [join, List.bind]
@[simp] theorem append_bind xs ys (f : α List β) :
List.bind (xs ++ ys) f = List.bind xs f ++ List.bind ys f := by
induction xs; {rfl}; simp_all [cons_bind, append_assoc]
@[simp] theorem bind_id (l : List (List α)) : List.bind l id = l.join := by simp [List.bind]
/-! ### join -/
@[simp] theorem join_nil : List.join ([] : List (List α)) = [] := rfl
@[simp] theorem join_cons : (l :: ls).join = l ++ ls.join := rfl
/-! ### bounded quantifiers over Lists -/
theorem forall_mem_cons {p : α Prop} {a : α} {l : List α} :
( x, x a :: l p x) p a x, x l p x :=
fun H => H _ (.head ..), fun _ h => H _ (.tail _ h),
fun H₁, H₂ _ => fun | .head .. => H₁ | .tail _ h => H₂ _ h
/-! ### reverse -/
@[simp] theorem reverseAux_nil : reverseAux [] r = r := rfl
@[simp] theorem reverseAux_cons : reverseAux (a::l) r = reverseAux l (a::r) := rfl
theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs :=
reverseAux_eq_append ..
theorem reverse_map (f : α β) (l : List α) : (l.map f).reverse = l.reverse.map f := by
induction l <;> simp [*]
@[simp] theorem reverse_eq_nil_iff {xs : List α} : xs.reverse = [] xs = [] := by
match xs with
| [] => simp
| x :: xs => simp
/-! ### nth element -/
theorem get_of_mem : {a} {l : List α}, a l n, get l n = a
| _, _ :: _, .head .. => 0, Nat.succ_pos _, rfl
| _, _ :: _, .tail _ m => let n, h, e := get_of_mem m; n+1, Nat.succ_lt_succ h, e
theorem get_mem : (l : List α) n h, get l n, h l
| _ :: _, 0, _ => .head ..
| _ :: l, _+1, _ => .tail _ (get_mem l ..)
theorem mem_iff_get {a} {l : List α} : a l n, get l n = a :=
get_of_mem, fun _, e => e get_mem ..
theorem get?_len_le : {l : List α} {n}, length l n l.get? n = none
| [], _, _ => rfl
| _ :: l, _+1, h => get?_len_le (l := l) <| Nat.le_of_succ_le_succ h
theorem get?_eq_get : {l : List α} {n} (h : n < l.length), l.get? n = some (get l n, h)
| _ :: _, 0, _ => rfl
| _ :: l, _+1, _ => get?_eq_get (l := l) _
theorem get?_eq_some : l.get? n = some a h, get l n, h = a :=
fun e =>
have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_len_le hn e
this, by rwa [get?_eq_get this, Option.some.injEq] at e,
fun h, e => e get?_eq_get _
@[simp] theorem get?_eq_none : l.get? n = none length l n :=
fun e => Nat.ge_of_not_lt (fun h' => by cases e get?_eq_some.2 h', rfl), get?_len_le
@[simp] theorem get?_map (f : α β) : l n, (map f l).get? n = (l.get? n).map f
| [], _ => rfl
| _ :: _, 0 => rfl
| _ :: l, n+1 => get?_map f l n
@[simp] theorem get?_concat_length : (l : List α) (a : α), (l ++ [a]).get? l.length = some a
| [], a => rfl
| b :: l, a => by rw [cons_append, length_cons]; simp only [get?, get?_concat_length]
theorem getLast_eq_get : (l : List α) (h : l []),
getLast l h = l.get l.length - 1, by
match l with
| [] => contradiction
| a :: l => exact Nat.le_refl _
| [a], h => rfl
| a :: b :: l, h => by
simp [getLast, get, Nat.succ_sub_succ, getLast_eq_get]
@[simp] theorem getLast?_nil : @getLast? α [] = none := rfl
theorem getLast?_eq_getLast : l h, @getLast? α l = some (getLast l h)
| [], h => nomatch h rfl
| _::_, _ => rfl
theorem getLast?_eq_get? : (l : List α), getLast? l = l.get? (l.length - 1)
| [] => rfl
| a::l => by rw [getLast?_eq_getLast (a::l) nofun, getLast_eq_get, get?_eq_get]
@[simp] theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by
simp [getLast?_eq_get?, Nat.succ_sub_succ]
/-! ### take and drop -/
@[simp] theorem take_append_drop : (n : Nat) (l : List α), take n l ++ drop n l = l
| 0, _ => rfl
| _+1, [] => rfl
| n+1, x :: xs => congrArg (cons x) <| take_append_drop n xs
@[simp] theorem length_drop : (i : Nat) (l : List α), length (drop i l) = length l - i
| 0, _ => rfl
| succ i, [] => Eq.symm (Nat.zero_sub (succ i))
| succ i, x :: l => calc
length (drop (succ i) (x :: l)) = length l - i := length_drop i l
_ = succ (length l) - succ i := (Nat.succ_sub_succ_eq_sub (length l) i).symm
theorem drop_length_le {l : List α} (h : l.length i) : drop i l = [] :=
length_eq_zero.1 (length_drop .. Nat.sub_eq_zero_of_le h)
theorem take_length_le {l : List α} (h : l.length i) : take i l = l := by
have := take_append_drop i l
rw [drop_length_le h, append_nil] at this; exact this
@[simp] theorem take_zero (l : List α) : l.take 0 = [] := rfl
@[simp] theorem take_nil : ([] : List α).take i = [] := by cases i <;> rfl
@[simp] theorem take_cons_succ : (a::as).take (i+1) = a :: as.take i := rfl
@[simp] theorem drop_zero (l : List α) : l.drop 0 = l := rfl
@[simp] theorem drop_succ_cons : (a :: l).drop (n + 1) = l.drop n := rfl
@[simp] theorem drop_length (l : List α) : drop l.length l = [] := drop_length_le (Nat.le_refl _)
@[simp] theorem take_length (l : List α) : take l.length l = l := take_length_le (Nat.le_refl _)
theorem take_concat_get (l : List α) (i : Nat) (h : i < l.length) :
(l.take i).concat l[i] = l.take (i+1) :=
Eq.symm <| (append_left_inj _).1 <| (take_append_drop (i+1) l).trans <| by
rw [concat_eq_append, append_assoc, singleton_append, get_drop_eq_drop, take_append_drop]
theorem reverse_concat (l : List α) (a : α) : (l.concat a).reverse = a :: l.reverse := by
rw [concat_eq_append, reverse_append]; rfl
/-! ### takeWhile and dropWhile -/
@[simp] theorem dropWhile_nil : ([] : List α).dropWhile p = [] := rfl
theorem dropWhile_cons :
(x :: xs : List α).dropWhile p = if p x then xs.dropWhile p else x :: xs := by
split <;> simp_all [dropWhile]
/-! ### foldlM and foldrM -/
@[simp] theorem foldlM_reverse [Monad m] (l : List α) (f : β α m β) (b) :
l.reverse.foldlM f b = l.foldrM (fun x y => f y x) b := rfl
@[simp] theorem foldlM_nil [Monad m] (f : β α m β) (b) : [].foldlM f b = pure b := rfl
@[simp] theorem foldlM_cons [Monad m] (f : β α m β) (b) (a) (l : List α) :
(a :: l).foldlM f b = f b a >>= l.foldlM f := by
simp [List.foldlM]
@[simp] theorem foldlM_append [Monad m] [LawfulMonad m] (f : β α m β) (b) (l l' : List α) :
(l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by
induction l generalizing b <;> simp [*]
@[simp] theorem foldrM_nil [Monad m] (f : α β m β) (b) : [].foldrM f b = pure b := rfl
@[simp] theorem foldrM_cons [Monad m] [LawfulMonad m] (a : α) (l) (f : α β m β) (b) :
(a :: l).foldrM f b = l.foldrM f b >>= f a := by
simp only [foldrM]
induction l <;> simp_all
@[simp] theorem foldrM_reverse [Monad m] (l : List α) (f : α β m β) (b) :
l.reverse.foldrM f b = l.foldlM (fun x y => f y x) b :=
(foldlM_reverse ..).symm.trans <| by simp
theorem foldl_eq_foldlM (f : β α β) (b) (l : List α) :
l.foldl f b = l.foldlM (m := Id) f b := by
induction l generalizing b <;> simp [*, foldl]
theorem foldr_eq_foldrM (f : α β β) (b) (l : List α) :
l.foldr f b = l.foldrM (m := Id) f b := by
induction l <;> simp [*, foldr]
/-! ### foldl and foldr -/
@[simp] theorem foldl_reverse (l : List α) (f : β α β) (b) :
l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
@[simp] theorem foldr_reverse (l : List α) (f : α β β) (b) :
l.reverse.foldr f b = l.foldl (fun x y => f y x) b :=
(foldl_reverse ..).symm.trans <| by simp
@[simp] theorem foldrM_append [Monad m] [LawfulMonad m] (f : α β m β) (b) (l l' : List α) :
(l ++ l').foldrM f b = l'.foldrM f b >>= l.foldrM f := by
induction l <;> simp [*]
@[simp] theorem foldl_append {β : Type _} (f : β α β) (b) (l l' : List α) :
(l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM]
@[simp] theorem foldr_append (f : α β β) (b) (l l' : List α) :
(l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM]
@[simp] theorem foldl_nil : [].foldl f b = b := rfl
@[simp] theorem foldl_cons (l : List α) (b : β) : (a :: l).foldl f b = l.foldl f (f b a) := rfl
@[simp] theorem foldr_nil : [].foldr f b = b := rfl
@[simp] theorem foldr_cons (l : List α) : (a :: l).foldr f b = f a (l.foldr f b) := rfl
@[simp] theorem foldr_self_append (l : List α) : l.foldr cons l' = l ++ l' := by
induction l <;> simp [*]
theorem foldr_self (l : List α) : l.foldr cons [] = l := by simp
/-! ### mapM -/
/-- Alternate (non-tail-recursive) form of mapM for proofs. -/
def mapM' [Monad m] (f : α m β) : List α m (List β)
| [] => pure []
| a :: l => return ( f a) :: ( l.mapM' f)
@[simp] theorem mapM'_nil [Monad m] {f : α m β} : mapM' f [] = pure [] := rfl
@[simp] theorem mapM'_cons [Monad m] {f : α m β} :
mapM' f (a :: l) = return (( f a) :: ( l.mapM' f)) :=
rfl
theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α m β) (l : List α) :
mapM' f l = mapM f l := by simp [go, mapM] where
go : l acc, mapM.loop f l acc = return acc.reverse ++ ( mapM' f l)
| [], acc => by simp [mapM.loop, mapM']
| a::l, acc => by simp [go l, mapM.loop, mapM']
@[simp] theorem mapM_nil [Monad m] (f : α m β) : [].mapM f = pure [] := rfl
@[simp] theorem mapM_cons [Monad m] [LawfulMonad m] (f : α m β) :
(a :: l).mapM f = (return ( f a) :: ( l.mapM f)) := by simp [ mapM'_eq_mapM, mapM']
@[simp] theorem mapM_append [Monad m] [LawfulMonad m] (f : α m β) {l₁ l₂ : List α} :
(l₁ ++ l₂).mapM f = (return ( l₁.mapM f) ++ ( l₂.mapM f)) := by induction l₁ <;> simp [*]
/-! ### forM -/
-- We use `List.forM` as the simp normal form, rather that `ForM.forM`.
-- As such we need to replace `List.forM_nil` and `List.forM_cons` from Lean:
@[simp] theorem forM_nil' [Monad m] : ([] : List α).forM f = (pure .unit : m PUnit) := rfl
@[simp] theorem forM_cons' [Monad m] :
(a::as).forM f = (f a >>= fun _ => as.forM f : m PUnit) :=
List.forM_cons _ _ _
/-! ### eraseIdx -/
@[simp] theorem eraseIdx_nil : ([] : List α).eraseIdx i = [] := rfl
@[simp] theorem eraseIdx_cons_zero : (a::as).eraseIdx 0 = as := rfl
@[simp] theorem eraseIdx_cons_succ : (a::as).eraseIdx (i+1) = a :: as.eraseIdx i := rfl
/-! ### find? -/
@[simp] theorem find?_nil : ([] : List α).find? p = none := rfl
theorem find?_cons : (a::as).find? p = match p a with | true => some a | false => as.find? p :=
rfl
/-! ### filter -/
@[simp] theorem filter_nil (p : α Bool) : filter p [] = [] := rfl
@[simp] theorem filter_cons_of_pos {p : α Bool} {a : α} (l) (pa : p a) :
filter p (a :: l) = a :: filter p l := by rw [filter, pa]
@[simp] theorem filter_cons_of_neg {p : α Bool} {a : α} (l) (pa : ¬ p a) :
filter p (a :: l) = filter p l := by rw [filter, eq_false_of_ne_true pa]
theorem filter_cons :
(x :: xs : List α).filter p = if p x then x :: (xs.filter p) else xs.filter p := by
split <;> simp [*]
theorem mem_filter : x filter p as x as p x := by
induction as with
| nil => simp [filter]
| cons a as ih =>
by_cases h : p a <;> simp [*, or_and_right]
· exact or_congr_left (and_iff_left_of_imp fun | rfl => h).symm
· exact (or_iff_right fun rfl, h' => h h').symm
theorem filter_eq_nil {l} : filter p l = [] a, a l ¬p a := by
simp only [eq_nil_iff_forall_not_mem, mem_filter, not_and]
/-! ### findSome? -/
@[simp] theorem findSome?_nil : ([] : List α).findSome? f = none := rfl
theorem findSome?_cons {f : α Option β} :
(a::as).findSome? f = match f a with | some b => some b | none => as.findSome? f :=
rfl
/-! ### replace -/
@[simp] theorem replace_nil [BEq α] : ([] : List α).replace a b = [] := rfl
theorem replace_cons [BEq α] {a : α} :
(a::as).replace b c = match a == b with | true => c::as | false => a :: replace as b c :=
rfl
@[simp] theorem replace_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).replace a b = b::as := by
simp [replace_cons]
/-! ### elem -/
@[simp] theorem elem_nil [BEq α] : ([] : List α).elem a = false := rfl
theorem elem_cons [BEq α] {a : α} :
(a::as).elem b = match b == a with | true => true | false => as.elem b :=
rfl
@[simp] theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by
simp [elem_cons]
/-! ### lookup -/
@[simp] theorem lookup_nil [BEq α] : ([] : List (α × β)).lookup a = none := rfl
theorem lookup_cons [BEq α] {k : α} :
((k,b)::es).lookup a = match a == k with | true => some b | false => es.lookup a :=
rfl
@[simp] theorem lookup_cons_self [BEq α] [LawfulBEq α] {k : α} : ((k,b)::es).lookup k = some b := by
simp [lookup_cons]
/-! ### zipWith -/
@[simp] theorem zipWith_nil_left {f : α β γ} : zipWith f [] l = [] := by
rfl
@[simp] theorem zipWith_nil_right {f : α β γ} : zipWith f l [] = [] := by
simp [zipWith]
@[simp] theorem zipWith_cons_cons {f : α β γ} :
zipWith f (a :: as) (b :: bs) = f a b :: zipWith f as bs := by
rfl
theorem zipWith_get? {f : α β γ} :
(List.zipWith f as bs).get? i = match as.get? i, bs.get? i with
| some a, some b => some (f a b) | _, _ => none := by
induction as generalizing bs i with
| nil => cases bs with
| nil => simp
| cons b bs => simp
| cons a as aih => cases bs with
| nil => simp
| cons b bs => cases i <;> simp_all
/-! ### zipWithAll -/
theorem zipWithAll_get? {f : Option α Option β γ} :
(zipWithAll f as bs).get? i = match as.get? i, bs.get? i with
| none, none => .none | a?, b? => some (f a? b?) := by
induction as generalizing bs i with
| nil => induction bs generalizing i with
| nil => simp
| cons b bs bih => cases i <;> simp_all
| cons a as aih => cases bs with
| nil =>
specialize @aih []
cases i <;> simp_all
| cons b bs => cases i <;> simp_all
/-! ### zip -/
@[simp] theorem zip_nil_left : zip ([] : List α) (l : List β) = [] := by
rfl
@[simp] theorem zip_nil_right : zip (l : List α) ([] : List β) = [] := by
simp [zip]
@[simp] theorem zip_cons_cons : zip (a :: as) (b :: bs) = (a, b) :: zip as bs := by
rfl
/-! ### unzip -/
@[simp] theorem unzip_nil : ([] : List (α × β)).unzip = ([], []) := rfl
@[simp] theorem unzip_cons {h : α × β} :
(h :: t).unzip = match unzip t with | (al, bl) => (h.1::al, h.2::bl) := rfl
/-! ### all / any -/
@[simp] theorem all_eq_true {l : List α} : l.all p x, x l p x := by induction l <;> simp [*]
@[simp] theorem any_eq_true {l : List α} : l.any p x, x l p x := by induction l <;> simp [*]
/-! ### enumFrom -/
@[simp] theorem enumFrom_nil : ([] : List α).enumFrom i = [] := rfl
@[simp] theorem enumFrom_cons : (a::as).enumFrom i = (i, a) :: as.enumFrom (i+1) := rfl
/-! ### iota -/
@[simp] theorem iota_zero : iota 0 = [] := rfl
@[simp] theorem iota_succ : iota (i+1) = (i+1) :: iota i := rfl
/-! ### intersperse -/
@[simp] theorem intersperse_nil (sep : α) : ([] : List α).intersperse sep = [] := rfl
@[simp] theorem intersperse_single (sep : α) : [x].intersperse sep = [x] := rfl
@[simp] theorem intersperse_cons₂ (sep : α) :
(x::y::zs).intersperse sep = x::sep::((y::zs).intersperse sep) := rfl
/-! ### isPrefixOf -/
@[simp] theorem isPrefixOf_nil_left [BEq α] : isPrefixOf ([] : List α) l = true := by
simp [isPrefixOf]
@[simp] theorem isPrefixOf_cons_nil [BEq α] : isPrefixOf (a::as) ([] : List α) = false := rfl
theorem isPrefixOf_cons₂ [BEq α] {a : α} :
isPrefixOf (a::as) (b::bs) = (a == b && isPrefixOf as bs) := rfl
@[simp] theorem isPrefixOf_cons₂_self [BEq α] [LawfulBEq α] {a : α} :
isPrefixOf (a::as) (a::bs) = isPrefixOf as bs := by simp [isPrefixOf_cons₂]
/-! ### isEqv -/
@[simp] theorem isEqv_nil_nil : isEqv ([] : List α) [] eqv = true := rfl
@[simp] theorem isEqv_nil_cons : isEqv ([] : List α) (a::as) eqv = false := rfl
@[simp] theorem isEqv_cons_nil : isEqv (a::as : List α) [] eqv = false := rfl
theorem isEqv_cons₂ : isEqv (a::as) (b::bs) eqv = (eqv a b && isEqv as bs eqv) := rfl
/-! ### dropLast -/
@[simp] theorem dropLast_nil : ([] : List α).dropLast = [] := rfl
@[simp] theorem dropLast_single : [x].dropLast = [] := rfl
@[simp] theorem dropLast_cons₂ :
(x::y::zs).dropLast = x :: (y::zs).dropLast := rfl
-- We may want to replace these `simp` attributes with explicit equational lemmas,
-- as we already have for all the non-monadic functions.
attribute [simp] mapA forA filterAuxM firstM anyM allM findM? findSomeM?
-- Previously `range.loop`, `mapM.loop`, `filterMapM.loop`, `forIn.loop`, `forIn'.loop`
-- had attribute `@[simp]`.
-- We don't currently provide simp lemmas,
-- as this is an internal implementation and they don't seem to be needed.
/-! ### minimum? -/
@[simp] theorem minimum?_nil [Min α] : ([] : List α).minimum? = none := rfl
-- We don't put `@[simp]` on `minimum?_cons`,
-- because the definition in terms of `foldl` is not useful for proofs.
theorem minimum?_cons [Min α] {xs : List α} : (x :: xs).minimum? = foldl min x xs := rfl
@[simp] theorem minimum?_eq_none_iff {xs : List α} [Min α] : xs.minimum? = none xs = [] := by
cases xs <;> simp [minimum?]
theorem minimum?_mem [Min α] (min_eq_or : a b : α, min a b = a min a b = b) :
{xs : List α} xs.minimum? = some a a xs := by
intro xs
match xs with
| nil => simp
| x :: xs =>
simp only [minimum?_cons, Option.some.injEq, List.mem_cons]
intro eq
induction xs generalizing x with
| nil =>
simp at eq
simp [eq]
| cons y xs ind =>
simp at eq
have p := ind _ eq
cases p with
| inl p =>
cases min_eq_or x y with | _ q => simp [p, q]
| inr p => simp [p, mem_cons]
theorem le_minimum?_iff [Min α] [LE α]
(le_min_iff : a b c : α, a min b c a b a c) :
{xs : List α} xs.minimum? = some a x, x a b, b xs x b
| nil => by simp
| cons x xs => by
rw [minimum?]
intro eq y
simp only [Option.some.injEq] at eq
induction xs generalizing x with
| nil =>
simp at eq
simp [eq]
| cons z xs ih =>
simp at eq
simp [ih _ eq, le_min_iff, and_assoc]
-- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `min_eq_or`,
-- and `le_min_iff`.
theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ·)]
(le_refl : a : α, a a)
(min_eq_or : a b : α, min a b = a min a b = b)
(le_min_iff : a b c : α, a min b c a b a c) {xs : List α} :
xs.minimum? = some a a xs b, b xs a b := by
refine fun h => minimum?_mem min_eq_or h, (le_minimum?_iff le_min_iff h _).1 (le_refl _), ?_
intro h₁, h₂
cases xs with
| nil => simp at h₁
| cons x xs =>
exact congrArg some <| anti.1
((le_minimum?_iff le_min_iff (xs := x::xs) rfl _).1 (le_refl _) _ h₁)
(h₂ _ (minimum?_mem min_eq_or (xs := x::xs) rfl))

View File

@@ -7,3 +7,4 @@ prelude
import Init.Data.Option.Basic
import Init.Data.Option.BasicAux
import Init.Data.Option.Instances
import Init.Data.Option.Lemmas

View File

@@ -1,7 +1,7 @@
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
Authors: Leonardo de Moura, Mario Carneiro
-/
prelude
import Init.Core
@@ -10,6 +10,9 @@ import Init.Coe
namespace Option
deriving instance DecidableEq for Option
deriving instance BEq for Option
def toMonad [Monad m] [Alternative m] : Option α m α
| none => failure
| some a => pure a
@@ -81,10 +84,131 @@ def merge (fn : ααα) : Option α → Option α → Option α
| none , some y => some y
| some x, some y => some <| fn x y
end Option
@[simp] theorem getD_none : getD none a = a := rfl
@[simp] theorem getD_some : getD (some a) b = a := rfl
deriving instance DecidableEq for Option
deriving instance BEq for Option
@[simp] theorem map_none' (f : α β) : none.map f = none := rfl
@[simp] theorem map_some' (a) (f : α β) : (some a).map f = some (f a) := rfl
@[simp] theorem none_bind (f : α Option β) : none.bind f = none := rfl
@[simp] theorem some_bind (a) (f : α Option β) : (some a).bind f = f a := rfl
/-- An elimination principle for `Option`. It is a nondependent version of `Option.recOn`. -/
@[simp, inline] protected def elim : Option α β (α β) β
| some x, _, f => f x
| none, y, _ => y
/-- Extracts the value `a` from an option that is known to be `some a` for some `a`. -/
@[inline] def get {α : Type u} : (o : Option α) isSome o α
| some x, _ => x
/-- `guard p a` returns `some a` if `p a` holds, otherwise `none`. -/
@[inline] def guard (p : α Prop) [DecidablePred p] (a : α) : Option α :=
if p a then some a else none
/--
Cast of `Option` to `List`. Returns `[a]` if the input is `some a`, and `[]` if it is `none`.
-/
@[inline] def toList : Option α List α
| none => .nil
| some a => .cons a .nil
/--
Cast of `Option` to `Array`. Returns `#[a]` if the input is `some a`, and `#[]` if it is `none`.
-/
@[inline] def toArray : Option α Array α
| none => List.toArray .nil
| some a => List.toArray (.cons a .nil)
/--
Two arguments failsafe function. Returns `f a b` if the inputs are `some a` and `some b`, and
"does nothing" otherwise.
-/
def liftOrGet (f : α α α) : Option α Option α Option α
| none, none => none
| some a, none => some a
| none, some b => some b
| some a, some b => some (f a b)
/-- Lifts a relation `α → β → Prop` to a relation `Option α → Option β → Prop` by just adding
`none ~ none`. -/
inductive Rel (r : α β Prop) : Option α Option β Prop
/-- If `a ~ b`, then `some a ~ some b` -/
| some {a b} : r a b Rel r (some a) (some b)
/-- `none ~ none` -/
| none : Rel r none none
/-- Flatten an `Option` of `Option`, a specialization of `joinM`. -/
@[simp, inline] def join (x : Option (Option α)) : Option α := x.bind id
/-- Like `Option.mapM` but for applicative functors. -/
@[inline] protected def mapA [Applicative m] {α β} (f : α m β) : Option α m (Option β)
| none => pure none
| some x => some <$> f x
/--
If you maybe have a monadic computation in a `[Monad m]` which produces a term of type `α`, then
there is a naturally associated way to always perform a computation in `m` which maybe produces a
result.
-/
@[inline] def sequence [Monad m] {α : Type u} : Option (m α) m (Option α)
| none => pure none
| some fn => some <$> fn
/-- A monadic analogue of `Option.elim`. -/
@[inline] def elimM [Monad m] (x : m (Option α)) (y : m β) (z : α m β) : m β :=
do ( x).elim y z
/-- A monadic analogue of `Option.getD`. -/
@[inline] def getDM [Monad m] (x : Option α) (y : m α) : m α :=
match x with
| some a => pure a
| none => y
instance (α) [BEq α] [LawfulBEq α] : LawfulBEq (Option α) where
rfl {x} :=
match x with
| some x => LawfulBEq.rfl (α := α)
| none => rfl
eq_of_beq {x y h} := by
match x, y with
| some x, some y => rw [LawfulBEq.eq_of_beq (α := α) h]
| none, none => rfl
@[simp] theorem all_none : Option.all p none = true := rfl
@[simp] theorem all_some : Option.all p (some x) = p x := rfl
/-- The minimum of two optional values. -/
protected def min [Min α] : Option α Option α Option α
| some x, some y => some (Min.min x y)
| some x, none => some x
| none, some y => some y
| none, none => none
instance [Min α] : Min (Option α) where min := Option.min
@[simp] theorem min_some_some [Min α] {a b : α} : min (some a) (some b) = some (min a b) := rfl
@[simp] theorem min_some_none [Min α] {a : α} : min (some a) none = some a := rfl
@[simp] theorem min_none_some [Min α] {b : α} : min none (some b) = some b := rfl
@[simp] theorem min_none_none [Min α] : min (none : Option α) none = none := rfl
/-- The maximum of two optional values. -/
protected def max [Max α] : Option α Option α Option α
| some x, some y => some (Max.max x y)
| some x, none => some x
| none, some y => some y
| none, none => none
instance [Max α] : Max (Option α) where max := Option.max
@[simp] theorem max_some_some [Max α] {a b : α} : max (some a) (some b) = some (max a b) := rfl
@[simp] theorem max_some_none [Max α] {a : α} : max (some a) none = some a := rfl
@[simp] theorem max_none_some [Max α] {b : α} : max none (some b) = some b := rfl
@[simp] theorem max_none_none [Max α] : max (none : Option α) none = none := rfl
end Option
instance [LT α] : LT (Option α) where
lt := Option.lt (· < ·)

View File

@@ -8,11 +8,82 @@ import Init.Data.Option.Basic
universe u v
theorem Option.eq_of_eq_some {α : Type u} : {x y : Option α}, (z, x = some z y = some z) x = y
namespace Option
theorem eq_of_eq_some {α : Type u} : {x y : Option α}, (z, x = some z y = some z) x = y
| none, none, _ => rfl
| none, some z, h => Option.noConfusion ((h z).2 rfl)
| some z, none, h => Option.noConfusion ((h z).1 rfl)
| some _, some w, h => Option.noConfusion ((h w).2 rfl) (congrArg some)
theorem Option.eq_none_of_isNone {α : Type u} : {o : Option α}, o.isNone o = none
theorem eq_none_of_isNone {α : Type u} : {o : Option α}, o.isNone o = none
| none, _ => rfl
instance : Membership α (Option α) := fun a b => b = some a
@[simp] theorem mem_def {a : α} {b : Option α} : a b b = some a := .rfl
instance [DecidableEq α] (j : α) (o : Option α) : Decidable (j o) :=
inferInstanceAs <| Decidable (o = some j)
theorem isNone_iff_eq_none {o : Option α} : o.isNone o = none :=
Option.eq_none_of_isNone, fun e => e.symm rfl
theorem some_inj {a b : α} : some a = some b a = b := by simp; rfl
/--
`o = none` is decidable even if the wrapped type does not have decidable equality.
This is not an instance because it is not definitionally equal to `instance : DecidableEq Option`.
Try to use `o.isNone` or `o.isSome` instead.
-/
@[inline] def decidable_eq_none {o : Option α} : Decidable (o = none) :=
decidable_of_decidable_of_iff isNone_iff_eq_none
instance {p : α Prop} [DecidablePred p] : o : Option α, Decidable ( a, a o p a)
| none => isTrue nofun
| some a =>
if h : p a then isTrue fun _ e => some_inj.1 e h
else isFalse <| mt (· _ rfl) h
instance {p : α Prop} [DecidablePred p] : o : Option α, Decidable (Exists fun a => a o p a)
| none => isFalse nofun
| some a => if h : p a then isTrue _, rfl, h else isFalse fun _, rfl, hn => h hn
/--
Partial bind. If for some `x : Option α`, `f : Π (a : α), a ∈ x → Option β` is a
partial function defined on `a : α` giving an `Option β`, where `some a = x`,
then `pbind x f h` is essentially the same as `bind x f`
but is defined only when all `x = some a`, using the proof to apply `f`.
-/
@[simp, inline]
def pbind : x : Option α, ( a : α, a x Option β) Option β
| none, _ => none
| some a, f => f a rfl
/--
Partial map. If `f : Π a, p a → β` is a partial function defined on `a : α` satisfying `p`,
then `pmap f x h` is essentially the same as `map f x` but is defined only when all members of `x`
satisfy `p`, using the proof to apply `f`.
-/
@[simp, inline] def pmap {p : α Prop} (f : a : α, p a β) :
x : Option α, ( a, a x p a) Option β
| none, _ => none
| some a, H => f a (H a rfl)
/-- Map a monadic function which returns `Unit` over an `Option`. -/
@[inline] protected def forM [Pure m] : Option α (α m PUnit) m PUnit
| none , _ => pure ()
| some a, f => f a
instance : ForM m (Option α) α :=
Option.forM
instance : ForIn' m (Option α) α inferInstance where
forIn' x init f := do
match x with
| none => return init
| some a =>
match f a rfl init with
| .done r | .yield r => return r
end Option

View File

@@ -0,0 +1,238 @@
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
prelude
import Init.Data.Option.Instances
import Init.Classical
import Init.Ext
namespace Option
theorem mem_iff {a : α} {b : Option α} : a b b = a := .rfl
theorem some_ne_none (x : α) : some x none := nofun
protected theorem «forall» {p : Option α Prop} : ( x, p x) p none x, p (some x) :=
fun h => h _, fun _ => h _, fun h x => Option.casesOn x h.1 h.2
protected theorem «exists» {p : Option α Prop} :
( x, p x) p none x, p (some x) :=
fun | none, hx => .inl hx | some x, hx => .inr x, hx,
fun | .inl h => _, h | .inr _, hx => _, hx
theorem get_mem : {o : Option α} (h : isSome o), o.get h o
| some _, _ => rfl
theorem get_of_mem : {o : Option α} (h : isSome o), a o o.get h = a
| _, _, rfl => rfl
theorem not_mem_none (a : α) : a (none : Option α) := nofun
@[simp] theorem some_get : {x : Option α} (h : isSome x), some (x.get h) = x
| some _, _ => rfl
@[simp] theorem get_some (x : α) (h : isSome (some x)) : (some x).get h = x := rfl
theorem getD_of_ne_none {x : Option α} (hx : x none) (y : α) : some (x.getD y) = x := by
cases x; {contradiction}; rw [getD_some]
theorem getD_eq_iff {o : Option α} {a b} : o.getD a = b (o = some b o = none a = b) := by
cases o <;> simp
theorem mem_unique {o : Option α} {a b : α} (ha : a o) (hb : b o) : a = b :=
some.inj <| ha hb
@[ext] theorem ext : {o₁ o₂ : Option α}, ( a, a o₁ a o₂) o₁ = o₂
| none, none, _ => rfl
| some _, _, H => ((H _).1 rfl).symm
| _, some _, H => (H _).2 rfl
theorem eq_none_iff_forall_not_mem : o = none a, a o :=
fun e a h => by rw [e] at h; (cases h), fun h => ext <| by simp; exact h
@[simp] theorem isSome_none : @isSome α none = false := rfl
@[simp] theorem isSome_some : isSome (some a) = true := rfl
theorem isSome_iff_exists : isSome x a, x = some a := by cases x <;> simp [isSome]
@[simp] theorem isNone_none : @isNone α none = true := rfl
@[simp] theorem isNone_some : isNone (some a) = false := rfl
@[simp] theorem not_isSome : isSome a = false a.isNone = true := by
cases a <;> simp
theorem eq_some_iff_get_eq : o = some a h : o.isSome, o.get h = a := by
cases o <;> simp; nofun
theorem eq_some_of_isSome : {o : Option α} (h : o.isSome), o = some (o.get h)
| some _, _ => rfl
theorem not_isSome_iff_eq_none : ¬o.isSome o = none := by
cases o <;> simp
theorem ne_none_iff_isSome : o none o.isSome := by cases o <;> simp
theorem ne_none_iff_exists : o none x, some x = o := by cases o <;> simp
theorem ne_none_iff_exists' : o none x, o = some x :=
ne_none_iff_exists.trans <| exists_congr fun _ => eq_comm
theorem bex_ne_none {p : Option α Prop} : ( x, (_ : x none), p x) x, p (some x) :=
fun x, hx, hp => x.get <| ne_none_iff_isSome.1 hx, by rwa [some_get],
fun x, hx => some x, some_ne_none x, hx
theorem ball_ne_none {p : Option α Prop} : ( x (_ : x none), p x) x, p (some x) :=
fun h x => h (some x) (some_ne_none x),
fun h x hx => by
have := h <| x.get <| ne_none_iff_isSome.1 hx
simp [some_get] at this
exact this
@[simp] theorem pure_def : pure = @some α := rfl
@[simp] theorem bind_eq_bind : bind = @Option.bind α β := rfl
@[simp] theorem bind_some (x : Option α) : x.bind some = x := by cases x <;> rfl
@[simp] theorem bind_none (x : Option α) : x.bind (fun _ => none (α := β)) = none := by
cases x <;> rfl
@[simp] theorem bind_eq_some : x.bind f = some b a, x = some a f a = some b := by
cases x <;> simp
@[simp] theorem bind_eq_none {o : Option α} {f : α Option β} :
o.bind f = none a, o = some a f a = none := by cases o <;> simp
theorem bind_eq_none' {o : Option α} {f : α Option β} :
o.bind f = none b a, a o b f a := by
simp only [eq_none_iff_forall_not_mem, not_exists, not_and, mem_def, bind_eq_some]
theorem bind_comm {f : α β Option γ} (a : Option α) (b : Option β) :
(a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y := by
cases a <;> cases b <;> rfl
theorem bind_assoc (x : Option α) (f : α Option β) (g : β Option γ) :
(x.bind f).bind g = x.bind fun y => (f y).bind g := by cases x <;> rfl
theorem join_eq_some : x.join = some a x = some (some a) := by
simp
theorem join_ne_none : x.join none z, x = some (some z) := by
simp only [ne_none_iff_exists', join_eq_some, iff_self]
theorem join_ne_none' : ¬x.join = none z, x = some (some z) :=
join_ne_none
theorem join_eq_none : o.join = none o = none o = some none :=
match o with | none | some none | some (some _) => by simp
theorem bind_id_eq_join {x : Option (Option α)} : x.bind id = x.join := rfl
@[simp] theorem map_eq_map : Functor.map f = Option.map f := rfl
theorem map_none : f <$> none = none := rfl
theorem map_some : f <$> some a = some (f a) := rfl
@[simp] theorem map_eq_some' : x.map f = some b a, x = some a f a = b := by cases x <;> simp
theorem map_eq_some : f <$> x = some b a, x = some a f a = b := map_eq_some'
@[simp] theorem map_eq_none' : x.map f = none x = none := by
cases x <;> simp only [map_none', map_some', eq_self_iff_true]
theorem map_eq_none : f <$> x = none x = none := map_eq_none'
theorem map_eq_bind {x : Option α} : x.map f = x.bind (some f) := by
cases x <;> simp [Option.bind]
theorem map_congr {x : Option α} (h : a, a x f a = g a) : x.map f = x.map g := by
cases x <;> simp only [map_none', map_some', h, mem_def]
@[simp] theorem map_id' : Option.map (@id α) = id := map_id
@[simp] theorem map_id'' {x : Option α} : (x.map fun a => a) = x := congrFun map_id x
@[simp] theorem map_map (h : β γ) (g : α β) (x : Option α) :
(x.map g).map h = x.map (h g) := by
cases x <;> simp only [map_none', map_some', ··]
theorem comp_map (h : β γ) (g : α β) (x : Option α) : x.map (h g) = (x.map g).map h :=
(map_map ..).symm
@[simp] theorem map_comp_map (f : α β) (g : β γ) :
Option.map g Option.map f = Option.map (g f) := by funext x; simp
theorem mem_map_of_mem (g : α β) (h : a x) : g a Option.map g x := h.symm map_some' ..
theorem bind_map_comm {α β} {x : Option (Option α)} {f : α β} :
x.bind (Option.map f) = (x.map (Option.map f)).bind id := by cases x <;> simp
theorem join_map_eq_map_join {f : α β} {x : Option (Option α)} :
(x.map (Option.map f)).join = x.join.map f := by cases x <;> simp
theorem join_join {x : Option (Option (Option α))} : x.join.join = (x.map join).join := by
cases x <;> simp
theorem mem_of_mem_join {a : α} {x : Option (Option α)} (h : a x.join) : some a x :=
h.symm join_eq_some.1 h
@[simp] theorem some_orElse (a : α) (x : Option α) : (some a <|> x) = some a := rfl
@[simp] theorem none_orElse (x : Option α) : (none <|> x) = x := rfl
@[simp] theorem orElse_none (x : Option α) : (x <|> none) = x := by cases x <;> rfl
theorem map_orElse {x y : Option α} : (x <|> y).map f = (x.map f <|> y.map f) := by
cases x <;> simp
@[simp] theorem guard_eq_some [DecidablePred p] : guard p a = some b a = b p a :=
if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]
theorem liftOrGet_eq_or_eq {f : α α α} (h : a b, f a b = a f a b = b) :
o₁ o₂, liftOrGet f o₁ o₂ = o₁ liftOrGet f o₁ o₂ = o₂
| none, none => .inl rfl
| some a, none => .inl rfl
| none, some b => .inr rfl
| some a, some b => by have := h a b; simp [liftOrGet] at this ; exact this
@[simp] theorem liftOrGet_none_left {f} {b : Option α} : liftOrGet f none b = b := by
cases b <;> rfl
@[simp] theorem liftOrGet_none_right {f} {a : Option α} : liftOrGet f a none = a := by
cases a <;> rfl
@[simp] theorem liftOrGet_some_some {f} {a b : α} :
liftOrGet f (some a) (some b) = f a b := rfl
theorem elim_none (x : β) (f : α β) : none.elim x f = x := rfl
theorem elim_some (x : β) (f : α β) (a : α) : (some a).elim x f = f a := rfl
@[simp] theorem getD_map (f : α β) (x : α) (o : Option α) :
(o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl
section
attribute [local instance] Classical.propDecidable
/-- An arbitrary `some a` with `a : α` if `α` is nonempty, and otherwise `none`. -/
noncomputable def choice (α : Type _) : Option α :=
if h : Nonempty α then some (Classical.choice h) else none
theorem choice_eq {α : Type _} [Subsingleton α] (a : α) : choice α = some a := by
simp [choice]
rw [dif_pos (a : Nonempty α)]
simp; apply Subsingleton.elim
theorem choice_isSome_iff_nonempty {α : Type _} : (choice α).isSome Nonempty α :=
fun h => (choice α).get h, fun h => by simp only [choice, dif_pos h, isSome_some]
end
@[simp] theorem toList_some (a : α) : (a : Option α).toList = [a] := rfl
@[simp] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl

View File

@@ -12,16 +12,105 @@ inductive Ordering where
| lt | eq | gt
deriving Inhabited, BEq
namespace Ordering
deriving instance DecidableEq for Ordering
/-- Swaps less and greater ordering results -/
def swap : Ordering Ordering
| .lt => .gt
| .eq => .eq
| .gt => .lt
/--
If `o₁` and `o₂` are `Ordering`, then `o₁.then o₂` returns `o₁` unless it is `.eq`,
in which case it returns `o₂`. Additionally, it has "short-circuiting" semantics similar to
boolean `x && y`: if `o₁` is not `.eq` then the expression for `o₂` is not evaluated.
This is a useful primitive for constructing lexicographic comparator functions:
```
structure Person where
name : String
age : Nat
instance : Ord Person where
compare a b := (compare a.name b.name).then (compare b.age a.age)
```
This example will sort people first by name (in ascending order) and will sort people with
the same name by age (in descending order). (If all fields are sorted ascending and in the same
order as they are listed in the structure, you can also use `deriving Ord` on the structure
definition for the same effect.)
-/
@[macro_inline] def «then» : Ordering Ordering Ordering
| .eq, f => f
| o, _ => o
/--
Check whether the ordering is 'equal'.
-/
def isEq : Ordering Bool
| eq => true
| _ => false
/--
Check whether the ordering is 'not equal'.
-/
def isNe : Ordering Bool
| eq => false
| _ => true
/--
Check whether the ordering is 'less than or equal to'.
-/
def isLE : Ordering Bool
| gt => false
| _ => true
/--
Check whether the ordering is 'less than'.
-/
def isLT : Ordering Bool
| lt => true
| _ => false
/--
Check whether the ordering is 'greater than'.
-/
def isGT : Ordering Bool
| gt => true
| _ => false
/--
Check whether the ordering is 'greater than or equal'.
-/
def isGE : Ordering Bool
| lt => false
| _ => true
end Ordering
@[inline] def compareOfLessAndEq {α} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering :=
if x < y then Ordering.lt
else if x = y then Ordering.eq
else Ordering.gt
/--
Compare `a` and `b` lexicographically by `cmp₁` and `cmp₂`. `a` and `b` are
first compared by `cmp₁`. If this returns 'equal', `a` and `b` are compared
by `cmp₂` to break the tie.
-/
@[inline] def compareLex (cmp₁ cmp₂ : α β Ordering) (a : α) (b : β) : Ordering :=
(cmp₁ a b).then (cmp₂ a b)
class Ord (α : Type u) where
compare : α α Ordering
export Ord (compare)
@[inline] def compareOfLessAndEq {α} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering :=
if x < y then Ordering.lt
else if x = y then Ordering.eq
else Ordering.gt
/--
Compare `x` and `y` by comparing `f x` and `f y`.
-/
@[inline] def compareOn [ord : Ord β] (f : α β) (x y : α) : Ordering :=
compare (f x) (f y)
instance : Ord Nat where
compare x y := compareOfLessAndEq x y
@@ -71,13 +160,55 @@ def ltOfOrd [Ord α] : LT α where
instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) :=
inferInstanceAs (DecidableRel (fun a b => compare a b == Ordering.lt))
def Ordering.isLE : Ordering Bool
| Ordering.lt => true
| Ordering.eq => true
| Ordering.gt => false
def leOfOrd [Ord α] : LE α where
le a b := (compare a b).isLE
instance [Ord α] : DecidableRel (@LE.le α leOfOrd) :=
inferInstanceAs (DecidableRel (fun a b => (compare a b).isLE))
namespace Ord
/--
Derive a `BEq` instance from an `Ord` instance.
-/
protected def toBEq (ord : Ord α) : BEq α where
beq x y := ord.compare x y == .eq
/--
Derive an `LT` instance from an `Ord` instance.
-/
protected def toLT (_ : Ord α) : LT α :=
ltOfOrd
/--
Derive an `LE` instance from an `Ord` instance.
-/
protected def toLE (_ : Ord α) : LE α :=
leOfOrd
/--
Invert the order of an `Ord` instance.
-/
protected def opposite (ord : Ord α) : Ord α where
compare x y := ord.compare y x
/--
`ord.on f` compares `x` and `y` by comparing `f x` and `f y` according to `ord`.
-/
protected def on (ord : Ord β) (f : α β) : Ord α where
compare := compareOn f
/--
Derive the lexicographic order on products `α × β` from orders for `α` and `β`.
-/
protected def lex (_ : Ord α) (_ : Ord β) : Ord (α × β) :=
lexOrd
/--
Create an order which compares elements first by `ord₁` and then, if this
returns 'equal', by `ord₂`.
-/
protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
compare := compareLex ord₁.compare ord₂.compare
end Ord

View File

@@ -42,17 +42,15 @@ instance : Repr StdGen where
def stdNext : StdGen Nat × StdGen
| s1, s2 =>
let s1 : Int := s1
let s2 : Int := s2
let k : Int := s1 / 53668
let s1' : Int := 40014 * ((s1 : Int) - k * 53668) - k * 12211
let s1'' : Int := if s1' < 0 then s1' + 2147483563 else s1'
let k' : Int := s2 / 52774
let s2' : Int := 40692 * ((s2 : Int) - k' * 52774) - k' * 3791
let s2'' : Int := if s2' < 0 then s2' + 2147483399 else s2'
let z : Int := s1'' - s2''
let z' : Int := if z < 1 then z + 2147483562 else z % 2147483562
(z'.toNat, s1''.toNat, s2''.toNat)
let k : Int := Int.ofNat (s1 / 53668)
let s1' : Int := 40014 * (Int.ofNat s1 - k * 53668) - k * 12211
let s1'' : Nat := if s1' < 0 then (s1' + 2147483563).toNat else s1'.toNat
let k' : Int := Int.ofNat (s2 / 52774)
let s2' : Int := 40692 * (Int.ofNat s2 - k' * 52774) - k' * 3791
let s2'' : Nat := if s2' < 0 then (s2' + 2147483399).toNat else s2'.toNat
let z : Int := Int.ofNat s1'' - Int.ofNat s2''
let z' : Nat := if z < 1 then (z + 2147483562).toNat else z.toNat % 2147483562
(z', s1'', s2'')
def stdSplit : StdGen StdGen × StdGen
| g@s1, s2 =>

View File

@@ -587,6 +587,9 @@ def mkLit (kind : SyntaxNodeKind) (val : String) (info := SourceInfo.none) : TSy
let atom : Syntax := Syntax.atom info val
mkNode kind #[atom]
def mkCharLit (val : Char) (info := SourceInfo.none) : CharLit :=
mkLit charLitKind (Char.quote val) info
def mkStrLit (val : String) (info := SourceInfo.none) : StrLit :=
mkLit strLitKind (String.quote val) info
@@ -1004,6 +1007,7 @@ instance [Quote α k] [CoeHTCT (TSyntax k) (TSyntax [k'])] : Quote α k' := ⟨f
instance : Quote Term := ⟨id⟩
instance : Quote Bool := ⟨fun | true => mkCIdent ``Bool.true | false => mkCIdent ``Bool.false⟩
instance : Quote Char charLitKind := ⟨Syntax.mkCharLit⟩
instance : Quote String strLitKind := ⟨Syntax.mkStrLit⟩
instance : Quote Nat numLitKind := ⟨fun n => Syntax.mkNumLit <| toString n⟩
instance : Quote Substring := ⟨fun s => Syntax.mkCApp ``String.toSubstring' #[quote s.toString]⟩

View File

@@ -173,16 +173,15 @@ syntax (name := calcTactic) "calc" calcSteps : tactic
/--
Denotes a term that was omitted by the pretty printer.
This is only used for pretty printing, and it cannot be elaborated.
The presence of `⋯` is controlled by the `pp.deepTerms` and `pp.deepTerms.threshold`
options.
The presence of `⋯` is controlled by the `pp.deepTerms` and `pp.proofs` options.
-/
syntax "" : term
macro_rules | `() => Macro.throwError "\
Error: The '⋯' token is used by the pretty printer to indicate omitted terms, \
and it cannot be elaborated. \
Its presence in pretty printing output is controlled by the 'pp.deepTerms' and \
`pp.deepTerms.threshold` options."
and it cannot be elaborated.\
\n\nIts presence in pretty printing output is controlled by the 'pp.deepTerms' and `pp.proofs` options. \
These options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`."
@[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
| `($(_)) => `(())

View File

@@ -172,6 +172,19 @@ example (x : Nat) (h : x ≠ x) : p := by contradiction
-/
syntax (name := contradiction) "contradiction" : tactic
/--
Changes the goal to `False`, retaining as much information as possible:
* If the goal is `False`, do nothing.
* If the goal is an implication or a function type, introduce the argument and restart.
(In particular, if the goal is `x ≠ y`, introduce `x = y`.)
* Otherwise, for a propositional goal `P`, replace it with `¬ ¬ P`
(attempting to find a `Decidable` instance, but otherwise falling back to working classically)
and introduce `¬ P`.
* For a non-propositional goal use `False.elim`.
-/
syntax (name := falseOrByContra) "false_or_by_contra" : tactic
/--
`apply e` tries to match the current goal against the conclusion of `e`'s type.
If it succeeds, then the tactic returns as many subgoals as the number of premises that
@@ -201,6 +214,9 @@ and implicit parameters are also converted into new goals.
-/
syntax (name := refine') "refine' " term : tactic
/-- `exfalso` converts a goal `⊢ tgt` into `⊢ False` by applying `False.elim`. -/
macro "exfalso" : tactic => `(tactic| refine False.elim ?_)
/--
If the main goal's target type is an inductive type, `constructor` solves it with
the first matching constructor, or else fails.

View File

@@ -90,6 +90,11 @@ def toCInitName (n : Name) : M String := do
def emitCInitName (n : Name) : M Unit :=
toCInitName n >>= emit
def shouldExport (n : Name) : Bool :=
-- HACK: exclude symbols very unlikely to be used by the interpreter or other consumers of
-- libleanshared to avoid Windows symbol limit
!(`Lean.Compiler.LCNF).isPrefixOf n
def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M Unit := do
let ps := decl.params
let env getEnv
@@ -98,7 +103,7 @@ def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M U
else if isExternal then emit "extern "
else emit "LEAN_EXPORT "
else
if !isExternal then emit "LEAN_EXPORT "
if !isExternal && shouldExport decl.name then emit "LEAN_EXPORT "
emit (toCType decl.resultType ++ " " ++ cppBaseName)
unless ps.isEmpty do
emit "("
@@ -640,7 +645,7 @@ def emitDeclAux (d : Decl) : M Unit := do
let baseName toCName f;
if xs.size == 0 then
emit "static "
else
else if shouldExport f then
emit "LEAN_EXPORT " -- make symbol visible to the interpreter
emit (toCType t); emit " ";
if xs.size > 0 then

View File

@@ -194,3 +194,11 @@ def insertMany [ForIn Id ρ α] (s : HashSet α) (as : ρ) : HashSet α := Id.ru
for a in as do
s := s.insert a
return s
/--
`O(|t|)` amortized. Merge two `HashSet`s.
-/
@[inline]
def merge {α : Type u} [BEq α] [Hashable α] (s t : HashSet α) : HashSet α :=
t.fold (init := s) fun s a => s.insert a
-- We don't use `insertMany` here because it gives weird universes.

View File

@@ -98,7 +98,7 @@ protected def toString : JsonNumber → String
-- grow exponentially in the value of exponent.
let exp : Int := 9 + countDigits m - (e : Int)
let exp := if exp < 0 then exp else 0
let e' := (10 : Int) ^ (e - exp.natAbs)
let e' := 10 ^ (e - exp.natAbs)
let left := (m / e').repr
if m % e' = 0 && exp = 0 then
s!"{sign}{left}"

View File

@@ -24,7 +24,7 @@ instance : Repr Rat where
@[inline] def Rat.normalize (a : Rat) : Rat :=
let n := Nat.gcd a.num.natAbs a.den
if n == 1 then a else { num := a.num / n, den := a.den / n }
if n == 1 then a else { num := a.num.div n, den := a.den / n }
def mkRat (num : Int) (den : Nat) : Rat :=
if den == 0 then { num := 0 } else Rat.normalize { num, den }
@@ -48,7 +48,7 @@ protected def lt (a b : Rat) : Bool :=
protected def mul (a b : Rat) : Rat :=
let g1 := Nat.gcd a.den b.num.natAbs
let g2 := Nat.gcd a.num.natAbs b.den
{ num := (a.num / g2)*(b.num / g1)
{ num := (a.num.div g2)*(b.num.div g1)
den := (b.den / g2)*(a.den / g1) }
protected def inv (a : Rat) : Rat :=
@@ -68,12 +68,12 @@ protected def add (a b : Rat) : Rat :=
{ num := a.num * b.den + b.num * a.den, den := a.den * b.den }
else
let den := (a.den / g) * b.den
let num := (b.den / g) * a.num + (a.den / g) * b.num
let num := Int.ofNat (b.den / g) * a.num + Int.ofNat (a.den / g) * b.num
let g1 := Nat.gcd num.natAbs g
if g1 == 1 then
{ num, den }
else
{ num := num / g1, den := den / g1 }
{ num := num.div g1, den := den / g1 }
protected def sub (a b : Rat) : Rat :=
let g := Nat.gcd a.den b.den
@@ -86,7 +86,7 @@ protected def sub (a b : Rat) : Rat :=
if g1 == 1 then
{ num, den }
else
{ num := num / g1, den := den / g1 }
{ num := num.div g1, den := den / g1 }
protected def neg (a : Rat) : Rat :=
{ a with num := - a.num }
@@ -95,14 +95,14 @@ protected def floor (a : Rat) : Int :=
if a.den == 1 then
a.num
else
let r := a.num / a.den
let r := a.num.mod a.den
if a.num < 0 then r - 1 else r
protected def ceil (a : Rat) : Int :=
if a.den == 1 then
a.num
else
let r := a.num / a.den
let r := a.num.mod a.den
if a.num > 0 then r + 1 else r
instance : LT Rat where

View File

@@ -756,8 +756,9 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
for i in [:views.size] do
let indFVar := indFVars[i]!
Term.addLocalVarInfo views[i]!.declId indFVar
let r := rs[i]!
let type mkForallFVars params r.type
let r := rs[i]!
let type := r.type |>.abstract r.params |>.instantiateRev params
let type mkForallFVars params type
let ctors withExplicitToImplicit params (elabCtors indFVars indFVar params r)
indTypesArray := indTypesArray.push { name := r.view.declName, type, ctors }
Term.synthesizeSyntheticMVarsNoPostponing

View File

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Util.HasConstCache
import Lean.Meta.CasesOn
import Lean.Meta.Match.Match
import Lean.Elab.RecAppSyntax
import Lean.Elab.PreDefinition.Basic
@@ -83,20 +82,6 @@ private partial def toBelow (below : Expr) (numIndParams : Nat) (recArg : Expr)
withBelowDict below numIndParams fun C belowDict =>
toBelowAux C belowDict recArg below
/--
This method is used after `matcherApp.addArg arg` to check whether the new type of `arg` has been "refined/modified"
in at least one alternative.
-/
def refinedArgType (matcherApp : MatcherApp) (arg : Expr) : MetaM Bool := do
let argType inferType arg
(Array.zip matcherApp.alts matcherApp.altNumParams).anyM fun (alt, numParams) =>
lambdaTelescope alt fun xs _ => do
if xs.size >= numParams then
let refinedArg := xs[numParams - 1]!
return !( isDefEq ( inferType refinedArg) argType)
else
return false
private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) (below : Expr) (e : Expr) : M Expr :=
let containsRecFn (e : Expr) : StateRefT (HasConstCache recFnName) M Bool :=
modifyGet (·.contains e)
@@ -143,7 +128,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
return mkAppN f fArgs
else
return mkAppN ( loop below f) ( args.mapM (loop below))
match ( matchMatcherApp? e) with
match ( matchMatcherApp? (alsoCasesOn := true) e) with
| some matcherApp =>
if !recArgHasLooseBVarsAt recFnName recArgInfo.recArgPos e then
processApp e
@@ -165,10 +150,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
If this is too annoying in practice, we may replace `ys` with the matching term, but
this may generate weird error messages, when it doesn't work. -/
trace[Elab.definition.structural] "below before matcherApp.addArg: {below} : {← inferType below}"
let matcherApp mapError (matcherApp.addArg below) (fun msg => "failed to add `below` argument to 'matcher' application" ++ indentD msg)
if !( refinedArgType matcherApp below) then
processApp e
else
if let some matcherApp matcherApp.addArg? below then
let altsNew (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun (alt, numParams) =>
lambdaTelescope alt fun xs altBody => do
trace[Elab.definition.structural] "altNumParams: {numParams}, xs: {xs}"
@@ -177,21 +159,8 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
let belowForAlt := xs[numParams - 1]!
mkLambdaFVars xs ( loop belowForAlt altBody)
pure { matcherApp with alts := altsNew }.toExpr
| none =>
match ( toCasesOnApp? e) with
| some casesOnApp =>
if !recArgHasLooseBVarsAt recFnName recArgInfo.recArgPos e then
processApp e
else if let some casesOnApp casesOnApp.addArg? below (checkIfRefined := true) then
let altsNew (Array.zip casesOnApp.alts casesOnApp.altNumParams).mapM fun (alt, numParams) =>
lambdaTelescope alt fun xs altBody => do
unless xs.size >= numParams do
throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}"
let belowForAlt := xs[numParams]!
mkLambdaFVars xs ( loop belowForAlt altBody)
return { casesOnApp with alts := altsNew }.toExpr
else
processApp e
else
processApp e
| none => processApp e
| e => ensureNoRecFn recFnName e
loop below e |>.run' {}

View File

@@ -57,7 +57,7 @@ where
def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
withOptions (tactic.hygienic.set · false) do
let eqnTypes withNewMCtxDepth <| lambdaTelescope info.value fun xs body => do
let eqnTypes withNewMCtxDepth <| lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
let us := info.levelParams.map mkLevelParam
let target mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
let goal mkFreshExprSyntheticOpaqueMVar target

View File

@@ -107,7 +107,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
withOptions (tactic.hygienic.set · false) do
let baseName := mkPrivateName ( getEnv) declName
let eqnTypes withNewMCtxDepth <| lambdaTelescope info.value fun xs body => do
let eqnTypes withNewMCtxDepth <| lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
let us := info.levelParams.map mkLevelParam
let target mkEq (mkAppN (Lean.mkConst declName us) xs) body
let goal mkFreshExprSyntheticOpaqueMVar target

View File

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Util.HasConstCache
import Lean.Meta.CasesOn
import Lean.Meta.Match.Match
import Lean.Meta.Tactic.Simp.Main
import Lean.Meta.Tactic.Cleanup
@@ -77,34 +76,16 @@ where
| Expr.proj n i e => return mkProj n i ( loop F e)
| Expr.const .. => if e.isConstOf recFnName then processRec F e else return e
| Expr.app .. =>
match ( matchMatcherApp? e) with
match ( matchMatcherApp? (alsoCasesOn := true) e) with
| some matcherApp =>
if let some matcherApp matcherApp.addArg? F then
if !( Structural.refinedArgType matcherApp F) then
processApp F e
else
let altsNew (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun (alt, numParams) =>
lambdaTelescope alt fun xs altBody => do
unless xs.size >= numParams do
throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
let FAlt := xs[numParams - 1]!
mkLambdaFVars xs ( loop FAlt altBody)
return { matcherApp with alts := altsNew, discrs := ( matcherApp.discrs.mapM (loop F)) }.toExpr
else
processApp F e
| none =>
match ( toCasesOnApp? e) with
| some casesOnApp =>
if let some casesOnApp casesOnApp.addArg? F (checkIfRefined := true) then
let altsNew (Array.zip casesOnApp.alts casesOnApp.altNumParams).mapM fun (alt, numParams) =>
let altsNew (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun (alt, numParams) =>
lambdaTelescope alt fun xs altBody => do
unless xs.size >= numParams do
throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}"
let FAlt := xs[numParams]!
throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
let FAlt := xs[numParams - 1]!
mkLambdaFVars xs ( loop FAlt altBody)
return { casesOnApp with
alts := altsNew
remaining := ( casesOnApp.remaining.mapM (loop F)) }.toExpr
return { matcherApp with alts := altsNew, discrs := ( matcherApp.discrs.mapM (loop F)) }.toExpr
else
processApp F e
| none => processApp F e

View File

@@ -5,7 +5,6 @@ Authors: Joachim Breitner
-/
import Lean.Util.HasConstCache
import Lean.Meta.CasesOn
import Lean.Meta.Match.Match
import Lean.Meta.Tactic.Cleanup
import Lean.Meta.Tactic.Refl
@@ -176,7 +175,7 @@ where
| Expr.proj _n _i e => loop param e
| Expr.const .. => if e.isConstOf recFnName then processRec param e
| Expr.app .. =>
match ( matchMatcherApp? e) with
match ( matchMatcherApp? (alsoCasesOn := true) e) with
| some matcherApp =>
if let some altParams matcherApp.refineThrough? param then
matcherApp.discrs.forM (loop param)
@@ -191,23 +190,6 @@ where
matcherApp.remaining.forM (loop param)
else
processApp param e
| none =>
match ( toCasesOnApp? e) with
| some casesOnApp =>
if let some altParams casesOnApp.refineThrough? param then
loop param casesOnApp.major
(Array.zip casesOnApp.alts (Array.zip casesOnApp.altNumParams altParams)).forM
fun (alt, altNumParam, altParam) =>
lambdaTelescope altParam fun xs altParam => do
-- TODO: Use boundedLambdaTelescope
unless altNumParam = xs.size do
throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}"
let altBody := alt.beta xs
loop altParam altBody
casesOnApp.remaining.forM (loop param)
else
trace[Elab.definition.wf] "withRecApps: casesOnApp.refineThrough? failed"
processApp param e
| none => processApp param e
| e => do
let _ ensureNoRecFn recFnName e

View File

@@ -293,8 +293,10 @@ mutual
Try to synthesize a term `val` using the tactic code `tacticCode`, and then assign `mvarId := val`.
The `tacticCode` syntax comprises the whole `by ...` expression.
If `report := false`, then `runTactic` will not capture exceptions nor will report unsolved goals. Unsolved goals become exceptions.
-/
partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := withoutAutoBoundImplicit do
partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
let code := tacticCode[1]
instantiateMVarDeclMVars mvarId
/-
@@ -320,9 +322,12 @@ mutual
evalTactic code
synthesizeSyntheticMVars (mayPostpone := false)
unless remainingGoals.isEmpty do
reportUnsolvedGoals remainingGoals
if report then
reportUnsolvedGoals remainingGoals
else
throwError "unsolved goals\n{goalsToMessageData remainingGoals}"
catch ex =>
if ( read).errToSorry then
if report && ( read).errToSorry then
for mvarId in ( getMVars (mkMVar mvarId)) do
mvarId.admit
logException ex

View File

@@ -28,3 +28,4 @@ import Lean.Elab.Tactic.RCases
import Lean.Elab.Tactic.Repeat
import Lean.Elab.Tactic.Ext
import Lean.Elab.Tactic.Change
import Lean.Elab.Tactic.FalseOrByContra

View File

@@ -0,0 +1,63 @@
/-
Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import Lean.Elab.Tactic.Basic
import Lean.Meta.Tactic.Apply
import Lean.Meta.Tactic.Intro
/-!
# `false_or_by_contra` tactic
Changes the goal to `False`, retaining as much information as possible:
* If the goal is `False`, do nothing.
* If the goal is an implication or a function type, introduce the argument and restart.
(In particular, if the goal is `x ≠ y`, introduce `x = y`.)
* Otherwise, for a propositional goal `P`, replace it with `¬ ¬ P`
(attempting to find a `Decidable` instance, but otherwise falling back to working classically)
and introduce `¬ P`.
* For a non-propositional goal use `False.elim`.
-/
namespace Lean.MVarId
open Lean Meta Elab Tactic
@[inherit_doc Lean.Parser.Tactic.falseOrByContra]
-- When `useClassical` is `none`, we try to find a `Decidable` instance when replacing `P` with `¬ ¬ P`,
-- but fall back to a classical instance. When it is `some true`, we always use the classical instance.
-- When it is `some false`, if there is no `Decidable` instance we don't introduce the double negation,
-- and fall back to `False.elim`.
partial def falseOrByContra (g : MVarId) (useClassical : Option Bool := none) : MetaM MVarId := do
let ty whnfR ( g.getType)
match ty with
| .const ``False _ => pure g
| .forallE _ _ _ _
| .app (.const ``Not _) _ => falseOrByContra ( g.intro1).2
| _ =>
let gs if isProp ty then
match useClassical with
| some true => some <$> g.applyConst ``Classical.byContradiction
| some false =>
try some <$> g.applyConst ``Decidable.byContradiction
catch _ => pure none
| none =>
try some <$> g.applyConst ``Decidable.byContradiction
catch _ => some <$> g.applyConst ``Classical.byContradiction
else
pure none
if let some gs := gs then
let [g] := gs | panic! "expected one subgoal"
pure ( g.intro1).2
else
let [g] g.applyConst ``False.elim | panic! "expected one sugoal"
pure g
@[builtin_tactic falseOrByContra]
def elabFalseOrByContra : Tactic
| `(tactic| false_or_by_contra) => do liftMetaTactic1 (falseOrByContra ·)
| _ => no_error_if_unused% throwUnsupportedSyntax
end Lean.MVarId

View File

@@ -43,9 +43,11 @@ def tacticToDischarge (tacticCode : Syntax) : TacticM (IO.Ref Term.State × Simp
let runTac? : TermElabM (Option Expr) :=
try
/- We must only save messages and info tree changes. Recall that `simp` uses temporary metavariables (`withNewMCtxDepth`).
So, we must not save references to them at `Term.State`. -/
So, we must not save references to them at `Term.State`.
-/
withoutModifyingStateWithInfoAndMessages do
Term.withSynthesize (mayPostpone := false) <| Term.runTactic mvar.mvarId! tacticCode
Term.withSynthesize (mayPostpone := false) do
Term.runTactic (report := false) mvar.mvarId! tacticCode
let result instantiateMVars mvar
if result.hasExprMVar then
return none

View File

@@ -884,182 +884,6 @@ def isLit : Expr → Bool
| lit .. => true
| _ => false
/--
Return the "body" of a forall expression.
Example: let `e` be the representation for `forall (p : Prop) (q : Prop), p ∧ q`, then
`getForallBody e` returns ``.app (.app (.const `And []) (.bvar 1)) (.bvar 0)``
-/
def getForallBody : Expr Expr
| forallE _ _ b .. => getForallBody b
| e => e
def getForallBodyMaxDepth : (maxDepth : Nat) Expr Expr
| (n+1), forallE _ _ b _ => getForallBodyMaxDepth n b
| 0, e => e
| _, e => e
/-- Given a sequence of nested foralls `(a₁ : α₁) → ... → (aₙ : αₙ) → _`,
returns the names `[a₁, ... aₙ]`. -/
def getForallBinderNames : Expr List Name
| forallE n _ b _ => n :: getForallBinderNames b
| _ => []
/--
If the given expression is a sequence of
function applications `f a₁ .. aₙ`, return `f`.
Otherwise return the input expression.
-/
def getAppFn : Expr Expr
| app f _ => getAppFn f
| e => e
private def getAppNumArgsAux : Expr Nat Nat
| app f _, n => getAppNumArgsAux f (n+1)
| _, n => n
/-- Counts the number `n` of arguments for an expression `f a₁ .. aₙ`. -/
def getAppNumArgs (e : Expr) : Nat :=
getAppNumArgsAux e 0
/--
Like `Lean.Expr.getAppFn` but assumes the application has up to `maxArgs` arguments.
If there are any more arguments than this, then they are returned by `getAppFn` as part of the function.
In particular, if the given expression is a sequence of function applications `f a₁ .. aₙ`,
returns `f a₁ .. aₖ` where `k` is minimal such that `n - k ≤ maxArgs`.
-/
def getBoundedAppFn : (maxArgs : Nat) Expr Expr
| maxArgs' + 1, .app f _ => getBoundedAppFn maxArgs' f
| _, e => e
private def getAppArgsAux : Expr Array Expr Nat Array Expr
| app f a, as, i => getAppArgsAux f (as.set! i a) (i-1)
| _, as, _ => as
/-- Given `f a₁ a₂ ... aₙ`, returns `#[a₁, ..., aₙ]` -/
@[inline] def getAppArgs (e : Expr) : Array Expr :=
let dummy := mkSort levelZero
let nargs := e.getAppNumArgs
getAppArgsAux e (mkArray nargs dummy) (nargs-1)
private def getBoundedAppArgsAux : Expr Array Expr Nat Array Expr
| app f a, as, i + 1 => getBoundedAppArgsAux f (as.set! i a) i
| _, as, _ => as
/--
Like `Lean.Expr.getAppArgs` but returns up to `maxArgs` arguments.
In particular, given `f a₁ a₂ ... aₙ`, returns `#[aₖ₊₁, ..., aₙ]`
where `k` is minimal such that the size of this array is at most `maxArgs`.
-/
@[inline] def getBoundedAppArgs (maxArgs : Nat) (e : Expr) : Array Expr :=
let dummy := mkSort levelZero
let nargs := min maxArgs e.getAppNumArgs
getBoundedAppArgsAux e (mkArray nargs dummy) nargs
private def getAppRevArgsAux : Expr Array Expr Array Expr
| app f a, as => getAppRevArgsAux f (as.push a)
| _, as => as
/-- Same as `getAppArgs` but reverse the output array. -/
@[inline] def getAppRevArgs (e : Expr) : Array Expr :=
getAppRevArgsAux e (Array.mkEmpty e.getAppNumArgs)
@[specialize] def withAppAux (k : Expr Array Expr α) : Expr Array Expr Nat α
| app f a, as, i => withAppAux k f (as.set! i a) (i-1)
| f, as, _ => k f as
/-- Given `e = f a₁ a₂ ... aₙ`, returns `k f #[a₁, ..., aₙ]`. -/
@[inline] def withApp (e : Expr) (k : Expr Array Expr α) : α :=
let dummy := mkSort levelZero
let nargs := e.getAppNumArgs
withAppAux k e (mkArray nargs dummy) (nargs-1)
/--
Given `f a_1 ... a_n`, returns `#[a_1, ..., a_n]`.
Note that `f` may be an application.
The resulting array has size `n` even if `f.getAppNumArgs < n`.
-/
@[inline] def getAppArgsN (e : Expr) (n : Nat) : Array Expr :=
let dummy := mkSort levelZero
loop n e (mkArray n dummy)
where
loop : Nat Expr Array Expr Array Expr
| 0, _, as => as
| i+1, .app f a, as => loop i f (as.set! i a)
| _, _, _ => panic! "too few arguments at"
/--
Given `e` of the form `f a_1 ... a_n`, return `f`.
If `n` is greater than the number of arguments, then return `e.getAppFn`.
-/
def stripArgsN (e : Expr) (n : Nat) : Expr :=
match n, e with
| 0, _ => e
| n+1, .app f _ => stripArgsN f n
| _, _ => e
/--
Given `e` of the form `f a_1 ... a_n ... a_m`, return `f a_1 ... a_n`.
If `n` is greater than the arity, then return `e`.
-/
def getAppPrefix (e : Expr) (n : Nat) : Expr :=
e.stripArgsN (e.getAppNumArgs - n)
/-- Given `e = fn a₁ ... aₙ`, runs `f` on `fn` and each of the arguments `aᵢ` and
makes a new function application with the results. -/
def traverseApp {M} [Monad M]
(f : Expr M Expr) (e : Expr) : M Expr :=
e.withApp fun fn args => mkAppN <$> f fn <*> args.mapM f
@[specialize] private def withAppRevAux (k : Expr Array Expr α) : Expr Array Expr α
| app f a, as => withAppRevAux k f (as.push a)
| f, as => k f as
/-- Same as `withApp` but with arguments reversed. -/
@[inline] def withAppRev (e : Expr) (k : Expr Array Expr α) : α :=
withAppRevAux k e (Array.mkEmpty e.getAppNumArgs)
def getRevArgD : Expr Nat Expr Expr
| app _ a, 0, _ => a
| app f _, i+1, v => getRevArgD f i v
| _, _, v => v
def getRevArg! : Expr Nat Expr
| app _ a, 0 => a
| app f _, i+1 => getRevArg! f i
| _, _ => panic! "invalid index"
/-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or panics if out of bounds. -/
@[inline] def getArg! (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr :=
getRevArg! e (n - i - 1)
/-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or returns `v₀` if out of bounds. -/
@[inline] def getArgD (e : Expr) (i : Nat) (v₀ : Expr) (n := e.getAppNumArgs) : Expr :=
getRevArgD e (n - i - 1) v₀
/-- Given `f a₀ a₁ ... aₙ`, returns true if `f` is a constant with name `n`. -/
def isAppOf (e : Expr) (n : Name) : Bool :=
match e.getAppFn with
| const c _ => c == n
| _ => false
/--
Given `f a₁ ... aᵢ`, returns true if `f` is a constant
with name `n` and has the correct number of arguments.
-/
def isAppOfArity : Expr Name Nat Bool
| const c _, n, 0 => c == n
| app f _, n, a+1 => isAppOfArity f n a
| _, _, _ => false
/-- Similar to `isAppOfArity` but skips `Expr.mdata`. -/
def isAppOfArity' : Expr Name Nat Bool
| mdata _ b , n, a => isAppOfArity' b n a
| const c _, n, 0 => c == n
| app f _, n, a+1 => isAppOfArity' f n a
| _, _, _ => false
def appFn! : Expr Expr
| app f _ => f
| _ => panic! "application expected"
@@ -1098,8 +922,9 @@ def isStringLit : Expr → Bool
| lit (Literal.strVal _) => true
| _ => false
def isCharLit (e : Expr) : Bool :=
e.isAppOfArity ``Char.ofNat 1 && e.appArg!.isNatLit
def isCharLit : Expr Bool
| app (const c _) a => c == ``Char.ofNat && a.isNatLit
| _ => false
def constName! : Expr Name
| const n _ => n
@@ -1109,6 +934,10 @@ def constName? : Expr → Option Name
| const n _ => some n
| _ => none
/-- If the expression is a constant, return that name. Otherwise return `Name.anonymous`. -/
def constName (e : Expr) : Name :=
e.constName?.getD Name.anonymous
def constLevels! : Expr List Level
| const _ ls => ls
| _ => panic! "constant expected"
@@ -1177,6 +1006,213 @@ def projIdx! : Expr → Nat
| proj _ i _ => i
| _ => panic! "proj expression expected"
/--
Return the "body" of a forall expression.
Example: let `e` be the representation for `forall (p : Prop) (q : Prop), p ∧ q`, then
`getForallBody e` returns ``.app (.app (.const `And []) (.bvar 1)) (.bvar 0)``
-/
def getForallBody : Expr Expr
| forallE _ _ b .. => getForallBody b
| e => e
def getForallBodyMaxDepth : (maxDepth : Nat) Expr Expr
| (n+1), forallE _ _ b _ => getForallBodyMaxDepth n b
| 0, e => e
| _, e => e
/-- Given a sequence of nested foralls `(a₁ : α₁) → ... → (aₙ : αₙ) → _`,
returns the names `[a₁, ... aₙ]`. -/
def getForallBinderNames : Expr List Name
| forallE n _ b _ => n :: getForallBinderNames b
| _ => []
/--
If the given expression is a sequence of
function applications `f a₁ .. aₙ`, return `f`.
Otherwise return the input expression.
-/
def getAppFn : Expr Expr
| app f _ => getAppFn f
| e => e
/-- Given `f a₀ a₁ ... aₙ`, returns true if `f` is a constant with name `n`. -/
def isAppOf (e : Expr) (n : Name) : Bool :=
match e.getAppFn with
| const c _ => c == n
| _ => false
/--
Given `f a₁ ... aᵢ`, returns true if `f` is a constant
with name `n` and has the correct number of arguments.
-/
def isAppOfArity : Expr Name Nat Bool
| const c _, n, 0 => c == n
| app f _, n, a+1 => isAppOfArity f n a
| _, _, _ => false
/-- Similar to `isAppOfArity` but skips `Expr.mdata`. -/
def isAppOfArity' : Expr Name Nat Bool
| mdata _ b , n, a => isAppOfArity' b n a
| const c _, n, 0 => c == n
| app f _, n, a+1 => isAppOfArity' f n a
| _, _, _ => false
/--
Checks if an expression is a "natural number numeral in normal form",
i.e. of type `Nat`, and explicitly of the form `OfNat.ofNat n`
where `n` matches `.lit (.natVal n)` for some literal natural number `n`.
and if so returns `n`.
-/
-- Note that `Expr.lit (.natVal n)` is not considered in normal form!
def nat? (e : Expr) : Option Nat := do
guard <| e.isAppOfArity ``OfNat.ofNat 3
let lit (.natVal n) := e.appFn!.appArg! | none
n
/--
Checks if an expression is an "integer numeral in normal form",
i.e. of type `Nat` or `Int`, and either a natural number numeral in normal form (as specified by `nat?`),
or the negation of a positive natural number numberal in normal form,
and if so returns the integer.
-/
def int? (e : Expr) : Option Int :=
if e.isAppOfArity ``Neg.neg 3 then
match e.appArg!.nat? with
| none => none
| some 0 => none
| some n => some (-n)
else
e.nat?
private def getAppNumArgsAux : Expr Nat Nat
| app f _, n => getAppNumArgsAux f (n+1)
| _, n => n
/-- Counts the number `n` of arguments for an expression `f a₁ .. aₙ`. -/
def getAppNumArgs (e : Expr) : Nat :=
getAppNumArgsAux e 0
/--
Like `Lean.Expr.getAppFn` but assumes the application has up to `maxArgs` arguments.
If there are any more arguments than this, then they are returned by `getAppFn` as part of the function.
In particular, if the given expression is a sequence of function applications `f a₁ .. aₙ`,
returns `f a₁ .. aₖ` where `k` is minimal such that `n - k ≤ maxArgs`.
-/
def getBoundedAppFn : (maxArgs : Nat) Expr Expr
| maxArgs' + 1, .app f _ => getBoundedAppFn maxArgs' f
| _, e => e
private def getAppArgsAux : Expr Array Expr Nat Array Expr
| app f a, as, i => getAppArgsAux f (as.set! i a) (i-1)
| _, as, _ => as
/-- Given `f a₁ a₂ ... aₙ`, returns `#[a₁, ..., aₙ]` -/
@[inline] def getAppArgs (e : Expr) : Array Expr :=
let dummy := mkSort levelZero
let nargs := e.getAppNumArgs
getAppArgsAux e (mkArray nargs dummy) (nargs-1)
private def getBoundedAppArgsAux : Expr Array Expr Nat Array Expr
| app f a, as, i + 1 => getBoundedAppArgsAux f (as.set! i a) i
| _, as, _ => as
/--
Like `Lean.Expr.getAppArgs` but returns up to `maxArgs` arguments.
In particular, given `f a₁ a₂ ... aₙ`, returns `#[aₖ₊₁, ..., aₙ]`
where `k` is minimal such that the size of this array is at most `maxArgs`.
-/
@[inline] def getBoundedAppArgs (maxArgs : Nat) (e : Expr) : Array Expr :=
let dummy := mkSort levelZero
let nargs := min maxArgs e.getAppNumArgs
getBoundedAppArgsAux e (mkArray nargs dummy) nargs
private def getAppRevArgsAux : Expr Array Expr Array Expr
| app f a, as => getAppRevArgsAux f (as.push a)
| _, as => as
/-- Same as `getAppArgs` but reverse the output array. -/
@[inline] def getAppRevArgs (e : Expr) : Array Expr :=
getAppRevArgsAux e (Array.mkEmpty e.getAppNumArgs)
@[specialize] def withAppAux (k : Expr Array Expr α) : Expr Array Expr Nat α
| app f a, as, i => withAppAux k f (as.set! i a) (i-1)
| f, as, _ => k f as
/-- Given `e = f a₁ a₂ ... aₙ`, returns `k f #[a₁, ..., aₙ]`. -/
@[inline] def withApp (e : Expr) (k : Expr Array Expr α) : α :=
let dummy := mkSort levelZero
let nargs := e.getAppNumArgs
withAppAux k e (mkArray nargs dummy) (nargs-1)
/-- Return the function (name) and arguments of an application. -/
def getAppFnArgs (e : Expr) : Name × Array Expr :=
withApp e λ e a => (e.constName, a)
/--
Given `f a_1 ... a_n`, returns `#[a_1, ..., a_n]`.
Note that `f` may be an application.
The resulting array has size `n` even if `f.getAppNumArgs < n`.
-/
@[inline] def getAppArgsN (e : Expr) (n : Nat) : Array Expr :=
let dummy := mkSort levelZero
loop n e (mkArray n dummy)
where
loop : Nat Expr Array Expr Array Expr
| 0, _, as => as
| i+1, .app f a, as => loop i f (as.set! i a)
| _, _, _ => panic! "too few arguments at"
/--
Given `e` of the form `f a_1 ... a_n`, return `f`.
If `n` is greater than the number of arguments, then return `e.getAppFn`.
-/
def stripArgsN (e : Expr) (n : Nat) : Expr :=
match n, e with
| 0, _ => e
| n+1, .app f _ => stripArgsN f n
| _, _ => e
/--
Given `e` of the form `f a_1 ... a_n ... a_m`, return `f a_1 ... a_n`.
If `n` is greater than the arity, then return `e`.
-/
def getAppPrefix (e : Expr) (n : Nat) : Expr :=
e.stripArgsN (e.getAppNumArgs - n)
/-- Given `e = fn a₁ ... aₙ`, runs `f` on `fn` and each of the arguments `aᵢ` and
makes a new function application with the results. -/
def traverseApp {M} [Monad M]
(f : Expr M Expr) (e : Expr) : M Expr :=
e.withApp fun fn args => mkAppN <$> f fn <*> args.mapM f
@[specialize] private def withAppRevAux (k : Expr Array Expr α) : Expr Array Expr α
| app f a, as => withAppRevAux k f (as.push a)
| f, as => k f as
/-- Same as `withApp` but with arguments reversed. -/
@[inline] def withAppRev (e : Expr) (k : Expr Array Expr α) : α :=
withAppRevAux k e (Array.mkEmpty e.getAppNumArgs)
def getRevArgD : Expr Nat Expr Expr
| app _ a, 0, _ => a
| app f _, i+1, v => getRevArgD f i v
| _, _, v => v
def getRevArg! : Expr Nat Expr
| app _ a, 0 => a
| app f _, i+1 => getRevArg! f i
| _, _ => panic! "invalid index"
/-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or panics if out of bounds. -/
@[inline] def getArg! (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr :=
getRevArg! e (n - i - 1)
/-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or returns `v₀` if out of bounds. -/
@[inline] def getArgD (e : Expr) (i : Nat) (v₀ : Expr) (n := e.getAppNumArgs) : Expr :=
getRevArgD e (n - i - 1) v₀
def hasLooseBVars (e : Expr) : Bool :=
e.looseBVarRange > 0
@@ -1559,6 +1595,12 @@ partial def cleanupAnnotations (e : Expr) : Expr :=
let e' := e.consumeMData.consumeTypeAnnotations
if e' == e then e else cleanupAnnotations e'
def isFalse (e : Expr) : Bool :=
e.cleanupAnnotations.isConstOf ``False
def isTrue (e : Expr) : Bool :=
e.cleanupAnnotations.isConstOf ``True
/-- Return true iff `e` contains a free variable which satisfies `p`. -/
@[inline] def hasAnyFVar (e : Expr) (p : FVarId Bool) : Bool :=
let rec @[specialize] visit (e : Expr) := if !e.hasFVar then false else

View File

@@ -64,8 +64,7 @@ inductive MessageData where
/-- Tagged sections. `Name` should be viewed as a "kind", and is used by `MessageData` inspector functions.
Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". -/
| tagged : Name MessageData MessageData
| trace (cls : Name) (msg : MessageData) (children : Array MessageData)
(collapsed : Bool := false)
| trace (cls : Name) (msg : MessageData) (children : Array MessageData) (collapsed : Bool)
deriving Inhabited
namespace MessageData

View File

@@ -39,7 +39,6 @@ import Lean.Meta.Structure
import Lean.Meta.Constructions
import Lean.Meta.CongrTheorems
import Lean.Meta.Eqns
import Lean.Meta.CasesOn
import Lean.Meta.ExprLens
import Lean.Meta.ExprTraverse
import Lean.Meta.Eval

View File

@@ -1084,19 +1084,21 @@ private def forallBoundedTelescopeImp (type : Expr) (maxFVars? : Option Nat) (k
def forallBoundedTelescope (type : Expr) (maxFVars? : Option Nat) (k : Array Expr Expr n α) : n α :=
map2MetaM (fun k => forallBoundedTelescopeImp type maxFVars? k) k
private partial def lambdaTelescopeImp (e : Expr) (consumeLet : Bool) (k : Array Expr Expr MetaM α) : MetaM α := do
private partial def lambdaTelescopeImp (e : Expr) (consumeLet : Bool) (k : Array Expr Expr MetaM α) (cleanupAnnotations := false) : MetaM α := do
process consumeLet ( getLCtx) #[] 0 e
where
process (consumeLet : Bool) (lctx : LocalContext) (fvars : Array Expr) (j : Nat) (e : Expr) : MetaM α := do
match consumeLet, e with
| _, .lam n d b bi =>
let d := d.instantiateRevRange j fvars.size fvars
let d := if cleanupAnnotations then d.cleanupAnnotations else d
let fvarId mkFreshFVarId
let lctx := lctx.mkLocalDecl fvarId n d bi
let fvar := mkFVar fvarId
process consumeLet lctx (fvars.push fvar) j b
| true, .letE n t v b _ => do
let t := t.instantiateRevRange j fvars.size fvars
let t := if cleanupAnnotations then t.cleanupAnnotations else t
let v := v.instantiateRevRange j fvars.size fvars
let fvarId mkFreshFVarId
let lctx := lctx.mkLetDecl fvarId n t v
@@ -1108,16 +1110,23 @@ where
withNewLocalInstancesImp fvars j do
k fvars e
/-- Similar to `lambdaTelescope` but for lambda and let expressions. -/
def lambdaLetTelescope (e : Expr) (k : Array Expr Expr n α) : n α :=
map2MetaM (fun k => lambdaTelescopeImp e true k) k
/--
Similar to `lambdaTelescope` but for lambda and let expressions.
If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
-/
def lambdaLetTelescope (e : Expr) (k : Array Expr Expr n α) (cleanupAnnotations := false) : n α :=
map2MetaM (fun k => lambdaTelescopeImp e true k (cleanupAnnotations := cleanupAnnotations)) k
/--
Given `e` of the form `fun ..xs => A`, execute `k xs A`.
This combinator will declare local declarations, create free variables for them,
execute `k` with updated local context, and make sure the cache is restored after executing `k`. -/
def lambdaTelescope (e : Expr) (k : Array Expr Expr n α) : n α :=
map2MetaM (fun k => lambdaTelescopeImp e false k) k
execute `k` with updated local context, and make sure the cache is restored after executing `k`.
If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
-/
def lambdaTelescope (e : Expr) (k : Array Expr Expr n α) (cleanupAnnotations := false) : n α :=
map2MetaM (fun k => lambdaTelescopeImp e false k (cleanupAnnotations := cleanupAnnotations)) k
/-- Return the parameter names for the given global declaration. -/
def getParamNames (declName : Name) : MetaM (Array Name) := do

View File

@@ -1,178 +0,0 @@
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.KAbstract
import Lean.Meta.Check
import Lean.Meta.AppBuilder
namespace Lean.Meta
structure CasesOnApp where
declName : Name
us : List Level
params : Array Expr
motive : Expr
indices : Array Expr
major : Expr
alts : Array Expr
altNumParams : Array Nat
remaining : Array Expr
/-- `true` if the `casesOn` can only eliminate into `Prop` -/
propOnly : Bool
/-- Return `some c` if `e` is a `casesOn` application. -/
def toCasesOnApp? (e : Expr) : MetaM (Option CasesOnApp) := do
let f := e.getAppFn
let .const declName us := f | return none
unless isCasesOnRecursor ( getEnv) declName do return none
let indName := declName.getPrefix
let .inductInfo info getConstInfo indName | return none
let args := e.getAppArgs
unless args.size >= info.numParams + 1 /- motive -/ + info.numIndices + 1 /- major -/ + info.numCtors do return none
let params := args[:info.numParams]
let motive := args[info.numParams]!
let indices := args[info.numParams + 1 : info.numParams + 1 + info.numIndices]
let major := args[info.numParams + 1 + info.numIndices]!
let alts := args[info.numParams + 1 + info.numIndices + 1 : info.numParams + 1 + info.numIndices + 1 + info.numCtors]
let remaining := args[info.numParams + 1 + info.numIndices + 1 + info.numCtors :]
let propOnly := info.levelParams.length == us.length
let mut altNumParams := #[]
for ctor in info.ctors do
let .ctorInfo ctorInfo getConstInfo ctor | unreachable!
altNumParams := altNumParams.push ctorInfo.numFields
return some { declName, us, params, motive, indices, major, alts, remaining, propOnly, altNumParams }
/-- Convert `c` back to `Expr` -/
def CasesOnApp.toExpr (c : CasesOnApp) : Expr :=
mkAppN (mkAppN (mkApp (mkAppN (mkApp (mkAppN (mkConst c.declName c.us) c.params) c.motive) c.indices) c.major) c.alts) c.remaining
/--
Given a `casesOn` application `c` of the form
```
casesOn As (fun is x => motive[is, xs]) is major (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining
```
and an expression `e : B[is, major]`, construct the term
```
casesOn As (fun is x => B[is, x] → motive[i, xs]) is major (fun ys_1 (y : B[_, C_1[ys_1]]) => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n (y : B[_, C_n[ys_n]]) => (alt_n : motive (C_n[ys_n]) e remaining
```
We use `kabstract` to abstract the `is` and `major` from `B[is, major]`.
This is used in in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to
the argument provided by `fix` to refine the termination argument, which may mention `major`.
See there for how to use this function.
-/
def CasesOnApp.addArg (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := false) : MetaM CasesOnApp := do
lambdaTelescope c.motive fun motiveArgs motiveBody => do
unless motiveArgs.size == c.indices.size + 1 do
throwError "failed to add argument to `casesOn` application, motive must be lambda expression with #{c.indices.size + 1} binders"
let argType inferType arg
let discrs := c.indices ++ #[c.major]
let mut argTypeAbst := argType
for motiveArg in motiveArgs.reverse, discr in discrs.reverse do
argTypeAbst := ( kabstract argTypeAbst discr).instantiate1 motiveArg
let motiveBody mkArrow argTypeAbst motiveBody
let us if c.propOnly then pure c.us else pure (( getLevel motiveBody) :: c.us.tail!)
let motive mkLambdaFVars motiveArgs motiveBody
let remaining := #[arg] ++ c.remaining
let aux := mkAppN (mkConst c.declName us) c.params
let aux := mkApp aux motive
let aux := mkAppN aux discrs
check aux
unless ( isTypeCorrect aux) do
throwError "failed to add argument to `casesOn` application, type error when constructing the new motive{indentExpr aux}"
let auxType inferType aux
let alts updateAlts argType auxType
return { c with us, motive, alts, remaining }
where
updateAlts (argType : Expr) (auxType : Expr) : MetaM (Array Expr) := do
let mut auxType := auxType
let mut altsNew := #[]
let mut refined := false
for alt in c.alts, numParams in c.altNumParams do
auxType whnfD auxType
match auxType with
| .forallE _ d b _ =>
let (altNew, refinedAt) forallBoundedTelescope d (some numParams) fun xs d => do
forallBoundedTelescope d (some 1) fun x _ => do
let alt := alt.beta xs
let alt mkLambdaFVars x alt -- x is the new argument we are adding to the alternative
if checkIfRefined then
return ( mkLambdaFVars xs alt, !( isDefEq argType ( inferType x[0]!)))
else
return ( mkLambdaFVars xs alt, true)
if refinedAt then
refined := true
auxType := b.instantiate1 altNew
altsNew := altsNew.push altNew
| _ => throwError "unexpected type at `casesOnAddArg`"
unless refined do
throwError "failed to add argument to `casesOn` application, argument type was not refined by `casesOn`"
return altsNew
/-- Similar to `CasesOnApp.addArg`, but returns `none` on failure. -/
def CasesOnApp.addArg? (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := false) : MetaM (Option CasesOnApp) :=
try
return some ( c.addArg arg checkIfRefined)
catch _ =>
return none
/--
Given a `casesOn` application `c` of the form
```
casesOn As (fun is x => motive[is, xs]) is major (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining
```
and an expression `B[is, major]` (which may not be a type, e.g. `n : Nat`)
for every alternative `i`, construct the expression `fun ys_i => B[_, C_i[ys_i]]`
This is similar to `CasesOnApp.addArg` when you only have an expression to
refined, and not a type with a value.
This is used in in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive
calls to refine the functions' paramter, which may mention `major`.
See there for how to use this function.
-/
def CasesOnApp.refineThrough (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) :=
lambdaTelescope c.motive fun motiveArgs _motiveBody => do
unless motiveArgs.size == c.indices.size + 1 do
throwError "failed to transfer argument through `casesOn` application, motive must be lambda expression with #{c.indices.size + 1} binders"
let discrs := c.indices ++ #[c.major]
let mut eAbst := e
for motiveArg in motiveArgs.reverse, discr in discrs.reverse do
eAbst kabstract eAbst discr
eAbst := eAbst.instantiate1 motiveArg
-- Let's create something thats a `Sort` and mentions `e`
-- (recall that `e` itself possibly isn't a type),
-- by writing `e = e`, so that we can use it as a motive
let eEq mkEq eAbst eAbst
let motive mkLambdaFVars motiveArgs eEq
let us := if c.propOnly then c.us else levelZero :: c.us.tail!
-- Now instantiate the casesOn wth this synthetic motive
let aux := mkAppN (mkConst c.declName us) c.params
let aux := mkApp aux motive
let aux := mkAppN aux discrs
check aux
let auxType inferType aux
-- The type of the remaining arguments will mention `e` instantiated for each arg
-- so extract them
forallTelescope auxType fun altAuxs _ => do
let altAuxTys altAuxs.mapM (inferType ·)
(Array.zip c.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do
forallBoundedTelescope altAuxTy altNumParams fun fvs body => do
unless fvs.size = altNumParams do
throwError "failed to transfer argument through `casesOn` application, alt type must be telescope with #{altNumParams} arguments"
-- extract type from our synthetic equality
let body := body.getArg! 2
-- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out
mkLambdaFVars fvs body
/-- A non-failing version of `CasesOnApp.refineThrough` -/
def CasesOnApp.refineThrough? (c : CasesOnApp) (e : Expr) :
MetaM (Option (Array Expr)) :=
try
return some ( c.refineThrough e)
catch _ =>
return none
end Lean.Meta

View File

@@ -62,7 +62,7 @@ builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
-/
private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
if let some (.defnInfo info) := ( getEnv).find? declName then
lambdaTelescope info.value fun xs body => do
lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs
let type mkForallFVars xs ( mkEq lhs body)
let value mkLambdaFVars xs ( mkEqRefl lhs)

View File

@@ -889,22 +889,27 @@ def withMkMatcherInput (matcherName : Name) (k : MkMatcherInput → MetaM α) :
end Match
/-- Auxiliary function for MatcherApp.addArg -/
private partial def updateAlts (typeNew : Expr) (altNumParams : Array Nat) (alts : Array Expr) (i : Nat) : MetaM (Array Nat × Array Expr) := do
private partial def updateAlts (unrefinedArgType : Expr) (typeNew : Expr) (altNumParams : Array Nat) (alts : Array Expr) (refined : Bool) (i : Nat) : MetaM (Array Nat × Array Expr) := do
if h : i < alts.size then
let alt := alts.get i, h
let numParams := altNumParams[i]!
let typeNew whnfD typeNew
match typeNew with
| Expr.forallE _ d b _ =>
let alt forallBoundedTelescope d (some numParams) fun xs d => do
let (alt, refined) forallBoundedTelescope d (some numParams) fun xs d => do
let alt try instantiateLambda alt xs catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative"
forallBoundedTelescope d (some 1) fun x _ => do
let alt mkLambdaFVars x alt -- x is the new argument we are adding to the alternative
mkLambdaFVars xs alt
updateAlts (b.instantiate1 alt) (altNumParams.set! i (numParams+1)) (alts.set i, h alt) (i+1)
let refined := if refined then refined else
!( isDefEq unrefinedArgType ( inferType x[0]!))
return ( mkLambdaFVars xs alt, refined)
updateAlts unrefinedArgType (b.instantiate1 alt) (altNumParams.set! i (numParams+1)) (alts.set i, h alt) refined (i+1)
| _ => throwError "unexpected type at MatcherApp.addArg"
else
return (altNumParams, alts)
if refined then
return (altNumParams, alts)
else
throwError "failed to add argument to matcher application, argument type was not refined by `casesOn`"
/-- Given
- matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and
@@ -948,7 +953,7 @@ def MatcherApp.addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp :=
unless ( isTypeCorrect aux) do
throwError "failed to add argument to matcher application, type error when constructing the new motive"
let auxType inferType aux
let (altNumParams, alts) updateAlts auxType matcherApp.altNumParams matcherApp.alts 0
let (altNumParams, alts) updateAlts eType auxType matcherApp.altNumParams matcherApp.alts false 0
return { matcherApp with
matcherLevels := matcherLevels,
motive := motive,

View File

@@ -131,6 +131,7 @@ structure MatcherApp where
matcherName : Name
matcherLevels : Array Level
uElimPos? : Option Nat
discrInfos : Array Match.DiscrInfo
params : Array Expr
motive : Expr
discrs : Array Expr
@@ -138,28 +139,55 @@ structure MatcherApp where
alts : Array Expr
remaining : Array Expr
def matchMatcherApp? [Monad m] [MonadEnv m] (e : Expr) : m (Option MatcherApp) := do
match e.getAppFn with
| Expr.const declName declLevels =>
match ( getMatcherInfo? declName) with
| none => return none
| some info =>
/--
Recognizes if `e` is a matcher application, and destructs it into the `MatcherApp` data structure.
This can optionally also treat `casesOn` recursor applications as a special case
of matcher applications.
-/
def matchMatcherApp? [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (alsoCasesOn := false) :
m (Option MatcherApp) := do
if let .const declName declLevels := e.getAppFn then
if let some info getMatcherInfo? declName then
let args := e.getAppArgs
if args.size < info.arity then
return none
else
return some {
matcherName := declName
matcherLevels := declLevels.toArray
uElimPos? := info.uElimPos?
params := args.extract 0 info.numParams
motive := args[info.getMotivePos]!
discrs := args[info.numParams + 1 : info.numParams + 1 + info.numDiscrs]
altNumParams := info.altNumParams
alts := args[info.numParams + 1 + info.numDiscrs : info.numParams + 1 + info.numDiscrs + info.numAlts]
remaining := args[info.numParams + 1 + info.numDiscrs + info.numAlts : args.size]
}
| _ => return none
return some {
matcherName := declName
matcherLevels := declLevels.toArray
uElimPos? := info.uElimPos?
discrInfos := info.discrInfos
params := args.extract 0 info.numParams
motive := args[info.getMotivePos]!
discrs := args[info.numParams + 1 : info.numParams + 1 + info.numDiscrs]
altNumParams := info.altNumParams
alts := args[info.numParams + 1 + info.numDiscrs : info.numParams + 1 + info.numDiscrs + info.numAlts]
remaining := args[info.numParams + 1 + info.numDiscrs + info.numAlts : args.size]
}
if alsoCasesOn && isCasesOnRecursor ( getEnv) declName then
let indName := declName.getPrefix
let .inductInfo info getConstInfo indName | return none
let args := e.getAppArgs
unless args.size >= info.numParams + 1 /- motive -/ + info.numIndices + 1 /- major -/ + info.numCtors do return none
let params := args[:info.numParams]
let motive := args[info.numParams]!
let discrs := args[info.numParams + 1 : info.numParams + 1 + info.numIndices + 1]
let discrInfos := Array.mkArray (info.numIndices + 1) {}
let alts := args[info.numParams + 1 + info.numIndices + 1 : info.numParams + 1 + info.numIndices + 1 + info.numCtors]
let remaining := args[info.numParams + 1 + info.numIndices + 1 + info.numCtors :]
let uElimPos? := if info.levelParams.length == declLevels.length then none else some 0
let mut altNumParams := #[]
for ctor in info.ctors do
let .ctorInfo ctorInfo getConstInfo ctor | unreachable!
altNumParams := altNumParams.push ctorInfo.numFields
return some {
matcherName := declName
matcherLevels := declLevels.toArray
uElimPos?, discrInfos, params, motive, discrs, alts, remaining, altNumParams
}
return none
def MatcherApp.toExpr (matcherApp : MatcherApp) : Expr :=
let result := mkAppN (mkConst matcherApp.matcherName matcherApp.matcherLevels.toList) matcherApp.params

View File

@@ -40,7 +40,7 @@ def matchEqHEq? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) := do
return none
def matchFalse (e : Expr) : MetaM Bool := do
testHelper e fun e => return e.isConstOf ``False
testHelper e fun e => return e.isFalse
def matchNot? (e : Expr) : MetaM (Option Expr) :=
matchHelper? e fun e => do

View File

@@ -188,6 +188,10 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
def apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List MVarId) :=
mvarId.apply e cfg
/-- Short-hand for applying a constant to the goal. -/
def _root_.Lean.MVarId.applyConst (mvar : MVarId) (c : Name) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
mvar.apply ( mkConstWithFreshMVarLevels c) cfg
partial def splitAndCore (mvarId : MVarId) : MetaM (List MVarId) :=
mvarId.withContext do
mvarId.checkNotAssigned `splitAnd

View File

@@ -8,3 +8,5 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
import Lean.Meta.Tactic.Simp.BuiltinSimprocs.String

View File

@@ -0,0 +1,71 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.ToExpr
import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
namespace Char
open Lean Meta Simp
def fromExpr? (e : Expr) : SimpM (Option Char) := OptionT.run do
guard (e.isAppOfArity ``Char.ofNat 1)
let value Nat.fromExpr? e.appArg!
return Char.ofNat value
@[inline] def reduceUnary [ToExpr α] (declName : Name) (op : Char α) (arity : Nat := 1) (e : Expr) : SimpM Step := do
unless e.isAppOfArity declName arity do return .continue
let some c fromExpr? e.appArg! | return .continue
return .done { expr := toExpr (op c) }
@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Char Char Bool) (e : Expr) : SimpM Step := do
unless e.isAppOfArity declName arity do return .continue
let some n fromExpr? e.appFn!.appArg! | return .continue
let some m fromExpr? e.appArg! | return .continue
evalPropStep e (op n m)
@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Char Char Bool) (e : Expr) : SimpM Step := do
unless e.isAppOfArity declName arity do return .continue
let some n fromExpr? e.appFn!.appArg! | return .continue
let some m fromExpr? e.appArg! | return .continue
return .done { expr := toExpr (op n m) }
builtin_simproc [simp, seval] reduceToLower (Char.toLower _) := reduceUnary ``Char.toLower Char.toLower
builtin_simproc [simp, seval] reduceToUpper (Char.toUpper _) := reduceUnary ``Char.toUpper Char.toUpper
builtin_simproc [simp, seval] reduceToNat (Char.toNat _) := reduceUnary ``Char.toNat Char.toNat
builtin_simproc [simp, seval] reduceIsWhitespace (Char.isWhitespace _) := reduceUnary ``Char.isWhitespace Char.isWhitespace
builtin_simproc [simp, seval] reduceIsUpper (Char.isUpper _) := reduceUnary ``Char.isUpper Char.isUpper
builtin_simproc [simp, seval] reduceIsLower (Char.isLower _) := reduceUnary ``Char.isLower Char.isLower
builtin_simproc [simp, seval] reduceIsAlpha (Char.isAlpha _) := reduceUnary ``Char.isAlpha Char.isAlpha
builtin_simproc [simp, seval] reduceIsDigit (Char.isDigit _) := reduceUnary ``Char.isDigit Char.isDigit
builtin_simproc [simp, seval] reduceIsAlphaNum (Char.isAlphanum _) := reduceUnary ``Char.isAlphanum Char.isAlphanum
builtin_simproc [simp, seval] reduceToString (toString (_ : Char)) := reduceUnary ``toString toString 3
builtin_simproc [simp, seval] reduceVal (Char.val _) := fun e => do
unless e.isAppOfArity ``Char.val 1 do return .continue
let some c fromExpr? e.appArg! | return .continue
return .done { expr := UInt32.toExprCore c.val }
builtin_simproc [simp, seval] reduceEq (( _ : Char) = _) := reduceBinPred ``Eq 3 (. = .)
builtin_simproc [simp, seval] reduceNe (( _ : Char) _) := reduceBinPred ``Ne 3 (. .)
builtin_simproc [simp, seval] reduceBEq (( _ : Char) == _) := reduceBoolPred ``BEq.beq 4 (. == .)
builtin_simproc [simp, seval] reduceBNe (( _ : Char) != _) := reduceBoolPred ``bne 4 (. != .)
/--
Return `.done` for Char values. We don't want to unfold in the symbolic evaluator.
In regular `simp`, we want to prevent the nested raw literal from being converted into
a `OfNat.ofNat` application. TODO: cleanup
-/
builtin_simproc [simp, seval] isValue (Char.ofNat _ ) := fun e => do
unless ( fromExpr? e).isSome do return .continue
return .done { expr := e }
builtin_simproc [simp, seval] reduceOfNatAux (Char.ofNatAux _ _) := fun e => do
unless e.isAppOfArity ``Char.ofNatAux 2 do return .continue
let some n Nat.fromExpr? e.appFn!.appArg! | return .continue
return .done { expr := toExpr (Char.ofNat n) }
builtin_simproc [simp, seval] reduceDefault ((default : Char)) := fun e => do
unless e.isAppOfArity ``default 2 do return .continue
return .done { expr := toExpr (default : Char) }
end Char

View File

@@ -11,11 +11,11 @@ builtin_simproc ↓ [simp, seval] reduceIte (ite _ _ _) := fun e => do
unless e.isAppOfArity ``ite 5 do return .continue
let c := e.getArg! 1
let r simp c
if r.expr.isConstOf ``True then
if r.expr.isTrue then
let eNew := e.getArg! 3
let pr := mkApp (mkAppN (mkConst ``ite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) ( r.getProof)
return .visit { expr := eNew, proof? := pr }
if r.expr.isConstOf ``False then
if r.expr.isFalse then
let eNew := e.getArg! 4
let pr := mkApp (mkAppN (mkConst ``ite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) ( r.getProof)
return .visit { expr := eNew, proof? := pr }
@@ -25,13 +25,13 @@ builtin_simproc ↓ [simp, seval] reduceDite (dite _ _ _) := fun e => do
unless e.isAppOfArity ``dite 5 do return .continue
let c := e.getArg! 1
let r simp c
if r.expr.isConstOf ``True then
if r.expr.isTrue then
let pr r.getProof
let h := mkApp2 (mkConst ``of_eq_true) c pr
let eNew := mkApp (e.getArg! 3) h |>.headBeta
let prNew := mkApp (mkAppN (mkConst ``dite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) pr
return .visit { expr := eNew, proof? := prNew }
if r.expr.isConstOf ``False then
if r.expr.isFalse then
let pr r.getProof
let h := mkApp2 (mkConst ``of_eq_false) c pr
let eNew := mkApp (e.getArg! 4) h |>.headBeta

View File

@@ -42,6 +42,12 @@ def Value.toExpr (v : Value) : Expr :=
let some v₂ fromExpr? e.appArg! | return .continue
evalPropStep e (op v₁.value v₂.value)
@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Nat Nat Bool) (e : Expr) : SimpM Step := do
unless e.isAppOfArity declName arity do return .continue
let some v₁ fromExpr? e.appFn!.appArg! | return .continue
let some v₂ fromExpr? e.appArg! | return .continue
return .done { expr := Lean.toExpr (op v₁.value v₂.value) }
/-
The following code assumes users did not override the `Fin n` instances for the arithmetic operators.
If they do, they must disable the following `simprocs`.
@@ -57,6 +63,10 @@ builtin_simproc [simp, seval] reduceLT (( _ : Fin _) < _) := reduceBinPred ``L
builtin_simproc [simp, seval] reduceLE (( _ : Fin _) _) := reduceBinPred ``LE.le 4 (. .)
builtin_simproc [simp, seval] reduceGT (( _ : Fin _) > _) := reduceBinPred ``GT.gt 4 (. > .)
builtin_simproc [simp, seval] reduceGE (( _ : Fin _) _) := reduceBinPred ``GE.ge 4 (. .)
builtin_simproc [simp, seval] reduceEq (( _ : Fin _) = _) := reduceBinPred ``Eq 3 (. = .)
builtin_simproc [simp, seval] reduceNe (( _ : Fin _) _) := reduceBinPred ``Ne 3 (. .)
builtin_simproc [simp, seval] reduceBEq (( _ : Fin _) == _) := reduceBoolPred ``BEq.beq 4 (. == .)
builtin_simproc [simp, seval] reduceBNe (( _ : Fin _) != _) := reduceBoolPred ``bne 4 (. != .)
/-- Return `.done` for Fin values. We don't want to unfold in the symbolic evaluator. -/
builtin_simproc [seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do

View File

@@ -49,6 +49,12 @@ def toExpr (v : Int) : Expr :=
let some v₂ fromExpr? e.appArg! | return .continue
evalPropStep e (op v₁ v₂)
@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Int Int Bool) (e : Expr) : SimpM Step := do
unless e.isAppOfArity declName arity do return .continue
let some n fromExpr? e.appFn!.appArg! | return .continue
let some m fromExpr? e.appArg! | return .continue
return .done { expr := Lean.toExpr (op n m) }
/-
The following code assumes users did not override the `Int` instances for the arithmetic operators.
If they do, they must disable the following `simprocs`.
@@ -93,5 +99,9 @@ builtin_simproc [simp, seval] reduceLT (( _ : Int) < _) := reduceBinPred ``LT.
builtin_simproc [simp, seval] reduceLE (( _ : Int) _) := reduceBinPred ``LE.le 4 (. .)
builtin_simproc [simp, seval] reduceGT (( _ : Int) > _) := reduceBinPred ``GT.gt 4 (. > .)
builtin_simproc [simp, seval] reduceGE (( _ : Int) _) := reduceBinPred ``GE.ge 4 (. .)
builtin_simproc [simp, seval] reduceEq (( _ : Int) = _) := reduceBinPred ``Eq 3 (. = .)
builtin_simproc [simp, seval] reduceNe (( _ : Int) _) := reduceBinPred ``Ne 3 (. .)
builtin_simproc [simp, seval] reduceBEq (( _ : Int) == _) := reduceBoolPred ``BEq.beq 4 (. == .)
builtin_simproc [simp, seval] reduceBNe (( _ : Int) != _) := reduceBoolPred ``bne 4 (. != .)
end Int

View File

@@ -31,6 +31,12 @@ def fromExpr? (e : Expr) : SimpM (Option Nat) := do
let some m fromExpr? e.appArg! | return .continue
evalPropStep e (op n m)
@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Nat Nat Bool) (e : Expr) : SimpM Step := do
unless e.isAppOfArity declName arity do return .continue
let some n fromExpr? e.appFn!.appArg! | return .continue
let some m fromExpr? e.appArg! | return .continue
return .done { expr := toExpr (op n m) }
builtin_simproc [simp, seval] reduceSucc (Nat.succ _) := reduceUnary ``Nat.succ 1 (· + 1)
/-
@@ -50,6 +56,10 @@ builtin_simproc [simp, seval] reduceLT (( _ : Nat) < _) := reduceBinPred ``LT.
builtin_simproc [simp, seval] reduceLE (( _ : Nat) _) := reduceBinPred ``LE.le 4 (. .)
builtin_simproc [simp, seval] reduceGT (( _ : Nat) > _) := reduceBinPred ``GT.gt 4 (. > .)
builtin_simproc [simp, seval] reduceGE (( _ : Nat) _) := reduceBinPred ``GE.ge 4 (. .)
builtin_simproc [simp, seval] reduceEq (( _ : Nat) = _) := reduceBinPred ``Eq 3 (. = .)
builtin_simproc [simp, seval] reduceNe (( _ : Nat) _) := reduceBinPred ``Ne 3 (. .)
builtin_simproc [simp, seval] reduceBEq (( _ : Nat) == _) := reduceBoolPred ``BEq.beq 4 (. == .)
builtin_simproc [simp, seval] reduceBNe (( _ : Nat) != _) := reduceBoolPred ``bne 4 (. != .)
/-- Return `.done` for Nat values. We don't want to unfold in the symbolic evaluator. -/
builtin_simproc [seval] isValue ((OfNat.ofNat _ : Nat)) := fun e => do

View File

@@ -0,0 +1,36 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.ToExpr
import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
namespace String
open Lean Meta Simp
def fromExpr? (e : Expr) : SimpM (Option String) := OptionT.run do
let .lit (.strVal s) := e | failure
return s
builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : String)) := fun e => do
unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue
let some a fromExpr? e.appFn!.appArg! | return .continue
let some b fromExpr? e.appArg! | return .continue
return .done { expr := toExpr (a ++ b) }
private partial def reduceListChar (e : Expr) (s : String) : SimpM Step := do
trace[Meta.debug] "reduceListChar {e}, {s}"
if e.isAppOfArity ``List.nil 1 then
return .done { expr := toExpr s }
else if e.isAppOfArity ``List.cons 3 then
let some c Char.fromExpr? e.appFn!.appArg! | return .continue
reduceListChar e.appArg! (s.push c)
else
return .continue
builtin_simproc [simp, seval] reduceMk (String.mk _) := fun e => do
unless e.isAppOfArity ``String.mk 1 do return .continue
reduceListChar e.appArg! ""
end String

View File

@@ -9,7 +9,10 @@ open Lean Meta Simp
macro "declare_uint_simprocs" typeName:ident : command =>
let ofNat := typeName.getId ++ `ofNat
let ofNatCore := mkIdent (typeName.getId ++ `ofNatCore)
let toNat := mkIdent (typeName.getId ++ `toNat)
let fromExpr := mkIdent `fromExpr
let toExprCore := mkIdent `toExprCore
let toExpr := mkIdent `toExpr
`(
namespace $typeName
@@ -26,6 +29,10 @@ def $fromExpr (e : Expr) : OptionT SimpM Value := do
let value := $(mkIdent ofNat) value
return { value, ofNatFn := e.appFn!.appFn! }
def $toExprCore (v : $typeName) : Expr :=
let vExpr := mkRawNatLit v.val
mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst $(quote typeName.getId)) vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
def $toExpr (v : Value) : Expr :=
let vExpr := mkRawNatLit v.value.val
mkApp2 v.ofNatFn vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
@@ -43,6 +50,12 @@ def $toExpr (v : Value) : Expr :=
let some m ($fromExpr e.appArg!) | return .continue
evalPropStep e (op n.value m.value)
@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : $typeName $typeName Bool) (e : Expr) : SimpM Step := do
unless e.isAppOfArity declName arity do return .continue
let some n ($fromExpr e.appFn!.appArg!) | return .continue
let some m ($fromExpr e.appArg!) | return .continue
return .done { expr := Lean.toExpr (op n.value m.value) }
builtin_simproc [simp, seval] $(mkIdent `reduceAdd):ident ((_ + _ : $typeName)) := reduceBin ``HAdd.hAdd 6 (· + ·)
builtin_simproc [simp, seval] $(mkIdent `reduceMul):ident ((_ * _ : $typeName)) := reduceBin ``HMul.hMul 6 (· * ·)
builtin_simproc [simp, seval] $(mkIdent `reduceSub):ident ((_ - _ : $typeName)) := reduceBin ``HSub.hSub 6 (· - ·)
@@ -53,6 +66,23 @@ builtin_simproc [simp, seval] $(mkIdent `reduceLT):ident (( _ : $typeName) < _)
builtin_simproc [simp, seval] $(mkIdent `reduceLE):ident (( _ : $typeName) _) := reduceBinPred ``LE.le 4 (. .)
builtin_simproc [simp, seval] $(mkIdent `reduceGT):ident (( _ : $typeName) > _) := reduceBinPred ``GT.gt 4 (. > .)
builtin_simproc [simp, seval] $(mkIdent `reduceGE):ident (( _ : $typeName) _) := reduceBinPred ``GE.ge 4 (. .)
builtin_simproc [simp, seval] reduceEq (( _ : $typeName) = _) := reduceBinPred ``Eq 3 (. = .)
builtin_simproc [simp, seval] reduceNe (( _ : $typeName) _) := reduceBinPred ``Ne 3 (. .)
builtin_simproc [simp, seval] reduceBEq (( _ : $typeName) == _) := reduceBoolPred ``BEq.beq 4 (. == .)
builtin_simproc [simp, seval] reduceBNe (( _ : $typeName) != _) := reduceBoolPred ``bne 4 (. != .)
builtin_simproc [simp, seval] $(mkIdent `reduceOfNatCore):ident ($ofNatCore _ _) := fun e => do
unless e.isAppOfArity $(quote ofNatCore.getId) 2 do return .continue
let some value Nat.fromExpr? e.appFn!.appArg! | return .continue
let value := $(mkIdent ofNat) value
let eNew := $toExprCore value
return .done { expr := eNew }
builtin_simproc [simp, seval] $(mkIdent `reduceToNat):ident ($toNat _) := fun e => do
unless e.isAppOfArity $(quote toNat.getId) 1 do return .continue
let some v ($fromExpr e.appArg!) | return .continue
let n := $toNat v.value
return .done { expr := mkNatLit n }
/-- Return `.done` for UInt values. We don't want to unfold in the symbolic evaluator. -/
builtin_simproc [seval] isValue ((OfNat.ofNat _ : $typeName)) := fun e => do

View File

@@ -650,7 +650,7 @@ def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsAr
(mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
let target instantiateMVars ( mvarId.getType)
let (r, usedSimps) simp target ctx simprocs discharge? usedSimps
if mayCloseGoal && r.expr.consumeMData.isConstOf ``True then
if mayCloseGoal && r.expr.isTrue then
match r.proof? with
| some proof => mvarId.assign ( mkOfEqTrue proof)
| none => mvarId.assign (mkConst ``True.intro)
@@ -673,7 +673,7 @@ def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray
This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
def applySimpResultToProp (mvarId : MVarId) (proof : Expr) (prop : Expr) (r : Simp.Result) (mayCloseGoal := true) : MetaM (Option (Expr × Expr)) := do
if mayCloseGoal && r.expr.consumeMData.isConstOf ``False then
if mayCloseGoal && r.expr.isFalse then
match r.proof? with
| some eqProof => mvarId.assign ( mkFalseElim ( mvarId.getType) ( mkEqMP eqProof proof))
| none => mvarId.assign ( mkFalseElim ( mvarId.getType) proof)
@@ -721,7 +721,7 @@ def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Res
if r.proof?.isNone then
-- New result is definitionally equal to input. Thus, we can avoid creating a new variable if there are dependencies
let mvarId mvarId.replaceLocalDeclDefEq fvarId r.expr
if mayCloseGoal && r.expr.consumeMData.isConstOf ``False then
if mayCloseGoal && r.expr.isFalse then
mvarId.assign ( mkFalseElim ( mvarId.getType) (mkFVar fvarId))
return none
else
@@ -757,7 +757,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray :=
| none => return (none, usedSimps)
| some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
| none =>
if r.expr.consumeMData.isConstOf ``False then
if r.expr.isFalse then
mvarIdNew.assign ( mkFalseElim ( mvarIdNew.getType) (mkFVar fvarId))
return (none, usedSimps)
-- TODO: if there are no forwards dependencies we may consider using the same approach we used when `r.proof?` is a `some ...`
@@ -802,7 +802,7 @@ def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := t
let type instantiateMVars ( fvarId.getType)
let (typeNew, usedSimps') dsimp type ctx
usedSimps := usedSimps'
if typeNew.consumeMData.isConstOf ``False then
if typeNew.isFalse then
mvarIdNew.assign ( mkFalseElim ( mvarIdNew.getType) (mkFVar fvarId))
return (none, usedSimps)
if typeNew != type then
@@ -811,7 +811,7 @@ def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := t
let target mvarIdNew.getType
let (targetNew, usedSimps') dsimp target ctx usedSimps
usedSimps := usedSimps'
if targetNew.consumeMData.isConstOf ``True then
if targetNew.isTrue then
mvarIdNew.assign (mkConst ``True.intro)
return (none, usedSimps)
if let some (_, lhs, rhs) := targetNew.consumeMData.eq? then

View File

@@ -182,7 +182,7 @@ def simpCtorEq : Simproc := fun e => withReducibleAndInstances do
@[inline] def simpUsingDecide : Simproc := fun e => do
unless ( getConfig).decide do
return .continue
if e.hasFVar || e.hasMVar || e.consumeMData.isConstOf ``True || e.consumeMData.isConstOf ``False then
if e.hasFVar || e.hasMVar || e.isTrue || e.isFalse then
return .continue
try
let d mkDecide e
@@ -288,7 +288,7 @@ Discharge procedure for the ground/symbolic evaluator.
def dischargeGround (e : Expr) : SimpM (Option Expr) := do
trace[Meta.Tactic.simp.discharge] ">> discharge?: {e}"
let r simp e
if r.expr.consumeMData.isConstOf ``True then
if r.expr.isTrue then
try
return some ( mkOfEqTrue ( r.getProof))
catch _ =>
@@ -387,9 +387,10 @@ def simpGround : Simproc := fun e => do
if ctx.simpTheorems.isErased (.decl declName) then return .continue
-- Matcher applications should have been reduced before we get here.
if ( isMatcher declName) then return .continue
trace[Meta.Tactic.Simp.ground] "seval: {e}"
let r seval e
trace[Meta.Tactic.Simp.ground] "seval result: {e} => {r.expr}"
let r withTraceNode `Meta.Tactic.simp.ground (fun
| .ok r => return m!"seval: {e} => {r.expr}"
| .error err => return m!"seval: {e} => {err.toMessageData}") do
seval e
return .done r
def preDefault (s : SimprocsArray) : Simproc :=
@@ -431,7 +432,7 @@ where
go (e : Expr) : Bool :=
match e with
| .forallE _ d b _ => (d.isEq || d.isHEq || b.hasLooseBVar 0) && go b
| _ => e.consumeMData.isConstOf ``False
| _ => e.isFalse
def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
( getLCtx).findDeclRevM? fun localDecl => do
@@ -471,6 +472,7 @@ where
return some mvarId
def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
let e := e.cleanupAnnotations
if isEqnThmHypothesis e then
if let some r dischargeUsingAssumption? e then
return some r
@@ -484,7 +486,7 @@ def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
else
withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
let r simp e
if r.expr.consumeMData.isConstOf ``True then
if r.expr.isTrue then
try
return some ( mkOfEqTrue ( r.getProof))
catch _ =>

View File

@@ -130,7 +130,7 @@ def main : M (Option MVarId) := do
let mut toClear := #[]
let mut modified := false
for e in ( get).entries do
if e.type.consumeMData.isConstOf ``True then
if e.type.isTrue then
-- Do not assert `True` hypotheses
toClear := toClear.push e.fvarId
else if modified || e.type != e.origType then

View File

@@ -247,6 +247,19 @@ See also `Lean.PrettyPrinter.Delaborator.Context.depth`.
def withIncDepth (act : DelabM α) : DelabM α := fun ctx =>
act { ctx with depth := ctx.depth + 1 }
/--
Returns true if `e` is a "shallow" expression.
Local variables, constants, and other atomic expressions are always shallow.
In general, an expression is considered to be shallow if its depth is at most `threshold`.
Since the implementation uses `Lean.Expr.approxDepth`, the `threshold` is clamped to `[0, 254]`.
-/
def isShallowExpression (threshold : Nat) (e : Expr) : Bool :=
-- Approximate depth is saturated at 255 for very deep expressions.
-- Need to clamp to `[0, 254]` so that not every expression is shallow.
let threshold := min 254 threshold
e.approxDepth.toNat threshold
/--
Returns `true` if, at the current depth, we should omit the term and use `⋯` rather than
delaborating it. This function can only return `true` if `pp.deepTerms` is set to `false`.
@@ -255,25 +268,59 @@ an expression, which prevents terms such as atomic expressions or `OfNat.ofNat`
delaborated as `⋯`.
-/
def shouldOmitExpr (e : Expr) : DelabM Bool := do
if getPPOption getPPDeepTerms then
-- Atomic expressions never get omitted, so we can do an early return here.
if e.isAtomic then
return false
if ( getPPOption getPPDeepTerms) then
return false
let depth := ( read).depth
let depthThreshold getPPOption getPPDeepTermsThreshold
let approxDepth := e.approxDepth.toNat
let depthExcess := depth - depthThreshold
-- This threshold for shallow expressions effectively allows full terms to be pretty printed 25% deeper,
-- so long as the subterm actually can be fully pretty printed within this extra 25% depth.
let threshold := depthThreshold/4 - depthExcess
let isMaxedOutApproxDepth := approxDepth >= 255
let isShallowExpression :=
!isMaxedOutApproxDepth && approxDepth <= depthThreshold/4 - depthExcess
return depthExcess > 0 && !isShallowExpression threshold e
return depthExcess > 0 && !isShallowExpression
/--
Returns `true` if the given expression is a proof and should be omitted.
This function only returns `true` if `pp.proofs` is set to `false`.
"Shallow" proofs are not omitted.
The `pp.proofs.threshold` option controls the depth threshold for what constitutes a shallow proof.
See `Lean.PrettyPrinter.Delaborator.isShallowExpression`.
-/
def shouldOmitProof (e : Expr) : DelabM Bool := do
-- Atomic expressions never get omitted, so we can do an early return here.
if e.isAtomic then
return false
if ( getPPOption getPPProofs) then
return false
unless ( try Meta.isProof e catch _ => pure false) do
return false
return !isShallowExpression ( getPPOption getPPProofsThreshold) e
/--
Annotates the term with the current expression position and registers `TermInfo`
to associate the term to the current expression.
-/
def annotateTermInfo (stx : Term) : Delab := do
let stx annotateCurPos stx
addTermInfo ( getPos) stx ( getExpr)
pure stx
/--
Modifies the delaborator so that it annotates the resulting term with the current expression
position and registers `TermInfo` to associate the term to the current expression.
-/
def withAnnotateTermInfo (d : Delab) : Delab := do
let stx d
annotateTermInfo stx
/--
Delaborates the current expression as `⋯` and attaches `Elab.OmissionInfo`, which influences how the
@@ -299,13 +346,14 @@ partial def delab : Delab := do
if shouldOmitExpr e then
return omission
-- no need to hide atomic proofs
if pure !e.isAtomic <&&> pure !( getPPOption getPPProofs) <&&> (try Meta.isProof e catch _ => pure false) then
if shouldOmitProof e then
let pf omission
if getPPOption getPPProofsWithType then
let stx withType delab
return annotateTermInfo ( `((_ : $stx)))
return annotateCurPos ( `(($pf : $stx)))
else
return annotateTermInfo ( ``(_))
return pf
let k getExprKind
let stx withIncDepth <| delabFor k <|> (liftM $ show MetaM _ from throwError "don't know how to delaborate '{k}'")
if getPPOption getPPAnalyzeTypeAscriptions <&&> getPPOption getPPAnalysisNeedsType <&&> pure !e.isMData then

View File

@@ -331,7 +331,11 @@ With this combinator one can use an arity-2 delaborator to pretty print this as
The combinator will fail if fewer than this number of arguments are passed,
and if more than this number of arguments are passed the arguments are handled using
the standard application delaborator.
* `x`: constructs data corresponding to the main application (`f x` in the example)
* `x`: constructs data corresponding to the main application (`f x` in the example).
In the event of overapplication, the delaborator `x` is wrapped in
`Lean.PrettyPrinter.Delaborator.withAnnotateTermInfo` to register `TermInfo` for the resulting term.
The effect of this is that the term is hoverable in the Infoview.
-/
def withOverApp (arity : Nat) (x : Delab) : Delab := do
let n := ( getExpr).getAppNumArgs
@@ -339,7 +343,7 @@ def withOverApp (arity : Nat) (x : Delab) : Delab := do
if n == arity then
x
else
delabAppCore (n - arity) x
delabAppCore (n - arity) (withAnnotateTermInfo x)
/-- State for `delabAppMatch` and helpers. -/
structure AppMatchState where
@@ -677,6 +681,13 @@ def delabLetE : Delab := do
`(let $(mkIdent n) : $stxT := $stxV; $stxB)
else `(let $(mkIdent n) := $stxV; $stxB)
@[builtin_delab app.Char.ofNat]
def delabChar : Delab := do
let e getExpr
guard <| e.getAppNumArgs == 1
let .lit (.natVal n) := e.appArg! | failure
return quote (Char.ofNat n)
@[builtin_delab lit]
def delabLit : Delab := do
let Expr.lit l getExpr | unreachable!

View File

@@ -118,12 +118,17 @@ register_builtin_option pp.tagAppFns : Bool := {
register_builtin_option pp.proofs : Bool := {
defValue := false
group := "pp"
descr := "(pretty printer) if set to false, replace proofs appearing as an argument to a function with a placeholder"
descr := "(pretty printer) display proofs when true, and replace proofs appearing within expressions by `⋯` when false"
}
register_builtin_option pp.proofs.withType : Bool := {
defValue := true
defValue := false
group := "pp"
descr := "(pretty printer) when eliding a proof (see `pp.proofs`), show its type instead"
descr := "(pretty printer) when `pp.proofs` is false, adds a type ascription to the omitted proof"
}
register_builtin_option pp.proofs.threshold : Nat := {
defValue := 0
group := "pp"
descr := "(pretty printer) when `pp.proofs` is false, controls the complexity of proofs at which they begin being replaced with `⋯`"
}
register_builtin_option pp.instances : Bool := {
defValue := true
@@ -220,14 +225,15 @@ def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPA
def getPPInstantiateMVars (o : Options) : Bool := o.get pp.instantiateMVars.name pp.instantiateMVars.defValue
def getPPBeta (o : Options) : Bool := o.get pp.beta.name pp.beta.defValue
def getPPSafeShadowing (o : Options) : Bool := o.get pp.safeShadowing.name pp.safeShadowing.defValue
def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (getPPAll o)
def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (pp.proofs.defValue || getPPAll o)
def getPPProofsWithType (o : Options) : Bool := o.get pp.proofs.withType.name pp.proofs.withType.defValue
def getPPProofsThreshold (o : Options) : Nat := o.get pp.proofs.threshold.name pp.proofs.threshold.defValue
def getPPMotivesPi (o : Options) : Bool := o.get pp.motives.pi.name pp.motives.pi.defValue
def getPPMotivesNonConst (o : Options) : Bool := o.get pp.motives.nonConst.name pp.motives.nonConst.defValue
def getPPMotivesAll (o : Options) : Bool := o.get pp.motives.all.name pp.motives.all.defValue
def getPPInstances (o : Options) : Bool := o.get pp.instances.name pp.instances.defValue
def getPPInstanceTypes (o : Options) : Bool := o.get pp.instanceTypes.name pp.instanceTypes.defValue
def getPPDeepTerms (o : Options) : Bool := o.get pp.deepTerms.name pp.deepTerms.defValue
def getPPDeepTerms (o : Options) : Bool := o.get pp.deepTerms.name (pp.deepTerms.defValue || getPPAll o)
def getPPDeepTermsThreshold (o : Options) : Nat := o.get pp.deepTerms.threshold.name pp.deepTerms.threshold.defValue
end Lean

View File

@@ -117,7 +117,7 @@ def publishDiagnostics (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic) (
method := "textDocument/publishDiagnostics"
param := {
uri := m.uri
version? := m.version
version? := some m.version
diagnostics := diagnostics
: PublishDiagnosticsParams
}

View File

@@ -28,12 +28,18 @@ instance : ToExpr Nat where
toExpr := mkNatLit
toTypeExpr := mkConst ``Nat
instance : ToExpr Int where
toTypeExpr := .const ``Int []
toExpr i := match i with
| .ofNat n => mkApp (.const ``Int.ofNat []) (toExpr n)
| .negSucc n => mkApp (.const ``Int.negSucc []) (toExpr n)
instance : ToExpr Bool where
toExpr := fun b => if b then mkConst ``Bool.true else mkConst ``Bool.false
toTypeExpr := mkConst ``Bool
instance : ToExpr Char where
toExpr := fun c => mkApp (mkConst ``Char.ofNat) (toExpr c.toNat)
toExpr := fun c => mkApp (mkConst ``Char.ofNat) (mkRawNatLit c.toNat)
toTypeExpr := mkConst ``Char
instance : ToExpr String where

View File

@@ -128,7 +128,7 @@ def addRawTrace (msg : MessageData) : m Unit := do
def addTrace (cls : Name) (msg : MessageData) : m Unit := do
let ref getRef
let msg addMessageContext msg
modifyTraces (·.push { ref, msg := .trace cls msg #[] })
modifyTraces (·.push { ref, msg := .trace (collapsed := false) cls msg #[] })
@[inline] def trace (cls : Name) (msg : Unit MessageData) : m Unit := do
if ( isTracingEnabledFor cls) then

View File

@@ -82,7 +82,8 @@ def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos :=
withOptionAtCurrPos pp.explicit.name true do
delabApp
else
delab
withOptionAtCurrPos pp.proofs.name true do
delab
let fmt, infos PrettyPrinter.ppExprWithInfos e (delab := delab)
let tt := TaggedText.prettyTagged fmt
let ctx := {

View File

@@ -91,6 +91,15 @@ private inductive EmbedFmt
private abbrev MsgFmtM := StateT (Array EmbedFmt) IO
/--
Number of trace node children to display by default in the info view in order to prevent slowdowns
from rendering.
-/
register_option infoview.maxTraceChildren : Nat := {
defValue := 50
descr := "Number of trace node children to display by default"
}
open MessageData in
private partial def msgToInteractiveAux (msgData : MessageData) : IO (Format × Array EmbedFmt) :=
go { currNamespace := Name.anonymous, openDecls := [] } none msgData #[]
@@ -138,12 +147,25 @@ where
match ctx with
| some ctx => MessageData.withContext ctx child
| none => child
let blockSize := ctx.bind (infoview.maxTraceChildren.get? ·.opts)
|>.getD infoview.maxTraceChildren.defValue
let children := chopUpChildren cls blockSize children.toSubarray
pure (.lazy children)
else
pure (.strict ( children.mapM (go nCtx ctx)))
let e := .trace cls header collapsed nodes
return .tag ( pushEmbed e) ".\n"
/-- Recursively moves child nodes after the first `blockSize` into a new "more" node. -/
chopUpChildren (cls : Name) (blockSize : Nat) (children : Subarray MessageData) :
Array MessageData :=
if children.size > blockSize + 1 then -- + 1 to make idempotent
let more := chopUpChildren cls blockSize children[blockSize:]
children[:blockSize].toArray.push <|
.trace (collapsed := true) cls
f!"{dbgTraceVal <| children.size - blockSize} more entries..." more
else children
partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent : Nat := 0) : IO (TaggedText MsgEmbed) := do
if !hasWidgets then
return (TaggedText.prettyTagged ( msgData.format)).rewrite fun _ tt => .text tt.stripTags

View File

@@ -21,6 +21,9 @@ abbrev ResultM := OptionIO
namespace Job
@[inline] def try? (self : Job α) : Job (Option α) := do
some <$> self.run
@[inline] def nil : Job Unit :=
pure ()
@@ -62,6 +65,11 @@ namespace BuildJob
instance : Pure BuildJob := BuildJob.pure
@[inline] def try? (self : BuildJob α) : BuildJob (Option α) :=
mk <| self.toJob.map fun
| none => some (none, nilTrace)
| some (a, t) => some (some a, t)
@[inline] protected def map (f : α β) (self : BuildJob α) : BuildJob β :=
mk <| (fun (a,t) => (f a,t)) <$> self.toJob
@@ -88,6 +96,9 @@ instance : Await BuildJob ResultM := ⟨BuildJob.await⟩
@[inline] def materialize (self : BuildJob α) : ResultM Unit :=
discard <| await self.toJob
def add (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob α) :=
mk <$> seqLeftAsync t1.toJob t2.toJob
def mix (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob Unit) :=
mk <$> seqWithAsync (fun (_,t) (_,t') => ((), mixTrace t t')) t1.toJob t2.toJob

View File

@@ -35,7 +35,7 @@ def Package.recBuildExtraDepTargets (self : Package) : IndexBuildM (BuildJob Uni
job job.mix <| dep.extraDep.fetch
-- Fetch pre-built release if desired and this package is a dependency
if self.name ( getWorkspace).root.name self.preferReleaseBuild then
job job.mix <| self.release.fetch
job job.add ( self.release.fetch).try?
-- Build this package's extra dep targets
for target in self.extraDepTargets do
job job.mix <| self.fetchTargetJob target
@@ -49,28 +49,23 @@ def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
def Package.fetchRelease (self : Package) : SchedulerM (BuildJob Unit) := Job.async do
let repo := GitRepo.mk self.dir
let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
let some repoUrl := repoUrl? <|> ( repo.getFilteredRemoteUrl?) | do
logWarning <| s!"{self.name}: wanted prebuilt release, " ++
let some repoUrl := repoUrl? <|> ( repo.getFilteredRemoteUrl?)
| error <| s!"{self.name}: wanted prebuilt release, " ++
"but package's repository URL was not known; it may need to set `releaseRepo?`"
return ((), .nil)
let some tag repo.findTag? | do
logWarning <| s!"{self.name}: wanted prebuilt release, " ++
let some tag repo.findTag?
| error <| s!"{self.name}: wanted prebuilt release, " ++
"but could not find an associated tag for the package's revision"
return ((), .nil)
let url := s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}"
let logName := s!"{self.name}/{tag}/{self.buildArchive}"
try
let depTrace := Hash.ofString url
let traceFile := FilePath.mk <| self.buildArchiveFile.toString ++ ".trace"
let upToDate buildUnlessUpToDate' self.buildArchiveFile depTrace traceFile do
logStep s!"Downloading {self.name} cloud release"
download logName url self.buildArchiveFile
unless upToDate && ( self.buildDir.pathExists) do
logStep s!"Unpacking {self.name} cloud release"
untar logName self.buildArchiveFile self.buildDir
return ((), .nil)
else
return ((), .nil)
let depTrace := Hash.ofString url
let traceFile := FilePath.mk <| self.buildArchiveFile.toString ++ ".trace"
let upToDate buildUnlessUpToDate' self.buildArchiveFile depTrace traceFile do
logStep s!"Downloading {self.name} cloud release"
download logName url self.buildArchiveFile
unless upToDate && ( self.buildDir.pathExists) do
logStep s!"Unpacking {self.name} cloud release"
untar logName self.buildArchiveFile self.buildDir
return ((), .nil)
/-- The `PackageFacetConfig` for the builtin `releaseFacet`. -/
def Package.releaseFacetConfig : PackageFacetConfig releaseFacet :=

View File

@@ -151,10 +151,6 @@ structure ConfigTrace where
options : NameMap String
deriving ToJson, FromJson
inductive ConfigLock
| olean (h : IO.FS.Handle)
| lean (h : IO.FS.Handle) (lakeOpts : NameMap String)
/--
Import the `.olean` for the configuration file if `reconfigure` is not set and
an up-to-date one exists (i.e., one with matching configuration and on the same
@@ -166,55 +162,63 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String)
| error "invalid configuration file name"
let olean := lakeDir / configName.withExtension "olean"
let traceFile := lakeDir / configName.withExtension "olean.trace"
let lockFile := lakeDir / configName.withExtension "olean.lock"
/-
Remark: To prevent race conditions between the `.olean` and its trace file
Remark:
To prevent race conditions between the `.olean` and its trace file
(i.e., one process writes a new configuration while another reads an old one
and vice versa), Lake takes opens a single handle on the trace file and
acquires a lock on it. The lock is held while the lock data is read and
the olean is either imported or a new one is written with new lock data.
and vice versa), Lake performs file locking to ensure exclusive access.
To check if the trace is up-to-date, Lake opens a read-only handle on the
trace file and acquires a shared lock on it. The lock is held while the
trace is read and compared to the expected value. If it matches, the olean is
imported and the (shared) lock is then released.
If the trace is out-of-date, Lake upgrades the trace to read-write handle
with an exclusive lock. Lake does this by first acquiring a exclusive lock to
configuration's lock file (i.e. `olean.lock`). While holding this lock, Lake
releases the shared lock on the trace, re-opens the trace with a read-write
handle, and acquires an exclusive lock on the trace. It then releases its
lock on the lock file. writes the new lock data.
-/
let configHash computeTextFileHash configFile
let configLock : ConfigLock id do
let validateTrace h : IO ConfigLock := id do
if reconfigure then
h.lock; return .lean h lakeOpts
h.lock (exclusive := false)
let contents h.readToEnd; h.rewind
let .ok (trace : ConfigTrace) := Json.parse contents >>= fromJson?
| error "compiled configuration is invalid; run with `-R` to reconfigure"
let upToDate :=
( olean.pathExists) trace.platform = System.Platform.target
trace.leanHash = Lean.githash trace.configHash = configHash
if upToDate then
return .olean h
else
-- Upgrade to an exclusive lock
let lockFile := lakeDir / configName.withExtension "olean.lock"
let hLock IO.FS.Handle.mk lockFile .write
hLock.lock; h.unlock; h.lock; hLock.unlock
return .lean h trace.options
if ( traceFile.pathExists) then
validateTrace <| IO.FS.Handle.mk traceFile .readWrite
else
IO.FS.createDirAll lakeDir
match ( IO.FS.Handle.mk traceFile .writeNew |>.toBaseIO) with
| .ok h =>
h.lock; return .lean h lakeOpts
| .error (.alreadyExists ..) =>
validateTrace <| IO.FS.Handle.mk traceFile .readWrite
| .error e => error e.toString
match configLock with
| .olean h =>
let env importConfigFileCore olean leanOpts
h.unlock
return env
| .lean h lakeOpts =>
let acquireTrace h : IO IO.FS.Handle := id do
let hLock IO.FS.Handle.mk lockFile .write
/-
NOTE: We write the trace before elaborating the configuration file
Remark:
We do not wait for a lock here, because that can lead to deadlock.
This is because we are already holding a shared lock on the trace.
If multiple process race for this lock, one will get it and then
wait for an exclusive lock one the trace file, but be blocked by the
other process with a shared lock waiting on this file.
While there is likely a way to sequence this to avoid erroring,
simultaneous reconfigures are likely to produce unexpected results
anyway, so the error seems wise nonetheless.
-/
if ( hLock.tryLock) then
h.unlock
let h IO.FS.Handle.mk traceFile .readWrite
h.lock
hLock.unlock
return h
else
h.unlock
error <| s!"could not acquire an exclusive configuration lock; " ++
"another process may already be reconfiguring the package"
let configHash computeTextFileHash configFile
let elabConfig h (lakeOpts : NameMap String) : LogIO Environment := id do
/-
Remark:
We write the trace before elaborating the configuration file
to enable automatic reconfiguration on the next `lake` invocation if
elaboration fails. To ensure a failure triggers a reconfigure, we must also
remove any previous out-of-date `.olean`. Otherwise, Lake will treat the
older `.olean` as matching the new trace.
See the related PR and Zulip discussion for more details:
[leanprover/lean4#3069](https://github.com/leanprover/lean4/pull/3069).
-/
match ( IO.FS.removeFile olean |>.toBaseIO) with
| .ok _ | .error (.noFileOrDirectory ..) =>
@@ -231,3 +235,30 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String)
h.unlock
IO.FS.removeFile traceFile
failure
let validateTrace h : LogIO Environment := id do
if reconfigure then
elabConfig ( acquireTrace h) lakeOpts
else
h.lock (exclusive := false)
let contents h.readToEnd
let .ok (trace : ConfigTrace) := Json.parse contents >>= fromJson?
| error "compiled configuration is invalid; run with '-R' to reconfigure"
let upToDate :=
( olean.pathExists) trace.platform = System.Platform.target
trace.leanHash = Lean.githash trace.configHash = configHash
if upToDate then
let env importConfigFileCore olean leanOpts
h.unlock
return env
else
elabConfig ( acquireTrace h) trace.options
if ( traceFile.pathExists) then
validateTrace <| IO.FS.Handle.mk traceFile .read
else
IO.FS.createDirAll lakeDir
match ( IO.FS.Handle.mk traceFile .writeNew |>.toBaseIO) with
| .ok h =>
h.lock; elabConfig h lakeOpts
| .error (.alreadyExists ..) =>
validateTrace <| IO.FS.Handle.mk traceFile .read
| .error e => error e.toString

Binary file not shown.

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Array/Lemmas.c generated Normal file

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Cast.c generated Normal file

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Int/Bitwise.c generated Normal file

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Int/DivMod.c generated Normal file

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Int/DivModLemmas.c generated Normal file

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Int/Gcd.c generated Normal file

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Int/Lemmas.c generated Normal file

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Int/Order.c generated Normal file

Binary file not shown.

Binary file not shown.

BIN
stage0/stdlib/Init/Data/List/Lemmas.c generated Normal file

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Option/Lemmas.c generated Normal file

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Some files were not shown because too many files have changed in this diff Show More