[RFC] Equation compiler wildcard behavior

[dselsam]

trafficstars

Many users have gotten confused and frustrated by the behavior of wildcards in the equation compiler. There is at least one open Github issue devoted to this discussion (https://github.com/leanprover/lean/issues/1466).

The purpose of this RFC is two-fold:

1. To accumulate examples that users think should work.
2. To discuss possible solutions.

Even for users who do not want to think about how the equation compiler works or what it might take to solve the problem adequately, please post your examples anyway.

---

Example 1: the simplest example that illustrates the current problem is due to @theemathas:

inductive foo : bool → Prop
| bar : foo ff
| baz : foo tt

example : ∀ (x : bool), foo x → true
| .(ff) foo.bar := trivial
| b    x        := trivial -- error: non-exhaustive

This does not work in the current implementation because:

1. All variables in inaccessible transitions (e.g. b) become local constants.
2. When we then "split" x to enumerate constructors of foo, we try to unify each of the possible result types foo ff and foo tt with the expected type foo b, and both of the unifications fail.

The proposed solution (not all details worked out yet) is to treat variables in inaccessible transitions as fresh metavariables for each possible downstream split. So in the example above, we would unify foo ff =?= foo ?b1 and foo tt =?= foo ?b2, and both would succeed and so the resulting equations would be exhaustive.

Example 2: tricky dependency nested deep inside

inductive op : ℕ → ℕ → Type
| mk : ∀ n, op n n

structure node : Type := (id₁ id₂ : ℕ) (o : op id₁ id₂)

def f : list node → true
| (⟨.m₁, .m₁, op.mk m₁⟩::⟨1, 1, op.mk 1⟩::rest) := trivial
| _                                             := trivial -- error: non-exhaustive

Implementation details aside, I believe the proposed solution will work for this example as well.

---

I have a few more examples that I will post once I clean them up and simplify them. @rlewis1988 @timjb can you post the examples you have run into?

[robertylewis]

I'll double check this next time I'm at my office computer, but I'm fairly sure the issues I've had with wildcard behavior follow the same pattern as @theemathas' example. When I took the time to reduce them to something minimal, it was nearly identical to your Example 1. I'll think about whether the non-reduced examples will be fixed by your proposal. (I hope I still have them saved somewhere.)

@leodemoura has mentioned an "equation validator" in other issues. Some of my original examples were a little strange, and I wouldn't complain (too much :) ) if they got rejected with a more accurate error message. Obviously your proposal would be preferable, but especially if it doesn't catch all cases, something that could identify the point of failure would be really helpful.

[theemathas]

FYI, my original code had baz : foo ff

[timjb]

I'm getting the "invalid non-exhaustive set of equations" error for the directed_associator_coherence_thm lemma that is commented out at the end of this file. Here's a version that is cleaned up and simplified somewhat:

variable (α : Type)

inductive bin_tree
| leaf : α → bin_tree
| branch : bin_tree → bin_tree → bin_tree

open bin_tree

inductive cong_clos_step (R : bin_tree α → bin_tree α → Type) : bin_tree α → bin_tree α → Type
| lift  : Π s t, R s t → cong_clos_step s t
| left  : Π l₁ l₂ r, cong_clos_step l₁ l₂ → cong_clos_step (branch l₁ r) (branch l₂ r)
| right : Π l r₁ r₂, cong_clos_step r₁ r₂ → cong_clos_step (branch l r₁) (branch l r₂)

inductive reassoc_dir_single_step : bin_tree α → bin_tree α → Type
| rotate_right : Π r s t, reassoc_dir_single_step (branch (branch r s) t) (branch r (branch s t))

-- smallest reflexive, transitive, congruent (but not necessarily symmetric) relation that includes R
inductive cong_clos (R : bin_tree α → bin_tree α → Type) : bin_tree α → bin_tree α → Type
| refl : Π t, cong_clos t t
| step : Π r s t, cong_clos_step α R r s → cong_clos s t → cong_clos r t

@[reducible] def reassoc_dir : bin_tree α → bin_tree α → Type :=
  cong_clos α (reassoc_dir_single_step α)

lemma toy_directed_associator_coherence_thm : Π (Xs Ys : bin_tree α) (p : reassoc_dir α Xs Ys), unit
| (branch l r) Ys (cong_clos.step ._ ._ ._ (cong_clos_step.left ._ lp ._ p) ps) := ()
| (branch l r) Ys (cong_clos.step ._ ._ ._ (cong_clos_step.right ._ ._ rp p) ps) := ()
| (branch (branch x y) z) Ys (cong_clos.step ._ ._ ._ (cong_clos_step.lift ._ ._ (reassoc_dir_single_step.rotate_right ._ ._ ._)) _) := ()
| Xs ._ (cong_clos.refl ._ ._) := ()

Interestingly, the example is accepted when I change the penultimate pattern match to

| .(branch (branch x y) z) Ys (cong_clos.step ._ ._ ._ (cong_clos_step.lift ._ ._ (reassoc_dir_single_step.rotate_right x y z)) _) := ()

But I when making the same change to the full directed_associator_coherence_thm, I get other errors.

Another way I got it working was to compose the inductive definitions cong_clos_step and reassoc_dir_single_step:

variable (α : Type)

inductive bin_tree
| leaf : α → bin_tree
| branch : bin_tree → bin_tree → bin_tree

open bin_tree

inductive reassoc_dir_step : bin_tree α → bin_tree α → Type
| rotate_right : Π r s t, reassoc_dir_step (branch (branch r s) t) (branch r (branch s t))
| left  : Π l₁ l₂ r, reassoc_dir_step l₁ l₂ → reassoc_dir_step (branch l₁ r) (branch l₂ r)
| right : Π l r₁ r₂, reassoc_dir_step r₁ r₂ → reassoc_dir_step (branch l r₁) (branch l r₂)

-- smallest reflexive, transitive, congruent (but not necessarily symmetric) relation that includes R
inductive reassoc_dir : bin_tree α → bin_tree α → Type
| refl : Π t, reassoc_dir t t
| step : Π r s t, reassoc_dir_step α r s → reassoc_dir s t → reassoc_dir r t

lemma toy_directed_associator_coherence_thm : Π (Xs Ys : bin_tree α) (p : reassoc_dir α Xs Ys), unit
| (branch l r) Ys (reassoc_dir.step ._ ._ ._ (reassoc_dir_step.left ._ lp ._ p) ps) := ()
| (branch l r) Ys (reassoc_dir.step ._ ._ ._ (reassoc_dir_step.right ._ ._ rp p) ps) := ()
| (branch (branch x y) z) Ys (reassoc_dir.step ._ ._ ._ (reassoc_dir_step.rotate_right ._ ._ ._) _) := ()
| Xs ._ (reassoc_dir.refl ._) := ()

[leodemoura]

@dselsam I closed other issues related to this one.

[robertylewis]

Here's another example using wildcards that fails unexpectedly, or at least it's unexpected given my intuitions about wildcards. I don't know how related this is to the above problems. If nothing else, the error message is inscrutable (although the sorrys don't help with that).

variables (A : Type) (f : A → ℕ → A) [has_mul A]
open nat

-- works
theorem thm (a : A) : ∀ m n, f a m * f a n = f a n * f a m
| 0 0 := sorry
| (succ m) 0 := sorry
| 0 (succ n) := sorry
| (succ m) (succ n) :=
 have h : f a m * f a n = f a n * f a m, from thm _ _,
 sorry

-- fails
theorem thm' (a : A) : ∀ m n, f a m * f a n = f a n * f a m
| 0 n := sorry
| m 0 := sorry
| (succ m) (succ n) :=
 have h : f a m * f a n = f a n * f a m, from thm' _ _,
 sorry

[digama0]

This looks like a bug in the if-then compilation strategy for matches. It is producing a term of the form ite (n = 0) T E : P n, but T has type P 0 instead of P n. To resolve this, it could either use dite instead, or put a term of type P n in for T (which is possible in this case because T is obtained from the first match branch with n := 0, so if you skip the substitution you get the appropriate type).

Alternatively, it could just avoid this compilation strategy altogether in the dependent case. (Why is it even triggering in this case?)

[leodemoura]

@digama0 We check if there are forward dependencies, but we forgot to check the goal. https://github.com/leanprover/lean/blob/master/src/library/equations_compiler/elim_match.cpp#L550-L558 I will fix this.

I have considered using dite in the past, but I'm not willing to do it. We would have to use eq.drec in the then-branch.

[andreasabel]

Inspired by Jeremy's tutorial I tried the example of renaming for intrinsically typed lambda calculus.

inductive ty
| base
| arr (a b : ty)

def cxt := list ty

inductive var : Π (g : cxt) (a : ty), Type
| vz {g a}   : var (a :: g) a
| vs {g a b} : var g a → var (b :: g) a

inductive tm : cxt → ty → Type
| var {g a}   : var g a → tm g a
| app {g a b} : tm g (ty.arr a b) → tm g a → tm g b
| abs {g a b} : tm (a :: g) b → tm g (ty.arr a b)

def ren (g d : cxt) := Π a, var d a → var g a

def liftr {g d a} (r : ren g d) : ren (a :: g) (a :: d)
| ._  var.vz    := var.vz
| _  (var.vs x) := var.vs (r _ x)

def rename' : Π {g d} (r : ren g d) {a}, tm d a → tm g a
| g d r _  (tm.var x)   := tm.var (r _ x)
| g d r _  (tm.app t u) := tm.app (rename' r t) (rename' r u)
| g d r ._ (tm.abs t)   := tm.abs (rename' (liftr r) t)

However, rename' is rejected with an error on the dot-pattern in the last line:

invalid use of inaccessible term, it is not completely fixed by other arguments
   ty.arr .?m_1 .?m_2 (lean-checker)

The only way I get this through is to provide the hidden arguments of abs and app:

def rename : Π {g d} (r : ren g d) {a}, tm d a → tm g a
| g d r _  (tm.var x)            := tm.var (r _ x)
| g d r _  (@tm.app ._ _ ._ t u) := tm.app (rename r t) (rename r u)
| g d r ._ (@tm.abs ._ _ _ t)    := tm.abs (rename (liftr r) t)

It seems that lean is more sensitive to correct dot placement than Agda. In Agda, _ can also be solved by a dot pattern.

[leodemoura]

opening again... the previous commit does not fix this issue, it just describes how to fix it.