Changes in COND_ELIM_CONV and SUB_AND_COND_ELIM_CONV

[binghe]

Hi,

I occasionally found that the outputs of two COND-elimination conversions COND_ELIM_CONV and SUB_AND_COND_ELIM_CONV have changed w.r.t. their documentation, for instance:

> COND_ELIM_CONV ``!f n. f (if (SUC n = 0) then 0 else (SUC n - 1)) < (f n) + 1``;
(new)
|- (!f n. f (if SUC n = 0 then 0 else SUC n - 1) < f n + 1) <=>
    !f n. (SUC n = 0 ==> f 0 < f n + 1) /\
          (SUC n <> 0 ==> f (SUC n - 1) < f n + 1)

(old)
|- (!f n. (f(if (SUC n = 0) then 0 else (SUC n) - 1)) < ((f n) + 1)) =
   (!f n.
     (~(SUC n = 0) \/ (f 0) < ((f n) + 1)) /\
     ((SUC n = 0) \/ (f((SUC n) - 1)) < ((f n) + 1)))

> COND_ELIM_CONV ``!f n. (\m. f (if (m = 0) then 0 else (m - 1))) (SUC n) < (f n) + 1``;
(new)
|- (!f n. (\m. f (if m = 0 then 0 else m - 1)) (SUC n) < f n + 1) <=>
    !f n. (\m. if m = 0 then f 0 else f (m - 1)) (SUC n) < f n + 1: thm

(old)
|- (!f n. ((\m. f(if (m = 0) then 0 else m - 1))(SUC n)) < ((f n) + 1)) =
   (!f n. ((\m. (if (m = 0) then f 0 else f(m - 1)))(SUC n)) < ((f n) + 1))
}

> SUB_AND_COND_ELIM_CONV
   ``((p + 3) <= n) ==> (!m. (if (m = 0) then (n - 1) else (n - 2)) > p)``;
(new)
|- p + 3 <= n ==> (!m. (if m = 0 then n - 1 else n - 2) > p) <=>
   p + 3 <= n ==> !m. (m = 0 ==> p + 1 < n) /\ (m <> 0 ==> p + 2 < n) :thm

(old)
|- (p + 3) <= n ==> (!m. (if (m = 0) then n - 1 else n - 2) > p) =
   (p + 3) <= n ==>
   (!m. (~(m = 0) \/ n > (1 + p)) /\ ((m = 0) \/ n > (2 + p)))

> SUB_AND_COND_ELIM_CONV
   ``!f n. f (if (SUC n = 0) then 0 else (SUC n - 1)) < (f n) + 1``;
(new)
|- (!f n. f (if SUC n = 0 then 0 else SUC n - 1) < f n + 1) <=>
    !f n d.
        (1 = SUC (n + d) ==> (SUC n = 0 ==> f 0 < f n + 1) /\
                             (SUC n <> 0 ==> f 0 < f n + 1)) /\
        (SUC n = 1 + d ==> (SUC n = 0 ==> f 0 < f n + 1) /\
                           (SUC n <> 0 ==> f d < f n + 1)) :thm
(old)
|- (!f n. (f(if (SUC n = 0) then 0 else (SUC n) - 1)) < ((f n) + 1)) =
   (!f n.
     (~(SUC n = 0) \/ (f 0) < ((f n) + 1)) /\
     ((SUC n = 0) \/ (f((SUC n) - 1)) < ((f n) + 1)))
}

I didn't investigate how the changes have happened (I don't even know if the documentation is correct). But basically this looks like their behavior depends on global simplifiers when "lift_disj_eq", "lift_imp_disj" were added into std_ss. If these conversions are used underlying other higher level tools, this changes may lead to subtle bugs if the higher level code was expecting only Boolean conjunctions and disjunctions.

For this reason (mostly), in PR #1043 I ported CONDS_ELIM_CONV and CONDS_CELIM_CONV from HOL-Light, the former seems have the "old" behavior of the existing COND_ELIM_CONV.

Regards,

Chun Tian

[mn200]

I think the changes here were earlier than the disjunction-fiddling with the simplifier. Certainly, the simplifier is not used in the implementation. git log reveals likely changes in 6e5a9e36d6 and 4d7be3baba1. See also issues #642 and #561 (referred to by those commits)

[mn200]

See also issue #6. As long as the implementation keeps the example there efficient, I don't mind what it does. I agree that the use of implication is perhaps unfortunate (could clearly just use disjunctions).

[binghe]

Hi, thanks for the additional information. I don't understand #642 but I tried the sample in #561:

?!m. ((m = n) \/ m < n) /\ ((if m < n then f m else a) = x)

e (CONV_TAC(ONCE_DEPTH_CONV COND_ELIM_CONV));

Currently the existing COND_ELIM_CONV cannot eliminate if ... then ... else in the above goal (i.e. the goal is unchanged after the above tactics) but the new CONDS_ELIM_CONV that I ported from HOL-Light does an even better job then HOL4-K10:

> val it =
   Initial goal:

   ?!m. (m = n \/ m < n) /\ (if m < n then f m else a) = x: proof
> e (CONV_TAC(ONCE_DEPTH_CONV CONDS_ELIM_CONV));
OK..
1 subgoal:
val it =   
   ?!m. m < n /\ f m = x \/ ~(m < n) /\ m = n /\ a = x   
   : proof

Perhaps we consider promoting this CONDS_ELIM_CONV as the new COND_ELIM_CONV (and just remove the old one)?

As for SUB_COND_ELIM_CONV, now I see from https://github.com/HOL-Theorem-Prover/HOL/commit/6e5a9e36d6d031abe391f08107745b61a91da7ee that, the conversion is based on the following theorems in arithmeticTheory:

   [SUB_ELIM_THM]  Theorem      
      ⊢ P (a − b) ⇔ ∀d. (b = a + d ⇒ P 0) ∧ (a = b + d ⇒ P d)

   [SUB_ELIM_THM_EXISTS]  Theorem      
      ⊢ P (a − b) ⇔ (∃d. b = a + d ∧ P 0) ∨ ∃d. a = b + d ∧ P d

I think they are not very good because P occurs twice in the rhs of the theorem, and this will cause some blowups whenever a subtraction gets eliminated. Perhaps in the future we can try the following alternative theorems I ported from HOL-Light, where P only occurs once in rhs:

   [SUB_ELIM_THM']  Theorem
      ⊢ P (a − b) ⇔ ∀d. a = b + d ∨ a < b ∧ d = 0 ⇒ P d

   [SUB_ELIM_THM_EXISTS']  Theorem
      ⊢ P (a − b) ⇔ ∃d. (a = b + d ∨ a < b ∧ d = 0) ∧ P d

But maybe it's better to rename the two theorems to following the existing naming conventions. (Currently the above theorems are used in Grobner.sml for the elimination of subtractions as HOL-Light doesn't have SUB_COND_ELIM_CONV.

[binghe]

Following the last piece of discussions in #1043. For the following example term in #6:

val tm = ``x - PRE i - SUC (PRE i - PRE i) = 0``;

If I simply replace the two theorems used in function find_elim (Sub_and_cond.sml), then the resulting new SUB_AND_COND_ELIM_CONV seems not only faster but produces shorter results:

> time Sub_and_cond.SUB_AND_COND_ELIM_CONV tm;
runtime: 0.00033s,    gctime: 0.00000s,     systime: 0.00000s.
val it =
   |- x - PRE i - SUC (PRE i - PRE i) = 0 <=>
      !d. (1 = i + d ==> x <= SUC 0) /\ (i = 1 + d ==> x <= SUC d): thm

> time SUB_AND_COND_ELIM_CONV tm;
runtime: 0.00015s,    gctime: 0.00000s,     systime: 0.00000s.
val it = |- x - PRE i - SUC (PRE i - PRE i) = 0 <=> x <= i - 1 + SUC 0: thm

But, for a reason that I failed to debug out, the new SUB_AND_COND_ELIM_CONV doesn't work on the selftest term, where "Existential in implication on left", in src/num/arith/src/selftest.sml:

val tm' = “(2 < j ==> ?u. 0 < u ∧ u <= j − 1) ∧ 0 < j ==> 1 <= j”;

> time Sub_and_cond.SUB_AND_COND_ELIM_CONV tm';
runtime: 0.00052s,    gctime: 0.00000s,     systime: 0.00000s.
val it =
   |- (2 < j ==> ?u. 0 < u /\ u <= j - 1) /\ 0 < j ==> 1 <= j <=>
      (2 < j ==> ?u. (?d. 1 = j + d /\ 0 < u /\ u <= 0) \/ ?d. j = 1 + d /\ 0 < u /\ u <= d) /\
      0 < j ==>
      1 <= j: thm

> time SUB_AND_COND_ELIM_CONV tm';
runtime: 0.00023s,    gctime: 0.00000s,     systime: 0.00000s.
Exception- UNCHANGED raised

[binghe]

Furthermore, I found that the existing Sub_and_cond.COND_ELIM_CONV has some knowledge on integer arithmetics, and it can also do ABS_CONV:

> Sub_and_cond.COND_ELIM_CONV ``(\x. if b then f x else g x)``;
<<HOL message: inventing new type variable names: 'a, 'b>>
val it = |- (\x. if b then f x else g x) = if b then (\x. f x) else (\x. g x): thm

The similar normalForms.CONDS_CELIM_CONV I ported from HOL-Light cannot do above conversions, although it works on the sample terms given in the help document of COND_ELIM_CONV (as in the issue main contents).

I think those new elimination theorems from HOL-Light are better, but some additional work is required to make all existing test cases still passing. I felt great difficulties when trying to debug the functions find_elim (and also the similar find_celim) due to the way it was written...

[binghe]

Also, note that the changed SUB_AND_COND_CONV produces x <= i - 1 + SUC 0 for the example in #6. I don't know which arithmetic conversion can further convert SUC 0 to 1 but if it's added as an additional step, the overall result should be in general better.

P. S. It seems that i - 1 + 1 cannot be further simplified to just i because (I guess) if i = 0 then i - 1 + 1 = 0 - 1 + 1 = 0 + 1 = 1 <> i.