Leonardo de Moura
0c1c6c0a73
feat: convert universe metavariables into parameters after elaborating theorem header
...
closes #318
Like Lean 3, we are doing it only for theorems.
@Kha, we talked about doing it for definitions too, it sounded like a
good idea, and it would make the system's behavior more uniform, but
unfortunately it creates too many problems. There are so many trivial
cases where it breaks. Here are some examples.
1- Definitions that take multiple bundled structures
```
def foo (s1 : Group) (s2 : CommRing) ...
```
They are universe polymorphic, and the different structures must be in
the same universe, but we don't know it when we elaborate the header,
that is, we need to elaborate the body.
An extreme case is `PUnit` occurring in the header. It is universe
polymorphic, but we only lear the constraints on this universe after
we elaborate the body.
2- All files containing unification hints broke.
Again, there are universe constraints on the header that we only learn
after we elaborate the body.
3- Many `CoeSort` and `CoeFun` examples broke.
Example:
```
structure Group :=
(carrier : Type u) (mul : carrier → carrier → carrier) (one : carrier)
instance GroupToType : CoeSort Group (Type u) :=
CoeSort.mk (fun g => g.carrier)
```
We would have to write
```
instance GroupToType : CoeSort Group.{u} (Type u) :=
CoeSort.mk (fun g => g.carrier)
```
We would have to provide universe level parameters manually in this
kind of instance. I think it would be too annoying.
2021-02-25 16:53:58 -08:00
Zygimantas Straznickas
49ebd30fd5
fix: fix deriving Repr for structure-like inductives
...
The deriving code currently uses isStructureLike when choosing whether to use
Inductive or Structure logic, which fails for inductives that are
structure-like. The commit changes the code to use isStructure.
2021-02-25 13:38:33 -08:00
Leonardo de Moura
1b16f9b33c
fix: make sure kernel checks examples
...
We discard the resulting environment for examples.
closes #309
cc @Kha
2021-02-25 13:34:27 -08:00
Leonardo de Moura
d770c55326
feat: universe level parameters in instances are outParam by default
...
This commit makes sure Lean 4 treats universe level parameters in
instances as `outParam`s. This the behavior in Lean 3.
fixes #319
2021-02-25 13:21:53 -08:00
Leonardo de Moura
162062b3de
feat: improve Lawful.lean
2021-02-23 12:38:00 -08:00
Leonardo de Moura
0ceac85c6d
chore: fix test
2021-02-21 16:29:13 -08:00
Leonardo de Moura
1b15a848e0
chore: fix test
2021-02-21 11:16:21 -08:00
Leonardo de Moura
1ed2ee4df8
fix: local simp lemmas with implicits
2021-02-20 14:29:15 -08:00
Leonardo de Moura
d8ca6d847b
test: lost synthetic mvar issue
2021-02-20 13:01:36 -08:00
Leonardo de Moura
8fa1ecde49
fix: throw error when default value contains metavariables
2021-02-20 11:31:56 -08:00
Leonardo de Moura
6eeccdd675
test: for field auto implicit bound feature
2021-02-20 07:52:42 -08:00
Leonardo de Moura
e1f6965266
feat: allow user to define rewrite lemmas with (local) match expressions
2021-02-19 15:18:19 -08:00
Leonardo de Moura
d493e700cc
fix: matchUnit simplification
2021-02-19 13:51:08 -08:00
Leonardo de Moura
2861f71c61
feat: add option autoLift
2021-02-19 11:02:58 -08:00
Leonardo de Moura
c06ca8304d
fix: test
2021-02-18 16:54:45 -08:00
Joe Hendrix
ffef5635bb
fix: Json.num
...
Handle negative numbers correctly.
2021-02-18 13:27:31 +01:00
Leonardo de Moura
df8634e9ad
fix: assertAfter
2021-02-17 13:52:43 -08:00
Leonardo de Moura
bb2ca97df9
refactor: add options for controlling whether variables are included or not at mkLambdaFVars and mkForallFVars
2021-02-17 13:49:27 -08:00
Leonardo de Moura
c97ae92afe
chore: cleanup
2021-02-17 13:03:24 -08:00
Leonardo de Moura
79a4aebf96
feat: add byCases tactic
2021-02-17 13:03:24 -08:00
Leonardo de Moura
08927f1e66
test: tactic framework and AC by reflection
2021-02-17 13:03:24 -08:00
Leonardo de Moura
1a7535263e
fix: unfolding class projections at simp
2021-02-16 17:55:57 -08:00
Leonardo de Moura
5f80659b45
fix: unfold constants at simp
2021-02-16 15:42:31 -08:00
Leonardo de Moura
5e24da0c2e
fix: simp argument issue
...
See new test.
2021-02-16 13:12:57 -08:00
Leonardo de Moura
d1009e8405
chore: add simp lemmas, theorem naming convention
2021-02-16 11:53:49 -08:00
Sebastian Ullrich
1490d095a8
fix: delaborator: bind without lambda
2021-02-16 12:07:46 +01:00
Leonardo de Moura
242a8dcfbf
test: simp
2021-02-15 17:09:51 -08:00
Leonardo de Moura
e97df2f61b
feat: functions to unfold at simp
2021-02-15 15:32:25 -08:00
Leonardo de Moura
1c5de9842d
feat: use decide at simp
2021-02-15 13:08:45 -08:00
Leonardo de Moura
9528c1abd7
chore: add basic simp lemmas
...
TODO: consistent naming convention for theorems.
cc @Kha
2021-02-15 11:32:19 -08:00
Leonardo de Moura
3bc5b89ac3
test: add if p x then .. else .. example
...
cc @Kha
2021-02-14 11:44:10 -08:00
Leonardo de Moura
ac51d3e621
feat: eager coe expansion
2021-02-14 11:34:08 -08:00
Leonardo de Moura
f07b9926b1
feat: unfold coercions and coeFun, coeSort, coeM, liftCoeM
...
TODO: `coe`
2021-02-14 10:27:34 -08:00
Leonardo de Moura
0787886cea
feat: improve simp local lemma elaboration
2021-02-13 18:55:19 -08:00
Leonardo de Moura
2944da2a0b
feat: use simp itself as default method for discharging hypotheses of conditional rewriting rules
2021-02-13 18:55:19 -08:00
Leonardo de Moura
21878030d1
fix: fixes #310
...
@Kha I implemented the following approach:
- Error if user tries to revert `auxDecl`.
- Clear any `auxDecl` that depends on variables being reverted by the user.
2021-02-12 18:14:42 -08:00
Sebastian Ullrich
75243e7f24
feat: change back seqLeft/Right signature
...
This was originally changed for the sake of `do`, which does not depend on it anymore
2021-02-12 17:08:06 -08:00
Leonardo de Moura
c64d053f9e
test: ite and dite congr test
2021-02-12 16:52:56 -08:00
Leonardo de Moura
8b3c61dbb0
fix: checkAssignment
2021-02-11 16:56:32 -08:00
Sebastian Ullrich
18aaef4d93
chore: fix test
2021-02-11 18:45:06 +01:00
Sebastian Ullrich
8320ab6177
fix: syntax match: check identifiers (using strict equality)
2021-02-11 17:50:05 +01:00
Sebastian Ullrich
a74960a4ab
fix: delaborator: match with shadowing
2021-02-11 11:30:25 +01:00
Leonardo de Moura
896ce41b33
chore: fix test
2021-02-10 12:04:33 -08:00
Leonardo de Moura
2aed9a4ec2
chore: special support for match d with | PUnit.unit => rhs
2021-02-10 09:54:12 -08:00
Leonardo de Moura
16429e393d
test: add dep hd test
...
It has been reported in the general channel that this example
generates problems for the Lean 3 elaborator.
2021-02-08 11:26:23 -08:00
Leonardo de Moura
4e4194af41
feat: add autoBoundImplicit support for structure fields
2021-02-06 17:58:29 -08:00
Leonardo de Moura
023d7605fb
feat: add "transitivity" to "has_loose_bvars_in_domain"
2021-02-06 17:42:38 -08:00
Leonardo de Moura
565f6a9372
chore: fix test
2021-02-06 12:54:53 -08:00
Leonardo de Moura
c984e9be4b
test: for issues #306 and #307
2021-02-06 12:48:43 -08:00
Leonardo de Moura
78fb026201
test: add test for issue #305
...
Issue #305 was fixed by previous commits submitted today for problems
exposed by the `for in` notation based on typeclasses :)
closes #305
2021-02-05 18:15:11 -08:00
