From 812ddf1ef56da7e06dc893b096619dc5d2746ad5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Jul 2015 12:15:12 -0700 Subject: [PATCH] feat(frontends/lean): add 'suppose'-expression It is a variant of 'assume' that allow anonymous declarations. --- library/data/list/basic.lean | 79 +++++++++++----------- library/data/list/perm.lean | 12 ++-- library/theories/number_theory/primes.lean | 23 ++++--- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_exprs.cpp | 32 +++++++++ src/frontends/lean/token_table.cpp | 2 +- 6 files changed, 91 insertions(+), 59 deletions(-) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 27adc5e90..3766cf6f2 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -311,22 +311,21 @@ list.rec_on l decidable.rec_on iH (assume Hp : x ∈ l, decidable.rec_on (H x h) - (assume Heq : x = h, - decidable.inl (or.inl Heq)) - (assume Hne : x ≠ h, + (suppose x = h, + decidable.inl (or.inl this)) + (suppose x ≠ h, decidable.inl (or.inr Hp))) - (assume Hn : ¬x ∈ l, + (suppose ¬x ∈ l, decidable.rec_on (H x h) - (assume Heq : x = h, - decidable.inl (or.inl Heq)) - (assume Hne : x ≠ h, - have H1 : ¬(x = h ∨ x ∈ l), from - assume H2 : x = h ∨ x ∈ l, or.elim H2 - (assume Heq, by contradiction) - (assume Hp, by contradiction), - have H2 : ¬x ∈ h::l, from - iff.elim_right (not_iff_not_of_iff !mem_cons_iff) H1, - decidable.inr H2))) + (suppose x = h, decidable.inl (or.inl this)) + (suppose x ≠ h, + have ¬(x = h ∨ x ∈ l), from + suppose x = h ∨ x ∈ l, or.elim this + (suppose x = h, by contradiction) + (suppose x ∈ l, by contradiction), + have ¬x ∈ h::l, from + iff.elim_right (not_iff_not_of_iff !mem_cons_iff) this, + decidable.inr this))) theorem mem_of_ne_of_mem {x y : T} {l : list T} (H₁ : x ≠ y) (H₂ : x ∈ y :: l) : x ∈ l := or.elim (eq_or_mem_of_mem_cons H₂) (λe, absurd e H₁) (λr, r) @@ -378,24 +377,24 @@ theorem sub_cons_of_sub (a : T) {l₁ l₂ : list T} : l₁ ⊆ l₂ → l₁ theorem sub_app_of_sub_left (l l₁ l₂ : list T) : l ⊆ l₁ → l ⊆ l₁++l₂ := λ (s : l ⊆ l₁) (x : T) (xinl : x ∈ l), - have xinl₁ : x ∈ l₁, from s xinl, - mem_append_of_mem_or_mem (or.inl xinl₁) + have x ∈ l₁, from s xinl, + mem_append_of_mem_or_mem (or.inl this) theorem sub_app_of_sub_right (l l₁ l₂ : list T) : l ⊆ l₂ → l ⊆ l₁++l₂ := λ (s : l ⊆ l₂) (x : T) (xinl : x ∈ l), - have xinl₁ : x ∈ l₂, from s xinl, - mem_append_of_mem_or_mem (or.inr xinl₁) + have x ∈ l₂, from s xinl, + mem_append_of_mem_or_mem (or.inr this) theorem cons_sub_of_sub_of_mem {a : T} {l m : list T} : a ∈ m → l ⊆ m → a::l ⊆ m := λ (ainm : a ∈ m) (lsubm : l ⊆ m) (x : T) (xinal : x ∈ a::l), or.elim (eq_or_mem_of_mem_cons xinal) - (assume xeqa : x = a, by substvars; exact ainm) - (assume xinl : x ∈ l, lsubm xinl) + (suppose x = a, by substvars; exact ainm) + (suppose x ∈ l, lsubm this) theorem app_sub_of_sub_of_sub {l₁ l₂ l : list T} : l₁ ⊆ l → l₂ ⊆ l → l₁++l₂ ⊆ l := λ (l₁subl : l₁ ⊆ l) (l₂subl : l₂ ⊆ l) (x : T) (xinl₁l₂ : x ∈ l₁++l₂), or.elim (mem_or_mem_of_mem_append xinl₁l₂) - (λ xinl₁ : x ∈ l₁, l₁subl xinl₁) - (λ xinl₂ : x ∈ l₂, l₂subl xinl₂) + (suppose x ∈ l₁, l₁subl this) + (suppose x ∈ l₂, l₂subl this) /- find -/ section @@ -421,13 +420,13 @@ list.rec_on l (assume P₁ : ¬x ∈ [], _) (take y l, assume iH : ¬x ∈ l → find x l = length l, - assume P₁ : ¬x ∈ y::l, - have P₂ : ¬(x = y ∨ x ∈ l), from iff.elim_right (not_iff_not_of_iff !mem_cons_iff) P₁, - have P₃ : ¬x = y ∧ ¬x ∈ l, from (iff.elim_left not_or_iff_not_and_not P₂), + suppose ¬x ∈ y::l, + have ¬(x = y ∨ x ∈ l), from iff.elim_right (not_iff_not_of_iff !mem_cons_iff) this, + have ¬x = y ∧ ¬x ∈ l, from (iff.elim_left not_or_iff_not_and_not this), calc find x (y::l) = if x = y then 0 else succ (find x l) : !find_cons - ... = succ (find x l) : if_neg (and.elim_left P₃) - ... = succ (length l) : {iH (and.elim_right P₃)} + ... = succ (find x l) : if_neg (and.elim_left this) + ... = succ (length l) : {iH (and.elim_right this)} ... = length (y::l) : !length_cons⁻¹) lemma find_le_length : ∀ {a} {l : list T}, find a l ≤ length l @@ -476,8 +475,8 @@ theorem nth_eq_some : ∀ {l : list T} {n : nat}, n < length l → Σ a : T, nth | [] n h := absurd h !not_lt_zero | (a::l) 0 h := ⟨a, rfl⟩ | (a::l) (succ n) h := - have aux : n < length l, from lt_of_succ_lt_succ h, - obtain (r : T) (req : nth l n = some r), from nth_eq_some aux, + have n < length l, from lt_of_succ_lt_succ h, + obtain (r : T) (req : nth l n = some r), from nth_eq_some this, ⟨r, by rewrite [nth_succ, req]⟩ open decidable @@ -566,10 +565,10 @@ list.induction_on l exists.intro xs (qhead x xs), by rewrite aeqx; exact aux) (λ ainxs : a ∈ xs, - have ex : ∃l', xs ≈ a|l', from r ainxs, - obtain (l' : list A) (q : xs ≈ a|l'), from ex, - have q₂ : x::xs ≈ a | x::l', from qcons x q, - exists.intro (x::l') q₂)) + have ∃l', xs ≈ a|l', from r ainxs, + obtain (l' : list A) (q : xs ≈ a|l'), from this, + have x::xs ≈ a | x::l', from qcons x q, + exists.intro (x::l') this)) theorem qeq_split {a : A} {l l' : list A} : l'≈a|l → ∃l₁ l₂, l = l₁++l₂ ∧ l' = l₁++(a::l₂) := take q, qeq.induction_on q @@ -578,20 +577,20 @@ take q, qeq.induction_on q exists.intro [] (exists.intro t aux)) (λ b t t' q r, obtain (l₁ l₂ : list A) (h : t = l₁++l₂ ∧ t' = l₁++(a::l₂)), from r, - have aux : b::t = (b::l₁)++l₂ ∧ b::t' = (b::l₁)++(a::l₂), + have b::t = (b::l₁)++l₂ ∧ b::t' = (b::l₁)++(a::l₂), begin rewrite [and.elim_right h, and.elim_left h], constructor, repeat reflexivity end, - exists.intro (b::l₁) (exists.intro l₂ aux)) + exists.intro (b::l₁) (exists.intro l₂ this)) theorem sub_of_mem_of_sub_of_qeq {a : A} {l : list A} {u v : list A} : a ∉ l → a::l ⊆ v → v≈a|u → l ⊆ u := λ (nainl : a ∉ l) (s : a::l ⊆ v) (q : v≈a|u) (x : A) (xinl : x ∈ l), - have xinv : x ∈ v, from s (or.inr xinl), - have xinau : x ∈ a::u, from mem_cons_of_qeq q x xinv, - or.elim (eq_or_mem_of_mem_cons xinau) - (λ xeqa : x = a, by substvars; contradiction) - (λ xinu : x ∈ u, xinu) + have x ∈ v, from s (or.inr xinl), + have x ∈ a::u, from mem_cons_of_qeq q x this, + or.elim (eq_or_mem_of_mem_cons this) + (suppose x = a, by substvars; contradiction) + (suppose x ∈ u, this) end qeq end list diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 8ba0dc43a..bb0de5d87 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -64,13 +64,13 @@ theorem mem_perm {a : A} {l₁ l₂ : list A} : l₁ ~ l₂ → a ∈ l₁ → a assume p, perm.induction_on p (λ h, h) (λ x l₁ l₂ p₁ r₁ i, or.elim (eq_or_mem_of_mem_cons i) - (assume aeqx : a = x, by rewrite aeqx; apply !mem_cons) - (assume ainl₁ : a ∈ l₁, or.inr (r₁ ainl₁))) + (suppose a = x, by rewrite this; apply !mem_cons) + (suppose a ∈ l₁, or.inr (r₁ this))) (λ x y l ainyxl, or.elim (eq_or_mem_of_mem_cons ainyxl) - (assume aeqy : a = y, by rewrite aeqy; exact (or.inr !mem_cons)) - (assume ainxl : a ∈ x::l, or.elim (eq_or_mem_of_mem_cons ainxl) - (assume aeqx : a = x, or.inl aeqx) - (assume ainl : a ∈ l, or.inr (or.inr ainl)))) + (suppose a = y, by rewrite this; exact (or.inr !mem_cons)) + (suppose a ∈ x::l, or.elim (eq_or_mem_of_mem_cons this) + (suppose a = x, or.inl this) + (suppose a ∈ l, or.inr (or.inr this)))) (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂ ainl₁, r₂ (r₁ ainl₁)) theorem not_mem_perm {a : A} {l₁ l₂ : list A} : l₁ ~ l₂ → a ∉ l₁ → a ∉ l₂ := diff --git a/library/theories/number_theory/primes.lean b/library/theories/number_theory/primes.lean index 385d41291..47728c03f 100644 --- a/library/theories/number_theory/primes.lean +++ b/library/theories/number_theory/primes.lean @@ -31,7 +31,8 @@ definition decidable_prime [instance] (p : nat) : decidable (prime p) := decidable_of_decidable_of_iff _ (prime_ext_iff_prime p) lemma ge_two_of_prime {p : nat} : prime p → p ≥ 2 := -assume h, obtain h₁ h₂, from h, h₁ +suppose prime p, obtain h₁ h₂, from this, +h₁ theorem gt_one_of_prime {p : ℕ} (primep : prime p) : p > 1 := lt_of_succ_le (ge_two_of_prime primep) @@ -52,9 +53,9 @@ lemma prime_three : prime 3 := dec_trivial lemma pred_prime_pos {p : nat} : prime p → pred p > 0 := -assume h, -have h₁ : p ≥ 2, from ge_two_of_prime h, -lt_of_succ_le (pred_le_pred h₁) +suppose prime p, +have p ≥ 2, from ge_two_of_prime this, +show pred p > 0, from lt_of_succ_le (pred_le_pred this) lemma succ_pred_prime {p : nat} : prime p → succ (pred p) = p := assume h, succ_pred_of_pos (pos_of_prime h) @@ -127,8 +128,8 @@ obtain p (prime_p : prime p) (p_dvd_m1 : p ∣ m + 1), from sub_prime_and_dvd th 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 ≥ n, from by_contradiction - (assume h₁ : ¬ p ≥ n, - have p < n, from lt_of_not_ge h₁, + (suppose ¬ p ≥ n, + have p < n, from lt_of_not_ge this, 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, @@ -154,11 +155,11 @@ or_resolve_right H nc ▸ !gcd_dvd_right theorem coprime_of_prime_of_not_dvd {p n : ℕ} (primep : prime p) (npdvdn : ¬ p ∣ n) : coprime p n := -by_contradiction (assume nc : ¬ coprime p n, npdvdn (dvd_of_prime_of_not_coprime primep nc)) +by_contradiction (suppose ¬ coprime p n, npdvdn (dvd_of_prime_of_not_coprime primep this)) theorem not_dvd_of_prime_of_coprime {p n : ℕ} (primep : prime p) (cop : coprime p n) : ¬ p ∣ n := -assume pdvdn : p ∣ n, -have p ∣ gcd p n, from dvd_gcd !dvd.refl pdvdn, +suppose p ∣ n, +have p ∣ gcd p n, from dvd_gcd !dvd.refl this, 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 @@ -183,8 +184,8 @@ assume Hmn, Hm (dvd_of_prime_of_dvd_mul_right primep Hmn Hn) lemma dvd_or_dvd_of_prime_of_dvd_mul {p m n : nat} : prime p → p ∣ m * n → p ∣ m ∨ p ∣ n := λ h₁ h₂, by_cases - (assume h : p ∣ m, or.inl h) - (assume h : ¬ p ∣ m, or.inr (dvd_of_prime_of_dvd_mul_left h₁ h₂ h)) + (suppose p ∣ m, or.inl this) + (suppose ¬ p ∣ m, or.inr (dvd_of_prime_of_dvd_mul_left h₁ h₂ this)) lemma dvd_of_prime_of_dvd_pow {p m : nat} : ∀ {n}, prime p → p ∣ m^n → p ∣ m | 0 hp hd := diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index fce21c492..3c9a59a1a 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" "this" + "eval" "check" "end" "reveal" "this" "suppose" "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 9109b6a57..9f5f72bd7 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -446,6 +446,37 @@ static expr parse_assert(parser & p, unsigned, expr const *, pos_info const & po return parse_have_core(p, pos, none_expr(), true); } +static expr parse_suppose(parser & p, unsigned, expr const *, pos_info const & pos) { + auto id_pos = p.pos(); + name id; + expr prop; + if (p.curr_is_identifier()) { + id = p.get_name_val(); + p.next(); + if (p.curr_is_token(get_colon_tk())) { + p.next(); + prop = p.parse_expr(); + } else { + expr left = p.id_to_expr(id, id_pos); + id = get_this_tk(); + unsigned rbp = 0; + while (rbp < p.curr_expr_lbp()) { + left = p.parse_led(left); + } + prop = left; + } + } else { + id = get_this_tk(); + prop = p.parse_expr(); + } + p.check_token_next(get_comma_tk(), "invalid 'suppose', ',' expected"); + parser::local_scope scope(p); + expr l = p.save_pos(mk_local(id, prop), id_pos); + p.add_local(l); + expr body = p.parse_expr(); + return p.save_pos(Fun(l, body), pos); +} + static name * H_show = nullptr; static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) { expr prop = p.parse_expr(); @@ -630,6 +661,7 @@ parse_table init_nud_table() { r = r.add({transition("by+", mk_ext_action_core(parse_by_plus))}, x0); r = r.add({transition("have", mk_ext_action(parse_have))}, x0); r = r.add({transition("assert", mk_ext_action(parse_assert))}, x0); + r = r.add({transition("suppose", mk_ext_action(parse_suppose))}, x0); r = r.add({transition("show", mk_ext_action(parse_show))}, x0); r = r.add({transition("obtain", mk_ext_action(parse_obtain))}, x0); r = r.add({transition("abstract", mk_ext_action(parse_nested_declaration))}, x0); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index a3acf93e0..b70b294c0 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -88,7 +88,7 @@ static char const * g_decreasing_unicode = "↓"; void init_token_table(token_table & t) { pair builtin[] = - {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"assert", 0}, {"show", 0}, {"obtain", 0}, + {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"assert", 0}, {"suppose", 0}, {"show", 0}, {"obtain", 0}, {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"by+", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0}, {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec}, {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},