From ff41886a329386420fa810d80d563f9df8d758bb Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 4 Jun 2015 19:57:56 -0400 Subject: [PATCH] feat(nat/bquant): give instances for quantification bounded with le also add theorems c_iff_c to logic/connectives, where c is a connective --- hott/types/nat/order.hlean | 2 +- library/data/nat/bquant.lean | 13 +++++++++++++ library/data/nat/order.lean | 11 +++++++---- library/logic/connectives.lean | 23 +++++++++++++++++++++++ src/emacs/lean-input.el | 2 +- 5 files changed, 45 insertions(+), 6 deletions(-) diff --git a/hott/types/nat/order.hlean b/hott/types/nat/order.hlean index d7337d69c1..b0179f54e0 100644 --- a/hott/types/nat/order.hlean +++ b/hott/types/nat/order.hlean @@ -189,7 +189,7 @@ eq_zero_of_add_eq_zero_right Hk /- succ and pred -/ theorem lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n := -iff.intro succ_le_of_lt lt_of_succ_le +iff.rfl theorem self_le_succ (n : ℕ) : n ≤ succ n := le.intro !add_one diff --git a/library/data/nat/bquant.lean b/library/data/nat/bquant.lean index 2d52cca09f..4597522898 100644 --- a/library/data/nat/bquant.lean +++ b/library/data/nat/bquant.lean @@ -78,4 +78,17 @@ section (λ p_pos, inl (ball_succ_of_ball ih_pos p_pos)) (λ p_neg, inr (not_ball_of_not p_neg))) (λ ih_neg, inr (not_ball_succ_of_not_ball ih_neg))) + + definition decidable_bex_le [instance] (n : nat) (P : nat → Prop) [H : decidable_pred P] + : decidable (∃ x, x ≤ n ∧ P x) := + decidable_of_decidable_of_iff + (decidable_bex (succ n) P) + (exists_congr (λn, and_iff_and !lt_succ_iff_le !iff.refl)) + + definition decidable_ball_le [instance] (n : nat) (P : nat → Prop) [H : decidable_pred P] + : decidable (∀ x, x ≤ n → P x) := + decidable_of_decidable_of_iff + (decidable_ball (succ n) P) + (forall_congr (λn, imp_iff_imp !lt_succ_iff_le !iff.refl)) + end diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 5ccf6a484a..1493856574 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -202,8 +202,14 @@ eq_zero_of_add_eq_zero_right Hk /- succ and pred -/ +theorem le_of_lt_succ {m n : nat} (H : m < succ n) : m ≤ n := +le_of_succ_le_succ H + theorem lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n := -iff.intro succ_le_of_lt lt_of_succ_le +iff.rfl + +theorem lt_succ_iff_le (m n : nat) : m < succ n ↔ m ≤ n := +iff.intro le_of_lt_succ lt_succ_of_le theorem self_le_succ (n : ℕ) : n ≤ succ n := le.intro !add_one @@ -268,9 +274,6 @@ discriminate theorem lt_succ_self (n : ℕ) : n < succ n := lt.base n -theorem le_of_lt_succ {n m : ℕ} (H : n < succ m) : n ≤ m := -le_of_succ_le_succ (succ_le_of_lt H) - /- other forms of induction -/ protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean index d0f5bab5ad..5462e541b9 100644 --- a/library/logic/connectives.lean +++ b/library/logic/connectives.lean @@ -32,6 +32,11 @@ theorem imp_false (a : Prop) : (a → false) ↔ ¬ a := iff.rfl theorem false_imp (a : Prop) : (false → a) ↔ true := iff.intro (assume H, trivial) (assume H H1, false.elim H1) +theorem imp_iff_imp (H1 : a ↔ c) (H2 : b ↔ d) : (a → b) ↔ (c → d) := +iff.intro + (λHab Hc, iff.elim_left H2 (Hab (iff.elim_right H1 Hc))) + (λHcd Ha, iff.elim_right H2 (Hcd (iff.elim_left H1 Ha))) + /- not -/ theorem not.elim (H1 : ¬a) (H2 : a) : false := H1 H2 @@ -62,6 +67,12 @@ iff.intro (assume H, H trivial) (assume H, false.elim H) theorem not_false_iff : ¬ false ↔ true := iff.intro (assume H, trivial) (assume H H1, H1) +theorem not_iff_not (H : a ↔ b) : ¬a ↔ ¬b := +iff.intro + (λHna Hb, Hna (iff.elim_right H Hb)) + (λHnb Ha, Hnb (iff.elim_left H Ha)) + + /- and -/ definition not_and_of_not_left (b : Prop) (Hna : ¬a) : ¬(a ∧ b) := @@ -124,6 +135,11 @@ iff.intro (assume Hab, and.elim_left Hab) (assume Ha, and.intro Ha Hb) +theorem and_iff_and (H1 : a ↔ c) (H2 : b ↔ d) : (a ∧ b) ↔ (c ∧ d) := +iff.intro + (assume Hab, and.intro (iff.elim_left H1 (and.left Hab)) (iff.elim_left H2 (and.right Hab))) + (assume Hcd, and.intro (iff.elim_right H1 (and.left Hcd)) (iff.elim_right H2 (and.right Hcd))) + /- or -/ definition not_or (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) := @@ -195,6 +211,11 @@ iff.intro (assume H, or.elim H (assume H1, H1) (assume H1, H1)) (assume H, or.inl H) +theorem or_iff_or (H1 : a ↔ c) (H2 : b ↔ d) : (a ∨ b) ↔ (c ∨ d) := +iff.intro + (λHab, or.elim Hab (λHa, or.inl (iff.elim_left H1 Ha)) (λHb, or.inr (iff.elim_left H2 Hb))) + (λHcd, or.elim Hcd (λHc, or.inl (iff.elim_right H1 Hc)) (λHd, or.inr (iff.elim_right H2 Hd))) + /- distributivity -/ theorem and.distrib_left (a b c : Prop) : a ∧ (b ∨ c) ↔ (a ∧ b) ∨ (a ∧ c) := @@ -260,6 +281,8 @@ iff.intro (λp a, iff.elim_left (H a) (p a)) (λq a, iff.elim_right (H a) (q a)) theorem imp_iff {P : Prop} (Q : Prop) (p : P) : (P → Q) ↔ Q := iff.intro (λf, f p) (λq p, q) +theorem iff_iff_iff (H1 : a ↔ c) (H2 : b ↔ d) : (a ↔ b) ↔ (c ↔ d) := +and_iff_and (imp_iff_imp H1 H2) (imp_iff_imp H2 H1) /- if-then-else -/ diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el index 48cf9e05e6..19c612f091 100644 --- a/src/emacs/lean-input.el +++ b/src/emacs/lean-input.el @@ -392,7 +392,7 @@ order for the change to take effect." ("join" . ,(lean-input-to-string-list "⋈⋉⋊⋋⋌⨝⟕⟖⟗")) ;; Arrows. - ("iff" . ("↔")) + ("iff" . ("↔")) ("imp" . ("→")) ("l" . ,(lean-input-to-string-list "λ←⇐⇚⇇⇆↤⇦↞↼↽⇠⇺↜⇽⟵⟸↚⇍⇷ ↹ ↢↩↫⇋⇜⇤⟻⟽⤆↶↺⟲ ")) ("r" . ,(lean-input-to-string-list "→⇒⇛⇉⇄↦⇨↠⇀⇁⇢⇻↝⇾⟶⟹↛⇏⇸⇶ ↴ ↣↪↬⇌⇝⇥⟼⟾⤇↷↻⟳⇰⇴⟴⟿ ➵➸➙➔➛➜➝➞➟➠➡➢➣➤➧➨➩➪➫➬➭➮➯➱➲➳➺➻➼➽➾⊸")) ("u" . ,(lean-input-to-string-list "↑⇑⟰⇈⇅↥⇧↟↿↾⇡⇞ ↰↱➦ ⇪⇫⇬⇭⇮⇯ "))