fix(tactic/omega): fix omega bugs, add docstring (closes #1484) (#1620)

* Fix omega bugs, add docstring

* style(tactic/omega/main): trivial cleaning

src/tactic/omega/int/main.lean

@@ -18,7 +18,7 @@ open_locale omega.int
 
 run_cmd mk_simp_attr `sugar
 attribute [sugar]
-  not_le not_lt
+  ne not_le not_lt
   int.lt_iff_add_one_le
   or_false false_or
   and_true true_and
@@ -76,7 +76,7 @@ meta def to_form_core : expr → tactic form
   do p ← to_form_core px,
      q ← to_form_core qx,
      return (p ∧* q)
-| _ := failed
+| x := trace "Cannot reify expr : " >> trace x >> failed
 
 meta def to_form : nat → expr → tactic (form × nat)
 | m `(_ → %%px) := to_form (m+1) px
@@ -92,4 +92,4 @@ end omega
 open omega.int
 
 meta def omega_int : tactic unit :=
-desugar >> prove_lia >>= apply >> skip
+desugar >> (done <|> (prove_lia >>= apply >> skip))

src/tactic/omega/main.lean

@@ -3,26 +3,26 @@ Copyright (c) 2019 Seul Baek. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Seul Baek
 
-A tactic for discharging linear integer & natural 
+A tactic for discharging linear integer & natural
 number arithmetic goals using the Omega test.
 -/
 
-import tactic.omega.int.main 
-import tactic.omega.nat.main 
+import tactic.omega.int.main
+import tactic.omega.nat.main
 
 namespace omega
 
 open tactic
 
 meta def revert_cond (t : expr → tactic unit) (x : expr) : tactic unit :=
-(t x >> revert x >> skip) <|> skip 
+(t x >> revert x >> skip) <|> skip
 
 meta def revert_cond_all (t : expr → tactic unit) : tactic unit :=
 do hs ← local_context, mmap (revert_cond t) hs, skip
 
 meta def select_domain (t s : tactic (option bool)) : tactic (option bool) :=
 do a ← t, b ← s,
-   match a, b with 
+   match a, b with
    | a,         none      := return a
    | none,      b         := return b
    | (some tt), (some tt) := return (some tt)
@@ -33,36 +33,40 @@ do a ← t, b ← s,
 meta def type_domain (x : expr) : tactic (option bool) :=
 if x = `(int)
 then return (some tt)
-else if x = `(nat) 
+else if x = `(nat)
      then return (some ff)
      else failed
 
-/- 
-Detects domain of a formula from its expr. 
-- Returns none, if domain can be either ℤ or ℕ 
-- Returns some tt, if domain is exclusively ℤ 
+/-
+Detects domain of a formula from its expr.
+- Returns none, if domain can be either ℤ or ℕ
+- Returns some tt, if domain is exclusively ℤ
 - Returns some ff, if domain is exclusively ℕ
-- Fails, if domain is neither ℤ nor ℕ 
+- Fails, if domain is neither ℤ nor ℕ
 -/
+
 meta def form_domain : expr → tactic (option bool)
 | `(¬ %%px)      := form_domain px
 | `(%%px ∨ %%qx) := select_domain (form_domain px) (form_domain qx)
 | `(%%px ∧ %%qx) := select_domain (form_domain px) (form_domain qx)
 | `(%%px ↔ %%qx) := select_domain (form_domain px) (form_domain qx)
-| `(%%(expr.pi _ _ px qx)) := 
-  monad.cond 
-    (if expr.has_var px then return tt else is_prop px)
-    (select_domain (form_domain px) (form_domain qx))
-    (select_domain (type_domain px) (form_domain qx))
+| `(%%(expr.pi _ _ px qx)) :=
+  monad.cond
+     (if expr.has_var px then return tt else is_prop px)
+     (select_domain (form_domain px) (form_domain qx))
+     (select_domain (type_domain px) (form_domain qx))
 | `(@has_lt.lt %%dx %%h _ _) := type_domain dx
 | `(@has_le.le %%dx %%h _ _) := type_domain dx
 | `(@eq %%dx _ _)            := type_domain dx
 | `(@ge %%dx %%h _ _)        := type_domain dx
 | `(@gt %%dx %%h _ _)        := type_domain dx
 | `(@ne %%dx _ _)            := type_domain dx
-| `(true)                    := return none 
-| `(false)                   := return none 
-| _                          := failed 
+| `(true)                    := return none
+| `(false)                   := return none
+| x                          := failed
+
+meta def form_wf (x : expr) : tactic bool :=
+(form_domain x >> return tt) <|> return ff
 
 meta def term_domain (x : expr) : tactic (option bool) :=
 infer_type x >>= type_domain
@@ -76,7 +80,7 @@ do (some tt) ← term_domain x, skip
 meta def rev_lia : tactic unit :=
 do revert_cond_all is_lia_form,
    revert_cond_all is_lia_term
-   
+
 meta def is_lna_form (x : expr) : tactic unit :=
 do (some ff) ← infer_type x >>= form_domain, skip
 
@@ -86,13 +90,13 @@ do (some ff) ← term_domain x, skip
 meta def rev_lna : tactic unit :=
 do revert_cond_all is_lna_form,
    revert_cond_all is_lna_term
-   
-meta def goal_domain_aux : list expr → tactic bool 
+
+meta def goal_domain_aux : list expr → tactic bool
 | []      := failed
-| (x::xs) := 
+| (x::xs) :=
   do b1 ← ((form_domain x >>= return ∘ some) <|> return none),
-     match b1 with 
-     | none             := goal_domain_aux xs 
+     match b1 with
+     | none             := goal_domain_aux xs
      | (some none)      := goal_domain_aux xs
      | (some (some tt)) := return tt
      | (some (some ff)) := return ff
@@ -103,23 +107,42 @@ do gx ← target,
    hxs ← local_context >>= monad.mapm infer_type,
    goal_domain_aux (gx::hxs)
 
+meta def clear_unused_hyp (hx : expr) : tactic unit :=
+do x ← infer_type hx,
+   b ← form_wf x,
+   if (b ∨ x = `(nat) ∨ x = `(int))
+   then skip
+   else clear hx >> skip
+
+meta def clear_unused_hyps : tactic unit :=
+local_context >>= mmap' clear_unused_hyp
+
 meta def preprocess (opt : list name) : tactic unit :=
-if `manual ∈ opt 
+if `manual ∈ opt
 then skip
-else if `int ∈ opt 
+else clear_unused_hyps >>
+     if `int ∈ opt
      then rev_lia
-     else if `nat ∈ opt 
+     else if `nat ∈ opt
           then rev_lna
           else monad.cond goal_domain rev_lia rev_lna
 
 end omega
 
 open lean.parser interactive omega
 
-meta def tactic.interactive.omega (opt : parse (many ident)) : tactic unit := 
-preprocess opt >> 
-if `int ∈ opt 
+/--
+Attempts to discharge goals in the quantifier-free fragment of
+linear integer and natural number arithmetic using the Omega test.
+Guesses the correct domain by looking at the goal and hypotheses,
+and then reverts all relevant hypotheses and variables.
+Use `omega manual` to disable automatic reverts, and `omega int` or
+`omega nat` to specify the domain.
+-/
+meta def tactic.interactive.omega (opt : parse (many ident)) : tactic unit :=
+preprocess opt >>
+if `int ∈ opt
 then omega_int
-else if `nat ∈ opt 
+else if `nat ∈ opt
      then omega_nat
-     else monad.cond goal_domain omega_int omega_nat
+     else mcond goal_domain omega_int omega_nat

src/tactic/omega/nat/main.lean

@@ -20,7 +20,7 @@ open_locale omega.nat
 
 run_cmd mk_simp_attr `sugar_nat
 attribute [sugar_nat]
-  not_le not_lt
+  ne not_le not_lt
   nat.lt_iff_add_one_le
   nat.succ_eq_add_one
   or_false false_or
@@ -148,7 +148,7 @@ meta def to_form_core : expr → tactic form
      q ← to_form_core qx,
      return (p ∧* q)
 | `(_ → %%px) := to_form_core px
-| _ := failed
+| x := trace "Cannot reify expr : " >> trace x >> failed
 
 meta def to_form : nat → expr → tactic (form × nat)
 | m `(_ → %%px) := to_form (m+1) px
@@ -164,4 +164,4 @@ end omega
 open omega.nat
 
 meta def omega_nat : tactic unit :=
-desugar >> prove_lna >>= apply >> skip
+desugar >> (done <|> (prove_lna >>= apply >> skip))

test/omega.lean

@@ -5,6 +5,7 @@ Handbook of Practical Logic and Automated Reasoning.
 
 import tactic.omega
 
+example (n : ℤ) : n - 1 ≠ n := by omega
 example (x : int) : (x = 5 ∨ x = 7) → 2 < x := by omega
 example (x : int) : x ≤ -x → x ≤ 0 := by omega
 example : ∀ x y : int, (x ≤ 5 ∧ y ≤ 3) → x + y ≤ 8 := by omega
@@ -33,6 +34,10 @@ example (x y z : nat) : (x ≤ y) → (z > y) → (x - z = 0) := by omega
 example (x y z : nat) : x - 5 > 122 → y ≤ 127 → y < x := by omega
 example : ∀ (x y : nat), x ≤ y ↔ x - y = 0 := by omega
 example (k : nat) (h : 1 * 1 + 1 * 1 + 1 = 1 * 1 * k) : k = 3 := by omega
+example (a b : ℕ) (h : a < b + 1) (ha : a.prime) : a ≤ b := by omega
+example (a b c : ℕ) (h : a < b + 1) (ha : c.prime) : a ≤ b := by omega
+example (a b : ℕ) (h : a < b + 1) (p : fin a) : a ≤ b := by omega
+example : 3 < 4 := by omega
 
 /-
 Use `omega manual` to disable automatic reverts,