Fix bugs in Nelson-Oppen

1- Purification non longer generates ill-typed terms
2- Equations are proved if types are convertible (instead of equal)

Note that purification is possibly too aggressive. It names every subterm.

Fixes #28

Makefile

@@ -78,9 +78,9 @@ clean : cleanaux
 
 
 TESTSUITE = arith.v  refl_bool.v no_test_lia.v no_test_lra.v
-ISSUES    = issue_2.v issue_3.v issue_5.v issue_6.v issue_8.v issue_9.v issue_10.v \
+ISSUES    =  cnf.v issue_2.v issue_3.v issue_5.v issue_6.v issue_8.v issue_9.v issue_10.v \
 	issue_11.v issue_12.v issue_13.v issue_14.v issue_15.v issue_16.v issue_19.v issue_20.v issue_21.v \
-	issue_22.v issue_23.v issue_cc.v issue_25.v cnf.v
+	issue_22.v issue_23.v issue_cc.v issue_25.v issue_28.v
 
 ALLTESTV = $(addprefix test-suite/,$(TESTSUITE)) $(addprefix issues/,$(ISSUES))
 ALLTESTVO = $(ALLTESTV:.v=.vo)

issues/issue_25.v

 Require Import Cdcl.Itauto.
 Require Import List.
-Require Import cnf.
 
 Goal forall A a a0 (r l l' : list A), (In a l' <-> In a l /\ ~ In a r) ->
 ~ (~ In a0 r) ->

issues/issue_28.v

+From Coq Require Import  ZArith Zify ZifyClasses ZifyBool ZifyInst Lia.
+
+From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp.zify Require Import zify.
+
+
+Require Import Cdcl.NOlia.
+
+Local Open Scope Z_scope.
+
+(* arith on Z *)
+Lemma foo_Z (x : Z) : 1 + x = x + 1.
+Proof. lia. Qed.
+
+(* eq + arith on Z *)
+Lemma foo_f (f : Z -> Z) (x : Z) : f (1 + x) = f (x + 1).
+Proof. smt. Qed.
+
+Import Order.Theory.
+Import GRing.Theory.
+
+Local Open Scope ring_scope.
+
+(* arith on int, thx to mczify's instances *)
+Lemma foo_int (x : int) : 1 + x = x + 1.
+Proof. lia. Qed.
+
+Lemma foo_f_int (f : int -> int) (x : int) : f (1 + x) = f (x + 1).
+Proof.
+  smt.
+Qed.

src/no.ml

@@ -153,6 +153,19 @@ let declared_term thy env evd c a =
     | exception Not_found -> is_arity_op env evd thy c a 1
          
 
+let declared_term thy env evd c a =
+  match declared_term thy env evd c a with
+  | (c',a') ->
+    if debug then Feedback.msg_debug (Pp.(str "declared_term " ++
+                            Printer.pr_econstr_env env evd (EConstr.mkApp(c,a)) ++
+                            str "=>"  ++
+                            Printer.pr_econstr_env env evd (EConstr.mkApp(c',a')) ++
+                            str "\n")) ; (c',a')
+  | exception e -> if debug then     Feedback.msg_debug (Pp.(str "declared_term " ++
+                            Printer.pr_econstr_env env evd (EConstr.mkApp(c,a)) ++
+                            str "=>"  ++ str (Printexc.to_string e) ++
+                            str "\n")) ; raise e
+
 let is_declared_type thy env evd  typS = 
   let typ = EConstr.mkApp(Lazy.force coq_TheoryType,[|thy;typS|]) in
   try 
@@ -182,12 +195,12 @@ let rec remember_term thy env evd senv t =
     ((EConstr.mkVar id, p), senv)
   with Not_found -> (
     let c, a = decompose_app env evd t in
-    let a, p =
+    let c, a, p =
       match declared_term thy env evd c a with
-      | c, a -> (a, Arith)
+      | c, a -> (c, a, Arith)
       | exception Not_found ->
          if isVar evd c && a = [||] && is_declared_type thy env evd  (Retyping.get_type_of env evd c)
-         then (a, Arith) else (a, NonArith)
+         then (c, a, Arith) else (c, a, NonArith)
     in
     let a, senv =
       Array.fold_right
@@ -356,7 +369,7 @@ let no_tacs thy tacl =
                   (EConstr.mkVar (Nameops.add_subscript name sub), typ))
                 l) in
          let ll =
-           all_pairs (EConstr.eq_constr evd) vars in
+           all_pairs (Reductionops.is_conv env evd) vars in
          if debug
          then
            (Feedback.msg_debug Pp.(pr_enum (Printer.pr_econstr_env env evd) (List.map fst vars));