max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
33961 commits 1 branch 0 tags 5.3 GiB
Commit graph

3412 commits

Author SHA1 Message Date
Kim Morrison
c7819bd6eb
chore: missing List.set_replicate_self (#5460) 2024-09-25 01:15:24 +00:00
Kim Morrison
a4fb740d2f
chore: missing BitVec lemmas (#5459) 2024-09-25 01:06:39 +00:00
Kyle Miller
ea75c924a1
feat: add heq_comm (#5456) 
Requested [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/heq_comm/near/472516757).
 2024-09-24 23:36:00 +00:00
Kim Morrison
65f4b92505
chore: cleanup of Array docstrings after refactor (#5458) 
Sorry this is coming through in tiny pieces; I'm still hitting a
bootstrapping problem and getting things through piecemeal to localise
it.
 2024-09-24 23:16:49 +00:00
Kim Morrison
a6f0112fc5
feat: refactor of Array (#5452) 
This is a second attempt at #5446, first reverting parts of #5403.
 2024-09-24 12:57:55 +00:00
Kim Morrison
eee0553318
chore: make some instance arguments implicit (#5454) 
This was causing a few unnecessary `_` downstream.
 2024-09-24 12:57:46 +00:00
Tobias Grosser
5d2c7fc1d9
feat: more of BitVec.getElem_* (#5404) 2024-09-24 08:04:39 +00:00
Kim Morrison
b612403980
chore: update copyrights (#5449) 2024-09-24 05:27:53 +00:00
Kim Morrison
6b0d4e50c0
chore: update Pi instance names (#5447) 
Override instance names for nonempty / inhabited / subsingleton arrows,
per
[zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pi.20instance.20names.20in.20Lean.204.20core/near/466248246).
 2024-09-24 04:12:51 +00:00
Siddharth
0cae7165aa
feat: BitVec.toNat_{add,sub,mul_of_lt} for BitVector non-overflow reasoning (#5411) 
These theorems are useful when one wants to simplify the goal state,
under knowledge that the bitvector operations don't overflow. This can
produce much smaller goal states that eventually allows `bv_omega` to
quickly close the goal.

Note that the LHS of the theorem is *not* in `simp` normal form, since
e.g. `(x + y).toNat` is normalized to `(x.toNat + y.toNat) % 2^w`. It's
not immediately clear to me what should be done about this.

Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
 2024-09-24 03:54:50 +00:00
euprunin
ba43ce18c3
chore: remove repeated words (#5438) 
Co-authored-by: euprunin <euprunin@users.noreply.github.com>
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
 2024-09-24 03:40:11 +00:00
Tobias Grosser
3190be3058
feat: add LawCommIdentity + IdempotentOp for BitVec.[and|or|xor] (#5416) 
As these instances seemingly require explicit arguments, this PR also
makes some arguments explicit.
 2024-09-24 03:27:57 +00:00
euprunin
27c4c366b4
chore: remove (syntactically) duplicate imports (#5437) 
---

Related: https://github.com/leanprover-community/mathlib4/pull/16384
("feat: lint on (syntactically) duplicate imports")

Co-authored-by: euprunin <euprunin@users.noreply.github.com>
 2024-09-23 23:07:56 +00:00
euprunin
624f1b9963
chore: fix spelling mistakes in src/Init/ (#5427) 
Co-authored-by: euprunin <euprunin@users.noreply.github.com>
 2024-09-23 21:09:58 +00:00
Leonardo de Moura
fc20b5dfb4
fix: must not reduce ite in the discriminant of match-expression when reducibility setting is .reducible (#5419) 
closes #5388

See updated comment for additional details.
 2024-09-23 12:26:53 +00:00
Kim Morrison
7fba7ed7b6
feat: decidable quantifers for BitVec (#5418) 2024-09-23 11:02:49 +00:00
Kim Morrison
e551a366a0
feat: theorems about List.toArray (#5403) 2024-09-23 05:24:03 +00:00
Siddharth
f4afbc2f8b
feat: BitVec analogues of Nat.{mul_two, two_mul, mul_succ, succ_mul} (#5410) 
As requested by @hargoniX .
 2024-09-23 04:37:04 +00:00
Kim Morrison
8c8585536c
feat: refactor DecidableEq (Array α) (#5422) 2024-09-23 03:49:03 +00:00
Kim Morrison
c825b5a560
chore: reverse direction of List.set_map (#5405) 2024-09-23 03:44:11 +00:00
Kim Morrison
738435b90a
chore: make Array functions either semireducible or use structural recursion (#5420) 
Previously, it was not possible to use `decide` with most Array
functions (including `==`).

Later, we may replace some of these functions with defeqs that go via
the `List` operations, and use `csimp` lemmas for fast runtime
behaviour. In the meantime, this allows using `decide`.
 2024-09-23 02:41:41 +00:00
TomasPuverle
1883c9b7eb
feat: implement Repr Empty (#5415) 
Given the derived `Repr` instance for types with parameters, the absence
of `Repr Empty` can cause `Repr` instance synthesis to fail. For
example, given
```lean
inductive Prim (special : Type) where
  | plus
  | other : special → Prim special
deriving Repr
```
this works:
```lean
#eval (Prim.plus : Prim Int)
```
but this fails:
```lean
#eval (Prim.plus : Prim Empty)
```

---------

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
 2024-09-23 01:11:36 +00:00
Tobias Grosser
fc52015841
feat: add _self, _zero, and _allOnes for BitVec.[and|or|xor] (#5413) 
The `xor_allOnes` theorems end up in the `not` section, as the relevant
simplification lemmas are otherwise not defined.
 2024-09-22 10:10:54 +00:00
Kim Morrison
152ca85fa9
chore: reorganization in Array/Basic (#5400) 
Getting started on `Array`.
 2024-09-20 02:01:52 +00:00
Kim Morrison
0ecf2a030a
feat: List.fold relators (#5393) 2024-09-20 00:48:03 +00: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
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
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
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
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
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
Kim Morrison
c25d206647
chore: Fin.ofNat' uses NeZero (#5356) 2024-09-16 07:13:18 +00:00
Violeta Hernández
078e9b6d77
doc: add documentation for groupBy.loop (#5349) 
We add some documentation explaining the auxiliary function in the
definition of `groupBy`. This has been moved here from Mathlib PR
[16818](https://github.com/leanprover-community/mathlib4/pull/16818) by
request of @semorrison.

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
 2024-09-16 05:56:44 +00:00
Kim Morrison
a745e33123
feat: BitVec.truncate lemmas (#5357) 
These improve confluence of lemmas involving `truncate`.
 2024-09-16 05:55:50 +00:00
Kim Morrison
7740a38a71
chore: remove @[simp] from Option.bind_map (#5354) 2024-09-16 04:44:38 +00:00
Kim Morrison
9568f305d8
chore: switch primes on List.getElem_take (#5294) 
This will probably have fallout downstream, and as it is a direct name
switch I'm not going to provide any deprecations.
 2024-09-16 03:40:42 +00:00
Kim Morrison
b1179d5cc3
chore: fix implicitness of List.getElem_mem (#5331) 2024-09-16 03:28:14 +00:00