From 6da1b447f048cf8cdc34934b99aaff2244a2d593 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Jan 2014 00:21:05 -0800
Subject: [PATCH] fix(library/hop_match): do not match iff with =

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/hop_match.cpp        | 66 ++++++++++++++------------------
 tests/lean/nnf.lean              | 16 ++++++++
 tests/lean/nnf.lean.expected.out |  8 ++++
 3 files changed, 52 insertions(+), 38 deletions(-)
 create mode 100644 tests/lean/nnf.lean
 create mode 100644 tests/lean/nnf.lean.expected.out

diff --git a/src/library/hop_match.cpp b/src/library/hop_match.cpp
index ce60f6caa3..546398590c 100644
--- a/src/library/hop_match.cpp
+++ b/src/library/hop_match.cpp
@@ -272,46 +272,36 @@ class hop_match_fn {
             return match_constant(p, t);
         }
 
-        if (is_equality(p) && is_equality(t) && (!is_eq(p) || !is_eq(t))) {
-            // Remark: if p and t are homogeneous equality, then we handle as an application (in the else branch)
-            // We do that because we can get more information. For example, the pattern
-            // may be    (eq #1 a b).
-            // This branch ignores the type.
-            expr_pair p1 = get_equality_args(p);
-            expr_pair p2 = get_equality_args(t);
-            return match(p1.first, p2.first, ctx, ctx_size) && match(p1.second, p2.second, ctx, ctx_size);
-        } else {
-            if (p.kind() != t.kind())
-                return false;
-            switch (p.kind()) {
-            case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type:
-            case expr_kind::Value: case expr_kind::MetaVar:
-                return false;
-            case expr_kind::App: {
-                unsigned i1 = num_args(p);
-                unsigned i2 = num_args(t);
-                while (i1 > 0 && i2 > 0) {
-                    --i1;
-                    --i2;
-                    if (i1 == 0 && i2 > 0) {
-                        return match(arg(p, i1), mk_app(i2+1, begin_args(t)), ctx, ctx_size);
-                    } else if (i2 == 0 && i1 > 0) {
-                        return match(mk_app(i1+1, begin_args(p)), arg(t, i2), ctx, ctx_size);
-                    } else {
-                        if (!match(arg(p, i1), arg(t, i2), ctx, ctx_size))
-                            return false;
-                    }
+        if (p.kind() != t.kind())
+            return false;
+        switch (p.kind()) {
+        case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type:
+        case expr_kind::Value: case expr_kind::MetaVar:
+            return false;
+        case expr_kind::App: {
+            unsigned i1 = num_args(p);
+            unsigned i2 = num_args(t);
+            while (i1 > 0 && i2 > 0) {
+                --i1;
+                --i2;
+                if (i1 == 0 && i2 > 0) {
+                    return match(arg(p, i1), mk_app(i2+1, begin_args(t)), ctx, ctx_size);
+                } else if (i2 == 0 && i1 > 0) {
+                    return match(mk_app(i1+1, begin_args(p)), arg(t, i2), ctx, ctx_size);
+                } else {
+                    if (!match(arg(p, i1), arg(t, i2), ctx, ctx_size))
+                        return false;
                 }
-                return true;
-            }
-            case expr_kind::Lambda: case expr_kind::Pi:
-                return
-                    match(abst_domain(p), abst_domain(t), ctx, ctx_size) &&
-                    match(abst_body(p), abst_body(t), extend(ctx, abst_name(t), abst_domain(t)), ctx_size+1);
-            case expr_kind::Let:
-                // TODO(Leo)
-                return false;
             }
+            return true;
+        }
+        case expr_kind::Lambda: case expr_kind::Pi:
+            return
+                match(abst_domain(p), abst_domain(t), ctx, ctx_size) &&
+                match(abst_body(p), abst_body(t), extend(ctx, abst_name(t), abst_domain(t)), ctx_size+1);
+        case expr_kind::Let:
+            // TODO(Leo)
+            return false;
         }
         lean_unreachable();
     }
diff --git a/tests/lean/nnf.lean b/tests/lean/nnf.lean
new file mode 100644
index 0000000000..04308f0225
--- /dev/null
+++ b/tests/lean/nnf.lean
@@ -0,0 +1,16 @@
+rewrite_set NNF
+add_rewrite not_not_eq not_true not_false not_neq not_and not_or not_iff not_implies not_forall
+            not_exists forall_and_distribute exists_and_distributer exists_and_distributel : NNF
+
+variable p : Nat → Nat → Bool
+variable f : Nat → Nat
+variable g : Nat → Nat → Nat
+
+(*
+local t1     = parse_lean('¬ ∀ x, (∃ y, p x y ∨ p (f x) (f y)) ∨ f 0 = 1')
+local t2, pr = simplify(t1, "NNF")
+print(t1)
+print("====>")
+print(t2)
+get_environment():type_check(pr)
+*)
diff --git a/tests/lean/nnf.lean.expected.out b/tests/lean/nnf.lean.expected.out
new file mode 100644
index 0000000000..292466ccbd
--- /dev/null
+++ b/tests/lean/nnf.lean.expected.out
@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: p
+  Assumed: f
+  Assumed: g
+¬ (∀ x : ℕ, (∃ y : ℕ, p x y ∨ p (f x) (f y)) ∨ f 0 = 1)
+====>
+(∃ x : ℕ, (∀ x::1 : ℕ, ¬ p x x::1) ∧ (∀ x::1 : ℕ, ¬ p (f x) (f x::1))) ∧ ¬ f 0 = 1