FOLDR congruence too weak

[xrchz]

I don't have a great motivating example yet, but I think one might want a congruence more like this for FOLDR (and similarly for FOLDL) than what's currently in DefnBase (it only gives you that the argument to f is a member of l, and doesn't constrain a at all).

val FOLDR_cong = store_thm(
"FOLDR_cong",
``!l l' b b' f f'.
  (l = l') /\ (b = b') /\
  (!x a. (?n. (n < LENGTH l') /\ (x = EL n l') /\
              (a = FOLDR f' b' (DROP (SUC n) l')))
         ==> (f x a = f' x a))
  ==> (FOLDR f b l = FOLDR f' b' l')``,
Induct >> rw[] >> rw[FOLDR] >> fs[] >> 
qsuff_tac `FOLDR f b l = FOLDR f' b l`>- (
  rw[] >>
  first_x_assum match_mp_tac >>
  qexists_tac `0` >> rw[]) >>
first_x_assum match_mp_tac >>
rw[] >>
first_x_assum match_mp_tac >>
qexists_tac `SUC n` >> rw[])

However, the rule above doesn't work as a congruence. I don't know why not.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[mn200]

I think you'd need to find a seriously good motivating example before I lost any sleep on including that monster in the Defnbase....

What happens if you move the (?n ...) out to be a universally quantified n in the last hypothesis?

[konrad-slind]

Probably fails because the hypotheses of the the proposed
cong. theorem are of an unexpected shape, e.g., the code doesn't
know how to push an existential to the assums and skolemize.

As best I remember, the hyps of a cong have the form of

x = x'

or

f x = f x'

or

(x = x') ==> (f x = f x')

(universal quants allowed).

..... anything of any other shape may well not work.

Konrad.

On Mon, Mar 19, 2012 at 12:50 PM, Ramana Kumar
[email protected]
wrote:

I don't have a great motivating example yet, but I think one might want a congruence more like this for FOLDR (and similarly for FOLDL) than what's currently in DefnBase (it only gives you that the argument to f is a member of l, and doesn't constrain a at all).

   val FOLDR_cong = store_thm(
   "FOLDR_cong",
   !l l' b b' f f'.      (l = l') /\ (b = b') /\      (!x a. (?n. (n < LENGTH l') /\ (x = EL n l') /\                  (a = FOLDR f' b' (DROP (SUC n) l')))             ==> (f x a = f' x a))      ==> (FOLDR f b l = FOLDR f' b' l'),
   Induct >> rw[] >> rw[FOLDR] >> fs[] >>
   qsuff_tac FOLDR f b l = FOLDR f' b l>- (
     rw[] >>
     first_x_assum match_mp_tac >>
     qexists_tac 0 >> rw[]) >>
   first_x_assum match_mp_tac >>
   rw[] >>
   first_x_assum match_mp_tac >>
   qexists_tac SUC n >> rw[])

However, the rule above doesn't work as a congruence. I don't know why not.

---

Reply to this email directly or view it on GitHub:
#54