From 21bad7cb970f5341be22dcc88339f9cc3d9e1bb1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 23 Nov 2016 13:19:54 -0800
Subject: [PATCH] feat(library/init/meta/comp_value_tactics): add support for
 char/string/fin at comp_val tactic

---
 library/init/meta/comp_value_tactics.lean | 51 ++++++++++++++++-------
 src/library/vm/vm_expr.cpp                | 15 +++++++
 tests/lean/run/comp_val2.lean             | 16 +++++++
 3 files changed, 66 insertions(+), 16 deletions(-)
 create mode 100644 tests/lean/run/comp_val2.lean

diff --git a/library/init/meta/comp_value_tactics.lean b/library/init/meta/comp_value_tactics.lean
index 3ef84fb781..3abd339638 100644
--- a/library/init/meta/comp_value_tactics.lean
+++ b/library/init/meta/comp_value_tactics.lean
@@ -9,6 +9,9 @@ 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
+meta constant mk_fin_val_ne_proof : expr → expr → option expr
+meta constant mk_char_val_ne_proof : expr → expr → option expr
+meta constant mk_string_val_ne_proof : expr → expr → option expr
 
 namespace tactic
 open expr
@@ -16,27 +19,43 @@ 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),
+   (do is_def_eq 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 is_def_eq type (const `char []),
+       (a, b) ← returnopt (is_ne t),
+       pr     ← returnopt (mk_char_val_ne_proof a b),
        exact pr)
    <|>
-   (do (a, b) ← returnopt (is_lt t),
-       pr     ← returnopt (mk_nat_val_lt_proof a b),
+   (do is_def_eq type (const `string []),
+       (a, b) ← returnopt (is_ne t),
+       pr     ← returnopt (mk_string_val_ne_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),
+   (do type   ← whnf type,
+       guard (is_app_of type `fin),
+       (a, b) ← returnopt (is_ne t),
+       pr     ← returnopt (mk_fin_val_ne_proof a b),
        exact pr)
    <|>
    (do (a, b) ← returnopt (is_eq t),
-       unify a b, to_expr `(eq.refl %%a) >>= exact)
+        unify a b, to_expr `(eq.refl %%a) >>= exact)
 end tactic
diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp
index 53c21cbc30..0f5ca3d215 100644
--- a/src/library/vm/vm_expr.cpp
+++ b/src/library/vm/vm_expr.cpp
@@ -336,6 +336,18 @@ 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)));
 }
 
+vm_obj vm_mk_fin_val_ne_proof(vm_obj const & a, vm_obj const & b) {
+    return to_obj(mk_fin_val_ne_proof(to_expr(a), to_expr(b)));
+}
+
+vm_obj vm_mk_char_val_ne_proof(vm_obj const & a, vm_obj const & b) {
+    return to_obj(mk_char_val_ne_proof(to_expr(a), to_expr(b)));
+}
+
+vm_obj vm_mk_string_val_ne_proof(vm_obj const & a, vm_obj const & b) {
+    return to_obj(mk_string_val_ne_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);
@@ -373,6 +385,9 @@ void initialize_vm_expr() {
     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);
+    DECLARE_VM_BUILTIN(name("mk_fin_val_ne_proof"),        vm_mk_fin_val_ne_proof);
+    DECLARE_VM_BUILTIN(name("mk_char_val_ne_proof"),       vm_mk_char_val_ne_proof);
+    DECLARE_VM_BUILTIN(name("mk_string_val_ne_proof"),     vm_mk_string_val_ne_proof);
 }
 
 void finalize_vm_expr() {
diff --git a/tests/lean/run/comp_val2.lean b/tests/lean/run/comp_val2.lean
new file mode 100644
index 0000000000..c293784af8
--- /dev/null
+++ b/tests/lean/run/comp_val2.lean
@@ -0,0 +1,16 @@
+open tactic
+
+example : #"a" ≠ #"b" := by comp_val
+example : #"0" ≠ #"a" := by comp_val
+
+example : "hello worlg" ≠ "hhello world" := by comp_val
+example : "hello world" ≠ "hhello world" := by comp_val
+example : "abc" ≠ "cde" := by comp_val
+example : "abc" ≠ "" := by comp_val
+example : "" ≠ "cde" := by comp_val
+
+example : @fin.mk 5 3 dec_trivial ≠ @fin.mk 5 4 dec_trivial :=
+by comp_val
+
+example : @fin.mk 5 4 dec_trivial ≠ @fin.mk 5 1 dec_trivial :=
+by comp_val