Array.Mem

Stream: lean4

[Joe Hendrix]

I saw a curious use of a structure on the Array Membership instance:

/-- `a ∈ as` is a predicate which asserts that `a` is in the array `a s`. -/
-- NB: This is defined as a structure rather than a plain def so that a lemma
-- like `sizeOf_lt_of_mem` will not apply with no actual arrays around.
structure Mem (a : α) (as : Array α) : Prop where
  val : a ∈ as.data

instance : Membership α (Array α) where
  mem a as := Mem a as

...

theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a < sizeOf as := by
  ...

Is this use of a structure still needed? I noticed other Membership instances don't always use a structure.

[Mario Carneiro]

This was a recent change

[Mario Carneiro]

lean4#2774

[Joe Hendrix]

Thanks. I should have checked git blame before asking.

[Notification Bot]

Joe Hendrix has marked this topic as resolved.

[Mario Carneiro]

I'm still not sure whether a structure is the right solution here, we don't normally use structures for this

[Mario Carneiro]

e.g. instance : LT (Fin n) is just a def

[Notification Bot]

Joe Hendrix has marked this topic as unresolved.

[Joe Hendrix]

I just stumbled across this class while working through potential definitions for a Vector class, so it's not blocking me, but it'd be good to understand the issue a bit better so I do the right thing for Vector.

[Mario Carneiro]

The rationale given is:

The definition for a ∈ as is intentionally not defeq to a ∈ as.data so that the termination tactics for Arrays don’t spuriously apply when recursing through lists.

but I don't see why this is a problem, and/or why fixing the relevant tactics doesn't work

[Mario Carneiro]

@Joachim Breitner

[Joe Hendrix]

There's a comment in lean4#2774 with a bit more detail, but I think it'd be great to have some clarity.

[Joachim Breitner]

Maybe fixing the tactic would work; I didn’t dare to touch the List stuff when I was dabbling with Array. If someone has a better plan, please by all means implement it.

[Joachim Breitner]

The problem was that

macro "array_mem_dec" : tactic =>
  `(tactic| first
    | apply Array.sizeOf_lt_of_mem; assumption; done
    | apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
      case' h => assumption
      simp_arith)

should look for a ∈ as in the context. If that’s defeq to a ∈ as.data, it would match x ∈ xs (here xs being a normal list, no arrays around)

[Mario Carneiro]

More specifically, is there a test case that fails without this?

[Joachim Breitner]

Yes, otherwise I wouldn't even have noticed :-)

[Mario Carneiro]

was it checked in?

[Joachim Breitner]

It was already there

[Joachim Breitner]

tests/lean/run/wfForIn.lean for example, based on my comments at the PR

[Joachim Breitner]

Maybe I did something wrong, of course. OR maybe a def with some annotation that prevents reduction would be more idiomatic.

[Mario Carneiro]

MWE:

structure Array' (α : Type u) where
  data : List α

namespace Array'

def size (as : Array' α) : Nat := as.data.length
def get (as : Array' α) (i : Fin as.size) : α := as.data.get i

def Mem (a : α) (as : Array' α) : Prop := a ∈ as.data

instance : Membership α (Array' α) where
  mem a as := Mem a as

theorem sizeOf_lt_of_mem [SizeOf α] {as : Array' α} (h : a ∈ as) : sizeOf a < sizeOf as :=
  sorry

@[simp] theorem sizeOf_get [SizeOf α] (as : Array' α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as :=
  sorry

macro "array'_mem_dec" : tactic =>
  `(tactic| first
    | apply Array'.sizeOf_lt_of_mem; assumption; done
    | apply Nat.lt_trans (Array'.sizeOf_lt_of_mem ?h)
      case' h => assumption
      simp_arith)

macro_rules | `(tactic| decreasing_trivial) => `(tactic| array'_mem_dec)

inductive Term where
  | app (f : String) (args : List Term)

def printFns : Term → IO Unit
  | Term.app f args => do
    IO.println f
    for h : arg in args do
      have : sizeOf arg < 1 + sizeOf f + sizeOf args := Nat.lt_trans (List.sizeOf_lt_of_mem h) (by simp_arith)
      printFns arg

[Joachim Breitner]

Thanks for MWE’ing.

@[irreducible]
def Mem (a : α) (as : Array' α) : Prop := a ∈ as.data

seems to help. Is that preferable?

[Mario Carneiro]

Alternatively:

macro "array'_mem_dec" : tactic =>
  `(tactic| first
    | apply Array'.sizeOf_lt_of_mem; assumption; done
    | with_reducible apply Nat.lt_trans (Array'.sizeOf_lt_of_mem ‹_›)
      simp_arith)

[Eric Wieser]

Should that be with_reducible assumption?

[Mario Carneiro]

you could also put with_reducible first ...

[Mario Carneiro]

I figure for the first case it doesn't matter though since if it closed the goal then no problemo

[Joe Hendrix]

What sort of example is in mind for the Nat.lt_trans case?

[Mario Carneiro]

the example at the end is pretty similar to what kind of thing would require that case

[Mario Carneiro]

you prove sizeOf arg < 1 + sizeOf f + sizeOf args by transitivity on sizeOf arg < sizeOf args and sizeOf args <= 1 + sizeOf f + sizeOf args and solve the latter with simp_arith

[Joe Hendrix]

Yep that makes sense.

[Joe Hendrix]

I think ideally there would be some sort of chaining where a linear arithmetic procedure queried for additional facts about the terms it treats as uninterpreted variable, but that's out of scope for now.

[Mario Carneiro]

I think what happens when this mistakenly applies in the list case is that you instead get the subgoal sizeOf { data := args } <= 1 + sizeOf f + sizeOf args (where the LHS was able to unify because of eta for structures) and sizeOf { data := args } is larger, I think 1 + sizeOf args, which makes it harder to prove

[Mario Carneiro]

IMO simp_arith is overkill here, it should be something more tailored to this kind of goal

[Joe Hendrix]

I think for now, I'd recommend using @Mario Carneiro's tactic. That's what I'll add for Vector.

[Mario Carneiro]

the lean3 version of this tactic would just try x <= x + y and y <= x + y with backtracking

[Mario Carneiro]

but maybe simp_arith is better suited to the case where the user overrides the decreasing metric and now you have more interesting and arbitrary goals

[Joachim Breitner]

My (preliminary) impression is that the termination tactics are not quite compositional, and may need an overhaul. For example, what if I nest multiple data structures; list of list of list. I’d expect the default tactic setup to use all the List.Mem assumptions and still arrive at the result. But unless I am mistaken, the current setup of decreasing_trivial is that is handles a finite set of typical cases, but only if it can solve them completely.

Or maybe once we have omega the the tactic will first make all the < facts known (by changing List.Mem assumptions to <) and then simply call omega.

[Joe Hendrix]

Yeah, I think the current approach is too specific. It'd be great to have a fast omega tactic with a mechanism for pulling < facts out of the environment (using lemmas such as sizeOf_lt_of_mem automatically).

[Joe Hendrix]

At least in the example above, forward chaining would probably provide be a good approach by seeing arg ∈ args in the hypotheses and automatically synthesizing sizeOf arg < sizeOf args.

Are there existing general forward chaining tactics in Lean?

[Mario Carneiro]

there is apply at in mathlib, we could use apply thm at * to mean forward chaining

[Mario Carneiro]

usually have is used for forward chaining but it isn't easy to say

for $h in context do
  try
    have := thm $h