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 ***@***.***> 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 = 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. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#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 <#681 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAIOAD2BK4VIFB4APPHTCB3VSOJA3ANCNFSM4HAVXNWA> . You are receiving this because you commented.Message ID: ***@***.***>