Congruence rule in TFL depends on bound variable

[mn200]

In the following, valueOf extracts a value from a monad ('a M -> 'a). This is possible, for example, in a writer monad. In something like the option monad, you'd have SOME xxxx = m1 as the precondition to the equality on fm1 and fm2.

val bind_cong = store_thm(
  "bind_cong[defncong]",
  ``!m1 m2 fm1 fm2. (m1 = m2) /\ (!xxxx. xxxx = valueOf m1 ==> fm1 xxxx = fm2 xxxx) ==>
      (bind m1 fm1 = bind m2 fm2)``,
  rw[bind_def, valueOf_def] >>
  Cases_on `m1` >>
  Cases_on `r` >>
  fs[]);

Now, using xxxx below causes an error:

val fooM_def = Define`
    fooM b =
      do
        if b = 0 then return 0
        else do
             (* no problem if xxxx is replaced by x *)
               xxxx <- incM b;
               y <- decM b;
               fooM y;
             od
      od
`;

Discovered by Joseph Chan.

[konrad-slind]

Not sure the congruence rule is quite right. You have

m1 = m2

but then the next clause

(!xxxx. xxxx = valueOf m1 ==> fm1 xxxx = fm2 xxxx)

takes valueOf m1, instead of valueOf m2, which is what TFL's handling of congruence rules assumes.

Konrad.

On Sun, Mar 24, 2019 at 5:50 AM Michael Norrish [email protected] wrote:

In the following, valueOf extracts a value from a monad ('a M -> 'a). This is possible, for example, in a writer monad. In something like the option monad, you'd have SOME xxxx = m1 as the precondition to the equality on fm1 and fm2.

val bind_cong = store_thm( "bind_cong[defncong]", !m1 m2 fm1 fm2. (m1 = m2) /\ (!xxxx. xxxx = valueOf m1 ==> fm1 xxxx = fm2 xxxx) ==> (bind m1 fm1 = bind m2 fm2), rw[bind_def, valueOf_def] >> Cases_on m1 >> Cases_on r >> fs[]);

Now, using xxxx below causes an error:

val fooM_def = DefinefooM b = do if b = 0 then return 0 else do (* no problem if xxxx is replaced by x *) xxxx <- incM b; y <- decM b; fooM y; od od;

Discovered by Joseph Chan.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/681, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgD3aeRBsnu9gZJPKQ4NGJP7pTuu74ks5vZ1iDgaJpZM4cFbts .

[mn200]

The following is perhaps simpler, and I think is probably/possibly the same bug:

Datatype:
  tree = Lf | Nd tree (tree option)
End

Definition foo_def:
  foo Lf = Lf ∧
  foo (Nd x topt) =
  let x' = foo x ;
      topt' = OPTION_MAP foo topt ;
  in
    Nd x' topt'
Termination
  cheat
End

The variable x appears in the OPTION_MAP congruence rule. If you substitute out the first let-binding, so that you have Nd (foo x) topt' after the in it works again. It also works with both let-bindings if you use a name other than x under Nd. The congruence rule in question is

⊢ ∀opt1 opt2 f1 f2.
    opt1 = opt2 ∧ (∀x. opt2 = SOME x ⇒ f1 x = f2 x) ⇒
    OPTION_MAP f1 opt1 = OPTION_MAP f2 opt2

[konrad-slind]

Thanks for the simple example. Looks like a revisit to the congruence-rule instantiation code in the TC extractor.

On Mon, Jul 4, 2022 at 8:57 PM Michael Norrish @.***> wrote:

The following is perhaps simpler, and I think is probably/possibly the same bug:

Datatype:

tree = Lf | Nd tree (tree option)

End

Definition foo_def:

foo Lf = Lf ∧

foo (Nd x topt) =

let x' = foo x ;

  topt' = OPTION_MAP foo topt ;

in

Nd x' topt'

Termination

cheat

End

The variable x appears in the OPTION_MAP congruence rule. If you substitute out the first let-binding, so that you have Nd (foo x) topt' after the in it works again. It also works with both let-bindings if you use a name other than x under Nd. The congruence rule in question is

⊢ ∀opt1 opt2 f1 f2.

opt1 = opt2 ∧ (∀x. opt2 = SOME x ⇒ f1 x = f2 x) ⇒

OPTION_MAP f1 opt1 = OPTION_MAP f2 opt2

— Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/681#issuecomment-1174518521, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIOAD2BK4VIFB4APPHTCB3VSOJA3ANCNFSM4HAVXNWA . You are receiving this because you commented.Message ID: @.***>