Leonardo de Moura
88c73f1daa
chore: remove old if-then-else parser and elaborator
2021-09-30 20:33:58 -07:00
Leonardo de Moura
a5502e652c
chore: activate builtin if-then-else elaborator
2021-09-30 20:29:49 -07:00
Leonardo de Moura
698760c5eb
refactor: add if-then-else builtin parser
2021-09-30 19:33:41 -07:00
Leonardo de Moura
09d0c93589
feat: declare functions in mutual block using auxiliary fuction defined using WF
2021-09-29 11:24:52 -07:00
Leonardo de Moura
608417b946
fix: check number of explicit variables at induction/cases alternatives when @ is not used
...
fixes #690
2021-09-29 07:39:38 -07:00
Leonardo de Moura
3fed9c9df7
feat: reject partial when if constant is not a function
...
fixes #697
2021-09-28 21:07:14 -07:00
Leonardo de Moura
bd98e6a586
feat: refine WellFounded.fix functional F over PSigma.casesOn
2021-09-27 19:06:10 -07:00
Leonardo de Moura
d0391d07c2
feat: use PSigma.casesOn instead of projections at packDomain
...
Reason: we want to "refine" the `WellFounded.fix` functional `F` over it.
2021-09-27 19:06:10 -07:00
Leonardo de Moura
8b79176102
feat: refine WellFounded.fix functional F over Sum.casesOn
2021-09-27 19:06:10 -07:00
Leonardo de Moura
108518aad1
feat: use simp at mkDecreasingProof
2021-09-26 16:32:48 -07:00
Leonardo de Moura
d13bdef6e2
feat: add WF.mkFix
2021-09-26 16:01:07 -07:00
Leonardo de Moura
a7f36cc642
chore: style
2021-09-26 15:52:13 -07:00
Leonardo de Moura
9d69189a60
chore: use Sum instead of PSum at PackMutual
2021-09-25 17:24:56 -07:00
Leonardo de Moura
d4509878bb
feat: add WellFoundedRelation for termination_by
2021-09-25 17:21:03 -07:00
Leonardo de Moura
ceb9889b0e
feat: elaborate temination_by term
2021-09-25 16:54:41 -07:00
Leonardo de Moura
a5b27952b5
fix: panic messages on invalid input
...
fixes #689
2021-09-25 09:01:01 -07:00
Leonardo de Moura
58c938cef8
feat: 'termination_by' goodies
2021-09-22 21:09:33 -07:00
Leonardo de Moura
38f91a2fa4
doc: PackMutual.lean
2021-09-22 18:27:57 -07:00
Leonardo de Moura
0b7b174f25
feat: replace recursive applications at packMutual
2021-09-22 18:07:07 -07:00
Leonardo de Moura
b8454f3568
fix: packDomain
2021-09-22 18:00:22 -07:00
Leonardo de Moura
65983ef45b
feat: add WF/PackMutual.lean
2021-09-22 15:46:47 -07:00
Sebastian Ullrich
ea244c298c
chore: un-orphan file
2021-09-22 16:04:18 +02:00
Leonardo de Moura
07fb8504a1
fix: bug introduced today
2021-09-21 20:36:18 -07:00
Leonardo de Moura
a909e8cf26
feat: arity mismatch error message at well-founded recursion
2021-09-21 20:34:15 -07:00
Leonardo de Moura
ed47091691
chore: add extra trace messages and document issue
2021-09-21 20:33:44 -07:00
Leonardo de Moura
c41b3d6928
fix: reset local context at addPreDefinitions
2021-09-21 20:18:59 -07:00
Leonardo de Moura
ee2bdc1f84
feat: add WF/PackDomain.lean
2021-09-21 19:38:43 -07:00
Leonardo de Moura
5a301d8c3b
refactor: add src/Lean/Elab/PreDefinition/WF directory
2021-09-21 15:44:21 -07:00
Leonardo de Moura
640fc964b6
feat: basic termination_by bookkeeping
2021-09-21 15:24:42 -07:00
Leonardo de Moura
59ed4dea7b
feat: add runTactic for running tactic Syntax in MetaM
2021-09-21 12:57:08 -07:00
Leonardo de Moura
0351c96831
feat: better error message for induction tactic on mutually inductives
2021-09-21 06:56:17 -07:00
Leonardo de Moura
06a741be5c
feat: ensure equational theorem conditions occur after the main variables
2021-09-20 11:41:33 -07:00
Leonardo de Moura
5fe40fbccf
refactor: add sortFVarIds to Meta/Basic.lean
2021-09-20 11:32:53 -07:00
Leonardo de Moura
f2a418a7ae
chore: smartUnfolding cleanup
...
We remove dead code, update comments, and add new tests
See #445
2021-09-19 15:29:11 -07:00
Leonardo de Moura
5b0a1c2b2f
feat: smart unfolding support for nested match-expressions
...
See #445
2021-09-19 15:17:56 -07:00
Leonardo de Moura
82f3042fa4
fix: equational theorem generation for structural recursion
2021-09-19 08:48:40 -07:00
Leonardo de Moura
233a262c03
feat: improve whnfReducibleLHS?
2021-09-19 08:33:51 -07:00
Leonardo de Moura
c2d33a1a58
fix: bug at addSmartUnfoldingDef
...
The approach using `matcherBelowDep : NameSet` was not correct because
we "reuse" matcher-declarations. For example, in the definition
```
def f : Nat → Bool
| 0 => true
| n + 1 => (match n with
| 0 => true
| _ + 1 => true) && f n
```
we have to `match`-expressions but they can be compiled the same
matcher `f.match_1`. Thus, the set `matcherBelowDep` would contain
`f.match_1` since the first occurence refined the `Nat.below` argument
at `mkBRecOn`. Thus, `addSmartUnfoldingDef` was incorrectly assuming the second
`match` was refined too.
We fixed this issue by simulating `mkBRecOn` behavior.
fixes #445
2021-09-18 19:15:38 -07:00
Leonardo de Moura
c795a75045
feat: modify approach for generating equational theorems
2021-09-18 15:58:31 -07:00
Leonardo de Moura
1ce65672ba
chore: modify strategy for constructing equational theorems
2021-09-18 08:27:07 -07:00
Leonardo de Moura
07bd5ae2b8
chore: remove dead code
2021-09-18 07:36:14 -07:00
Leonardo de Moura
d413aa1dc5
feat: generate proofs for structural (conditional) equality theorems
2021-09-17 18:57:39 -07:00
Leonardo de Moura
1a0badac06
feat: generate conditional structural equation theorem types
...
TODO: proofs
2021-09-17 16:49:30 -07:00
Leonardo de Moura
6ffb3f91f0
feat: save information for generating structural equation theorems later
2021-09-17 14:20:28 -07:00
Leonardo de Moura
94ede53940
chore: use doc string
2021-09-17 14:20:28 -07:00
Leonardo de Moura
d378df47d7
fix: fixes #633
2021-09-16 14:11:34 -07:00
Leonardo de Moura
0a898965a3
chore: use snake_case for user-facing tactic names
2021-09-16 10:23:12 -07:00
Leonardo de Moura
c2a5e37c60
feat: simp discharger
2021-09-16 10:11:27 -07:00
Leonardo de Moura
fd8fb3cf9e
chore: prepare to change simp syntax
2021-09-16 07:41:04 -07:00
Leonardo de Moura
deea3996be
fix: allow renameI to rename shadowed names
2021-09-13 06:43:34 -07:00
