From 92f8eb173bd43c94f123c6bfc43c4033a259fc6c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Jul 2015 13:36:05 -0500 Subject: [PATCH] feat(frontends/lean): use 'this' as the name for anonymous 'have'-expression --- library/data/list/perm.lean | 49 ++++++------- library/data/nat/basic.lean | 6 +- library/data/nat/bquant.lean | 12 ++-- library/data/nat/choose.lean | 10 +-- library/data/nat/div.lean | 22 +++--- library/data/nat/order.lean | 22 +++--- library/theories/number_theory/primes.lean | 82 +++++++++++----------- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_exprs.cpp | 12 ++-- src/frontends/lean/tokens.cpp | 4 ++ src/frontends/lean/tokens.h | 1 + src/frontends/lean/tokens.txt | 1 + 12 files changed, 117 insertions(+), 106 deletions(-) diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 2ed44bdd1..8ba0dc43a 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -237,17 +237,17 @@ definition decidable_perm_aux : ∀ (n : nat) (l₁ l₂ : list A), length l₁ by_cases (assume xinl₂ : x ∈ l₂, let t₂ : list A := erase x l₂ in - have len_t₁ : length t₁ = n, begin injection H₁ with e, exact e end, - assert len_t₂_aux : length t₂ = pred (length l₂), from length_erase_of_mem xinl₂, - assert len_t₂ : length t₂ = n, by rewrite [len_t₂_aux, H₂], - match decidable_perm_aux n t₁ t₂ len_t₁ len_t₂ with + have len_t₁ : length t₁ = n, begin injection H₁ with e, exact e end, + assert length t₂ = pred (length l₂), from length_erase_of_mem xinl₂, + assert length t₂ = n, by rewrite [this, H₂], + match decidable_perm_aux n t₁ t₂ len_t₁ this with | inl p := inl (calc x::t₁ ~ x::(erase x l₂) : skip x p ... ~ l₂ : perm_erase xinl₂) | inr np := inr (λ p : x::t₁ ~ l₂, - assert p₁ : erase x (x::t₁) ~ erase x l₂, from erase_perm_erase_of_perm x p, - have p₂ : t₁ ~ erase x l₂, by rewrite [erase_cons_head at p₁]; exact p₁, - absurd p₂ np) + assert erase x (x::t₁) ~ erase x l₂, from erase_perm_erase_of_perm x p, + have t₁ ~ erase x l₂, by rewrite [erase_cons_head at this]; exact this, + absurd this np) end) (assume nxinl₂ : x ∉ l₂, inr (λ p : x::t₁ ~ l₂, absurd (mem_perm p !mem_cons) nxinl₂)) @@ -450,9 +450,9 @@ perm_induction_on p' (r₁ : ∀{a s₁ s₂}, t₁ ≈ a|s₁ → t₂≈a|s₂ → s₁ ~ s₂) (r₂ : ∀{a s₁ s₂}, t₂ ≈ a|s₁ → t₃≈a|s₂ → s₁ ~ s₂) a s₁ s₂ e₁ e₂, - have aint₁ : a ∈ t₁, from mem_head_of_qeq e₁, - have aint₂ : a ∈ t₂, from mem_perm p₁ aint₁, - obtain (t₂' : list A) (e₂' : t₂≈a|t₂'), from qeq_of_mem aint₂, + have a ∈ t₁, from mem_head_of_qeq e₁, + have a ∈ t₂, from mem_perm p₁ this, + obtain (t₂' : list A) (e₂' : t₂≈a|t₂'), from qeq_of_mem this, calc s₁ ~ t₂' : r₁ e₁ e₂' ... ~ s₂ : r₂ e₂' e₂) @@ -688,17 +688,15 @@ theorem perm_ext : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → (∀a | [] (a₂::t₂) d₁ d₂ e := absurd (iff.mpr (e a₂) !mem_cons) (not_mem_nil a₂) | (a₁::t₁) [] d₁ d₂ e := absurd (iff.mp (e a₁) !mem_cons) (not_mem_nil a₁) | (a₁::t₁) (a₂::t₂) d₁ d₂ e := - have a₁inl₂ : a₁ ∈ a₂::t₂, from iff.mp (e a₁) !mem_cons, - have dt₁ : nodup t₁, from nodup_of_nodup_cons d₁, - have na₁int₁ : a₁ ∉ t₁, from not_mem_of_nodup_cons d₁, - have ex : ∃s₁ s₂, a₂::t₂ = s₁++(a₁::s₂), from mem_split a₁inl₂, - obtain (s₁ s₂ : list A) (t₂_eq : a₂::t₂ = s₁++(a₁::s₂)), from ex, + have a₁ ∈ a₂::t₂, from iff.mp (e a₁) !mem_cons, + have ∃s₁ s₂, a₂::t₂ = s₁++(a₁::s₂), from mem_split this, + obtain (s₁ s₂ : list A) (t₂_eq : a₂::t₂ = s₁++(a₁::s₂)), from this, have dt₂' : nodup (a₁::(s₁++s₂)), from nodup_head (by rewrite [t₂_eq at d₂]; exact d₂), have na₁s₁s₂ : a₁ ∉ s₁++s₂, from not_mem_of_nodup_cons dt₂', have na₁s₁ : a₁ ∉ s₁, from not_mem_of_not_mem_append_left na₁s₁s₂, have na₁s₂ : a₁ ∉ s₂, from not_mem_of_not_mem_append_right na₁s₁s₂, have ds₁s₂ : nodup (s₁++s₂), from nodup_of_nodup_cons dt₂', - have eqv : ∀a, a ∈ t₁ ↔ a ∈ s₁++s₂, from + have eqv : ∀a, a ∈ t₁ ↔ a ∈ s₁++s₂, from take a, iff.intro (λ aint₁ : a ∈ t₁, assert aina₂t₂ : a ∈ a₂::t₂, from iff.mp (e a) (mem_cons_of_mem _ aint₁), @@ -706,22 +704,25 @@ theorem perm_ext : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → (∀a or.elim (mem_or_mem_of_mem_append ains₁a₁s₂) (λ ains₁ : a ∈ s₁, mem_append_left s₂ ains₁) (λ aina₁s₂ : a ∈ a₁::s₂, or.elim (eq_or_mem_of_mem_cons aina₁s₂) - (λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ aint₁) na₁int₁) + (λ aeqa₁ : a = a₁, + have a₁ ∉ t₁, from not_mem_of_nodup_cons d₁, + absurd (aeqa₁ ▸ aint₁) this) (λ ains₂ : a ∈ s₂, mem_append_right s₁ ains₂))) (λ ains₁s₂ : a ∈ s₁ ++ s₂, or.elim (mem_or_mem_of_mem_append ains₁s₂) (λ ains₁ : a ∈ s₁, - have aina₂t₂ : a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_left _ ains₁), - have aina₁t₁ : a ∈ a₁::t₁, from iff.mpr (e a) aina₂t₂, - or.elim (eq_or_mem_of_mem_cons aina₁t₁) + have a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_left _ ains₁), + have a ∈ a₁::t₁, from iff.mpr (e a) this, + or.elim (eq_or_mem_of_mem_cons this) (λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ ains₁) na₁s₁) (λ aint₁ : a ∈ t₁, aint₁)) (λ ains₂ : a ∈ s₂, - have aina₂t₂ : a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_right _ (mem_cons_of_mem _ ains₂)), - have aina₁t₁ : a ∈ a₁::t₁, from iff.mpr (e a) aina₂t₂, - or.elim (eq_or_mem_of_mem_cons aina₁t₁) + have a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_right _ (mem_cons_of_mem _ ains₂)), + have a ∈ a₁::t₁, from iff.mpr (e a) this, + or.elim (eq_or_mem_of_mem_cons this) (λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ ains₂) na₁s₂) (λ aint₁ : a ∈ t₁, aint₁))), - calc a₁::t₁ ~ a₁::(s₁++s₂) : skip a₁ (perm_ext dt₁ ds₁s₂ eqv) + have nodup t₁, from nodup_of_nodup_cons d₁, + calc a₁::t₁ ~ a₁::(s₁++s₂) : skip a₁ (perm_ext this ds₁s₂ eqv) ... ~ s₁++(a₁::s₂) : !perm_middle ... = a₂::t₂ : by rewrite t₂_eq end ext diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index c3ef4904a..4de7aa535 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -157,13 +157,13 @@ nat.induction_on n (take H : 0 + m = 0 + k, !zero_add⁻¹ ⬝ H ⬝ !zero_add) (take (n : ℕ) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k), - have H2 : succ (n + m) = succ (n + k), + have succ (n + m) = succ (n + k), from calc succ (n + m) = succ n + m : succ_add ... = succ n + k : H ... = succ (n + k) : succ_add, - have H3 : n + m = n + k, from succ.inj H2, - IH H3) + have n + m = n + k, from succ.inj this, + IH this) theorem add.cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k := have H2 : m + n = m + k, from !add.comm ⬝ H ⬝ !add.comm, diff --git a/library/data/nat/bquant.lean b/library/data/nat/bquant.lean index 26ae85568..b6b714d76 100644 --- a/library/data/nat/bquant.lean +++ b/library/data/nat/bquant.lean @@ -123,10 +123,10 @@ namespace nat | 0 h := absurd (ball_zero P) h | (succ n) h := decidable.by_cases (λ hp : P n, - have h₁ : ¬ ball n P, from + have ¬ ball n P, from assume b : ball n P, absurd (ball_succ_of_ball b hp) h, - have h₂ : {i | i < n ∧ ¬ P i}, from bsub_not_of_not_ball h₁, - bsub_succ h₂) + have {i | i < n ∧ ¬ P i}, from bsub_not_of_not_ball this, + bsub_succ this) (λ hn : ¬ P n, bsub_succ_of_pred hn) theorem bex_not_of_not_ball {n : nat} (H : ¬ ball n P) : bex n (λ n, ¬ P n) := @@ -137,8 +137,8 @@ namespace nat | (succ n) h := by_cases (λ hp : P n, absurd (bex_succ_of_pred hp) h) (λ hn : ¬ P n, - have h₁ : ¬ bex n P, from + have ¬ bex n P, from assume b : bex n P, absurd (bex_succ b) h, - have h₂ : ball n (λ n, ¬ P n), from ball_not_of_not_bex h₁, - ball_succ_of_ball h₂ hn) + have ball n (λ n, ¬ P n), from ball_not_of_not_bex this, + ball_succ_of_ball this hn) end nat diff --git a/library/data/nat/choose.lean b/library/data/nat/choose.lean index 8100a0f15..36025adf2 100644 --- a/library/data/nat/choose.lean +++ b/library/data/nat/choose.lean @@ -42,12 +42,12 @@ acc.intro x (λ (y : nat) (l : y ≺ x), private lemma acc_of_acc_succ {x : nat} : acc gtb (succ x) → acc gtb x := assume h, acc.intro x (λ (y : nat) (l : y ≺ x), - have ygtx : x < y, from and.elim_left l, by_cases - (λ yeqx : y = succ x, by substvars; assumption) - (λ ynex : y ≠ succ x, - have ygtsx : succ x < y, from lt_of_le_and_ne ygtx (ne.symm ynex), - acc.inv h (and.intro ygtsx (and.elim_right l)))) + (assume yeqx : y = succ x, by substvars; assumption) + (assume ynex : y ≠ succ x, + have x < y, from and.elim_left l, + have succ x < y, from lt_of_le_and_ne this (ne.symm ynex), + acc.inv h (and.intro this (and.elim_right l)))) private lemma acc_of_px_of_gt {x y : nat} : p x → y > x → acc gtb y := assume px ygtx, diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 37c1a0342..9af907260 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -135,14 +135,14 @@ nat.case_strong_induction_on x show succ x mod y < y, from by_cases -- (succ x < y) (assume H1 : succ x < y, - have H2 : succ x mod y = succ x, from mod_eq_of_lt H1, - show succ x mod y < y, from H2⁻¹ ▸ H1) + have succ x mod y = succ x, from mod_eq_of_lt H1, + show succ x mod y < y, from this⁻¹ ▸ H1) (assume H1 : ¬ succ x < y, - have H2 : y ≤ succ x, from le_of_not_gt H1, - have H3 : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H H2, - have H4 : succ x - y < succ x, from sub_lt !succ_pos H, - have H5 : succ x - y ≤ x, from le_of_lt_succ H4, - show succ x mod y < y, from H3⁻¹ ▸ IH _ H5)) + have y ≤ succ x, from le_of_not_gt H1, + have h : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H this, + have succ x - y < succ x, from sub_lt !succ_pos H, + have succ x - y ≤ x, from le_of_lt_succ this, + show succ x mod y < y, from h⁻¹ ▸ IH _ this)) theorem mod_one (n : ℕ) : n mod 1 = 0 := have H1 : n mod 1 < 1, from !mod_lt !succ_pos, @@ -368,10 +368,10 @@ by_cases_zero_pos n assume H2 : n ∣ m, obtain k (Hk : n = m * k), from exists_eq_mul_right_of_dvd H1, obtain l (Hl : m = n * l), from exists_eq_mul_right_of_dvd H2, - have H3 : n * (l * k) = n, from !mul.assoc ▸ Hl ▸ Hk⁻¹, - have H4 : l * k = 1, from eq_one_of_mul_eq_self_right Hpos H3, - have H5 : k = 1, from eq_one_of_mul_eq_one_left H4, - show m = n, from (mul_one m)⁻¹ ⬝ (H5 ▸ Hk⁻¹)) + have n * (l * k) = n, from !mul.assoc ▸ Hl ▸ Hk⁻¹, + have l * k = 1, from eq_one_of_mul_eq_self_right Hpos this, + have k = 1, from eq_one_of_mul_eq_one_left this, + show m = n, from (mul_one m)⁻¹ ⬝ (this ▸ Hk⁻¹)) theorem mul_div_assoc (m : ℕ) {n k : ℕ} (H : k ∣ n) : m * n div k = m * (n div k) := or.elim (eq_zero_or_pos k) diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 9162e42d7..19f2d4250 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -392,11 +392,11 @@ have H4 : k * m < k * l, from mul_lt_mul_of_pos_left H2 (lt_of_le_of_lt !zero_le lt_of_le_of_lt H3 H4 theorem eq_of_mul_eq_mul_left {m k n : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k := -have H2 : n * m ≤ n * k, by rewrite H, -have H3 : n * k ≤ n * m, by rewrite H, -have H4 : m ≤ k, from le_of_mul_le_mul_left H2 Hn, -have H5 : k ≤ m, from le_of_mul_le_mul_left H3 Hn, -le.antisymm H4 H5 +have n * m ≤ n * k, by rewrite H, +have h : m ≤ k, from le_of_mul_le_mul_left this Hn, +have n * k ≤ n * m, by rewrite H, +have k ≤ m, from le_of_mul_le_mul_left this Hn, +le.antisymm h this theorem eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k := eq_of_mul_eq_mul_left Hm (!mul.comm ▸ !mul.comm ▸ H) @@ -410,15 +410,15 @@ eq_zero_or_eq_of_mul_eq_mul_left (!mul.comm ▸ !mul.comm ▸ H) theorem eq_one_of_mul_eq_one_right {n m : ℕ} (H : n * m = 1) : n = 1 := have H2 : n * m > 0, by rewrite H; apply succ_pos, -have H3 : n > 0, from pos_of_mul_pos_right H2, -have H4 : m > 0, from pos_of_mul_pos_left H2, or.elim (le_or_gt n 1) (assume H5 : n ≤ 1, - show n = 1, from le.antisymm H5 (succ_le_of_lt H3)) + have n > 0, from pos_of_mul_pos_right H2, + show n = 1, from le.antisymm H5 (succ_le_of_lt this)) (assume H5 : n > 1, - have H6 : n * m ≥ 2 * 1, from mul_le_mul (succ_le_of_lt H5) (succ_le_of_lt H4), - have H7 : 1 ≥ 2, from !mul_one ▸ H ▸ H6, - absurd !lt_succ_self (not_lt_of_ge H7)) + have m > 0, from pos_of_mul_pos_left H2, + have n * m ≥ 2 * 1, from mul_le_mul (succ_le_of_lt H5) (succ_le_of_lt this), + have 1 ≥ 2, from !mul_one ▸ H ▸ this, + absurd !lt_succ_self (not_lt_of_ge this)) theorem eq_one_of_mul_eq_one_left {n m : ℕ} (H : n * m = 1) : m = 1 := eq_one_of_mul_eq_one_right (!mul.comm ▸ H) diff --git a/library/theories/number_theory/primes.lean b/library/theories/number_theory/primes.lean index 9671f9105..385d41291 100644 --- a/library/theories/number_theory/primes.lean +++ b/library/theories/number_theory/primes.lean @@ -64,23 +64,23 @@ assume h d, obtain h₁ h₂, from h, h₂ m d lemma gt_one_of_pos_of_prime_dvd {i p : nat} : prime p → 0 < i → i mod p = 0 → 1 < i := assume ipp pos h, -have h₁ : p ∣ i, from dvd_of_mod_eq_zero h, -have h₂ : p ≥ 2, from ge_two_of_prime ipp, -have h₃ : p ≤ i, from le_of_dvd pos h₁, -lt_of_succ_le (le.trans h₂ h₃) +have h₁ : p ≥ 2, from ge_two_of_prime ipp, +have p ∣ i, from dvd_of_mod_eq_zero h, +have p ≤ i, from le_of_dvd pos this, +lt_of_succ_le (le.trans h₁ this) definition sub_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → {m | m ∣ n ∧ m ≠ 1 ∧ m ≠ n} := assume h₁ h₂, -have h₃ : ¬ prime_ext n, from iff.mpr (not_iff_not_of_iff !prime_ext_iff_prime) h₂, -have h₄ : ¬ n ≥ 2 ∨ ¬ (∀ m, m ≤ n → m ∣ n → m = 1 ∨ m = n), from iff.mp !not_and_iff_not_or_not h₃, -have h₅ : ¬ (∀ m, m ≤ n → m ∣ n → m = 1 ∨ m = n), from or_resolve_right h₄ (not_not_intro h₁), -have h₆ : ¬ (∀ m, m < succ n → m ∣ n → m = 1 ∨ m = n), from - assume h, absurd (λ m hl hd, h m (lt_succ_of_le hl) hd) h₅, -have h₇ : {m | m < succ n ∧ ¬(m ∣ n → m = 1 ∨ m = n)}, from bsub_not_of_not_ball h₆, -obtain m hlt (h₈ : ¬(m ∣ n → m = 1 ∨ m = n)), from h₇, -obtain (h₈ : m ∣ n) (h₉ : ¬ (m = 1 ∨ m = n)), from iff.mp !not_implies_iff_and_not h₈, -have h₁₀ : ¬ m = 1 ∧ ¬ m = n, from iff.mp !not_or_iff_not_and_not h₉, -subtype.tag m (and.intro h₈ h₁₀) +have ¬ prime_ext n, from iff.mpr (not_iff_not_of_iff !prime_ext_iff_prime) h₂, +have ¬ n ≥ 2 ∨ ¬ (∀ m, m ≤ n → m ∣ n → m = 1 ∨ m = n), from iff.mp !not_and_iff_not_or_not this, +have ¬ (∀ m, m ≤ n → m ∣ n → m = 1 ∨ m = n), from or_resolve_right this (not_not_intro h₁), +have ¬ (∀ m, m < succ n → m ∣ n → m = 1 ∨ m = n), from + assume h, absurd (λ m hl hd, h m (lt_succ_of_le hl) hd) this, +have {m | m < succ n ∧ ¬(m ∣ n → m = 1 ∨ m = n)}, from bsub_not_of_not_ball this, +obtain m hlt (h₃ : ¬(m ∣ n → m = 1 ∨ m = n)), from this, +obtain (h₄ : m ∣ n) (h₅ : ¬ (m = 1 ∨ m = n)), from iff.mp !not_implies_iff_and_not h₃, +have ¬ m = 1 ∧ ¬ m = n, from iff.mp !not_or_iff_not_and_not h₅, +subtype.tag m (and.intro h₄ this) theorem ex_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n := assume h₁ h₂, ex_of_sub (sub_dvd_of_not_prime h₁ h₂) @@ -121,20 +121,20 @@ open eq.ops definition infinite_primes (n : nat) : {p | p ≥ n ∧ prime p} := let m := fact (n + 1) in -have m_ge_1 : m ≥ 1, from le_of_lt_succ (succ_lt_succ (fact_pos _)), -have m1_ge_2 : m + 1 ≥ 2, from succ_le_succ m_ge_1, -obtain p (prime_p : prime p) (p_dvd_m1 : p ∣ m + 1), from sub_prime_and_dvd m1_ge_2, +have m ≥ 1, from le_of_lt_succ (succ_lt_succ (fact_pos _)), +have m + 1 ≥ 2, from succ_le_succ this, +obtain p (prime_p : prime p) (p_dvd_m1 : p ∣ m + 1), from sub_prime_and_dvd this, have p_ge_2 : p ≥ 2, from ge_two_of_prime prime_p, have p_gt_0 : p > 0, from lt_of_succ_lt (lt_of_succ_le p_ge_2), -have p_ge_n : p ≥ n, from by_contradiction +have p ≥ n, from by_contradiction (assume h₁ : ¬ p ≥ n, - have h₂ : p < n, from lt_of_not_ge h₁, - have h₃ : p ≤ n + 1, from le_of_lt (lt.step h₂), - have h₄ : p ∣ m, from dvd_fact p_gt_0 h₃, - have h₅ : p ∣ 1, from dvd_of_dvd_add_right (!add.comm ▸ p_dvd_m1) h₄, - have h₆ : p ≤ 1, from le_of_dvd zero_lt_one h₅, - absurd (le.trans p_ge_2 h₆) dec_trivial), -subtype.tag p (and.intro p_ge_n prime_p) + have p < n, from lt_of_not_ge h₁, + have p ≤ n + 1, from le_of_lt (lt.step this), + have p ∣ m, from dvd_fact p_gt_0 this, + have p ∣ 1, from dvd_of_dvd_add_right (!add.comm ▸ p_dvd_m1) this, + have p ≤ 1, from le_of_dvd zero_lt_one this, + absurd (le.trans p_ge_2 this) dec_trivial), +subtype.tag p (and.intro this prime_p) lemma ex_infinite_primes (n : nat) : ∃ p, p ≥ n ∧ prime p := ex_of_sub (infinite_primes n) @@ -158,10 +158,10 @@ by_contradiction (assume nc : ¬ coprime p n, npdvdn (dvd_of_prime_of_not_coprim theorem not_dvd_of_prime_of_coprime {p n : ℕ} (primep : prime p) (cop : coprime p n) : ¬ p ∣ n := assume pdvdn : p ∣ n, -have H1 : p ∣ gcd p n, from dvd_gcd !dvd.refl pdvdn, -have H2 : p ≤ gcd p n, from le_of_dvd (!gcd_pos_of_pos_left (pos_of_prime primep)) H1, -have H3 : 2 ≤ 1, from le.trans (ge_two_of_prime primep) (cop ▸ H2), -show false, from !not_succ_le_self H3 +have p ∣ gcd p n, from dvd_gcd !dvd.refl pdvdn, +have p ≤ gcd p n, from le_of_dvd (!gcd_pos_of_pos_left (pos_of_prime primep)) this, +have 2 ≤ 1, from le.trans (ge_two_of_prime primep) (cop ▸ this), +show false, from !not_succ_le_self this theorem not_coprime_of_prime_dvd {p n : ℕ} (primep : prime p) (pdvdn : p ∣ n) : ¬ coprime p n := assume cop, not_dvd_of_prime_of_coprime primep cop pdvdn @@ -169,8 +169,8 @@ assume cop, not_dvd_of_prime_of_coprime primep cop pdvdn theorem dvd_of_prime_of_dvd_mul_left {p m n : ℕ} (primep : prime p) (Hmn : p ∣ m * n) (Hm : ¬ p ∣ m) : p ∣ n := -have copm : coprime p m, from coprime_of_prime_of_not_dvd primep Hm, -show p ∣ n, from dvd_of_coprime_of_dvd_mul_left copm Hmn +have coprime p m, from coprime_of_prime_of_not_dvd primep Hm, +show p ∣ n, from dvd_of_coprime_of_dvd_mul_left this Hmn theorem dvd_of_prime_of_dvd_mul_right {p m n : ℕ} (primep : prime p) (Hmn : p ∣ m * n) (Hn : ¬ p ∣ n) : @@ -188,12 +188,12 @@ lemma dvd_or_dvd_of_prime_of_dvd_mul {p m n : nat} : prime p → p ∣ m * n → lemma dvd_of_prime_of_dvd_pow {p m : nat} : ∀ {n}, prime p → p ∣ m^n → p ∣ m | 0 hp hd := - assert peq1 : p = 1, from eq_one_of_dvd_one hd, - have h₂ : 1 ≥ 2, by rewrite -peq1; apply ge_two_of_prime hp, - absurd h₂ dec_trivial + assert p = 1, from eq_one_of_dvd_one hd, + have 1 ≥ 2, by rewrite -this; apply ge_two_of_prime hp, + absurd this dec_trivial | (succ n) hp hd := - have hd₁ : p ∣ (m^n)*m, by rewrite [pow_succ at hd]; exact hd, - or.elim (dvd_or_dvd_of_prime_of_dvd_mul hp hd₁) + have p ∣ (m^n)*m, by rewrite [pow_succ at hd]; exact hd, + or.elim (dvd_or_dvd_of_prime_of_dvd_mul hp this) (λ h : p ∣ m^n, dvd_of_prime_of_dvd_pow hp h) (λ h : p ∣ m, h) @@ -202,13 +202,13 @@ lemma coprime_pow_of_prime_of_not_dvd {p m a : nat} : prime p → ¬ p ∣ a → lemma coprime_primes {p q : nat} : prime p → prime q → p ≠ q → coprime p q := λ hp hq hn, - assert d₁ : gcd p q ∣ p, from !gcd_dvd_left, - assert d₂ : gcd p q ∣ q, from !gcd_dvd_right, - or.elim (eq_one_or_eq_self_of_prime_of_dvd hp d₁) + assert gcd p q ∣ p, from !gcd_dvd_left, + or.elim (eq_one_or_eq_self_of_prime_of_dvd hp this) (λ h : gcd p q = 1, h) (λ h : gcd p q = p, - have d₃ : p ∣ q, by rewrite -h; exact d₂, - or.elim (eq_one_or_eq_self_of_prime_of_dvd hq d₃) + assert gcd p q ∣ q, from !gcd_dvd_right, + have p ∣ q, by rewrite -h; exact this, + or.elim (eq_one_or_eq_self_of_prime_of_dvd hq this) (λ h₁ : p = 1, by subst p; exact absurd hp not_prime_one) (λ he : p = q, by contradiction)) diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index c5eae4ab8..fce21c492 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -16,7 +16,7 @@ "alias" "help" "environment" "options" "precedence" "reserve" "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "tactic_infix" "tactic_infixl" "tactic_infixr" "tactic_notation" "tactic_postfix" "tactic_prefix" - "eval" "check" "end" "reveal" + "eval" "check" "end" "reveal" "this" "using" "namespace" "section" "fields" "find_decl" "attribute" "local" "set_option" "extends" "include" "omit" "classes" "instances" "coercions" "metaclasses" "raw" "migrate" "replacing") diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 5c1fcb78a..9109b6a57 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -369,7 +369,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional con if (p.curr_is_token(get_visible_tk())) { p.next(); is_visible = true; - id = p.mk_fresh_name(); + id = get_this_tk(); prop = p.parse_expr(); } else if (p.curr_is_identifier()) { id = p.get_name_val(); @@ -384,11 +384,15 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional con prop = p.parse_expr(); } else { expr left = p.id_to_expr(id, id_pos); - id = p.mk_fresh_name(); - prop = p.parse_led(left); + id = get_this_tk(); + unsigned rbp = 0; + while (rbp < p.curr_expr_lbp()) { + left = p.parse_led(left); + } + prop = left; } } else { - id = p.mk_fresh_name(); + id = get_this_tk(); prop = p.parse_expr(); } expr proof; diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 3c603a01c..808145c17 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -141,6 +141,7 @@ static name const * g_fields_tk = nullptr; static name const * g_trust_tk = nullptr; static name const * g_metaclasses_tk = nullptr; static name const * g_inductive_tk = nullptr; +static name const * g_this_tk = nullptr; void initialize_tokens() { g_period_tk = new name{"."}; g_placeholder_tk = new name{"_"}; @@ -280,6 +281,7 @@ void initialize_tokens() { g_trust_tk = new name{"trust"}; g_metaclasses_tk = new name{"metaclasses"}; g_inductive_tk = new name{"inductive"}; + g_this_tk = new name{"this"}; } void finalize_tokens() { delete g_period_tk; @@ -420,6 +422,7 @@ void finalize_tokens() { delete g_trust_tk; delete g_metaclasses_tk; delete g_inductive_tk; + delete g_this_tk; } name const & get_period_tk() { return *g_period_tk; } name const & get_placeholder_tk() { return *g_placeholder_tk; } @@ -559,4 +562,5 @@ name const & get_fields_tk() { return *g_fields_tk; } name const & get_trust_tk() { return *g_trust_tk; } name const & get_metaclasses_tk() { return *g_metaclasses_tk; } name const & get_inductive_tk() { return *g_inductive_tk; } +name const & get_this_tk() { return *g_this_tk; } } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 323195b8e..621dc6daa 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -143,4 +143,5 @@ name const & get_fields_tk(); name const & get_trust_tk(); name const & get_metaclasses_tk(); name const & get_inductive_tk(); +name const & get_this_tk(); } diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index a76230e5e..a00f8abc4 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -136,3 +136,4 @@ fields fields trust trust metaclasses metaclasses inductive inductive +this this