From a4c0699e814754ffc80a90204d23c25641d3172d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 17 Jun 2015 23:48:54 -0700 Subject: [PATCH] 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' --- hott/init/tactic.hlean | 11 ++++++----- library/init/tactic.lean | 11 ++++++----- src/emacs/lean-syntax.el | 2 +- src/library/tactic/constructor_tactic.cpp | 13 +++++++++++-- tests/lean/run/676.lean | 2 +- tests/lean/run/eassumption.lean | 6 ++++++ tests/lean/run/soundness.lean | 12 ++++++------ 7 files changed, 37 insertions(+), 20 deletions(-) create mode 100644 tests/lean/run/eassumption.lean diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index d51e75e81..99e29d384 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -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 diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 895d0714c..eff940036 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -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 diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index f62789c85..943c95a32 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -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) diff --git a/src/library/tactic/constructor_tactic.cpp b/src/library/tactic/constructor_tactic.cpp index 19e7f4e67..a9a4d60e0 100644 --- a/src/library/tactic/constructor_tactic.cpp +++ b/src/library/tactic/constructor_tactic.cpp @@ -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 _i, optional num_constructors, list const & given_args) { +tactic constructor_tactic(elaborate_fn const & elab, optional _i, optional num_constructors, + list 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 _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(), list()); }); + 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(), list(), true); + }); register_tac(name{"tactic", "split"}, [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) { return constructor_tactic(fn, optional(1), optional(1), list()); diff --git a/tests/lean/run/676.lean b/tests/lean/run/676.lean index 136d199d0..d3e8b2c3f 100644 --- a/tests/lean/run/676.lean +++ b/tests/lean/run/676.lean @@ -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 diff --git a/tests/lean/run/eassumption.lean b/tests/lean/run/eassumption.lean new file mode 100644 index 000000000..833d68745 --- /dev/null +++ b/tests/lean/run/eassumption.lean @@ -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 diff --git a/tests/lean/run/soundness.lean b/tests/lean/run/soundness.lean index e1cd93b95..5c33e2d07 100644 --- a/tests/lean/run/soundness.lean +++ b/tests/lean/run/soundness.lean @@ -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,