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

@@ -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

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

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) :

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 -/
 

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 "↑⇑⟰⇈⇅↥⇧↟↿↾⇡⇞          ↰↱➦ ⇪⇫⇬⇭⇮⇯                                           "))