feat(library/tactic/constructor_tactic): restore 'constructor' tactic old semantics, add 'fconstructor' tactic
See issue #676 Add new test demonstrating why it is useful to have the old semantics for 'constructor'
This commit is contained in:
Leonardo de Moura
parent
bf71d9f342
commit
a4c0699e81
7 changed files with 37 additions and 20 deletions
|
|
@ -109,11 +109,12 @@ definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin
|
|||
|
||||
definition lettac (id : identifier) (e : expr) : tactic := builtin
|
||||
|
||||
definition constructor (k : option num) : tactic := builtin
|
||||
definition existsi (e : expr) : tactic := builtin
|
||||
definition split : tactic := builtin
|
||||
definition left : tactic := builtin
|
||||
definition right : tactic := builtin
|
||||
definition constructor (k : option num) : tactic := builtin
|
||||
definition fconstructor (k : option num) : tactic := builtin
|
||||
definition existsi (e : expr) : tactic := builtin
|
||||
definition split : tactic := builtin
|
||||
definition left : tactic := builtin
|
||||
definition right : tactic := builtin
|
||||
|
||||
definition injection (e : expr) (ids : opt_identifier_list) : tactic := builtin
|
||||
|
||||
|
|
|
|||
|
|
@ -109,11 +109,12 @@ definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin
|
|||
|
||||
definition lettac (id : identifier) (e : expr) : tactic := builtin
|
||||
|
||||
definition constructor (k : option num) : tactic := builtin
|
||||
definition existsi (e : expr) : tactic := builtin
|
||||
definition split : tactic := builtin
|
||||
definition left : tactic := builtin
|
||||
definition right : tactic := builtin
|
||||
definition constructor (k : option num) : tactic := builtin
|
||||
definition fconstructor (k : option num) : tactic := builtin
|
||||
definition existsi (e : expr) : tactic := builtin
|
||||
definition split : tactic := builtin
|
||||
definition left : tactic := builtin
|
||||
definition right : tactic := builtin
|
||||
|
||||
definition injection (e : expr) (ids : opt_identifier_list) : tactic := builtin
|
||||
|
||||
|
|
|
|||
|
|
@ -139,7 +139,7 @@
|
|||
"generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact"
|
||||
"refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite"
|
||||
"xrewrite" "krewrite" "esimp" "unfold" "change" "check_expr" "contradiction"
|
||||
"exfalso" "split" "existsi" "constructor" "left" "right" "injection" "congruence" "reflexivity"
|
||||
"exfalso" "split" "existsi" "constructor" "fconstructor" "left" "right" "injection" "congruence" "reflexivity"
|
||||
"symmetry" "transitivity" "state" "induction" "induction_using"
|
||||
"substvars"))
|
||||
word-end)
|
||||
|
|
|
|||
|
|
@ -22,7 +22,8 @@ namespace lean {
|
|||
If \c given_args is provided, then the tactic fixes the given arguments.
|
||||
It creates a subgoal for each remaining argument.
|
||||
*/
|
||||
tactic constructor_tactic(elaborate_fn const & elab, optional<unsigned> _i, optional<unsigned> num_constructors, list<expr> const & given_args) {
|
||||
tactic constructor_tactic(elaborate_fn const & elab, optional<unsigned> _i, optional<unsigned> num_constructors,
|
||||
list<expr> const & given_args, bool use_fapply = false) {
|
||||
auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
|
||||
goals const & gs = s.get_goals();
|
||||
if (empty(gs)) {
|
||||
|
|
@ -83,7 +84,10 @@ tactic constructor_tactic(elaborate_fn const & elab, optional<unsigned> _i, opti
|
|||
return proof_state_seq();
|
||||
}
|
||||
}
|
||||
return fapply_tactic_core(env, ios, new_s, C, cs);
|
||||
if (use_fapply)
|
||||
return fapply_tactic_core(env, ios, new_s, C, cs);
|
||||
else
|
||||
return apply_tactic_core(env, ios, new_s, C, cs);
|
||||
};
|
||||
|
||||
if (_i) {
|
||||
|
|
@ -109,6 +113,11 @@ void initialize_constructor_tactic() {
|
|||
auto i = get_optional_unsigned(tc, app_arg(e));
|
||||
return constructor_tactic(fn, i, optional<unsigned>(), list<expr>());
|
||||
});
|
||||
register_tac(name{"tactic", "fconstructor"},
|
||||
[](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
|
||||
auto i = get_optional_unsigned(tc, app_arg(e));
|
||||
return constructor_tactic(fn, i, optional<unsigned>(), list<expr>(), true);
|
||||
});
|
||||
register_tac(name{"tactic", "split"},
|
||||
[](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
|
||||
return constructor_tactic(fn, optional<unsigned>(1), optional<unsigned>(1), list<expr>());
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ mk : ∀ {a : nat}, a > 0 → foo
|
|||
|
||||
example (b : nat) (h : b > 1) : foo :=
|
||||
begin
|
||||
constructor,
|
||||
fconstructor,
|
||||
exact b,
|
||||
exact lt_of_succ_lt h
|
||||
end
|
||||
|
|
|
|||
6
tests/lean/run/eassumption.lean
Normal file
6
tests/lean/run/eassumption.lean
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
variable p : nat → Prop
|
||||
variable q : nat → Prop
|
||||
variables a b c : nat
|
||||
|
||||
example : p c → p b → q b → p a → ∃ x, p x ∧ q x :=
|
||||
by intros; repeat (constructor | eassumption); now
|
||||
|
|
@ -90,26 +90,26 @@ namespace PropF
|
|||
lemma weakening2 : ∀ {Γ A Δ}, Γ ⊢ A → Γ ⊆ Δ → Δ ⊢ A
|
||||
| Γ ⌞A⌟ Δ (Nax Γ A Hin) Hs := by constructor; exact Hs Hin
|
||||
| Γ ⌞A ⇒ B⌟ Δ (ImpI Γ A B H) Hs := by constructor; exact weakening2 H (cons_sub_cons A Hs)
|
||||
| Γ ⌞B⌟ Δ (ImpE Γ A B H₁ H₂) Hs := by constructor; eassumption; exact weakening2 H₁ Hs; exact weakening2 H₂ Hs
|
||||
| Γ ⌞B⌟ Δ (ImpE Γ A B H₁ H₂) Hs := by constructor; exact weakening2 H₁ Hs; exact weakening2 H₂ Hs
|
||||
| Γ ⌞A⌟ Δ (BotC Γ A H) Hs := by constructor; exact weakening2 H (cons_sub_cons (~A) Hs)
|
||||
| Γ ⌞A ∧ B⌟ Δ (AndI Γ A B H₁ H₂) Hs := by constructor; exact weakening2 H₁ Hs; exact weakening2 H₂ Hs
|
||||
| Γ ⌞A⌟ Δ (AndE₁ Γ A B H) Hs := by constructor; eassumption; exact weakening2 H Hs
|
||||
| Γ ⌞B⌟ Δ (AndE₂ Γ A B H) Hs := by constructor; eassumption; exact weakening2 H Hs
|
||||
| Γ ⌞A⌟ Δ (AndE₁ Γ A B H) Hs := by constructor; exact weakening2 H Hs
|
||||
| Γ ⌞B⌟ Δ (AndE₂ Γ A B H) Hs := by constructor; exact weakening2 H Hs
|
||||
| Γ ⌞A ∨ B⌟ Δ (OrI₁ Γ A B H) Hs := by constructor; exact weakening2 H Hs
|
||||
| Γ ⌞A ∨ B⌟ Δ (OrI₂ Γ A B H) Hs := by constructor; exact weakening2 H Hs
|
||||
| Γ ⌞C⌟ Δ (OrE Γ A B C H₁ H₂ H₃) Hs :=
|
||||
by constructor; eassumption; eassumption; exact weakening2 H₁ Hs; exact weakening2 H₂ (cons_sub_cons A Hs); exact weakening2 H₃ (cons_sub_cons B Hs)
|
||||
by constructor; exact weakening2 H₁ Hs; exact weakening2 H₂ (cons_sub_cons A Hs); exact weakening2 H₃ (cons_sub_cons B Hs)
|
||||
|
||||
lemma weakening : ∀ Γ Δ A, Γ ⊢ A → Γ++Δ ⊢ A :=
|
||||
λ Γ Δ A H, weakening2 H (sub_append_left Γ Δ)
|
||||
|
||||
lemma deduction : ∀ Γ A B, Γ ⊢ A ⇒ B → A::Γ ⊢ B :=
|
||||
λ Γ A B H, by constructor; exact A; exact weakening2 H (sub_cons A Γ); constructor; exact mem_cons A Γ
|
||||
λ Γ A B H, by constructor; exact weakening2 H (sub_cons A Γ); constructor; exact mem_cons A Γ
|
||||
|
||||
lemma prov_impl : ∀ A B, Provable (A ⇒ B) → ∀ Γ, Γ ⊢ A → Γ ⊢ B :=
|
||||
λ A B Hp Γ Ha,
|
||||
assert wHp : Γ ⊢ (A ⇒ B), from !weakening Hp,
|
||||
by constructor; eassumption; eassumption; eassumption
|
||||
by constructor; eassumption; eassumption
|
||||
|
||||
lemma Satisfies_cons : ∀ {A Γ v}, Satisfies v Γ → is_true (TrueQ v A) → Satisfies v (A::Γ) :=
|
||||
λ A Γ v s t B BinAG,
|
||||
|
|
|
|||
Loading…
Reference in a new issue