From 49e7a642c35e83ed16cbc573deef5bd3b6dfc627 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Dec 2017 19:10:10 -0800 Subject: [PATCH] feat(library/init/meta/interactive): merge `ginduction` and `induction` This commit is based on 638b34b16de6443. The changes were applied manually to make sure all changes are compatible with our plans to `induction`. --- doc/changes.md | 2 + library/init/data/bool/lemmas.lean | 2 +- library/init/data/list/qsort.lean | 4 +- library/init/data/nat/bitwise.lean | 4 +- library/init/data/nat/lemmas.lean | 2 +- library/init/meta/interactive.lean | 100 +++++++++++++------------ library/init/meta/smt/interactive.lean | 2 +- 7 files changed, 61 insertions(+), 55 deletions(-) diff --git a/doc/changes.md b/doc/changes.md index 704b81eff7..df336b871b 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -117,6 +117,8 @@ master branch (aka work in progress branch) In this case, `apply t` behaves as `apply t _ ... _` where `n` `_` have been added, independently of the goal target type. The new behavior is useful when using `apply` with eliminator-like definitions. +- `ginduction t with h h1 h2` is now `induction h : t with h1 h2`. + *API name changes* v3.3.0 (14 September 2017) diff --git a/library/init/data/bool/lemmas.lean b/library/init/data/bool/lemmas.lean index 80c73aba52..c378a8ef0f 100644 --- a/library/init/data/bool/lemmas.lean +++ b/library/init/data/bool/lemmas.lean @@ -126,7 +126,7 @@ theorem of_to_bool_ff {p : Prop} [decidable p] : to_bool p = ff → ¬p := (to_b theorem to_bool_congr {p q : Prop} [decidable p] [decidable q] (h : p ↔ q) : to_bool p = to_bool q := begin - ginduction to_bool q with h', + induction h' : to_bool q, exact to_bool_ff (mt h.1 $ of_to_bool_ff h'), exact to_bool_true (h.2 $ of_to_bool_true h') end diff --git a/library/init/data/list/qsort.lean b/library/init/data/list/qsort.lean index d736e759d8..1bde114faa 100644 --- a/library/init/data/list/qsort.lean +++ b/library/init/data/list/qsort.lean @@ -14,7 +14,7 @@ def qsort.F {α} (lt : α → α → bool) : Π (x : list α), (Π (y : list α), length y < length x → list α) → list α | [] IH := [] | (h::t) IH := begin - ginduction partition (λ x, lt h x = tt) t with e large small, + induction e : partition (λ x, lt h x = tt) t with large small, have : length small < length (h::t) ∧ length large < length (h::t), { rw partition_eq_filter_filter at e, injection e, @@ -38,7 +38,7 @@ by rw [qsort, well_founded.fix_eq, qsort.F] qsort lt small ++ h :: qsort lt large := begin rw [qsort, well_founded.fix_eq, qsort.F], - ginduction partition (λ x, lt h x = tt) t with e large small, + induction e : partition (λ x, lt h x = tt) t with large small, simp [e], rw [e] end diff --git a/library/init/data/nat/bitwise.lean b/library/init/data/nat/bitwise.lean index 36b72137b3..8ceea3c316 100644 --- a/library/init/data/nat/bitwise.lean +++ b/library/init/data/nat/bitwise.lean @@ -235,7 +235,7 @@ lemma bitwise_bit_aux {f : bool → bool → bool} (h : f ff ff = ff) : begin funext n, apply bit_cases_on n, intros b n, rw [binary_rec_eq], - { cases b; try {rw h}; ginduction f ff tt with fft; simp [cond]; refl }, + { cases b; try {rw h}; induction fft : f ff tt; simp [cond]; refl }, { rw [h, show cond (f ff tt) 0 0 = 0, by cases f ff tt; refl, show cond (f tt ff) (bit ff 0) 0 = 0, by cases f tt ff; refl]; refl } end @@ -258,7 +258,7 @@ by rw bitwise_zero_left; cases f ff tt; refl begin unfold bitwise, rw [binary_rec_eq, binary_rec_eq], - { ginduction f tt ff with ftf; dsimp [cond], + { induction ftf : f tt ff; dsimp [cond], rw [show f a ff = ff, by cases a; assumption], apply @congr_arg _ _ _ 0 (bit ff), tactic.swap, rw [show f a ff = a, by cases a; assumption], diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index ad003ed891..49e985c25f 100644 --- a/library/init/data/nat/lemmas.lean +++ b/library/init/data/nat/lemmas.lean @@ -894,7 +894,7 @@ theorem succ_inj {n m : ℕ} (H : succ n = succ m) : n = m := nat.succ.inj_arrow H id theorem discriminate {B : Sort u} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B := -by ginduction n with h; [exact H1 h, exact H2 _ h] +by induction h : n; [exact H1 h, exact H2 _ h] theorem one_succ_zero : 1 = succ 0 := rfl diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index ddac1c22b9..e0c316e1a9 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -378,6 +378,44 @@ do e_type ← infer_type e >>= whnf, (const I ls) ← return $ get_app_fn e_type, return I +private meta def generalize_arg_p_aux : pexpr → parser (pexpr × name) +| (app (app (macro _ [const `eq _ ]) h) (local_const x _ _ _)) := pure (h, x) +| _ := fail "parse error" + + +private meta def generalize_arg_p : parser (pexpr × name) := +with_desc "expr = id" $ parser.pexpr 0 >>= generalize_arg_p_aux + +/-- +`generalize : e = x` replaces all occurrences of `e` in the target with a new hypothesis `x` of the same type. + +`generalize h : e = x` in addition registers the hypothesis `h : e = x`. +-/ +meta def generalize (h : parse ident?) (_ : parse $ tk ":") (p : parse generalize_arg_p) : tactic unit := +do let (p, x) := p, + e ← i_to_expr p, + some h ← pure h | tactic.generalize e x >> intro1 >> skip, + tgt ← target, + -- if generalizing fails, fall back to not replacing anything + tgt' ← do { + ⟨tgt', _⟩ ← solve_aux tgt (tactic.generalize e x >> target), + to_expr ``(Π x, %%e = x → %%(tgt'.binding_body.lift_vars 0 1)) + } <|> to_expr ``(Π x, %%e = x → %%tgt), + t ← assert h tgt', + swap, + exact ``(%%t %%e rfl), + intro x, + intro h + +meta def cases_arg_p : parser (option name × pexpr) := +with_desc "(id :)? expr" $ do + t ← texpr, + match t with + | (local_const x _ _ _) := + (tk ":" *> do t ← texpr, pure (some x, t)) <|> pure (none, t) + | _ := pure (none, t) + end + precedence `generalizing` : 0 /-- @@ -392,14 +430,24 @@ For example, given `n : nat` and a goal with a hypothesis `h : P n` and target ` `induction e using r` allows the user to specify the principle of induction that should be used. Here `r` should be a theorem whose result type must be of the form `C t`, where `C` is a bound variable and `t` is a (possibly empty) sequence of bound variables `induction e generalizing z₁ ... zₙ`, where `z₁ ... zₙ` are variables in the local context, generalizes over `z₁ ... zₙ` before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized. + +`induction h : t` will introduce an equality of the form `h : t = C x y`, asserting that the input term is equal to the current constructor case, to the context. -/ -meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list) +meta def induction (hp : parse cases_arg_p) (rec_name : parse using_ident) (ids : parse with_ident_list) (revert : parse $ (tk "generalizing" *> ident*)?) : tactic unit := -do e ← i_to_expr p, +do + -- process `h : t` case + e ← match hp with + | (some h, p) := do + x ← mk_fresh_name, + generalize h () (p, x), + get_local x + | (none, p) := i_to_expr p + end, -- generalize major premise e ← if e.is_local_constant then pure e - else generalize e >> intro1, + else tactic.generalize e >> intro1, -- generalize major premise args (e, newvars, locals) ← do { @@ -534,50 +582,6 @@ For example, given `n : nat` and a goal with a hypothesis `h : P n` and target ` meta def destruct (p : parse texpr) : tactic unit := i_to_expr p >>= tactic.destruct -private meta def generalize_arg_p : pexpr → parser (pexpr × name) -| (app (app (macro _ [const `eq _ ]) h) (local_const x _ _ _)) := pure (h, x) -| _ := fail "parse error" - -/-- -`generalize : e = x` replaces all occurrences of `e` in the target with a new hypothesis `x` of the same type. - -`generalize h : e = x` in addition registers the hypothesis `h : e = x`. --/ -meta def generalize (h : parse ident?) (p : parse $ tk ":" *> with_desc "expr = id" (parser.pexpr 0 >>= generalize_arg_p)) : tactic unit := -do let (p, x) := p, - e ← i_to_expr p, - some h ← pure h | tactic.generalize e x >> intro1 >> skip, - tgt ← target, - -- if generalizing fails, fall back to not replacing anything - tgt' ← do { - ⟨tgt', _⟩ ← solve_aux tgt (tactic.generalize e x >> target), - to_expr ``(Π x, %%e = x → %%(tgt'.binding_body.lift_vars 0 1)) - } <|> to_expr ``(Π x, %%e = x → %%tgt), - t ← assert h tgt', - swap, - exact ``(%%t %%e rfl), - intro x, - intro h - -meta def ginduction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list) : tactic unit := -do x ← mk_fresh_name, - let (h, hs) := (match ids with - | [] := (`_h, []) - | (h :: hs) := (h, hs) - end : name × list name), - generalize h (p, x), - t ← get_local x, - induction (to_pexpr t) rec_name hs ([] : list name) - -private meta def cases_arg_p : parser (option name × pexpr) := -with_desc "(id :)? expr" $ do - t ← texpr, - match t with - | (local_const x _ _ _) := - (tk ":" *> do t ← texpr, pure (some x, t)) <|> pure (none, t) - | _ := pure (none, t) - end - /-- Assuming `x` is a variable in the local context with an inductive type, `cases x` splits the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor. If the type of an element in the local context depends on `x`, that element is reverted and reintroduced afterward, so that the case split affects that hypothesis as well. @@ -595,7 +599,7 @@ meta def cases : parse cases_arg_p → parse with_ident_list → tactic unit tactic.cases e ids | (some h, p) ids := do x ← mk_fresh_name, - generalize h (p, x), + generalize h () (p, x), hx ← get_local x, tactic.cases hx ids diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean index a8dd5a2ea4..ffa611358e 100644 --- a/library/init/meta/smt/interactive.lean +++ b/library/init/meta/smt/interactive.lean @@ -229,7 +229,7 @@ smt_tactic.iterate t meta def all_goals (t : itactic) : smt_tactic unit := smt_tactic.all_goals t -meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list) +meta def induction (p : parse tactic.interactive.cases_arg_p) (rec_name : parse using_ident) (ids : parse with_ident_list) (revert : parse $ (tk "generalizing" *> ident*)?) : smt_tactic unit := slift (tactic.interactive.induction p rec_name ids revert)