From 7d39b3e94884ad3c7e35da2f93b02077bb984e9a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 8 Jul 2017 18:28:57 +0200 Subject: [PATCH] refactor(init/meta/interactive): merge generalize and generalize2 and introduce nicer syntax --- doc/changes.md | 2 ++ library/data/bitvec.lean | 16 ++++++++-------- library/data/hash_map.lean | 2 +- library/init/data/nat/bitwise.lean | 26 +++++++++++++++----------- library/init/meta/interactive.lean | 18 +++++++++++------- tests/lean/run/generalize_inst.lean | 4 ++-- 6 files changed, 39 insertions(+), 29 deletions(-) diff --git a/doc/changes.md b/doc/changes.md index 866a4f3936..3758e6d8b4 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -90,6 +90,8 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/ * Universes `max u v + 1` and `imax u v + 1` are now parsed as `(max u v) + 1` and `(imax u v) + 1`. +* Merged `generalize` and `generalize2` tactics into new `generalize id? : expr = id` tactic + *API name changes* * `list.dropn` => `list.drop` diff --git a/library/data/bitvec.lean b/library/data/bitvec.lean index 082d7f0317..4fbfac3300 100644 --- a/library/data/bitvec.lean +++ b/library/data/bitvec.lean @@ -164,14 +164,14 @@ section conversion cases xs with xs P, simp [bits_to_nat_to_list], clear P, unfold bits_to_nat list.foldl, - -- the next 4 lines generalize the accumulator of foldl - let x := 0, - change _ = add_lsb x b + _, - generalize 0 y, - revert x, simp, - induction xs with x xs ; intro y, - { simp, unfold list.foldl add_lsb, simp [nat.mul_succ] }, - { simp, apply ih_1 } + -- generalize the accumulator of foldl + have : ∀ x, list.foldl add_lsb x (xs ++ [b]) = add_lsb 0 b + list.foldl add_lsb x xs * 2, { + simp, + induction xs with x xs ; intro y, + { simp, unfold list.foldl add_lsb, simp [nat.mul_succ] }, + { simp, apply ih_1 } + }, + apply this end theorem bits_to_nat_to_bool (n : ℕ) diff --git a/library/data/hash_map.lean b/library/data/hash_map.lean index 13bd2c9722..49daf6bf4a 100644 --- a/library/data/hash_map.lean +++ b/library/data/hash_map.lean @@ -640,7 +640,7 @@ match (by apply_instance : decidable (contains_aux a bkt)) with have h : bkts'' = bkts'.as_list.foldl _ _, from bkts'.foldl_eq _ _, begin rw [← list.foldr_reverse] at h, rw h, - generalize bkts'.as_list.reverse l, intro l, induction l with a l IH, + generalize : bkts'.as_list.reverse = l, induction l with a l IH, { simp, rw[mk_as_list hash_fn n'], simp }, { cases a with a'' b'', simp, rw [← IH], exact let B := l.foldr (λ y (x : bucket_array α β n'), diff --git a/library/init/data/nat/bitwise.lean b/library/init/data/nat/bitwise.lean index 067ecfac93..4cdc0e92d1 100644 --- a/library/init/data/nat/bitwise.lean +++ b/library/init/data/nat/bitwise.lean @@ -203,17 +203,21 @@ namespace nat binary_rec z f (bit b n) = f b n (binary_rec z f n) := begin rw [binary_rec], - by_cases bit b n = 0 with h'; simp [h'], - { generalize (binary_rec._main._pack._proof_1 (bit b n) h') e, - have bf := bodd_bit b n, - have n0 := div2_bit b n, - rw h' at bf n0, - simp at bf n0, - rw [← bf, ← n0, binary_rec_zero], - intros, exact h.symm }, - { generalize (binary_rec._main._pack._proof_2 (bit b n)) e, - rw [bodd_bit, div2_bit], - intros, refl } + by_cases (bit b n = 0) with h', + {simp [dif_pos h'], + generalize : binary_rec._main._pack._proof_1 (bit b n) h' = e, + revert e, + have bf := bodd_bit b n, + have n0 := div2_bit b n, + rw h' at bf n0, + simp at bf n0, + rw [← bf, ← n0, binary_rec_zero], + intros, exact h.symm }, + {simp [dif_neg h'], + generalize : binary_rec._main._pack._proof_2 (bit b n) = e, + revert e, + rw [bodd_bit, div2_bit], + intros, refl} end lemma bitwise_bit_aux {f : bool → bool → bool} (h : f ff ff = ff) : diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index ae1661849f..af33d01b13 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -455,16 +455,20 @@ do r ← result, meta def destruct (p : parse texpr) : tactic unit := i_to_expr p >>= tactic.destruct -meta def generalize (p : parse parser.pexpr) (x : parse ident) : tactic unit := -do e ← i_to_expr p, - tactic.generalize e x +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" -meta def generalize2 (p : parse parser.pexpr) (x : parse ident) (h : parse ident) : tactic unit := -do tgt ← target, +/-- `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 `_ >> target), + ⟨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', @@ -479,7 +483,7 @@ do x ← mk_fresh_name, | [] := (`_h, []) | (h :: hs) := (h, hs) end : name × list name), - generalize2 p x h, + generalize h (p, x), t ← get_local x, induction (to_pexpr t) rec_name hs ([] : list name) diff --git a/tests/lean/run/generalize_inst.lean b/tests/lean/run/generalize_inst.lean index 99ba5d02ce..ff3dca4bd7 100644 --- a/tests/lean/run/generalize_inst.lean +++ b/tests/lean/run/generalize_inst.lean @@ -5,6 +5,6 @@ begin apply exists.intro, apply and.intro, apply rfl, - generalize 1 z, - exact nat.zero_le + generalize : 1 = z, + apply nat.zero_le end