From e513b0ead489d47fc63b8fb2070e0bf20baa3111 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Wed, 25 Feb 2015 15:34:49 -0500 Subject: [PATCH] refactor(library,hott): rename theorems for decidable and inhabited The convention is this: we use e.g. nat.is_inhabited and nat.has_decidable_eq for these two purposes only, to avoid clashing with "inhabited" and "decidable_eq" in a namespace. Otherwise, we use "decidable_foo" and "inhabited_foo". --- hott/init/logic.hlean | 18 +++++++++--------- hott/init/nat.hlean | 4 ++-- library/data/bool.lean | 4 ++-- library/data/list/basic.lean | 2 +- library/data/sum.lean | 10 +++++----- library/init/logic.lean | 20 ++++++++++---------- library/init/nat.lean | 4 ++-- library/logic/identities.lean | 2 +- 8 files changed, 32 insertions(+), 32 deletions(-) diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index 4f19082321..f0e3091d0c 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -185,10 +185,10 @@ namespace inhabited protected definition destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B := inhabited.rec H2 H1 -definition fun_inhabited [instance] (A : Type) {B : Type} [H : inhabited B] : inhabited (A → B) := +definition inhabited_fun [instance] (A : Type) {B : Type} [H : inhabited B] : inhabited (A → B) := destruct H (λb, mk (λa, b)) -definition dfun_inhabited [instance] (A : Type) {B : A → Type} [H : Πx, inhabited (B x)] : +definition inhabited_Pi [instance] (A : Type) {B : A → Type} [H : Πx, inhabited (B x)] : inhabited (Πx, B x) := mk (λa, destruct (H a) (λb, b)) @@ -235,39 +235,39 @@ section variables {p q : Type} open decidable (rec_on inl inr) - definition unit.decidable [instance] : decidable unit := + definition decidable_unit [instance] : decidable unit := inl unit.star - definition empty.decidable [instance] : decidable empty := + definition decidable_empty [instance] : decidable empty := inr not_empty - definition prod.decidable [instance] [Hp : decidable p] [Hq : decidable q] : decidable (prod p q) := + definition decidable_prod [instance] [Hp : decidable p] [Hq : decidable q] : decidable (prod p q) := rec_on Hp (assume Hp : p, rec_on Hq (assume Hq : q, inl (prod.mk Hp Hq)) (assume Hnq : ¬q, inr (λ H : prod p q, prod.rec_on H (λ Hp Hq, absurd Hq Hnq)))) (assume Hnp : ¬p, inr (λ H : prod p q, prod.rec_on H (λ Hp Hq, absurd Hp Hnp))) - definition sum.decidable [instance] [Hp : decidable p] [Hq : decidable q] : decidable (sum p q) := + definition decidable_sum [instance] [Hp : decidable p] [Hq : decidable q] : decidable (sum p q) := rec_on Hp (assume Hp : p, inl (sum.inl Hp)) (assume Hnp : ¬p, rec_on Hq (assume Hq : q, inl (sum.inr Hq)) (assume Hnq : ¬q, inr (λ H : sum p q, sum.rec_on H (λ Hp, absurd Hp Hnp) (λ Hq, absurd Hq Hnq)))) - definition not.decidable [instance] [Hp : decidable p] : decidable (¬p) := + definition decidable_not [instance] [Hp : decidable p] : decidable (¬p) := rec_on Hp (assume Hp, inr (not_not_intro Hp)) (assume Hnp, inl Hnp) - definition implies.decidable [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p → q) := + definition decidable_implies [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p → q) := rec_on Hp (assume Hp : p, rec_on Hq (assume Hq : q, inl (assume H, Hq)) (assume Hnq : ¬q, inr (assume H : p → q, absurd (H Hp) Hnq))) (assume Hnp : ¬p, inl (assume Hp, absurd Hp Hnp)) - definition iff.decidable [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ↔ q) := + definition decidable_if [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ↔ q) := show decidable (prod (p → q) (q → p)), from _ end diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean index 81d9683b71..a1c3572518 100644 --- a/hott/init/nat.hlean +++ b/hott/init/nat.hlean @@ -114,7 +114,7 @@ namespace nat lt.of_succ_lt hlt), aux - definition lt.is_decidable_rel [instance] : decidable_rel lt := + definition decidable_lt [instance] : decidable_rel lt := λ a b, nat.rec_on b (λ (a : nat), inr (not_lt_zero a)) (λ (b₁ : nat) (ih : ∀ a, decidable (a < b₁)) (a : nat), nat.cases_on a @@ -145,7 +145,7 @@ namespace nat (λ hl, eq.rec_on hl !le.refl) (λ hr, le.of_lt hr) - definition le.is_decidable_rel [instance] : decidable_rel le := + definition decidable_le [instance] : decidable_rel le := λ a b, decidable_iff_equiv _ (iff.intro le.of_eq_or_lt eq_or_lt_of_le) definition le.rec_on {a : nat} {P : nat → Type} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : ∀ b, a < b → P b) : P b := diff --git a/library/data/bool.lean b/library/data/bool.lean index 1e564097af..1088d32666 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -120,10 +120,10 @@ end bool open bool -protected definition bool.inhabited [instance] : inhabited bool := +protected definition bool.is_inhabited [instance] : inhabited bool := inhabited.mk ff -protected definition bool.decidable_eq [instance] : decidable_eq bool := +protected definition bool.has_decidable_eq [instance] : decidable_eq bool := take a b : bool, bool.rec_on a (bool.rec_on b (inl rfl) (inr ff_ne_tt)) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index e37331715b..c3cbb2faeb 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -215,7 +215,7 @@ list.induction_on l from H3 ▸ rfl, !exists.intro (!exists.intro H4))) -definition mem.is_decidable [instance] [H : decidable_eq T] (x : T) (l : list T) : decidable (x ∈ l) := +definition decidable_mem [instance] [H : decidable_eq T] (x : T) (l : list T) : decidable (x ∈ l) := list.rec_on l (decidable.inr (not_of_iff_false !mem_nil)) (take (h : T) (l : list T) (iH : decidable (x ∈ l)), diff --git a/library/data/sum.lean b/library/data/sum.lean index 686b4c47f9..17488a057e 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -39,15 +39,15 @@ namespace sum protected definition is_inhabited_right [instance] [h : inhabited B] : inhabited (A + B) := inhabited.mk (inr (default B)) - protected definition has_eq_decidable [instance] [h₁ : decidable_eq A] [h₂ : decidable_eq B] : ∀ s₁ s₂ : A + B, decidable (s₁ = s₂), - has_eq_decidable (inl a₁) (inl a₂) := + protected definition has_decidable_eq [instance] [h₁ : decidable_eq A] [h₂ : decidable_eq B] : ∀ s₁ s₂ : A + B, decidable (s₁ = s₂), + has_decidable_eq (inl a₁) (inl a₂) := match h₁ a₁ a₂ with decidable.inl hp := decidable.inl (hp ▸ rfl), decidable.inr hn := decidable.inr (λ he, absurd (inl_inj he) hn) end, - has_eq_decidable (inl a₁) (inr b₂) := decidable.inr (λ e, sum.no_confusion e), - has_eq_decidable (inr b₁) (inl a₂) := decidable.inr (λ e, sum.no_confusion e), - has_eq_decidable (inr b₁) (inr b₂) := + has_decidable_eq (inl a₁) (inr b₂) := decidable.inr (λ e, sum.no_confusion e), + has_decidable_eq (inr b₁) (inl a₂) := decidable.inr (λ e, sum.no_confusion e), + has_decidable_eq (inr b₁) (inr b₂) := match h₂ b₁ b₂ with decidable.inl hp := decidable.inl (hp ▸ rfl), decidable.inr hn := decidable.inr (λ he, absurd (inr_inj he) hn) diff --git a/library/init/logic.lean b/library/init/logic.lean index 083b843b52..b2cf2b005a 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -244,10 +244,10 @@ inductive decidable [class] (p : Prop) : Type := inl : p → decidable p, inr : ¬p → decidable p -definition true.decidable [instance] : decidable true := +definition decidable_true [instance] : decidable true := decidable.inl trivial -definition false.decidable [instance] : decidable false := +definition decidable_false [instance] : decidable false := decidable.inr not_false namespace decidable @@ -289,33 +289,33 @@ section variables {p q : Prop} open decidable (rec_on inl inr) - definition and.decidable [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ∧ q) := + definition decidable_and [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ∧ q) := rec_on Hp (assume Hp : p, rec_on Hq (assume Hq : q, inl (and.intro Hp Hq)) (assume Hnq : ¬q, inr (assume H : p ∧ q, and.rec_on H (assume Hp Hq, absurd Hq Hnq)))) (assume Hnp : ¬p, inr (assume H : p ∧ q, and.rec_on H (assume Hp Hq, absurd Hp Hnp))) - definition or.decidable [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ∨ q) := + definition decidable_or [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ∨ q) := rec_on Hp (assume Hp : p, inl (or.inl Hp)) (assume Hnp : ¬p, rec_on Hq (assume Hq : q, inl (or.inr Hq)) (assume Hnq : ¬q, inr (assume H : p ∨ q, or.elim H (assume Hp, absurd Hp Hnp) (assume Hq, absurd Hq Hnq)))) - definition not.decidable [instance] [Hp : decidable p] : decidable (¬p) := + definition decidable_not [instance] [Hp : decidable p] : decidable (¬p) := rec_on Hp (assume Hp, inr (λ Hnp, absurd Hp Hnp)) (assume Hnp, inl Hnp) - definition implies.decidable [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p → q) := + definition decidable_implies [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p → q) := rec_on Hp (assume Hp : p, rec_on Hq (assume Hq : q, inl (assume H, Hq)) (assume Hnq : ¬q, inr (assume H : p → q, absurd (H Hp) Hnq))) (assume Hnp : ¬p, inl (assume Hp, absurd Hp Hnp)) - definition iff.decidable [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ↔ q) := + definition decidable_iff [instance] [Hp : decidable p] [Hq : decidable q] : decidable (p ↔ q) := show decidable ((p → q) ∧ (q → p)), from _ end @@ -341,13 +341,13 @@ inhabited.rec (λa, a) H opaque definition arbitrary (A : Type) [H : inhabited A] : A := inhabited.rec (λa, a) H -definition Prop_inhabited [instance] : inhabited Prop := +definition Prop.is_inhabited [instance] : inhabited Prop := inhabited.mk true -definition fun_inhabited [instance] (A : Type) {B : Type} [H : inhabited B] : inhabited (A → B) := +definition inhabited_fun [instance] (A : Type) {B : Type} [H : inhabited B] : inhabited (A → B) := inhabited.rec_on H (λb, inhabited.mk (λa, b)) -definition dfun_inhabited [instance] (A : Type) {B : A → Type} [H : Πx, inhabited (B x)] : +definition inhabited_Pi [instance] (A : Type) {B : A → Type} [H : Πx, inhabited (B x)] : inhabited (Πx, B x) := inhabited.mk (λa, inhabited.rec_on (H a) (λb, b)) diff --git a/library/init/nat.lean b/library/init/nat.lean index 03f31d28ad..e6a5ef8527 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -105,7 +105,7 @@ namespace nat lt_of_succ_lt hlt), aux - definition lt.is_decidable_rel [instance] : decidable_rel lt := + definition decidable_lt [instance] : decidable_rel lt := λ a b, nat.rec_on b (λ (a : nat), inr (not_lt_zero a)) (λ (b₁ : nat) (ih : ∀ a, decidable (a < b₁)) (a : nat), nat.cases_on a @@ -136,7 +136,7 @@ namespace nat (λ hl, eq.rec_on hl !le.refl) (λ hr, le_of_lt hr) - definition le.is_decidable_rel [instance] : decidable_rel le := + definition decidable_le [instance] : decidable_rel le := λ a b, decidable_of_decidable_of_iff _ (iff.intro le_of_eq_or_lt eq_or_lt_of_le) definition le.rec_on {a : nat} {P : nat → Prop} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : ∀ b, a < b → P b) : P b := diff --git a/library/logic/identities.lean b/library/logic/identities.lean index 660d3c3448..1862936a3d 100644 --- a/library/logic/identities.lean +++ b/library/logic/identities.lean @@ -106,7 +106,7 @@ theorem exists_not_of_not_forall {A : Type} {P : A → Prop} [D : ∀x, decidabl [D' : decidable (∃x, ¬P x)] (H : ¬∀x, P x) : ∃x, ¬P x := @by_contradiction _ D' (assume H1 : ¬∃x, ¬P x, - have H2 : ∀x, ¬¬P x, from @forall_not_of_not_exists _ _ (take x, not.decidable) H1, + have H2 : ∀x, ¬¬P x, from @forall_not_of_not_exists _ _ (take x, decidable_not) H1, have H3 : ∀x, P x, from take x, @not_not_elim _ (D x) (H2 x), absurd H3 H)