grind and cofinite quantification

Stream: general

[Chris Henson]

I am using grind for the first time with Cslib's locally nameless STLC. A problem I've run into is how to handle cofinite quantification. Here is a minimized mwe:

import Mathlib

universe u

variable {Var : Type u}

inductive Term (Var : Type u)
| bvar : ℕ → Term Var
| fvar : Var → Term Var
| abs  : Term Var → Term Var
| app  : Term Var → Term Var → Term Var

namespace Term

/-- Variable opening of the ith bound variable. -/
@[grind =]
def openRec (i : ℕ) (sub : Term Var) : Term Var → Term Var
| bvar i' => if i = i' then sub else bvar i'
| fvar x  => fvar x
| app l r => app (openRec i sub l) (openRec i sub r)
| abs M   => abs <| openRec (i+1) sub M

/-- Locally closed terms. -/
@[aesop safe [constructors]]
inductive LC : Term Var → Prop
| fvar (x)  : LC (fvar x)
| abs (L : Finset Var) (e : Term Var) (cofin : ∀ x ∉ L, LC (openRec 0 e (fvar x))) : LC (abs e)
| app {l r} : l.LC → r.LC → LC (app l r)

attribute [grind] LC.fvar LC.app

-- fails, I think becasue `cofin` does not appear in `LC (abs e)`?
attribute [grind] LC.abs

You can see that previously we have used Aesop's [constructors], but grind is not able to automatically derive a pattern for LC.abs. From reading the new chapter in the Lean reference my understanding is this is because the parameter cofin is not used in the conclusion. Is this something I can handle with a custom grind_pattern?

[Kim Morrison]

What are you hoping for grind to do here?

Does

@[grind?]
theorem foo {e : Term Var} (h : ∃ L : Finset Var, ∀ x ∉ L, LC (openRec 0 e (fvar x))) : LC (abs e) := LC.abs h.choose e h.choose_spec

achieve what you want?

[Chris Henson]

I should have given a better example. Consider if I add to the above:

attribute [aesop safe forward] LC.abs

example (L : Finset Var) (cofin : ∀ x ∉ L, LC (openRec 0 e (fvar x))) : LC (abs e) := by
  -- ▼ suggestion:
  --   have fwd : e.abs.LC := LC.abs L e cofin
  --   simp_all only
  aesop?

With a forward rule, aesop selects a particular finset from the local context. This doesn't seem to work with the grind pattern you've shown above. For other theorems without the cofinite aspect, the "forward reasoning" @[grind →] seemed to work analogously.

[Kim Morrison]

Yes, grind won't currently do this, however you annotate the theorem.