Leonardo de Moura
54f68226f4
chore(frontends/lean): disable old tactic framework and blast
2016-04-25 16:22:15 -07:00
Leonardo de Moura
fdea718d9d
chore(frontends/lean): remove all #include "library/tactic.*" from frontends/lean
2016-04-25 15:41:12 -07:00
Leonardo de Moura
d88098f38d
chore(frontends/lean): remove some of the tactic support
2016-04-25 15:26:56 -07:00
Leonardo de Moura
de64750621
chore(frontends/lean): disable expressions that use tactic framework
2016-04-25 15:07:26 -07:00
Leonardo de Moura
22f3efc5be
remove(frontends/lean): begin_end pre-tactics
...
This was never used
2016-03-03 10:02:09 -08:00
Leonardo de Moura
3c878ecd01
feat(kernel): add let-expressions to the kernel
...
The frontend is still using the old "let-expression macros".
We will use the new let-expressions to implement the new tactic framework.
2016-02-29 16:40:17 -08:00
Leonardo de Moura
f55e456c84
chore(*): remove remaining references to by+ and begin+
2016-02-29 13:59:06 -08:00
Leonardo de Moura
b7b4b6d838
chore(src/frontends/lean/builtin_exprs): remove unnecessary parameter
2016-02-29 13:57:18 -08:00
Leonardo de Moura
fbe5188480
refactor(frontends/lean): remove 'by+' and 'begin+' tokens
2016-02-29 13:45:43 -08:00
Leonardo de Moura
bf60999ede
fix(frontends/lean/builtin_exprs): 'using' expression
2016-02-29 13:23:39 -08:00
Leonardo de Moura
2b1d734544
feat(kernel/expr): remove 'contextual' flag from binder_info
2016-02-29 12:41:43 -08:00
Leonardo de Moura
b41c65f549
feat(frontends/lean): remove '[visible]' annotation, remove 'is_visible' tracking
2016-02-29 12:31:23 -08:00
Leonardo de Moura
101cf1ec4c
feat(frontends/lean): remove difference between 'have' and 'assert'
2016-02-29 11:28:20 -08:00
Leonardo de Moura
04eaf184a9
feat(frontends/lean,library/unifier): checkpoints at have-expressions
...
@avigad, @fpvandoorn, @rlewis1988, @dselsam
This commit modifies how have-expressions are elaborated.
Now, to process
have H : <type>, from <proof>,
<rest>
we first process the constraints in <type> and <proof> simultaneously.
After all these constraints are solved, the elaborator performs
a Prolog-like cut, and process the constraints in <rest>.
So, all overloads, type classes and coercions in <type> and <proof> are solved
before we start processing <rest>. Moreover, while processing <rest>, we
cannot backtrack to <type> and <proof> anymore.
I fixed all affected proofs in the standard and HoTT libraries in
previous commits pushed today and yesterday. I think most affected proofs were not using a good
style and/or were easy to fix. Here is a common pattern that does not
work anymore.
structure has_scalar [class] (F V : Type) :=
(smul : F → V → V)
infixl ` • `:73 := has_scalar.smul
proposition smul_zero (a : R) : a • (0 : M) = 0 :=
have a • 0 + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero],
!add.left_cancel this
The `have` doesn't work because Lean can't figure out the type of 0 before
it starts processing `!add.left_cancel this`. This is easy to fix, we just have to
annotate one of the `0`s in the `have`:
proposition smul_zero (a : R) : a • (0 : M) = 0 :=
have a • (0:M) + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero],
!add.left_cancel this
BTW, all tactics are still being executed after all constraints are solved.
We may change that in the future. I didn't want to execute
the tactics at <proof> before <rest> because of universe
meta-variables. In Lean, unassigned universe meta-variables become
parameters. Moreover, we perform this conversion *before*
we start processing tactics. Reason: universe meta-variables
create many problems for tactics such as `rewrite`, `blast` and `simp`.
Finally, we can recover the previous behavior using the option
set_option parser.checkpoint_have false
2016-02-04 19:01:19 -08:00
Leonardo de Moura
ba392f504f
feat(kernel/expr,library/blast/blast,frontends/lean/decl_cmds): add workaround for allowing users to use blast inside of recursive equations
2016-01-03 21:53:31 -08:00
Leonardo de Moura
732a92de05
feat(frontends/lean): add 'simp' as shortcut for 'with_options [blast.strategy "simp"] blast'
2015-12-06 13:14:04 -08:00
Leonardo de Moura
edd1b34143
doc(library/blast/forward/pattern): describe pattern inference heuristic
2015-11-25 11:57:30 -08:00
Leonardo de Moura
017abdfb6a
feat(frontends/lean): add notation for providing patterns
2015-11-24 18:48:22 -08:00
Daniel Selsam
6b06a19294
chore(frontends/lean): remove whitespace
2015-11-08 14:05:00 -08:00
Daniel Selsam
fa58d7c71e
feat(frontends/lean): basic support for partial explicit
2015-11-08 14:05:00 -08:00
Leonardo de Moura
1d670e3193
feat(frontends/lean): support for '@@' -- the partial explicit operator
2015-11-08 14:05:00 -08:00
Leonardo de Moura
28a5ca5809
fix(frontends/lean): fixes #830
2015-09-18 07:51:02 -07:00
Leonardo de Moura
1fdbd681cc
feat(frontends/lean/builtin_exprs): name hypothesis in suffices
...
closes #817
2015-09-03 16:09:39 -07:00
Leonardo de Moura
3a72cd9621
fix(frontends/lean): rename multiword keyword "suffices to show" to "suffices"
2015-08-18 17:57:53 -07:00
Leonardo de Moura
3ce8c5d6f7
feat(frontends/lean): add "suffices to show A, from B, C" construct
2015-08-18 17:04:38 -07:00
Leonardo de Moura
06f20694c8
fix(frontends/lean/builtin_exprs): fixes #768
2015-08-08 04:20:17 -07:00
Leonardo de Moura
f21647899f
feat(frontends/lean/builtin_exprs): rename 'show' hidden name to 'this'
...
This is useful if 'show' is recursive
2015-08-07 13:29:21 -07:00
Leonardo de Moura
cfa9412f96
fix(frontends/lean): "show goal" localization, add "position", support "by tactic"
2015-07-28 12:48:12 -07:00
Leonardo de Moura
e0209a1532
feat(frontends/lean): better error localization for 'have'-expressions in tactic mode
2015-07-23 18:52:59 -07:00
Leonardo de Moura
946308b187
feat(frontends/lean): allow anonymous 'have'-expressions in tactic mode
2015-07-23 18:52:59 -07:00
Leonardo de Moura
812ddf1ef5
feat(frontends/lean): add 'suppose'-expression
...
It is a variant of 'assume' that allow anonymous declarations.
2015-07-19 12:15:12 -07:00
Leonardo de Moura
92f8eb173b
feat(frontends/lean): use 'this' as the name for anonymous 'have'-expression
2015-07-18 13:36:05 -05:00
Leonardo de Moura
382d4d32b7
feat(frontends/lean): 'override' command and '#<namespace> <expr>' notation also override aliases
...
Before this commit they were only overriding notation declarations.
2015-06-14 15:48:36 -07:00
Leonardo de Moura
3d9b557cfd
feat(frontends/lean): allow the user to mark subterms that should be automatically abstracted into new definitions
...
closes #484
2015-06-12 17:49:26 -07:00
Leonardo de Moura
4b91cfccff
feat(frontends/lean/builtin_exprs): make notation ( e : T ) builtin
...
In the previous approach, the following (definitionally equal) term was being generated
(fun (A : Type) (a : A), a) T e
2015-06-10 14:52:59 -07:00
Leonardo de Moura
af3f0088f4
feat(frontends/lean): add 'override' (notation) command
2015-05-20 11:42:16 -07:00
Leonardo de Moura
8ce992b077
feat(frontends/lean/builtin_exprs): allow 'obtain' to be used in tactic mode
2015-05-19 16:26:02 -07:00
Leonardo de Moura
c133d26505
feat(frontends/lean/builtin_exprs): change how 'show' is processed in tactics
...
Unresolved placeholders were not being reported
2015-05-19 16:23:50 -07:00
Leonardo de Moura
5f628d5080
feat(frontends/lean/builtin_exprs): allow 'calc' expressions to be used in tactic mode
2015-05-19 15:54:49 -07:00
Leonardo de Moura
7f8afcf04b
fix(frontends/lean/builtin_exprs): bug in 'using' expressions
2015-05-14 17:17:48 -07:00
Leonardo de Moura
613281d622
fix(frontends/lean/builtin_exprs): bug in new 'obtain' expression
2015-05-06 10:01:24 -07:00
Leonardo de Moura
26c662accd
feat(frontends/lean/builtin_exprs): improve new 'obtain' expression
2015-05-06 09:56:57 -07:00
Leonardo de Moura
7cd444882c
feat(frontends/lean): add 'begin+' and 'by+' that enter tactic mode with the whole context visible
2015-05-05 18:47:25 -07:00
Leonardo de Moura
616f49c2e4
feat(frontends/lean): improved 'obtains' expression
2015-05-05 18:30:16 -07:00
Leonardo de Moura
87aaf373f4
fix(frontends/lean): fix '#' override notation on the left-hand-side of recursive equations (and match-expressions)
2015-05-03 21:08:09 -07:00
Leonardo de Moura
441f1f9fe2
feat(frontends/lean): import error message for "unknown" tactics when parsing
2015-05-02 18:57:58 -07:00
Leonardo de Moura
a23118d357
feat(frontends/lean): add tactic_notation command
...
This addresses the first part of issue #461
We still need support for tactic definitions
2015-04-27 17:46:13 -07:00
Leonardo de Moura
9d01868361
feat(frontends/lean): use rewrite tactic to implement unfold (it has a unfold step)
...
closes #502
2015-04-24 17:23:12 -07:00
Leonardo de Moura
107763a506
fix(frontends/lean): better error message for 'proof ... qed' blocks containing unsolved placeholders
2015-04-20 15:50:37 -07:00
Leonardo de Moura
2bc13f6bfd
feat(library/tactic/exact): enforce goal type during elaboration when executing 'exact' tactic
...
Remark: this was the behavior of the 'sexact' tactic.
This commit also adds the 'rexact' (relaxed exact) tactic which does not
enforce the goal type.
closes #495
2015-04-06 13:23:38 -07:00
