From 242ad1bd6515ca295f0231c73c5fea8ea8be752b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Nov 2016 17:03:21 -0800
Subject: [PATCH] feat(library/init/meta/comp_value_tactics): add comp_val
 tactic for testing

---
 library/init/meta/comp_value_tactics.lean |  42 +++++
 library/init/meta/default.lean            |   1 +
 library/init/meta/expr.lean               |  26 +++-
 src/library/vm/vm_expr.cpp                |  18 +++
 tests/lean/run/comp_val1.lean             | 178 ++++++++++++++++++++++
 5 files changed, 262 insertions(+), 3 deletions(-)
 create mode 100644 library/init/meta/comp_value_tactics.lean
 create mode 100644 tests/lean/run/comp_val1.lean

diff --git a/library/init/meta/comp_value_tactics.lean b/library/init/meta/comp_value_tactics.lean
new file mode 100644
index 0000000000..3ef84fb781
--- /dev/null
+++ b/library/init/meta/comp_value_tactics.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.meta.tactic
+
+meta constant mk_nat_val_ne_proof : expr → expr → option expr
+meta constant mk_nat_val_lt_proof : expr → expr → option expr
+meta constant mk_nat_val_le_proof : expr → expr → option expr
+
+namespace tactic
+open expr
+meta def comp_val : tactic unit :=
+do t ← target,
+   guard (is_app t),
+   type ← infer_type t^.app_arg,
+   guard (type = const `nat []),
+   (do (a, b) ← returnopt (is_ne t),
+       pr     ← returnopt (mk_nat_val_ne_proof a b),
+       exact pr)
+   <|>
+   (do (a, b) ← returnopt (is_lt t),
+       pr     ← returnopt (mk_nat_val_lt_proof a b),
+       exact pr)
+   <|>
+   (do (a, b) ← returnopt (is_gt t),
+       pr     ← returnopt (mk_nat_val_lt_proof b a),
+       exact pr)
+   <|>
+   (do (a, b) ← returnopt (is_le t),
+       pr     ← returnopt (mk_nat_val_le_proof a b),
+       exact pr)
+   <|>
+   (do (a, b) ← returnopt (is_ge t),
+       pr     ← returnopt (mk_nat_val_le_proof b a),
+       exact pr)
+   <|>
+   (do (a, b) ← returnopt (is_eq t),
+       unify a b, to_expr `(eq.refl %%a) >>= exact)
+end tactic
diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean
index 5f78d29eb0..7800f80f63 100644
--- a/library/init/meta/default.lean
+++ b/library/init/meta/default.lean
@@ -13,3 +13,4 @@ import init.meta.backward init.meta.rewrite_tactic
 import init.meta.mk_dec_eq_instance init.meta.mk_inhabited_instance
 import init.meta.simp_tactic init.meta.set_get_option_tactics
 import init.meta.interactive init.meta.converter init.meta.vm
+import init.meta.comp_value_tactics
diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index 4d3f3c2510..0646a75153 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -147,6 +147,9 @@ meta def is_constant_of : expr → name → bool
 meta def is_app_of (e : expr) (n : name) : bool :=
 is_app e && is_constant_of (get_app_fn e) n
 
+meta def is_napp_of (e : expr) (c : name) (n : nat) : bool :=
+to_bool (is_app_of e c ∧ get_app_num_args e = n)
+
 meta def is_false (e : expr) : bool :=
 is_constant_of e `false
 
@@ -156,17 +159,34 @@ meta def is_not : expr → option expr
 | e             := none
 
 meta def is_eq (e : expr) : option (expr × expr) :=
-if is_app_of e `eq ∧ get_app_num_args e = 3
+if is_napp_of e `eq 3
 then some (app_arg (app_fn e), app_arg e)
 else none
 
 meta def is_ne (e : expr) : option (expr × expr) :=
-if is_app_of e `ne ∧ get_app_num_args e = 3
+if is_napp_of e `ne 3
 then some (app_arg (app_fn e), app_arg e)
 else none
 
+meta def is_bin_arith_app (e : expr) (op : name) : option (expr × expr) :=
+if is_napp_of e op 4
+then some (app_arg (app_fn e), app_arg e)
+else none
+
+meta def is_lt (e : expr) : option (expr × expr) :=
+is_bin_arith_app e `lt
+
+meta def is_gt (e : expr) : option (expr × expr) :=
+is_bin_arith_app e `gt
+
+meta def is_le (e : expr) : option (expr × expr) :=
+is_bin_arith_app e `le
+
+meta def is_ge (e : expr) : option (expr × expr) :=
+is_bin_arith_app e `ge
+
 meta def is_heq (e : expr) : option (expr × expr × expr × expr) :=
-if is_app_of e `heq ∧ get_app_num_args e = 4
+if is_napp_of e `heq 4
 then some (app_arg (app_fn (app_fn (app_fn e))),
            app_arg (app_fn (app_fn e)),
            app_arg (app_fn e),
diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp
index ba3a7dd3b4..53c21cbc30 100644
--- a/src/library/vm/vm_expr.cpp
+++ b/src/library/vm/vm_expr.cpp
@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 #include "library/expr_lt.h"
 #include "library/deep_copy.h"
+#include "library/comp_val.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_nat.h"
 #include "library/vm/vm_string.h"
@@ -322,6 +323,19 @@ vm_obj expr_copy_pos_info(vm_obj const & src, vm_obj const & tgt) {
     return to_obj(copy_tag(to_expr(src), copy(to_expr(tgt))));
 }
 
+// TODO(Leo): move to a different file
+vm_obj vm_mk_nat_val_ne_proof(vm_obj const & a, vm_obj const & b) {
+    return to_obj(mk_nat_val_ne_proof(to_expr(a), to_expr(b)));
+}
+
+vm_obj vm_mk_nat_val_lt_proof(vm_obj const & a, vm_obj const & b) {
+    return to_obj(mk_nat_val_lt_proof(to_expr(a), to_expr(b)));
+}
+
+vm_obj vm_mk_nat_val_le_proof(vm_obj const & a, vm_obj const & b) {
+    return to_obj(mk_nat_val_le_proof(to_expr(a), to_expr(b)));
+}
+
 void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name({"expr", "var"}),              expr_var);
     DECLARE_VM_BUILTIN(name({"expr", "sort"}),             expr_sort);
@@ -355,6 +369,10 @@ void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name({"expr", "hash"}),             expr_hash);
     DECLARE_VM_BUILTIN(name({"expr", "copy_pos_info"}),    expr_copy_pos_info);
     DECLARE_VM_CASES_BUILTIN(name({"expr", "cases_on"}),   expr_cases_on);
+
+    DECLARE_VM_BUILTIN(name("mk_nat_val_ne_proof"),        vm_mk_nat_val_ne_proof);
+    DECLARE_VM_BUILTIN(name("mk_nat_val_lt_proof"),        vm_mk_nat_val_lt_proof);
+    DECLARE_VM_BUILTIN(name("mk_nat_val_le_proof"),        vm_mk_nat_val_le_proof);
 }
 
 void finalize_vm_expr() {
diff --git a/tests/lean/run/comp_val1.lean b/tests/lean/run/comp_val1.lean
new file mode 100644
index 0000000000..5770b48004
--- /dev/null
+++ b/tests/lean/run/comp_val1.lean
@@ -0,0 +1,178 @@
+open tactic
+
+example : 0 < 1 := by comp_val
+example : 0 < 2 := by comp_val
+example : 0 < 3 := by comp_val
+example : 0 < 4 := by comp_val
+example : 0 < 5 := by comp_val
+example : 0 < 6 := by comp_val
+example : 0 < 1293821 := by comp_val
+example : 0 < 1293822 := by comp_val
+
+example : 1 < 2 := by comp_val
+example : 1 < 3 := by comp_val
+example : 1 < 4 := by comp_val
+example : 1 < 5 := by comp_val
+example : 1 < 6 := by comp_val
+example : 1 < 1293821 := by comp_val
+example : 1 < 1293822 := by comp_val
+
+example : 2 < 3 := by comp_val
+example : 2 < 4 := by comp_val
+example : 2 < 5 := by comp_val
+example : 2 < 6 := by comp_val
+example : 2 < 1293821 := by comp_val
+example : 2 < 1293822 := by comp_val
+
+example : 3 < 4 := by comp_val
+example : 3 < 5 := by comp_val
+example : 3 < 6 := by comp_val
+example : 3 < 1293821 := by comp_val
+example : 3 < 1293822 := by comp_val
+
+example : 4 < 5 := by comp_val
+example : 4 < 6 := by comp_val
+example : 4 < 1293821 := by comp_val
+example : 4 < 1293822 := by comp_val
+
+example : 103093 < 1293821 := by comp_val
+example : 3121 < 1293822 := by comp_val
+example : 312110028381818 < 1181171711293822 := by comp_val
+example : 312110028381819 < 1181171711293822 := by comp_val
+example : 312110028381819 < 1181171711293821 := by comp_val
+
+example (h : false) : 0 < 0 := by (try comp_val >> contradiction)
+example (h : false) : 1 < 1 := by (try comp_val >> contradiction)
+example (h : false) : 120201 < 1 := by (try comp_val >> contradiction)
+example (h : false) : 120201 < 32019 := by (try comp_val >> contradiction)
+example (h : false) : 120202 < 1 := by (try comp_val >> contradiction)
+example (h : false) : 120202 < 32019 := by (try comp_val >> contradiction)
+example (h : false) : 120202 < 2 := by (try comp_val >> contradiction)
+example (h : false) : 120202 < 3192 := by (try comp_val >> contradiction)
+
+
+example : 0 ≤ 0 := by comp_val
+example : 0 ≤ 1 := by comp_val
+example : 0 ≤ 2 := by comp_val
+example : 0 ≤ 3 := by comp_val
+example : 0 ≤ 4 := by comp_val
+example : 0 ≤ 5 := by comp_val
+example : 0 ≤ 6 := by comp_val
+example : 0 ≤ 1293821 := by comp_val
+example : 0 ≤ 1293822 := by comp_val
+
+example : 1 ≤ 1 := by comp_val
+example : 1 ≤ 2 := by comp_val
+example : 1 ≤ 3 := by comp_val
+example : 1 ≤ 4 := by comp_val
+example : 1 ≤ 5 := by comp_val
+example : 1 ≤ 6 := by comp_val
+example : 1 ≤ 1293821 := by comp_val
+example : 1 ≤ 1293822 := by comp_val
+
+example : 2 ≤ 2 := by comp_val
+example : 2 ≤ 3 := by comp_val
+example : 2 ≤ 4 := by comp_val
+example : 2 ≤ 5 := by comp_val
+example : 2 ≤ 6 := by comp_val
+example : 2 ≤ 1293821 := by comp_val
+example : 2 ≤ 1293822 := by comp_val
+
+example : 3 ≤ 3 := by comp_val
+example : 3 ≤ 4 := by comp_val
+example : 3 ≤ 5 := by comp_val
+example : 3 ≤ 6 := by comp_val
+example : 3 ≤ 1293821 := by comp_val
+example : 3 ≤ 1293822 := by comp_val
+
+example : 4 ≤ 4 := by comp_val
+example : 4 ≤ 5 := by comp_val
+example : 4 ≤ 6 := by comp_val
+example : 4 ≤ 1293821 := by comp_val
+example : 4 ≤ 1293822 := by comp_val
+
+example : 103093 ≤ 103093 := by comp_val
+example : 103093 ≤ 1293821 := by comp_val
+example : 3121 ≤ 1293822 := by comp_val
+example : 312110028381818 ≤ 1181171711293822 := by comp_val
+example : 312110028381819 ≤ 1181171711293822 := by comp_val
+example : 312110028381819 ≤ 1181171711293821 := by comp_val
+
+example : 1 ≤ 5 := by comp_val
+example : 3 ≤ 5 := by comp_val
+
+example (h : false) : 1 ≤ 0 := by (try comp_val >> contradiction)
+example (h : false) : 2 ≤ 1 := by (try comp_val >> contradiction)
+example (h : false) : 120201 ≤ 1 := by (try comp_val >> contradiction)
+example (h : false) : 120201 ≤ 32019 := by (try comp_val >> contradiction)
+example (h : false) : 120202 ≤ 1 := by (try comp_val >> contradiction)
+example (h : false) : 120202 ≤ 32019 := by (try comp_val >> contradiction)
+example (h : false) : 120202 ≤ 2 := by (try comp_val >> contradiction)
+example (h : false) : 120202 ≤ 3192 := by (try comp_val >> contradiction)
+
+example : 0 ≠ 1 := by comp_val
+example : 0 ≠ 2 := by comp_val
+example : 0 ≠ 3 := by comp_val
+example : 0 ≠ 4 := by comp_val
+example : 0 ≠ 5 := by comp_val
+example : 0 ≠ 6 := by comp_val
+example : 0 ≠ 1293821 := by comp_val
+example : 0 ≠ 1293822 := by comp_val
+
+example : 1 ≠ 0 := by comp_val
+example : 1 ≠ 2 := by comp_val
+example : 1 ≠ 3 := by comp_val
+example : 1 ≠ 4 := by comp_val
+example : 1 ≠ 5 := by comp_val
+example : 1 ≠ 6 := by comp_val
+example : 1 ≠ 1293821 := by comp_val
+example : 1 ≠ 1293822 := by comp_val
+
+example : 2 ≠ 0 := by comp_val
+example : 2 ≠ 1 := by comp_val
+example : 2 ≠ 3 := by comp_val
+example : 2 ≠ 4 := by comp_val
+example : 2 ≠ 5 := by comp_val
+example : 2 ≠ 6 := by comp_val
+example : 2 ≠ 1293821 := by comp_val
+example : 2 ≠ 1293822 := by comp_val
+
+example : 3 ≠ 0 := by comp_val
+example : 3 ≠ 2 := by comp_val
+example : 3 ≠ 1 := by comp_val
+example : 3 ≠ 4 := by comp_val
+example : 3 ≠ 5 := by comp_val
+example : 3 ≠ 6 := by comp_val
+example : 3 ≠ 1293821 := by comp_val
+example : 3 ≠ 1293822 := by comp_val
+
+example : 4 ≠ 0 := by comp_val
+example : 4 ≠ 2 := by comp_val
+example : 4 ≠ 3 := by comp_val
+example : 4 ≠ 1 := by comp_val
+example : 4 ≠ 5 := by comp_val
+example : 4 ≠ 6 := by comp_val
+example : 4 ≠ 1293821 := by comp_val
+example : 4 ≠ 1293822 := by comp_val
+
+example : 5 ≠ 0 := by comp_val
+example : 5 ≠ 2 := by comp_val
+example : 5 ≠ 3 := by comp_val
+example : 5 ≠ 4 := by comp_val
+example : 5 ≠ 1 := by comp_val
+example : 5 ≠ 6 := by comp_val
+example : 5 ≠ 1293821 := by comp_val
+example : 5 ≠ 1293822 := by comp_val
+
+example : 103093 ≠ 103095 := by comp_val
+example : 103093 ≠ 1293821 := by comp_val
+example : 3121 ≠ 1293822 := by comp_val
+example : 312110028381818 ≠ 1181171711293822 := by comp_val
+example : 312110028381819 ≠ 1181171711293822 := by comp_val
+example : 312110028381819 ≠ 1181171711293821 := by comp_val
+
+example (h : false) : 1 ≠ 1 := by (try comp_val >> contradiction)
+example (h : false) : 2 ≠ 2 := by (try comp_val >> contradiction)
+example (h : false) : 120201 ≠ 120201 := by (try comp_val >> contradiction)
+example (h : false) : 32019  ≠ 32019 := by (try comp_val >> contradiction)
+example (h : false) : 120202 ≠ 120202 := by (try comp_val >> contradiction)