michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/tactic/boolean_tactics): avoid unnecessary Let expression in proof terms

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-06 15:01:54 -08:00
parent 1df9d18891
commit 0390f3c39b
4 changed files with 12 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/abstract.h
View file

@ -52,6 +52,10 @@ inline expr Let(name const & x, expr const & v, expr const & b) { return mk_let(
inline expr Let(expr const & x, expr const & v, expr const & b) { return mk_let(const_name(x), expr(), v, abstract(b, x)); }
inline expr Let(std::pair<expr const &, expr const &> const & p, expr const & b) { return Let(p.first, p.second, b); }
expr Let(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b);
/**
\brief Similar to Let(x, v, b), but returns v if x == b
*/
inline expr Let_simp(expr const & x, expr const & v, expr const & b) { return x == b ? v : Let(x, v, b); }
/**
\brief Create a Let expression (Let x : t := v in b), the term b is abstracted using abstract(b, x).

4
src/library/tactic/boolean_tactics.cpp
View file

@ -141,9 +141,9 @@ tactic conj_hyp_tactic(bool all) {
expr const & H_1 = mk_constant(name(H_name, 1));
expr const & H_2 = mk_constant(name(H_name, 2));
if (occurs(H_1, pr))
pr = Let(H_1, Conjunct1(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr);
pr = Let_simp(H_1, Conjunct1(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr);
if (occurs(H_2, pr))
pr = Let(H_2, Conjunct2(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr);
pr = Let_simp(H_2, Conjunct2(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr);
}
new_m.insert(goal_name, pr);
}

4
tests/lean/interactive/t12.lean
View file

@ -1,6 +1,6 @@
(**
-- Define a simple tactic using Lua
auto = REPEAT(ORELSE(conj_hyp_tac, conj_tac, assumption_tac))
auto = REPEAT(ORELSE(assumption_tac, conj_tac, conj_hyp_tac))
**)
(*
@ -17,6 +17,8 @@ Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
lemma2 : B := (by auto)
in (show B /\ A by auto)
Show Environment 1. (* Show proof for the previous theorem *)
(*
When hints are not provided, the user must fill the (remaining) holes using tactic command sequences.
Each hole must be filled with a tactic command sequence that terminates with the command 'done' and

4
tests/lean/interactive/t12.lean.expected.out
View file

@ -2,7 +2,9 @@ Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
# Set: pp::colors
Set: pp::unicode
Proved: T1
Proof state:
Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
let lemma1 : A := Conjunct1 assumption, lemma2 : B := Conjunct2 assumption in Conj lemma2 lemma1
# Proof state:
A : Bool, B : Bool, assumption : A ∧ B ⊢ A
## Proof state:
no goals