Leonardo de Moura
1a7dd56f0f
fix(library/tools/tactic): 'cases' argument precedence
2014-11-29 21:03:45 -08:00
Leonardo de Moura
f51fa93292
feat(library/tactic): add 'fapply' tactic, closes #356
2014-11-29 19:20:41 -08:00
Leonardo de Moura
2487e3b83d
fix(frontends/lean/parser): user provided numeral notation should have precedence over the default based on 'num'
2014-11-29 17:29:03 -08:00
Leonardo de Moura
bc65aeb5e1
fix(frontends/lean/calc): add expected type for single-step calc expressions, fixes #357
...
This is not an issue for calc expressions containing multiple steps,
since the transitivity step will "force" the expected type for the proofs.
2014-11-29 15:35:09 -08:00
Leonardo de Moura
6fbbf66565
test(tests/lean/run/vector): define 'map' on vector using brec_on and new inversion tactic
2014-11-29 13:28:01 -08:00
Leonardo de Moura
7000365a04
fix(tests/lean): to reflect changes in the standard library
2014-11-28 23:03:37 -08:00
Leonardo de Moura
e0debca771
feat(library/tactic/inversion_tactic): add 'case ... with ...' variant that allows user to specify names for new hypotheses
2014-11-28 22:25:37 -08:00
Leonardo de Moura
22b2f3c78c
fix(library/tactic/inversion_tactic): bug in injectivity transition
2014-11-28 22:07:35 -08:00
Leonardo de Moura
a6be460166
feat(library/tactic/inversion_tactic): basic 'inversion' tactic
2014-11-28 21:56:13 -08:00
Leonardo de Moura
f7deabfd19
feat(library/rename): add notation for rename
2014-11-26 19:02:11 -08:00
Leonardo de Moura
e55397d422
feat(library/tactic): add 'clears' and 'reverts' variants
2014-11-26 14:49:48 -08:00
Leonardo de Moura
2bd8f969d5
feat(library/tactic): add 'revert' tactic, closes #346
2014-11-26 14:23:42 -08:00
Leonardo de Moura
c28e9b9234
feat(library/tactic): add 'clear' tactic, closes #341
2014-11-26 13:11:36 -08:00
Leonardo de Moura
ffdeb0edc4
fix(frontends/lean/elaborator): unsolved metavariables, fix #329
2014-11-26 11:56:39 -08:00
Leonardo de Moura
df51ba8b7c
feat(library/definitional/projection): use strict implicit inference, closes #344
2014-11-25 18:04:06 -08:00
Leonardo de Moura
edc9e4908c
test(tests/lean/run): add another subterm example
2014-11-25 16:53:09 -08:00
Leonardo de Moura
f737a140c1
test(tests/lean/run): direct subterm for non-reflexive datatype
2014-11-25 16:22:11 -08:00
Leonardo de Moura
ef75cac1c0
feat(kernel/expr): change the rules for inferring implicit arguments, closes #344
2014-11-25 12:54:07 -08:00
Leonardo de Moura
24a15b6c46
fix(frontends/lean): disable class-instance resolution when executing find_decl, fixes #343
2014-11-24 21:33:52 -08:00
Leonardo de Moura
f729762c23
test(tests/lean/run): add test for well_founded relation for mutually recursive datatypes
2014-11-24 14:58:30 -08:00
Leonardo de Moura
d81a6259e8
feat(frontends/lean/find_cmd): add options for controlling find_decl
2014-11-24 00:16:10 -08:00
Leonardo de Moura
f1e915a188
feat(frontends/lean): add 'find_decl' command
2014-11-23 23:00:59 -08:00
Leonardo de Moura
44a2ef8f6f
fix(frontends/lean/parser_config): binder(s) rbp was not being saved in .olean file
2014-11-23 17:49:14 -08:00
Leonardo de Moura
64686c1278
feat(frontends/lean): allow user to associate precedence to binders, closes #323
2014-11-23 17:30:46 -08:00
Leonardo de Moura
cf3b0e1087
feat(frontends/lean/placeholder_elaborator): apply substitution before collecting local instances, closes #333
2014-11-23 17:30:46 -08:00
Leonardo de Moura
13fba433b0
feat(library/tactic/generalize): add 'generalizes' syntax sugar, closes #327
2014-11-23 17:30:22 -08:00
Leonardo de Moura
919007612a
fix(tests/lean): adjust tests since module 'logic' depends on nat
...
We need that because of the definitional package
2014-11-22 17:34:05 -08:00
Leonardo de Moura
5db13da95f
test(tests/lean/run/div_wf): cleanup div based on well founded recursion
2014-11-22 09:56:47 -08:00
Leonardo de Moura
064ecd3e3d
refactor(library/data/nat): declare lt and le asap using inductive definitions, and make key theorems transparent for definitional package
...
We also define key theorems that will be used to generate the
automatically generated a well-founded subterm relation for inductive
datatypes.
We also prove decidability and wf theorems asap.
2014-11-22 00:19:39 -08:00
Leonardo de Moura
5d5fd2da50
fix(frontends/lean): tactic + section variables, fixes #332
2014-11-21 10:07:16 -08:00
Leonardo de Moura
7e7e7c241c
test(tests/lean/run/gcd): gcd compiled by hand into wf recursion
2014-11-18 19:34:01 -08:00
Leonardo de Moura
4fbb5cfcca
test(tests/lean/run/div_wf): cleanup
2014-11-18 17:59:14 -08:00
Leonardo de Moura
a065c7bf96
test(tests/lean/run/tree_height): experiment with wf relation based on the height
...
This is easier to generate than the subterm relation
2014-11-18 17:57:17 -08:00
Leonardo de Moura
5fbe990c7a
test(tests/lean/run): define div using wf package
2014-11-18 13:55:58 -08:00
Leonardo de Moura
5daff18017
test(tests/lean/run): pre-quotient experiment
2014-11-17 18:30:11 -08:00
Leonardo de Moura
28c63e685b
feat(frontends/lean): add '[local]' notation, closes #322
2014-11-16 21:15:04 -08:00
Leonardo de Moura
a171f8fbc3
test(tests/lean/run): simple diag for square matrices
2014-11-15 18:49:17 -08:00
Leonardo de Moura
1b95b69251
test(tests/lean/run): define subterm relation for vectors
2014-11-15 16:17:51 -08:00
Leonardo de Moura
ea640257bf
feat(frontends/lean/structure_cmd): generate no_confusion for structures too
2014-11-15 16:00:09 -08:00
Leonardo de Moura
b87559dac5
test(tests/lean/run): define subterm relation for trees by hand
2014-11-15 13:29:23 -08:00
Leonardo de Moura
7685516d1e
feat(frontends/lean): better default for atomic notation
2014-11-14 16:25:13 -08:00
Leonardo de Moura
00df34a1c4
feat(library/unifier): generalize method process_succ_eq_max_core
2014-11-14 14:25:41 -08:00
Leonardo de Moura
488f989c46
fix(frontends/lean/inductive_cmd): generate error for inductive datatype declarations that will produce an eliminator that can only eliminate to Prop
2014-11-14 13:57:42 -08:00
Leonardo de Moura
51719145f9
feat(library/unifier): solved universe constraints of the form succ^k1 a = max k2 ?m (when k1 >= k2)
2014-11-12 17:28:33 -08:00
Leonardo de Moura
edd04881ee
fix(library/logic): import prod and unit declarations in logic
...
Reason: we need them for automatically generating constructions needed
by the definitional package
2014-11-12 16:54:50 -08:00
Leonardo de Moura
6bc89f0916
feat(library/definitional): define ibelow and below
...
These are helper definitions for brec_on and binduction_on
2014-11-12 16:38:46 -08:00
Leonardo de Moura
97609d1625
test(tests/lean/run/nateq): add example that triggered previous modification
2014-11-12 15:11:08 -08:00
Leonardo de Moura
b07b82cf43
fix(library/definitional): marking cases_on and rec_on as reducible
...
The idea is to avoid counter-intuitive behavior
2014-11-12 15:03:30 -08:00
Leonardo de Moura
a3066e3eaa
fix(frontends/lean/inductive_cmd): bug in inductive datatype elaborator
2014-11-12 13:10:19 -08:00
Leonardo de Moura
463e70332d
test(tests/lean/run): define brec_on and binduction_on for a reflexive type
...
We say an inductive type T is reflexive if it contains at least one constructor that
takes as an argument a function returning T.
For reflexive types it doesn't seen to be possible to define a single
brec_on that can eliminate to Type.{>=1} and Prop.
The universe level expressions get too complicated.
Even if we extend the universe constraint solver in the kernel, the
additional complexity might be a problem.
We workaround this issue by defining two versions of brec_on:
- One (brec_on) that eliminates to Type.{>=1}, and
- binduction_on that eliminates to Prop.
For non-reflexive types, we can combine both of them.
2014-11-12 10:52:32 -08:00
