Compare commits

...

29 Commits

Author SHA1 Message Date
Kim Morrison
5aedb2b8d4 chore: reordering in Array.Basic 2024-09-20 11:45:25 +10:00
Kim Morrison
cd9f3e12e0 chore: reordering in Array.Basic 2024-09-20 11:45:17 +10:00
David Thrane Christiansen
7b8f2fe54c doc: mark «tacticHave'_:=_» as an alternative form of have' (#5396)
This is to simplify the manual's cross-referencing.
2024-09-19 17:09:57 +00:00
Sebastian Ullrich
34f85bee02 fix: unused variable false positive when combining alias and non-lexical use (#5335)
We need to follow the fvar aliases registered by `match` in both
directions

Fixes #4714, fixes #2837

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
2024-09-19 10:51:14 +00:00
Kim Morrison
590c725943 feat: lemmas about List.maximum? (#5394) 2024-09-19 09:23:11 +00:00
Kim Morrison
9193196208 feat: List.fold / attach lemmas (#5392) 2024-09-19 08:26:06 +00:00
Kim Morrison
c3f384d6a5 feat: review of List.erase / List.find lemmas (#5391) 2024-09-19 05:37:04 +00:00
Tobias Grosser
daf24ff6aa feat: add BitVec.ofBool_[and|or|xor]_ofBool theorems (#5385)
... and use them to simplify some proofs.
2024-09-18 21:59:09 +00:00
Henrik Böving
fa6afa85df refactor: remove the last use of Lean.(HashSet|HashMap) (#5362) 2024-09-18 18:20:51 +00:00
Henrik Böving
592e1dc6c2 feat: bv_decide diagnosis (#5365)
Fixes: #5326
2024-09-18 17:55:16 +00:00
David Thrane Christiansen
c4293f04ef feat: add Nonempty instances for products (#5374)
After #5270, `partial` functions that use products of sums no longer
compile with only `Nonempty` constraints on their arguments. These
instances allow the compilation to work.
2024-09-18 16:34:45 +00:00
Kim Morrison
e417ad8a70 feat: missing Fin @[simp] lemmas (#5380) 2024-09-18 10:06:35 +00:00
Kim Morrison
ddd471223c chore: cleaning up redundant simp lemmas (#5381)
Problems reported by the simpNF linter downstream.
2024-09-18 10:06:29 +00:00
Kim Morrison
4e5e2ad311 chore: fixes spurious omega error in #5315 (#5382) 2024-09-18 09:43:09 +00:00
Kim Morrison
dcff54edb5 chore: notation ^^ for Bool.xor (#5332)
Not sure why this had been missing. Precedence is slightly higher than
`||`, matching the precedence order we have for bitwise operators.
2024-09-18 08:59:11 +00:00
Kim Morrison
30e90a4dff chore: upstream map_mergeSort (#5377)
This incorporates contributions from @eric-wieser in
https://github.com/leanprover-community/mathlib4/pull/15952 and
@fgdorais in https://github.com/leanprover-community/batteries/pull/579
2024-09-18 08:19:42 +00:00
Jeremy Tan Jie Rui
988fc7b25a chore: ensure that the rfl tactic tries Iff.rfl (#5359)
Revert the removal of the macro containing `Iff.rfl` in #5329; it was
causing errors in leanprover-community/mathlib4#16839.
2024-09-18 08:01:41 +00:00
Kim Morrison
3872027d92 chore: update stage0 2024-09-18 18:20:06 +10:00
Tobias Grosser
d38dc72a54 chore: introduce BitVec.setWidth to unify zeroExtend and truncate
incomplete deprecations

chore: complete deprecations
2024-09-18 18:20:06 +10:00
Alex Keizer
4641ed8c96 feat: add bv_decide normalization rules for ofBool (a.getLsbD i) and ofBool a[i] (#5375)
In LNSym we often use the pattern `ofBool (a.getLsbD i)` to pick out a
specific bit (`i`) from a bitvector (`a`).

By adding a rewrite to `extractLsb` to `bv_decide`s normalization set,
we can still automatically close goals that have this pattern. In the
process, I also added a simp-lemma about the value of a `Fin 1`.
2024-09-18 07:04:30 +00:00
Kim Morrison
77cd700fa8 chore: remove some @[simp]s from Fin lemmas (#5379)
These were dubious simps, barely used, that hurt confluence.
2024-09-18 05:50:11 +00:00
Kim Morrison
a6a06a620f chore: modify signature of lemmas about mergeSort (#5378)
This slightly smooths the interaction with `Prop` based reasoning in
Mathlib. Still not totally happy here.
2024-09-18 01:49:15 +00:00
Kim Morrison
21d71de481 chore: fix name of List.length_mergeSort (#5373) 2024-09-17 12:43:39 +00:00
Eric Wieser
b74f85accd fix: do not ban .. with a . on the next line (#4768)
Without this change,
```lean
example : True := by
  refine' trivial ..
  . trivial
```
is a parse error.
2024-09-17 09:57:35 +00:00
Eric Wieser
46b16b6df1 doc: explain the borrow syntax (#4305)
Obviously a link to the web docs isn't ideal, but having hovers
available on the symbol is much better than nothing.

---------

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2024-09-17 09:52:41 +00:00
Joachim Breitner
445c8f2ee0 feat: FunInd: more equalities in context, more careful cleanup (#5364)
A round of clean-up for the context of the functional induction
principle cases.

* Already previously, with `match e with | p => …`, functional induction
would ensure that `h : e = p` is in scope, but it wouldn’t work in
dependent cases. Now it introduces heterogeneous equality where needed
(fixes #4146)
* These equalities are now added always (previously we omitted them when
the discriminant was a variable that occurred in the goal, on the
grounds that the goal gets refined through the match, but it’s more
consistent to introduce the equality in any case)
* We no longer use `MVarId.cleanup` to clean up the goal; it was
sometimes too aggressive (fixes #5347)
* Instead, we clean up more carefully and with a custom strategy:
* First, we substitute all variables without a user-accessible name, if
we can.
  * Then, we substitute all variable, if we can, outside in.
* As we do that, we look for `HEq`s that we can turn into `Eq`s to
substitute some more
  * We substitute unused `let`s.
  
**Breaking change**: In some cases leads to a different functional
induction principle (different names and order of assumptions, for
example).
2024-09-16 12:30:12 +00:00
Kim Morrison
3f8e3e726d feat: some BitVec GetElem lemmas (#5361) 2024-09-16 11:30:05 +00:00
Kim Morrison
45af92fcd1 feat: lemmas about List.tail (#5360) 2024-09-16 09:25:24 +00:00
Tobias Grosser
7952a7f74d feat: add BitVec.getElem_truncate (#5278)
Co-authored-by: luisacicolini <luisacicolini@gmail.com>
Co-authored-by: Kim Morrison <scott@tqft.net>
2024-09-16 08:59:33 +00:00
84 changed files with 2265 additions and 835 deletions

View File

@@ -40,21 +40,23 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
/-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
@[simp] theorem dite_eq_ite [Decidable P] : (dite P (fun _ => a) fun _ => b) = ite P a b := rfl
-- We don't mark this as `simp` as it is already handled by `ite_eq_right_iff`.
@[deprecated "Use `ite_eq_right_iff`" (since := "2024-09-18")]
theorem ite_some_none_eq_none [Decidable P] :
(if P then some x else none) = none ¬ P := by
simp only [ite_eq_right_iff, reduceCtorEq]
rfl
@[simp] theorem ite_some_none_eq_some [Decidable P] :
@[deprecated "Use `Option.ite_none_right_eq_some`" (since := "2024-09-18")]
theorem ite_some_none_eq_some [Decidable P] :
(if P then some x else none) = some y P x = y := by
split <;> simp_all
-- This is not marked as `simp` as it is already handled by `dite_eq_right_iff`.
@[deprecated "Use `dite_eq_right_iff" (since := "2024-09-18")]
theorem dite_some_none_eq_none [Decidable P] {x : P α} :
(if h : P then some (x h) else none) = none ¬P := by
simp
@[simp] theorem dite_some_none_eq_some [Decidable P] {x : P α} {y : α} :
@[deprecated "Use `Option.dite_none_right_eq_some`" (since := "2024-09-18")]
theorem dite_some_none_eq_some [Decidable P] {x : P α} {y : α} :
(if h : P then some (x h) else none) = some y h : P, x h = y := by
by_cases h : P <;> simp [h]

View File

@@ -823,6 +823,8 @@ theorem iff_iff_implies_and_implies {a b : Prop} : (a ↔ b) ↔ (a → b) ∧ (
protected theorem Iff.rfl {a : Prop} : a a :=
Iff.refl a
macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl)
theorem Iff.of_eq (h : a = b) : a b := h Iff.rfl
theorem Iff.trans (h₁ : a b) (h₂ : b c) : a c :=
@@ -1191,6 +1193,21 @@ end
/-! # Product -/
instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (α × β) :=
Nonempty.elim h1 fun x =>
Nonempty.elim h2 fun y =>
(x, y)
instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (MProd α β) :=
Nonempty.elim h1 fun x =>
Nonempty.elim h2 fun y =>
x, y
instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (PProd α β) :=
Nonempty.elim h1 fun x =>
Nonempty.elim h2 fun y =>
x, y
instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
default := (default, default)

View File

@@ -15,3 +15,4 @@ import Init.Data.Array.BasicAux
import Init.Data.Array.Lemmas
import Init.Data.Array.TakeDrop
import Init.Data.Array.Bootstrap
import Init.Data.Array.GetLit

View File

@@ -13,43 +13,76 @@ import Init.Data.ToString.Basic
import Init.GetElem
universe u v w
namespace Array
/-! ### Array literal syntax -/
syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
macro_rules
| `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
variable {α : Type u}
namespace Array
/-! ### Preliminary theorems -/
@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
List.length_set ..
@[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
List.length_concat ..
theorem ext (a b : Array α)
(h₁ : a.size = b.size)
(h₂ : (i : Nat) (hi₁ : i < a.size) (hi₂ : i < b.size) a[i] = b[i])
: a = b := by
let rec extAux (a b : List α)
(h₁ : a.length = b.length)
(h₂ : (i : Nat) (hi₁ : i < a.length) (hi₂ : i < b.length) a.get i, hi₁ = b.get i, hi₂)
: a = b := by
induction a generalizing b with
| nil =>
cases b with
| nil => rfl
| cons b bs => rw [List.length_cons] at h₁; injection h₁
| cons a as ih =>
cases b with
| nil => rw [List.length_cons] at h₁; injection h₁
| cons b bs =>
have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
have headEq : a = b := h₂ 0 hz₁ hz₂
have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁
have h₂' : (i : Nat) (hi₁ : i < as.length) (hi₂ : i < bs.length) as.get i, hi₁ = bs.get i, hi₂ := by
intro i hi₁ hi₂
have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
have : (a::as).get i+1, hi₁' = (b::bs).get i+1, hi₂' := h₂ (i+1) hi₁' hi₂'
apply this
have tailEq : as = bs := ih bs h₁' h₂'
rw [headEq, tailEq]
cases a; cases b
apply congrArg
apply extAux
assumption
assumption
theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
cases as; cases bs; simp at h; rw [h]
@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := by
simp [List.toArray, Array.mkEmpty]
@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
@[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
@[extern "lean_mk_array"]
def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
toList := List.replicate n v
/--
`ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
```
ofFn f = #[f 0, f 1, ... , f(n - 1)]
``` -/
def ofFn {n} (f : Fin n α) : Array α := go 0 (mkEmpty n) where
/-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
go (i : Nat) (acc : Array α) : Array α :=
if h : i < n then go (i+1) (acc.push (f i, h)) else acc
termination_by n - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
/-- The array `#[0, 1, ..., n - 1]`. -/
def range (n : Nat) : Array Nat :=
n.fold (flip Array.push) (mkEmpty n)
@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
List.length_replicate ..
instance : EmptyCollection (Array α) := Array.empty
instance : Inhabited (Array α) where
default := Array.empty
@[simp] def isEmpty (a : Array α) : Bool :=
a.size = 0
def singleton (v : α) : Array α :=
mkArray 1 v
/-! ### Externs -/
/-- Low-level version of `size` that directly queries the C array object cached size.
While this is not provable, `usize` always returns the exact size of the array since
@@ -65,29 +98,6 @@ def usize (a : @& Array α) : USize := a.size.toUSize
def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
a[i.toNat]
instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
getElem xs i h := xs.uget i h
def back [Inhabited α] (a : Array α) : α :=
a.get! (a.size - 1)
def get? (a : Array α) (i : Nat) : Option α :=
if h : i < a.size then some a[i] else none
def back? (a : Array α) : Option α :=
a.get? (a.size - 1)
-- auxiliary declaration used in the equation compiler when pattern matching array literals.
abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
have := h₁.symm h₂
a[i]
@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
List.length_set ..
@[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
List.length_concat ..
/-- Low-level version of `fset` which is as fast as a C array fset.
`Fin` values are represented as tag pointers in the Lean runtime. Thus,
`fset` may be slightly slower than `uset`. -/
@@ -95,6 +105,19 @@ abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size =
def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
a.set i.toNat, h v
@[extern "lean_array_pop"]
def pop (a : Array α) : Array α where
toList := a.toList.dropLast
@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
match a with
| [] => rfl
| a::as => simp [pop, Nat.succ_sub_succ_eq_sub, size]
@[extern "lean_mk_array"]
def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
toList := List.replicate n v
/--
Swaps two entries in an array.
@@ -108,6 +131,10 @@ def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
let a' := a.set i v₂
a'.set (size_set a i v₂ j) v₁
@[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
show ((a.set i (a.get j)).set (size_set a i _ j) (a.get i)).size = a.size
rw [size_set, size_set]
/--
Swaps two entries in an array, or returns the array unchanged if either index is out of bounds.
@@ -121,6 +148,66 @@ def swap! (a : Array α) (i j : @& Nat) : Array α :=
else a
else a
/-! ### GetElem instance for `USize`, backed by `uget` -/
instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
getElem xs i h := xs.uget i h
/-! ### Definitions -/
instance : EmptyCollection (Array α) := Array.empty
instance : Inhabited (Array α) where
default := Array.empty
@[simp] def isEmpty (a : Array α) : Bool :=
a.size = 0
-- TODO(Leo): cleanup
@[specialize]
def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α α Bool) (i : Nat) : Bool :=
if h : i < a.size then
have : i < b.size := hsz h
p a[i] b[i] && isEqvAux a b hsz p (i+1)
else
true
decreasing_by simp_wf; decreasing_trivial_pre_omega
@[inline] def isEqv (a b : Array α) (p : α α Bool) : Bool :=
if h : a.size = b.size then
isEqvAux a b h p 0
else
false
instance [BEq α] : BEq (Array α) :=
fun a b => isEqv a b BEq.beq
/--
`ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
```
ofFn f = #[f 0, f 1, ... , f(n - 1)]
``` -/
def ofFn {n} (f : Fin n α) : Array α := go 0 (mkEmpty n) where
/-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
go (i : Nat) (acc : Array α) : Array α :=
if h : i < n then go (i+1) (acc.push (f i, h)) else acc
decreasing_by simp_wf; decreasing_trivial_pre_omega
/-- The array `#[0, 1, ..., n - 1]`. -/
def range (n : Nat) : Array Nat :=
n.fold (flip Array.push) (mkEmpty n)
def singleton (v : α) : Array α :=
mkArray 1 v
def back [Inhabited α] (a : Array α) : α :=
a.get! (a.size - 1)
def get? (a : Array α) (i : Nat) : Option α :=
if h : i < a.size then some a[i] else none
def back? (a : Array α) : Option α :=
a.get? (a.size - 1)
@[inline] def swapAt (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
let e := a.get i
let a := a.set i v
@@ -134,10 +221,6 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
have : Inhabited α := v
panic! ("index " ++ toString i ++ " out of bounds")
@[extern "lean_array_pop"]
def pop (a : Array α) : Array α where
toList := a.toList.dropLast
def shrink (a : Array α) (n : Nat) : Array α :=
let rec loop
| 0, a => a
@@ -311,7 +394,6 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
map (i+1) (r.push ( f as[i]))
else
pure r
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
map 0 (mkEmpty as.size)
@@ -384,7 +466,6 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
loop (j+1)
else
pure false
termination_by stop - j
decreasing_by simp_wf; decreasing_trivial_pre_omega
loop start
if h : stop as.size then
@@ -470,12 +551,22 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
if h : j < as.size then
if p as[j] then some j else loop (j + 1)
else none
termination_by as.size - j
decreasing_by simp_wf; decreasing_trivial_pre_omega
loop 0
def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
a.findIdx? fun a => a == v
a.findIdx? fun a => a == v
def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
if h : i < a.size then
let idx : Fin a.size := i, h;
if a.get idx == v then some idx
else indexOfAux a v (i+1)
else none
decreasing_by simp_wf; decreasing_trivial_pre_omega
def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
indexOfAux a v 0
@[inline]
def any (as : Array α) (p : α Bool) (start := 0) (stop := as.size) : Bool :=
@@ -491,13 +582,6 @@ def contains [BEq α] (as : Array α) (a : α) : Bool :=
def elem [BEq α] (a : α) (as : Array α) : Bool :=
as.contains a
@[inline] def getEvenElems (as : Array α) : Array α :=
(·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
if even then
(false, r.push a)
else
(true, r)
/-- Convert a `Array α` into an `List α`. This is O(n) in the size of the array. -/
-- This function is exported to C, where it is called by `Array.toList`
-- (the projection) to implement this functionality.
@@ -510,17 +594,6 @@ def toListImpl (as : Array α) : List α :=
def toListAppend (as : Array α) (l : List α) : List α :=
as.foldr List.cons l
instance {α : Type u} [Repr α] : Repr (Array α) where
reprPrec a _ :=
let _ : Std.ToFormat α := repr
if a.size == 0 then
"#[]"
else
Std.Format.bracketFill "#[" (Std.Format.joinSep (toList a) ("," ++ Std.Format.line)) "]"
instance [ToString α] : ToString (Array α) where
toString a := "#" ++ toString a.toList
protected def append (as : Array α) (bs : Array α) : Array α :=
bs.foldl (init := as) fun r v => r.push v
@@ -546,44 +619,13 @@ def concatMap (f : α → Array β) (as : Array α) : Array β :=
def flatten (as : Array (Array α)) : Array α :=
as.foldl (init := empty) fun r a => r ++ a
end Array
export Array (mkArray)
syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
macro_rules
| `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
namespace Array
-- TODO(Leo): cleanup
@[specialize]
def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α α Bool) (i : Nat) : Bool :=
if h : i < a.size then
have : i < b.size := hsz h
p a[i] b[i] && isEqvAux a b hsz p (i+1)
else
true
termination_by a.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
@[inline] def isEqv (a b : Array α) (p : α α Bool) : Bool :=
if h : a.size = b.size then
isEqvAux a b h p 0
else
false
instance [BEq α] : BEq (Array α) :=
fun a b => isEqv a b BEq.beq
@[inline]
def filter (p : α Bool) (as : Array α) (start := 0) (stop := as.size) : Array α :=
as.foldl (init := #[]) (start := start) (stop := stop) fun r a =>
if p a then r.push a else r
@[inline]
def filterM [Monad m] (p : α m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) :=
def filterM {α : Type} [Monad m] (p : α m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) :=
as.foldlM (init := #[]) (start := start) (stop := stop) fun r a => do
if ( p a) then return r.push a else return r
@@ -618,92 +660,23 @@ def partition (p : α → Bool) (as : Array α) : Array α × Array α := Id.run
cs := cs.push a
return (bs, cs)
theorem ext (a b : Array α)
(h₁ : a.size = b.size)
(h₂ : (i : Nat) (hi₁ : i < a.size) (hi₂ : i < b.size) a[i] = b[i])
: a = b := by
let rec extAux (a b : List α)
(h₁ : a.length = b.length)
(h₂ : (i : Nat) (hi₁ : i < a.length) (hi₂ : i < b.length) a.get i, hi₁ = b.get i, hi₂)
: a = b := by
induction a generalizing b with
| nil =>
cases b with
| nil => rfl
| cons b bs => rw [List.length_cons] at h₁; injection h₁
| cons a as ih =>
cases b with
| nil => rw [List.length_cons] at h₁; injection h₁
| cons b bs =>
have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
have headEq : a = b := h₂ 0 hz₁ hz₂
have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁
have h₂' : (i : Nat) (hi₁ : i < as.length) (hi₂ : i < bs.length) as.get i, hi₁ = bs.get i, hi₂ := by
intro i hi₁ hi₂
have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
have : (a::as).get i+1, hi₁' = (b::bs).get i+1, hi₂' := h₂ (i+1) hi₁' hi₂'
apply this
have tailEq : as = bs := ih bs h₁' h₂'
rw [headEq, tailEq]
cases a; cases b
apply congrArg
apply extAux
assumption
assumption
theorem extLit {n : Nat}
(a b : Array α)
(hsz₁ : a.size = n) (hsz₂ : b.size = n)
(h : (i : Nat) (hi : i < n) a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b :=
Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ hi₁)
end Array
-- CLEANUP the following code
namespace Array
def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
if h : i < a.size then
let idx : Fin a.size := i, h;
if a.get idx == v then some idx
else indexOfAux a v (i+1)
else none
termination_by a.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
indexOfAux a v 0
@[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
show ((a.set i (a.get j)).set (size_set a i _ j) (a.get i)).size = a.size
rw [size_set, size_set]
@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
match a with
| [] => rfl
| a::as => simp [pop, Nat.succ_sub_succ_eq_sub, size]
theorem reverse.termination {i j : Nat} (h : i < j) : j - 1 - (i + 1) < j - i := by
rw [Nat.sub_sub, Nat.add_comm]
exact Nat.lt_of_le_of_lt (Nat.pred_le _) (Nat.sub_succ_lt_self _ _ h)
def reverse (as : Array α) : Array α :=
if h : as.size 1 then
as
else
loop as 0 as.size - 1, Nat.pred_lt (mt (fun h : as.size = 0 => h by decide) h)
where
termination {i j : Nat} (h : i < j) : j - 1 - (i + 1) < j - i := by
rw [Nat.sub_sub, Nat.add_comm]
exact Nat.lt_of_le_of_lt (Nat.pred_le _) (Nat.sub_succ_lt_self _ _ h)
loop (as : Array α) (i : Nat) (j : Fin as.size) :=
if h : i < j then
have := reverse.termination h
have := termination h
let as := as.swap i, Nat.lt_trans h j.2 j
have : j-1 < as.size := by rw [size_swap]; exact Nat.lt_of_le_of_lt (Nat.pred_le _) j.2
loop as (i+1) j-1, this
else
as
termination_by j - i
def popWhile (p : α Bool) (as : Array α) : Array α :=
if h : as.size > 0 then
@@ -713,7 +686,6 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
as
else
as
termination_by as.size
decreasing_by simp_wf; decreasing_trivial_pre_omega
def takeWhile (p : α Bool) (as : Array α) : Array α :=
@@ -726,7 +698,6 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
r
else
r
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
go 0 #[]
@@ -744,6 +715,7 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
termination_by a.size - i.val
decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
-- This is required in `Lean.Data.PersistentHashMap`.
theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
induction a, i using Array.feraseIdx.induct with
| @case1 a i h a' _ ih =>
@@ -774,7 +746,6 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
loop as j', by rw [size_swap]; exact j'.2
else
as
termination_by j.1
decreasing_by simp_wf; decreasing_trivial_pre_omega
let j := as.size
let as := as.push a
@@ -786,41 +757,6 @@ def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
insertAt as i, Nat.lt_succ_of_le h a
else panic! "invalid index"
def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : (i : Nat), i a.size List α List α
| 0, _, acc => acc
| (i+1), hi, acc => toListLitAux a n hsz i (Nat.le_of_succ_le hi) (a.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
List.toArray <| toListLitAux a n hsz n (hsz Nat.le_refl _) []
theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
cases as; cases bs; simp at h; rw [h]
@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := by
simp [List.toArray, Array.mkEmpty]
@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
apply ext'
simp [toArrayLit, toList_toArray]
have hle : n as.size := hsz Nat.le_refl _
have hge : as.size n := hsz Nat.le_refl _
have := go n hle
rw [List.drop_eq_nil_of_le hge] at this
rw [this]
where
getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) h₂) :=
rfl
go (i : Nat) (hi : i as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size bs.size) (i : Nat) : Bool :=
if h : i < as.size then
let a := as[i]
@@ -832,7 +768,6 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
false
else
true
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
/-- Return true iff `as` is a prefix of `bs`.
@@ -843,23 +778,6 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
else
false
private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size Bool
| 0, _ => true
| i+1, h =>
have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
a != as[i] && allDiffAuxAux as a i this
private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
if h : i < as.size then
allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
else
true
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
def allDiff [BEq α] (as : Array α) : Bool :=
allDiffAux as 0
@[specialize] def zipWithAux (f : α β γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : Array γ :=
if h : i < as.size then
let a := as[i]
@@ -870,7 +788,6 @@ def allDiff [BEq α] (as : Array α) : Bool :=
cs
else
cs
termination_by as.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega
@[inline] def zipWith (as : Array α) (bs : Array β) (f : α β γ) : Array γ :=
@@ -886,4 +803,47 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
as.foldl (init := (#[], #[])) fun (as, bs) a =>
if p a then (as.push a, bs) else (as, bs.push a)
/-! ### Auxiliary functions used in metaprogramming.
We do not intend to provide verification theorems for these functions.
-/
private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size Bool
| 0, _ => true
| i+1, h =>
have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
a != as[i] && allDiffAuxAux as a i this
private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
if h : i < as.size then
allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
else
true
decreasing_by simp_wf; decreasing_trivial_pre_omega
def allDiff [BEq α] (as : Array α) : Bool :=
allDiffAux as 0
@[inline] def getEvenElems (as : Array α) : Array α :=
(·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
if even then
(false, r.push a)
else
(true, r)
/-! ### Repr and ToString -/
instance {α : Type u} [Repr α] : Repr (Array α) where
reprPrec a _ :=
let _ : Std.ToFormat α := repr
if a.size == 0 then
"#[]"
else
Std.Format.bracketFill "#[" (Std.Format.joinSep (toList a) ("," ++ Std.Format.line)) "]"
instance [ToString α] : ToString (Array α) where
toString a := "#" ++ toString a.toList
end Array
export Array (mkArray)

View File

@@ -0,0 +1,46 @@
/-
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Data.Array.Basic
namespace Array
/-! ### getLit -/
-- auxiliary declaration used in the equation compiler when pattern matching array literals.
abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
have := h₁.symm h₂
a[i]
theorem extLit {n : Nat}
(a b : Array α)
(hsz₁ : a.size = n) (hsz₂ : b.size = n)
(h : (i : Nat) (hi : i < n) a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b :=
Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ hi₁)
def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : (i : Nat), i a.size List α List α
| 0, _, acc => acc
| (i+1), hi, acc => toListLitAux a n hsz i (Nat.le_of_succ_le hi) (a.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
List.toArray <| toListLitAux a n hsz n (hsz Nat.le_refl _) []
theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
apply ext'
simp [toArrayLit, toList_toArray]
have hle : n as.size := hsz Nat.le_refl _
have hge : as.size n := hsz Nat.le_refl _
have := go n hle
rw [List.drop_eq_nil_of_le hge] at this
rw [this]
where
getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) h₂) :=
rfl
go (i : Nat) (hi : i as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
end Array

View File

@@ -19,7 +19,7 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
namespace Array
attribute [simp] data_toArray uset
attribute [simp] uset
@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
@@ -271,6 +271,9 @@ termination_by n - i
/-- # mkArray -/
@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
List.length_replicate ..
@[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
@[deprecated toList_mkArray (since := "2024-09-09")]
@@ -495,7 +498,6 @@ abbrev size_eq_length_data := @size_eq_length_toList
let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
rw [reverse.loop]
if h : i < j then
have := reverse.termination h
simp [(go · (i+1) j-1, ·), h]
else simp [h]
termination_by j - i
@@ -527,9 +529,8 @@ set_option linter.deprecated false in
(H : k, as.toList.get? k = if i k k j then a.toList.get? k else a.toList.reverse.get? k)
(k) : (reverse.loop as i j, hj).toList.get? k = a.toList.reverse.get? k := by
rw [reverse.loop]; dsimp; split <;> rename_i h₁
· have p := reverse.termination h₁
match j with | j+1 => ?_
simp only [Nat.add_sub_cancel] at p
· match j with | j+1 => ?_
simp only [Nat.add_sub_cancel]
rw [(go · (i+1) j)]
· rwa [Nat.add_right_comm i]
· simp [size_swap, h₂]
@@ -1113,5 +1114,4 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
· split <;> simp_all
· split <;> simp_all
end Array

View File

@@ -173,6 +173,9 @@ instance : GetElem (BitVec w) Nat Bool fun _ i => i < w where
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
x[i] = x.toNat.testBit i := rfl
theorem getLsbD_eq_getElem {x : BitVec w} {i : Nat} (h : i < w) :
x.getLsbD i = x[i] := rfl
end getElem
section Int
@@ -450,13 +453,15 @@ SMT-Lib name: `extract`.
def extractLsb (hi lo : Nat) (x : BitVec n) : BitVec (hi - lo + 1) := extractLsb' lo _ x
/--
A version of `zeroExtend` that requires a proof, but is a noop.
A version of `setWidth` that requires a proof, but is a noop.
-/
def zeroExtend' {n w : Nat} (le : n w) (x : BitVec n) : BitVec w :=
def setWidth' {n w : Nat} (le : n w) (x : BitVec n) : BitVec w :=
x.toNat#'(by
apply Nat.lt_of_lt_of_le x.isLt
exact Nat.pow_le_pow_of_le_right (by trivial) le)
@[deprecated setWidth' (since := "2024-09-18"), inherit_doc setWidth'] abbrev zeroExtend' := @setWidth'
/--
`shiftLeftZeroExtend x n` returns `zeroExtend (w+n) x <<< n` without
needing to compute `x % 2^(2+n)`.
@@ -469,22 +474,35 @@ def shiftLeftZeroExtend (msbs : BitVec w) (m : Nat) : BitVec (w + m) :=
(msbs.toNat <<< m)#'(shiftLeftLt msbs.isLt m)
/--
Zero extend vector `x` of length `w` by adding zeros in the high bits until it has length `v`.
If `v < w` then it truncates the high bits instead.
Transform `x` of length `w` into a bitvector of length `v`, by either:
- zero extending, that is, adding zeros in the high bits until it has length `v`, if `v > w`, or
- truncating the high bits, if `v < w`.
SMT-Lib name: `zero_extend`.
-/
def zeroExtend (v : Nat) (x : BitVec w) : BitVec v :=
def setWidth (v : Nat) (x : BitVec w) : BitVec v :=
if h : w v then
zeroExtend' h x
setWidth' h x
else
.ofNat v x.toNat
/--
Truncate the high bits of bitvector `x` of length `w`, resulting in a vector of length `v`.
If `v > w` then it zero-extends the vector instead.
Transform `x` of length `w` into a bitvector of length `v`, by either:
- zero extending, that is, adding zeros in the high bits until it has length `v`, if `v > w`, or
- truncating the high bits, if `v < w`.
SMT-Lib name: `zero_extend`.
-/
abbrev truncate := @zeroExtend
abbrev zeroExtend := @setWidth
/--
Transform `x` of length `w` into a bitvector of length `v`, by either:
- zero extending, that is, adding zeros in the high bits until it has length `v`, if `v > w`, or
- truncating the high bits, if `v < w`.
SMT-Lib name: `zero_extend`.
-/
abbrev truncate := @setWidth
/--
Sign extend a vector of length `w`, extending with `i` additional copies of the most significant
@@ -635,7 +653,7 @@ input is on the left, so `0xAB#8 ++ 0xCD#8 = 0xABCD#16`.
SMT-Lib name: `concat`.
-/
def append (msbs : BitVec n) (lsbs : BitVec m) : BitVec (n+m) :=
shiftLeftZeroExtend msbs m ||| zeroExtend' (Nat.le_add_left m n) lsbs
shiftLeftZeroExtend msbs m ||| setWidth' (Nat.le_add_left m n) lsbs
instance : HAppend (BitVec w) (BitVec v) (BitVec (w + v)) := .append

View File

@@ -132,18 +132,18 @@ theorem toNat_add_of_and_eq_zero {x y : BitVec w} (h : x &&& y = 0#w) :
simp [not_eq_true, carry_of_and_eq_zero h]
/-- Carry function for bitwise addition. -/
def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, Bool.xor x (Bool.xor y c))
def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, x ^^ (y ^^ c))
/-- Bitwise addition implemented via a ripple carry adder. -/
def adc (x y : BitVec w) : Bool Bool × BitVec w :=
iunfoldr fun (i : Fin w) c => adcb (x.getLsbD i) (y.getLsbD i) c
theorem getLsbD_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
getLsbD (x + y + zeroExtend w (ofBool c)) i =
Bool.xor (getLsbD x i) (Bool.xor (getLsbD y i) (carry i x y c)) := by
getLsbD (x + y + setWidth w (ofBool c)) i =
(getLsbD x i ^^ (getLsbD y i ^^ carry i x y c)) := by
let x, x_lt := x
let y, y_lt := y
simp only [getLsbD, toNat_add, toNat_zeroExtend, i_lt, toNat_ofFin, toNat_ofBool,
simp only [getLsbD, toNat_add, toNat_setWidth, i_lt, toNat_ofFin, toNat_ofBool,
Nat.mod_add_mod, Nat.add_mod_mod]
apply Eq.trans
rw [ Nat.div_add_mod x (2^i), Nat.div_add_mod y (2^i)]
@@ -161,15 +161,15 @@ theorem getLsbD_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool
theorem getLsbD_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
getLsbD (x + y) i =
Bool.xor (getLsbD x i) (Bool.xor (getLsbD y i) (carry i x y false)) := by
(getLsbD x i ^^ (getLsbD y i ^^ carry i x y false)) := by
simpa using getLsbD_add_add_bool i_lt x y false
theorem adc_spec (x y : BitVec w) (c : Bool) :
adc x y c = (carry w x y c, x + y + zeroExtend w (ofBool c)) := by
adc x y c = (carry w x y c, x + y + setWidth w (ofBool c)) := by
simp only [adc]
apply iunfoldr_replace
(fun i => carry i x y c)
(x + y + zeroExtend w (ofBool c))
(x + y + setWidth w (ofBool c))
c
case init =>
simp [carry, Nat.mod_one]
@@ -306,12 +306,12 @@ theorem mulRec_succ_eq (x y : BitVec w) (s : Nat) :
Recurrence lemma: truncating to `i+1` bits and then zero extending to `w`
equals truncating upto `i` bits `[0..i-1]`, and then adding the `i`th bit of `x`.
-/
theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w) (i : Nat) :
zeroExtend w (x.truncate (i + 1)) =
zeroExtend w (x.truncate i) + (x &&& twoPow w i) := by
theorem setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (x : BitVec w) (i : Nat) :
setWidth w (x.setWidth (i + 1)) =
setWidth w (x.setWidth i) + (x &&& twoPow w i) := by
rw [add_eq_or_of_and_eq_zero]
· ext k
simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
simp only [getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
by_cases hik : i = k
· subst hik
simp
@@ -322,27 +322,32 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w
· have hik'' : ¬ (k < i) := by omega
simp [hik', hik'']
· ext k
simp only [and_twoPow, getLsbD_and, getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and,
simp only [and_twoPow, getLsbD_and, getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and,
getLsbD_zero, and_eq_false_imp, and_eq_true, decide_eq_true_eq, and_imp]
by_cases hi : x.getLsbD i <;> simp [hi] <;> omega
@[deprecated setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (since := "2024-09-18"),
inherit_doc setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow]
abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow :=
@setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow
/--
Recurrence lemma: multiplying `x` with the first `s` bits of `y` is the
same as truncating `y` to `s` bits, then zero extending to the original length,
and performing the multplication. -/
theorem mulRec_eq_mul_signExtend_truncate (x y : BitVec w) (s : Nat) :
mulRec x y s = x * ((y.truncate (s + 1)).zeroExtend w) := by
theorem mulRec_eq_mul_signExtend_setWidth (x y : BitVec w) (s : Nat) :
mulRec x y s = x * ((y.setWidth (s + 1)).setWidth w) := by
induction s
case zero =>
simp only [mulRec_zero_eq, ofNat_eq_ofNat, Nat.reduceAdd]
by_cases y.getLsbD 0
case pos hy =>
simp only [hy, reduceIte, truncate, zeroExtend_one_eq_ofBool_getLsb_zero,
simp only [hy, reduceIte, setWidth_one_eq_ofBool_getLsb_zero,
ofBool_true, ofNat_eq_ofNat]
rw [zeroExtend_ofNat_one_eq_ofNat_one_of_lt (by omega)]
rw [setWidth_ofNat_one_eq_ofNat_one_of_lt (by omega)]
simp
case neg hy =>
simp [hy, zeroExtend_one_eq_ofBool_getLsb_zero]
simp [hy, setWidth_one_eq_ofBool_getLsb_zero]
case succ s' hs =>
rw [mulRec_succ_eq, hs]
have heq :
@@ -350,13 +355,16 @@ theorem mulRec_eq_mul_signExtend_truncate (x y : BitVec w) (s : Nat) :
(x * (y &&& (BitVec.twoPow w (s' + 1)))) := by
simp only [ofNat_eq_ofNat, and_twoPow]
by_cases hy : y.getLsbD (s' + 1) <;> simp [hy]
rw [heq, BitVec.mul_add, zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow]
rw [heq, BitVec.mul_add, setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow]
@[deprecated mulRec_eq_mul_signExtend_setWidth (since := "2024-09-18"),
inherit_doc mulRec_eq_mul_signExtend_setWidth]
abbrev mulRec_eq_mul_signExtend_truncate := @mulRec_eq_mul_signExtend_setWidth
theorem getLsbD_mul (x y : BitVec w) (i : Nat) :
(x * y).getLsbD i = (mulRec x y w).getLsbD i := by
simp only [mulRec_eq_mul_signExtend_truncate]
rw [truncate, truncate_eq_zeroExtend, truncate_eq_zeroExtend,
truncate_truncate_of_le]
simp only [mulRec_eq_mul_signExtend_setWidth]
rw [setWidth_setWidth_of_le]
· simp
· omega
@@ -402,22 +410,22 @@ theorem shiftLeft_or_of_and_eq_zero {x : BitVec w₁} {y z : BitVec w₂}
`shiftLeftRec x y n` shifts `x` to the left by the first `n` bits of `y`.
-/
theorem shiftLeftRec_eq {x : BitVec w₁} {y : BitVec w₂} {n : Nat} :
shiftLeftRec x y n = x <<< (y.truncate (n + 1)).zeroExtend w₂ := by
shiftLeftRec x y n = x <<< (y.setWidth (n + 1)).setWidth w₂ := by
induction n generalizing x y
case zero =>
ext i
simp only [shiftLeftRec_zero, twoPow_zero, Nat.reduceAdd, truncate_one,
and_one_eq_zeroExtend_ofBool_getLsbD]
simp only [shiftLeftRec_zero, twoPow_zero, Nat.reduceAdd, setWidth_one,
and_one_eq_setWidth_ofBool_getLsbD]
case succ n ih =>
simp only [shiftLeftRec_succ, and_twoPow]
rw [ih]
by_cases h : y.getLsbD (n + 1)
· simp only [h, reduceIte]
rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
rw [setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true h,
shiftLeft_or_of_and_eq_zero]
simp [and_twoPow]
· simp only [h, false_eq_true, reduceIte, shiftLeft_zero']
rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false (i := n + 1)]
rw [setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false (i := n + 1)]
simp [h]
/--
@@ -466,18 +474,18 @@ theorem sshiftRight'_or_of_and_eq_zero {x : BitVec w₁} {y z : BitVec w₂}
toNat_add_of_and_eq_zero h, sshiftRight_add]
theorem sshiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
sshiftRightRec x y n = x.sshiftRight' ((y.truncate (n + 1)).zeroExtend w₂) := by
sshiftRightRec x y n = x.sshiftRight' ((y.setWidth (n + 1)).setWidth w₂) := by
induction n generalizing x y
case zero =>
ext i
simp [twoPow_zero, Nat.reduceAdd, and_one_eq_zeroExtend_ofBool_getLsbD, truncate_one]
simp [twoPow_zero, Nat.reduceAdd, and_one_eq_setWidth_ofBool_getLsbD, setWidth_one]
case succ n ih =>
simp only [sshiftRightRec_succ_eq, and_twoPow, ih]
by_cases h : y.getLsbD (n + 1)
· rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
· rw [setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true h,
sshiftRight'_or_of_and_eq_zero (by simp [and_twoPow]), h]
simp
· rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false (i := n + 1)
· rw [setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false (i := n + 1)
(by simp [h])]
simp [h]
@@ -529,20 +537,20 @@ theorem ushiftRight'_or_of_and_eq_zero {x : BitVec w₁} {y z : BitVec w₂}
simp [ add_eq_or_of_and_eq_zero _ _ h, toNat_add_of_and_eq_zero h, shiftRight_add]
theorem ushiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
ushiftRightRec x y n = x >>> (y.truncate (n + 1)).zeroExtend w₂ := by
ushiftRightRec x y n = x >>> (y.setWidth (n + 1)).setWidth w₂ := by
induction n generalizing x y
case zero =>
ext i
simp only [ushiftRightRec_zero, twoPow_zero, Nat.reduceAdd,
and_one_eq_zeroExtend_ofBool_getLsbD, truncate_one]
and_one_eq_setWidth_ofBool_getLsbD, setWidth_one]
case succ n ih =>
simp only [ushiftRightRec_succ, and_twoPow]
rw [ih]
by_cases h : y.getLsbD (n + 1) <;> simp only [h, reduceIte]
· rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
· rw [setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true h,
ushiftRight'_or_of_and_eq_zero]
simp [and_twoPow]
· simp [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false, h]
· simp [setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false, h]
/--
Show that `x >>> y` can be written in terms of `ushiftRightRec`.

View File

@@ -48,7 +48,7 @@ private theorem iunfoldr.eq_test
simp only [init, eq_nil]
case step =>
intro i
simp_all [truncate_succ]
simp_all [setWidth_succ]
theorem iunfoldr_getLsbD' {f : Fin w α α × Bool} (state : Nat α)
(ind : (i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :

View File

@@ -234,6 +234,15 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
@[simp] theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b) := by cases b <;> rfl
@[simp] theorem ofBool_and_ofBool : ofBool b &&& ofBool b' = ofBool (b && b') := by
cases b <;> cases b' <;> rfl
@[simp] theorem ofBool_or_ofBool : ofBool b ||| ofBool b' = ofBool (b || b') := by
cases b <;> cases b' <;> rfl
@[simp] theorem ofBool_xor_ofBool : ofBool b ^^^ ofBool b' = ofBool (b ^^ b') := by
cases b <;> cases b' <;> rfl
@[simp, bv_toNat] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
@[simp] theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
@@ -273,8 +282,31 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m n) : x < 2 ^ n :=
Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
@[simp] theorem getElem_zero_ofNat_zero (i : Nat) (h : i < w) : (BitVec.ofNat w 0)[i] = false := by
simp [getElem_eq_testBit_toNat]
@[simp] theorem getElem_zero_ofNat_one (h : 0 < w) : (BitVec.ofNat w 1)[0] = true := by
simp [getElem_eq_testBit_toNat, h]
theorem getElem?_zero_ofNat_zero : (BitVec.ofNat (w+1) 0)[0]? = some false := by
simp
theorem getElem?_zero_ofNat_one : (BitVec.ofNat (w+1) 1)[0]? = some true := by
simp
-- This does not need to be a `@[simp]` theorem as it is already handled by `getElem?_eq_getElem`.
theorem getElem?_zero_ofBool (b : Bool) : (ofBool b)[0]? = some b := by
simp [ofBool, cond_eq_if]
split <;> simp_all
@[simp] theorem getElem_zero_ofBool (b : Bool) : (ofBool b)[0] = b := by
rw [getElem_eq_iff, getElem?_zero_ofBool]
theorem getElem?_succ_ofBool (b : Bool) (i : Nat) : (ofBool b)[i + 1]? = none := by
simp
@[simp]
theorem getLsbD_ofBool (b : Bool) (i : Nat) : (BitVec.ofBool b).getLsbD i = ((i = 0) && b) := by
theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) && b) := by
rcases b with rfl | rfl
· simp [ofBool]
· simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true]
@@ -330,6 +362,10 @@ theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat
@[simp] theorem getMsbD_cast (h : w = v) (x : BitVec w) : (cast h x).getMsbD i = x.getMsbD i := by
subst h; simp
@[simp] theorem getElem_cast (h : w = v) (x : BitVec w) (p : i < v) : (cast h x)[i] = x[i] := by
subst h; simp
@[simp] theorem msb_cast (h : w = v) (x : BitVec w) : (cast h x).msb = x.msb := by
simp [BitVec.msb]
@@ -412,46 +448,46 @@ theorem toInt_pos_iff {w : Nat} {x : BitVec w} :
0 BitVec.toInt x 2 * x.toNat < 2 ^ w := by
simp [toInt_eq_toNat_cond]; omega
/-! ### zeroExtend and truncate -/
/-! ### setWidth, zeroExtend and truncate -/
theorem truncate_eq_zeroExtend {v : Nat} {x : BitVec w} :
truncate v x = zeroExtend v x := rfl
@[simp]
theorem truncate_eq_setWidth {v : Nat} {x : BitVec w} :
truncate v x = setWidth v x := rfl
@[simp, bv_toNat] theorem toNat_zeroExtend' {m n : Nat} (p : m n) (x : BitVec m) :
(zeroExtend' p x).toNat = x.toNat := by
simp [zeroExtend']
@[simp]
theorem zeroExtend_eq_setWidth {v : Nat} {x : BitVec w} :
zeroExtend v x = setWidth v x := rfl
@[bv_toNat] theorem toNat_zeroExtend (i : Nat) (x : BitVec n) :
BitVec.toNat (zeroExtend i x) = x.toNat % 2^i := by
@[simp, bv_toNat] theorem toNat_setWidth' {m n : Nat} (p : m n) (x : BitVec m) :
(setWidth' p x).toNat = x.toNat := by
simp [setWidth']
@[simp, bv_toNat] theorem toNat_setWidth (i : Nat) (x : BitVec n) :
BitVec.toNat (setWidth i x) = x.toNat % 2^i := by
let x, lt_n := x
simp only [zeroExtend]
simp only [setWidth]
if n_le_i : n i then
have x_lt_two_i : x < 2 ^ i := lt_two_pow_of_le lt_n n_le_i
simp [n_le_i, Nat.mod_eq_of_lt, x_lt_two_i]
else
simp [n_le_i, toNat_ofNat]
theorem zeroExtend'_eq {x : BitVec w} (h : w v) : x.zeroExtend' h = x.zeroExtend v := by
theorem setWidth'_eq {x : BitVec w} (h : w v) : x.setWidth' h = x.setWidth v := by
apply eq_of_toNat_eq
rw [toNat_zeroExtend, toNat_zeroExtend']
rw [toNat_setWidth, toNat_setWidth']
rw [Nat.mod_eq_of_lt]
exact Nat.lt_of_lt_of_le x.isLt (Nat.pow_le_pow_right (Nat.zero_lt_two) h)
@[simp, bv_toNat] theorem toNat_truncate (x : BitVec n) : (truncate i x).toNat = x.toNat % 2^i :=
toNat_zeroExtend i x
@[simp] theorem zeroExtend_eq (x : BitVec n) : zeroExtend n x = x := by
@[simp] theorem setWidth_eq (x : BitVec n) : setWidth n x = x := by
apply eq_of_toNat_eq
let x, lt_n := x
simp [truncate, zeroExtend]
simp [setWidth]
@[simp] theorem zeroExtend_zero (m n : Nat) : zeroExtend m 0#n = 0#m := by
@[simp] theorem setWidth_zero (m n : Nat) : setWidth m 0#n = 0#m := by
apply eq_of_toNat_eq
simp [toNat_zeroExtend]
simp [toNat_setWidth]
theorem truncate_eq (x : BitVec n) : truncate n x = x := zeroExtend_eq x
@[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : BitVec.ofNat m x.toNat = truncate m x := by
@[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : BitVec.ofNat m x.toNat = setWidth m x := by
apply eq_of_toNat_eq
simp
@@ -470,33 +506,33 @@ theorem nat_eq_toNat {x : BitVec w} {y : Nat}
rw [@eq_comm _ _ x.toNat]
apply toNat_eq_nat
theorem getElem_zeroExtend' (x : BitVec w) (i : Nat) (h : w v) (hi : i < v) :
(zeroExtend' h x)[i] = x.getLsbD i := by
rw [getElem_eq_testBit_toNat, toNat_zeroExtend', getLsbD]
theorem getElem_setWidth' (x : BitVec w) (i : Nat) (h : w v) (hi : i < v) :
(setWidth' h x)[i] = x.getLsbD i := by
rw [getElem_eq_testBit_toNat, toNat_setWidth', getLsbD]
theorem getElem_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) :
(zeroExtend m x)[i] = x.getLsbD i := by
rw [zeroExtend]
theorem getElem_setWidth (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) :
(setWidth m x)[i] = x.getLsbD i := by
rw [setWidth]
split
· rw [getElem_zeroExtend']
· rw [getElem_setWidth']
· simp [getElem_eq_testBit_toNat, getLsbD]
omega
theorem getElem?_zeroExtend' (x : BitVec w) (i : Nat) (h : w v) :
(zeroExtend' h x)[i]? = if i < v then some (x.getLsbD i) else none := by
simp [getElem?_eq, getElem_zeroExtend']
theorem getElem?_setWidth' (x : BitVec w) (i : Nat) (h : w v) :
(setWidth' h x)[i]? = if i < v then some (x.getLsbD i) else none := by
simp [getElem?_eq, getElem_setWidth']
theorem getElem?_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
(x.zeroExtend m)[i]? = if i < m then some (x.getLsbD i) else none := by
simp [getElem?_eq, getElem_zeroExtend]
theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
(x.setWidth m)[i]? = if i < m then some (x.getLsbD i) else none := by
simp [getElem?_eq, getElem_setWidth]
@[simp] theorem getLsbD_zeroExtend' (ge : m n) (x : BitVec n) (i : Nat) :
getLsbD (zeroExtend' ge x) i = getLsbD x i := by
simp [getLsbD, toNat_zeroExtend']
@[simp] theorem getLsbD_setWidth' (ge : m n) (x : BitVec n) (i : Nat) :
getLsbD (setWidth' ge x) i = getLsbD x i := by
simp [getLsbD, toNat_setWidth']
@[simp] theorem getMsbD_zeroExtend' (ge : m n) (x : BitVec n) (i : Nat) :
getMsbD (zeroExtend' ge x) i = (decide (i m - n) && getMsbD x (i - (m - n))) := by
simp only [getMsbD, getLsbD_zeroExtend', gt_iff_lt]
@[simp] theorem getMsbD_setWidth' (ge : m n) (x : BitVec n) (i : Nat) :
getMsbD (setWidth' ge x) i = (decide (i m - n) && getMsbD x (i - (m - n))) := by
simp only [getMsbD, getLsbD_setWidth', gt_iff_lt]
by_cases h₁ : decide (i < m) <;> by_cases h₂ : decide (i m - n) <;> by_cases h₃ : decide (i - (m - n) < n) <;>
by_cases h₄ : n - 1 - (i - (m - n)) = m - 1 - i
all_goals
@@ -507,15 +543,15 @@ theorem getElem?_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
(try apply (getLsbD_ge _ _ _).symm) <;>
omega
@[simp] theorem getLsbD_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
getLsbD (zeroExtend m x) i = (decide (i < m) && getLsbD x i) := by
simp [getLsbD, toNat_zeroExtend, Nat.testBit_mod_two_pow]
@[simp] theorem getLsbD_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
getLsbD (setWidth m x) i = (decide (i < m) && getLsbD x i) := by
simp [getLsbD, toNat_setWidth, Nat.testBit_mod_two_pow]
@[simp] theorem getMsbD_zeroExtend_add {x : BitVec w} (h : k i) :
(x.zeroExtend (w + k)).getMsbD i = x.getMsbD (i - k) := by
@[simp] theorem getMsbD_setWidth_add {x : BitVec w} (h : k i) :
(x.setWidth (w + k)).getMsbD i = x.getMsbD (i - k) := by
by_cases h : w = 0
· subst h; simp [of_length_zero]
simp only [getMsbD, getLsbD_zeroExtend]
simp only [getMsbD, getLsbD_setWidth]
by_cases h₁ : i < w + k <;> by_cases h₂ : i - k < w <;> by_cases h₃ : w + k - 1 - i < w + k
<;> simp [h₁, h₂, h₃]
· congr 1
@@ -523,78 +559,60 @@ theorem getElem?_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
all_goals (first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge)
<;> omega
theorem getLsbD_truncate (m : Nat) (x : BitVec n) (i : Nat) :
getLsbD (truncate m x) i = (decide (i < m) && getLsbD x i) :=
getLsbD_zeroExtend m x i
theorem msb_truncate (x : BitVec w) : (x.truncate (k + 1)).msb = x.getLsbD k := by
simp [BitVec.msb, getMsbD]
@[simp] theorem cast_zeroExtend (h : v = v') (x : BitVec w) :
cast h (zeroExtend v x) = zeroExtend v' x := by
@[simp] theorem cast_setWidth (h : v = v') (x : BitVec w) :
cast h (setWidth v x) = setWidth v' x := by
subst h
ext
simp
@[simp] theorem cast_truncate (h : v = v') (x : BitVec w) :
cast h (truncate v x) = truncate v' x := by
subst h
ext
simp
@[simp] theorem zeroExtend_zeroExtend_of_le (x : BitVec w) (h : k l) :
(x.zeroExtend l).zeroExtend k = x.zeroExtend k := by
@[simp] theorem setWidth_setWidth_of_le (x : BitVec w) (h : k l) :
(x.setWidth l).setWidth k = x.setWidth k := by
ext i
simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and]
simp only [getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and]
have p := lt_of_getLsbD (x := x) (i := i)
revert p
cases getLsbD x i <;> simp; omega
@[simp] theorem truncate_truncate_of_le (x : BitVec w) (h : k l) :
(x.truncate l).truncate k = x.truncate k :=
zeroExtend_zeroExtend_of_le x h
/-- Truncating by the bitwidth has no effect. -/
-- This doesn't need to be a `@[simp]` lemma, as `zeroExtend_eq` applies.
theorem truncate_eq_self {x : BitVec w} : x.truncate w = x := zeroExtend_eq _
@[simp] theorem truncate_cast {h : w = v} : (cast h x).truncate k = x.truncate k := by
@[simp] theorem setWidth_cast {h : w = v} : (cast h x).setWidth k = x.setWidth k := by
apply eq_of_getLsbD_eq
simp
theorem msb_zeroExtend (x : BitVec w) : (x.zeroExtend v).msb = (decide (0 < v) && x.getLsbD (v - 1)) := by
theorem msb_setWidth (x : BitVec w) : (x.setWidth v).msb = (decide (0 < v) && x.getLsbD (v - 1)) := by
rw [msb_eq_getLsbD_last]
simp only [getLsbD_zeroExtend]
simp only [getLsbD_setWidth]
cases getLsbD x (v - 1) <;> simp; omega
theorem msb_zeroExtend' (x : BitVec w) (h : w v) : (x.zeroExtend' h).msb = (decide (0 < v) && x.getLsbD (v - 1)) := by
rw [zeroExtend'_eq, msb_zeroExtend]
theorem msb_setWidth' (x : BitVec w) (h : w v) : (x.setWidth' h).msb = (decide (0 < v) && x.getLsbD (v - 1)) := by
rw [setWidth'_eq, msb_setWidth]
theorem msb_setWidth'' (x : BitVec w) : (x.setWidth (k + 1)).msb = x.getLsbD k := by
simp [BitVec.msb, getMsbD]
/-- zero extending a bitvector to width 1 equals the boolean of the lsb. -/
theorem zeroExtend_one_eq_ofBool_getLsb_zero (x : BitVec w) :
x.zeroExtend 1 = BitVec.ofBool (x.getLsbD 0) := by
theorem setWidth_one_eq_ofBool_getLsb_zero (x : BitVec w) :
x.setWidth 1 = BitVec.ofBool (x.getLsbD 0) := by
ext i
simp [getLsbD_zeroExtend, Fin.fin_one_eq_zero i]
simp [getLsbD_setWidth, Fin.fin_one_eq_zero i]
/-- Zero extending `1#v` to `1#w` equals `1#w` when `v > 0`. -/
theorem zeroExtend_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
(BitVec.ofNat v 1).zeroExtend w = BitVec.ofNat w 1 := by
theorem setWidth_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
(BitVec.ofNat v 1).setWidth w = BitVec.ofNat w 1 := by
ext i, hilt
simp only [getLsbD_zeroExtend, hilt, decide_True, getLsbD_ofNat, Bool.true_and,
simp only [getLsbD_setWidth, hilt, decide_True, getLsbD_ofNat, Bool.true_and,
Bool.and_iff_right_iff_imp, decide_eq_true_eq]
intros hi₁
have hv := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi₁
omega
/-- Truncating to width 1 produces a bitvector equal to the least significant bit. -/
theorem truncate_one {x : BitVec w} :
x.truncate 1 = ofBool (x.getLsbD 0) := by
theorem setWidth_one {x : BitVec w} :
x.setWidth 1 = ofBool (x.getLsbD 0) := by
ext i
simp [show i = 0 by omega]
@[simp] theorem truncate_ofNat_of_le (h : v w) (x : Nat) : truncate v (BitVec.ofNat w x) = BitVec.ofNat v x := by
@[simp] theorem setWidth_ofNat_of_le (h : v w) (x : Nat) : setWidth v (BitVec.ofNat w x) = BitVec.ofNat v x := by
apply BitVec.eq_of_toNat_eq
simp only [toNat_truncate, toNat_ofNat]
simp only [toNat_setWidth, toNat_ofNat]
rw [Nat.mod_mod_of_dvd]
exact Nat.pow_dvd_pow_iff_le_right'.mpr h
@@ -639,6 +657,9 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
@[simp] theorem getLsbD_allOnes : (allOnes v).getLsbD i = decide (i < v) := by
simp [allOnes]
@[simp] theorem getElem_allOnes (i : Nat) (h : i < v) : (allOnes v)[i] = true := by
simp [getElem_eq_testBit_toNat, h]
@[simp] theorem ofFin_add_rev (x : Fin (2^n)) : ofFin (x + x.rev) = allOnes n := by
ext
simp only [Fin.rev, getLsbD_ofFin, getLsbD_allOnes, Fin.is_lt, decide_True]
@@ -666,11 +687,14 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
simp only [getMsbD]
by_cases h : i < w <;> simp [h]
@[simp] theorem getElem_or {x y : BitVec w} {i : Nat} (h : i < w) : (x ||| y)[i] = (x[i] || y[i]) := by
simp [getElem_eq_testBit_toNat]
@[simp] theorem msb_or {x y : BitVec w} : (x ||| y).msb = (x.msb || y.msb) := by
simp [BitVec.msb]
@[simp] theorem truncate_or {x y : BitVec w} :
(x ||| y).truncate k = x.truncate k ||| y.truncate k := by
@[simp] theorem setWidth_or {x y : BitVec w} :
(x ||| y).setWidth k = x.setWidth k ||| y.setWidth k := by
ext
simp
@@ -704,11 +728,14 @@ instance : Std.Commutative (fun (x y : BitVec w) => x ||| y) := ⟨BitVec.or_com
simp only [getMsbD]
by_cases h : i < w <;> simp [h]
@[simp] theorem getElem_and {x y : BitVec w} {i : Nat} (h : i < w) : (x &&& y)[i] = (x[i] && y[i]) := by
simp [getElem_eq_testBit_toNat]
@[simp] theorem msb_and {x y : BitVec w} : (x &&& y).msb = (x.msb && y.msb) := by
simp [BitVec.msb]
@[simp] theorem truncate_and {x y : BitVec w} :
(x &&& y).truncate k = x.truncate k &&& y.truncate k := by
@[simp] theorem setWidth_and {x y : BitVec w} :
(x &&& y).setWidth k = x.setWidth k &&& y.setWidth k := by
ext
simp
@@ -735,21 +762,24 @@ instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_co
exact (Nat.mod_eq_of_lt <| Nat.xor_lt_two_pow x.isLt y.isLt).symm
@[simp] theorem getLsbD_xor {x y : BitVec v} :
(x ^^^ y).getLsbD i = (xor (x.getLsbD i) (y.getLsbD i)) := by
(x ^^^ y).getLsbD i = ((x.getLsbD i) ^^ (y.getLsbD i)) := by
rw [ testBit_toNat, getLsbD, getLsbD]
simp
@[simp] theorem getMsbD_xor {x y : BitVec w} :
(x ^^^ y).getMsbD i = (xor (x.getMsbD i) (y.getMsbD i)) := by
(x ^^^ y).getMsbD i = (x.getMsbD i ^^ y.getMsbD i) := by
simp only [getMsbD]
by_cases h : i < w <;> simp [h]
@[simp] theorem getElem_xor {x y : BitVec w} {i : Nat} (h : i < w) : (x ^^^ y)[i] = (x[i] ^^ y[i]) := by
simp [getElem_eq_testBit_toNat]
@[simp] theorem msb_xor {x y : BitVec w} :
(x ^^^ y).msb = (xor x.msb y.msb) := by
(x ^^^ y).msb = (x.msb ^^ y.msb) := by
simp [BitVec.msb]
@[simp] theorem truncate_xor {x y : BitVec w} :
(x ^^^ y).truncate k = x.truncate k ^^^ y.truncate k := by
@[simp] theorem setWidth_xor {x y : BitVec w} :
(x ^^^ y).setWidth k = x.setWidth k ^^^ y.setWidth k := by
ext
simp
@@ -797,8 +827,14 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
@[simp] theorem getLsbD_not {x : BitVec v} : (~~~x).getLsbD i = (decide (i < v) && ! x.getLsbD i) := by
by_cases h' : i < v <;> simp_all [not_def]
@[simp] theorem truncate_not {x : BitVec w} (h : k w) :
(~~~x).truncate k = ~~~(x.truncate k) := by
@[simp] theorem getElem_not {x : BitVec w} {i : Nat} (h : i < w) : (~~~x)[i] = !x[i] := by
simp only [getElem_eq_testBit_toNat, toNat_not]
rw [ Nat.sub_add_eq, Nat.add_comm 1]
rw [Nat.testBit_two_pow_sub_succ x.isLt]
simp [h]
@[simp] theorem setWidth_not {x : BitVec w} (h : k w) :
(~~~x).setWidth k = ~~~(x.setWidth k) := by
ext
simp [h]
omega
@@ -886,9 +922,9 @@ theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) :
<;> omega
theorem shiftLeftZeroExtend_eq {x : BitVec w} :
shiftLeftZeroExtend x n = zeroExtend (w+n) x <<< n := by
shiftLeftZeroExtend x n = setWidth (w+n) x <<< n := by
apply eq_of_toNat_eq
rw [shiftLeftZeroExtend, zeroExtend]
rw [shiftLeftZeroExtend, setWidth]
split
· simp
rw [Nat.mod_eq_of_lt]
@@ -899,7 +935,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
@[simp] theorem getLsbD_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
getLsbD (shiftLeftZeroExtend x n) i = ((! decide (i < n)) && getLsbD x (i - n)) := by
rw [shiftLeftZeroExtend_eq]
simp only [getLsbD_shiftLeft, getLsbD_zeroExtend]
simp only [getLsbD_shiftLeft, getLsbD_setWidth]
cases h₁ : decide (i < n) <;> cases h₂ : decide (i - n < m + n) <;> cases h₃ : decide (i < m + n)
<;> simp_all
<;> (rw [getLsbD_ge]; omega)
@@ -953,6 +989,10 @@ theorem getLsbD_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} :
getLsbD (x >>> i) j = getLsbD x (i+j) := by
unfold getLsbD ; simp
@[simp] theorem getElem_ushiftRight (x : BitVec w) (i n : Nat) (h : i < w) :
(x >>> n)[i] = x.getLsbD (n + i) := by
simp [getElem_eq_testBit_toNat, toNat_ushiftRight, Nat.testBit_shiftRight, getLsbD]
theorem ushiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
(x ^^^ y) >>> n = (x >>> n) ^^^ (y >>> n) := by
ext
@@ -1138,15 +1178,15 @@ private theorem Int.negSucc_emod (m : Nat) (n : Int) :
-(m + 1) % n = Int.subNatNat (Int.natAbs n) ((m % Int.natAbs n) + 1) := rfl
/-- The sign extension is the same as zero extending when `msb = false`. -/
theorem signExtend_eq_not_zeroExtend_not_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
x.signExtend v = x.zeroExtend v := by
theorem signExtend_eq_not_setWidth_not_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
x.signExtend v = x.setWidth v := by
ext i
by_cases hv : i < v
· simp only [signExtend, getLsbD, getLsbD_zeroExtend, hv, decide_True, Bool.true_and, toNat_ofInt,
· simp only [signExtend, getLsbD, getLsbD_setWidth, hv, decide_True, Bool.true_and, toNat_ofInt,
BitVec.toInt_eq_msb_cond, hmsb, reduceIte, reduceCtorEq]
rw [Int.ofNat_mod_ofNat, Int.toNat_ofNat, Nat.testBit_mod_two_pow]
simp [BitVec.testBit_toNat]
· simp only [getLsbD_zeroExtend, hv, decide_False, Bool.false_and]
· simp only [getLsbD_setWidth, hv, decide_False, Bool.false_and]
apply getLsbD_ge
omega
@@ -1154,11 +1194,11 @@ theorem signExtend_eq_not_zeroExtend_not_of_msb_false {x : BitVec w} {v : Nat} (
The sign extension is a bitwise not, followed by a zero extend, followed by another bitwise not
when `msb = true`. The double bitwise not ensures that the high bits are '1',
and the lower bits are preserved. -/
theorem signExtend_eq_not_zeroExtend_not_of_msb_true {x : BitVec w} {v : Nat} (hmsb : x.msb = true) :
x.signExtend v = ~~~((~~~x).zeroExtend v) := by
theorem signExtend_eq_not_setWidth_not_of_msb_true {x : BitVec w} {v : Nat} (hmsb : x.msb = true) :
x.signExtend v = ~~~((~~~x).setWidth v) := by
apply BitVec.eq_of_toNat_eq
simp only [signExtend, BitVec.toInt_eq_msb_cond, toNat_ofInt, toNat_not,
toNat_truncate, hmsb, reduceIte]
toNat_setWidth, hmsb, reduceIte]
norm_cast
rw [Int.ofNat_sub_ofNat_of_lt, Int.negSucc_emod]
simp only [Int.natAbs_ofNat, Nat.succ_eq_add_one]
@@ -1174,27 +1214,27 @@ theorem signExtend_eq_not_zeroExtend_not_of_msb_true {x : BitVec w} {v : Nat} (h
@[simp] theorem getLsbD_signExtend (x : BitVec w) {v i : Nat} :
(x.signExtend v).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb) := by
rcases hmsb : x.msb with rfl | rfl
· rw [signExtend_eq_not_zeroExtend_not_of_msb_false hmsb]
· rw [signExtend_eq_not_setWidth_not_of_msb_false hmsb]
by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
· rw [signExtend_eq_not_zeroExtend_not_of_msb_true hmsb]
· rw [signExtend_eq_not_setWidth_not_of_msb_true hmsb]
by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
/-- Sign extending to a width smaller than the starting width is a truncation. -/
theorem signExtend_eq_truncate_of_lt (x : BitVec w) {v : Nat} (hv : v w):
x.signExtend v = x.truncate v := by
theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v w):
x.signExtend v = x.setWidth v := by
ext i
simp only [getLsbD_signExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_zeroExtend,
simp only [getLsbD_signExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_setWidth,
ite_eq_left_iff, Nat.not_lt]
omega
/-- Sign extending to the same bitwidth is a no op. -/
theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by
rw [signExtend_eq_truncate_of_lt _ (Nat.le_refl _), truncate_eq]
rw [signExtend_eq_setWidth_of_lt _ (Nat.le_refl _), setWidth_eq]
/-! ### append -/
theorem append_def (x : BitVec v) (y : BitVec w) :
x ++ y = (shiftLeftZeroExtend x w ||| zeroExtend' (Nat.le_add_left w v) y) := rfl
x ++ y = (shiftLeftZeroExtend x w ||| setWidth' (Nat.le_add_left w v) y) := rfl
@[simp] theorem toNat_append (x : BitVec m) (y : BitVec n) :
(x ++ y).toNat = x.toNat <<< n ||| y.toNat :=
@@ -1202,7 +1242,7 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
@[simp] theorem getLsbD_append {x : BitVec n} {y : BitVec m} :
getLsbD (x ++ y) i = bif i < m then getLsbD y i else getLsbD x (i - m) := by
simp only [append_def, getLsbD_or, getLsbD_shiftLeftZeroExtend, getLsbD_zeroExtend']
simp only [append_def, getLsbD_or, getLsbD_shiftLeftZeroExtend, getLsbD_setWidth']
by_cases h : i < m
· simp [h]
· simp [h]; simp_all
@@ -1217,7 +1257,7 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
theorem msb_append {x : BitVec w} {y : BitVec v} :
(x ++ y).msb = bif (w == 0) then (y.msb) else (x.msb) := by
rw [ append_eq, append]
simp [msb_zeroExtend']
simp [msb_setWidth']
by_cases h : w = 0
· subst h
simp [BitVec.msb, getMsbD]
@@ -1252,11 +1292,11 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
ext
simp
theorem truncate_append {x : BitVec w} {y : BitVec v} :
(x ++ y).truncate k = if h : k v then y.truncate k else (x.truncate (k - v) ++ y).cast (by omega) := by
theorem setWidth_append {x : BitVec w} {y : BitVec v} :
(x ++ y).setWidth k = if h : k v then y.setWidth k else (x.setWidth (k - v) ++ y).cast (by omega) := by
apply eq_of_getLsbD_eq
intro i
simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, getLsbD_append, Bool.true_and]
simp only [getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_append, Bool.true_and]
split
· have t : i < v := by omega
simp [t]
@@ -1265,11 +1305,11 @@ theorem truncate_append {x : BitVec w} {y : BitVec v} :
· have t' : i - v < k - v := by omega
simp [t, t']
@[simp] theorem truncate_append_of_eq {x : BitVec v} {y : BitVec w} (h : w' = w) : truncate (v' + w') (x ++ y) = truncate v' x ++ truncate w' y := by
@[simp] theorem setWidth_append_of_eq {x : BitVec v} {y : BitVec w} (h : w' = w) : setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y := by
subst h
ext i
simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, getLsbD_append, cond_eq_if,
decide_eq_true_eq, Bool.true_and, zeroExtend_eq]
simp only [getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_append, cond_eq_if,
decide_eq_true_eq, Bool.true_and, setWidth_eq]
split
· simp_all
· simp_all only [Bool.iff_and_self, decide_eq_true_eq]
@@ -1277,8 +1317,8 @@ theorem truncate_append {x : BitVec w} {y : BitVec v} :
have := BitVec.lt_of_getLsbD h
omega
@[simp] theorem truncate_cons {x : BitVec w} : (cons a x).truncate w = x := by
simp [cons, truncate_append]
@[simp] theorem setWidth_cons {x : BitVec w} : (cons a x).setWidth w = x := by
simp [cons, setWidth_append]
@[simp] theorem not_append {x : BitVec w} {y : BitVec v} : ~~~ (x ++ y) = (~~~ x) ++ (~~~ y) := by
ext i
@@ -1365,18 +1405,18 @@ theorem toNat_cons' {x : BitVec w} :
@[simp] theorem getMsbD_cons_succ : (cons a x).getMsbD (i + 1) = x.getMsbD i := by
simp [cons, Nat.le_add_left 1 i]
theorem truncate_succ (x : BitVec w) :
truncate (i+1) x = cons (getLsbD x i) (truncate i x) := by
theorem setWidth_succ (x : BitVec w) :
setWidth (i+1) x = cons (getLsbD x i) (setWidth i x) := by
apply eq_of_getLsbD_eq
intro j
simp only [getLsbD_truncate, getLsbD_cons, j.isLt, decide_True, Bool.true_and]
simp only [getLsbD_setWidth, getLsbD_cons, j.isLt, decide_True, Bool.true_and]
if j_eq : j.val = i then
simp [j_eq]
else
have j_lt : j.val < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ j.isLt) j_eq
simp [j_eq, j_lt]
theorem eq_msb_cons_truncate (x : BitVec (w+1)) : x = (cons x.msb (x.truncate w)) := by
theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
ext i
simp
split <;> rename_i h
@@ -1390,15 +1430,18 @@ theorem eq_msb_cons_truncate (x : BitVec (w+1)) : x = (cons x.msb (x.truncate w)
@[simp] theorem cons_or_cons (x y : BitVec w) (a b : Bool) :
(cons a x) ||| (cons b y) = cons (a || b) (x ||| y) := by
ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
ext i
simp [cons]
@[simp] theorem cons_and_cons (x y : BitVec w) (a b : Bool) :
(cons a x) &&& (cons b y) = cons (a && b) (x &&& y) := by
ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
ext i
simp [cons]
@[simp] theorem cons_xor_cons (x y : BitVec w) (a b : Bool) :
(cons a x) ^^^ (cons b y) = cons (xor a b) (x ^^^ y) := by
ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
(cons a x) ^^^ (cons b y) = cons (a ^^ b) (x ^^^ y) := by
ext i
simp [cons]
/-! ### concat -/
@@ -1436,7 +1479,7 @@ theorem getLsbD_concat (x : BitVec w) (b : Bool) (i : Nat) :
ext i; cases i using Fin.succRecOn <;> simp
@[simp] theorem concat_xor_concat (x y : BitVec w) (a b : Bool) :
(concat x a) ^^^ (concat y b) = concat (x ^^^ y) (xor a b) := by
(concat x a) ^^^ (concat y b) = concat (x ^^^ y) (a ^^ b) := by
ext i; cases i using Fin.succRecOn <;> simp
/-! ### add -/
@@ -1454,7 +1497,8 @@ Definition of bitvector addition as a nat.
x + .ofFin y = .ofFin (x.toFin + y) := rfl
theorem ofNat_add {n} (x y : Nat) : BitVec.ofNat n (x + y) = BitVec.ofNat n x + BitVec.ofNat n y := by
apply eq_of_toNat_eq ; simp [BitVec.ofNat]
apply eq_of_toNat_eq
simp [BitVec.ofNat, Fin.ofNat'_add]
theorem ofNat_add_ofNat {n} (x y : Nat) : BitVec.ofNat n x + BitVec.ofNat n y = BitVec.ofNat n (x + y) :=
(ofNat_add x y).symm
@@ -1474,8 +1518,8 @@ instance : Std.LawfulIdentity (α := BitVec n) (· + ·) 0#n where
left_id := BitVec.zero_add
right_id := BitVec.add_zero
theorem truncate_add (x y : BitVec w) (h : i w) :
(x + y).truncate i = x.truncate i + y.truncate i := by
theorem setWidth_add (x y : BitVec w) (h : i w) :
(x + y).setWidth i = x.setWidth i + y.setWidth i := by
have dvd : 2^i 2^w := Nat.pow_dvd_pow _ h
simp [bv_toNat, h, Nat.mod_mod_of_dvd _ dvd]
@@ -1508,10 +1552,12 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN
rfl
@[simp] theorem sub_ofFin (x : BitVec n) (y : Fin (2^n)) : x - .ofFin y = .ofFin (x.toFin - y) :=
rfl
-- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
-- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea.
theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y = .ofNat n ((2^n - y % 2^n) + x) := by
apply eq_of_toNat_eq ; simp [BitVec.ofNat]
apply eq_of_toNat_eq
simp [BitVec.ofNat, Fin.ofNat'_sub]
@[simp] protected theorem sub_zero (x : BitVec n) : x - 0#n = x := by apply eq_of_toNat_eq ; simp
@@ -1646,7 +1692,7 @@ theorem ofInt_mul {n} (x y : Int) : BitVec.ofInt n (x * y) =
x < BitVec.ofFin y x.toFin < y := Iff.rfl
@[simp] theorem ofFin_lt {x : Fin (2^n)} {y : BitVec n} :
BitVec.ofFin x < y x < y.toFin := Iff.rfl
@[simp] theorem ofNat_lt_ofNat {n} (x y : Nat) : BitVec.ofNat n x < BitVec.ofNat n y x % 2^n < y % 2^n := by
@[simp] theorem ofNat_lt_ofNat {n} {x y : Nat} : BitVec.ofNat n x < BitVec.ofNat n y x % 2^n < y % 2^n := by
simp [lt_def]
@[simp] protected theorem not_le {x y : BitVec n} : ¬ x y y < x := by
@@ -1931,18 +1977,18 @@ theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by
theorem getLsbD_one {w i : Nat} : (1#w).getLsbD i = (decide (0 < w) && decide (0 = i)) := by
rw [ twoPow_zero, getLsbD_twoPow]
/- ### zeroExtend, truncate, and bitwise operations -/
/- ### setWidth, setWidth, and bitwise operations -/
/--
When the `(i+1)`th bit of `x` is false,
keeping the lower `(i + 1)` bits of `x` equals keeping the lower `i` bits.
-/
theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false
theorem setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false
{x : BitVec w} {i : Nat} (hx : x.getLsbD i = false) :
zeroExtend w (x.truncate (i + 1)) =
zeroExtend w (x.truncate i) := by
setWidth w (x.setWidth (i + 1)) =
setWidth w (x.setWidth i) := by
ext k
simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
simp only [getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
by_cases hik : i = k
· subst hik
simp [hx]
@@ -1953,22 +1999,22 @@ When the `(i+1)`th bit of `x` is true,
keeping the lower `(i + 1)` bits of `x` equalsk eeping the lower `i` bits
and then performing bitwise-or with `twoPow i = (1 << i)`,
-/
theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true
theorem setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true
{x : BitVec w} {i : Nat} (hx : x.getLsbD i = true) :
zeroExtend w (x.truncate (i + 1)) =
zeroExtend w (x.truncate i) ||| (twoPow w i) := by
setWidth w (x.setWidth (i + 1)) =
setWidth w (x.setWidth i) ||| (twoPow w i) := by
ext k
simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
simp only [getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
by_cases hik : i = k
· subst hik
simp [hx]
· by_cases hik' : k < i + 1 <;> simp [hik, hik'] <;> omega
/-- Bitwise and of `(x : BitVec w)` with `1#w` equals zero extending `x.lsb` to `w`. -/
theorem and_one_eq_zeroExtend_ofBool_getLsbD {x : BitVec w} :
(x &&& 1#w) = zeroExtend w (ofBool (x.getLsbD 0)) := by
theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
(x &&& 1#w) = setWidth w (ofBool (x.getLsbD 0)) := by
ext i
simp only [getLsbD_and, getLsbD_one, getLsbD_zeroExtend, Fin.is_lt, decide_True, getLsbD_ofBool,
simp only [getLsbD_and, getLsbD_one, getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_ofBool,
Bool.true_and]
by_cases h : (0 = (i : Nat)) <;> simp [h] <;> omega
@@ -2080,4 +2126,143 @@ theorem toNat_sub_of_le {x y : BitVec n} (h : y ≤ x) :
· have : 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat) := by omega
rw [this, Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)]
/-! ### Deprecations -/
set_option linter.missingDocs false
@[deprecated truncate_eq_setWidth (since := "2024-09-18")]
abbrev truncate_eq_zeroExtend := @truncate_eq_setWidth
@[deprecated toNat_setWidth' (since := "2024-09-18")]
abbrev toNat_zeroExtend' := @toNat_setWidth'
@[deprecated toNat_setWidth (since := "2024-09-18")]
abbrev toNat_zeroExtend := @toNat_setWidth
@[deprecated toNat_setWidth (since := "2024-09-18")]
abbrev toNat_truncate := @toNat_setWidth
@[deprecated setWidth_eq (since := "2024-09-18")]
abbrev zeroExtend_eq := @setWidth_eq
@[deprecated setWidth_eq (since := "2024-09-18")]
abbrev truncate_eq := @setWidth_eq
@[deprecated setWidth_zero (since := "2024-09-18")]
abbrev zeroExtend_zero := @setWidth_zero
@[deprecated getElem_setWidth (since := "2024-09-18")]
abbrev getElem_zeroExtend := @getElem_setWidth
@[deprecated getElem_setWidth' (since := "2024-09-18")]
abbrev getElem_zeroExtend' := @getElem_setWidth'
@[deprecated getElem?_setWidth (since := "2024-09-18")]
abbrev getElem?_zeroExtend := @getElem?_setWidth
@[deprecated getElem?_setWidth' (since := "2024-09-18")]
abbrev getElem?_zeroExtend' := @getElem?_setWidth'
@[deprecated getLsbD_setWidth (since := "2024-09-18")]
abbrev getLsbD_zeroExtend := @getLsbD_setWidth
@[deprecated getLsbD_setWidth' (since := "2024-09-18")]
abbrev getLsbD_zeroExtend' := @getLsbD_setWidth'
@[deprecated getMsbD_setWidth_add (since := "2024-09-18")]
abbrev getMsbD_zeroExtend_add := @getMsbD_setWidth_add
@[deprecated getMsbD_setWidth' (since := "2024-09-18")]
abbrev getMsbD_zeroExtend' := @getMsbD_setWidth'
@[deprecated getElem_setWidth (since := "2024-09-18")]
abbrev getElem_truncate := @getElem_setWidth
@[deprecated getElem?_setWidth (since := "2024-09-18")]
abbrev getElem?_truncate := @getElem?_setWidth
@[deprecated getLsbD_setWidth (since := "2024-09-18")]
abbrev getLsbD_truncate := @getLsbD_setWidth
@[deprecated msb_setWidth (since := "2024-09-18")]
abbrev msb_truncate := @msb_setWidth
@[deprecated cast_setWidth (since := "2024-09-18")]
abbrev cast_zeroExtend := @cast_setWidth
@[deprecated cast_setWidth (since := "2024-09-18")]
abbrev cast_truncate := @cast_setWidth
@[deprecated setWidth_setWidth_of_le (since := "2024-09-18")]
abbrev zeroExtend_zeroExtend_of_le := @setWidth_setWidth_of_le
@[deprecated setWidth_eq (since := "2024-09-18")]
abbrev truncate_eq_self := @setWidth_eq
@[deprecated setWidth_cast (since := "2024-09-18")]
abbrev truncate_cast := @setWidth_cast
@[deprecated msb_setWidth (since := "2024-09-18")]
abbrev mbs_zeroExtend := @msb_setWidth
@[deprecated msb_setWidth' (since := "2024-09-18")]
abbrev mbs_zeroExtend' := @msb_setWidth'
@[deprecated setWidth_one_eq_ofBool_getLsb_zero (since := "2024-09-18")]
abbrev zeroExtend_one_eq_ofBool_getLsb_zero := @setWidth_one_eq_ofBool_getLsb_zero
@[deprecated setWidth_ofNat_one_eq_ofNat_one_of_lt (since := "2024-09-18")]
abbrev zeroExtend_ofNat_one_eq_ofNat_one_of_lt := @setWidth_ofNat_one_eq_ofNat_one_of_lt
@[deprecated setWidth_one (since := "2024-09-18")]
abbrev truncate_one := @setWidth_one
@[deprecated setWidth_ofNat_of_le (since := "2024-09-18")]
abbrev truncate_ofNat_of_le := @setWidth_ofNat_of_le
@[deprecated setWidth_or (since := "2024-09-18")]
abbrev truncate_or := @setWidth_or
@[deprecated setWidth_and (since := "2024-09-18")]
abbrev truncate_and := @setWidth_and
@[deprecated setWidth_xor (since := "2024-09-18")]
abbrev truncate_xor := @setWidth_xor
@[deprecated setWidth_not (since := "2024-09-18")]
abbrev truncate_not := @setWidth_not
@[deprecated signExtend_eq_not_setWidth_not_of_msb_false (since := "2024-09-18")]
abbrev signExtend_eq_not_zeroExtend_not_of_msb_false := @signExtend_eq_not_setWidth_not_of_msb_false
@[deprecated signExtend_eq_not_setWidth_not_of_msb_true (since := "2024-09-18")]
abbrev signExtend_eq_not_zeroExtend_not_of_msb_true := @signExtend_eq_not_setWidth_not_of_msb_true
@[deprecated signExtend_eq_setWidth_of_lt (since := "2024-09-18")]
abbrev signExtend_eq_truncate_of_lt := @signExtend_eq_setWidth_of_lt
@[deprecated truncate_append (since := "2024-09-18")]
abbrev truncate_append := @setWidth_append
@[deprecated truncate_append_of_eq (since := "2024-09-18")]
abbrev truncate_append_of_eq := @setWidth_append_of_eq
@[deprecated truncate_cons (since := "2024-09-18")]
abbrev truncate_cons := @setWidth_cons
@[deprecated truncate_succ (since := "2024-09-18")]
abbrev truncate_succ := @setWidth_succ
@[deprecated truncate_add (since := "2024-09-18")]
abbrev truncate_add := @setWidth_add
@[deprecated setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false (since := "2024-09-18")]
abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false := @setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false
@[deprecated setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true (since := "2024-09-18")]
abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true := @setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true
@[deprecated and_one_eq_setWidth_ofBool_getLsbD (since := "2024-09-18")]
abbrev and_one_eq_zeroExtend_ofBool_getLsbD := @and_one_eq_setWidth_ofBool_getLsbD
end BitVec

View File

@@ -12,6 +12,8 @@ namespace Bool
/-- Boolean exclusive or -/
abbrev xor : Bool Bool Bool := bne
@[inherit_doc] infixl:33 " ^^ " => xor
instance (p : Bool Prop) [inst : DecidablePred p] : Decidable ( x, p x) :=
match inst true, inst false with
| isFalse ht, _ => isFalse fun h => absurd (h _) ht
@@ -145,8 +147,8 @@ theorem and_or_distrib_right : ∀ (x y z : Bool), ((x || y) && z) = (x && z ||
theorem or_and_distrib_left : (x y z : Bool), (x || y && z) = ((x || y) && (x || z)) := by decide
theorem or_and_distrib_right : (x y z : Bool), (x && y || z) = ((x || z) && (y || z)) := by decide
theorem and_xor_distrib_left : (x y z : Bool), (x && xor y z) = xor (x && y) (x && z) := by decide
theorem and_xor_distrib_right : (x y z : Bool), (xor x y && z) = xor (x && z) (y && z) := by decide
theorem and_xor_distrib_left : (x y z : Bool), (x && (y ^^ z)) = ((x && y) ^^ (x && z)) := by decide
theorem and_xor_distrib_right : (x y z : Bool), ((x ^^ y) && z) = ((x && z) ^^ (y && z)) := by decide
/-- De Morgan's law for boolean and -/
@[simp] theorem not_and : (x y : Bool), (!(x && y)) = (!x || !y) := by decide
@@ -252,15 +254,6 @@ theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
theorem eq_not : {a b : Bool}, (a = (!b)) (a b) := by decide
theorem not_eq : {a b : Bool}, ((!a) = b) (a b) := by decide
@[simp] theorem not_eq_not : {a b : Bool}, ¬a = !b a = b := by decide
@[simp] theorem not_not_eq : {a b : Bool}, ¬(!a) = b a = b := by decide
/--
We move `!` from the left hand side of an equality to the right hand side.
This helps confluence, and also helps combining pairs of `!`s.
-/
@[simp] theorem not_eq_eq_eq_not : {a b : Bool}, ((!a) = b) (a = !b) := by decide
@[simp] theorem coe_iff_coe : {a b : Bool}, (a b) a = b := by decide
@[simp] theorem coe_true_iff_false : {a b : Bool}, (a b = false) a = (!b) := by decide
@@ -274,37 +267,37 @@ theorem beq_comm {α} [BEq α] [LawfulBEq α] {a b : α} : (a == b) = (b == a) :
/-! ### xor -/
theorem false_xor : (x : Bool), xor false x = x := false_bne
theorem false_xor : (x : Bool), (false ^^ x) = x := false_bne
theorem xor_false : (x : Bool), xor x false = x := bne_false
theorem xor_false : (x : Bool), (x ^^ false) = x := bne_false
theorem true_xor : (x : Bool), xor true x = !x := true_bne
theorem true_xor : (x : Bool), (true ^^ x) = !x := true_bne
theorem xor_true : (x : Bool), xor x true = !x := bne_true
theorem xor_true : (x : Bool), (x ^^ true) = !x := bne_true
theorem not_xor_self : (x : Bool), xor (!x) x = true := not_bne_self
theorem not_xor_self : (x : Bool), (!x ^^ x) = true := not_bne_self
theorem xor_not_self : (x : Bool), xor x (!x) = true := bne_not_self
theorem xor_not_self : (x : Bool), (x ^^ !x) = true := bne_not_self
theorem not_xor : (x y : Bool), xor (!x) y = !(xor x y) := by decide
theorem not_xor : (x y : Bool), (!x ^^ y) = !(x ^^ y) := by decide
theorem xor_not : (x y : Bool), xor x (!y) = !(xor x y) := by decide
theorem xor_not : (x y : Bool), (x ^^ !y) = !(x ^^ y) := by decide
theorem not_xor_not : (x y : Bool), xor (!x) (!y) = (xor x y) := not_bne_not
theorem not_xor_not : (x y : Bool), (!x ^^ !y) = (x ^^ y) := not_bne_not
theorem xor_self : (x : Bool), xor x x = false := by decide
theorem xor_self : (x : Bool), (x ^^ x) = false := by decide
theorem xor_comm : (x y : Bool), xor x y = xor y x := by decide
theorem xor_comm : (x y : Bool), (x ^^ y) = (y ^^ x) := by decide
theorem xor_left_comm : (x y z : Bool), xor x (xor y z) = xor y (xor x z) := by decide
theorem xor_left_comm : (x y z : Bool), (x ^^ (y ^^ z)) = (y ^^ (x ^^ z)) := by decide
theorem xor_right_comm : (x y z : Bool), xor (xor x y) z = xor (xor x z) y := by decide
theorem xor_right_comm : (x y z : Bool), ((x ^^ y) ^^ z) = ((x ^^ z) ^^ y) := by decide
theorem xor_assoc : (x y z : Bool), xor (xor x y) z = xor x (xor y z) := bne_assoc
theorem xor_assoc : (x y z : Bool), ((x ^^ y) ^^ z) = (x ^^ (y ^^ z)) := bne_assoc
theorem xor_left_inj : {x y z : Bool}, xor x y = xor x z y = z := bne_left_inj
theorem xor_left_inj : {x y z : Bool}, (x ^^ y) = (x ^^ z) y = z := bne_left_inj
theorem xor_right_inj : {x y z : Bool}, xor x z = xor y z x = y := bne_right_inj
theorem xor_right_inj : {x y z : Bool}, (x ^^ z) = (y ^^ z) x = y := bne_right_inj
/-! ### le/lt -/

View File

@@ -54,7 +54,12 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
@[simp] theorem val_ofNat' (n : Nat) [NeZero n] (a : Nat) :
(Fin.ofNat' n a).val = a % n := rfl
@[simp] theorem ofNat'_val_eq_self [NeZero n](x : Fin n) : (Fin.ofNat' n x) = x := by
@[simp] theorem ofNat'_self {n : Nat} [NeZero n] : Fin.ofNat' n n = 0 := by
ext
simp
congr
@[simp] theorem ofNat'_val_eq_self [NeZero n] (x : Fin n) : (Fin.ofNat' n x) = x := by
ext
rw [val_ofNat', Nat.mod_eq_of_lt]
exact x.2
@@ -68,6 +73,9 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
@[simp] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
rfl
@[simp] theorem val_eq_zero (a : Fin 1) : a.val = 0 :=
Nat.eq_zero_of_le_zero <| Nat.le_of_lt_succ a.isLt
theorem ite_val {n : Nat} {c : Prop} [Decidable c] {x : c Fin n} (y : ¬c Fin n) :
(if h : c then x h else y h).val = if h : c then (x h).val else (y h).val := by
by_cases c <;> simp [*]
@@ -120,7 +128,7 @@ theorem mk_le_of_le_val {b : Fin n} {a : Nat} (h : a ≤ b) :
@[simp] theorem mk_lt_mk {x y : Nat} {hx hy} : (x, hx : Fin n) < y, hy x < y := .rfl
@[simp] theorem val_zero (n : Nat) : (0 : Fin (n + 1)).1 = 0 := rfl
@[simp] theorem val_zero (n : Nat) [NeZero n] : ((0 : Fin n) : Nat) = 0 := rfl
@[simp] theorem mk_zero : (0, Nat.succ_pos n : Fin (n + 1)) = 0 := rfl
@@ -167,8 +175,24 @@ theorem rev_eq {n a : Nat} (i : Fin (n + 1)) (h : n = a + i) :
@[simp] theorem rev_lt_rev {i j : Fin n} : rev i < rev j j < i := by
rw [ Fin.not_le, Fin.not_le, rev_le_rev]
/-! ### last -/
@[simp] theorem val_last (n : Nat) : last n = n := rfl
@[simp] theorem last_zero : (Fin.last 0 : Fin 1) = 0 := by
ext
simp
@[simp] theorem zero_eq_last_iff {n : Nat} : (0 : Fin (n + 1)) = last n n = 0 := by
constructor
· intro h
simp_all [Fin.ext_iff]
· rintro rfl
simp
@[simp] theorem last_eq_zero_iff {n : Nat} : Fin.last n = 0 n = 0 := by
simp [eq_comm (a := Fin.last n)]
theorem le_last (i : Fin (n + 1)) : i last n := Nat.le_of_lt_succ i.is_lt
theorem last_pos : (0 : Fin (n + 2)) < last (n + 1) := Nat.succ_pos _
@@ -202,10 +226,28 @@ instance subsingleton_one : Subsingleton (Fin 1) := subsingleton_iff_le_one.2 (b
theorem fin_one_eq_zero (a : Fin 1) : a = 0 := Subsingleton.elim a 0
@[simp] theorem zero_eq_one_iff {n : Nat} [NeZero n] : (0 : Fin n) = 1 n = 1 := by
constructor
· intro h
simp [Fin.ext_iff] at h
change 0 % n = 1 % n at h
rw [eq_comm] at h
simpa using h
· rintro rfl
simp
@[simp] theorem one_eq_zero_iff {n : Nat} [NeZero n] : (1 : Fin n) = 0 n = 1 := by
rw [eq_comm]
simp
theorem add_def (a b : Fin n) : a + b = Fin.mk ((a + b) % n) (Nat.mod_lt _ a.size_pos) := rfl
theorem val_add (a b : Fin n) : (a + b).val = (a.val + b.val) % n := rfl
@[simp] protected theorem zero_add {n : Nat} [NeZero n] (i : Fin n) : (0 : Fin n) + i = i := by
ext
simp [Fin.add_def, Nat.mod_eq_of_lt i.2]
theorem val_add_one_of_lt {n : Nat} {i : Fin n.succ} (h : i < last _) : (i + 1).1 = i + 1 := by
match n with
| 0 => cases h
@@ -329,6 +371,10 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
@[simp] theorem cast_mk (h : n = m) (i : Nat) (hn : i < n) : cast h i, hn = i, h hn := rfl
@[simp] theorem cast_refl (n : Nat) (h : n = n) : cast h = id := by
ext
simp
@[simp] theorem cast_trans {k : Nat} (h : n = m) (h' : m = k) {i : Fin n} :
cast h' (cast h i) = cast (Eq.trans h h') i := rfl
@@ -437,6 +483,10 @@ theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = castSucc i.succ
@[simp] theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
@[simp] theorem addNat_zero (n : Nat) (i : Fin n) : addNat i 0 = i := by
ext
simp
@[simp] theorem addNat_one {i : Fin n} : addNat i 1 = i.succ := rfl
theorem le_coe_addNat (m : Nat) (i : Fin n) : m addNat i m :=
@@ -466,7 +516,7 @@ theorem cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
theorem le_coe_natAdd (m : Nat) (i : Fin n) : m natAdd m i := Nat.le_add_right ..
theorem natAdd_zero {n : Nat} : natAdd 0 = cast (Nat.zero_add n).symm := by ext; simp
@[simp] theorem natAdd_zero {n : Nat} : natAdd 0 = cast (Nat.zero_add n).symm := by ext; simp
/-- For rewriting in the reverse direction, see `Fin.cast_natAdd_right`. -/
theorem natAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
@@ -504,9 +554,19 @@ theorem cast_addNat {n : Nat} (m : Nat) (i : Fin n) :
@[simp] theorem natAdd_last {m n : Nat} : natAdd n (last m) = last (n + m) := rfl
@[simp] theorem addNat_last (n : Nat) :
addNat (last n) m = cast (by omega) (last (n + m)) := by
ext
simp
theorem natAdd_castSucc {m n : Nat} {i : Fin m} : natAdd n (castSucc i) = castSucc (natAdd n i) :=
rfl
@[simp] theorem natAdd_eq_addNat (n : Nat) (i : Fin n) : Fin.natAdd n i = i.addNat n := by
ext
simp
omega
theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := Fin.ext <| by
rw [val_rev, coe_castAdd, coe_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]
@@ -572,6 +632,15 @@ theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
@[simp] theorem subNat_mk {i : Nat} (h₁ : i < n + m) (h₂ : m i) :
subNat m i, h₁ h₂ = i - m, Nat.sub_lt_right_of_lt_add h₂ h₁ := rfl
@[simp] theorem subNat_zero (i : Fin n) (h : 0 (i : Nat)): Fin.subNat 0 i h = i := by
ext
simp
@[simp] theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 i) : (subNat 1 i h).succ = i := by
ext
simp
omega
@[simp] theorem pred_castSucc_succ (i : Fin n) :
pred (castSucc i.succ) (Fin.ne_of_gt (castSucc_pos i.succ_pos)) = castSucc i := rfl
@@ -582,7 +651,7 @@ theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
subNat m (addNat i m) h = i := Fin.ext <| Nat.add_sub_cancel i m
@[simp] theorem natAdd_subNat_cast {i : Fin (n + m)} (h : n i) :
natAdd n (subNat n (cast (Nat.add_comm ..) i) h) = i := by simp [ cast_addNat]; rfl
natAdd n (subNat n (cast (Nat.add_comm ..) i) h) = i := by simp [ cast_addNat]
/-! ### recursion and induction principles -/
@@ -750,12 +819,12 @@ theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right
/-! ### add -/
@[simp] theorem ofNat'_add [NeZero n] (x : Nat) (y : Fin n) :
theorem ofNat'_add [NeZero n] (x : Nat) (y : Fin n) :
Fin.ofNat' n x + y = Fin.ofNat' n (x + y.val) := by
apply Fin.eq_of_val_eq
simp [Fin.ofNat', Fin.add_def]
@[simp] theorem add_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
theorem add_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
x + Fin.ofNat' n y = Fin.ofNat' n (x.val + y) := by
apply Fin.eq_of_val_eq
simp [Fin.ofNat', Fin.add_def]
@@ -765,16 +834,21 @@ theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right
protected theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : Nat) = ((n - b) + a) % n := by
cases a; cases b; rfl
@[simp] theorem ofNat'_sub [NeZero n] (x : Nat) (y : Fin n) :
theorem ofNat'_sub [NeZero n] (x : Nat) (y : Fin n) :
Fin.ofNat' n x - y = Fin.ofNat' n ((n - y.val) + x) := by
apply Fin.eq_of_val_eq
simp [Fin.ofNat', Fin.sub_def]
@[simp] theorem sub_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
theorem sub_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
x - Fin.ofNat' n y = Fin.ofNat' n ((n - y % n) + x.val) := by
apply Fin.eq_of_val_eq
simp [Fin.ofNat', Fin.sub_def]
@[simp] protected theorem sub_self [NeZero n] {x : Fin n} : x - x = 0 := by
ext
rw [Fin.sub_def]
simp
private theorem _root_.Nat.mod_eq_sub_of_lt_two_mul {x n} (h₁ : n x) (h₂ : x < 2 * n) :
x % n = x - n := by
rw [Nat.mod_eq, if_pos (by omega), Nat.mod_eq_of_lt (by omega)]

View File

@@ -130,24 +130,6 @@ theorem attachWith_map_subtype_val {p : α → Prop} (l : List α) (H : ∀ a
(l.attachWith p H).map Subtype.val = l :=
(attachWith_map_coe _ _ _).trans (List.map_id _)
theorem countP_attach (l : List α) (p : α Bool) :
l.attach.countP (fun a : {x // x l} => p a) = l.countP p := by
simp only [ Function.comp_apply (g := Subtype.val), countP_map, attach_map_subtype_val]
theorem countP_attachWith {p : α Prop} (l : List α) (H : a l, p a) (q : α Bool) :
(l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by
simp only [ Function.comp_apply (g := Subtype.val), countP_map, attachWith_map_subtype_val]
@[simp]
theorem count_attach [DecidableEq α] (l : List α) (a : {x // x l}) :
l.attach.count a = l.count a :=
Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _
@[simp]
theorem count_attachWith [DecidableEq α] {p : α Prop} (l : List α) (H : a l, p a) (a : {x // p x}) :
(l.attachWith p H).count a = l.count a :=
Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attachWith _ _ _
@[simp]
theorem mem_attach (l : List α) : x, x l.attach
| a, h => by
@@ -312,6 +294,60 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
| nil => simp at h
| cons x xs => simp [head_attach, h]
@[simp] theorem tail_pmap {P : α Prop} (f : (a : α) P a β) (xs : List α)
(H : (a : α), a xs P a) :
(xs.pmap f H).tail = xs.tail.pmap f (fun a h => H a (mem_of_mem_tail h)) := by
cases xs <;> simp
@[simp] theorem tail_attachWith {P : α Prop} {xs : List α}
{H : (a : α), a xs P a} :
(xs.attachWith P H).tail = xs.tail.attachWith P (fun a h => H a (mem_of_mem_tail h)) := by
cases xs <;> simp
@[simp] theorem tail_attach (xs : List α) :
xs.attach.tail = xs.tail.attach.map (fun x, h => x, mem_of_mem_tail h) := by
cases xs <;> simp
theorem foldl_pmap (l : List α) {P : α Prop} (f : (a : α) P a β)
(H : (a : α), a l P a) (g : γ β γ) (x : γ) :
(l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
rw [pmap_eq_map_attach, foldl_map]
theorem foldr_pmap (l : List α) {P : α Prop} (f : (a : α) P a β)
(H : (a : α), a l P a) (g : β γ γ) (x : γ) :
(l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
rw [pmap_eq_map_attach, foldr_map]
/--
If we fold over `l.attach` with a function that ignores the membership predicate,
we get the same results as folding over `l` directly.
This is useful when we need to use `attach` to show termination.
Unfortunately this can't be applied by `simp` because of the higher order unification problem,
and even when rewriting we need to specify the function explicitly.
-/
theorem foldl_attach (l : List α) (f : β α β) (b : β) :
l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
induction l generalizing b with
| nil => simp
| cons a l ih => rw [foldl_cons, attach_cons, foldl_cons, foldl_map, ih]
/--
If we fold over `l.attach` with a function that ignores the membership predicate,
we get the same results as folding over `l` directly.
This is useful when we need to use `attach` to show termination.
Unfortunately this can't be applied by `simp` because of the higher order unification problem,
and even when rewriting we need to specify the function explicitly.
-/
theorem foldr_attach (l : List α) (f : α β β) (b : β) :
l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
induction l generalizing b with
| nil => simp
| cons a l ih => rw [foldr_cons, attach_cons, foldr_cons, foldr_map, ih]
theorem attach_map {l : List α} (f : α β) :
(l.map f).attach = l.attach.map (fun x, h => f x, mem_map_of_mem f h) := by
induction l <;> simp [*]
@@ -492,4 +528,24 @@ theorem getLast_attach {xs : List α} (h : xs.attach ≠ []) :
xs.attach.getLast h = xs.getLast (by simpa using h), getLast_mem (by simpa using h) := by
simp only [getLast_eq_head_reverse, reverse_attach, head_map, head_attach]
@[simp]
theorem countP_attach (l : List α) (p : α Bool) :
l.attach.countP (fun a : {x // x l} => p a) = l.countP p := by
simp only [ Function.comp_apply (g := Subtype.val), countP_map, attach_map_subtype_val]
@[simp]
theorem countP_attachWith {p : α Prop} (l : List α) (H : a l, p a) (q : α Bool) :
(l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by
simp only [ Function.comp_apply (g := Subtype.val), countP_map, attachWith_map_subtype_val]
@[simp]
theorem count_attach [DecidableEq α] (l : List α) (a : {x // x l}) :
l.attach.count a = l.count a :=
Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _
@[simp]
theorem count_attachWith [DecidableEq α] {p : α Prop} (l : List α) (H : a l, p a) (a : {x // p x}) :
(l.attachWith p H).count a = l.count a :=
Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attachWith _ _ _
end List

View File

@@ -115,6 +115,13 @@ theorem IsPrefix.countP_le (s : l₁ <+: l₂) : countP p l₁ ≤ countP p l₂
theorem IsSuffix.countP_le (s : l₁ <:+ l₂) : countP p l₁ countP p l₂ := s.sublist.countP_le _
theorem IsInfix.countP_le (s : l₁ <:+: l₂) : countP p l₁ countP p l₂ := s.sublist.countP_le _
-- See `Init.Data.List.Nat.Count` for `Sublist.le_countP : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁`.
theorem countP_tail_le (l) : countP p l.tail countP p l :=
(tail_sublist l).countP_le _
-- See `Init.Data.List.Nat.Count` for `le_countP_tail : countP p l - 1 ≤ countP p l.tail`.
theorem countP_filter (l : List α) :
countP p (filter q l) = countP (fun a => p a && q a) l := by
simp only [countP_eq_length_filter, filter_filter]
@@ -207,6 +214,13 @@ theorem IsPrefix.count_le (h : l₁ <+: l₂) (a : α) : count a l₁ ≤ count
theorem IsSuffix.count_le (h : l₁ <:+ l₂) (a : α) : count a l₁ count a l₂ := h.sublist.count_le _
theorem IsInfix.count_le (h : l₁ <:+: l₂) (a : α) : count a l₁ count a l₂ := h.sublist.count_le _
-- See `Init.Data.List.Nat.Count` for `Sublist.le_count : count a l₂ - (l₂.length - l₁.length) ≤ countP a l₁`.
theorem count_tail_le (a : α) (l) : count a l.tail count a l :=
(tail_sublist l).count_le _
-- See `Init.Data.List.Nat.Count` for `le_count_tail : count a l - 1 ≤ count a l.tail`.
theorem count_le_count_cons (a b : α) (l : List α) : count a l count a (b :: l) :=
(sublist_cons_self _ _).count_le _

View File

@@ -109,6 +109,10 @@ protected theorem Sublist.eraseP : l₁ <+ l₂ → l₁.eraseP p <+ l₂.eraseP
theorem length_eraseP_le (l : List α) : (l.eraseP p).length l.length :=
l.eraseP_sublist.length_le
theorem le_length_eraseP (l : List α) : l.length - 1 (l.eraseP p).length := by
rw [length_eraseP]
split <;> simp
theorem mem_of_mem_eraseP {l : List α} : a l.eraseP p a l := (eraseP_subset _ ·)
@[simp] theorem mem_eraseP_of_neg {l : List α} (pa : ¬p a) : a l.eraseP p a l := by
@@ -332,6 +336,10 @@ theorem IsPrefix.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁
theorem length_erase_le (a : α) (l : List α) : (l.erase a).length l.length :=
(erase_sublist a l).length_le
theorem le_length_erase [LawfulBEq α] (a : α) (l : List α) : l.length - 1 (l.erase a).length := by
rw [length_erase]
split <;> simp
theorem mem_of_mem_erase {a b : α} {l : List α} (h : a l.erase b) : a l := erase_subset _ _ h
@[simp] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {l : List α} (ab : a b) :
@@ -452,13 +460,22 @@ end erase
/-! ### eraseIdx -/
theorem length_eraseIdx : {l i}, i < length l length (@eraseIdx α l i) = length l - 1
| [], _, _ => rfl
| _::_, 0, _ => by simp [eraseIdx]
| x::xs, i+1, h => by
have : i < length xs := Nat.lt_of_succ_lt_succ h
simp [eraseIdx, Nat.add_one]
rw [length_eraseIdx this, Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) this)]
theorem length_eraseIdx (l : List α) (i : Nat) :
(l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length := by
induction l generalizing i with
| nil => simp
| cons x l ih =>
cases i with
| zero => simp
| succ i =>
simp only [eraseIdx, length_cons, ih, add_one_lt_add_one_iff, Nat.add_one_sub_one]
split
· cases l <;> simp_all
· rfl
theorem length_eraseIdx_of_lt {l : List α} {i} (h : i < length l) :
(l.eraseIdx i).length = length l - 1 := by
simp [length_eraseIdx, h]
@[simp] theorem eraseIdx_zero (l : List α) : eraseIdx l 0 = tail l := by cases l <;> rfl
@@ -468,6 +485,8 @@ theorem eraseIdx_eq_take_drop_succ :
| a::l, 0 => by simp
| a::l, i + 1 => by simp [eraseIdx_eq_take_drop_succ l i]
-- See `Init.Data.List.Nat.Erase` for `getElem?_eraseIdx` and `getElem_eraseIdx`.
@[simp] theorem eraseIdx_eq_nil {l : List α} {i : Nat} : eraseIdx l i = [] l = [] (length l = 1 i = 0) := by
match l, i with
| [], _
@@ -499,6 +518,13 @@ theorem eraseIdx_eq_self : ∀ {l : List α} {k : Nat}, eraseIdx l k = l ↔ len
theorem eraseIdx_of_length_le {l : List α} {k : Nat} (h : length l k) : eraseIdx l k = l := by
rw [eraseIdx_eq_self.2 h]
theorem length_eraseIdx_le (l : List α) (i : Nat) : length (l.eraseIdx i) length l :=
(eraseIdx_sublist l i).length_le
theorem le_length_eraseIdx (l : List α) (i : Nat) : length l - 1 length (l.eraseIdx i) := by
rw [length_eraseIdx]
split <;> simp
theorem eraseIdx_append_of_lt_length {l : List α} {k : Nat} (hk : k < length l) (l' : List α) :
eraseIdx (l ++ l') k = eraseIdx l k ++ l' := by
induction l generalizing k with
@@ -520,7 +546,7 @@ theorem eraseIdx_append_of_length_le {l : List α} {k : Nat} (hk : length l ≤
theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} :
(replicate n a).eraseIdx k = if k < n then replicate (n - 1) a else replicate n a := by
split <;> rename_i h
· rw [eq_replicate_iff, length_eraseIdx (by simpa using h)]
· rw [eq_replicate_iff, length_eraseIdx_of_lt (by simpa using h)]
simp only [length_replicate, true_and]
intro b m
replace m := mem_of_mem_eraseIdx m

View File

@@ -224,7 +224,7 @@ theorem find?_eq_some : xs.find? p = some b ↔ p b ∧ ∃ as bs, xs = as ++ b
simp only [cons_append] at h₁
obtain rfl, - := h₁
simp_all
· simp only [ih, Bool.not_eq_true', exists_and_right, and_congr_right_iff]
· simp only [ih, Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, and_congr_right_iff]
intro pb
constructor
· rintro as, bs, rfl, h₁
@@ -620,6 +620,18 @@ theorem IsPrefix.findIdx_eq_of_findIdx_lt_length {l₁ l₂ : List α} {p : α
· rfl
· simp_all
theorem findIdx_le_findIdx {l : List α} {p q : α Bool} (h : x l, p x q x) : l.findIdx q l.findIdx p := by
induction l with
| nil => simp
| cons x xs ih =>
simp only [findIdx_cons, cond_eq_if]
split
· simp
· split
· simp_all
· simp only [Nat.add_le_add_iff_right]
exact ih fun _ m w => h _ (mem_cons_of_mem x m) w
/-! ### findIdx? -/
@[simp] theorem findIdx?_nil : ([] : List α).findIdx? p i = none := rfl
@@ -803,7 +815,7 @@ theorem findIdx?_join {l : List (List α)} {p : α → Bool} :
simp only [replicate, findIdx?_cons, Nat.zero_add, findIdx?_succ, zero_lt_succ, true_and]
split <;> simp_all
theorem findIdx?_eq_enum_findSome? {xs : List α} {p : α Bool} :
theorem findIdx?_eq_findSome?_enum {xs : List α} {p : α Bool} :
xs.findIdx? p = xs.enum.findSome? fun i, a => if p a then some i else none := by
induction xs with
| nil => simp
@@ -814,6 +826,30 @@ theorem findIdx?_eq_enum_findSome? {xs : List α} {p : α → Bool} :
· simp_all only [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone, reduceCtorEq]
simp [Function.comp_def, map_fst_add_enum_eq_enumFrom, findSome?_map]
theorem findIdx?_eq_fst_find?_enum {xs : List α} {p : α Bool} :
xs.findIdx? p = (xs.enum.find? fun _, x => p x).map (·.1) := by
induction xs with
| nil => simp
| cons x xs ih =>
simp only [findIdx?_cons, Nat.zero_add, findIdx?_start_succ, enum_cons]
split
· simp_all
· simp only [Option.map_map, enumFrom_eq_map_enum, Bool.false_eq_true, not_false_eq_true,
find?_cons_of_neg, find?_map, *]
congr
-- See also `findIdx_le_findIdx`.
theorem findIdx?_eq_none_of_findIdx?_eq_none {xs : List α} {p q : α Bool} (w : x xs, p x q x) :
xs.findIdx? q = none xs.findIdx? p = none := by
simp only [findIdx?_eq_none_iff]
intro h x m
cases z : p x
· rfl
· exfalso
specialize w x m z
specialize h x m
simp_all
theorem Sublist.findIdx?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
(l₁.findIdx? p).isSome (l₂.findIdx? p).isSome := by
simp only [List.findIdx?_isSome, any_eq_true]
@@ -878,7 +914,7 @@ theorem lookup_eq_some_iff {l : List (α × β)} {k : α} {b : β} :
simp only [lookup_eq_findSome?, findSome?_eq_some_iff]
constructor
· rintro l₁, a, l₂, rfl, h₁, h₂
simp only [beq_iff_eq, ite_some_none_eq_some] at h₁
simp only [beq_iff_eq, Option.ite_none_right_eq_some, Option.some.injEq] at h₁
obtain rfl, rfl := h₁
simp at h₂
exact l₁, l₂, rfl, by simpa using h₂

View File

@@ -266,9 +266,15 @@ theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l
theorem getElem?_eq_some_iff {l : List α} : l[n]? = some a h : n < l.length, l[n] = a := by
simp only [ get?_eq_getElem?, get?_eq_some, get_eq_getElem]
theorem some_eq_getElem?_iff {l : List α} : some a = l[n]? h : n < l.length, l[n] = a := by
rw [eq_comm, getElem?_eq_some_iff]
@[simp] theorem getElem?_eq_none_iff : l[n]? = none length l n := by
simp only [ get?_eq_getElem?, get?_eq_none]
@[simp] theorem none_eq_getElem?_iff {l : List α} {n : Nat} : none = l[n]? length l n := by
simp [eq_comm (a := none)]
theorem getElem?_eq_none (h : length l n) : l[n]? = none := getElem?_eq_none_iff.mpr h
theorem getElem?_eq (l : List α) (i : Nat) :
@@ -1045,6 +1051,11 @@ theorem head?_eq_getElem? : ∀ l : List α, head? l = l[0]?
| [] => rfl
| a :: l => by simp
theorem head_eq_getElem (l : List α) (h : l []) : head l h = l[0]'(length_pos.mpr h) := by
cases l with
| nil => simp at h
| cons _ _ => simp
theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a xs.head? = some a := by
cases xs with
| nil => simp at h
@@ -1105,6 +1116,55 @@ theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_t
theorem mem_of_mem_tail {a : α} {l : List α} (h : a tail l) : a l := by
induction l <;> simp_all
theorem ne_nil_of_tail_ne_nil {l : List α} : l.tail [] l [] := by
cases l <;> simp
@[simp] theorem getElem_tail (l : List α) (i : Nat) (h : i < l.tail.length) :
(tail l)[i] = l[i + 1]'(add_lt_of_lt_sub (by simpa using h)) := by
cases l with
| nil => simp at h
| cons _ l => simp
@[simp] theorem getElem?_tail (l : List α) (i : Nat) :
(tail l)[i]? = l[i + 1]? := by
cases l <;> simp
@[simp] theorem set_tail (l : List α) (i : Nat) (a : α) :
l.tail.set i a = (l.set (i + 1) a).tail := by
cases l <;> simp
theorem one_lt_length_of_tail_ne_nil {l : List α} (h : l.tail []) : 1 < l.length := by
cases l with
| nil => simp at h
| cons _ l =>
simp only [tail_cons, ne_eq] at h
exact Nat.lt_add_of_pos_left (length_pos.mpr h)
@[simp] theorem head_tail (l : List α) (h : l.tail []) :
(tail l).head h = l[1]'(one_lt_length_of_tail_ne_nil h) := by
cases l with
| nil => simp at h
| cons _ l => simp [head_eq_getElem]
@[simp] theorem head?_tail (l : List α) : (tail l).head? = l[1]? := by
simp [head?_eq_getElem?]
@[simp] theorem getLast_tail (l : List α) (h : l.tail []) :
(tail l).getLast h = l.getLast (ne_nil_of_tail_ne_nil h) := by
simp only [getLast_eq_getElem, length_tail, getElem_tail]
congr
match l with
| _ :: _ :: l => simp
theorem getLast?_tail (l : List α) : (tail l).getLast? = if l.length = 1 then none else l.getLast? := by
match l with
| [] => simp
| [a] => simp
| _ :: _ :: l =>
simp only [tail_cons, length_cons, getLast?_cons_cons]
rw [if_neg]
rintro
/-! ## Basic operations -/
/-! ### map -/
@@ -1892,7 +1952,7 @@ theorem map_eq_append_iff {f : α → β} :
map f l = L₁ ++ L₂ l₁ l₂, l = l₁ ++ l₂ map f l₁ = L₁ map f l₂ = L₂ := by
rw [ filterMap_eq_map, filterMap_eq_append_iff]
theorem append_eq_map_iff (f : α β) :
theorem append_eq_map_iff {f : α β} :
L₁ ++ L₂ = map f l l₁ l₂, l = l₁ ++ l₂ map f l₁ = L₁ map f l₂ = L₂ := by
rw [eq_comm, map_eq_append_iff]
@@ -2847,6 +2907,12 @@ theorem dropLast_append_cons : dropLast (l₁ ++ b :: l₂) = l₁ ++ dropLast (
dropLast (a :: replicate n a) = replicate n a := by
rw [ replicate_succ, dropLast_replicate, Nat.add_sub_cancel]
@[simp] theorem tail_reverse (l : List α) : l.reverse.tail = l.dropLast.reverse := by
apply ext_getElem
· simp
· intro i h₁ h₂
simp [Nat.add_comm i, Nat.sub_add_eq]
/-!
### splitAt

View File

@@ -10,3 +10,5 @@ import Init.Data.List.Nat.Range
import Init.Data.List.Nat.Sublist
import Init.Data.List.Nat.TakeDrop
import Init.Data.List.Nat.Count
import Init.Data.List.Nat.Erase
import Init.Data.List.Nat.Find

View File

@@ -5,6 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
-/
prelude
import Init.Data.List.Count
import Init.Data.List.Find
import Init.Data.List.MinMax
import Init.Data.Nat.Lemmas
@@ -18,6 +19,26 @@ open Nat
namespace List
/-! ### dropLast -/
theorem tail_dropLast (l : List α) : tail (dropLast l) = dropLast (tail l) := by
ext1
simp only [getElem?_tail, getElem?_dropLast, length_tail]
split <;> split
· rfl
· omega
· omega
· rfl
@[simp] theorem dropLast_reverse (l : List α) : l.reverse.dropLast = l.tail.reverse := by
apply ext_getElem
· simp
· intro i h₁ h₂
simp only [getElem_dropLast, getElem_reverse, length_tail, getElem_tail]
congr
simp only [length_dropLast, length_reverse, length_tail] at h₁ h₂
omega
/-! ### filter -/
theorem length_filter_lt_length_iff_exists {l} :
@@ -37,7 +58,8 @@ theorem getElem_eq_getElem_reverse {l : List α} {i} (h : i < l.length) :
/-- The length of the List returned by `List.leftpad n a l` is equal
to the larger of `n` and `l.length` -/
@[simp]
-- We don't mark this as a `@[simp]` lemma since we allow `simp` to unfold `leftpad`,
-- so the left hand side simplifies directly to `n - l.length + l.length`.
theorem leftpad_length (n : Nat) (a : α) (l : List α) :
(leftpad n a l).length = max n l.length := by
simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max]
@@ -97,6 +119,53 @@ theorem minimum?_cons' {a : Nat} {l : List Nat} :
specialize le b h
split <;> omega
theorem foldl_min
{α : Type _} [Min α] [Std.IdempotentOp (min : α α α)] [Std.Associative (min : α α α)]
{l : List α} {a : α} :
l.foldl (init := a) min = min a (l.minimum?.getD a) := by
cases l with
| nil => simp [Std.IdempotentOp.idempotent]
| cons b l =>
simp only [minimum?]
induction l generalizing a b with
| nil => simp
| cons c l ih => simp [ih, Std.Associative.assoc]
theorem foldl_min_right {α β : Type _}
[Min β] [Std.IdempotentOp (min : β β β)] [Std.Associative (min : β β β)]
{l : List α} {b : β} {f : α β} :
(l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).minimum?.getD b) := by
rw [ foldl_map, foldl_min]
theorem foldl_min_le {l : List Nat} {a : Nat} : l.foldl (init := a) min a := by
induction l generalizing a with
| nil => simp
| cons c l ih =>
simp only [foldl_cons]
exact Nat.le_trans ih (Nat.min_le_left _ _)
theorem foldl_min_min_of_le {l : List Nat} {a b : Nat} (h : a b) :
l.foldl (init := a) min b :=
Nat.le_trans (foldl_min_le) h
theorem minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a l) :
l.minimum?.getD k a := by
cases l with
| nil => simp at h
| cons b l =>
simp [minimum?_cons]
simp at h
rcases h with (rfl | h)
· exact foldl_min_le
· induction l generalizing b with
| nil => simp_all
| cons c l ih =>
simp only [foldl_cons]
simp at h
rcases h with (rfl | h)
· exact foldl_min_min_of_le (Nat.min_le_right _ _)
· exact ih _ h
/-! ### maximum? -/
-- A specialization of `maximum?_eq_some_iff` to Nat.
@@ -130,4 +199,51 @@ theorem maximum?_cons' {a : Nat} {l : List Nat} :
specialize le b h
split <;> omega
theorem foldl_max
{α : Type _} [Max α] [Std.IdempotentOp (max : α α α)] [Std.Associative (max : α α α)]
{l : List α} {a : α} :
l.foldl (init := a) max = max a (l.maximum?.getD a) := by
cases l with
| nil => simp [Std.IdempotentOp.idempotent]
| cons b l =>
simp only [maximum?]
induction l generalizing a b with
| nil => simp
| cons c l ih => simp [ih, Std.Associative.assoc]
theorem foldl_max_right {α β : Type _}
[Max β] [Std.IdempotentOp (max : β β β)] [Std.Associative (max : β β β)]
{l : List α} {b : β} {f : α β} :
(l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).maximum?.getD b) := by
rw [ foldl_map, foldl_max]
theorem le_foldl_max {l : List Nat} {a : Nat} : a l.foldl (init := a) max := by
induction l generalizing a with
| nil => simp
| cons c l ih =>
simp only [foldl_cons]
exact Nat.le_trans (Nat.le_max_left _ _) ih
theorem le_foldl_max_of_le {l : List Nat} {a b : Nat} (h : a b) :
a l.foldl (init := b) max :=
Nat.le_trans h (le_foldl_max)
theorem le_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a l) :
a l.maximum?.getD k := by
cases l with
| nil => simp at h
| cons b l =>
simp [maximum?_cons]
simp at h
rcases h with (rfl | h)
· exact le_foldl_max
· induction l generalizing b with
| nil => simp_all
| cons c l ih =>
simp only [foldl_cons]
simp at h
rcases h with (rfl | h)
· exact le_foldl_max_of_le (Nat.le_max_right b a)
· exact ih _ h
end List

View File

@@ -28,4 +28,59 @@ theorem count_set [BEq α] (a b : α) (l : List α) (i : Nat) (h : i < l.length)
(l.set i a).count b = l.count b - (if l[i] == b then 1 else 0) + (if a == b then 1 else 0) := by
simp [count_eq_countP, countP_set, h]
/--
The number of elements satisfying a predicate in a sublist is at least the number of elements satisfying the predicate in the list,
minus the difference in the lengths.
-/
theorem Sublist.le_countP (s : l₁ <+ l₂) (p) : countP p l₂ - (l₂.length - l₁.length) countP p l₁ := by
match s with
| .slnil => simp
| .cons a s =>
rename_i l
simp only [countP_cons, length_cons]
have := s.le_countP p
have := s.length_le
split <;> omega
| .cons₂ a s =>
rename_i l₁ l₂
simp only [countP_cons, length_cons]
have := s.le_countP p
have := s.length_le
split <;> omega
theorem IsPrefix.le_countP (s : l₁ <+: l₂) : countP p l₂ - (l₂.length - l₁.length) countP p l₁ :=
s.sublist.le_countP _
theorem IsSuffix.le_countP (s : l₁ <:+ l₂) : countP p l₂ - (l₂.length - l₁.length) countP p l₁ :=
s.sublist.le_countP _
theorem IsInfix.le_countP (s : l₁ <:+: l₂) : countP p l₂ - (l₂.length - l₁.length) countP p l₁ :=
s.sublist.le_countP _
/--
The number of elements satisfying a predicate in the tail of a list is
at least one less than the number of elements satisfying the predicate in the list.
-/
theorem le_countP_tail (l) : countP p l - 1 countP p l.tail := by
have := (tail_sublist l).le_countP p
simp only [length_tail] at this
omega
variable [BEq α]
theorem Sublist.le_count (s : l₁ <+ l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) count a l₁ :=
s.le_countP _
theorem IsPrefix.le_count (s : l₁ <+: l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) count a l₁ :=
s.sublist.le_count _
theorem IsSuffix.le_count (s : l₁ <:+ l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) count a l₁ :=
s.sublist.le_count _
theorem IsInfix.le_count (s : l₁ <:+: l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) count a l₁ :=
s.sublist.le_count _
theorem le_count_tail (a : α) (l) : count a l - 1 count a l.tail :=
le_countP_tail _
end List

View File

@@ -0,0 +1,66 @@
/-
Copyright (c) 2024 Kim Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
prelude
import Init.Data.List.Nat.TakeDrop
import Init.Data.List.Erase
namespace List
theorem getElem?_eraseIdx (l : List α) (i : Nat) (j : Nat) :
(l.eraseIdx i)[j]? = if h : j < i then l[j]? else l[j + 1]? := by
rw [eraseIdx_eq_take_drop_succ, getElem?_append]
split <;> rename_i h
· rw [getElem?_take]
split
· rfl
· simp_all
omega
· rw [getElem?_drop]
split <;> rename_i h'
· simp only [length_take, Nat.min_def, Nat.not_lt] at h
split at h
· omega
· simp_all [getElem?_eq_none]
omega
· simp only [length_take]
simp only [length_take, Nat.min_def, Nat.not_lt] at h
split at h
· congr 1
omega
· rw [getElem?_eq_none, getElem?_eq_none] <;> omega
theorem getElem?_eraseIdx_of_lt (l : List α) (i : Nat) (j : Nat) (h : j < i) :
(l.eraseIdx i)[j]? = l[j]? := by
rw [getElem?_eraseIdx]
simp [h]
theorem getElem?_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : i j) :
(l.eraseIdx i)[j]? = l[j + 1]? := by
rw [getElem?_eraseIdx]
simp only [dite_eq_ite, ite_eq_right_iff]
intro h'
omega
theorem getElem_eraseIdx (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) :
(l.eraseIdx i)[j] = if h' : j < i then
l[j]'(by have := length_eraseIdx_le l i; omega)
else
l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
apply Option.some.inj
rw [ getElem?_eq_getElem, getElem?_eraseIdx]
split <;> simp
theorem getElem_eraseIdx_of_lt (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) (h' : j < i) :
(l.eraseIdx i)[j] = l[j]'(by have := length_eraseIdx_le l i; omega) := by
rw [getElem_eraseIdx]
simp only [dite_eq_left_iff, Nat.not_lt]
intro h'
omega
theorem getElem_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) (h' : i j) :
(l.eraseIdx i)[j] = l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
rw [getElem_eraseIdx, dif_neg]
omega

View File

@@ -0,0 +1,32 @@
/-
Copyright (c) 2024 Kim Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
prelude
import Init.Data.List.Nat.Range
import Init.Data.List.Find
namespace List
theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : List α} {p q : α Bool} (w : x xs, p x q x) {i : Nat}
(h : xs.findIdx? p = some i) : j, j i xs.findIdx? q = some j := by
simp only [findIdx?_eq_findSome?_enum] at h
rw [findSome?_eq_some_iff] at h
simp only [Option.ite_none_right_eq_some, Option.some.injEq, ite_eq_right_iff, reduceCtorEq,
imp_false, Bool.not_eq_true, Prod.forall, exists_and_right, Prod.exists] at h
obtain h, h₁, b, es, h₂, hb, rfl, h₃ := h
rw [enum_eq_enumFrom, enumFrom_eq_append_iff] at h₂
obtain l₁', l₂', rfl, rfl, h₂ := h₂
rw [eq_comm, enumFrom_eq_cons_iff] at h₂
obtain a, as, rfl, h₂, rfl := h₂
simp only [Nat.zero_add, Prod.mk.injEq] at h₂
obtain rfl, rfl := h₂
simp only [findIdx?_append]
match h : findIdx? q l₁' with
| some j =>
refine j, ?_, by simp
rw [findIdx?_eq_some_iff_findIdx_eq] at h
omega
| none =>
refine l₁'.length, by simp, by simp_all

View File

@@ -109,7 +109,8 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
@[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat Bool} :
(range' s n).find? p = some i p i i range' s n j, s j j < i !p j := by
rw [find?_eq_some]
simp only [Bool.not_eq_true', exists_and_right, mem_range'_1, and_congr_right_iff]
simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, mem_range'_1,
and_congr_right_iff]
simp only [range'_eq_append_iff, eq_comm (a := i :: _), range'_eq_cons_iff]
intro h
constructor
@@ -258,6 +259,9 @@ theorem nodup_iota (n : Nat) : Nodup (iota n) :=
| zero => simp at h
| succ n => simp
@[simp] theorem tail_iota (n : Nat) : (iota n).tail = iota (n - 1) := by
cases n <;> simp
@[simp] theorem reverse_iota : reverse (iota n) = range' 1 n := by
induction n with
| zero => simp
@@ -272,15 +276,15 @@ theorem nodup_iota (n : Nat) : Nodup (iota n) :=
rw [getLast_eq_head_reverse]
simp
theorem find?_iota_eq_none {n : Nat} (p : Nat Bool) :
theorem find?_iota_eq_none {n : Nat} {p : Nat Bool} :
(iota n).find? p = none i, 0 < i i n !p i := by
simp
@[simp] theorem find?_iota_eq_some {n : Nat} {i : Nat} {p : Nat Bool} :
(iota n).find? p = some i p i i iota n j, i < j j n !p j := by
rw [find?_eq_some]
simp only [iota_eq_reverse_range', reverse_eq_append_iff, reverse_cons, append_assoc,
singleton_append, Bool.not_eq_true', exists_and_right, mem_reverse, mem_range'_1,
simp only [iota_eq_reverse_range', reverse_eq_append_iff, reverse_cons, append_assoc, cons_append,
nil_append, Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, mem_reverse, mem_range'_1,
and_congr_right_iff]
intro h
constructor
@@ -354,17 +358,6 @@ theorem map_enumFrom (f : α → β) (n : Nat) (l : List α) :
map (Prod.map id f) (enumFrom n l) = enumFrom n (map f l) := by
induction l generalizing n <;> simp_all
@[simp]
theorem enumFrom_map_fst (n) :
(l : List α), map Prod.fst (enumFrom n l) = range' n l.length
| [] => rfl
| _ :: _ => congrArg (cons _) (enumFrom_map_fst _ _)
@[simp]
theorem enumFrom_map_snd : (n) (l : List α), map Prod.snd (enumFrom n l) = l
| _, [] => rfl
| _, _ :: _ => congrArg (cons _) (enumFrom_map_snd _ _)
theorem snd_mem_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x enumFrom n l) : x.2 l :=
enumFrom_map_snd n l mem_map_of_mem _ h
@@ -387,10 +380,6 @@ theorem mem_enumFrom {x : α} {i j : Nat} {xs : List α} (h : (i, x) ∈ xs.enum
x = xs[i - j]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega) :=
le_fst_of_mem_enumFrom h, fst_lt_add_of_mem_enumFrom h, snd_eq_of_mem_enumFrom h
theorem enumFrom_cons' (n : Nat) (x : α) (xs : List α) :
enumFrom n (x :: xs) = (n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id) := by
rw [enumFrom_cons, Nat.add_comm, map_fst_add_enumFrom_eq_enumFrom]
theorem enumFrom_map (n : Nat) (l : List α) (f : α β) :
enumFrom n (l.map f) = (enumFrom n l).map (Prod.map id f) := by
induction l with
@@ -407,22 +396,39 @@ theorem enumFrom_append (xs ys : List α) (n : Nat) :
rw [cons_append, enumFrom_cons, IH, cons_append, enumFrom_cons, length, Nat.add_right_comm,
Nat.add_assoc]
theorem enumFrom_eq_zip_range' (l : List α) {n : Nat} : l.enumFrom n = (range' n l.length).zip l :=
zip_of_prod (enumFrom_map_fst _ _) (enumFrom_map_snd _ _)
theorem enumFrom_eq_cons_iff {l : List α} {n : Nat} :
l.enumFrom n = x :: l' a as, l = a :: as x = (n, a) l' = enumFrom (n + 1) as := by
rw [enumFrom_eq_zip_range', zip_eq_cons_iff]
constructor
· rintro l₁, l₂, h, rfl, rfl
rw [range'_eq_cons_iff] at h
obtain rfl, -, rfl := h
exact x.2, l₂, by simp [enumFrom_eq_zip_range']
· rintro a, as, rfl, rfl, rfl
refine range' (n+1) as.length, as, ?_
simp [enumFrom_eq_zip_range', range'_succ]
@[simp]
theorem unzip_enumFrom_eq_prod (l : List α) {n : Nat} :
(l.enumFrom n).unzip = (range' n l.length, l) := by
simp only [enumFrom_eq_zip_range', unzip_zip, length_range']
theorem enumFrom_eq_append_iff {l : List α} {n : Nat} :
l.enumFrom n = l₁ ++ l₂
l₁' l₂', l = l₁' ++ l₂' l₁ = l₁'.enumFrom n l₂ = l₂'.enumFrom (n + l₁'.length) := by
rw [enumFrom_eq_zip_range', zip_eq_append_iff]
constructor
· rintro w, x, y, z, h, h', rfl, rfl, rfl
rw [range'_eq_append_iff] at h'
obtain k, -, rfl, rfl := h'
simp only [length_range'] at h
obtain rfl := h
refine y, z, rfl, ?_
simp only [enumFrom_eq_zip_range', length_append, true_and]
congr
omega
· rintro l₁', l₂', rfl, rfl, rfl
simp only [enumFrom_eq_zip_range']
refine range' n l₁'.length, range' (n + l₁'.length) l₂'.length, l₁', l₂', ?_
simp [Nat.add_comm]
/-! ### enum -/
theorem enum_cons : (a::as).enum = (0, a) :: as.enumFrom 1 := rfl
theorem enum_cons' (x : α) (xs : List α) :
enum (x :: xs) = (0, x) :: (enum xs).map (Prod.map (· + 1) id) :=
enumFrom_cons' _ _ _
@[simp]
theorem enum_eq_nil {l : List α} : List.enum l = [] l = [] := enumFrom_eq_nil
@@ -448,6 +454,9 @@ theorem getElem_enum (l : List α) (i : Nat) (h : i < l.enum.length) :
l.enum.getLast? = l.getLast?.map fun a => (l.length - 1, a) := by
simp [getLast?_eq_getElem?]
@[simp] theorem tail_enum (l : List α) : (enum l).tail = enumFrom 1 l.tail := by
simp [enum]
theorem mk_mem_enum_iff_getElem? {i : Nat} {x : α} {l : List α} : (i, x) enum l l[i]? = x := by
simp [enum, mk_mem_enumFrom_iff_le_and_getElem?_sub]

View File

@@ -5,6 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
-/
prelude
import Init.Data.List.Pairwise
import Init.Data.List.Zip
/-!
# Lemmas about `List.range` and `List.enum`
@@ -35,11 +36,16 @@ theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step)
theorem range'_ne_nil (s : Nat) {n : Nat} : range' s n [] n 0 := by
cases n <;> simp
@[simp] theorem range'_zero : range' s 0 = [] := by
@[simp] theorem range'_zero : range' s 0 step = [] := by
simp
@[simp] theorem range'_one {s step : Nat} : range' s 1 step = [s] := rfl
@[simp] theorem tail_range' (n : Nat) : (range' s n step).tail = range' (s + step) (n - 1) step := by
cases n with
| zero => simp
| succ n => simp [range'_succ]
@[simp] theorem range'_inj : range' s n = range' s' n' n = n' (n = 0 s = s') := by
constructor
· intro h
@@ -153,6 +159,9 @@ theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n) :=
theorem range_ne_nil {n : Nat} : range n [] n 0 := by
cases n <;> simp
@[simp] theorem tail_range (n : Nat) : (range n).tail = range' 1 (n - 1) := by
rw [range_eq_range', tail_range']
@[simp]
theorem range_sublist {m n : Nat} : range m <+ range n m n := by
simp only [range_eq_range', range'_sublist_right]
@@ -219,6 +228,12 @@ theorem getElem_enumFrom (l : List α) (n) (i : Nat) (h : i < (l.enumFrom n).len
simp only [getElem?_enumFrom, getElem?_eq_getElem h]
simp
@[simp]
theorem tail_enumFrom (l : List α) (n : Nat) : (enumFrom n l).tail = enumFrom (n + 1) l.tail := by
induction l generalizing n with
| nil => simp
| cons _ l ih => simp [ih, enumFrom_cons]
theorem map_fst_add_enumFrom_eq_enumFrom (l : List α) (n k : Nat) :
map (Prod.map (· + n) id) (enumFrom k l) = enumFrom (n + k) l :=
ext_getElem? fun i by simp [(· ·), Nat.add_comm, Nat.add_left_comm]; rfl
@@ -227,4 +242,47 @@ theorem map_fst_add_enum_eq_enumFrom (l : List α) (n : Nat) :
map (Prod.map (· + n) id) (enum l) = enumFrom n l :=
map_fst_add_enumFrom_eq_enumFrom l _ _
theorem enumFrom_cons' (n : Nat) (x : α) (xs : List α) :
enumFrom n (x :: xs) = (n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id) := by
rw [enumFrom_cons, Nat.add_comm, map_fst_add_enumFrom_eq_enumFrom]
@[simp]
theorem enumFrom_map_fst (n) :
(l : List α), map Prod.fst (enumFrom n l) = range' n l.length
| [] => rfl
| _ :: _ => congrArg (cons _) (enumFrom_map_fst _ _)
@[simp]
theorem enumFrom_map_snd : (n) (l : List α), map Prod.snd (enumFrom n l) = l
| _, [] => rfl
| _, _ :: _ => congrArg (cons _) (enumFrom_map_snd _ _)
theorem enumFrom_eq_zip_range' (l : List α) {n : Nat} : l.enumFrom n = (range' n l.length).zip l :=
zip_of_prod (enumFrom_map_fst _ _) (enumFrom_map_snd _ _)
@[simp]
theorem unzip_enumFrom_eq_prod (l : List α) {n : Nat} :
(l.enumFrom n).unzip = (range' n l.length, l) := by
simp only [enumFrom_eq_zip_range', unzip_zip, length_range']
/-! ### enum -/
theorem enum_cons : (a::as).enum = (0, a) :: as.enumFrom 1 := rfl
theorem enum_cons' (x : α) (xs : List α) :
enum (x :: xs) = (0, x) :: (enum xs).map (Prod.map (· + 1) id) :=
enumFrom_cons' _ _ _
theorem enum_eq_enumFrom {l : List α} : l.enum = l.enumFrom 0 := rfl
theorem enumFrom_eq_map_enum (l : List α) (n : Nat) :
enumFrom n l = (enum l).map (Prod.map (· + n) id) := by
induction l generalizing n with
| nil => simp
| cons x xs ih =>
simp only [enumFrom_cons, ih, enum_cons, map_cons, Prod.map_apply, Nat.zero_add, id_eq, map_map,
cons.injEq, map_inj_left, Function.comp_apply, Prod.forall, Prod.mk.injEq, and_true, true_and]
intro a b _
exact (succ_add a n).symm
end List

View File

@@ -1,7 +1,7 @@
/-
Copyright (c) 2024 Lean FRO. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
Authors: Kim Morrison, Eric Wieser, François G. Dorais
-/
prelude
import Init.Data.List.Perm
@@ -114,31 +114,40 @@ theorem enumLE_trans (trans : ∀ a b c, le a b → le b c → le a c)
· simp_all
· simp_all
theorem enumLE_total (total : a b, !le a b le b a)
(a b : Nat × α) : !enumLE le a b enumLE le b a := by
theorem enumLE_total (total : a b, le a b || le b a)
(a b : Nat × α) : enumLE le a b || enumLE le b a := by
simp only [enumLE]
split <;> split
· simpa using Nat.le_of_lt
· simpa using Nat.le_total a.fst b.fst
· simp
· simp
· simp_all [total a.2 b.2]
· have := total a.2 b.2
simp_all
/-! ### merge -/
theorem merge_stable : (xs ys) (_ : x y, x xs y ys x.1 y.1),
(merge xs ys (enumLE le)).map (·.2) = merge (xs.map (·.2)) (ys.map (·.2)) le
| [], ys, _ => by simp [merge]
| xs, [], _ => by simp [merge]
| (i, x) :: xs, (j, y) :: ys, h => by
simp only [merge, enumLE, map_cons]
split <;> rename_i w
· rw [if_pos (by simp [h _ _ (mem_cons_self ..) (mem_cons_self ..)])]
simp only [map_cons, cons.injEq, true_and]
rw [merge_stable, map_cons]
exact fun x' y' mx my => h x' y' (mem_cons_of_mem (i, x) mx) my
· simp only [reduceIte, map_cons, cons.injEq, true_and, reduceCtorEq]
rw [merge_stable, map_cons]
exact fun x' y' mx my => h x' y' mx (mem_cons_of_mem (j, y) my)
theorem cons_merge_cons (s : α α Bool) (a b l r) :
merge (a::l) (b::r) s = if s a b then a :: merge l (b::r) s else b :: merge (a::l) r s := by
simp only [merge]
@[simp] theorem cons_merge_cons_pos (s : α α Bool) (l r) (h : s a b) :
merge (a::l) (b::r) s = a :: merge l (b::r) s := by
rw [cons_merge_cons, if_pos h]
@[simp] theorem cons_merge_cons_neg (s : α α Bool) (l r) (h : ¬ s a b) :
merge (a::l) (b::r) s = b :: merge (a::l) r s := by
rw [cons_merge_cons, if_neg h]
@[simp] theorem length_merge (s : α α Bool) (l r) :
(merge l r s).length = l.length + r.length := by
match l, r with
| [], r => simp
| l, [] => simp
| a::l, b::r =>
rw [cons_merge_cons]
split
· simp_arith [length_merge s l (b::r)]
· simp_arith [length_merge s (a::l) r]
/--
The elements of `merge le xs ys` are exactly the elements of `xs` and `ys`.
@@ -158,16 +167,37 @@ theorem mem_merge {a : α} {xs ys : List α} : a ∈ merge xs ys le ↔ a ∈ xs
apply or_congr_left
simp only [or_comm (a := a = y), or_assoc]
theorem mem_merge_left (s : α α Bool) (h : x l) : x merge l r s :=
mem_merge.2 <| .inl h
theorem mem_merge_right (s : α α Bool) (h : x r) : x merge l r s :=
mem_merge.2 <| .inr h
theorem merge_stable : (xs ys) (_ : x y, x xs y ys x.1 y.1),
(merge xs ys (enumLE le)).map (·.2) = merge (xs.map (·.2)) (ys.map (·.2)) le
| [], ys, _ => by simp [merge]
| xs, [], _ => by simp [merge]
| (i, x) :: xs, (j, y) :: ys, h => by
simp only [merge, enumLE, map_cons]
split <;> rename_i w
· rw [if_pos (by simp [h _ _ (mem_cons_self ..) (mem_cons_self ..)])]
simp only [map_cons, cons.injEq, true_and]
rw [merge_stable, map_cons]
exact fun x' y' mx my => h x' y' (mem_cons_of_mem (i, x) mx) my
· simp only [reduceIte, map_cons, cons.injEq, true_and, reduceCtorEq]
rw [merge_stable, map_cons]
exact fun x' y' mx my => h x' y' mx (mem_cons_of_mem (j, y) my)
-- We enable this instance locally so we can write `Pairwise le` instead of `Pairwise (le · ·)` everywhere.
attribute [local instance] boolRelToRel
/--
If the ordering relation `le` is transitive and total (i.e. `le a b le b a` for all `a, b`)
If the ordering relation `le` is transitive and total (i.e. `le a b || le b a` for all `a, b`)
then the `merge` of two sorted lists is sorted.
-/
theorem sorted_merge
(trans : (a b c : α), le a b le b c le a c)
(total : (a b : α), !le a b le b a)
(total : (a b : α), le a b || le b a)
(l₁ l₂ : List α) (h₁ : l₁.Pairwise le) (h₂ : l₂.Pairwise le) : (merge l₁ l₂ le).Pairwise le := by
induction l₁ generalizing l₂ with
| nil => simpa only [merge]
@@ -188,9 +218,10 @@ theorem sorted_merge
· apply Pairwise.cons
· intro z m
rw [mem_merge, mem_cons] at m
simp only [Bool.not_eq_true] at h
rcases m with (rfl|m|m)
· exact total _ _ (by simpa using h)
· exact trans _ _ _ (total _ _ (by simpa using h)) (rel_of_pairwise_cons h₁ m)
· simpa [h] using total y z
· exact trans _ _ _ (by simpa [h] using total x y) (rel_of_pairwise_cons h₁ m)
· exact rel_of_pairwise_cons h₂ m
· exact ih₂ h₂.tail
@@ -234,7 +265,7 @@ theorem mergeSort_perm : ∀ (l : List α) (le), mergeSort l le ~ l
(Perm.of_eq (splitInTwo_fst_append_splitInTwo_snd _)))
termination_by l => l.length
@[simp] theorem mergeSort_length (l : List α) : (mergeSort l le).length = l.length :=
@[simp] theorem length_mergeSort (l : List α) : (mergeSort l le).length = l.length :=
(mergeSort_perm l le).length_eq
@[simp] theorem mem_mergeSort {a : α} {l : List α} : a mergeSort l le a l :=
@@ -243,13 +274,13 @@ termination_by l => l.length
/--
The result of `mergeSort` is sorted,
as long as the comparison function is transitive (`le a b → le b c → le a c`)
and total in the sense that `le a b le b a`.
and total in the sense that `le a b || le b a`.
The comparison function need not be irreflexive, i.e. `le a b` and `le b a` is allowed even when `a ≠ b`.
-/
theorem sorted_mergeSort
(trans : (a b c : α), le a b le b c le a c)
(total : (a b : α), !le a b le b a) :
(total : (a b : α), le a b || le b a) :
(l : List α) (mergeSort l le).Pairwise le
| [] => by simp [mergeSort]
| [a] => by simp [mergeSort]
@@ -317,7 +348,7 @@ termination_by _ l => l.length
theorem mergeSort_cons {le : α α Bool}
(trans : (a b c : α), le a b le b c le a c)
(total : (a b : α), !le a b le b a)
(total : (a b : α), le a b || le b a)
(a : α) (l : List α) :
l₁ l₂, mergeSort (a :: l) le = l₁ ++ a :: l₂ mergeSort l le = l₁ ++ l₂
b, b l₁ !le a b := by
@@ -376,7 +407,7 @@ then `c` is still a sublist of `mergeSort le l`.
-/
theorem sublist_mergeSort
(trans : (a b c : α), le a b le b c le a c)
(total : (a b : α), !le a b le b a) :
(total : (a b : α), le a b || le b a) :
{c : List α} (_ : c.Pairwise le) (_ : c <+ l),
c <+ mergeSort l le
| _, _, .slnil => nil_sublist _
@@ -407,8 +438,45 @@ then `[a, b]` is still a sublist of `mergeSort le l`.
-/
theorem pair_sublist_mergeSort
(trans : (a b c : α), le a b le b c le a c)
(total : (a b : α), !le a b le b a)
(total : (a b : α), le a b || le b a)
(hab : le a b) (h : [a, b] <+ l) : [a, b] <+ mergeSort l le :=
sublist_mergeSort trans total (pairwise_pair.mpr hab) h
@[deprecated (since := "2024-09-02")] abbrev mergeSort_stable_pair := @pair_sublist_mergeSort
theorem map_merge {f : α β} {r : α α Bool} {s : β β Bool} {l l' : List α}
(hl : a l, b l', r a b = s (f a) (f b)) :
(l.merge l' r).map f = (l.map f).merge (l'.map f) s := by
match l, l' with
| [], x' => simp
| x, [] => simp
| x :: xs, x' :: xs' =>
simp only [List.forall_mem_cons] at hl
simp only [forall_and] at hl
simp only [List.map, List.cons_merge_cons]
rw [ hl.1.1]
split
· rw [List.map, map_merge, List.map]
simp only [List.forall_mem_cons, forall_and]
exact hl.2.1, hl.2.2
· rw [List.map, map_merge, List.map]
simp only [List.forall_mem_cons]
exact hl.1.2, hl.2.2
theorem map_mergeSort {r : α α Bool} {s : β β Bool} {f : α β} {l : List α}
(hl : a l, b l, r a b = s (f a) (f b)) :
(l.mergeSort r).map f = (l.map f).mergeSort s :=
match l with
| [] => by simp
| [x] => by simp
| a :: b :: l => by
simp only [mergeSort, splitInTwo_fst, splitInTwo_snd, map_cons]
rw [map_merge (fun a am b bm => hl a (mem_of_mem_take (by simpa using am))
b (mem_of_mem_drop (by simpa using bm)))]
rw [map_mergeSort (s := s) (fun a am b bm => hl a (mem_of_mem_take (by simpa using am))
b (mem_of_mem_take (by simpa using bm)))]
rw [map_mergeSort (s := s) (fun a am b bm => hl a (mem_of_mem_drop (by simpa using am))
b (mem_of_mem_drop (by simpa using bm)))]
rw [map_take, map_drop]
simp
termination_by length l

View File

@@ -16,83 +16,6 @@ open Nat
/-! ## Zippers -/
/-! ### zip -/
theorem zip_map (f : α γ) (g : β δ) :
(l₁ : List α) (l₂ : List β), zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)
| [], l₂ => rfl
| l₁, [] => by simp only [map, zip_nil_right]
| a :: l₁, b :: l₂ => by
simp only [map, zip_cons_cons, zip_map, Prod.map]; constructor
theorem zip_map_left (f : α γ) (l₁ : List α) (l₂ : List β) :
zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [ zip_map, map_id]
theorem zip_map_right (f : β γ) (l₁ : List α) (l₂ : List β) :
zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [ zip_map, map_id]
theorem zip_append :
{l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
| [], r₁, l₂, r₂, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
| l₁, r₁, [], r₂, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
| a :: l₁, r₁, b :: l₂, r₂, h => by
simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]
theorem zip_map' (f : α β) (g : α γ) :
l : List α, zip (l.map f) (l.map g) = l.map fun a => (f a, g a)
| [] => rfl
| a :: l => by simp only [map, zip_cons_cons, zip_map']
theorem of_mem_zip {a b} : {l₁ : List α} {l₂ : List β}, (a, b) zip l₁ l₂ a l₁ b l₂
| _ :: l₁, _ :: l₂, h => by
cases h
case head => simp
case tail h =>
· have := of_mem_zip h
exact Mem.tail _ this.1, Mem.tail _ this.2
@[deprecated of_mem_zip (since := "2024-07-28")] abbrev mem_zip := @of_mem_zip
theorem map_fst_zip :
(l₁ : List α) (l₂ : List β), l₁.length l₂.length map Prod.fst (zip l₁ l₂) = l₁
| [], bs, _ => rfl
| _ :: as, _ :: bs, h => by
simp [Nat.succ_le_succ_iff] at h
show _ :: map Prod.fst (zip as bs) = _ :: as
rw [map_fst_zip as bs h]
| a :: as, [], h => by simp at h
theorem map_snd_zip :
(l₁ : List α) (l₂ : List β), l₂.length l₁.length map Prod.snd (zip l₁ l₂) = l₂
| _, [], _ => by
rw [zip_nil_right]
rfl
| [], b :: bs, h => by simp at h
| a :: as, b :: bs, h => by
simp [Nat.succ_le_succ_iff] at h
show _ :: map Prod.snd (zip as bs) = _ :: bs
rw [map_snd_zip as bs h]
theorem map_prod_left_eq_zip {l : List α} (f : α β) :
(l.map fun x => (x, f x)) = l.zip (l.map f) := by
rw [ zip_map']
congr
simp
theorem map_prod_right_eq_zip {l : List α} (f : α β) :
(l.map fun x => (f x, x)) = (l.map f).zip l := by
rw [ zip_map']
congr
simp
/-- See also `List.zip_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
@[simp] theorem zip_replicate' {a : α} {b : β} {n : Nat} :
zip (replicate n a) (replicate n b) = replicate n (a, b) := by
induction n with
| zero => rfl
| succ n ih => simp [replicate_succ, ih]
/-! ### zipWith -/
theorem zipWith_comm (f : α β γ) :
@@ -229,6 +152,7 @@ theorem drop_zipWith : (zipWith f l l').drop n = zipWith f (l.drop n) (l'.drop n
@[deprecated drop_zipWith (since := "2024-07-26")] abbrev zipWith_distrib_drop := @drop_zipWith
@[simp]
theorem tail_zipWith : (zipWith f l l').tail = zipWith f l.tail l'.tail := by
rw [ drop_one]; simp [drop_zipWith]
@@ -248,6 +172,65 @@ theorem zipWith_append (f : α → β → γ) (l la : List α) (l' lb : List β)
simp only [length_cons, Nat.succ.injEq] at h
simp [ih _ h]
theorem zipWith_eq_cons_iff {f : α β γ} {l₁ : List α} {l₂ : List β} :
zipWith f l₁ l₂ = g :: l
a l₁' b l₂', l₁ = a :: l₁' l₂ = b :: l₂' g = f a b l = zipWith f l₁' l₂' := by
match l₁, l₂ with
| [], [] => simp
| [], b :: l₂ => simp
| a :: l₁, [] => simp
| a' :: l₁, b' :: l₂ =>
simp only [zip_cons_cons, cons.injEq, Prod.mk.injEq]
constructor
· rintro rfl, rfl, rfl
refine a', l₁, b', l₂, by simp
· rintro a, l₁, b, l₂, rfl, rfl, rfl, rfl, rfl, rfl
simp
theorem zipWith_eq_append_iff {f : α β γ} {l₁ : List α} {l₂ : List β} :
zipWith f l₁ l₂ = l₁' ++ l₂'
w x y z, w.length = y.length l₁ = w ++ x l₂ = y ++ z l₁' = zipWith f w y l₂' = zipWith f x z := by
induction l₁ generalizing l₂ l₁' with
| nil =>
simp
constructor
· rintro rfl, rfl
exact [], [], [], by simp
· rintro _, _, _, -, rfl, rfl, _, rfl, rfl, rfl
simp
| cons x₁ l₁ ih₁ =>
cases l₂ with
| nil =>
constructor
· simp only [zipWith_nil_right, nil_eq, append_eq_nil, exists_and_left, and_imp]
rintro rfl rfl
exact [], x₁ :: l₁, [], by simp
· rintro w, x, y, z, h₁, _, h₃, rfl, rfl
simp only [nil_eq, append_eq_nil] at h₃
obtain rfl, rfl := h₃
simp
| cons x₂ l₂ =>
simp only [zipWith_cons_cons]
rw [cons_eq_append_iff]
constructor
· rintro (rfl, rfl | l₁'', rfl, h)
· exact [], x₁ :: l₁, [], x₂ :: l₂, by simp
· rw [ih₁] at h
obtain w, x, y, z, h, rfl, rfl, h', rfl := h
refine x₁ :: w, x, x₂ :: y, z, by simp [h, h']
· rintro w, x, y, z, h₁, h₂, h₃, rfl, rfl
rw [cons_eq_append_iff] at h₂
rw [cons_eq_append_iff] at h₃
obtain (rfl, rfl | w', rfl, rfl) := h₂
· simp only [zipWith_nil_left, true_and, nil_eq, reduceCtorEq, false_and, exists_const,
or_false]
obtain (rfl, rfl | y', rfl, rfl) := h₃
· simp
· simp_all
· obtain (rfl, rfl | y', rfl, rfl) := h₃
· simp_all
· simp_all [zipWith_append, Nat.succ_inj']
/-- See also `List.zipWith_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
@[simp] theorem zipWith_replicate' {a : α} {b : β} {n : Nat} :
zipWith f (replicate n a) (replicate n b) = replicate n (f a b) := by
@@ -255,6 +238,113 @@ theorem zipWith_append (f : α → β → γ) (l la : List α) (l' lb : List β)
| zero => rfl
| succ n ih => simp [replicate_succ, ih]
/-! ### zip -/
theorem zip_eq_zipWith : (l₁ : List α) (l₂ : List β), zip l₁ l₂ = zipWith Prod.mk l₁ l₂
| [], _ => rfl
| _, [] => rfl
| a :: l₁, b :: l₂ => by simp [zip_cons_cons, zip_eq_zipWith l₁ l₂]
theorem zip_map (f : α γ) (g : β δ) :
(l₁ : List α) (l₂ : List β), zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)
| [], l₂ => rfl
| l₁, [] => by simp only [map, zip_nil_right]
| a :: l₁, b :: l₂ => by
simp only [map, zip_cons_cons, zip_map, Prod.map]; constructor
theorem zip_map_left (f : α γ) (l₁ : List α) (l₂ : List β) :
zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [ zip_map, map_id]
theorem zip_map_right (f : β γ) (l₁ : List α) (l₂ : List β) :
zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [ zip_map, map_id]
@[simp] theorem tail_zip (l₁ : List α) (l₂ : List β) :
(zip l₁ l₂).tail = zip l₁.tail l₂.tail := by
cases l₁ <;> cases l₂ <;> simp
theorem zip_append :
{l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
| [], r₁, l₂, r₂, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
| l₁, r₁, [], r₂, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
| a :: l₁, r₁, b :: l₂, r₂, h => by
simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]
theorem zip_map' (f : α β) (g : α γ) :
l : List α, zip (l.map f) (l.map g) = l.map fun a => (f a, g a)
| [] => rfl
| a :: l => by simp only [map, zip_cons_cons, zip_map']
theorem of_mem_zip {a b} : {l₁ : List α} {l₂ : List β}, (a, b) zip l₁ l₂ a l₁ b l₂
| _ :: l₁, _ :: l₂, h => by
cases h
case head => simp
case tail h =>
· have := of_mem_zip h
exact Mem.tail _ this.1, Mem.tail _ this.2
@[deprecated of_mem_zip (since := "2024-07-28")] abbrev mem_zip := @of_mem_zip
theorem map_fst_zip :
(l₁ : List α) (l₂ : List β), l₁.length l₂.length map Prod.fst (zip l₁ l₂) = l₁
| [], bs, _ => rfl
| _ :: as, _ :: bs, h => by
simp [Nat.succ_le_succ_iff] at h
show _ :: map Prod.fst (zip as bs) = _ :: as
rw [map_fst_zip as bs h]
| a :: as, [], h => by simp at h
theorem map_snd_zip :
(l₁ : List α) (l₂ : List β), l₂.length l₁.length map Prod.snd (zip l₁ l₂) = l₂
| _, [], _ => by
rw [zip_nil_right]
rfl
| [], b :: bs, h => by simp at h
| a :: as, b :: bs, h => by
simp [Nat.succ_le_succ_iff] at h
show _ :: map Prod.snd (zip as bs) = _ :: bs
rw [map_snd_zip as bs h]
theorem map_prod_left_eq_zip {l : List α} (f : α β) :
(l.map fun x => (x, f x)) = l.zip (l.map f) := by
rw [ zip_map']
congr
simp
theorem map_prod_right_eq_zip {l : List α} (f : α β) :
(l.map fun x => (f x, x)) = (l.map f).zip l := by
rw [ zip_map']
congr
simp
@[simp] theorem zip_eq_nil_iff {l₁ : List α} {l₂ : List β} :
zip l₁ l₂ = [] l₁ = [] l₂ = [] := by
simp [zip_eq_zipWith]
theorem zip_eq_cons_iff {l₁ : List α} {l₂ : List β} :
zip l₁ l₂ = (a, b) :: l
l₁' l₂', l₁ = a :: l₁' l₂ = b :: l₂' l = zip l₁' l₂' := by
simp only [zip_eq_zipWith, zipWith_eq_cons_iff]
constructor
· rintro a, l₁, b, l₂, rfl, rfl, h, rfl, rfl
simp only [Prod.mk.injEq] at h
obtain rfl, rfl := h
simp
· rintro l₁', l₂', rfl, rfl, rfl
refine a, l₁', b, l₂', by simp
theorem zip_eq_append_iff {l₁ : List α} {l₂ : List β} :
zip l₁ l₂ = l₁' ++ l₂'
w x y z, w.length = y.length l₁ = w ++ x l₂ = y ++ z l₁' = zip w y l₂' = zip x z := by
simp [zip_eq_zipWith, zipWith_eq_append_iff]
/-- See also `List.zip_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
@[simp] theorem zip_replicate' {a : α} {b : β} {n : Nat} :
zip (replicate n a) (replicate n b) = replicate n (a, b) := by
induction n with
| zero => rfl
| succ n ih => simp [replicate_succ, ih]
/-! ### zipWithAll -/
theorem getElem?_zipWithAll {f : Option α Option β γ} {i : Nat} :
@@ -284,12 +374,16 @@ theorem head?_zipWithAll {f : Option α → Option β → γ} :
| none, none => .none | a?, b? => some (f a? b?) := by
simp [head?_eq_getElem?, getElem?_zipWithAll]
theorem head_zipWithAll {f : Option α Option β γ} (h) :
@[simp] theorem head_zipWithAll {f : Option α Option β γ} (h) :
(zipWithAll f as bs).head h = f as.head? bs.head? := by
apply Option.some.inj
rw [ head?_eq_head, head?_zipWithAll]
split <;> simp_all
@[simp] theorem tail_zipWithAll {f : Option α Option β γ} :
(zipWithAll f as bs).tail = zipWithAll f as.tail bs.tail := by
cases as <;> cases bs <;> simp
theorem zipWithAll_map {μ} (f : Option γ Option δ μ) (g : α γ) (h : β δ) (l₁ : List α) (l₂ : List β) :
zipWithAll f (l₁.map g) (l₂.map h) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂ := by
induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
@@ -358,6 +452,12 @@ theorem zip_of_prod {l : List α} {l' : List β} {lp : List (α × β)} (hl : lp
(hr : lp.map Prod.snd = l') : lp = l.zip l' := by
rw [ hl, hr, zip_unzip lp, unzip_fst, unzip_snd, zip_unzip, zip_unzip]
theorem tail_zip_fst {l : List (α × β)} : l.unzip.1.tail = l.tail.unzip.1 := by
simp
theorem tail_zip_snd {l : List (α × β)} : l.unzip.2.tail = l.tail.unzip.2 := by
simp
@[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
ext1 <;> simp

View File

@@ -237,7 +237,7 @@ theorem testBit_two_pow_add_eq (x i : Nat) : testBit (2^i + x) i = !(testBit x i
| _ p => simp [p]
theorem testBit_mul_two_pow_add_eq (a b i : Nat) :
testBit (2^i*a + b) i = Bool.xor (a%2 = 1) (testBit b i) := by
testBit (2^i*a + b) i = (a%2 = 1 ^^ testBit b i) := by
match a with
| 0 => simp
| a+1 =>
@@ -570,7 +570,7 @@ theorem or_div_two : (a ||| b) / 2 = a / 2 ||| b / 2 := by
/-! ### xor -/
@[simp] theorem testBit_xor (x y i : Nat) :
(x ^^^ y).testBit i = Bool.xor (x.testBit i) (y.testBit i) := by
(x ^^^ y).testBit i = ((x.testBit i) ^^ (y.testBit i)) := by
simp [HXor.hXor, Xor.xor, xor, testBit_bitwise ]
@[simp] theorem zero_xor (x : Nat) : 0 ^^^ x = x := by

View File

@@ -134,6 +134,19 @@ theorem mod_eq_of_lt {a b : Nat} (h : a < b) : a % b = a :=
if_neg h'
(mod_eq a b).symm this
@[simp] theorem one_mod_eq_zero_iff {n : Nat} : 1 % n = 0 n = 1 := by
match n with
| 0 => simp
| 1 => simp
| n + 2 =>
rw [mod_eq_of_lt (by exact Nat.lt_of_sub_eq_succ rfl)]
simp only [add_one_ne_zero, false_iff, ne_eq]
exact ne_of_beq_eq_false rfl
@[simp] theorem Nat.zero_eq_one_mod_iff {n : Nat} : 0 = 1 % n n = 1 := by
rw [eq_comm]
simp
theorem mod_eq_sub_mod {a b : Nat} (h : a b) : a % b = (a - b) % b :=
match eq_zero_or_pos b with
| Or.inl h₁ => h₁.symm (Nat.sub_zero a).symm rfl
@@ -157,6 +170,13 @@ theorem mod_lt (x : Nat) {y : Nat} : y > 0 → x % y < y := by
rw [mod_eq_sub_mod h₁]
exact h₂ h₃
@[simp] protected theorem sub_mod_add_mod_cancel (a b : Nat) [NeZero a] : a - b % a + b % a = a := by
rw [Nat.sub_add_cancel]
cases a with
| zero => simp_all
| succ a =>
exact Nat.le_of_lt (mod_lt b (zero_lt_succ a))
theorem mod_le (x y : Nat) : x % y x := by
match Nat.lt_or_ge x y with
| Or.inl h₁ => rw [mod_eq_of_lt h₁]; apply Nat.le_refl
@@ -197,7 +217,6 @@ decreasing_by apply div_rec_lemma; assumption
theorem div_eq_sub_div (h₁ : 0 < b) (h₂ : b a) : a / b = (a - b) / b + 1 := by
rw [div_eq a, if_pos]; constructor <;> assumption
theorem mod_add_div (m k : Nat) : m % k + k * (m / k) = m := by
induction m, k using mod.inductionOn with rw [div_eq, mod_eq]
| base x y h => simp [h]

View File

@@ -230,6 +230,17 @@ instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
@[simp] protected theorem min_self_assoc' {m n : Nat} : min n (min m n) = min n m := by
rw [Nat.min_comm m n, Nat.min_assoc, Nat.min_self]
@[simp] theorem min_add_left {a b : Nat} : min a (b + a) = a := by
rw [Nat.min_def]
simp
@[simp] theorem min_add_right {a b : Nat} : min a (a + b) = a := by
rw [Nat.min_def]
simp
@[simp] theorem add_left_min {a b : Nat} : min (b + a) a = a := by
rw [Nat.min_comm, min_add_left]
@[simp] theorem add_right_min {a b : Nat} : min (a + b) a = a := by
rw [Nat.min_comm, min_add_right]
protected theorem sub_sub_eq_min : (a b : Nat), a - (a - b) = min a b
| 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
| _, 0 => by rw [Nat.sub_zero, Nat.sub_self, Nat.min_zero]
@@ -284,6 +295,17 @@ protected theorem max_assoc : ∀ (a b c : Nat), max (max a b) c = max a (max b
| _+1, _+1, _+1 => by simp only [Nat.succ_max_succ]; exact congrArg succ <| Nat.max_assoc ..
instance : Std.Associative (α := Nat) max := Nat.max_assoc
@[simp] theorem max_add_left {a b : Nat} : max a (b + a) = b + a := by
rw [Nat.max_def]
simp
@[simp] theorem max_add_right {a b : Nat} : max a (a + b) = a + b := by
rw [Nat.max_def]
simp
@[simp] theorem add_left_max {a b : Nat} : max (b + a) a = b + a := by
rw [Nat.max_comm, max_add_left]
@[simp] theorem add_right_max {a b : Nat} : max (a + b) a = a + b := by
rw [Nat.max_comm, max_add_right]
protected theorem sub_add_eq_max (a b : Nat) : a - b + b = max a b := by
match Nat.le_total a b with
| .inl hl => rw [Nat.max_eq_right hl, Nat.sub_eq_zero_iff_le.mpr hl, Nat.zero_add]

View File

@@ -14,7 +14,7 @@ namespace Option
theorem mem_iff {a : α} {b : Option α} : a b b = some a := .rfl
@[simp] theorem mem_some {a b : α} : a some b b = a := by simp [mem_iff]
theorem mem_some {a b : α} : a some b b = a := by simp
theorem mem_some_self (a : α) : a some a := mem_some.2 rfl
@@ -231,7 +231,7 @@ theorem isSome_filter_of_isSome (p : α → Bool) (o : Option α) (h : (o.filter
o.isSome := by
cases o <;> simp at h
@[simp] theorem filter_eq_none (p : α Bool) :
@[simp] theorem filter_eq_none {p : α Bool} :
Option.filter p o = none o = none a, a o ¬ p a := by
cases o <;> simp [filter_some]
@@ -448,22 +448,6 @@ end beq
/-! ### ite -/
section ite
@[simp] theorem mem_dite_none_left {x : α} [Decidable p] {l : ¬ p Option α} :
(x if h : p then none else l h) h : ¬ p, x l h := by
split <;> simp_all
@[simp] theorem mem_dite_none_right {x : α} [Decidable p] {l : p Option α} :
(x if h : p then l h else none) h : p, x l h := by
split <;> simp_all
@[simp] theorem mem_ite_none_left {x : α} [Decidable p] {l : Option α} :
(x if p then none else l) ¬ p x l := by
split <;> simp_all
@[simp] theorem mem_ite_none_right {x : α} [Decidable p] {l : Option α} :
(x if p then l else none) p x l := by
split <;> simp_all
@[simp] theorem dite_none_left_eq_some {p : Prop} [Decidable p] {b : ¬p Option β} :
(if h : p then none else b h) = some a h, b h = some a := by
split <;> simp_all
@@ -496,6 +480,22 @@ section ite
some a = (if p then b else none) p some a = b := by
split <;> simp_all
theorem mem_dite_none_left {x : α} [Decidable p] {l : ¬ p Option α} :
(x if h : p then none else l h) h : ¬ p, x l h := by
simp
theorem mem_dite_none_right {x : α} [Decidable p] {l : p Option α} :
(x if h : p then l h else none) h : p, x l h := by
simp
theorem mem_ite_none_left {x : α} [Decidable p] {l : Option α} :
(x if p then none else l) ¬ p x l := by
simp
theorem mem_ite_none_right {x : α} [Decidable p] {l : Option α} :
(x if p then l else none) p x l := by
simp
@[simp] theorem isSome_dite {p : Prop} [Decidable p] {b : p β} :
(if h : p then some (b h) else none).isSome = true p := by
split <;> simpa

View File

@@ -7,7 +7,7 @@ Additional goodies for writing macros
-/
prelude
import Init.MetaTypes
import Init.Data.Array.Basic
import Init.Data.Array.GetLit
import Init.Data.Option.BasicAux
namespace Lean

View File

@@ -231,8 +231,21 @@ instance : Std.Associative (· || ·) := ⟨Bool.or_assoc⟩
@[simp] theorem Bool.not_false : (!false) = true := by decide
@[simp] theorem beq_true (b : Bool) : (b == true) = b := by cases b <;> rfl
@[simp] theorem beq_false (b : Bool) : (b == false) = !b := by cases b <;> rfl
@[simp] theorem Bool.not_eq_true' (b : Bool) : ((!b) = true) = (b = false) := by cases b <;> simp
@[simp] theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by cases b <;> simp
/--
We move `!` from the left hand side of an equality to the right hand side.
This helps confluence, and also helps combining pairs of `!`s.
-/
@[simp] theorem Bool.not_eq_eq_eq_not {a b : Bool} : ((!a) = b) (a = !b) := by
cases a <;> cases b <;> simp
@[simp] theorem Bool.not_eq_not {a b : Bool} : ¬a = !b a = b := by
cases a <;> cases b <;> simp
theorem Bool.not_not_eq {a b : Bool} : ¬(!a) = b a = b := by simp
theorem Bool.not_eq_true' (b : Bool) : ((!b) = true) = (b = false) := by simp
theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by simp
@[simp] theorem Bool.not_eq_true (b : Bool) : (¬(b = true)) = (b = false) := by cases b <;> decide
@[simp] theorem Bool.not_eq_false (b : Bool) : (¬(b = false)) = (b = true) := by cases b <;> decide

View File

@@ -773,8 +773,9 @@ macro_rules
macro "refine_lift' " e:term : tactic => `(tactic| focus (refine' no_implicit_lambda% $e; rotate_right))
/-- Similar to `have`, but using `refine'` -/
macro "have' " d:haveDecl : tactic => `(tactic| refine_lift' have $d:haveDecl; ?_)
/-- Similar to `have`, but using `refine'` -/
set_option linter.missingDocs false in -- OK, because `tactic_alt` causes inheritance of docs
macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x:ident : _ := $p)
attribute [tactic_alt tacticHave'_] «tacticHave'_:=_»
/-- Similar to `let`, but using `refine'` -/
macro "let' " d:letDecl : tactic => `(tactic| refine_lift' let $d:letDecl; ?_)

View File

@@ -68,7 +68,7 @@ namespace InitParamMap
def initBorrow (ps : Array Param) : Array Param :=
ps.map fun p => { p with borrow := p.ty.isObj }
/-- We do perform borrow inference for constants marked as `export`.
/-- We do not perform borrow inference for constants marked as `export`.
Reason: we current write wrappers in C++ for using exported functions.
These wrappers use smart pointers such as `object_ref`.
When writing a new wrapper we need to know whether an argument is a borrow

View File

@@ -183,7 +183,7 @@ def UserWidgetInfo.format (info : UserWidgetInfo) : Format :=
f!"UserWidget {info.id}\n{Std.ToFormat.format <| info.props.run' {}}"
def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
f!"FVarAlias {info.userName.eraseMacroScopes}"
f!"FVarAlias {info.userName.eraseMacroScopes}: {info.id.name} -> {info.baseId.name}"
def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
f!"FieldRedecl @ {formatStxRange ctx info.stx}"

View File

@@ -41,9 +41,9 @@ def lratChecker (cfg : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := d
@[inherit_doc Lean.Parser.Tactic.bvCheck]
def bvCheck (g : MVarId) (cfg : TacticContext) : MetaM Unit := do
let unsatProver : UnsatProver := fun bvExpr _ => do
let unsatProver : UnsatProver := fun reflectionResult _ => do
withTraceNode `sat (fun _ => return "Preparing LRAT reflection term") do
let proof lratChecker cfg bvExpr
let proof lratChecker cfg reflectionResult.bvExpr
return proof, ""
let _ closeWithBVReflection g unsatProver
return ()

View File

@@ -74,19 +74,111 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
finalMap := finalMap.push (atomExpr, BitVec.ofNat currentBit value)
return finalMap
structure ReflectionResult where
bvExpr : BVLogicalExpr
proveFalse : Expr M Expr
unusedHypotheses : Std.HashSet FVarId
structure UnsatProver.Result where
proof : Expr
lratCert : LratCert
abbrev UnsatProver := BVLogicalExpr Std.HashMap Nat Expr MetaM UnsatProver.Result
abbrev UnsatProver := ReflectionResult Std.HashMap Nat Expr MetaM UnsatProver.Result
def lratBitblaster (cfg : TacticContext) (bv : BVLogicalExpr)
/--
Contains values that will be used to diagnose spurious counter examples.
-/
structure DiagnosisInput where
unusedHypotheses : Std.HashSet FVarId
atomsAssignment : Std.HashMap Nat Expr
/--
The result of a spurious counter example diagnosis.
-/
structure Diagnosis where
uninterpretedSymbols : Std.HashSet Expr := {}
unusedRelevantHypotheses : Std.HashSet FVarId := {}
abbrev DiagnosisM : Type Type := ReaderT DiagnosisInput <| StateRefT Diagnosis MetaM
namespace DiagnosisM
def run (x : DiagnosisM Unit) (unusedHypotheses : Std.HashSet FVarId)
(atomsAssignment : Std.HashMap Nat Expr) : MetaM Diagnosis := do
let (_, issues) ReaderT.run x { unusedHypotheses, atomsAssignment } |>.run {}
return issues
def unusedHyps : DiagnosisM (Std.HashSet FVarId) := do
return ( read).unusedHypotheses
def atomsAssignment : DiagnosisM (Std.HashMap Nat Expr) := do
return ( read).atomsAssignment
def addUninterpretedSymbol (e : Expr) : DiagnosisM Unit :=
modify fun s => { s with uninterpretedSymbols := s.uninterpretedSymbols.insert e }
def addUnusedRelevantHypothesis (fvar : FVarId) : DiagnosisM Unit :=
modify fun s => { s with unusedRelevantHypotheses := s.unusedRelevantHypotheses.insert fvar }
def checkRelevantHypsUsed (fvar : FVarId) : DiagnosisM Unit := do
for hyp in unusedHyps do
if ( hyp.getType).containsFVar fvar then
addUnusedRelevantHypothesis hyp
/--
Diagnose spurious counter examples, currently this checks:
- Whether uninterpreted symbols were used
- Whether all hypotheses which contain any variable that was bitblasted were included
-/
def diagnose : DiagnosisM Unit := do
for (_, expr) in atomsAssignment do
match_expr expr with
| BitVec.ofBool x =>
match x with
| .fvar fvarId => checkRelevantHypsUsed fvarId
| _ => addUninterpretedSymbol expr
| _ =>
match expr with
| .fvar fvarId => checkRelevantHypsUsed fvarId
| _ => addUninterpretedSymbol expr
end DiagnosisM
def uninterpretedExplainer (d : Diagnosis) : Option MessageData := do
guard !d.uninterpretedSymbols.isEmpty
let symList := d.uninterpretedSymbols.toList
return m!"It abstracted the following unsupported expressions as opaque variables: {symList}"
def unusedRelevantHypothesesExplainer (d : Diagnosis) : Option MessageData := do
guard !d.unusedRelevantHypotheses.isEmpty
let hypList := d.unusedRelevantHypotheses.toList.map mkFVar
return m!"The following potentially relevant hypotheses could not be used: {hypList}"
def explainers : List (Diagnosis Option MessageData) :=
[uninterpretedExplainer, unusedRelevantHypothesesExplainer]
def explainCounterExampleQuality (unusedHypotheses : Std.HashSet FVarId)
(atomsAssignment : Std.HashMap Nat Expr) : MetaM MessageData := do
let diagnosis DiagnosisM.run DiagnosisM.diagnose unusedHypotheses atomsAssignment
let folder acc explainer := if let some m := explainer diagnosis then acc.push m else acc
let explanations := explainers.foldl (init := #[]) folder
if explanations.isEmpty then
return m!"The prover found a counterexample, consider the following assignment:\n"
else
let mut err := m!"The prover found a potentially spurious counterexample:\n"
err := err ++ explanations.foldl (init := m!"") (fun acc exp => acc ++ m!"- " ++ exp ++ m!"\n")
err := err ++ m!"Consider the following assignment:\n"
return err
def lratBitblaster (cfg : TacticContext) (reflectionResult : ReflectionResult)
(atomsAssignment : Std.HashMap Nat Expr) :
MetaM UnsatProver.Result := do
let bvExpr := reflectionResult.bvExpr
let entry
withTraceNode `bv (fun _ => return "Bitblasting BVLogicalExpr to AIG") do
-- lazyPure to prevent compiler lifting
IO.lazyPure (fun _ => bv.bitblast)
IO.lazyPure (fun _ => bvExpr.bitblast)
let aigSize := entry.aig.decls.size
trace[Meta.Tactic.bv] s!"AIG has {aigSize} nodes."
@@ -108,18 +200,25 @@ def lratBitblaster (cfg : TacticContext) (bv : BVLogicalExpr)
match res with
| .ok cert =>
let proof cert.toReflectionProof cfg bv ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
let proof cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
return proof, cert
| .error assignment =>
let reconstructed := reconstructCounterExample map assignment aigSize atomsAssignment
let mut error := m!"The prover found a potential counterexample, consider the following assignment:\n"
let mut error explainCounterExampleQuality reflectionResult.unusedHypotheses atomsAssignment
for (var, value) in reconstructed do
error := error ++ m!"{var} = {value.bv}\n"
throwError error
def reflectBV (g : MVarId) : M (BVLogicalExpr × (Expr M Expr)) := g.withContext do
let hyps getLocalHyps
let sats hyps.filterMapM SatAtBVLogical.of
def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
let hyps getPropHyps
let mut sats := #[]
let mut unusedHypotheses := {}
for hyp in hyps do
if let some reflected SatAtBVLogical.of (mkFVar hyp) then
sats := sats.push reflected
else
unusedHypotheses := unusedHypotheses.insert hyp
if sats.size = 0 then
let mut error := "None of the hypotheses are in the supported BitVec fragment.\n"
error := error ++ "There are two potential fixes for this:\n"
@@ -128,27 +227,32 @@ def reflectBV (g : MVarId) : M (BVLogicalExpr × (Expr → M Expr)) := g.withCon
error := error ++ " Consider expressing it in terms of different operations that are better supported."
throwError error
let sat := sats.foldl (init := SatAtBVLogical.trivial) SatAtBVLogical.and
return (sat.bvExpr, sat.proveFalse)
return {
bvExpr := sat.bvExpr,
proveFalse := sat.proveFalse,
unusedHypotheses := unusedHypotheses
}
def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
MetaM LratCert := M.run do
g.withContext do
let (bvLogicalExpr, f)
let reflectionResult
withTraceNode `bv (fun _ => return "Reflecting goal into BVLogicalExpr") do
reflectBV g
trace[Meta.Tactic.bv] "Reflected bv logical expression: {bvLogicalExpr}"
trace[Meta.Tactic.bv] "Reflected bv logical expression: {reflectionResult.bvExpr}"
let atomsPairs := ( getThe State).atoms.toList.map (fun (expr, _, ident) => (ident, expr))
let atomsAssignment := Std.HashMap.ofList atomsPairs
let bvExprUnsat, cert unsatProver bvLogicalExpr atomsAssignment
let proveFalse f bvExprUnsat
let bvExprUnsat, cert unsatProver reflectionResult atomsAssignment
let proveFalse reflectionResult.proveFalse bvExprUnsat
g.assign proveFalse
return cert
def bvUnsat (g : MVarId) (cfg : TacticContext) : MetaM LratCert := M.run do
let unsatProver : UnsatProver := fun bvExpr atomsAssignment => do
let unsatProver : UnsatProver := fun reflectionResult atomsAssignment => do
withTraceNode `bv (fun _ => return "Preparing LRAT reflection term") do
lratBitblaster cfg bvExpr atomsAssignment
lratBitblaster cfg reflectionResult atomsAssignment
closeWithBVReflection g unsatProver
structure Result where

View File

@@ -422,10 +422,11 @@ partial def addFact (p : MetaProblem) (h : Expr) : OmegaM (MetaProblem × Nat) :
trace[omega] "adding fact: {t}"
match t with
| .forallE _ x y _ =>
if ( isProp x) && ( isProp y) then
if pure t.isArrow <&&> isProp x <&&> isProp y then
p.addFact (mkApp4 (.const ``Decidable.not_or_of_imp []) x y
(.app (.const ``Classical.propDecidable []) x) h)
else
trace[omega] "rejecting forall: it's not an arrow, or not propositional"
return (p, 0)
| .app _ _ =>
match_expr t with

View File

@@ -447,7 +447,10 @@ def unusedVariables : Linter where
let fvarAliases : Std.HashMap FVarId FVarId := s.fvarAliases.fold (init := {}) fun m id baseId =>
m.insert id (followAliases s.fvarAliases baseId)
let getCanonVar (id : FVarId) : FVarId := fvarAliases.getD id id
-- Collect all non-alias fvars corresponding to `fvarUses` by resolving aliases in the list.
-- Unlike `s.fvarUses`, `fvarUsesRef` is guaranteed to contain no aliases.
let fvarUsesRef IO.mkRef <| fvarAliases.fold (init := s.fvarUses) fun fvarUses id baseId =>
if fvarUses.contains id then fvarUses.insert baseId else fvarUses
@@ -461,7 +464,7 @@ def unusedVariables : Linter where
let fvarUses fvarUsesRef.get
-- If any of the `fvar`s corresponding to this declaration is (an alias of) a variable in
-- `fvarUses`, then it is used
if aliases.any fun id => fvarUses.contains (fvarAliases.getD id id) then continue
if aliases.any fun id => fvarUses.contains (getCanonVar id) then continue
-- If this is a global declaration then it is (potentially) used after the command
if s.constDecls.contains range then continue
@@ -493,10 +496,12 @@ def unusedVariables : Linter where
if !initializedMVars then
-- collect additional `fvarUses` from tactic assignments
visitAssignments ( IO.mkRef {}) fvarUsesRef s.assignments
-- Resolve potential aliases again to preserve `fvarUsesRef` invariant
fvarUsesRef.modify fun fvarUses => fvarUses.fold (·.insert <| getCanonVar ·) {}
initializedMVars := true
let fvarUses fvarUsesRef.get
-- Redo the initial check because `fvarUses` could be bigger now
if aliases.any fun id => fvarUses.contains (fvarAliases.getD id id) then continue
if aliases.any fun id => fvarUses.contains (getCanonVar id) then continue
-- If we made it this far then the variable is unused and not ignored
unused := unused.push (declStx, userName)

View File

@@ -199,9 +199,8 @@ Performs a possibly type-changing transformation to a `MatcherApp`.
If `useSplitter` is true, the matcher is replaced with the splitter.
NB: Not all operations on `MatcherApp` can handle one `matcherName` is a splitter.
The array `addEqualities`, if provided, indicates for which of the discriminants an equality
connecting the discriminant to the parameters of the alternative (like in `match h : x with …`)
should be added (if it is isn't already there).
If `addEqualities` is true, then equalities connecting the discriminant to the parameters of the
alternative (like in `match h : x with …`) are be added, if not already there.
This function works even if the the type of alternatives do *not* fit the inferred type. This
allows you to post-process the `MatcherApp` with `MatcherApp.inferMatchType`, which will
@@ -212,20 +211,13 @@ def transform
[AddMessageContext n] [MonadOptions n]
(matcherApp : MatcherApp)
(useSplitter := false)
(addEqualities : Array Bool := mkArray matcherApp.discrs.size false)
(addEqualities : Bool := false)
(onParams : Expr n Expr := pure)
(onMotive : Array Expr Expr n Expr := fun _ e => pure e)
(onAlt : Expr Expr n Expr := fun _ e => pure e)
(onRemaining : Array Expr n (Array Expr) := pure) :
n MatcherApp := do
if addEqualities.size != matcherApp.discrs.size then
throwError "MatcherApp.transform: addEqualities has wrong size"
-- Do not add equalities when the matcher already does so
let addEqualities := Array.zipWith addEqualities matcherApp.discrInfos fun b di =>
if di.hName?.isSome then false else b
-- We also handle CasesOn applications here, and need to treat them specially in a
-- few places.
-- TODO: Expand MatcherApp with the necessary fields to make this more uniform
@@ -241,17 +233,26 @@ def transform
let params' matcherApp.params.mapM onParams
let discrs' matcherApp.discrs.mapM onParams
let (motive', uElim) lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do
let (motive', uElim, addHEqualities) lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do
unless motiveArgs.size == matcherApp.discrs.size do
throwError "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments"
let mut motiveBody' onMotive motiveArgs motiveBody
-- Prepend (x = e) → to the motive when an equality is requested
for arg in motiveArgs, discr in discrs', b in addEqualities do if b then
motiveBody' liftMetaM <| mkArrow ( mkEq discr arg) motiveBody'
-- Prepend `(x = e) →` or `(HEq x e) → ` to the motive when an equality is requested
-- and not already present, and remember whether we added an Eq or a HEq
let mut addHEqualities : Array (Option Bool) := #[]
for arg in motiveArgs, discr in discrs', di in matcherApp.discrInfos do
if addEqualities && di.hName?.isNone then
if isProof arg then
addHEqualities := addHEqualities.push none
else
let heq mkEqHEq discr arg
motiveBody' liftMetaM <| mkArrow heq motiveBody'
addHEqualities := addHEqualities.push heq.isHEq
else
addHEqualities := addHEqualities.push none
return ( mkLambdaFVars motiveArgs motiveBody', getLevel motiveBody')
return ( mkLambdaFVars motiveArgs motiveBody', getLevel motiveBody', addHEqualities)
let matcherLevels match matcherApp.uElimPos? with
| none => pure matcherApp.matcherLevels
@@ -261,15 +262,14 @@ def transform
-- (and count them along the way)
let mut remaining' := #[]
let mut extraEqualities : Nat := 0
for discr in discrs'.reverse, b in addEqualities.reverse do if b then
remaining' := remaining'.push ( mkEqRefl discr)
extraEqualities := extraEqualities + 1
for discr in discrs'.reverse, b in addHEqualities.reverse do
match b with
| none => pure ()
| some is_heq =>
remaining' := remaining'.push ( (if is_heq then mkHEqRefl else mkEqRefl) discr)
extraEqualities := extraEqualities + 1
if useSplitter && !isCasesOn then
-- We replace the matcher with the splitter
let matchEqns Match.getEquationsFor matcherApp.matcherName
let splitter := matchEqns.splitterName
let aux1 := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) params'
let aux1 := mkApp aux1 motive'
let aux1 := mkAppN aux1 discrs'
@@ -278,6 +278,10 @@ def transform
check aux1
let origAltTypes inferArgumentTypesN matcherApp.alts.size aux1
-- We replace the matcher with the splitter
let matchEqns Match.getEquationsFor matcherApp.matcherName
let splitter := matchEqns.splitterName
let aux2 := mkAppN (mkConst splitter matcherLevels.toList) params'
let aux2 := mkApp aux2 motive'
let aux2 := mkAppN aux2 discrs'

View File

@@ -8,7 +8,6 @@ prelude
import Lean.Meta.Basic
import Lean.Meta.Match.MatcherApp.Transform
import Lean.Meta.Check
import Lean.Meta.Tactic.Cleanup
import Lean.Meta.Tactic.Subst
import Lean.Meta.Injective -- for elimOptParam
import Lean.Meta.ArgsPacker
@@ -402,19 +401,51 @@ def assertIHs (vals : Array Expr) (mvarid : MVarId) : MetaM MVarId := do
mvarid mvarid.assert (.mkSimple s!"ih{i+1}") ( inferType v) v
return mvarid
/--
Substitutes equations, but makes sure to only substitute variables introduced after the motives
(given by the index) as the motive could depend on anything before, and `substVar` would happily
drop equations about these fixed parameters.
Goal cleanup:
Substitutes equations (with `substVar`) to remove superfluous varialbes, and clears unused
let bindings.
Substitutes from the outside in so that the inner-bound variable name wins, but does a first pass
looking only at variables with names with macro scope, so that preferably they disappear.
Careful to only touch the context after the motives (given by the index) as the motive could depend
on anything before, and `substVar` would happily drop equations about these fixed parameters.
-/
def substVarAfter (mvarId : MVarId) (index : Nat) : MetaM MVarId := do
mvarId.withContext do
let mut mvarId := mvarId
for localDecl in ( getLCtx) do
if localDecl.index > index then
mvarId trySubstVar mvarId localDecl.fvarId
return mvarId
partial def cleanupAfter (mvarId : MVarId) (index : Nat) : MetaM MVarId := do
let mvarId go mvarId index true
let mvarId go mvarId index false
return mvarId
where
go (mvarId : MVarId) (index : Nat) (firstPass : Bool) : MetaM MVarId := do
if let some mvarId cleanupAfter? mvarId index firstPass then
go mvarId index firstPass
else
return mvarId
allHeqToEq (mvarId : MVarId) (index : Nat) : MetaM MVarId :=
mvarId.withContext do
let mut mvarId := mvarId
for localDecl in ( getLCtx) do
if localDecl.index > index then
let (_, mvarId') heqToEq mvarId localDecl.fvarId
mvarId := mvarId'
return mvarId
cleanupAfter? (mvarId : MVarId) (index : Nat) (firstPass : Bool) : MetaM (Option MVarId) := do
mvarId.withContext do
for localDecl in ( getLCtx) do
if localDecl.index > index && (!firstPass || localDecl.userName.hasMacroScopes) then
if localDecl.isLet then
if let some mvarId' observing? <| mvarId.clear localDecl.fvarId then
return some mvarId'
if let some mvarId' substVar? mvarId localDecl.fvarId then
-- After substituting, some HEq might turn into Eqs, and we want to be able to substitute
-- them as well
let mvarId' allHeqToEq mvarId' index
return some mvarId'
return none
/--
Second helper monad collecting the cases as mvars
@@ -429,7 +460,7 @@ def M2.branch {α} (act : M2 α) : M2 α :=
/-- Base case of `buildInductionBody`: Construct a case for the final induction hypthesis. -/
def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr Option Expr) (toClear toPreserve : Array FVarId)
def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr Option Expr) (toClear : Array FVarId)
(goal : Expr) (e : Expr) : M2 Expr := do
let _e' foldAndCollect oldIH newIH isRecCall e
let IHs : Array Expr M.ask
@@ -441,8 +472,6 @@ def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr)
trace[Meta.FunInd] "Goal before cleanup:{mvarId}"
for fvarId in toClear do
mvarId mvarId.clear fvarId
mvarId mvarId.cleanup (toPreserve := toPreserve)
trace[Meta.FunInd] "Goal after cleanup (toClear := {toClear.map mkFVar}) (toPreserve := {toPreserve.map mkFVar}):{mvarId}"
modify (·.push mvarId)
let mvar instantiateMVars mvar
pure mvar
@@ -457,7 +486,7 @@ Like `mkLambdaFVars (usedOnly := true)`, but
The result `r` can be applied with `r.beta (maskArray mask args)`.
We use this when generating the functional induction principle to refine the goal through a `match`,
here `xs` are the discriminans of the `match`.
here `xs` are the discriminants of the `match`.
We do not expect non-trivial discriminants to appear in the goal (and if they do, the user will
get a helpful equality into the context).
-/
@@ -487,7 +516,7 @@ Builds an expression of type `goal` by replicating the expression `e` into its t
where it calls `buildInductionCase`. Collects the cases of the final induction hypothesis
as `MVars` as it goes.
-/
partial def buildInductionBody (toClear toPreserve : Array FVarId) (goal : Expr)
partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
(oldIH newIH : FVarId) (isRecCall : Expr Option Expr) (e : Expr) : M2 Expr := do
-- if-then-else cause case split:
@@ -496,10 +525,10 @@ partial def buildInductionBody (toClear toPreserve : Array FVarId) (goal : Expr)
let c' foldAndCollect oldIH newIH isRecCall c
let h' foldAndCollect oldIH newIH isRecCall h
let t' withLocalDecl `h .default c' fun h => M2.branch do
let t' buildInductionBody toClear (toPreserve.push h.fvarId!) goal oldIH newIH isRecCall t
let t' buildInductionBody toClear goal oldIH newIH isRecCall t
mkLambdaFVars #[h] t'
let f' withLocalDecl `h .default (mkNot c') fun h => M2.branch do
let f' buildInductionBody toClear (toPreserve.push h.fvarId!) goal oldIH newIH isRecCall f
let f' buildInductionBody toClear goal oldIH newIH isRecCall f
mkLambdaFVars #[h] f'
let u getLevel goal
return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
@@ -508,11 +537,11 @@ partial def buildInductionBody (toClear toPreserve : Array FVarId) (goal : Expr)
let h' foldAndCollect oldIH newIH isRecCall h
let t' withLocalDecl `h .default c' fun h => M2.branch do
let t instantiateLambda t #[h]
let t' buildInductionBody toClear (toPreserve.push h.fvarId!) goal oldIH newIH isRecCall t
let t' buildInductionBody toClear goal oldIH newIH isRecCall t
mkLambdaFVars #[h] t'
let f' withLocalDecl `h .default (mkNot c') fun h => M2.branch do
let f instantiateLambda f #[h]
let f' buildInductionBody toClear (toPreserve.push h.fvarId!) goal oldIH newIH isRecCall f
let f' buildInductionBody toClear goal oldIH newIH isRecCall f
mkLambdaFVars #[h] f'
let u getLevel goal
return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
@@ -523,8 +552,8 @@ partial def buildInductionBody (toClear toPreserve : Array FVarId) (goal : Expr)
match_expr goal with
| And goal₁ goal₂ => match_expr e with
| PProd.mk _α _β e₁ e₂ =>
let e₁' buildInductionBody toClear toPreserve goal₁ oldIH newIH isRecCall e₁
let e₂' buildInductionBody toClear toPreserve goal₂ oldIH newIH isRecCall e₂
let e₁' buildInductionBody toClear goal₁ oldIH newIH isRecCall e₁
let e₂' buildInductionBody toClear goal₂ oldIH newIH isRecCall e₂
return mkApp4 (.const ``And.intro []) goal₁ goal₂ e₁' e₂'
| _ =>
throwError "Goal is PProd, but expression is:{indentExpr e}"
@@ -543,14 +572,14 @@ partial def buildInductionBody (toClear toPreserve : Array FVarId) (goal : Expr)
-- so we need to replace that IH
if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then
let matcherApp' matcherApp.transform (useSplitter := true)
(addEqualities := mask.map not)
(addEqualities := true)
(onParams := (foldAndCollect oldIH newIH isRecCall ·))
(onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
(onAlt := fun expAltType alt => M2.branch do
removeLamda alt fun oldIH' alt => do
forallBoundedTelescope expAltType (some 1) fun newIH' goal' => do
let #[newIH'] := newIH' | unreachable!
let alt' buildInductionBody (toClear.push newIH'.fvarId!) toPreserve goal' oldIH' newIH'.fvarId! isRecCall alt
let alt' buildInductionBody (toClear.push newIH'.fvarId!) goal' oldIH' newIH'.fvarId! isRecCall alt
mkLambdaFVars #[newIH'] alt')
(onRemaining := fun _ => pure #[.fvar newIH])
return matcherApp'.toExpr
@@ -562,32 +591,34 @@ partial def buildInductionBody (toClear toPreserve : Array FVarId) (goal : Expr)
let (mask, absMotiveBody) mkLambdaFVarsMasked matcherApp.discrs goal
let matcherApp' matcherApp.transform (useSplitter := true)
(addEqualities := mask.map not)
(addEqualities := true)
(onParams := (foldAndCollect oldIH newIH isRecCall ·))
(onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
(onAlt := fun expAltType alt => M2.branch do
buildInductionBody toClear toPreserve expAltType oldIH newIH isRecCall alt)
buildInductionBody toClear expAltType oldIH newIH isRecCall alt)
return matcherApp'.toExpr
if let .letE n t v b _ := e then
let t' foldAndCollect oldIH newIH isRecCall t
let v' foldAndCollect oldIH newIH isRecCall v
return withLetDecl n t' v' fun x => M2.branch do
let b' buildInductionBody toClear toPreserve goal oldIH newIH isRecCall (b.instantiate1 x)
let b' buildInductionBody toClear goal oldIH newIH isRecCall (b.instantiate1 x)
mkLetFVars #[x] b'
if let some (n, t, v, b) := e.letFun? then
let t' foldAndCollect oldIH newIH isRecCall t
let v' foldAndCollect oldIH newIH isRecCall v
return withLocalDecl n .default t' fun x => M2.branch do
let b' buildInductionBody toClear toPreserve goal oldIH newIH isRecCall (b.instantiate1 x)
let b' buildInductionBody toClear goal oldIH newIH isRecCall (b.instantiate1 x)
mkLetFun x v' b'
liftM <| buildInductionCase oldIH newIH isRecCall toClear toPreserve goal e
liftM <| buildInductionCase oldIH newIH isRecCall toClear goal e
/--
Given an expression `e` with metavariables
* collects all these meta-variables,
Given an expression `e` with metavariables `mvars`
* performs more cleanup:
* removes unused let-expressions after index `index`
* tries to substitute variables after index `index`
* lifts them to the current context by reverting all local declarations after index `index`
* introducing a local variable for each of the meta variable
* assigning that local variable to the mvar
@@ -605,7 +636,7 @@ do not handle delayed assignemnts correctly.
def abstractIndependentMVars (mvars : Array MVarId) (index : Nat) (e : Expr) : MetaM Expr := do
trace[Meta.FunInd] "abstractIndependentMVars, to revert after {index}, original mvars: {mvars}"
let mvars mvars.mapM fun mvar => do
let mvar substVarAfter mvar index
let mvar cleanupAfter mvar index
mvar.withContext do
let fvarIds := ( getLCtx).foldl (init := #[]) (start := index+1) fun fvarIds decl => fvarIds.push decl.fvarId
let (_, mvar) mvar.revert fvarIds
@@ -662,7 +693,7 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
let body instantiateLambda body targets
removeLamda body fun oldIH body => do
let body instantiateLambda body extraParams
let body' buildInductionBody #[genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
let body' buildInductionBody #[genIH.fvarId!] goal oldIH genIH.fvarId! isRecCall body
if body'.containsFVar oldIH then
throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
mkLambdaFVars (targets.push genIH) ( mkLambdaFVars extraParams body')
@@ -972,7 +1003,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
removeLamda body fun oldIH body => do
trace[Meta.FunInd] "replacing {Expr.fvar oldIH} with {genIH}"
let body instantiateLambda body extraParams
let body' buildInductionBody #[genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
let body' buildInductionBody #[genIH.fvarId!] goal oldIH genIH.fvarId! isRecCall body
if body'.containsFVar oldIH then
throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
mkLambdaFVars (targets.push genIH) ( mkLambdaFVars extraParams body')

View File

@@ -51,7 +51,7 @@ Helper function for reducing homogenous binary bitvector operators.
else
return .continue
/-- Simplification procedure for `zeroExtend` and `signExtend` on `BitVec`s. -/
/-- Simplification procedure for `setWidth`, `zeroExtend` and `signExtend` on `BitVec`s. -/
@[inline] def reduceExtend (declName : Name)
(op : {n : Nat} (m : Nat) BitVec n BitVec m) (e : Expr) : SimpM DStep := do
unless e.isAppOfArity declName 3 do return .continue
@@ -253,13 +253,13 @@ builtin_dsimproc [simp, seval] reduceSLT (BitVec.slt _ _) :=
builtin_dsimproc [simp, seval] reduceSLE (BitVec.sle _ _) :=
reduceBoolPred ``BitVec.sle 3 BitVec.sle
/-- Simplification procedure for `zeroExtend'` on `BitVec`s. -/
builtin_dsimproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do
let_expr zeroExtend' _ w _ v e | return .continue
/-- Simplification procedure for `setWidth'` on `BitVec`s. -/
builtin_dsimproc [simp, seval] reduceSetWidth' (setWidth' _ _) := fun e => do
let_expr setWidth' _ w _ v e | return .continue
let some v fromExpr? v | return .continue
let some w Nat.fromExpr? w | return .continue
if h : v.n w then
return .done <| toExpr (v.value.zeroExtend' h)
return .done <| toExpr (v.value.setWidth' h)
else
return .continue
@@ -285,6 +285,9 @@ builtin_dsimproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
let some i Nat.fromExpr? i | return .continue
return .done <| toExpr (v.value.replicate i)
/-- Simplification procedure for `setWidth` on `BitVec`s. -/
builtin_dsimproc [simp, seval] reduceSetWidth (setWidth _ _) := reduceExtend ``setWidth setWidth
/-- Simplification procedure for `zeroExtend` on `BitVec`s. -/
builtin_dsimproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := reduceExtend ``zeroExtend zeroExtend

View File

@@ -451,6 +451,15 @@ def withAnonymousAntiquot := leading_parser
@[builtin_term_parser] def «trailing_parser» := leading_parser:leadPrec
"trailing_parser" >> optExprPrecedence >> optExprPrecedence >> ppSpace >> termParser
/--
Indicates that an argument to a function marked `@[extern]` is borrowed.
Being borrowed only affects the ABI and runtime behavior of the function when compiled or interpreted. From the perspective of Lean's type system, this annotation has no effect. It similarly has no effect on functions not marked `@[extern]`.
When a function argument is borrowed, the function does not consume the value. This means that the function will not decrement the value's reference count or deallocate it, and the caller is responsible for doing so.
Please see https://lean-lang.org/lean4/doc/dev/ffi.html#borrowing for a complete description.
-/
@[builtin_term_parser] def borrowed := leading_parser
"@& " >> termParser leadPrec
/-- A literal of type `Name`. -/
@@ -754,7 +763,7 @@ We use them to implement `macro_rules` and `elab_rules`
def namedArgument := leading_parser (withAnonymousAntiquot := false)
atomic ("(" >> ident >> " := ") >> withoutPosition termParser >> ")"
def ellipsis := leading_parser (withAnonymousAntiquot := false)
".." >> notFollowedBy "." "`.` immediately after `..`"
".." >> notFollowedBy (checkNoWsBefore >> ".") "`.` immediately after `..`"
def argument :=
checkWsBefore "expected space" >>
checkColGt "expected to be indented" >>

View File

@@ -5,19 +5,18 @@ Authors: Leonardo de Moura
-/
prelude
import Init.ShareCommon
import Lean.Data.HashSet
import Lean.Data.HashMap
import Std.Data.HashSet
import Std.Data.HashMap
import Lean.Data.PersistentHashMap
import Lean.Data.PersistentHashSet
open ShareCommon
namespace Lean.ShareCommon
set_option linter.deprecated false in
def objectFactory :=
StateFactory.mk {
Map := HashMap, mkMap := (mkHashMap ·), mapFind? := (·.find?), mapInsert := (·.insert)
Set := HashSet, mkSet := (mkHashSet ·), setFind? := (·.find?), setInsert := (·.insert)
Map := Std.HashMap, mkMap := (Std.HashMap.empty ·), mapFind? := (·.get?), mapInsert := (·.insert)
Set := Std.HashSet, mkSet := (Std.HashSet.empty ·), setFind? := (·.get?), setInsert := (·.insert)
}
def persistentObjectFactory :=

View File

@@ -67,7 +67,7 @@ theorem atomToCNF_eval :
theorem gateToCNF_eval :
(gateToCNF output lhs rhs linv rinv).eval assign
=
(assign output == ((xor (assign lhs) linv) && (xor (assign rhs) rinv))) := by
(assign output == (((assign lhs) ^^ linv) && ((assign rhs) ^^ rinv))) := by
simp only [CNF.eval, gateToCNF, CNF.Clause.eval, List.all_cons, List.any_cons, beq_false,
List.any_nil, Bool.or_false, beq_true, List.all_nil, Bool.and_true]
cases assign output

View File

@@ -32,7 +32,7 @@ private theorem or_as_aig : ∀ (a b : Bool), (!(!a && !b)) = (a || b) := by
/--
Encoding of XOR as boolean expression in AIG form.
-/
private theorem xor_as_aig : (a b : Bool), (!(a && b) && !(!a && !b)) = (xor a b) := by
private theorem xor_as_aig : (a b : Bool), (!(a && b) && !(!a && !b)) = (a ^^ b) := by
decide
/--

View File

@@ -92,11 +92,7 @@ instance : LawfulOperator α GateInput mkGate where
theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
aig.mkGate input, assign
=
(
(xor aig, input.lhs.ref, assign input.lhs.inv)
&&
(xor aig, input.rhs.ref, assign input.rhs.inv)
) := by
((aig, input.lhs.ref, assign ^^ input.lhs.inv) && (aig, input.rhs.ref, assign ^^ input.rhs.inv)) := by
conv =>
lhs
unfold denote denote.go
@@ -224,9 +220,9 @@ theorem denote_idx_gate {aig : AIG α} {hstart} (h : aig.decls[start] = .gate lh
aig, start, hstart, assign
=
(
(xor aig, lhs, by have := aig.invariant hstart h; omega, assign linv)
(aig, lhs, by have := aig.invariant hstart h; omega, assign ^^ linv)
&&
(xor aig, rhs, by have := aig.invariant hstart h; omega, assign rinv)
(aig, rhs, by have := aig.invariant hstart h; omega, assign ^^ rinv)
) := by
unfold denote
conv =>

View File

@@ -67,7 +67,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
simp [go, hidx, denote_blastVar]
| zeroExtend v inner ih =>
simp only [go, denote_blastZeroExtend, ih, dite_eq_ite, Bool.if_false_right,
eval_zeroExtend, BitVec.getLsbD_zeroExtend, hidx, decide_True, Bool.true_and,
eval_zeroExtend, BitVec.getLsbD_setWidth, hidx, decide_True, Bool.true_and,
Bool.and_iff_right_iff_imp, decide_eq_true_eq]
apply BitVec.lt_of_getLsbD
| append lhs rhs lih rih =>
@@ -93,9 +93,9 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
rw [blastSignExtend_empty_eq_zeroExtend] at hgo
· rw [ hgo]
simp only [eval_signExtend]
rw [BitVec.signExtend_eq_not_zeroExtend_not_of_msb_false]
rw [BitVec.signExtend_eq_not_setWidth_not_of_msb_false]
· simp only [denote_blastZeroExtend, ih, dite_eq_ite, Bool.if_false_right,
BitVec.getLsbD_zeroExtend, hidx, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp,
BitVec.getLsbD_setWidth, hidx, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp,
decide_eq_true_eq]
apply BitVec.lt_of_getLsbD
· subst heq

View File

@@ -27,7 +27,7 @@ namespace blastAdd
theorem denote_mkFullAdderOut (assign : α Bool) (aig : AIG α) (input : FullAdderInput aig) :
mkFullAdderOut aig input, assign
=
xor (xor aig, input.lhs, assign aig, input.rhs, assign) aig, input.cin, assign
((aig, input.lhs, assign ^^ aig, input.rhs, assign) ^^ aig, input.cin, assign)
:= by
simp only [mkFullAdderOut, Ref.cast_eq, denote_mkXorCached, denote_projected_entry, Bool.bne_assoc,
Bool.bne_left_inj]
@@ -37,10 +37,7 @@ theorem denote_mkFullAdderOut (assign : α → Bool) (aig : AIG α) (input : Ful
theorem denote_mkFullAdderCarry (assign : α Bool) (aig : AIG α) (input : FullAdderInput aig) :
mkFullAdderCarry aig input, assign
=
((xor
aig, input.lhs, assign
aig, input.rhs, assign) &&
aig, input.cin, assign ||
((aig, input.lhs, assign ^^ aig, input.rhs, assign) && aig, input.cin, assign ||
aig, input.lhs, assign && aig, input.rhs, assign)
:= by
simp only [mkFullAdderCarry, Ref.cast_eq, Int.reduceNeg, denote_mkOrCached,
@@ -133,7 +130,7 @@ theorem go_get (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig)
theorem atLeastTwo_eq_halfAdder (lhsBit rhsBit carry : Bool) :
Bool.atLeastTwo lhsBit rhsBit carry
=
(((xor lhsBit rhsBit) && carry) || (lhsBit && rhsBit)) := by
(((lhsBit ^^ rhsBit) && carry) || (lhsBit && rhsBit)) := by
revert lhsBit rhsBit carry
decide

View File

@@ -33,7 +33,7 @@ def toString : Gate → String
def eval : Gate Bool Bool Bool
| and => (· && ·)
| or => (· || ·)
| xor => Bool.xor
| xor => (· ^^ ·)
| beq => (· == ·)
| imp => (!· || ·)

View File

@@ -72,7 +72,7 @@ theorem check_sound (lratProof : Array IntAction) (cnf : CNF Nat) :
simp [ h2, WellFormedAction]
. simp only [Option.some.injEq] at h2
simp [ h2, WellFormedAction]
. simp only [ite_some_none_eq_some] at h2
. simp only [Option.ite_none_right_eq_some, Option.some.injEq] at h2
rcases h2 with hleft, hright
simp [WellFormedAction, hleft, hright, Clause.limplies_iff_mem]
)

View File

@@ -56,8 +56,8 @@ attribute [bv_normalize] BitVec.zero_add
attribute [bv_normalize] BitVec.neg_zero
attribute [bv_normalize] BitVec.sub_self
attribute [bv_normalize] BitVec.sub_zero
attribute [bv_normalize] BitVec.zeroExtend_eq
attribute [bv_normalize] BitVec.zeroExtend_zero
attribute [bv_normalize] BitVec.setWidth_eq
attribute [bv_normalize] BitVec.setWidth_zero
attribute [bv_normalize] BitVec.getLsbD_zero
attribute [bv_normalize] BitVec.getLsbD_zero_length
attribute [bv_normalize] BitVec.getLsbD_concat_zero
@@ -206,5 +206,17 @@ theorem BitVec.max_ult' (a : BitVec w) : (BitVec.ult (-1#w) a) = false := by
attribute [bv_normalize] BitVec.replicate_zero_eq
@[bv_normalize]
theorem BitVec.ofBool_getLsbD (a : BitVec w) (i : Nat) :
BitVec.ofBool (a.getLsbD i) = a.extractLsb' i 1 := by
ext j
simp
@[bv_normalize]
theorem BitVec.ofBool_getElem (a : BitVec w) (i : Nat) (h : i < w) :
BitVec.ofBool a[i] = a.extractLsb' i 1 := by
rw [ BitVec.getLsbD_eq_getElem]
apply ofBool_getLsbD
end Normalize
end Std.Tactic.BVDecide

View File

@@ -46,7 +46,7 @@ attribute [bv_normalize] Bool.and_self_left
attribute [bv_normalize] Bool.and_self_right
@[bv_normalize]
theorem Bool.not_xor : (a b : Bool), !(xor a b) = (a == b) := by decide
theorem Bool.not_xor : (a b : Bool), !(a ^^ b) = (a == b) := by decide
end Normalize
end Std.Tactic.BVDecide

View File

@@ -126,7 +126,7 @@ theorem or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
simp[*]
theorem xor_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
(Bool.xor lhs' rhs') = (xor lhs rhs) := by
(lhs' ^^ rhs') = (lhs ^^ rhs) := by
simp[*]
theorem beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :

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.

View File

@@ -29,7 +29,7 @@ def parity32_spec_rec (i : Nat) (x : BitVec 32) : Bool :=
| 0 => false
| i' + 1 =>
let bit_idx := BitVec.getLsbD x i'
Bool.xor bit_idx (parity32_spec_rec i' x)
bit_idx ^^ (parity32_spec_rec i' x)
def parity32_spec (x : BitVec 32) : Bool :=
parity32_spec_rec 32 x

View File

@@ -55,8 +55,8 @@ a : α
• Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
• a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
• FVarAlias a
• FVarAlias α
• FVarAlias a: _uniq.636 -> _uniq.312
• FVarAlias α: _uniq.635 -> _uniq.310
• ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
• [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
• Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -70,8 +70,8 @@ a : α
• Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
• n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
• a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
• FVarAlias a
• FVarAlias n
• FVarAlias a: _uniq.667 -> _uniq.312
• FVarAlias n: _uniq.666 -> _uniq.310
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
• [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩

View File

@@ -46,6 +46,30 @@
"position": {"line": 9, "character": 11}},
"id": {"const": {"declName": "BitVec.getMsbD_ofBoolListBE"}}}},
{"sortText": "4",
"label": "BitVec.ofBool_and_ofBool",
"kind": 3,
"data":
{"params":
{"textDocument": {"uri": "file:///completionPrv.lean"},
"position": {"line": 9, "character": 11}},
"id": {"const": {"declName": "BitVec.ofBool_and_ofBool"}}}},
{"sortText": "5",
"label": "BitVec.ofBool_or_ofBool",
"kind": 3,
"data":
{"params":
{"textDocument": {"uri": "file:///completionPrv.lean"},
"position": {"line": 9, "character": 11}},
"id": {"const": {"declName": "BitVec.ofBool_or_ofBool"}}}},
{"sortText": "6",
"label": "BitVec.ofBool_xor_ofBool",
"kind": 3,
"data":
{"params":
{"textDocument": {"uri": "file:///completionPrv.lean"},
"position": {"line": 9, "character": 11}},
"id": {"const": {"declName": "BitVec.ofBool_xor_ofBool"}}}},
{"sortText": "7",
"label": "BitVec.ofBoolListBE",
"kind": 3,
"documentation":

View File

@@ -250,6 +250,17 @@ example [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f
example {α β} [ord : Ord β] (f : α β) (x y : α) : Ordering := compare (f x) (f y)
example {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
inductive A where
| intro : Nat A
def A.out : A Nat
| .intro n => n
/-! `h` is used indirectly via an alias introduced by `match` that is used only via the mvar ctx -/
theorem problematicAlias (n : A) (i : Nat) (h : i n.out) : i n.out :=
match n with
| .intro _ => by assumption
/-!
The wildcard pattern introduces a copy of `x` that should not be linted as it is in an
inaccessible annotation.

10
tests/lean/run/4768.lean Normal file
View File

@@ -0,0 +1,10 @@
/-!
Test that `..` tokens do not break nearby `.`s.
Note that this tests specifically for issues with `.` that are not present with `·`.
-/
example : True True := by
constructor
refine trivial ..
. trivial -- this has to be . not · for this test to be useful

19
tests/lean/run/5359.lean Normal file
View File

@@ -0,0 +1,19 @@
/-!
Test that `Iff.rfl` is tried by the `rfl` tactic.
-/
universe u v w
class L (F : Sort u) (α : outParam (Sort v)) (β : outParam (α Sort w)) where
coe : F a : α, β a
instance {F : Sort u} {α : Sort v} {β : α Sort w} [L F α β] :
CoeFun F (fun _ a : α, β a) where coe := @L.coe _ _ β _
instance {π : Nat Type u} [ i, LE (π i)] : LE ( i, π i) where le x y := i, x i y i
structure S (α : Nat Type u) where
variable {α : Nat Type u} [ i, LE (α i)]
instance : L (S α) Nat α := sorry
instance : LE (S α) := fun f g i, f i g i
example : {a b : S α}, L.coe a L.coe b a b := by rfl

View File

@@ -99,7 +99,7 @@ example (h : x) : x = (3#3 ≥ 1#3) := by
simp; guard_target = x; assumption
example (h : ¬x) : x = (3#3 4#3) := by
simp; guard_target = ¬x; assumption
example (h : x = (5 : BitVec 7)) : x = (5#3).zeroExtend' (by decide) := by
example (h : x = (5 : BitVec 7)) : x = (5#3).setWidth' (by decide) := by
simp; guard_target = x = 5#7; assumption
example (h : x = (80 : BitVec 7)) : x = (5#3).shiftLeftZeroExtend 4 := by
simp; guard_target = x = 80#7; assumption

View File

@@ -3,7 +3,7 @@ import Std.Tactic.BVDecide
open BitVec
/--
error: The prover found a potential counterexample, consider the following assignment:
error: The prover found a counterexample, consider the following assignment:
x = 0xffffffffffffffff#64
-/
#guard_msgs in
@@ -11,7 +11,7 @@ example (x : BitVec 64) : x < x + 1 := by
bv_decide
/--
error: The prover found a potential counterexample, consider the following assignment:
error: The prover found a counterexample, consider the following assignment:
x = 0x00000000000001ff#64
-/
#guard_msgs in
@@ -43,7 +43,7 @@ def optimized (x : BitVec 32) : BitVec 32 :=
x &&& 0x0000004F
/--
error: The prover found a potential counterexample, consider the following assignment:
error: The prover found a counterexample, consider the following assignment:
x = 0xffffffff#32
-/
#guard_msgs in
@@ -53,7 +53,7 @@ example (x : BitVec 32) : pop_spec' x = optimized x := by
-- limit the search domain
/--
error: The prover found a potential counterexample, consider the following assignment:
error: The prover found a counterexample, consider the following assignment:
x = 0x0007ffff#32
-/
#guard_msgs in
@@ -62,7 +62,7 @@ example (x : BitVec 32) (h1 : x < 0xfffff) : pop_spec' x = optimized x := by
bv_decide
/--
error: The prover found a potential counterexample, consider the following assignment:
error: The prover found a counterexample, consider the following assignment:
x = 0x00000000#32
y = 0x80000000#32
ofBool a = 0x1#1
@@ -70,3 +70,41 @@ ofBool a = 0x1#1
#guard_msgs in
example (x y : BitVec 32) (a : Bool) (h : x < y) : (x = y) a := by
bv_decide
-- False counter examples but correctly detected as such.
/--
error: The prover found a potentially spurious counterexample:
- The following potentially relevant hypotheses could not be used: [h]
Consider the following assignment:
x = 0xffffffff#32
y = 0x7fffffff#32
-/
#guard_msgs in
example (x y : BitVec 32) (h : x.toNat = y.toNat) : x = y := by
bv_decide
def zeros (w : Nat) : BitVec w := 0#w
/--
error: The prover found a potentially spurious counterexample:
- It abstracted the following unsupported expressions as opaque variables: [zeros 32]
Consider the following assignment:
x = 0xffffffff#32
zeros 32 = 0xffffffff#32
-/
#guard_msgs in
example (x : BitVec 32) (h : x = zeros 32) : x = 0 := by
bv_decide
/--
error: The prover found a potentially spurious counterexample:
- It abstracted the following unsupported expressions as opaque variables: [zeros 32]
- The following potentially relevant hypotheses could not be used: [h1]
Consider the following assignment:
x = 0xffffffff#32
zeros 32 = 0xffffffff#32
y = 0xffffffff#32
-/
#guard_msgs in
example (x y : BitVec 32) (h1 : x.toNat = y.toNat) (h2 : x = zeros 32) : y = 0 := by
bv_decide

View File

@@ -13,3 +13,15 @@ theorem bv_extract_3 (h : x = 1#64) : extractLsb 63 32 x = 0#32 := by
theorem bv_extract_4 (h : x = 1#64) : extractLsb 31 0 x = 1#32 := by
bv_decide
theorem bv_ofBool_1 (h : x = 1#64) : ofBool (x.getLsbD 0) = 1#1 := by
bv_decide
theorem bv_ofBool_2 (h : x = 1#64) : ofBool (x.getLsbD 1) = 0#1 := by
bv_decide
theorem bv_ofBool_3 (h : x = 1#64) : ofBool x[0] = 1#1 := by
bv_decide
theorem bv_ofBool_4 (h : x = 1#64) : ofBool x[1] = 0#1 := by
bv_decide

View File

@@ -14,7 +14,7 @@ theorem substructure_unit_1'' (x y z : BitVec 8) : (Bool.and (x = y) (y = z))
theorem substructure_unit_2 (x y : BitVec 8) : x = y y = x := by
bv_decide
theorem substructure_unit_3 (x y : BitVec 8) : xor (x = y) (y x) := by
theorem substructure_unit_3 (x y : BitVec 8) : (x = y) ^^ (y x) := by
bv_decide
theorem substructure_unit_3' (x y : BitVec 8) : Bool.xor (x = y) (y x) := by

View File

@@ -3,7 +3,7 @@ import Std.Tactic.BVDecide
open BitVec
/--
error: The prover found a potential counterexample, consider the following assignment:
error: The prover found a counterexample, consider the following assignment:
y = 0xffffffffffffffff#64
-/
#guard_msgs in

View File

@@ -7,7 +7,7 @@ theorem write_simplify_test_0 (a x y : BitVec 64)
write (2 * ((8 * 8) / 8)) a (BitVec.cast h (zeroExtend (8 * 8) x ++ (zeroExtend (8 * 8) y))) s
=
write 16 a (x ++ y) s := by
simp only [zeroExtend_eq, BitVec.cast_eq]
simp only [setWidth_eq, BitVec.cast_eq]
/--
warning: declaration uses 'sorry'

View File

@@ -54,7 +54,7 @@ termination_by structural x => x
/--
info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop)
(case1 : ∀ (x : List β), motive [] x) (case2 : ∀ (x : List α), (x = [] → False) → motive x [])
(case1 : ∀ (x : List β), motive [] x) (case2 : ∀ (t : List α), (t = [] → False) → motive t [])
(case3 : ∀ (x : α) (xs : List α) (y : β) (ys : List β), motive xs ys → motive (x :: xs) (y :: ys)) :
∀ (a : List α) (a_1 : List β), motive a a_1
-/

View File

@@ -109,11 +109,7 @@ def let_tailrec : Nat → Nat
termination_by n => n
/--
info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
(case2 :
∀ (n : Nat),
let h2 := ⋯;
motive n → motive n.succ) :
info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
∀ (a : Nat), motive a
-/
#guard_msgs in
@@ -531,7 +527,7 @@ termination_by xs => xs
/--
info: LetFun.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
(case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a
(case2 : ∀ (_y : α) (ys : List α), Nat → motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a
-/
#guard_msgs in
#check bar.induct
@@ -686,12 +682,11 @@ def foo : Nat → Nat → (k : Nat) → Fin k → Nat
termination_by n => n
/--
info: Nary.foo.induct (motive : Nat → Nat → (k : Nat) → Fin k → Prop)
(case1 : ∀ (x x_1 : Nat) (x_2 : Fin x_1), motive 0 x x_1 x_2)
(case2 : ∀ (x x_1 : Nat) (x_2 : Fin x_1), (x = 0 → False) → motive x 0 x_1 x_2)
(case3 : ∀ (x x_1 : Nat) (x_2 : Fin 0), (x = 0 → False) → (x_1 = 0 → False) → motive x x_1 0 x_2)
(case4 : ∀ (x x_1 : Nat) (x_2 : Fin 1), (x = 0 → False) → (x_1 = 0 → False) → motive x x_1 1 x_2)
(case5 : ∀ (n m k : Nat) (x : Fin (k + 2)), motive n m (k + 1) ⟨0, ⋯⟩ → motive n.succ m.succ k.succ.succ x) :
info: Nary.foo.induct (motive : Nat → Nat → (k : Nat) → Fin k → Prop) (case1 : ∀ (k x : Nat) (x_1 : Fin k), motive 0 x k x_1)
(case2 : ∀ (k x : Nat), (x = 0 → False) → ∀ (x_2 : Fin k), motive x 0 k x_2)
(case3 : ∀ (x x_1 : Nat), (x = 0 → False) → (x_1 = 0 → False) → ∀ (a : Fin 0), motive x x_1 0 a)
(case4 : ∀ (x x_1 : Nat), (x = 0 → False) → (x_1 = 0 → False) → ∀ (a : Fin 1), motive x x_1 1 a)
(case5 : ∀ (n m k : Nat) (a : Fin k.succ.succ), motive n m (k + 1) ⟨0, ⋯⟩ → motive n.succ m.succ k.succ.succ a) :
∀ (a a_1 k : Nat) (a_2 : Fin k), motive a a_1 k a_2
-/
#guard_msgs in

View File

@@ -0,0 +1,49 @@
set_option linter.unusedVariables false
def bar (n : Nat) : Bool :=
if h : n = 0 then
true
else
match n with -- NB: the elaborator adds `h` as an discriminant
| m+1 => bar m
termination_by n
-- set_option pp.match false
-- #print bar
-- #check bar.match_1
-- #print bar.induct
-- NB: The induction theorem has both `h` in scope, as its original type mentioning `x`,
-- and a refined `h` mentioning `m+1`.
-- The former is redundant here, but will we always know that?
-- No HEq betwen the two `h`s due to proof irrelevance
/--
info: bar.induct (motive : Nat → Prop) (case1 : motive 0)
(case2 : ∀ (m : Nat), ¬m + 1 = 0 → ¬m.succ = 0 → motive m → motive m.succ) (n : Nat) : motive n
-/
#guard_msgs in
#check bar.induct
def baz (n : Nat) (i : Fin (n+1)) : Bool :=
if h : n = 0 then
true
else
match n, i + 1 with
| 1, _ => true
| m+2, j => baz (m+1) j.1-1, by omega
termination_by n
-- #print baz._unary
/--
info: baz.induct (motive : (n : Nat) → Fin (n + 1) → Prop) (case1 : ∀ (i : Fin (0 + 1)), motive 0 i)
(case2 : ¬1 = 0 → ∀ (i : Fin (1 + 1)), ¬1 = 0 → motive 1 i)
(case3 :
∀ (m : Nat),
¬m + 2 = 0 →
∀ (i : Fin (m.succ.succ + 1)), ¬m.succ.succ = 0 → motive (m + 1) ⟨↑(i + 1) - 1, ⋯⟩ → motive m.succ.succ i)
(n : Nat) (i : Fin (n + 1)) : motive n i
-/
#guard_msgs in
#check baz.induct

View File

@@ -9,11 +9,9 @@ def test (x: Nat): Nat :=
-- set_option trace.Meta.FunInd true
-- At the time of writing, the induction princpile misses the `f x = some k` assumptions:
/--
info: test.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), motive x) (case2 : motive 0)
(case3 : ∀ (n : Nat), motive n → motive n.succ) (x : Nat) : motive x
info: test.induct (motive : Nat → Prop) (case1 : ∀ (t k : Nat), f t = some k → motive t) (case2 : f 0 = none → motive 0)
(case3 : ∀ (n : Nat), f n.succ = none → motive n → motive n.succ) (x : Nat) : motive x
-/
#guard_msgs in
#check test.induct

View File

@@ -506,6 +506,54 @@ example
n = 65536 := by
bv_omega
-- From https://github.com/leanprover/lean4/issues/5315
-- This used to fail with an unexpected bound variable error.
def simple_foldl (f: β α β) (a: Array α) (i: Nat) (b: β): β :=
if h: i < a.size then
simple_foldl f a (i+1) (f b a[i])
else
b
/--
error: omega could not prove the goal:
No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
-/
#guard_msgs in
theorem simple_fold_monotonic₁ (a: Array α) (f: β α β) (i: Nat) {P: α β Prop} {x: α}
(base: P x b)
(mono: x x' y, P x y P x (f y x')): P x (simple_foldl f a i b) := by
unfold simple_foldl
split <;> try trivial
apply simple_fold_monotonic₁
. apply mono; exact base
. exact mono
termination_by a.size - i
decreasing_by
exfalso
rename_i a b
clear a b mono base
rename_i a; clear a
clear base
clear x
rename_i a; clear a
clear x
clear P
rename_i a; clear a
clear P
clear i
rename_i a; clear a
clear i
clear f
rename_i a; clear a
clear f
clear a
rename_i a; clear a
clear a
clear b
rename_i a
omega
/-! ### Error messages -/
/--

View File

@@ -21,13 +21,15 @@ example : Not
(@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))) := by
simp
@[simp] theorem OfNat.ofNat_ofNat : OfNat.ofNat (no_index OfNat.ofNat n) = OfNat.ofNat n := rfl
example : Not
(@Eq.{1} Nat
(@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instMod)
(@OfNat.ofNat.{0} Nat 1 (@One.toOfNat1.{0} Nat (@One.ofOfNat1.{0} Nat (instOfNatNat 1))))
(@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
(@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) := by
simp
simp only [reduceCtorEq, not_false_eq_true]
def WithTop (α : Type) := Option α

View File

@@ -16,15 +16,15 @@ namespace Foo
def f x y := x + y + 1
scoped infix:70 "^^" => f
scoped infix:70 "~~" => f
#check 1 ^^ 2
#check 1 ~~ 2
theorem ex1 : x ^^ y = f x y := rfl
theorem ex1 : x ~~ y = f x y := rfl
end Foo
#check 1 ^^ 2 -- works because we have an `open Foo` above
#check 1 ~~ 2 -- works because we have an `open Foo` above
theorem ex2 : x ^^ y = f x y := rfl
theorem ex3 : x ^^ y = Foo.f x y := rfl
theorem ex2 : x ~~ y = f x y := rfl
theorem ex3 : x ~~ y = Foo.f x y := rfl