Leonardo de Moura
|
9722aeaf32
|
feat: use String.Iterator.sizeOf_next_lt in the builtin decreasing_tactic
|
2022-03-19 09:04:40 -07:00 |
|
Leonardo de Moura
|
9727387129
|
feat: helper theorem for proving termination of simple String traversal functions
|
2022-03-19 07:37:59 -07:00 |
|
Leonardo de Moura
|
64bd82dddd
|
feat: custom SizeOf instance for String.Iterator
|
2022-03-19 07:21:17 -07:00 |
|
zygi
|
ac793ce196
|
fix: forward start and stop in Array.allM
|
2022-03-17 10:08:40 +01:00 |
|
Daniel Fabian
|
cf4e873974
|
feat: support Sort u in ac_refl.
|
2022-03-16 17:21:20 -07:00 |
|
Daniel Fabian
|
d667d5ab5d
|
feat: rewrite the tactic using simp as the basis.
|
2022-03-16 17:21:20 -07:00 |
|
Daniel Fabian
|
fda1c5b192
|
refactor: simplify proof using <;>
|
2022-03-16 17:21:20 -07:00 |
|
Daniel Fabian
|
a60220b036
|
feat: add tactic for ac_refl.
|
2022-03-16 17:21:20 -07:00 |
|
Daniel Fabian
|
eaa48f0d8d
|
refactor: move ac proofs to Init.
|
2022-03-16 17:21:20 -07:00 |
|
Leonardo de Moura
|
c6dae18787
|
chore: add helper theorems
|
2022-03-14 16:24:05 -07:00 |
|
Leonardo de Moura
|
40f608bfbd
|
chore: cleanup String.extract reference implementation
|
2022-03-14 16:23:13 -07:00 |
|
Leonardo de Moura
|
8e29747fe7
|
feat: add simp theorem (a : Nat) : (a ≤ 0) = (a = 0)
|
2022-03-14 15:43:42 -07:00 |
|
Leonardo de Moura
|
14ed473777
|
feat: mark Nat.zero_le as simp theorem
|
2022-03-14 15:19:52 -07:00 |
|
Leonardo de Moura
|
cab3217b05
|
feat: add forIn'_eq_forIn theorem for lists
|
2022-03-14 11:50:47 -07:00 |
|
Sebastian Ullrich
|
82c682d385
|
chore: remove redundant proof
|
2022-03-12 11:12:56 +01:00 |
|
Leonardo de Moura
|
5caf1bc692
|
chore: style
Use `·` instead of `.` for structuring tactics.
|
2022-03-11 16:12:46 -08:00 |
|
Leonardo de Moura
|
d3b2028a05
|
feat: add Fin.succ
|
2022-03-05 17:36:38 -08:00 |
|
Leonardo de Moura
|
ef38c82c77
|
fix: missing hypotheses at List.sizeOf_lt_of_mem
|
2022-03-03 19:52:05 -08:00 |
|
Leonardo de Moura
|
99677823c3
|
fix: ForIn' instance binder annotations
|
2022-03-03 19:51:45 -08:00 |
|
Leonardo de Moura
|
d8ee03c1bb
|
feat: add ForIn' instance that is similar to ForIn but provides a proof that the iterated elements are in the collection
|
2022-03-03 19:05:27 -08:00 |
|
Leonardo de Moura
|
e1424653b9
|
chore: remove workaround
|
2022-03-03 18:16:54 -08:00 |
|
Leonardo de Moura
|
337c55f322
|
fix: missing import
|
2022-03-03 18:13:34 -08:00 |
|
Leonardo de Moura
|
aeb9b2fb8c
|
chore: add Membership instance for Array
|
2022-03-03 18:13:34 -08:00 |
|
Leonardo de Moura
|
fd519401ff
|
feat: add Membership instance for List
and the theorem `a ∈ as -> sizeOf a < sizeOf as`.
We will use theorems like this one to improve the `decreasing_tactic`.
|
2022-03-03 18:13:21 -08:00 |
|
Leonardo de Moura
|
f629be745b
|
chore: add Nat.le_refl as simp theorem
|
2022-03-03 17:18:11 -08:00 |
|
Leonardo de Moura
|
5845002e8c
|
feat: use WF at anyM
|
2022-03-03 16:43:05 -08:00 |
|
Leonardo de Moura
|
02d7cedba8
|
chore: remove unnecessary termination_by annotations
|
2022-03-03 11:24:06 -08:00 |
|
Leonardo de Moura
|
de51160929
|
fix: core library
|
2022-03-01 13:36:24 -08:00 |
|
François G. Dorais
|
e84699f130
|
fix: remove unnecessary hypotheses
|
2022-03-01 13:31:01 -08:00 |
|
Leonardo de Moura
|
89e0de9fbb
|
chore: use WF compiler to define Nat.mod and Nat.div
|
2022-03-01 13:08:59 -08:00 |
|
Leonardo de Moura
|
0f796ac804
|
chore: avoid heterogeneous polymorphic operations and add add hugeFuel at Linear.lean
|
2022-03-01 11:25:15 -08:00 |
|
Leonardo de Moura
|
9bd82b798a
|
chore: use bif instead of if at Linear.lean
|
2022-03-01 10:55:03 -08:00 |
|
Leonardo de Moura
|
da55789c26
|
feat: add a proper BEq instance for Nat
|
2022-03-01 09:01:08 -08:00 |
|
Leonardo de Moura
|
0f06fbf648
|
feat: LawfulBEq must be reflexive
|
2022-02-28 19:27:51 -08:00 |
|
Leonardo de Moura
|
e8fb0c96ac
|
feat: add helper theorems
|
2022-02-28 18:06:02 -08:00 |
|
Leonardo de Moura
|
5ddb3c3435
|
feat: faster PolyCnstr.combine
|
2022-02-28 17:24:26 -08:00 |
|
Leonardo de Moura
|
b5f28239af
|
feat: add List helper theorems
|
2022-02-28 15:16:13 -08:00 |
|
Leonardo de Moura
|
89f88b1caa
|
feat: simplify nested arith expressions
|
2022-02-27 09:01:52 -08:00 |
|
Leonardo de Moura
|
812cc72285
|
chore: add helper theorems
|
2022-02-25 17:04:04 -08:00 |
|
Leonardo de Moura
|
3f636b9f83
|
feat: add Lean.Meta.Linear.Nat.simpCnstr?
|
2022-02-25 16:27:21 -08:00 |
|
Leonardo de Moura
|
346930af9d
|
feat: add ExprCnstr.eq_of_toNormPoly_eq
|
2022-02-25 14:55:20 -08:00 |
|
Leonardo de Moura
|
b8bed6fb5c
|
feat: add LawfulBEq class
|
2022-02-25 13:35:08 -08:00 |
|
Leonardo de Moura
|
3b130ee42f
|
feat: add Poly.toExpr
|
2022-02-25 12:31:30 -08:00 |
|
Leonardo de Moura
|
be2e2cb70e
|
chore: adjust proofs affected by update stage0
|
2022-02-24 17:20:17 -08:00 |
|
Leonardo de Moura
|
05be43455a
|
feat: add src/Init/Data/Nat/Linear.lean
|
2022-02-24 13:45:17 -08:00 |
|
Leonardo de Moura
|
902e60c480
|
feat: add Format.isEmpty
|
2022-02-23 13:34:25 -08:00 |
|
Leonardo de Moura
|
8d6750469e
|
chore: helper Nat theorems
|
2022-02-22 14:26:50 -08:00 |
|
Leonardo de Moura
|
7f3a3138d0
|
feat: helper Nat theorems
|
2022-02-21 08:49:50 -08:00 |
|
Leonardo de Moura
|
ba16903205
|
feat: add helper theorems
|
2022-02-19 21:25:44 -08:00 |
|
Leonardo de Moura
|
193859c72c
|
feat: add helper theorems
|
2022-02-19 17:53:54 -08:00 |
|