From 2185ee7e95f27f190b5e3cd26124ef43e684fb73 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 10 Dec 2015 19:37:55 +0100 Subject: [PATCH] feat(library/tactic): make let tactic transparent, introduce new opaque note tactic The new let tactic is semantically equivalent to let terms, while `note` preserves its old opaque behavior. --- hott/algebra/category/functor/adjoint.hlean | 24 +++++++++---------- hott/cubical/pathover2.hlean | 2 +- hott/cubical/squareover.hlean | 4 ++-- hott/homotopy/circle.hlean | 2 +- hott/homotopy/join.hlean | 2 +- hott/homotopy/sphere.hlean | 2 +- hott/init/tactic.hlean | 2 +- hott/types/univ.hlean | 4 ++-- library/data/int/order.lean | 4 ++-- library/data/real/basic.lean | 10 ++++---- library/data/real/complete.lean | 8 +++---- library/data/real/division.lean | 8 +++---- library/data/real/order.lean | 14 +++++------ library/init/tactic.lean | 2 +- library/theories/analysis/real_limit.lean | 6 ++--- library/theories/number_theory/bezout.lean | 2 +- .../number_theory/irrational_roots.lean | 2 +- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_tactics.cpp | 19 +++++++++++++-- src/frontends/lean/token_table.cpp | 2 +- src/library/constants.cpp | 8 +++---- src/library/constants.h | 2 +- src/library/constants.txt | 2 +- src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/init_module.cpp | 6 ++--- .../{let_tactic.cpp => note_tactic.cpp} | 20 ++++++++-------- .../tactic/{let_tactic.h => note_tactic.h} | 6 ++--- tests/lean/hott/670.hlean | 2 +- .../lean/interactive/alias.input.expected.out | 2 -- tests/lean/run/blast_cc8.lean | 2 +- tests/lean/run/congr_tac2.lean | 2 +- tests/lean/run/dep_subst.lean | 2 +- tests/lean/run/let_tac.lean | 2 ++ 33 files changed, 97 insertions(+), 82 deletions(-) rename src/library/tactic/{let_tactic.cpp => note_tactic.cpp} (75%) rename src/library/tactic/{let_tactic.h => note_tactic.h} (65%) diff --git a/hott/algebra/category/functor/adjoint.hlean b/hott/algebra/category/functor/adjoint.hlean index e5124bf32..75a4fb9b2 100644 --- a/hott/algebra/category/functor/adjoint.hlean +++ b/hott/algebra/category/functor/adjoint.hlean @@ -124,12 +124,12 @@ namespace category fapply nat_trans.mk: esimp, { intro c, exact natural_map (to_hom θ) (c, F c) id}, { intro c c' f, - let H := naturality (to_hom θ) (ID c, F f), - let K := ap10 H id, + note H := naturality (to_hom θ) (ID c, F f), + note K := ap10 H id, rewrite [▸* at K, id_right at K, ▸*, K, respect_id, +id_right], clear H K, - let H := naturality (to_hom θ) (f, ID (F c')), - let K := ap10 H id, + note H := naturality (to_hom θ) (f, ID (F c')), + note K := ap10 H id, rewrite [▸* at K, respect_id at K,+id_left at K, K]} end @@ -138,12 +138,12 @@ namespace category fapply nat_trans.mk: esimp, { intro d, exact natural_map (to_inv θ) (G d, d) id, }, { intro d d' g, - let H := naturality (to_inv θ) (Gᵒᵖᶠ g, ID d'), - let K := ap10 H id, + note H := naturality (to_inv θ) (Gᵒᵖᶠ g, ID d'), + note K := ap10 H id, rewrite [▸* at K, id_left at K, ▸*, K, respect_id, +id_left], clear H K, - let H := naturality (to_inv θ) (ID (G d), g), - let K := ap10 H id, + note H := naturality (to_inv θ) (ID (G d), g), + note K := ap10 H id, rewrite [▸* at K, respect_id at K,+id_right at K, K]} end @@ -151,8 +151,8 @@ namespace category : natural_map (to_hom θ) (c, d) f = G f ∘ adj_unit c := begin esimp, - let H := naturality (to_hom θ) (ID c, f), - let K := ap10 H id, + note H := naturality (to_hom θ) (ID c, f), + note K := ap10 H id, rewrite [▸* at K, id_right at K, K, respect_id, +id_right], end @@ -160,8 +160,8 @@ namespace category : natural_map (to_inv θ) (c, d) g = adj_counit d ∘ F g := begin esimp, - let H := naturality (to_inv θ) (g, ID d), - let K := ap10 H id, + note H := naturality (to_inv θ) (g, ID d), + note K := ap10 H id, rewrite [▸* at K, id_left at K, K, respect_id, +id_left], end diff --git a/hott/cubical/pathover2.hlean b/hott/cubical/pathover2.hlean index addbf9ace..193ac69c7 100644 --- a/hott/cubical/pathover2.hlean +++ b/hott/cubical/pathover2.hlean @@ -109,7 +109,7 @@ namespace eq begin rewrite [apdo_eq_apdo_ap _ _ p], let y := !change_path_of_pathover (apdo (apdo id) (ap_constant p b))⁻¹ᵒ, - rewrite -y, esimp, clear y, + rewrite -y, esimp, refine !pathover_ap_pathover_of_pathover_ap ⬝ _, rewrite pathover_ap_change_path, rewrite -change_path_con, apply ap (λx, change_path x idpo), diff --git a/hott/cubical/squareover.hlean b/hott/cubical/squareover.hlean index b37c5065c..f9f76513b 100644 --- a/hott/cubical/squareover.hlean +++ b/hott/cubical/squareover.hlean @@ -146,7 +146,7 @@ namespace eq (pathover_idp_of_eq l) (pathover_idp_of_eq r)) : square t b l r := begin - let H := square_of_squareover so, -- use apply ... in + note H := square_of_squareover so, -- use apply ... in rewrite [▸* at H,+idp_con at H,+ap_id at H,↑pathover_idp_of_eq at H], rewrite [+to_right_inv !(pathover_equiv_tr_eq (refl a)) at H], exact H @@ -230,7 +230,7 @@ namespace eq definition eq_of_vdeg_squareover {q₁₀' : b₀₀ =[p₁₀] b₂₀} (p : squareover B vrfl q₁₀ q₁₀' idpo idpo) : q₁₀ = q₁₀' := begin - let H := square_of_squareover p, -- use apply ... in + note H := square_of_squareover p, -- use apply ... in induction p₁₀, -- if needed we can remove this induction and use con_tr_idp in types/eq2 rewrite [▸* at H,idp_con at H,+ap_id at H], let H' := eq_of_vdeg_square H, diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index 9e6653cac..ab562546c 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -263,7 +263,7 @@ namespace circle induction x, { apply base_eq_base_equiv}, { apply equiv_pathover, intro p p' q, apply pathover_of_eq, - let H := eq_of_square (square_of_pathover q), + note H := eq_of_square (square_of_pathover q), rewrite con_comm_base at H, let H' := cancel_left H, induction H', reflexivity} diff --git a/hott/homotopy/join.hlean b/hott/homotopy/join.hlean index 7b1aecce1..f1dc334ee 100644 --- a/hott/homotopy/join.hlean +++ b/hott/homotopy/join.hlean @@ -128,7 +128,7 @@ namespace join (c : cube s₀₁₁ vrfl s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₁₁₂⁻¹ᵛ vrfl (massage_sq s₁₀₁) (massage_sq s₁₂₁) s₁₁₀⁻¹ᵛ s₀₁₁⁻¹ᵛ := begin - cases p₁₀₀, cases p₁₀₂, cases p₁₂₂, let c' := massage_cube' c, esimp[massage_sq], + cases p₁₀₀, cases p₁₀₂, cases p₁₂₂, note c' := massage_cube' c, esimp[massage_sq], krewrite vdeg_v_eq_ph_pv_hp at c', exact c', end diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index d6c1655df..b7dd1f3fe 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -188,7 +188,7 @@ namespace is_trunc (a : A) (f : map₊ (S. n) (pointed.Mk a)) (x : S n) : f x = f base := begin let H' := iff.elim_left (is_trunc_iff_is_contr_loop n A) H a, - let H'' := @is_trunc_equiv_closed_rev _ _ _ !pmap_sphere H', + note H'' := @is_trunc_equiv_closed_rev _ _ _ !pmap_sphere H', assert p : (f = pmap.mk (λx, f base) (respect_pt f)), apply is_hprop.elim, exact ap10 (ap pmap.map p) x diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 3e389c9a8..77554f3fc 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -126,7 +126,7 @@ definition change (e : expr) : tactic := builtin definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin -definition lettac (id : identifier) (e : expr) : tactic := builtin +definition notetac (id : identifier) (e : expr) : tactic := builtin definition constructor (k : option num) : tactic := builtin definition fconstructor (k : option num) : tactic := builtin diff --git a/hott/types/univ.hlean b/hott/types/univ.hlean index 720e37fad..ff554d914 100644 --- a/hott/types/univ.hlean +++ b/hott/types/univ.hlean @@ -52,10 +52,10 @@ namespace univ intro f, have u : ¬¬bool, by exact (λg, g tt), let H1 := apdo f eq_bnot, - let H2 := apo10 H1 u, + note H2 := apo10 H1 u, have p : eq_bnot ▸ u = u, from !is_hprop.elim, rewrite p at H2, - let H3 := eq_of_pathover_ua H2, esimp at H3, --TODO: use apply ... at after #700 + note H3 := eq_of_pathover_ua H2, esimp at H3, --TODO: use apply ... at after #700 exact absurd H3 (bnot_ne (f bool u)), end diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 8c623d7c8..b2b828314 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -388,7 +388,7 @@ theorem exists_least_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] have Hzbk : z = b + of_nat (nat_abs (z - b)), by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.add_comm, sub_add_cancel], have Hk : nat_abs (z - b) < least (λ n, P (b + of_nat n)) (nat.succ (nat_abs (elt - b))), begin - let Hz' := iff.mp !lt_add_iff_sub_lt_left Hz, + note Hz' := iff.mp !lt_add_iff_sub_lt_left Hz, rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'], apply lt_of_of_nat_lt_of_nat Hz' end, @@ -426,7 +426,7 @@ theorem exists_greatest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] have Hzbk : z = b - of_nat (nat_abs (b - z)), by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), sub_sub_self], have Hk : nat_abs (b - z) < least (λ n, P (b - of_nat n)) (nat.succ (nat_abs (b - elt))), begin - let Hz' := iff.mp !lt_add_iff_sub_lt_left (iff.mpr !lt_add_iff_sub_lt_right Hz), + note Hz' := iff.mp !lt_add_iff_sub_lt_left (iff.mpr !lt_add_iff_sub_lt_right Hz), rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'], apply lt_of_of_nat_lt_of_nat Hz' end, diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index 2d6464b59..ccf24a353 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -36,8 +36,8 @@ private theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : (H : n ≥ pceil (q / ε)) : q * n⁻¹ ≤ ε := begin - let H2 := pceil_helper H (div_pos_of_pos_of_pos Hq Hε), - let H3 := mul_le_of_le_div (div_pos_of_pos_of_pos Hq Hε) H2, + note H2 := pceil_helper H (div_pos_of_pos_of_pos Hq Hε), + note H3 := mul_le_of_le_div (div_pos_of_pos_of_pos Hq Hε) H2, rewrite -(one_mul ε), apply mul_le_mul_of_mul_div_le, repeat assumption @@ -138,7 +138,7 @@ private theorem factor_lemma (a b c d e : ℚ) : abs (a + b + c - (d + (b + e))) private theorem factor_lemma_2 (a b c d : ℚ) : (a + b) + (c + d) = (a + c) + (d + b) := begin - let H := (binary.comm4 add.comm add.assoc a b c d), + note H := (binary.comm4 add.comm add.assoc a b c d), rewrite [add.comm b d at H], exact H end @@ -773,7 +773,7 @@ theorem equiv_of_diff_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t) ... = b + d + a + e + c : add.comm, apply eq_of_bdd Hs Ht, intros, - let He := bdd_of_eq H, + note He := bdd_of_eq H, existsi 2 * (2 * (2 * j)), intros n Hn, rewrite (rewrite_helper5 _ _ (s (2 * n)) (t (2 * n))), @@ -908,7 +908,7 @@ theorem zero_nequiv_one : ¬ zero ≡ one := begin intro Hz, rewrite [↑equiv at Hz, ↑zero at Hz, ↑one at Hz], - let H := Hz (2 * 2), + note H := Hz (2 * 2), rewrite [zero_sub at H, abs_neg at H, pnat.add_halves at H], have H' : pone⁻¹ ≤ 2⁻¹, from calc pone⁻¹ = 1 : by rewrite -pone_inv diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index 41759108e..0ed89c328 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -472,7 +472,7 @@ theorem le_ceil (x : ℝ) : x ≤ ceil x := theorem lt_of_lt_ceil {x : ℝ} {z : ℤ} (Hz : z < ceil x) : z < x := begin rewrite ↑ceil at Hz, - let Hz' := lt_of_floor_lt (iff.mp !lt_neg_iff_lt_neg Hz), + note Hz' := lt_of_floor_lt (iff.mp !lt_neg_iff_lt_neg Hz), rewrite [of_int_neg at Hz'], apply lt_of_neg_lt_neg Hz' end @@ -482,10 +482,10 @@ theorem floor_succ (x : ℝ) : floor (x + 1) = floor x + 1 := apply by_contradiction, intro H, cases lt_or_gt_of_ne H with [Hgt, Hlt], - let Hl := lt_of_floor_lt Hgt, + note Hl := lt_of_floor_lt Hgt, rewrite [of_int_add at Hl], apply not_le_of_gt (lt_of_add_lt_add_right Hl) !floor_le, - let Hl := lt_of_floor_lt (iff.mp !add_lt_iff_lt_sub_right Hlt), + note Hl := lt_of_floor_lt (iff.mp !add_lt_iff_lt_sub_right Hlt), rewrite [of_int_sub at Hl], apply not_le_of_gt (iff.mpr !add_lt_iff_lt_sub_right Hl) !floor_le end @@ -844,7 +844,7 @@ private theorem regular_lemma (s : seq) (H : ∀ n i : ℕ+, i ≥ n → under_s intros, cases em (m ≤ n) with [Hm, Hn], apply regular_lemma_helper Hm H, - let T := regular_lemma_helper (pnat.le_of_lt (pnat.lt_of_not_le Hn)) H, + note T := regular_lemma_helper (pnat.le_of_lt (pnat.lt_of_not_le Hn)) H, rewrite [abs_sub at T, {n⁻¹ + _}add.comm at T], exact T end diff --git a/library/data/real/division.lean b/library/data/real/division.lean index 422421ebd..f1379c261 100644 --- a/library/data/real/division.lean +++ b/library/data/real/division.lean @@ -404,7 +404,7 @@ theorem inv_well_defined {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s s_inv Hs ≡ s_inv Ht := if Hsep : sep s zero then (begin - let Hsept := sep_of_equiv_sep Hs Ht Heq Hsep, + note Hsept := sep_of_equiv_sep Hs Ht Heq Hsep, have Hm : smul t (s_inv Hs) ≡ smul s (s_inv Hs), begin apply mul_well_defined, repeat (assumption | apply reg_inv_reg), @@ -462,15 +462,15 @@ theorem s_le_total {s t : seq} (Hs : regular s) (Ht : regular t) : s_le s t ∨ intro m, apply by_contradiction, intro Hm, - let Hm' := lt_of_not_ge Hm, - let Hex'' := exists.intro m Hm', + note Hm' := lt_of_not_ge Hm, + note Hex'' := exists.intro m Hm', apply Hex Hex'' end, apply H Hex' end, eapply exists.elim H', intro m Hm, - let Hm' := neg_lt_neg Hm, + note Hm' := neg_lt_neg Hm, rewrite neg_neg at Hm', apply s_nonneg_of_pos, rotate 1, diff --git a/library/data/real/order.lean b/library/data/real/order.lean index ba4217343..57e6976d2 100644 --- a/library/data/real/order.lean +++ b/library/data/real/order.lean @@ -236,7 +236,7 @@ theorem s_neg_add_eq_s_add_neg (s t : seq) : sneg (sadd s t) ≡ sadd (sneg s) ( theorem equiv_cancel_middle {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) : sadd (sadd u t) (sneg (sadd u s)) ≡ sadd t (sneg s) := begin - let Hz := zero_is_reg, + note Hz := zero_is_reg, apply equiv.trans, rotate 3, apply add_well_defined, @@ -308,7 +308,7 @@ protected theorem le_trans {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : (Lst : s_le s t) (Ltu : s_le t u) : s_le s u := begin rewrite ↑s_le at *, - let Rz := zero_is_reg, + note Rz := zero_is_reg, have Hsum : nonneg (sadd (sadd u (sneg t)) (sadd t (sneg s))), from rat_seq.add_nonneg_of_nonneg Ltu Lst, have H' : nonneg (sadd (sadd u (sadd (sneg t) t)) (sneg s)), begin @@ -384,7 +384,7 @@ theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_ cases Lst with [N, HN], let Rns := reg_neg_reg Hs, let Rtns := reg_add_reg Ht Rns, - let Habs := sub_le_of_abs_sub_le_right (Rtns N n), + note Habs := sub_le_of_abs_sub_le_right (Rtns N n), rewrite [sub_add_eq_sub_sub at Habs], exact (calc sadd t (sneg s) n ≥ sadd t (sneg s) N - N⁻¹ - n⁻¹ : Habs @@ -401,14 +401,14 @@ theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_ theorem lt_of_le_and_sep {s t : seq} (Hs : regular s) (Ht : regular t) (H : s_le s t ∧ sep s t) : s_lt s t := begin - let Le := and.left H, + note Le := and.left H, cases and.right H with [P, Hlt], exact P, rewrite [↑s_le at Le, ↑nonneg at Le, ↑s_lt at Hlt, ↑pos at Hlt], apply exists.elim Hlt, intro N HN, let LeN := Le N, - let HN' := (iff.mpr !neg_lt_neg_iff_lt) HN, + note HN' := (iff.mpr !neg_lt_neg_iff_lt) HN, rewrite [↑sadd at HN', ↑sneg at HN', neg_add at HN', neg_neg at HN', add.comm at HN'], let HN'' := not_le_of_gt HN', apply absurd LeN HN'' @@ -652,8 +652,8 @@ theorem s_mul_nonneg_of_nonneg {s t : seq} (Hs : regular s) (Ht : regular t) theorem s_mul_ge_zero_of_ge_zero {s t : seq} (Hs : regular s) (Ht : regular t) (Hzs : s_le zero s) (Hzt : s_le zero t) : s_le zero (smul s t) := begin - let Hzs' := s_nonneg_of_ge_zero Hs Hzs, - let Htz' := s_nonneg_of_ge_zero Ht Hzt, + note Hzs' := s_nonneg_of_ge_zero Hs Hzs, + note Htz' := s_nonneg_of_ge_zero Ht Hzt, apply s_ge_zero_of_nonneg, rotate 1, apply s_mul_nonneg_of_nonneg, diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 20dc701e6..2a95fac65 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -130,7 +130,7 @@ definition change (e : expr) : tactic := builtin definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin -definition lettac (id : identifier) (e : expr) : tactic := builtin +definition notetac (id : identifier) (e : expr) : tactic := builtin definition constructor (k : option num) : tactic := builtin definition fconstructor (k : option num) : tactic := builtin diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index 6697c7c19..1eee0bd4e 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -544,7 +544,7 @@ theorem pos_on_nbhd_of_cts_of_pos {f : ℝ → ℝ} (Hf : continuous f) {b : ℝ exact and.left Hδ, intro y Hy, let Hy' := and.right Hδ y Hy, - let Hlt := sub_lt_of_abs_sub_lt_right Hy', + note Hlt := sub_lt_of_abs_sub_lt_right Hy', rewrite sub_self at Hlt, assumption end @@ -560,7 +560,7 @@ theorem neg_on_nbhd_of_cts_of_neg {f : ℝ → ℝ} (Hf : continuous f) {b : ℝ intro y Hy, let Hy' := and.right Hδ y Hy, let Hlt := sub_lt_of_abs_sub_lt_left Hy', - let Hlt' := lt_add_of_sub_lt_right Hlt, + note Hlt' := lt_add_of_sub_lt_right Hlt, rewrite [-sub_eq_add_neg at Hlt', sub_self at Hlt'], assumption end @@ -780,7 +780,7 @@ theorem intermediate_value_incr_zero : ∃ c, a < c ∧ c < b ∧ f c = 0 := intro Hxgt, have Hxgt' : b - x < δ, from sub_lt_of_sub_lt Hxgt, krewrite -(abs_of_pos (sub_pos_of_lt (and.left Hx))) at Hxgt', - let Hxgt'' := and.right Hδ _ Hxgt', + note Hxgt'' := and.right Hδ _ Hxgt', exact not_lt_of_ge (le_of_lt Hxgt'') (and.right Hx)}, {exact sup_fn_interval} end diff --git a/library/theories/number_theory/bezout.lean b/library/theories/number_theory/bezout.lean index 97f797406..e7a6b2463 100644 --- a/library/theories/number_theory/bezout.lean +++ b/library/theories/number_theory/bezout.lean @@ -57,7 +57,7 @@ gcd.induction x y assume npos : 0 < n, assume IH, begin - let H := egcd_of_pos m npos, esimp at H, + note H := egcd_of_pos m npos, esimp at H, rewrite H, esimp, rewrite [gcd_rec, -IH], diff --git a/library/theories/number_theory/irrational_roots.lean b/library/theories/number_theory/irrational_roots.lean index 96082ba13..f2f4d3b7c 100644 --- a/library/theories/number_theory/irrational_roots.lean +++ b/library/theories/number_theory/irrational_roots.lean @@ -156,7 +156,7 @@ section have pnez : p ≠ 0, from (suppose p = 0, show false, - by let H := (pos_of_prime primep); rewrite this at H; exfalso; exact !lt.irrefl H), + by note H := (pos_of_prime primep); rewrite this at H; exfalso; exact !lt.irrefl H), assert agtz : a > 0, from pos_of_ne_zero (suppose a = 0, show false, using npos pnez, by revert peq; rewrite [this, zero_pow npos]; exact pnez), diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index b248a63d3..192c0ba27 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -72,7 +72,7 @@ "xrewrite" "krewrite" "blast" "simp" "esimp" "unfold" "change" "check_expr" "contradiction" "exfalso" "split" "existsi" "constructor" "fconstructor" "left" "right" "injection" "congruence" "reflexivity" "symmetry" "transitivity" "state" "induction" "induction_using" "fail" "append" - "substvars" "now" "with_options" "with_attributes" "with_attrs") + "substvars" "now" "with_options" "with_attributes" "with_attrs" "note") "lean tactics") (defconst lean-tactics-regexp (eval `(rx word-start (or ,@lean-tactics) word-end))) diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp index 2635f005a..34f76e218 100644 --- a/src/frontends/lean/builtin_tactics.cpp +++ b/src/frontends/lean/builtin_tactics.cpp @@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "library/tactic/let_tactic.h" +#include +#include +#include "library/tactic/note_tactic.h" #include "library/tactic/generalize_tactic.h" #include "frontends/lean/tokens.h" #include "frontends/lean/parser.h" @@ -43,10 +45,22 @@ static expr parse_rparen(parser &, unsigned, expr const * args, pos_info const & } static expr parse_let_tactic(parser & p, unsigned, expr const *, pos_info const & pos) { + auto id_pos = p.pos(); name id = p.check_atomic_id_next("invalid 'let' tactic, identifier expected"); p.check_token_next(get_assign_tk(), "invalid 'let' tactic, ':=' expected"); expr value = p.parse_tactic_expr_arg(); - return p.save_pos(mk_let_tactic_expr(id, value), pos); + // Register value as expandable local expr. Identical to let term parsing, but without surrounding mk_let. + value = p.save_pos(mk_let_value(value), id_pos); + p.add_local_expr(id, value); + // nothing to do, so return the id tactic + return p.save_pos(mk_constant(get_tactic_id_name()), pos); +} + +static expr parse_note_tactic(parser & p, unsigned, expr const *, pos_info const & pos) { + name id = p.check_atomic_id_next("invalid 'note' tactic, identifier expected"); + p.check_token_next(get_assign_tk(), "invalid 'note' tactic, ':=' expected"); + expr value = p.parse_tactic_expr_arg(); + return p.save_pos(mk_note_tactic_expr(id, value), pos); } static expr parse_with_options_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) { @@ -87,6 +101,7 @@ parse_table init_tactic_nud_table() { r = r.add({transition("unfold", mk_ext_action(parse_unfold_tactic_expr))}, x0); r = r.add({transition("fold", mk_ext_action(parse_fold_tactic_expr))}, x0); r = r.add({transition("let", mk_ext_action(parse_let_tactic))}, x0); + r = r.add({transition("note", mk_ext_action(parse_note_tactic))}, x0); r = r.add({transition("with_options", mk_ext_action(parse_with_options_tactic_expr))}, x0); r = r.add({transition("with_attributes", mk_ext_action(parse_with_attributes_tactic_expr))}, x0); r = r.add({transition("with_attrs", mk_ext_action(parse_with_attributes_tactic_expr))}, x0); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index a7517c664..da1ab555c 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -96,7 +96,7 @@ void init_token_table(token_table & t) { {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0}, {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"xrewrite", 0}, {"krewrite", 0}, - {"esimp", 0}, {"fold", 0}, {"unfold", 0}, {"with_options", 0}, {"with_attributes", 0}, {"with_attrs", 0}, + {"esimp", 0}, {"fold", 0}, {"unfold", 0}, {"note", 0}, {"with_options", 0}, {"with_attributes", 0}, {"with_attrs", 0}, {"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"#tactic", 0}, {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"begin+", g_max_prec}, {"abstract", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@@", g_max_prec}, {"@", g_max_prec}, diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 8fa7f2573..be8f19b87 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -229,8 +229,8 @@ name const * g_tactic_identifier_list = nullptr; name const * g_tactic_interleave = nullptr; name const * g_tactic_intro = nullptr; name const * g_tactic_intros = nullptr; -name const * g_tactic_lettac = nullptr; name const * g_tactic_none_expr = nullptr; +name const * g_tactic_notetac = nullptr; name const * g_tactic_now = nullptr; name const * g_tactic_opt_expr = nullptr; name const * g_tactic_opt_expr_list = nullptr; @@ -487,8 +487,8 @@ void initialize_constants() { g_tactic_interleave = new name{"tactic", "interleave"}; g_tactic_intro = new name{"tactic", "intro"}; g_tactic_intros = new name{"tactic", "intros"}; - g_tactic_lettac = new name{"tactic", "lettac"}; g_tactic_none_expr = new name{"tactic", "none_expr"}; + g_tactic_notetac = new name{"tactic", "notetac"}; g_tactic_now = new name{"tactic", "now"}; g_tactic_opt_expr = new name{"tactic", "opt_expr"}; g_tactic_opt_expr_list = new name{"tactic", "opt_expr_list"}; @@ -746,8 +746,8 @@ void finalize_constants() { delete g_tactic_interleave; delete g_tactic_intro; delete g_tactic_intros; - delete g_tactic_lettac; delete g_tactic_none_expr; + delete g_tactic_notetac; delete g_tactic_now; delete g_tactic_opt_expr; delete g_tactic_opt_expr_list; @@ -1004,8 +1004,8 @@ name const & get_tactic_identifier_list_name() { return *g_tactic_identifier_lis name const & get_tactic_interleave_name() { return *g_tactic_interleave; } name const & get_tactic_intro_name() { return *g_tactic_intro; } name const & get_tactic_intros_name() { return *g_tactic_intros; } -name const & get_tactic_lettac_name() { return *g_tactic_lettac; } name const & get_tactic_none_expr_name() { return *g_tactic_none_expr; } +name const & get_tactic_notetac_name() { return *g_tactic_notetac; } name const & get_tactic_now_name() { return *g_tactic_now; } name const & get_tactic_opt_expr_name() { return *g_tactic_opt_expr; } name const & get_tactic_opt_expr_list_name() { return *g_tactic_opt_expr_list; } diff --git a/src/library/constants.h b/src/library/constants.h index 26ba43162..4f69fe174 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -231,8 +231,8 @@ name const & get_tactic_identifier_list_name(); name const & get_tactic_interleave_name(); name const & get_tactic_intro_name(); name const & get_tactic_intros_name(); -name const & get_tactic_lettac_name(); name const & get_tactic_none_expr_name(); +name const & get_tactic_notetac_name(); name const & get_tactic_now_name(); name const & get_tactic_opt_expr_name(); name const & get_tactic_opt_expr_list_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 90621cf04..5097a8e52 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -224,8 +224,8 @@ tactic.identifier_list tactic.interleave tactic.intro tactic.intros -tactic.lettac tactic.none_expr +tactic.notetac tactic.now tactic.opt_expr tactic.opt_expr_list diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 4f1d9d62e..b798a07f2 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -3,7 +3,7 @@ apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp exact_tactic.cpp generalize_tactic.cpp inversion_tactic.cpp whnf_tactic.cpp revert_tactic.cpp assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp location.cpp rewrite_tactic.cpp util.cpp -init_module.cpp change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp +init_module.cpp change_tactic.cpp check_expr_tactic.cpp note_tactic.cpp contradiction_tactic.cpp exfalso_tactic.cpp constructor_tactic.cpp injection_tactic.cpp congruence_tactic.cpp relation_tactics.cpp induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp with_options_tactic.cpp diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 1ad835195..de29720a7 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -21,7 +21,7 @@ Author: Leonardo de Moura #include "library/tactic/rewrite_tactic.h" #include "library/tactic/change_tactic.h" #include "library/tactic/check_expr_tactic.h" -#include "library/tactic/let_tactic.h" +#include "library/tactic/note_tactic.h" #include "library/tactic/contradiction_tactic.h" #include "library/tactic/exfalso_tactic.h" #include "library/tactic/constructor_tactic.h" @@ -52,7 +52,7 @@ void initialize_tactic_module() { initialize_rewrite_tactic(); initialize_change_tactic(); initialize_check_expr_tactic(); - initialize_let_tactic(); + initialize_note_tactic(); initialize_contradiction_tactic(); initialize_exfalso_tactic(); initialize_constructor_tactic(); @@ -78,7 +78,7 @@ void finalize_tactic_module() { finalize_constructor_tactic(); finalize_exfalso_tactic(); finalize_contradiction_tactic(); - finalize_let_tactic(); + finalize_note_tactic(); finalize_check_expr_tactic(); finalize_change_tactic(); finalize_rewrite_tactic(); diff --git a/src/library/tactic/let_tactic.cpp b/src/library/tactic/note_tactic.cpp similarity index 75% rename from src/library/tactic/let_tactic.cpp rename to src/library/tactic/note_tactic.cpp index 53d142125..1bee54090 100644 --- a/src/library/tactic/let_tactic.cpp +++ b/src/library/tactic/note_tactic.cpp @@ -13,12 +13,12 @@ Author: Leonardo de Moura #include "library/tactic/expr_to_tactic.h" namespace lean { -expr mk_let_tactic_expr(name const & id, expr const & e) { - return mk_app(mk_constant(get_tactic_lettac_name()), +expr mk_note_tactic_expr(name const &id, expr const &e) { + return mk_app(mk_constant(get_tactic_notetac_name()), mk_constant(id), e); } -tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) { +tactic note_tactic(elaborate_fn const & elab, name const & id, expr const & e) { return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) { proof_state new_s = s; goals const & gs = new_s.get_goals(); @@ -33,7 +33,7 @@ tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) { expr new_e; substitution new_subst; constraints cs; std::tie(new_e, new_subst, cs) = esc; if (cs) - throw_tactic_exception_if_enabled(s, "invalid 'let' tactic, fail to resolve generated constraints"); + throw_tactic_exception_if_enabled(s, "invalid 'note' tactic, fail to resolve generated constraints"); auto tc = mk_type_checker(env, ngen.mk_child()); expr new_e_type = tc->infer(new_e).first; expr new_local = mk_local(ngen.next(), id, new_e_type, binder_info()); @@ -50,14 +50,14 @@ tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) { }); } -void initialize_let_tactic() { - register_tac(get_tactic_lettac_name(), +void initialize_note_tactic() { + register_tac(get_tactic_notetac_name(), [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'let' tactic, argument must be an identifier"); - check_tactic_expr(app_arg(e), "invalid 'let' tactic, argument must be an expression"); - return let_tactic(fn, id, get_tactic_expr_expr(app_arg(e))); + name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'note' tactic, argument must be an identifier"); + check_tactic_expr(app_arg(e), "invalid 'note' tactic, argument must be an expression"); + return note_tactic(fn, id, get_tactic_expr_expr(app_arg(e))); }); } -void finalize_let_tactic() { +void finalize_note_tactic() { } } diff --git a/src/library/tactic/let_tactic.h b/src/library/tactic/note_tactic.h similarity index 65% rename from src/library/tactic/let_tactic.h rename to src/library/tactic/note_tactic.h index 98d14c8c1..2bc8237fa 100644 --- a/src/library/tactic/let_tactic.h +++ b/src/library/tactic/note_tactic.h @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "kernel/expr.h" namespace lean { -expr mk_let_tactic_expr(name const & id, expr const & e); -void initialize_let_tactic(); -void finalize_let_tactic(); +expr mk_note_tactic_expr(name const &id, expr const &e); +void initialize_note_tactic(); +void finalize_note_tactic(); } diff --git a/tests/lean/hott/670.hlean b/tests/lean/hott/670.hlean index 39d076910..6cf6c6284 100644 --- a/tests/lean/hott/670.hlean +++ b/tests/lean/hott/670.hlean @@ -16,7 +16,7 @@ by krewrite [to_right_inv e b] example (b : B) : g (f (g b)) = g b := begin - let H := to_right_inv e b, + note H := to_right_inv e b, esimp at H, rewrite H end diff --git a/tests/lean/interactive/alias.input.expected.out b/tests/lean/interactive/alias.input.expected.out index 4047393b2..b7ab8cbea 100644 --- a/tests/lean/interactive/alias.input.expected.out +++ b/tests/lean/interactive/alias.input.expected.out @@ -8,7 +8,6 @@ bool.band_tt|∀ (a : bool), eq (bool.band a bool.tt) a bool.tt|bool bool.eq_tt_of_bnot_eq_ff|eq (bool.bnot ?a) bool.ff → eq ?a bool.tt bool.eq_ff_of_bnot_eq_tt|eq (bool.bnot ?a) bool.tt → eq ?a bool.ff -tactic.lettac|tactic.identifier → tactic.expr → tactic bool.absurd_of_eq_ff_of_eq_tt|eq ?a bool.ff → eq ?a bool.tt → ?B bool.eq_tt_of_ne_ff|ne ?a bool.ff → eq ?a bool.tt tactic.with_attributes_tac|tactic.expr → tactic.identifier_list → tactic → tactic @@ -28,7 +27,6 @@ bor_tt|∀ (a : bool), eq (bor a tt) tt band_tt|∀ (a : bool), eq (band a tt) a eq_tt_of_bnot_eq_ff|eq (bnot ?a) ff → eq ?a tt eq_ff_of_bnot_eq_tt|eq (bnot ?a) tt → eq ?a ff -tactic.lettac|tactic.identifier → tactic.expr → tactic absurd_of_eq_ff_of_eq_tt|eq ?a ff → eq ?a tt → ?B eq_tt_of_ne_ff|ne ?a ff → eq ?a tt tactic.with_attributes_tac|tactic.expr → tactic.identifier_list → tactic → tactic diff --git a/tests/lean/run/blast_cc8.lean b/tests/lean/run/blast_cc8.lean index b9afafe9b..ee05abde1 100644 --- a/tests/lean/run/blast_cc8.lean +++ b/tests/lean/run/blast_cc8.lean @@ -11,7 +11,7 @@ begin induction a with f₁ h₁, induction b with f₂ h₂, subst xs, - let e := to_set.inj h₂, + note e := to_set.inj h₂, subst e end diff --git a/tests/lean/run/congr_tac2.lean b/tests/lean/run/congr_tac2.lean index c4f2f107b..b0108cdaa 100644 --- a/tests/lean/run/congr_tac2.lean +++ b/tests/lean/run/congr_tac2.lean @@ -17,7 +17,7 @@ begin induction a with f₁ h₁, induction b with f₂ h₂, subst xs, - let e := to_set.inj h₂, + note e := to_set.inj h₂, subst e end diff --git a/tests/lean/run/dep_subst.lean b/tests/lean/run/dep_subst.lean index bbba1bff4..fccd1e928 100644 --- a/tests/lean/run/dep_subst.lean +++ b/tests/lean/run/dep_subst.lean @@ -23,6 +23,6 @@ begin induction fn₁ with fxs₁ h₁, induction fn₂ with fxs₂ h₂, subst xs, - let aux := to_set.inj h₂, + note aux := to_set.inj h₂, subst aux end diff --git a/tests/lean/run/let_tac.lean b/tests/lean/run/let_tac.lean index c64acc5ca..f92a4e43f 100644 --- a/tests/lean/run/let_tac.lean +++ b/tests/lean/run/let_tac.lean @@ -4,6 +4,8 @@ open algebra example (a b : Prop) : a → b → a ∧ b := begin intro Ha, intro Hb, + let Ha' := Ha, + let Hb' := Hb, let aux := and.intro Ha Hb, exact aux end