feat(library/data/list/comb): define upto list generator

library/data/list/comb.lean

@@ -101,31 +101,56 @@ theorem foldr_append (f : A → B → B) : ∀ (b : B) (l₁ l₂ : list A), fol
 | b []      l₂ := rfl
 | b (a::l₁) l₂ := by rewrite [append_cons, *foldr_cons, foldr_append]
 
-definition all (p : A → Prop) (l : list A) : Prop :=
+definition all (l : list A) (p : A → Prop) : Prop :=
 foldr (λ a r, p a ∧ r) true l
 
-definition any (p : A → Prop) (l : list A) : Prop :=
+definition any (l : list A) (p : A → Prop) : Prop :=
 foldr (λ a r, p a ∨ r) false l
 
-theorem all_nil (p : A → Prop) : all p [] = true
+theorem all_nil (p : A → Prop) : all [] p = true
 
-theorem all_cons (p : A → Prop) (a : A) (l : list A) : all p (a::l) = (p a ∧ all p l)
+theorem all_cons (p : A → Prop) (a : A) (l : list A) : all (a::l) p = (p a ∧ all l p)
 
-theorem of_mem_of_all {p : A → Prop} {a : A} : ∀ {l}, a ∈ l → all p l → p a
+theorem all_of_all_cons {p : A → Prop} {a : A} {l : list A} : all (a::l) p → all l p :=
+assume h, by rewrite [all_cons at h]; exact (and.elim_right h)
+
+theorem of_all_cons {p : A → Prop} {a : A} {l : list A} : all (a::l) p → p a :=
+assume h, by rewrite [all_cons at h]; exact (and.elim_left h)
+
+theorem all_cons_of_all {p : A → Prop} {a : A} {l : list A} : p a → all l p → all (a::l) p :=
+assume pa alllp, and.intro pa alllp
+
+theorem all_implies {p q : A → Prop} : ∀ {l}, all l p → (∀ x, p x → q x) → all l q
+| []     h₁ h₂ := trivial
+| (a::l) h₁ h₂ :=
+  have allq : all l q, from all_implies (all_of_all_cons h₁) h₂,
+  have qa : q a, from h₂ a (of_all_cons h₁),
+  all_cons_of_all qa allq
+
+theorem of_mem_of_all {p : A → Prop} {a : A} : ∀ {l}, a ∈ l → all l p → p a
 | []     h₁ h₂ := absurd h₁ !not_mem_nil
 | (b::l) h₁ h₂ :=
   or.elim (eq_or_mem_of_mem_cons h₁)
     (λ aeqb : a = b,
       by rewrite [all_cons at h₂, -aeqb at h₂]; exact (and.elim_left h₂))
     (λ ainl : a ∈ l,
-      have allp : all p l, by rewrite [all_cons at h₂]; exact (and.elim_right h₂),
+      have allp : all l p, by rewrite [all_cons at h₂]; exact (and.elim_right h₂),
       of_mem_of_all ainl allp)
 
-theorem any_nil (p : A → Prop) : any p [] = false
+theorem any_nil (p : A → Prop) : any [] p = false
 
-theorem any_cons (p : A → Prop) (a : A) (l : list A) : any p (a::l) = (p a ∨ any p l)
+theorem any_cons (p : A → Prop) (a : A) (l : list A) : any (a::l) p = (p a ∨ any l p)
 
-definition decidable_all (p : A → Prop) [H : decidable_pred p] : ∀ l, decidable (all p l)
+theorem any_of_mem (p : A → Prop) {a : A} : ∀ {l}, a ∈ l → p a → any l p
+| []     i h := absurd i !not_mem_nil
+| (b::l) i h :=
+  or.elim (eq_or_mem_of_mem_cons i)
+    (λ aeqb : a = b, by rewrite [-aeqb]; exact (or.inl h))
+    (λ ainl : a ∈ l,
+      have anyl : any l p, from any_of_mem ainl h,
+      or.inr anyl)
+
+definition decidable_all (p : A → Prop) [H : decidable_pred p] : ∀ l, decidable (all l p)
 | []       := decidable_true
 | (a :: l) :=
   match H a with
@@ -134,10 +159,10 @@ definition decidable_all (p : A → Prop) [H : decidable_pred p] : ∀ l, decida
     | inl Hp₂ := inl (and.intro Hp₁ Hp₂)
     | inr Hn₂ := inr (not_and_of_not_right (p a) Hn₂)
     end
-  | inr Hn := inr (not_and_of_not_left (all p l) Hn)
+  | inr Hn := inr (not_and_of_not_left (all l p) Hn)
   end
 
-definition decidable_any (p : A → Prop) [H : decidable_pred p] : ∀ l, decidable (any p l)
+definition decidable_any (p : A → Prop) [H : decidable_pred p] : ∀ l, decidable (any l p)
 | []       := decidable_false
 | (a :: l) :=
   match H a with

library/data/list/set.lean

@@ -376,6 +376,45 @@ theorem erase_dup_eq_of_nodup [H : decidable_eq A] : ∀ {l : list A}, nodup l
   by rewrite [erase_dup_cons_of_not_mem nainl, erase_dup_eq_of_nodup dl]
 end nodup
 
+/- upto -/
+definition upto : nat → list nat
+| 0     := []
+| (n+1) := n :: upto n
+
+theorem upto_nil  : upto 0 = nil
+
+theorem upto_succ (n : nat) : upto (succ n) = n :: upto n
+
+theorem length_upto : ∀ n, length (upto n) = n
+| 0        := rfl
+| (succ n) := by rewrite [upto_succ, length_cons, length_upto]
+
+theorem upto_less : ∀ n, all (upto n) (λ i, i < n)
+| 0        := trivial
+| (succ n) :=
+   have alln : all (upto n) (λ i, i < n), from upto_less n,
+   all_cons_of_all (lt.base n) (all_implies alln (λ x h, lt.step h))
+
+theorem nodup_upto : ∀ n, nodup (upto n)
+| 0     := nodup_nil
+| (n+1) :=
+  have d : nodup (upto n), from nodup_upto n,
+  have n : n ∉ upto n, from
+    assume i : n ∈ upto n, absurd (of_mem_of_all i (upto_less n)) (lt.irrefl n),
+  nodup_cons n d
+
+theorem lt_of_mem_upto {n i : nat} : i ∈ upto n → i < n :=
+assume i, of_mem_of_all i (upto_less n)
+
+theorem mem_upto_succ_of_mem_upto {n i : nat} : i ∈ upto n → i ∈ upto (succ n) :=
+assume i, mem_cons_of_mem _ i
+
+theorem mem_upto_of_lt : ∀ {n i : nat}, i < n → i ∈ upto n
+| 0        i h := absurd h !not_lt_zero
+| (succ n) i h := or.elim (eq_or_lt_of_le h)
+  (λ ieqn : i = n, by rewrite [ieqn, upto_succ]; exact !mem_cons)
+  (λ iltn : i < n, mem_upto_succ_of_mem_upto (mem_upto_of_lt iltn))
+
 /- union -/
 section union
 variable {A : Type}