From 4e2377ddfcbde9efd8a734c70fd3f8bafe9dfe2f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Sep 2014 15:04:52 -0700 Subject: [PATCH] refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint. Signed-off-by: Leonardo de Moura --- library/data/bool.lean | 8 +++--- library/data/empty.lean | 2 +- library/data/int/basic.lean | 4 +-- library/data/list/basic.lean | 6 ++-- library/data/nat/basic.lean | 8 +++--- library/data/nat/order.lean | 4 +-- library/data/num.lean | 8 +++--- library/data/option.lean | 10 +++---- library/data/prod.lean | 8 +++--- library/data/sigma.lean | 6 ++-- library/data/string.lean | 4 +-- library/data/subtype.lean | 8 +++--- library/data/sum.lean | 10 +++---- library/data/unit.lean | 6 ++-- library/data/vector.lean | 8 +++--- library/hott/path.lean | 2 +- library/logic/core/decidable.lean | 4 +-- library/logic/core/inhabited.lean | 2 +- library/logic/core/nonempty.lean | 2 +- src/emacs/lean-syntax.el | 6 ++-- src/frontends/lean/decl_cmds.cpp | 45 ++++++++++++++++++++---------- src/frontends/lean/token_table.cpp | 4 +-- tests/lean/interactive/coe.lean | 2 +- tests/lean/protected.lean | 2 +- tests/lean/run/lift.lean | 2 +- tests/lean/run/protected.lean | 2 +- 26 files changed, 94 insertions(+), 79 deletions(-) diff --git a/library/data/bool.lean b/library/data/bool.lean index cb591d982..4a5da8215 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -10,10 +10,10 @@ inductive bool : Type := ff : bool, tt : bool namespace bool - definition rec_on [protected] {C : bool → Type} (b : bool) (H₁ : C ff) (H₂ : C tt) : C b := + protected definition rec_on {C : bool → Type} (b : bool) (H₁ : C ff) (H₂ : C tt) : C b := rec H₁ H₂ b - definition cases_on [protected] {p : bool → Prop} (b : bool) (H₁ : p ff) (H₂ : p tt) : p b := + protected definition cases_on {p : bool → Prop} (b : bool) (H₁ : p ff) (H₂ : p tt) : p b := rec H₁ H₂ b definition cond {A : Type} (b : bool) (t e : A) := @@ -135,10 +135,10 @@ namespace bool theorem bnot_true : !tt = ff := rfl - theorem is_inhabited [protected] [instance] : inhabited bool := + protected theorem is_inhabited [instance] : inhabited bool := inhabited.mk ff - theorem has_decidable_eq [protected] [instance] : decidable_eq bool := + protected theorem has_decidable_eq [instance] : decidable_eq bool := take a b : bool, rec_on a (rec_on b (inl rfl) (inr ff_ne_tt)) diff --git a/library/data/empty.lean b/library/data/empty.lean index 50f9299c1..9d096c1d4 100644 --- a/library/data/empty.lean +++ b/library/data/empty.lean @@ -10,7 +10,7 @@ import logic.core.cast inductive empty : Type namespace empty - theorem elim [protected] (A : Type) (H : empty) : A := + protected theorem elim (A : Type) (H : empty) : A := rec (λe, A) H end empty diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 7552eed47..b5dc681e5 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -184,7 +184,7 @@ representative_map_idempotent_equiv proj_rel @proj_congr a -- ## Definition of ℤ and basic theorems and definitions -opaque definition int [protected] := image proj +protected opaque definition int := image proj notation `ℤ` := int opaque definition psub : ℕ × ℕ → ℤ := fun_image proj @@ -203,7 +203,7 @@ exists_intro (pr1 (rep a)) a = psub (rep a) : (psub_rep a)⁻¹ ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod_ext (rep a))⁻¹})) -theorem has_decidable_eq [instance] [protected] : decidable_eq ℤ := +protected theorem has_decidable_eq [instance] : decidable_eq ℤ := take a b : ℤ, _ reducible [off] int diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index f9c2f13e8..0ebc0b79f 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -29,15 +29,15 @@ section variable {T : Type} -theorem induction_on [protected] {P : list T → Prop} (l : list T) (Hnil : P nil) +protected theorem induction_on {P : list T → Prop} (l : list T) (Hnil : P nil) (Hind : ∀ (x : T) (l : list T), P l → P (x::l)) : P l := rec Hnil Hind l -theorem cases_on [protected] {P : list T → Prop} (l : list T) (Hnil : P nil) +protected theorem cases_on {P : list T → Prop} (l : list T) (Hnil : P nil) (Hcons : ∀ (x : T) (l : list T), P (x::l)) : P l := induction_on l Hnil (take x l IH, Hcons x l) -definition rec_on [protected] {A : Type} {C : list A → Type} (l : list A) +protected definition rec_on {A : Type} {C : list A → Type} (l : list A) (H1 : C nil) (H2 : Π (h : A) (t : list A), C t → C (h::t)) : C l := rec H1 H2 l diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index c77a97b79..269a87721 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -30,14 +30,14 @@ theorem rec_zero {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) theorem rec_succ {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) (n : ℕ) : nat.rec x f (succ n) = f n (nat.rec x f n) -theorem induction_on [protected] {P : ℕ → Prop} (a : ℕ) (H1 : P zero) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) : +protected theorem induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P zero) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) : P a := nat.rec H1 H2 a -definition rec_on [protected] {P : ℕ → Type} (n : ℕ) (H1 : P zero) (H2 : ∀m, P m → P (succ m)) : P n := +protected definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P zero) (H2 : ∀m, P m → P (succ m)) : P n := nat.rec H1 H2 n -theorem is_inhabited [protected] [instance] : inhabited nat := +protected theorem is_inhabited [instance] : inhabited nat := inhabited.mk zero -- Coercion from num @@ -105,7 +105,7 @@ induction_on n absurd H ne) (take k IH H, IH (succ_inj H)) -theorem has_decidable_eq [instance] [protected] : decidable_eq ℕ := +protected theorem has_decidable_eq [instance] : decidable_eq ℕ := take n m : ℕ, have general : ∀n, decidable (n = m), from rec_on m diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index e4010a0c5..111308b6d 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -430,7 +430,7 @@ theorem ge_decidable [instance] (n m : ℕ) : decidable (n ≥ m) -- ### misc -theorem strong_induction_on [protected] {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n := +protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n := have H1 : ∀ {n m : nat}, m < n → P m, from take n, induction_on n @@ -446,7 +446,7 @@ have H1 : ∀ {n m : nat}, m < n → P m, from (assume H4: m = n', H4⁻¹ ▸ H2)), H1 self_lt_succ -theorem case_strong_induction_on [protected] {P : nat → Prop} (a : nat) (H0 : P 0) +protected theorem case_strong_induction_on {P : nat → Prop} (a : nat) (H0 : P 0) (Hind : ∀(n : nat), (∀m, m ≤ n → P m) → P (succ n)) : P a := strong_induction_on a ( take n, diff --git a/library/data/num.lean b/library/data/num.lean index ab22b99d8..87c7cf54e 100644 --- a/library/data/num.lean +++ b/library/data/num.lean @@ -18,11 +18,11 @@ theorem pos_num.is_inhabited [instance] : inhabited pos_num := inhabited.mk pos_num.one namespace pos_num - theorem induction_on [protected] {P : pos_num → Prop} (a : pos_num) + protected theorem induction_on {P : pos_num → Prop} (a : pos_num) (H₁ : P one) (H₂ : ∀ (n : pos_num), P n → P (bit1 n)) (H₃ : ∀ (n : pos_num), P n → P (bit0 n)) : P a := rec H₁ H₂ H₃ a - definition rec_on [protected] {P : pos_num → Type} (a : pos_num) + protected definition rec_on {P : pos_num → Type} (a : pos_num) (H₁ : P one) (H₂ : ∀ (n : pos_num), P n → P (bit1 n)) (H₃ : ∀ (n : pos_num), P n → P (bit0 n)) : P a := rec H₁ H₂ H₃ a @@ -125,11 +125,11 @@ inhabited.mk num.zero namespace num open pos_num - theorem induction_on [protected] {P : num → Prop} (a : num) + protected theorem induction_on {P : num → Prop} (a : num) (H₁ : P zero) (H₂ : ∀ (p : pos_num), P (pos p)) : P a := rec H₁ H₂ a - definition rec_on [protected] {P : num → Type} (a : num) + protected definition rec_on {P : num → Type} (a : num) (H₁ : P zero) (H₂ : ∀ (p : pos_num), P (pos p)) : P a := rec H₁ H₂ a diff --git a/library/data/option.lean b/library/data/option.lean index 9dee13c03..5857b7459 100644 --- a/library/data/option.lean +++ b/library/data/option.lean @@ -10,11 +10,11 @@ inductive option (A : Type) : Type := some : A → option A namespace option - theorem induction_on [protected] {A : Type} {p : option A → Prop} (o : option A) + protected theorem induction_on {A : Type} {p : option A → Prop} (o : option A) (H1 : p none) (H2 : ∀a, p (some a)) : p o := rec H1 H2 o - definition rec_on [protected] {A : Type} {C : option A → Type} (o : option A) + protected definition rec_on {A : Type} {C : option A → Type} (o : option A) (H1 : C none) (H2 : ∀a, C (some a)) : C o := rec H1 H2 o @@ -32,13 +32,13 @@ namespace option (H ▸ is_none_none) (not_is_none_some a) - theorem equal [protected] {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ := + protected theorem equal {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ := congr_arg (option.rec a₁ (λ a, a)) H - theorem is_inhabited [protected] [instance] (A : Type) : inhabited (option A) := + protected theorem is_inhabited [instance] (A : Type) : inhabited (option A) := inhabited.mk none - theorem has_decidable_eq [protected] [instance] {A : Type} (H : decidable_eq A) : decidable_eq (option A) := + protected theorem has_decidable_eq [instance] {A : Type} (H : decidable_eq A) : decidable_eq (option A) := take o₁ o₂ : option A, rec_on o₁ (rec_on o₂ (inl rfl) (take a₂, (inr (none_ne_some a₂)))) diff --git a/library/data/prod.lean b/library/data/prod.lean index 466ee2378..d8d41cd9d 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -31,7 +31,7 @@ section theorem pr2_pair (a : A) (b : B) : pr2 (a, b) = b := rfl - theorem destruct [protected] {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p := + protected theorem destruct {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p := rec H p theorem prod_ext (p : prod A B) : pair (pr1 p) (pr2 p) = p := @@ -42,13 +42,13 @@ section theorem pair_eq {a1 a2 : A} {b1 b2 : B} (H1 : a1 = a2) (H2 : b1 = b2) : (a1, b1) = (a2, b2) := H1 ▸ H2 ▸ rfl - theorem equal [protected] {p1 p2 : prod A B} : ∀ (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2), p1 = p2 := + protected theorem equal {p1 p2 : prod A B} : ∀ (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2), p1 = p2 := destruct p1 (take a1 b1, destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2)) - theorem is_inhabited [protected] [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) := + protected theorem is_inhabited [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) := inhabited.destruct H1 (λa, inhabited.destruct H2 (λb, inhabited.mk (pair a b))) - theorem has_decidable_eq [protected] [instance] (H1 : decidable_eq A) (H2 : decidable_eq B) : decidable_eq (A × B) := + protected theorem has_decidable_eq [instance] (H1 : decidable_eq A) (H2 : decidable_eq B) : decidable_eq (A × B) := take u v : A × B, have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from iff.intro diff --git a/library/data/sigma.lean b/library/data/sigma.lean index 7846a7abf..b5707aafa 100644 --- a/library/data/sigma.lean +++ b/library/data/sigma.lean @@ -19,7 +19,7 @@ section theorem dpr1_dpair (a : A) (b : B a) : dpr1 (dpair a b) = a := rfl theorem dpr2_dpair (a : A) (b : B a) : dpr2 (dpair a b) = b := rfl - theorem destruct [protected] {P : sigma B → Prop} (p : sigma B) (H : ∀a b, P (dpair a b)) : P p := + protected theorem destruct {P : sigma B → Prop} (p : sigma B) (H : ∀a b, P (dpair a b)) : P p := rec H p theorem dpair_ext (p : sigma B) : dpair (dpr1 p) (dpr2 p) = p := @@ -34,11 +34,11 @@ section ... = dpair a₁ b₂ : {H₂}) b₂ H₁ H₂ - theorem equal [protected] {p₁ p₂ : Σx : A, B x} : + protected theorem equal {p₁ p₂ : Σx : A, B x} : ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : eq.rec_on H₁ (dpr2 p₁) = (dpr2 p₂)), p₁ = p₂ := destruct p₁ (take a₁ b₁, destruct p₂ (take a₂ b₂ H₁ H₂, dpair_eq H₁ H₂)) - theorem is_inhabited [protected] [instance] (H₁ : inhabited A) (H₂ : inhabited (B (default A))) : + protected theorem is_inhabited [instance] (H₁ : inhabited A) (H₂ : inhabited (B (default A))) : inhabited (sigma B) := inhabited.destruct H₁ (λa, inhabited.destruct H₂ (λb, inhabited.mk (dpair (default A) b))) end diff --git a/library/data/string.lean b/library/data/string.lean index 6f91b363e..d811a48ab 100644 --- a/library/data/string.lean +++ b/library/data/string.lean @@ -10,7 +10,7 @@ inductive char : Type := mk : bool → bool → bool → bool → bool → bool → bool → bool → char namespace char - theorem is_inhabited [protected] [instance] : inhabited char := + protected theorem is_inhabited [instance] : inhabited char := inhabited.mk (mk ff ff ff ff ff ff ff ff) end char @@ -19,6 +19,6 @@ inductive string : Type := str : char → string → string namespace string - theorem is_inhabited [protected] [instance] : inhabited string := + protected theorem is_inhabited [instance] : inhabited string := inhabited.mk empty end string diff --git a/library/data/subtype.lean b/library/data/subtype.lean index 9e3b25d61..c462e789b 100644 --- a/library/data/subtype.lean +++ b/library/data/subtype.lean @@ -22,7 +22,7 @@ section theorem elt_of_tag (a : A) (H : P a) : elt_of (tag a H) = a := rfl - theorem destruct [protected] {Q : {x, P x} → Prop} (a : {x, P x}) + protected theorem destruct {Q : {x, P x} → Prop} (a : {x, P x}) (H : ∀(x : A) (H1 : P x), Q (tag x H1)) : Q a := rec H a @@ -35,13 +35,13 @@ section theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 := eq.subst H3 (take H2, tag_irrelevant H1 H2) H2 - theorem equal [protected] {a1 a2 : {x, P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 := + protected theorem equal {a1 a2 : {x, P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 := destruct a1 (take x1 H1, destruct a2 (take x2 H2 H, tag_eq H)) - theorem is_inhabited [protected] [instance] {a : A} (H : P a) : inhabited {x, P x} := + protected theorem is_inhabited [instance] {a : A} (H : P a) : inhabited {x, P x} := inhabited.mk (tag a H) - theorem has_decidable_eq [protected] [instance] (H : decidable_eq A) : decidable_eq {x, P x} := + protected theorem has_decidable_eq [instance] (H : decidable_eq A) : decidable_eq {x, P x} := take a1 a2 : {x, P x}, have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from iff.intro (assume H, eq.subst H rfl) (assume H, equal H), diff --git a/library/data/sum.lean b/library/data/sum.lean index 28b6ff9b5..9db6904a1 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -17,11 +17,11 @@ namespace sum infixr `+`:25 := sum -- conflicts with notation for addition end extra_notation - definition rec_on [protected] {A B : Type} {C : (A ⊎ B) → Type} (s : A ⊎ B) + protected definition rec_on {A B : Type} {C : (A ⊎ B) → Type} (s : A ⊎ B) (H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s := rec H1 H2 s - definition cases_on [protected] {A B : Type} {P : (A ⊎ B) → Prop} (s : A ⊎ B) + protected definition cases_on {A B : Type} {P : (A ⊎ B) → Prop} (s : A ⊎ B) (H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s := rec H1 H2 s @@ -49,13 +49,13 @@ namespace sum have H2 : f (inr A b2), from H ▸ H1, H2 - theorem is_inhabited_left [protected] [instance] {A B : Type} (H : inhabited A) : inhabited (A ⊎ B) := + protected theorem is_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A ⊎ B) := inhabited.mk (inl B (default A)) - theorem is_inhabited_right [protected] [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) := + protected theorem is_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) := inhabited.mk (inr A (default B)) - theorem has_eq_decidable [protected] [instance] {A B : Type} (H1 : decidable_eq A) (H2 : decidable_eq B) : + protected theorem has_eq_decidable [instance] {A B : Type} (H1 : decidable_eq A) (H2 : decidable_eq B) : decidable_eq (A ⊎ B) := take s1 s2 : A ⊎ B, rec_on s1 diff --git a/library/data/unit.lean b/library/data/unit.lean index 532b1349c..36a1289a8 100644 --- a/library/data/unit.lean +++ b/library/data/unit.lean @@ -9,15 +9,15 @@ inductive unit : Type := namespace unit notation `⋆`:max := star - theorem equal [protected] (a b : unit) : a = b := + protected theorem equal (a b : unit) : a = b := rec (rec rfl b) a theorem eq_star (a : unit) : a = star := equal a star - theorem is_inhabited [protected] [instance] : inhabited unit := + protected theorem is_inhabited [instance] : inhabited unit := inhabited.mk ⋆ - theorem has_decidable_eq [protected] [instance] : decidable_eq unit := + protected theorem has_decidable_eq [instance] : decidable_eq unit := take (a b : unit), inl (equal a b) end unit diff --git a/library/data/vector.lean b/library/data/vector.lean index f975f42ae..21fe433d2 100644 --- a/library/data/vector.lean +++ b/library/data/vector.lean @@ -15,19 +15,19 @@ namespace vec section sc_vec variable {T : Type} - theorem rec_on [protected] {C : ∀ (n : ℕ), vec T n → Type} {n : ℕ} (v : vec T n) (Hnil : C 0 nil) + protected theorem rec_on {C : ∀ (n : ℕ), vec T n → Type} {n : ℕ} (v : vec T n) (Hnil : C 0 nil) (Hcons : ∀(x : T) {n : ℕ} (w : vec T n), C n w → C (succ n) (cons x w)) : C n v := rec Hnil Hcons v - theorem induction_on [protected] {C : ∀ (n : ℕ), vec T n → Prop} {n : ℕ} (v : vec T n) (Hnil : C 0 nil) + protected theorem induction_on {C : ∀ (n : ℕ), vec T n → Prop} {n : ℕ} (v : vec T n) (Hnil : C 0 nil) (Hcons : ∀(x : T) {n : ℕ} (w : vec T n), C n w → C (succ n) (cons x w)) : C n v := rec_on v Hnil Hcons - theorem case_on [protected] {C : ∀ (n : ℕ), vec T n → Type} {n : ℕ} (v : vec T n) (Hnil : C 0 nil) + protected theorem case_on {C : ∀ (n : ℕ), vec T n → Type} {n : ℕ} (v : vec T n) (Hnil : C 0 nil) (Hcons : ∀(x : T) {n : ℕ} (w : vec T n), C (succ n) (cons x w)) : C n v := rec_on v Hnil (take x n v IH, Hcons x v) - theorem is_inhabited [instance] [protected] (A : Type) (H : inhabited A) (n : nat) : inhabited (vec A n) := + protected theorem is_inhabited [instance] (A : Type) (H : inhabited A) (n : nat) : inhabited (vec A n) := nat.rec_on n (inhabited.mk (@vec.nil A)) (λ (n : nat) (iH : inhabited (vec A n)), diff --git a/library/hott/path.lean b/library/hott/path.lean index f058147a2..e0e5ea636 100644 --- a/library/hott/path.lean +++ b/library/hott/path.lean @@ -23,7 +23,7 @@ infix `≈` := path notation x `≈` y:50 `:>`:0 A:0 := @path A x y -- TODO: is this right? definition idp {A : Type} {a : A} := idpath a -definition induction_on [protected] {A : Type} {a b : A} (p : a ≈ b) +protected definition induction_on {A : Type} {a b : A} (p : a ≈ b) {C : Π (b : A) (p : a ≈ b), Type} (H : C a (idpath a)) : C b p := path.rec H p diff --git a/library/logic/core/decidable.lean b/library/logic/core/decidable.lean index 54d5c211b..876ec1eba 100644 --- a/library/logic/core/decidable.lean +++ b/library/logic/core/decidable.lean @@ -16,10 +16,10 @@ inl trivial theorem false_decidable [instance] : decidable false := inr not_false_trivial -theorem induction_on [protected] {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C := +protected theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C := decidable.rec H1 H2 H -definition rec_on [protected] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : +protected definition rec_on {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C := decidable.rec H1 H2 H diff --git a/library/logic/core/inhabited.lean b/library/logic/core/inhabited.lean index 71b78669b..f03db1ec3 100644 --- a/library/logic/core/inhabited.lean +++ b/library/logic/core/inhabited.lean @@ -9,7 +9,7 @@ mk : A → inhabited A namespace inhabited -definition destruct [protected] {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B := +protected definition destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B := inhabited.rec H2 H1 definition Prop_inhabited [instance] : inhabited Prop := diff --git a/library/logic/core/nonempty.lean b/library/logic/core/nonempty.lean index 9a08cf9ad..f787b7c16 100644 --- a/library/logic/core/nonempty.lean +++ b/library/logic/core/nonempty.lean @@ -8,7 +8,7 @@ inductive nonempty (A : Type) : Prop := intro : A → nonempty A namespace nonempty - definition elim [protected] {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B := + protected definition elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B := rec H2 H1 theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A := diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 8280d323a..93ad60f83 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -8,7 +8,7 @@ (require 'rx) (defconst lean-keywords - '("import" "reducible" "tactic_hint" "private" "opaque" "definition" "renaming" + '("import" "reducible" "tactic_hint" "protected" "private" "opaque" "definition" "renaming" "inline" "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment" @@ -70,8 +70,8 @@ ;; place holder (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face) ;; modifiers - (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[protected\]" - "\[instance\]" "\[class\]" "\[coercion\]" "\[off\]" "\[none\]" "\[on\]")) . 'font-lock-doc-face) + (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" + "\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]")) . 'font-lock-doc-face) ;; tactics (,(rx symbol-start (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "back" "beta" "done" "exact" "repeat") diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index d4d2e9c8a..b0be86a2e 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -28,7 +28,7 @@ static name g_colon(":"); static name g_assign(":="); static name g_definition("definition"); static name g_theorem("theorem"); -static name g_protected("[protected]"); +static name g_opaque("opaque"); static name g_instance("[instance]"); static name g_coercion("[coercion]"); static name g_reducible("[reducible]"); @@ -162,12 +162,10 @@ environment axiom_cmd(parser & p) { } struct decl_modifiers { - bool m_is_protected; bool m_is_instance; bool m_is_coercion; bool m_is_reducible; decl_modifiers() { - m_is_protected = false; m_is_instance = false; m_is_coercion = false; m_is_reducible = false; @@ -175,10 +173,7 @@ struct decl_modifiers { void parse(parser & p) { while (true) { - if (p.curr_is_token(g_protected)) { - m_is_protected = true; - p.next(); - } else if (p.curr_is_token(g_instance)) { + if (p.curr_is_token(g_instance)) { m_is_instance = true; p.next(); } else if (p.curr_is_token(g_coercion)) { @@ -204,14 +199,15 @@ static void erase_local_binder_info(buffer & ps) { p = update_local(p, binder_info()); } -environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, bool is_private) { +environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, bool is_private, bool is_protected) { + lean_assert(!(is_theorem && !is_opaque)); + lean_assert(!(is_private && !is_opaque)); + lean_assert(!(is_private && is_protected)); auto n_pos = p.pos(); unsigned start_line = n_pos.first; name n = p.check_id_next("invalid declaration, identifier expected"); decl_modifiers modifiers; name real_n; // real name for this declaration - if (is_theorem) - is_opaque = true; buffer ls_buffer; expr type, value; level_param_names ls; @@ -353,21 +349,21 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo env = add_instance(env, real_n); if (modifiers.m_is_coercion) env = add_coercion(env, real_n, p.ios()); - if (modifiers.m_is_protected) + if (is_protected) env = add_protected(env, real_n); if (modifiers.m_is_reducible) env = set_reducible(env, real_n, reducible_status::On); return env; } environment definition_cmd(parser & p) { - return definition_cmd_core(p, false, false, false); + return definition_cmd_core(p, false, false, false, false); } environment opaque_definition_cmd(parser & p) { p.check_token_next(g_definition, "invalid 'opaque' definition, 'definition' expected"); - return definition_cmd_core(p, false, true, false); + return definition_cmd_core(p, false, true, false, false); } environment theorem_cmd(parser & p) { - return definition_cmd_core(p, true, true, false); + return definition_cmd_core(p, true, true, false, false); } environment private_definition_cmd(parser & p) { bool is_theorem = false; @@ -379,7 +375,25 @@ environment private_definition_cmd(parser & p) { } else { throw parser_error("invalid 'private' definition/theorem, 'definition' or 'theorem' expected", p.pos()); } - return definition_cmd_core(p, is_theorem, true, true); + return definition_cmd_core(p, is_theorem, true, true, false); +} +environment protected_definition_cmd(parser & p) { + bool is_theorem = false; + bool is_opaque = false; + if (p.curr_is_token_or_id(g_opaque)) { + is_opaque = true; + p.next(); + p.check_token_next(g_definition, "invalid 'protected' definition, 'definition' expected"); + } else if (p.curr_is_token_or_id(g_definition)) { + p.next(); + } else if (p.curr_is_token_or_id(g_theorem)) { + p.next(); + is_theorem = true; + is_opaque = true; + } else { + throw parser_error("invalid 'protected' definition/theorem, 'definition' or 'theorem' expected", p.pos()); + } + return definition_cmd_core(p, is_theorem, is_opaque, false, true); } static name g_lparen("("), g_lcurly("{"), g_ldcurly("⦃"), g_lbracket("["); @@ -426,6 +440,7 @@ void register_decl_cmds(cmd_table & r) { add_cmd(r, cmd_info("definition", "add new definition", definition_cmd)); add_cmd(r, cmd_info("opaque", "add new opaque definition", opaque_definition_cmd)); add_cmd(r, cmd_info("private", "add new private definition/theorem", private_definition_cmd)); + add_cmd(r, cmd_info("protected", "add new protected definition/theorem", protected_definition_cmd)); add_cmd(r, cmd_info("theorem", "add new theorem", theorem_cmd)); add_cmd(r, cmd_info("variables", "declare new parameters", variables_cmd)); } diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 92f9a229d..a8e890012 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -77,8 +77,8 @@ token_table init_token_table() { {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}}; - char const * commands[] = {"theorem", "axiom", "variable", "private", "opaque", "definition", "coercion", - "variables", "[persistent]", "[protected]", "[visible]", "[instance]", + char const * commands[] = {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion", + "variables", "[persistent]", "[visible]", "[instance]", "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "reducible", "evaluate", "check", "print", "end", "namespace", "section", "import", "inductive", "record", "renaming", "extends", "structure", "module", "universe", diff --git a/tests/lean/interactive/coe.lean b/tests/lean/interactive/coe.lean index b7fe820ef..901f969c7 100644 --- a/tests/lean/interactive/coe.lean +++ b/tests/lean/interactive/coe.lean @@ -1,7 +1,7 @@ import data.int open int -theorem has_decidable_eq [instance] [protected] : decidable_eq ℤ := +protected theorem has_decidable_eq [instance] : decidable_eq ℤ := take (a b : ℤ), _ variable n : nat diff --git a/tests/lean/protected.lean b/tests/lean/protected.lean index edc1d14d6..746f4d5c0 100644 --- a/tests/lean/protected.lean +++ b/tests/lean/protected.lean @@ -1,7 +1,7 @@ import logic namespace foo - definition C [protected] := true + protected definition C := true definition D := true end foo diff --git a/tests/lean/run/lift.lean b/tests/lean/run/lift.lean index b258fcb40..edbdc9006 100644 --- a/tests/lean/run/lift.lean +++ b/tests/lean/run/lift.lean @@ -11,7 +11,7 @@ rec (λ a, a) a theorem down_up {A : Type} (a : A) : down (up a) = a := rfl -theorem induction_on [protected] {A : Type} {P : lift A → Prop} (a : lift A) (H : ∀ (a : A), P (up a)) : P a := +protected theorem induction_on {A : Type} {P : lift A → Prop} (a : lift A) (H : ∀ (a : A), P (up a)) : P a := rec H a theorem up_down {A : Type} (a' : lift A) : up (down a') = a' := diff --git a/tests/lean/run/protected.lean b/tests/lean/run/protected.lean index 72457ab52..2c0033dc1 100644 --- a/tests/lean/run/protected.lean +++ b/tests/lean/run/protected.lean @@ -1,7 +1,7 @@ import logic namespace foo - definition C [protected] := true + protected definition C := true definition D := true end foo