From abe129aa4fb55f3a564138eb311ded6767828140 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 15 Dec 2014 19:17:51 -0800 Subject: [PATCH] refactor(library): rename theorems "iff.flip_sign -> not_iff_not_of_iff" and "decidable_iff_equiv -> decidable_of_decidable_of_iff" --- library/data/int/order.lean | 4 ++-- library/data/list/basic.lean | 4 ++-- library/data/prod/thms.lean | 2 +- library/data/subtype.lean | 2 +- library/data/sum.lean | 4 ++-- library/init/logic.lean | 29 +++++++++++++++++------------ library/init/nat.lean | 2 +- library/logic/connectives.lean | 4 ++-- tests/lean/run/sum_bug.lean | 4 ++-- 9 files changed, 30 insertions(+), 25 deletions(-) diff --git a/library/data/int/order.lean b/library/data/int/order.lean index cf5176f1f4..6970dee005 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -431,8 +431,8 @@ have aux : Πx, decidable (0 ≤ x), from iff.intro (assume H1, nat_abs_nonneg_eq H1) (assume H1, H1 ▸ of_nat_nonneg (nat_abs x)), - decidable_iff_equiv _ (iff.symm H), -decidable_iff_equiv !aux (iff.symm (le_iff_sub_nonneg a b)) + decidable_of_decidable_of_iff _ (iff.symm H), +decidable_of_decidable_of_iff !aux (iff.symm (le_iff_sub_nonneg a b)) definition ge_decidable [instance] {a b : ℤ} : decidable (a ≥ b) := _ definition lt_decidable [instance] {a b : ℤ} : decidable (a < b) := _ diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index a3367096cf..02cc4419a5 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -203,7 +203,7 @@ rec_on l (assume Heq, absurd Heq Hne) (assume Hp, absurd Hp Hn), have H2 : ¬x ∈ h::l, from - iff.elim_right (iff.flip_sign !mem.cons) H1, + iff.elim_right (not_iff_not_of_iff !mem.cons) H1, decidable.inr H2))) -- Find @@ -225,7 +225,7 @@ rec_on l (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 (iff.flip_sign !mem.cons) P₁, + have P₂ : ¬(x = y ∨ x ∈ l), from iff.elim_right (not_iff_not_of_iff !mem.cons) P₁, have P₃ : ¬x = y ∧ ¬x ∈ l, from (iff.elim_left not_or_iff_not_and_not P₂), calc find x (y::l) = if x = y then 0 else succ (find x l) : !find.cons diff --git a/library/data/prod/thms.lean b/library/data/prod/thms.lean index b354269214..3c4886137a 100644 --- a/library/data/prod/thms.lean +++ b/library/data/prod/thms.lean @@ -23,7 +23,7 @@ namespace prod iff.intro (assume H, H ▸ and.intro rfl rfl) (assume H, and.elim H (assume H₄ H₅, equal H₄ H₅)), - decidable_iff_equiv _ (iff.symm H₃) + decidable_of_decidable_of_iff _ (iff.symm H₃) -- ### flip operation diff --git a/library/data/subtype.lean b/library/data/subtype.lean index d13ba25de8..ba55a2ad3d 100644 --- a/library/data/subtype.lean +++ b/library/data/subtype.lean @@ -29,5 +29,5 @@ namespace subtype 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), - decidable_iff_equiv _ (iff.symm H1) + decidable_of_decidable_of_iff _ (iff.symm H1) end subtype diff --git a/library/data/sum.lean b/library/data/sum.lean index 56c1f4b58c..b6b73cca4d 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -50,13 +50,13 @@ namespace sum (take b₂, have H₃ : (inl B a₁ = inr A b₂) ↔ false, from iff.intro inl_neq_inr (assume H₄, !false.rec H₄), - show decidable (inl B a₁ = inr A b₂), from decidable_iff_equiv _ (iff.symm H₃))) + show decidable (inl B a₁ = inr A b₂), from decidable_of_decidable_of_iff _ (iff.symm H₃))) (take b₁, show decidable (inr A b₁ = s₂), from rec_on s₂ (take a₂, have H₃ : (inr A b₁ = inl B a₂) ↔ false, from iff.intro (assume H₄, inl_neq_inr (H₄⁻¹)) (assume H₄, !false.rec H₄), - show decidable (inr A b₁ = inl B a₂), from decidable_iff_equiv _ (iff.symm H₃)) + show decidable (inr A b₁ = inl B a₂), from decidable_of_decidable_of_iff _ (iff.symm H₃)) (take b₂, show decidable (inr A b₁ = inr A b₂), from decidable.rec_on (H₂ b₁ b₂) (assume Heq : b₁ = b₂, decidable.inl (Heq ▸ rfl)) diff --git a/library/init/logic.lean b/library/init/logic.lean index 9cc7750e12..309cbc54b9 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -200,11 +200,6 @@ namespace iff definition mp' := @elim_right - definition flip_sign (H₁ : a ↔ b) : ¬a ↔ ¬b := - intro - (assume (Hna : ¬ a) (Hb : b), absurd (elim_right H₁ Hb) Hna) - (assume (Hnb : ¬ b) (Ha : a), absurd (elim_left H₁ Ha) Hnb) - definition refl (a : Prop) : a ↔ a := intro (assume H, H) (assume H, H) @@ -226,6 +221,11 @@ namespace iff iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb) end iff +definition not_iff_not_of_iff (H₁ : a ↔ b) : ¬a ↔ ¬b := +iff.intro + (assume (Hna : ¬ a) (Hb : b), absurd (iff.elim_right H₁ Hb) Hna) + (assume (Hnb : ¬ b) (Ha : a), absurd (iff.elim_left H₁ Ha) Hnb) + theorem of_iff_true (H : a ↔ true) : a := iff.mp (iff.symm H) trivial @@ -278,15 +278,20 @@ namespace decidable (assume H1 : p, H1) (assume H1 : ¬p, false.rec _ (H H1)) - definition decidable_iff_equiv (Hp : decidable p) (H : p ↔ q) : decidable q := - rec_on Hp - (assume Hp : p, inl (iff.elim_left H Hp)) - (assume Hnp : ¬p, inr (iff.elim_left (iff.flip_sign H) Hnp)) - - definition decidable_eq_equiv (Hp : decidable p) (H : p = q) : decidable q := - decidable_iff_equiv Hp (iff.of_eq H) end decidable +section + variables {p q : Prop} + open decidable + definition decidable_of_decidable_of_iff (Hp : decidable p) (H : p ↔ q) : decidable q := + decidable.rec_on Hp + (assume Hp : p, inl (iff.elim_left H Hp)) + (assume Hnp : ¬p, inr (iff.elim_left (not_iff_not_of_iff H) Hnp)) + + definition decidable_of_decidable_of_eq (Hp : decidable p) (H : p = q) : decidable q := + decidable_of_decidable_of_iff Hp (iff.of_eq H) +end + section variables {p q : Prop} open decidable (rec_on inl inr) diff --git a/library/init/nat.lean b/library/init/nat.lean index ee34238506..4097ee9952 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -146,7 +146,7 @@ namespace nat (λ hr, le.of_lt hr) definition le.is_decidable_rel [instance] : decidable_rel le := - λ a b, decidable_iff_equiv _ (iff.intro le.of_eq_or_lt eq_or_lt_of_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 := begin diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean index daa8abee75..4be528a36e 100644 --- a/library/logic/connectives.lean +++ b/library/logic/connectives.lean @@ -176,7 +176,7 @@ section theorem if_congr [H₁ : decidable c₁] {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : - (if c₁ then t₁ else e₁) = (@ite c₂ (decidable.decidable_iff_equiv H₁ Hc) A t₂ e₂) := - have H2 [visible] : decidable c₂, from (decidable.decidable_iff_equiv H₁ Hc), + (if c₁ then t₁ else e₁) = (@ite c₂ (decidable_of_decidable_of_iff H₁ Hc) A t₂ e₂) := + have H2 [visible] : decidable c₂, from (decidable_of_decidable_of_iff H₁ Hc), if_congr_aux Hc Ht He end diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean index a717a70736..0cecf9d7df 100644 --- a/tests/lean/run/sum_bug.lean +++ b/tests/lean/run/sum_bug.lean @@ -49,13 +49,13 @@ rec_on s1 (take b2, have H3 : (inl B a1 = inr A b2) ↔ false, from iff.intro inl_neq_inr (assume H4, false.elim H4), - show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff.symm H3))) + show decidable (inl B a1 = inr A b2), from decidable_of_decidable_of_iff _ (iff.symm H3))) (take b1, show decidable (inr A b1 = s2), from rec_on s2 (take a2, have H3 : (inr A b1 = inl B a2) ↔ false, from iff.intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false.elim H4), - show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff.symm H3)) + show decidable (inr A b1 = inl B a2), from decidable_of_decidable_of_iff _ (iff.symm H3)) (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2)) end sum