Leonardo de Moura
96bae46045
refactor: SimpLemma => SimpTheorem
2022-02-06 09:15:39 -08:00
Leonardo de Moura
6de0b1fc67
feat: add mkCongrSimp.mkProof
...
see #988
2022-02-04 17:57:28 -08:00
Leonardo de Moura
3ae455bccf
feat: add mkCongrSimp?
...
TODO: proof is still missing
see #988
2022-02-04 17:57:28 -08:00
Leonardo de Moura
a028a69159
feat: cache isProp and isDecInst at FunInfo
2022-02-04 17:57:28 -08:00
Mario Carneiro
6e7d76f4d8
fix: typo
2022-02-03 18:21:14 -08:00
Leonardo de Moura
12e2a79170
chore: fix codebase after removing auto pure
2022-02-03 18:08:14 -08:00
Leonardo de Moura
c30380e2fa
feat: lift the restriction in congr theorems that all function arguments on the lhs must be free variables
...
see #988
2022-02-02 18:23:18 -08:00
Leonardo de Moura
101fc12b54
feat: partially applied user congruence lemmas
...
see #988
2022-02-02 17:41:21 -08:00
Leonardo de Moura
188f0eb70f
fix: splitMatch tactic
...
Improve how we compute the motive for match-splitter eliminator.
closes #986
2022-02-02 15:06:03 -08:00
Leonardo de Moura
65e1fc1211
feat: at splitMatch only generalize discriminants that are not FVar
2022-02-02 15:06:03 -08:00
Leonardo de Moura
630bf4e129
chore: update error message for throwNestedTacticEx
2022-02-02 15:06:03 -08:00
Leonardo de Moura
3101b98f50
feat: used nested tactic exception at splitMatch
2022-02-02 15:06:03 -08:00
Leonardo de Moura
b1617fe04c
feat: add throwNestedTacticEx
...
closes #194
2022-01-31 16:25:44 -08:00
Leonardo de Moura
f02013fd76
fix: induction MetaM tactic
...
The major premise may be a let-declaration.
closes #983
2022-01-31 13:41:38 -08:00
Leonardo de Moura
3db640e770
chore: avoid Name.quickLt
...
`Name.quickLt` uses hash code and may produce counterintuitive results
to users.
2022-01-28 09:48:50 -08:00
Leonardo de Moura
e5ef61225b
fix: missing condition at lpo case 3
2022-01-28 09:47:35 -08:00
Leonardo de Moura
cb4a86ac68
fix: do not validate local eq theorems
...
see #973
2022-01-27 11:50:20 -08:00
Leonardo de Moura
a63163e992
feat: do not try to discharge hypotheses at simp when type contains assignable metavariables
...
closes #973
see https://github.com/leanprover-community/mathport/issues/70
2022-01-26 17:57:52 -08:00
Leonardo de Moura
2fff4c42b7
fix: make sure irreducible constants are not unfolded when using the default reducibility setting
2022-01-26 11:55:21 -08:00
Leonardo de Moura
8db923e010
feat: generate error message for simp theorems that are equivalent to x = x
...
see #973
see https://github.com/leanprover-community/mathport/issues/70
2022-01-26 11:16:31 -08:00
Leonardo de Moura
cf3b8d4eb4
chore: cleanup
...
Make the code style more uniform.
We still have a lot of leftovers from the old frontend.
2022-01-26 09:18:17 -08:00
Leonardo de Moura
a10e32f537
fix: check "heartbeats" at simp
2022-01-26 07:50:25 -08:00
Leonardo de Moura
15cca3000a
fix: withIncRecDepth was not aborting simp
...
It was just making it stop simplification at the current branch.
Now, elaboration is interrupted after a few seconds in the example at
issue #906 .
see #906
2022-01-26 07:48:58 -08:00
Leonardo de Moura
98407798af
fix: mkEquationsFor at Match/MatchEqs.lean
...
closes #974
2022-01-25 18:43:51 -08:00
Leonardo de Moura
a969014eb9
chore: add matchHEq?
2022-01-25 18:43:51 -08:00
Leonardo de Moura
9c293abb9c
chore: expose heqToEq tactic
2022-01-25 18:43:51 -08:00
Leonardo de Moura
6547af988b
feat: add substVars
2022-01-25 18:43:51 -08:00
Leonardo de Moura
234f70fadb
chore: remove the now incorrect comment
2022-01-24 19:05:05 -08:00
Leonardo de Moura
02677cf326
fix: igore instance implicit arguments in term ordering used at simp
...
closes #972
2022-01-24 18:57:31 -08:00
Leonardo de Moura
d4f7899591
chore: avoid code duplication setting Simp.Config
2022-01-24 18:57:31 -08:00
Leonardo de Moura
722bf54929
fix: trace message with incorrect MetavarContext
2022-01-24 10:34:44 -08:00
Leonardo de Moura
7ada79bf2e
fix: use an AC-compatible ordering on Expr at simp
...
closes #968
2022-01-22 09:42:59 -08:00
Leonardo de Moura
6f416147b4
chore: rename coeM and liftCoeM
2022-01-20 15:33:17 -08:00
Leonardo de Moura
2192e6148b
chore: remove coe, coeSort, and coeFun abbreviations
...
The notation `↑ e` is now expanded eagerly.
See #403
2022-01-20 15:19:06 -08:00
Leonardo de Moura
3c17755730
chore: prepare to remove coe definitions
...
The notation `↑ e` will eagerly expand the coersion.
See #403
2022-01-20 15:07:54 -08:00
Leonardo de Moura
d190d6dda4
fix: use default reducibility when proving equation theorems for definition
...
Addresses issue reported by @fpfu at #945
2022-01-20 08:23:51 -08:00
Leonardo de Moura
f5509ab867
fix: equational lemma generation for definitions using named patterns
...
closes #945
2022-01-19 17:45:54 -08:00
Leonardo de Moura
ef449e816f
chore: improve trace messages
2022-01-19 14:29:04 -08:00
Leonardo de Moura
873a2ba8a6
feat: unfold namedPattern applications at equation theorems
2022-01-18 15:03:20 -08:00
Leonardo de Moura
1e21815e41
fix: equality theorem generation when named patterns are used
...
closed #945
2022-01-18 14:37:51 -08:00
Leonardo de Moura
c816524d8d
feat: add subst?
2022-01-18 14:26:14 -08:00
Leonardo de Moura
c12fa6f0e2
fix: error message
...
The equation theorems may fail for other reasons.
2022-01-18 14:11:54 -08:00
Leonardo de Moura
1c1e6d79a7
feat: add equality proof for named patterns
...
The user can optionally name the equality proof.
The new test demostrates how to name the equality proof.
closes #501
2022-01-18 12:43:01 -08:00
Leonardo de Moura
42fe01a3eb
feat: add new flag to caseValues
2022-01-18 12:15:29 -08:00
Leonardo de Moura
9d05023325
chore: remove some [specialize] annotations
2022-01-18 09:24:06 -08:00
Leonardo de Moura
6631f1d5b3
chore: use namedPatternOld
2022-01-17 17:18:03 -08:00
Leonardo de Moura
2c690926cf
feat: update namedPattern parser
2022-01-17 16:49:20 -08:00
Leonardo de Moura
de11f7e1bc
feat: add sizeOf spec lemmas as simp theorems
2022-01-17 16:14:38 -08:00
Leonardo de Moura
8f47043aee
chore: add trace message for sizeOf theorem
2022-01-17 15:42:42 -08:00
Leonardo de Moura
bac91b9b5b
chore: remove arbitrary
2022-01-15 12:14:27 -08:00
