From 101cf1ec4c8d933441dc9239019950a79b53e97a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Feb 2016 11:28:20 -0800 Subject: [PATCH] feat(frontends/lean): remove difference between 'have' and 'assert' --- hott/algebra/ring.hlean | 4 +-- library/algebra/ring.lean | 4 +-- library/data/examples/vector.lean | 6 ++--- library/data/list/perm.lean | 2 +- library/data/nat/bigops.lean | 4 +-- library/data/set/basic.lean | 4 +-- library/data/set/filter.lean | 3 +-- library/theories/analysis/metric_space.lean | 4 +-- library/theories/analysis/normed_space.lean | 4 +-- library/theories/analysis/real_limit.lean | 7 +++--- .../measure_theory/sigma_algebra.lean | 6 ++--- .../number_theory/irrational_roots.lean | 25 +++++++++---------- library/theories/topology/basic.lean | 4 +-- src/frontends/lean/builtin_exprs.cpp | 8 ++---- src/frontends/lean/pp.cpp | 5 +--- tests/lean/congr_print.lean.expected.out | 9 +++---- tests/lean/extra/bag.661.20.expected.out | 1 + .../finset_induction_bug.lean.expected.out | 8 +++--- tests/lean/have1.lean | 4 +-- tests/lean/have1.lean.expected.out | 4 +-- tests/lean/run/830.lean | 2 +- tests/lean/run/have1.lean | 2 +- tests/lean/run/using_bug.lean | 2 +- tests/lean/run/using_bug2.lean | 5 ++-- tests/lean/show1.lean.expected.out | 4 +-- 25 files changed, 61 insertions(+), 70 deletions(-) diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean index af8a823e4..dd05f1eab 100644 --- a/hott/algebra/ring.hlean +++ b/hott/algebra/ring.hlean @@ -345,13 +345,13 @@ section theorem eq_of_mul_eq_mul_right {a b c : A} (Ha : a ≠ 0) (H : b * a = c * a) : b = c := have b * a - c * a = 0, from iff.mp !eq_iff_sub_eq_zero H, - have (b - c) * a = 0, using this, by rewrite [mul_sub_right_distrib, this], + have (b - c) * a = 0, by rewrite [mul_sub_right_distrib, this], have b - c = 0, from sum_resolve_left (eq_zero_sum_eq_zero_of_mul_eq_zero this) Ha, iff.elim_right !eq_iff_sub_eq_zero this theorem eq_of_mul_eq_mul_left {a b c : A} (Ha : a ≠ 0) (H : a * b = a * c) : b = c := have a * b - a * c = 0, from iff.mp !eq_iff_sub_eq_zero H, - have a * (b - c) = 0, using this, by rewrite [mul_sub_left_distrib, this], + have a * (b - c) = 0, by rewrite [mul_sub_left_distrib, this], have b - c = 0, from sum_resolve_right (eq_zero_sum_eq_zero_of_mul_eq_zero this) Ha, iff.elim_right !eq_iff_sub_eq_zero this diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 56089450f..e37433a94 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -347,13 +347,13 @@ section theorem eq_of_mul_eq_mul_right {a b c : A} (Ha : a ≠ 0) (H : b * a = c * a) : b = c := have b * a - c * a = 0, from iff.mp !eq_iff_sub_eq_zero H, - have (b - c) * a = 0, using this, by rewrite [mul_sub_right_distrib, this], + have (b - c) * a = 0, by rewrite [mul_sub_right_distrib, this], have b - c = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero this) Ha, iff.elim_right !eq_iff_sub_eq_zero this theorem eq_of_mul_eq_mul_left {a b c : A} (Ha : a ≠ 0) (H : a * b = a * c) : b = c := have a * b - a * c = 0, from iff.mp !eq_iff_sub_eq_zero H, - have a * (b - c) = 0, using this, by rewrite [mul_sub_left_distrib, this], + have a * (b - c) = 0, by rewrite [mul_sub_left_distrib, this], have b - c = 0, from or_resolve_right (eq_zero_or_eq_zero_of_mul_eq_zero this) Ha, iff.elim_right !eq_iff_sub_eq_zero this diff --git a/library/data/examples/vector.lean b/library/data/examples/vector.lean index d3d72b5df..76d824887 100644 --- a/library/data/examples/vector.lean +++ b/library/data/examples/vector.lean @@ -259,9 +259,9 @@ namespace vector | (n+1) (m+1) (x::xs) (y::ys) h₁ h₂ := assert e₁ : n = m, from succ.inj h₂, assert e₂ : x = y, begin unfold to_list at h₁, injection h₁, assumption end, - have to_list xs = to_list ys, begin unfold to_list at h₁, injection h₁, assumption end, - assert xs == ys, from heq_of_list_eq this e₁, - assert y :: xs == y :: ys, begin clear heq_of_list_eq h₁ h₂, revert xs ys this, induction e₁, intro xs ys h, rewrite [eq_of_heq h] end, + have e₃ : to_list xs = to_list ys, begin unfold to_list at h₁, injection h₁, assumption end, + assert xs == ys, from heq_of_list_eq e₃ e₁, + assert y :: xs == y :: ys, begin clear heq_of_list_eq h₁ h₂ e₃, revert xs ys this, induction e₁, intro xs ys h, rewrite [eq_of_heq h] end, show x :: xs == y :: ys, by rewrite e₂; exact this theorem list_eq_of_heq {n m} {v₁ : vector A n} {v₂ : vector A m} : v₁ == v₂ → n = m → to_list v₁ = to_list v₂ := diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index fdc7b9051..a963a4824 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -753,7 +753,7 @@ assume h, perm.induction_on h have nodup l₁, from nodup_of_nodup_cons this, have x ∉ l₁, from not_mem_of_nodup_cons `nodup (x::l₁)`, have y ∉ x::l₁, from not_mem_of_nodup_cons nd, - have x ≠ y, using this, from suppose x = y, begin subst x, exact absurd !mem_cons `y ∉ y::l₁` end, + have x ≠ y, from suppose x = y, begin subst x, exact absurd !mem_cons `y ∉ y::l₁` end, have y ∉ l₁, from not_mem_of_not_mem_cons `y ∉ x::l₁`, have x ∉ y::l₁, from not_mem_cons_of_ne_of_not_mem `x ≠ y` `x ∉ l₁`, have nodup (y::l₁), from nodup_cons `y ∉ l₁` `nodup l₁`, diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean index 940c39927..1f8b403e2 100644 --- a/library/data/nat/bigops.lean +++ b/library/data/nat/bigops.lean @@ -61,7 +61,7 @@ begin suppose x ∈ upto n, have x < n, from lt_of_mem_upto this, suppose x ∈ '{n}, - have x = n, using this, by rewrite -mem_singleton_iff; apply this, + have x = n, by rewrite -mem_singleton_iff; apply this, have n < n, from eq.subst this `x < n`, show false, from !lt.irrefl this), rewrite [sum_up_to_succ, ih, upto_succ, Sum_union _ H, Sum_singleton] @@ -152,7 +152,7 @@ begin suppose x ∈ upto n, have x < n, from lt_of_mem_upto this, suppose x ∈ '{n}, - have x = n, using this, by rewrite -mem_singleton_iff; apply this, + have x = n, by rewrite -mem_singleton_iff; apply this, have n < n, from eq.subst this `x < n`, show false, from !lt.irrefl this), rewrite [prod_up_to_succ, ih, upto_succ, Prod_union _ H, Prod_singleton] diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index d9e1454d4..97308cbab 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -750,7 +750,7 @@ ext (take x, iff.intro (suppose x ∈ sUnion '{s}, obtain u [(Hu : u ∈ '{s}) (xu : x ∈ u)], from this, have u = s, from eq_of_mem_singleton Hu, - show x ∈ s, using this, by rewrite -this; apply xu) + show x ∈ s, by rewrite -this; apply xu) (suppose x ∈ s, mem_sUnion this (mem_singleton s))) @@ -798,7 +798,7 @@ ext (take x, iff.intro take t, suppose t ∈ compl ' S, obtain t' [(Ht' : t' ∈ S) (Ht : -t' = t)], from this, have x ∈ -t', from suppose x ∈ t', H (mem_sUnion this Ht'), - show x ∈ t, using this, by rewrite -Ht; apply this) + show x ∈ t, by rewrite -Ht; apply this) (assume H : x ∈ ⋂₀ (compl ' S), suppose x ∈ ⋃₀ S, obtain t [(tS : t ∈ S) (xt : x ∈ t)], from this, diff --git a/library/data/set/filter.lean b/library/data/set/filter.lean index e96c826f5..87ad7139e 100644 --- a/library/data/set/filter.lean +++ b/library/data/set/filter.lean @@ -135,8 +135,7 @@ section assume H' : eventually (λx, ¬ (P x ∨ Q x)) F, have (λx, ¬ (P x ∨ Q x)) = λ x, ¬ P x ∧ ¬ Q x, by apply funext; intro x; rewrite not_or_iff_not_and_not, - show false, using this, - by rewrite this at H'; exact H (eventually_of_eventually_and_left H') + show false, by rewrite this at H'; exact H (eventually_of_eventually_and_left H') theorem frequently_inr (H : frequently Q F) : frequently (λx, P x ∨ Q x) F := begin diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean index 3b5be5b4c..fd3f01242 100644 --- a/library/theories/analysis/metric_space.lean +++ b/library/theories/analysis/metric_space.lean @@ -37,7 +37,7 @@ metric_space.dist_triangle x y z proposition dist_nonneg (x y : M) : 0 ≤ dist x y := have dist x y + dist y x ≥ 0, by rewrite -(dist_self x); apply dist_triangle, -have 2 * dist x y ≥ 0, using this, +have 2 * dist x y ≥ 0, by krewrite [-real.one_add_one, right_distrib, +one_mul, dist_comm at {2}]; apply this, nonneg_of_mul_nonneg_left this two_pos @@ -135,7 +135,7 @@ exists.intro (N + k) (take n : ℕ, assume nge : n ≥ N + k, have n - k ≥ N, from nat.le_sub_of_add_le nge, have dist (X (n - k + k)) y < ε, from HN (n - k) this, - show dist (X n) y < ε, using this, + show dist (X n) y < ε, by rewrite [(nat.sub_add_cancel (le.trans !le_add_left nge)) at this]; exact this) proposition converges_to_seq_of_converges_to_seq_offset_left diff --git a/library/theories/analysis/normed_space.lean b/library/theories/analysis/normed_space.lean index 2d94782bc..5a901929e 100644 --- a/library/theories/analysis/normed_space.lean +++ b/library/theories/analysis/normed_space.lean @@ -214,7 +214,7 @@ obtain N (HN : ∀ n, n ≥ N → norm (X n - 0) < ε), from HX `ε > 0`, exists.intro N (take n, assume Hn : n ≥ N, have norm (X n) < ε, begin rewrite -(sub_zero (X n)), apply HN n Hn end, - show abs (norm (X n) - 0) < ε, using this, + show abs (norm (X n) - 0) < ε, by rewrite [sub_zero, abs_of_nonneg !norm_nonneg]; apply this) proposition converges_to_seq_zero_of_norm_converges_to_seq_zero @@ -227,7 +227,7 @@ exists.intro (N : ℕ) have HN' : abs (norm (X n) - 0) < ε, from HN n Hn, have norm (X n) < ε, by+ rewrite [sub_zero at HN', abs_of_nonneg !norm_nonneg at HN']; apply HN', - show norm (X n - 0) < ε, using this, + show norm (X n - 0) < ε, by rewrite sub_zero; apply this) proposition norm_converges_to_seq_zero_iff (X : ℕ → V) : diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index 792795f32..b839100f0 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -140,7 +140,7 @@ have Hb' : ∀ x, x ∈ negX → -b ≤ x, have HX : X = {x | -x ∈ negX}, from set.ext (take x, by rewrite [↑set_of, ↑mem, +neg_neg]), show inf {x | -x ∈ X} = - sup X, - using HX Hb' nonempty_negX, by rewrite [HX at {2}, sup_neg nonempty_negX Hb', neg_neg] + by rewrite [HX at {2}, sup_neg nonempty_negX Hb', neg_neg] end end real @@ -453,11 +453,11 @@ have Hi' : ∀ j, j ≥ i → sX - ε < X j, from exists.intro i (take j, assume Hj : j ≥ i, have X j - sX ≤ 0, from sub_nonpos_of_le (Xle j), - have eq₁ : abs (X j - sX) = sX - X j, using this, by rewrite [abs_of_nonpos this, neg_sub], + have eq₁ : abs (X j - sX) = sX - X j, by rewrite [abs_of_nonpos this, neg_sub], have sX - ε < X j, from lt_of_lt_of_le (by rewrite Hi; apply H₂x') (nondecX Hj), have sX < X j + ε, from lt_add_of_sub_lt_right this, have sX - X j < ε, from sub_lt_left_of_lt_add this, - show (abs (X j - sX)) < ε, using eq₁ this, by rewrite eq₁; exact this) + show (abs (X j - sX)) < ε, by rewrite eq₁; exact this) definition nonincreasing (X : ℕ → ℝ) : Prop := ∀ ⦃i j⦄, i ≤ j → X i ≥ X j @@ -522,7 +522,6 @@ theorem pow_converges_to_seq_zero {x : ℝ} (H : abs x < 1) : (λ n, x^n) ⟶ 0 in ℕ := suffices H' : (λ n, (abs x)^n) ⟶ 0 in ℕ, from have (λ n, (abs x)^n) = (λ n, abs (x^n)), from funext (take n, eq.symm !abs_pow), - using this, by rewrite this at H'; exact converges_to_seq_zero_of_abs_converges_to_seq_zero H', let aX := (λ n, (abs x)^n), iaX := real.inf (aX ' univ), diff --git a/library/theories/measure_theory/sigma_algebra.lean b/library/theories/measure_theory/sigma_algebra.lean index 340f11443..008effcd5 100644 --- a/library/theories/measure_theory/sigma_algebra.lean +++ b/library/theories/measure_theory/sigma_algebra.lean @@ -43,17 +43,17 @@ theorem measurable_cInter {s : ℕ → set X} (H : ∀ i, measurable (s i)) : measurable (⋂ i, s i) := have ∀ i, measurable (-(s i)), from take i, measurable_compl (H i), have measurable (-(⋃ i, -(s i))), from measurable_compl (measurable_cUnion this), -show measurable (⋂ i, s i), using this, by rewrite Inter_eq_comp_Union_comp; apply this +show measurable (⋂ i, s i), by rewrite Inter_eq_comp_Union_comp; apply this theorem measurable_union {s t : set X} (Hs : measurable s) (Ht : measurable t) : measurable (s ∪ t) := have ∀ i, measurable (bin_ext s t i), by intro i; cases i; exact Hs; exact Ht, -show measurable (s ∪ t), using this, by rewrite -Union_bin_ext; exact measurable_cUnion this +show measurable (s ∪ t), by rewrite -Union_bin_ext; exact measurable_cUnion this theorem measurable_inter {s t : set X} (Hs : measurable s) (Ht : measurable t) : measurable (s ∩ t) := have ∀ i, measurable (bin_ext s t i), by intro i; cases i; exact Hs; exact Ht, -show measurable (s ∩ t), using this, by rewrite -Inter_bin_ext; exact measurable_cInter this +show measurable (s ∩ t), by rewrite -Inter_bin_ext; exact measurable_cInter this theorem measurable_diff {s t : set X} (Hs : measurable s) (Ht : measurable t) : measurable (s \ t) := diff --git a/library/theories/number_theory/irrational_roots.lean b/library/theories/number_theory/irrational_roots.lean index 9b2f97d37..fb06f6e94 100644 --- a/library/theories/number_theory/irrational_roots.lean +++ b/library/theories/number_theory/irrational_roots.lean @@ -100,15 +100,14 @@ section have bnnz : (b : rat)^n ≠ 0, from assume bneqz, bnz (_root_.eq_zero_of_pow_eq_zero bneqz), have a^n /[rat] (b:rat)^n = c, - using bnz, begin rewrite [*of_int_pow, -div_pow, -eq_num_div_denom, -H] end, + begin rewrite [*of_int_pow, -div_pow, -eq_num_div_denom, -H] end, have (a^n : rat) = c * (b:rat)^n, from eq.symm (!mul_eq_of_eq_div bnnz (eq.symm this)), have a^n = c * b^n, -- int version - using this, by rewrite [-of_int_pow at this, -of_int_mul at this]; exact of_int.inj this, + by rewrite [-of_int_pow at this, -of_int_mul at this]; exact of_int.inj this, have (abs a)^n = abs c * (abs b)^n, - using this, by rewrite [-abs_pow, this, abs_mul, abs_pow], + by rewrite [-abs_pow, this, abs_mul, abs_pow], have H₁ : (nat_abs a)^n = nat_abs c * (nat_abs b)^n, - using this, begin apply int.of_nat.inj, rewrite [int.of_nat_mul, +int.of_nat_pow, +of_nat_nat_abs], exact this end, have H₂ : nat.coprime (nat_abs a) (nat_abs b), @@ -118,7 +117,7 @@ section (suppose q = 0, by rewrite this) (suppose qne0 : q ≠ 0, - using H₁ H₂, begin + begin have ane0 : a ≠ 0, from suppose aeq0 : a = 0, have qeq0 : q = 0, @@ -133,13 +132,13 @@ section show nat_abs b = 1, from (root_irrational npos (pos_of_ne_zero this) H₂ H₁) end), show b = 1, - using this, begin rewrite [-of_nat_nat_abs_of_nonneg (le_of_lt !denom_pos), this] end + begin rewrite [-of_nat_nat_abs_of_nonneg (le_of_lt !denom_pos), this] end theorem eq_num_pow_of_pow_eq {q : ℚ} {n : ℕ} {c : ℤ} (npos : n > 0) (H : q^n = c) : c = (num q)^n := have denom q = 1, from denom_eq_one_of_pow_eq npos H, - have of_int c = of_int ((num q)^n), using this, + have of_int c = of_int ((num q)^n), by rewrite [-H, eq_num_div_denom q at {1}, this, of_int_one, div_one, of_int_pow], show c = (num q)^n , from of_int.inj this end @@ -159,7 +158,7 @@ section 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), + show false, by revert peq; rewrite [this, zero_pow npos]; exact pnez), have n * mult p a = 1, from calc n * mult p a = mult p (a^n) : begin rewrite [mult_pow n agtz primep] end ... = mult p p : peq @@ -168,7 +167,7 @@ section from dvd_of_mul_right_eq this, have n = 1, from eq_one_of_dvd_one this, - show false, using this, + show false, by rewrite this at ngt1; exact !lt.irrefl ngt1 open int rat @@ -180,7 +179,7 @@ section have npos : n > 0, from lt.trans dec_trivial ngt1, suppose q^n = p, have p = (num q)^n, from eq_num_pow_of_pow_eq npos this, - have p = (nat_abs (num q))^n, using this numq, + have p = (nat_abs (num q))^n, by apply of_nat.inj; rewrite [this, of_nat_pow, of_nat_nat_abs_of_nonneg numq], show false, from not_eq_pow_of_prime _ ngt1 primep this end @@ -204,15 +203,15 @@ section by rewrite -mul.assoc at H; apply H, have a / (gcd a b) = c * b / gcd (c * b) a, from div_gcd_eq_div_gcd this bpos apos, - have a = c * b / gcd c a, using this, + have a = c * b / gcd c a, by revert this; rewrite [↑coprime at co, co, int.div_one, H₁]; intros; assumption, - have a = b * (c / gcd c a), using this, + have a = b * (c / gcd c a), by revert this; rewrite [mul.comm, !int.mul_div_assoc !gcd_dvd_left]; intros; assumption, have b ∣ a, from dvd_of_mul_right_eq this⁻¹, have b ∣ gcd a b, from dvd_gcd this !dvd.refl, - have b ∣ 1, using this, + have b ∣ 1, by rewrite [↑coprime at co, co at this]; apply this, show b = 1, from eq_one_of_dvd_one (le_of_lt bpos) this diff --git a/library/theories/topology/basic.lean b/library/theories/topology/basic.lean index b543e1880..b94f75a9a 100644 --- a/library/theories/topology/basic.lean +++ b/library/theories/topology/basic.lean @@ -25,7 +25,7 @@ definition Open (s : set X) : Prop := s ∈ opens X theorem Open_empty : Open (∅ : set X) := have ∅ ⊆ opens X, from empty_subset _, have ⋃₀ ∅ ∈ opens X, from sUnion_mem_opens this, -show ∅ ∈ opens X, using this, by rewrite -sUnion_empty; apply this +show ∅ ∈ opens X, by rewrite -sUnion_empty; apply this theorem Open_univ : Open (univ : set X) := univ_mem_opens X @@ -42,7 +42,7 @@ using this, by rewrite Union_eq_sUnion_image; apply Open_sUnion this theorem Open_union {s t : set X} (Hs : Open s) (Ht : Open t) : Open (s ∪ t) := have ∀ i, Open (bin_ext s t i), by intro i; cases i; exact Hs; exact Ht, -show Open (s ∪ t), using this, by rewrite -Union_bin_ext; exact Open_Union this +show Open (s ∪ t), by rewrite -Union_bin_ext; exact Open_Union this theorem Open_inter {s t : set X} (Hs : Open s) (Ht : Open t) : Open (s ∩ t) := inter_mem_opens X Hs Ht diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 7ce415aa5..b47bc9d5c 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -404,11 +404,6 @@ static expr parse_proof(parser & p, expr const & prop) { } else if (p.curr_is_token(get_by_plus_tk())) { auto pos = p.pos(); return parse_by_plus(p, 0, nullptr, pos); - } else if (p.curr_is_token(get_using_tk())) { - // parse: 'using' locals* ',' proof - auto using_pos = p.pos(); - p.next(); - return parse_using_expr(p, prop, using_pos); } else { throw parser_error("invalid expression, 'by', 'begin', 'proof', 'using' or 'from' expected", p.pos()); } @@ -466,6 +461,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional con } p.check_token_next(get_comma_tk(), "invalid 'have/assert' declaration, ',' expected"); parser::local_scope scope(p); + is_visible = true; binder_info bi = mk_contextual_info(is_visible); expr l = p.save_pos(mk_local(id, prop, bi), pos); p.add_local(l); @@ -478,7 +474,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional con is_visible = true; } else { p.check_token_next(get_have_tk(), "invalid 'then' declaration, 'have' or 'assert' expected"); - is_visible = false; + is_visible = true; } body = parse_have_core(p, then_pos, some_expr(l), is_visible); } else { diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 525e5f958..61dcbdd4c 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -59,7 +59,6 @@ static format * g_let_fmt = nullptr; static format * g_in_fmt = nullptr; static format * g_assign_fmt = nullptr; static format * g_have_fmt = nullptr; -static format * g_assert_fmt = nullptr; static format * g_from_fmt = nullptr; static format * g_visible_fmt = nullptr; static format * g_show_fmt = nullptr; @@ -124,7 +123,6 @@ void initialize_pp() { g_in_fmt = new format(highlight_keyword(format("in"))); g_assign_fmt = new format(highlight_keyword(format(":="))); g_have_fmt = new format(highlight_keyword(format("have"))); - g_assert_fmt = new format(highlight_keyword(format("assert"))); g_from_fmt = new format(highlight_keyword(format("from"))); g_visible_fmt = new format(highlight_keyword(format("[visible]"))); g_show_fmt = new format(highlight_keyword(format("show"))); @@ -151,7 +149,6 @@ void finalize_pp() { delete g_in_fmt; delete g_assign_fmt; delete g_have_fmt; - delete g_assert_fmt; delete g_from_fmt; delete g_visible_fmt; delete g_show_fmt; @@ -779,7 +776,7 @@ auto pretty_fn::pp_have(expr const & e) -> result { format type_fmt = pp_child(mlocal_type(local), 0).fmt(); format proof_fmt = pp_child(proof, 0).fmt(); format body_fmt = pp_child(body, 0).fmt(); - format head_fmt = (binding_info(binding).is_contextual()) ? *g_assert_fmt : *g_have_fmt; + format head_fmt = *g_have_fmt; format r = head_fmt + space() + format(n) + space(); r += colon() + nest(m_indent, line() + type_fmt + comma() + space() + *g_from_fmt); r = group(r); diff --git a/tests/lean/congr_print.lean.expected.out b/tests/lean/congr_print.lean.expected.out index 06597dbd9..a7c474dbd 100644 --- a/tests/lean/congr_print.lean.expected.out +++ b/tests/lean/congr_print.lean.expected.out @@ -2,19 +2,18 @@ theorem perm.perm_erase_dup_of_perm [congr] : ∀ {A : Type} [H : decidable_eq A λ (A : Type) (H : decidable_eq A) (l₁ l₂ : list A) (p : l₁ ~ l₂), perm_induction_on p nil (λ (x : A) (t₁ t₂ : list A) (p : t₁ ~ t₂) (r : erase_dup t₁ ~ erase_dup t₂), - decidable.by_cases - (λ (xint₁ : x ∈ t₁), assert xint₂ : x ∈ t₂, from mem_of_mem_erase_dup …, … …) + decidable.by_cases (λ (xint₁ : x ∈ t₁), have xint₂ : x ∈ t₂, from mem_of_mem_erase_dup …, … …) (λ (nxint₁ : x ∉ t₁), - assert nxint₂ : x ∉ t₂, from λ (xint₂ : x ∈ t₂), … nxint₁, + have nxint₂ : x ∉ t₂, from λ (xint₂ : x ∈ t₂), … nxint₁, eq.rec … (eq.symm …))) (λ (y x : A) (t₁ t₂ : list A) (p : t₁ ~ t₂) (r : erase_dup t₁ ~ erase_dup t₂), decidable.by_cases (λ (xinyt₁ : x ∈ y :: t₁), decidable.by_cases (λ (yint₁ : …), …) - (λ (nyint₁ : y ∉ t₁), assert nyint₂ : …, from …, …)) + (λ (nyint₁ : y ∉ t₁), have nyint₂ : …, from …, …)) (λ (nxinyt₁ : x ∉ y :: t₁), have xney : x ≠ y, from ne_of_not_mem_cons nxinyt₁, have nxint₁ : x ∉ t₁, from not_mem_of_not_mem_cons nxinyt₁, - assert nxint₂ : x ∉ t₂, from λ (xint₂ : …), …, + have nxint₂ : x ∉ t₂, from λ (xint₂ : …), …, … …)) (λ (t₁ t₂ t₃ : list A) (p₁ : t₁ ~ t₂) (p₂ : t₂ ~ t₃), trans) diff --git a/tests/lean/extra/bag.661.20.expected.out b/tests/lean/extra/bag.661.20.expected.out index 7e9e05233..be03a4bc1 100644 --- a/tests/lean/extra/bag.661.20.expected.out +++ b/tests/lean/extra/bag.661.20.expected.out @@ -9,6 +9,7 @@ a : A, l₁ l₂ : list A, h : subcount (a :: l₁) l₂ = tt, x : A, +this : subcount l₁ l₂ = tt, ih : ∀ (a : A), list.count a l₁ ≤ list.count a l₂, i : list.count a (a :: l₁) ≤ list.count a l₂, this : x = a diff --git a/tests/lean/finset_induction_bug.lean.expected.out b/tests/lean/finset_induction_bug.lean.expected.out index 21ad4e10f..978fe4b99 100644 --- a/tests/lean/finset_induction_bug.lean.expected.out +++ b/tests/lean/finset_induction_bug.lean.expected.out @@ -65,9 +65,9 @@ remark: set 'formatter.hide_full_terms' to false to see the complete term (λ (l : …), @list.induction_on A … l … (λ (a : A) (l' : …) (IH : …) (nodup_al' : …), - assert anl' : …, from …, - assert H3 : …, from …, - assert nodup_l' : …, from …, - assert P_l' : …, from …, + have anl' : …, from …, + have H3 : …, from …, + have nodup_l' : …, from …, + have P_l' : …, from …, ?M_1 …))) finset_induction_bug.lean:30:49: error: invalid end of module, expecting 'end' diff --git a/tests/lean/have1.lean b/tests/lean/have1.lean index 30444a016..9b892974a 100644 --- a/tests/lean/have1.lean +++ b/tests/lean/have1.lean @@ -5,10 +5,10 @@ constants a b c : bool axiom H1 : a = b axiom H2 : b = c -check have e1 [visible] : a = b, from H1, +check have e1 : a = b, from H1, have e2 : a = c, by apply trans; apply e1; apply H2, have e3 : c = a, from e2⁻¹, - have e4 [visible] : b = a, from e1⁻¹, + have e4 : b = a, from e1⁻¹, have e5 : b = c, from e4 ⬝ e2, have e6 : a = a, from H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹ ⬝ H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹, e3 ⬝ e2 diff --git a/tests/lean/have1.lean.expected.out b/tests/lean/have1.lean.expected.out index 2f644230f..a196b8344 100644 --- a/tests/lean/have1.lean.expected.out +++ b/tests/lean/have1.lean.expected.out @@ -1,7 +1,7 @@ -assert e1 : a = b, from H1, +have e1 : a = b, from H1, have e2 : a = c, from e1 ⬝ H2, have e3 : c = a, from e2⁻¹, -assert e4 : b = a, from e1⁻¹, +have e4 : b = a, from e1⁻¹, have e5 : b = c, from e4 ⬝ e2, have e6 : a = a, from H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹ ⬝ H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹, e3 ⬝ e2 : diff --git a/tests/lean/run/830.lean b/tests/lean/run/830.lean index 634bff9b8..e4dfbaf56 100644 --- a/tests/lean/run/830.lean +++ b/tests/lean/run/830.lean @@ -23,7 +23,7 @@ show P, begin+ exact H end example : P := have H : P, from HP, -show P, using H, by exact H +show P, by exact H example : P := assert H : P, from HP, diff --git a/tests/lean/run/have1.lean b/tests/lean/run/have1.lean index 9fd2e17d1..aae47af58 100644 --- a/tests/lean/run/have1.lean +++ b/tests/lean/run/have1.lean @@ -5,5 +5,5 @@ axiom Ha : a axiom Hb : b axiom Hc : c check have H1 : a, from Ha, - have H2 : a, using H1, from H1, + have H2 : a, from H1, H2 diff --git a/tests/lean/run/using_bug.lean b/tests/lean/run/using_bug.lean index 71e882b74..787511c43 100644 --- a/tests/lean/run/using_bug.lean +++ b/tests/lean/run/using_bug.lean @@ -3,7 +3,7 @@ assume Hpqr : p ∧ q ∧ r, have Hp : p, from and.elim_left Hpqr, have Hqr : q ∧ r, from and.elim_right Hpqr, have Hq : q, from and.elim_left Hqr, -show q ∧ p, using Hp Hq, from +show q ∧ p, from proof and.intro Hq Hp qed diff --git a/tests/lean/run/using_bug2.lean b/tests/lean/run/using_bug2.lean index cf457f683..d74e84f60 100644 --- a/tests/lean/run/using_bug2.lean +++ b/tests/lean/run/using_bug2.lean @@ -3,10 +3,11 @@ variable {f : A → A → A} variable {finv : A → A} premise (h : ∀ x y : A, finv (f x y) = y) +include h theorem foo₁ : ∀ x y z : A, f x y = f x z → y = z := -λ x y z, assume e, using h, from sorry +λ x y z, assume e, sorry theorem foo₂ : ∀ x y z : A, f x y = f x z → y = z := λ x y z, assume e, assert s₁ : finv (f x y) = finv (f x z), by rewrite e, -show y = z, using h, by rewrite *h at s₁; exact s₁ +show y = z, by rewrite *h at s₁; exact s₁ diff --git a/tests/lean/show1.lean.expected.out b/tests/lean/show1.lean.expected.out index cc67b811b..b9e6b5b4e 100644 --- a/tests/lean/show1.lean.expected.out +++ b/tests/lean/show1.lean.expected.out @@ -1,8 +1,8 @@ show a = c, from H1 ⬝ H2 : a = c ------------ -assert e1 : a = b, from H1, +have e1 : a = b, from H1, have e2 : a = c, from e1 ⬝ H2, have e3 : c = a, from e2⁻¹, -assert e4 : b = a, from e1⁻¹, +have e4 : b = a, from e1⁻¹, show b = c, from e1⁻¹ ⬝ e2 : b = c