feat(tactic/omega): tactic for linear integer & natural number arithm…

…etic (#827)

* feat(tactic/omega): tactic for discharging linear integer and natural number arithmetic goals

* refactor(tactic/omega): clean up namespace and notations

* Update src/data/list/func.lean

Co-Authored-By: skbaek <seulkeebaek@gmail.com>

* Add changed files

* Refactor val_between_map_div

* Use default inhabitants for list.func

docs/tactics.md

@@ -845,6 +845,33 @@ h : y = 3
 end
 ```
 
+## omega
+
+`omega` attempts to discharge goals in the quantifier-free fragment of linear integer and natural number arithmetic using the Omega test. In other words, the core procedure of `omega` works with goals of the form
+```lean
+∀ x₁, ... ∀ xₖ, P
+```
+where `x₁, ... xₖ` are integer (resp. natural number) variables, and `P` is a quantifier-free formula of linear integer (resp. natural number) arithmetic. For instance:
+```lean
+example : ∀ (x y : int), (x ≤ 5 ∧ y ≤ 3) → x + y ≤ 8 := by omega
+```
+By default, `omega` tries to guess the correct domain by looking at the goal and hypotheses, and then reverts all relevant hypotheses and variables (e.g., all variables of type `nat` and `Prop`s in linear natural number arithmetic, if the domain was determined to be `nat`) to universally close the goal before calling the main procedure. Therefore, `omega` will often work even if the goal is not in the above form:
+```lean
+example (x y : nat) (h : 2 * x + 1 = 2 * y) : false := by omega
+```
+But this behaviour is not always optimal, since it may revert irrelevant hypotheses or incorrectly guess the domain. Use `omega manual` to disable automatic reverts, and `omega int` or `omega nat` to specify the domain. 
+```lean
+example (x y z w : int) (h1 : 3 * y ≥ x) (h2 : z > 19 * w) : 3 * x ≤ 9 * y := 
+by {revert h1 x y, omega manual}
+
+example (i : int) (n : nat) (h1 : i = 0) (h2 : n < n) : false := by omega nat
+
+example (n : nat) (h1 : n < 34) (i : int) (h2 : i * 9 = -72) : i = -8 := 
+by {revert h2 i, omega manual int}
+```
+`omega` handles `nat` subtraction by repeatedly rewriting goals of the form `P[t-s]` into `P[x] ∧ (t = s + x ∨ (t ≤ s ∧ x = 0))`, where `x` is fresh. This means that each (distinct) occurrence of subtraction will cause the goal size to double during DNF transformation.
+
+`omega` implements the real shadow step of the Omega test, but not the dark and gray shadows. Therefore, it should (in principle) succeed whenever the negation of the goal has no real solution, but it may fail if a real solution exists, even if there is no integer/natural number solution.
 ### push_neg
 
 This tactic pushes negations inside expressions. For instance, given an assumption

src/data/int/basic.lean

@@ -8,10 +8,15 @@ The integers, with addition, multiplication, and subtraction.
 import data.nat.basic data.list.basic algebra.char_zero algebra.order_functions
 open nat
 
+
 namespace int
 
-instance : inhabited ℤ := ⟨0⟩
+instance : inhabited ℤ := ⟨int.zero⟩
+
+@[simp] lemma default_eq_zero : default ℤ = 0 := rfl
+
 meta instance : has_to_format ℤ := ⟨λ z, int.rec_on z (λ k, ↑k) (λ k, "-("++↑k++"+1)")⟩
+meta instance : has_reflect ℤ := by tactic.mk_has_reflect_instance
 
 attribute [simp] int.coe_nat_add int.coe_nat_mul int.coe_nat_zero int.coe_nat_one int.coe_nat_succ
 
@@ -558,6 +563,18 @@ theorem neg_div_of_dvd : ∀ {a b : ℤ} (H : b ∣ a), -a / b = -(a / b)
 | ._ b ⟨c, rfl⟩ := if bz : b = 0 then by simp [bz] else
   by rw [neg_mul_eq_mul_neg, int.mul_div_cancel_left _ bz, int.mul_div_cancel_left _ bz]
 
+lemma add_div_of_dvd {a b c : ℤ} :
+  c ∣ a → c ∣ b → (a + b) / c = a / c + b / c :=
+begin
+  intros h1 h2,
+  by_cases h3 : c = 0,
+  { rw [h3, zero_dvd_iff] at *,
+    rw [h1, h2, h3], refl },
+  { apply eq_of_mul_eq_mul_right h3,
+    rw add_mul, repeat {rw [int.div_mul_cancel]};
+    try {apply dvd_add}; assumption }
+end
+
 theorem div_sign : ∀ a b, a / sign b = a * sign b
 | a (n+1:ℕ) := by unfold sign; simp
 | a 0       := by simp [sign]

src/data/list/basic.lean

@@ -4325,7 +4325,7 @@ begin
   { rw [eq_nil_of_le hml, filter_ge_of_top_le hml] }
 end
 
-@[simp] lemma filter_ge (n m l : ℕ) : (Ico n m).filter (λ x, x ≥ l) = Ico (max n l) m :=
+@[simp] lemma filter_ge (n m l : ℕ) : (Ico n m).filter (λ x, x ≥ l) = Ico (_root_.max n l) m :=
 begin
   cases le_total n l with hnl hln,
   { rw [max_eq_right hnl, filter_ge_of_ge hnl] },
@@ -4514,8 +4514,306 @@ lemma choose_property (hp : ∃ a, a ∈ l ∧ p a) : p (choose p l hp) := (choo
 
 end choose
 
+
+namespace func
+
+variables {a : α} 
+variables {as as1 as2 as3 : list α}
+
+local notation as `{` m `↦` a `}` := set a as m
+
+/- set -/
+
+lemma length_set [inhabited α] : ∀ {m : ℕ} {as : list α},
+  (as {m ↦ a}).length = _root_.max as.length (m+1)
+| 0 []          := rfl
+| 0 (a::as)     := by {rw max_eq_left, refl, simp [nat.le_add_right]}
+| (m+1) []      := by simp only [set, nat.zero_max, length, @length_set m]
+| (m+1) (a::as) := by simp only [set, nat.max_succ_succ, length, @length_set m]
+
+@[simp] lemma get_nil [inhabited α] {k : ℕ} : get k [] = default α := 
+by {cases k; refl} 
+
+lemma get_eq_default_of_le [inhabited α] :
+  ∀ (k : ℕ) {as : list α}, as.length ≤ k → get k as = default α
+| 0     []      h1 := rfl
+| 0     (a::as) h1 := by cases h1
+| (k+1) []      h1 := rfl
+| (k+1) (a::as) h1 :=
+  begin
+    apply get_eq_default_of_le k,
+    rw ← nat.succ_le_succ_iff, apply h1,
+  end
+
+@[simp] lemma get_set [inhabited α] {a : α} :
+  ∀ {k : ℕ} {as : list α}, get k (as {k ↦ a}) = a
+| 0 as     := by {cases as; refl, }
+| (k+1) as := by {cases as; simp [get_set]} 
+
+lemma eq_get_of_mem [inhabited α] {a : α} :
+  ∀ {as : list α}, a ∈ as → ∃ n : nat, ∀ d : α, a = (get n as)
+| [] h := by cases h
+| (b::as) h :=
+  begin
+    rw mem_cons_iff at h, cases h,
+    { existsi 0, intro d, apply h },
+    { cases eq_get_of_mem h with n h2,
+      existsi (n+1), apply h2 }
+  end
+
+lemma mem_get_of_le [inhabited α] :
+  ∀ {n : ℕ} {as : list α}, n < as.length → get n as ∈ as
+| _ [] h1 := by cases h1
+| 0 (a::as) _ := or.inl rfl
+| (n+1) (a::as) h1 :=
+  begin
+    apply or.inr, unfold get,
+    apply mem_get_of_le,
+    apply nat.lt_of_succ_lt_succ h1,
+  end
+
+lemma mem_get_of_ne_zero [inhabited α] :
+  ∀ {n : ℕ} {as : list α},
+  get n as ≠ default α → get n as ∈ as
+| _ [] h1 := begin exfalso, apply h1, rw get_nil end
+| 0 (a::as) h1 := or.inl rfl
+| (n+1) (a::as) h1 :=
+  begin
+    unfold get,
+    apply (or.inr (mem_get_of_ne_zero _)),
+    apply h1
+  end
+
+lemma get_set_eq_of_ne [inhabited α] {a : α} :
+  ∀ {as : list α} (k : ℕ) (m : ℕ),
+  m ≠ k → get m (as {k ↦ a}) = get m as
+| as 0 m h1 :=
+  by { cases m, contradiction, cases as; 
+       simp only [set, get, get_nil] }
+| as (k+1) m h1 :=
+  begin
+    cases as; cases m,
+    simp only [set, get],
+    { have h3 : get m (nil {k ↦ a}) = default α,
+      { rw [get_set_eq_of_ne k m, get_nil],
+        intro hc, apply h1, simp [hc] },
+      apply h3 },
+    simp only [set, get],
+    { apply get_set_eq_of_ne k m, 
+      intro hc, apply h1, simp [hc], }
+  end
+
+lemma get_map [inhabited α] [inhabited β] {f : α → β} : 
+  ∀ {n : ℕ} {as : list α}, n < as.length → 
+  get n (as.map f) = f (get n as)
+| _ [] h := by cases h
+| 0 (a::as) h := rfl
+| (n+1) (a::as) h1 :=
+  begin
+    have h2 : n < length as, 
+    { rw [← nat.succ_le_iff, ← nat.lt_succ_iff], 
+      apply h1 },
+    apply get_map h2,
+  end
+
+lemma get_map' [inhabited α] [inhabited β] 
+  {f : α → β} {n : ℕ} {as : list α} :
+  f (default α) = (default β) → 
+  get n (as.map f) = f (get n as) :=
+begin
+  intro h1, by_cases h2 : n < as.length,
+  { apply get_map h2, },
+  { rw not_lt at h2,
+    rw [get_eq_default_of_le _ h2, get_eq_default_of_le, h1], 
+    rw [length_map], apply h2 }
+end
+
+lemma forall_val_of_forall_mem [inhabited α] 
+  {as : list α} {p : α → Prop} :
+  p (default α) → (∀ x ∈ as, p x) → (∀ n, p (get n as)) :=
+begin
+  intros h1 h2 n,
+  by_cases h3 : n < as.length,
+  { apply h2 _ (mem_get_of_le h3) },
+  { rw not_lt at h3,
+    rw get_eq_default_of_le _ h3, apply h1 }
+end
+
+/- equiv -/
+
+lemma equiv_refl [inhabited α] : equiv as as := λ k, rfl
+
+lemma equiv_symm [inhabited α] : equiv as1 as2 → equiv as2 as1 := 
+λ h1 k, (h1 k).symm
+
+lemma equiv_trans [inhabited α] :
+  equiv as1 as2 → equiv as2 as3 → equiv as1 as3 :=
+λ h1 h2 k, eq.trans (h1 k) (h2 k)
+
+lemma equiv_of_eq [inhabited α] : as1 = as2 → equiv as1 as2 := 
+begin intro h1, rw h1, apply equiv_refl end
+
+lemma eq_of_equiv [inhabited α] :
+  ∀ {as1 as2 : list α}, as1.length = as2.length → 
+  equiv as1 as2 → as1 = as2 
+| []     [] h1 h2 := rfl
+| (_::_) [] h1 h2 := by cases h1
+| [] (_::_) h1 h2 := by cases h1
+| (a1::as1) (a2::as2) h1 h2 := 
+  begin
+    congr,
+    { apply h2 0 },
+    have h3 : as1.length = as2.length, 
+    { simpa [add_left_inj, add_comm, length] using h1 },
+    apply eq_of_equiv h3,
+    intro m, apply h2 (m+1) 
+  end
+
+/- neg -/
+
+@[simp] lemma get_neg [inhabited α] [add_group α] 
+  {k : ℕ} {as : list α} : @get α ⟨0⟩ k (neg as) = -(@get α ⟨0⟩ k as) :=
+by {unfold neg, rw (@get_map' α α ⟨0⟩), apply neg_zero}
+
+@[simp] lemma length_neg 
+  [inhabited α] [has_neg α] (as : list α) : 
+  (neg as).length = as.length := 
+by simp only [neg, length_map]
+
+/- pointwise -/
+
+lemma nil_pointwise [inhabited α] [inhabited β] {f : α → β → γ} : 
+  ∀ bs : list β, pointwise f [] bs = bs.map (f $ default α) 
+| []      := rfl
+| (b::bs) := 
+  by simp only [nil_pointwise bs, pointwise, 
+     eq_self_iff_true, and_self, map] 
+
+lemma pointwise_nil [inhabited α] [inhabited β] {f : α → β → γ} : 
+  ∀ as : list α, pointwise f as [] = as.map (λ a, f a $ default β) 
+| []      := rfl
+| (a::as) := 
+  by simp only [pointwise_nil as, pointwise, 
+     eq_self_iff_true, and_self, list.map] 
+
+lemma get_pointwise [inhabited α] [inhabited β] [inhabited γ] 
+  {f : α → β → γ} (h1 : f (default α) (default β) = default γ) : 
+  ∀ (k : nat) (as : list α) (bs : list β), 
+  get k (pointwise f as bs) = f (get k as) (get k bs) 
+| k [] [] := by simp only [h1, get_nil, pointwise, get]
+| 0 [] (b::bs) := 
+  by simp only [get_pointwise, get_nil, 
+      pointwise, get, nat.nat_zero_eq_zero, map] 
+| (k+1) [] (b::bs) := 
+  by { have : get k (map (f $ default α) bs) = f (default α) (get k bs),
+       { simpa [nil_pointwise, get_nil] using (get_pointwise k [] bs) },
+       simpa [get, get_nil, pointwise, map] }
+| 0 (a::as) [] := 
+  by simp only [get_pointwise, get_nil, 
+     pointwise, get, nat.nat_zero_eq_zero, map] 
+| (k+1) (a::as) [] := 
+  by simpa [get, get_nil, pointwise, map, pointwise_nil, get_nil] 
+     using get_pointwise k as []
+| 0 (a::as) (b::bs) := by simp only [pointwise, get] 
+| (k+1) (a::as) (b::bs) := 
+  by simp only [pointwise, get, get_pointwise k] 
+
+lemma length_pointwise [inhabited α] [inhabited β] {f : α → β → γ} : 
+  ∀ {as : list α} {bs : list β}, 
+  (pointwise f as bs).length = _root_.max as.length bs.length 
+| []      []      := rfl
+| []      (b::bs) := 
+  by simp only [pointwise, length, length_map,
+     max_eq_right (nat.zero_le (length bs + 1))]
+| (a::as) []      := 
+  by simp only [pointwise, length, length_map,
+     max_eq_left (nat.zero_le (length as + 1))]
+| (a::as) (b::bs) :=
+  by simp only [pointwise, length, 
+     nat.max_succ_succ, @length_pointwise as bs]
+
+/- add -/
+
+@[simp] lemma get_add {α : Type u} [add_monoid α] {k : ℕ} {xs ys : list α} :
+  @get α ⟨0⟩ k (add xs ys) = ( @get α ⟨0⟩ k xs + @get α ⟨0⟩ k ys) :=
+by {apply get_pointwise, apply zero_add}
+
+@[simp] lemma length_add {α : Type u} 
+  [has_zero α] [has_add α] {xs ys : list α} : 
+  (add xs ys).length = _root_.max xs.length ys.length := 
+@length_pointwise α α α ⟨0⟩ ⟨0⟩ _ _ _
+
+@[simp] lemma nil_add {α : Type u} [add_monoid α] 
+  (as : list α) : add [] as = as := 
+begin
+  rw [add, @nil_pointwise α α α ⟨0⟩ ⟨0⟩],
+  apply eq.trans _ (map_id as), 
+  congr, ext, 
+  have : @default α ⟨0⟩ = 0 := rfl,
+  rw [this, zero_add], refl
+end
+
+@[simp] lemma add_nil {α : Type u} [add_monoid α] 
+  (as : list α) : add as [] = as := 
+begin
+  rw [add, @pointwise_nil α α α ⟨0⟩ ⟨0⟩], 
+  apply eq.trans _ (map_id as), 
+  congr, ext, 
+  have : @default α ⟨0⟩ = 0 := rfl,
+  rw [this, add_zero], refl
+end
+
+lemma map_add_map {α : Type u} [add_monoid α] (f g : α → α) {as : list α} :
+  add (as.map f) (as.map g) = as.map (λ x, f x + g x) :=
+begin
+  apply @eq_of_equiv _ (⟨0⟩ : inhabited α),
+  { rw [length_map, length_add, max_eq_left, length_map],
+    apply le_of_eq, 
+    rw [length_map, length_map] },
+  intros m, 
+  rw [get_add], 
+  by_cases h : m < length as,
+  { repeat {rw [@get_map α α ⟨0⟩ ⟨0⟩ _ _ _ h]} },
+  rw not_lt at h,
+  repeat {rw [get_eq_default_of_le m]};
+  try {rw length_map, apply h},
+  apply zero_add
+end
+
+/- sub -/
+
+@[simp] lemma get_sub {α : Type u} 
+  [add_group α] {k : ℕ} {xs ys : list α} :
+  @get α ⟨0⟩ k (sub xs ys) = (@get α ⟨0⟩ k xs - @get α ⟨0⟩ k ys) :=
+by {apply get_pointwise, apply sub_zero}
+
+@[simp] lemma length_sub [has_zero α] [has_sub α] {xs ys : list α} : 
+  (sub xs ys).length = _root_.max xs.length ys.length := 
+@length_pointwise α α α ⟨0⟩ ⟨0⟩ _ _ _
+
+@[simp] lemma nil_sub {α : Type} [add_group α] 
+  (as : list α) : sub [] as = @neg α ⟨0⟩ _ as := 
+begin
+  rw [sub, nil_pointwise], 
+  congr, ext, 
+  have : @default α ⟨0⟩ = 0 := rfl,
+  rw [this, zero_sub]
+end
+
+@[simp] lemma sub_nil {α : Type} [add_group α] 
+  (as : list α) : sub as [] = as := 
+begin
+  rw [sub, pointwise_nil], 
+  apply eq.trans _ (map_id as), 
+  congr, ext, 
+  have : @default α ⟨0⟩ = 0 := rfl,
+  rw [this, sub_zero], refl
+end
+
+end func
+
 end list
 
 theorem option.to_list_nodup {α} : ∀ o : option α, o.to_list.nodup
 | none     := list.nodup_nil
-| (some x) := list.nodup_singleton x
+| (some x) := list.nodup_singleton x