lean2/tests/lean/run/tactic14.lean

import logic
open tactic

notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r

definition basic_tac : tactic
:= repeat (apply @and.intro | assumption)

set_begin_end_tactic basic_tac -- basic_tac is automatically applied to each element of a proof-qed block

theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
begin
  assume Ha, or.elim H
    (assume Hna, @absurd _ false Ha Hna)
    (assume Hnb, @absurd _ false Hb Hnb),
  now
end
-												chore(*): minimize dependencies on tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-08-24 19:58:48 -07:00
+								import logic
-												feat(frontends/lean): rename 'using' command to 'open'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-09-03 16:00:38 -07:00
+								open tactic
-												feat(frontends/lean): add command for customizing the behavior of proof-qed blocks: we can automatically register tactics to be automatically applied before each component

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-07-02 20:45:10 -07:00
-												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
+								notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
-												feat(frontends/lean): add command for customizing the behavior of proof-qed blocks: we can automatically register tactics to be automatically applied before each component

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-07-02 20:45:10 -07:00
+								definition basic_tac : tactic
-												feat(frontends/lean): round parenthesis for [tactic1 | tactic2]

This commit also replaces the notation for divides
     `(` a `|` b `)`
with
      a `∣` b

The character `∣` is entered by typing \|

closes #516

											
										
										
											2015-04-06 09:24:09 -07:00
+								:= repeat (apply @and.intro | assumption)
-												feat(frontends/lean): add command for customizing the behavior of proof-qed blocks: we can automatically register tactics to be automatically applied before each component

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-07-02 20:45:10 -07:00
-												feat(frontends/lean): use 'begin-end' instead of 'proof-qed' for blocks of tactics, closes #81

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-08-21 10:36:44 -07:00
+								set_begin_end_tactic basic_tac -- basic_tac is automatically applied to each element of a proof-qed block
-												feat(frontends/lean): add command for customizing the behavior of proof-qed blocks: we can automatically register tactics to be automatically applied before each component

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-07-02 20:45:10 -07:00
-												refactor(*): rename Bool to Prop

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-07-22 09:43:18 -07:00
+								theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
-												feat(frontends/lean): use 'begin-end' instead of 'proof-qed' for blocks of tactics, closes #81

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-08-21 10:36:44 -07:00
+								begin
-												refactor(library): add namespaces 'or', 'and' and 'iff'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-09-04 21:25:21 -07:00
+								  assume Ha, or.elim H
-												refactor(library/logic/basic): rename absurd_elim to absurd, delete contrapos and trivial_not_true theorems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-08-27 18:34:09 -07:00
+								    (assume Hna, @absurd _ false Ha Hna)
-												feat(library/tactic): improve 'assumption' tactic

- It uses the unifier in "conservative" mode
- It only affects the current goal

closes #570

											
										
										
											2015-05-02 17:32:03 -07:00
+								    (assume Hnb, @absurd _ false Hb Hnb),
 								  now
-												refactor(library/logic/basic): rename absurd_elim to absurd, delete contrapos and trivial_not_true theorems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-08-27 18:34:09 -07:00
+								end