cc bug

Stream: mathlib4

[Patrick Massot]

I’ve found the following bug:

import Mathlib.Tactic


example (n k : ℤ) (hnk : n = 2 * k + 1)
    (hk : (2 * k + 1) * (2 * k + 1 + 1) = 2 * ((2 * k + 1) * (k + 1))) :
    n * (n + 1) = 2 * ((2 * k + 1) * (k + 1)) := by
  -- rw [hnk]
  -- exact hk
  cc

The commented out proof works fine, but cc raises a PANIC at outOfBounds Init.GetElem:11:2: index out of bounds.

[Patrick Massot]

I guess cc runs in circles but I’m not even sure. I would really appreciate some help because I have no idea how cc is meant to work.

[Patrick Massot]

Needless to say, this is a minimized example. I know using cc here is stupid.

[Patrick Massot]

@Miyahara Kō

[Patrick Massot]

@Anne Baanen

[Miyahara Kō]

OK, I'll work on it right away.

[Patrick Massot]

Thanks!

[Miyahara Kō]

I have fixed this bug and I'm creating the PR, but I'm going to attend to the meeting in my internship company now so I just tell the solution for now.

In Mathlib.Tactic.CC.Datatypes, replacing

/-- Ordering on `ACApps` sorts `.ofExpr` before `.apps`, and sorts `.apps` by function symbol,
  then by shortlex order. -/
scoped instance : Ord ACApps where
  compare
    | .ofExpr a, .ofExpr b => compare a b
    | .ofExpr _, .apps _ _ => .lt
    | .apps _ _, .ofExpr _ => .gt
    | .apps op₁ args₁, .apps op₂ args₂ =>
      compare op₁ op₂ |>.then <| compare args₁.size args₂.size |>.then <| Id.run do
        for i in [:args₁.size] do
          let o := compare args₁[i]! args₂[i]!
          if o != .eq then return o
        return .eq

with

@[macro_inline] private def _root_.Ordering.dthen :
    (o : Ordering) → (o = .eq → Ordering) → Ordering
  | .eq, f => f rfl
  | o, _ => o

/-- Ordering on `ACApps` sorts `.ofExpr` before `.apps`, and sorts `.apps` by function symbol,
  then by shortlex order. -/
scoped instance : Ord ACApps where
  compare
    | .ofExpr a, .ofExpr b => compare a b
    | .ofExpr _, .apps _ _ => .lt
    | .apps _ _, .ofExpr _ => .gt
    | .apps op₁ args₁, .apps op₂ args₂ =>
      compare op₁ op₂ |>.then <| compare args₁.size args₂.size |>.dthen <| fun hs => Id.run do
        for hi : i in [:args₁.size] do
          let o :=
            compare (args₁[i]'hi.right) (args₂[i]'(Batteries.BEqCmp.cmp_iff_eq.mp hs ▸ hi.right))
          if o != .eq then return o
        return .eq

fixes the bug.

[Miyahara Kō]

#20422

[Patrick Massot]

Great, thanks a lot for the very quick fix!

[Patrick Massot]

@Mario Carneiro do you have any comment about why Ordering.then was not short-circuiting as advertised here?

[Mario Carneiro]

@Patrick Massot it uses the same technique as ite and Bool.or to do short circuiting, namely @[macro_inline]

[Mario Carneiro]

this is a slightly brittle method, and a fair number of lean functions use unit functions instead, but I would prefer not to change the type signature if possible

[Mario Carneiro]

I blame the compiler for any issues here

[Mario Carneiro]

Seems like the difference is in the way the match is written:

bad:

@[macro_inline] def «then» : Ordering → Ordering → Ordering
  | .eq, f => f
  | o, _ => o

-- equivalent to
@[macro_inline] def «then» (a b : Ordering) : Ordering :=
  match a, b with
  | .eq, f => f
  | o, _ => o

good:

@[macro_inline] def «then» (a b : Ordering) : Ordering :=
  match a with
  | .eq => b
  | a => a

@Kim Morrison ^ can you PR this?

[Mario Carneiro]

The double match seems to get desugared to a primitive match with some let __discr := ... lines before it, which foils the macro_inline since it causes both arguments to be evaluated before the match

[Mario Carneiro]

note that Bool.and and Bool.or are already written in this style, and I seem to recall needing to do this for an option combinator as well (although Option.orElse uses the unit function style since I'm not sure when, and Option.or, while it could benefit from this transformation, seems to be deliberately documented as strict in the right argument even though it uses macro_inline)

[Patrick Massot]

Thanks Mario! It’s nice (and very useful!) to have you back.

[Kim Morrison]

Mario Carneiro said:

Seems like the difference is in the way the match is written:

bad:

@[macro_inline] def «then» : Ordering → Ordering → Ordering
  | .eq, f => f
  | o, _ => o

-- equivalent to
@[macro_inline] def «then» (a b : Ordering) : Ordering :=
  match a, b with
  | .eq, f => f
  | o, _ => o

good:

@[macro_inline] def «then» (a b : Ordering) : Ordering :=
  match a with
  | .eq => b
  | a => a

Kim Morrison ^ can you PR this?

Can you provide some code that shows a difference?

[Mario Carneiro]

@Kim Morrison

def foo (a : List ℕ) := Ordering.then (compare a.length 1) (compare a[0]! 1)
#eval foo []

this panics with the bad definition of then and succeeds with Ordering.lt for the good definition

[Kim Morrison]

Fixed in lean#6907.