max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init
History
Leonardo de Moura 6ca31baa55
feat: structure extensionality in grind (#8330) 
This PR improves support for structure extensionality in `grind`. It now
uses eta expansion for structures instead of the extensionality theorems
generated by `[ext]`. Examples:

```lean
opaque f (a : Nat) : Nat × Bool

attribute [grind ext] Prod Subtype

example (a b : Nat) : (f a).1 = (f b).1 → (f a).2 = (f b).2 → f a = f b := by
  grind

def g (a : Nat) : { x : Nat // x > 1 } :=
  ⟨a + 2, by grind⟩

example (a b : Nat) : (g a).1 = (g b).1 → g a = g b := by
  grind

@[grind ext] structure S where
  x : Nat
  y : Int

example (x y : S) : x.1 = y.1 → x.2 = y.2 → x = y := by
  grind
```
2025-05-14 02:43:52 +00:00
..
Control feat: initial @[grind] attributes for List/Array/Vector (#8136) 2025-04-28 13:48:20 +00:00
Data feat: follow-up to lemmas about List.intersperse (#8318) 2025-05-14 00:24:13 +00:00
Grind feat: structure extensionality in grind (#8330) 2025-05-14 02:43:52 +00:00
Internal feat: add support for lattice-theoretic (co)inductive predicates (#8097) 2025-04-30 15:48:58 +00:00
Omega feat: add instance Grind.CommRing (Fin n) (#8276) 2025-05-13 12:09:02 +00:00
System chore: cleaning up imports (#8314) 2025-05-13 07:09:21 +00:00
BinderNameHint.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
BinderPredicates.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
ByCases.lean chore: remove >6 month old deprecations (#8312) 2025-05-13 11:11:22 +00:00
Classical.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Coe.lean chore: do not use the coercion α → Option α in Init and Std (#8085) 2025-04-24 13:35:01 +00:00
Control.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Conv.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Core.lean chore: remove >6 month old deprecations (#8312) 2025-05-13 11:11:22 +00:00
Data.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Dynamic.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Ext.lean chore: remove grind ext lemmas for List/Array/Vector (#8207) 2025-05-02 17:41:02 +00:00
GetElem.lean feat: add @[grind] annotations for generic GetElem lemmas (#8327) 2025-05-14 00:03:38 +00:00
Grind.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Guard.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Hints.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Internal.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
MacroTrace.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Meta.lean chore: do not use the coercion α → Option α in Init and Std (#8085) 2025-04-24 13:35:01 +00:00
MetaTypes.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Notation.lean feat: guard_msgs to treat trace messages separate (#8267) 2025-05-09 05:44:34 +00:00
NotationExtra.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Omega.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Prelude.lean feat: do not export theorem bodies (#8090) 2025-04-25 20:22:32 +00:00
PropLemmas.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
RCases.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
ShareCommon.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
SimpLemmas.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Simproc.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
SizeOf.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
SizeOfLemmas.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Syntax.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
System.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Tactics.lean feat: fun_induction to unfold function application in the goal (#8104) 2025-05-13 09:37:39 +00:00
TacticsExtra.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Task.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Try.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Util.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
WF.lean fix: wf preprocess of ite (#8112) 2025-04-26 07:30:45 +00:00
WFTactics.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
While.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00