Support for match-expressions with overlapping patterns. Recall that when a match-expression has overlapping patterns, some of its equation theorems are conditional. Let's consider the following example

inductive S where
  | mk1 (n : Nat)
  | mk2 (n : Nat) (s : S)
  | mk3 (n : Bool)
  | mk4 (s1 s2 : S)

def f (x y : S) :=
  match x, y with
  | .mk1 a, c => a + 2
  | a, .mk2 1 (.mk4 b c) => 3
  | .mk3 a, .mk4 b c => 4
  | a, b => 5

The match-expression in this example has 4 equations. The second and fourth are conditional.

f.match_1.eq_2
  (motive : S → S → Sort u) (a b c : S)
  (h_1 : (a : Nat) → (c : S) → motive (S.mk1 a) c)
  (h_2 : (a b c : S) → motive a (S.mk2 1 (b.mk4 c)))
  (h_3 : (a : Bool) → (b c : S) → motive (S.mk3 a) (b.mk4 c))
  (h_4 : (a b : S) → motive a b) :
  (∀ (a_1 : Nat),  a = S.mk1 a_1 → False) → -- <<< Condition stating it is not the first case
  f.match_1 motive a (S.mk2 1 (b.mk4 c)) h_1 h_2 h_3 h_4 = h_2 a b c

f.match_1.eq_4
  (motive : S → S → Sort u) (a b : S)
  (h_1 : (a : Nat) → (c : S) → motive (S.mk1 a) c)
  (h_2 : (a b c : S) → motive a (S.mk2 1 (b.mk4 c)))
  (h_3 : (a : Bool) → (b c : S) → motive (S.mk3 a) (b.mk4 c))
  (h_4 : (a b : S) → motive a b) :
  (∀ (a_1 : Nat), a = S.mk1 a_1 → False) →  -- <<< Condition stating it is not the first case
  (∀ (b_1 c : S), b = S.mk2 1 (b_1.mk4 c) → False) →  -- <<< Condition stating it is not the second case
  (∀ (a_1 : Bool) (b_1 c : S), a = S.mk3 a_1 → b = b_1.mk4 c → False) → -- -- <<< Condition stating it is not the third case
  f.match_1 motive a b h_1 h_2 h_3 h_4 = h_4 a b

In the two equational theorems above, we have the following conditions.

- `(∀ (a_1 : Nat),  a = S.mk1 a_1 → False)`
- `(∀ (b_1 c : S), b = S.mk2 1 (b_1.mk4 c) → False)`
- `(∀ (a_1 : Bool) (b_1 c : S), a = S.mk3 a_1 → b = b_1.mk4 c → False)`

When instantiating the equations (and match-splitter), we wrap the conditions with the gadget Grind.MatchCond. This gadget is used for implementing truth-value propagation. See the propagator propagateMatchCond below. For example, given a condition C of the form Grind.MatchCond (∀ (a : Nat), t = S.mk1 a → False), if t is merged with an equivalence class containing S.mk2 n s, then C is asseted to true by propagateMatchCond.

This module also provides auxiliary functions for detecting congruences between match-expression conditions. See function collectMatchCondLhssAndAbstract.

Remark: This note highlights that the representation used for encoding match-expressions with overlapping patterns is far from ideal for the grind module which operates with equivalence classes and does not perform substitutions like simp. While modifying how match-expressions are encoded in Lean would require major refactoring and affect many modules, this issue is important to acknowledge. A different representation could simplify grind, but it could add extra complexity to other modules.

def Lean.Meta.Grind.markAsMatchCond (e : Expr) : Expr

Returns Grind.MatchCond e. Recall that Grind.MatchCond is an identity function, but the following simproc is used to prevent the term e from being simplified, and we have special support for propagating is truth value.

Equations

• Lean.Meta.Grind.markAsMatchCond e = Lean.mkApp (Lean.mkConst `Lean.Grind.MatchCond) e

def Lean.Meta.Grind.isMatchCond (e : Expr) : Bool

Equations

• Lean.Meta.Grind.isMatchCond e = e.isAppOfArity `Lean.Grind.MatchCond 1

def Lean.Meta.Grind.reduceMatchCond : Simp.DSimproc

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.addMatchCond (s : Simprocs) : CoreM Simprocs

Adds reduceMatchCond to s

Equations

• Lean.Meta.Grind.addMatchCond s = s.add `Lean.Meta.Grind.reduceMatchCond false

def Lean.Meta.Grind.collectMatchCondLhssAndAbstract (matchCond : Expr) : GoalM (Array Expr × Expr)

Given e a match-expression condition, returns the left-hand side of the ground equations, and function application that abstracts the left-hand sides. As an example, assume we have a match-expression condition C₁ of the form

Grind.MatchCond (∀ y₁ y₂ y₃, t = .mk₁ y₁ → s = .mk₂ y₂ y₃ → False)

then the result returned by this function is

(#[t, s], (fun x₁ x₂ => (∀ y₁ y₂ y₃, x₁ = .mk₁ y₁ → x₂ = .mk₂ y₂ y₃ → False)) t s)

Note that the returned expression is definitionally equal to C₁. We use this expression to detect whether two different match-expression conditions are congruent. For example, suppose we also have the match-expression C₂ of the form

Grind.MatchCond (∀ y₁ y₂ y₃, a = .mk₁ y₁ → b = .mk₂ y₂ y₃ → False)

This function would return

(#[a, b], (fun x₁ x₂ => (∀ y₁ y₂ y₃, x₁ = .mk₁ y₁ → x₂ = .mk₂ y₂ y₃ → False)) a b)

Note that the lambda abstraction is identical to the first one. Let's call it l. Thus, we can write the two pairs above as

• (#[t, s], l t s)
• (#[a, b], l a b) Moreover, C₁ is definitionally equal to l t s, and C₂ is definitionally equal to l a b. Then, if grind infers that t = a and s = b, it will detect that l t s and l a b are equal by congruence, and consequently C₁ is equal to C₂.

Gruesome details for heterogenenous equalities.

When pattern matching on indexing families, the generated conditions often use heterogenenous equalities. Here is an example:

(∀ (x : Vec α 0), n = 0 → HEq as Vec.nil → HEq bs x → False)

In this case, it is not sufficient to abstract the left-hand side. We also have to abstract its type. The following is produced in this case.

(#[n, Vec α n, as, Vec α n, bs],
 (fun (x_0 : Nat) (ty_1 : Type u_1) (x_1 : ty_1) (ty_2 : Type u_1) (x_2 : ty_2) =>
    ∀ (x : Vec α 0), x_0 = 0 → HEq x_1 Vec.nil → HEq x_2 x → False)
 n (Vec α n) as (Vec α n) bs)

The example makes it clear why this is needed, as and bs depend on n. Note that we can abstract the type without introducing typer errors because heterogenenous equality is used for as and bs.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go (e : Expr) (lhssαs : Array (Expr × Option Expr)) (i : Nat) (xs : Array Expr) (tys : Array (Option Expr)) (tysxs args : Array Expr) : GoalM (Array Expr × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go.replaceLhss (xs : Array Expr) (tys : Array (Option Expr)) (e : Expr) (i : Nat) : Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go.replaceLhss xs tys e i = (pure e).run

def Lean.Meta.Grind.tryToProveFalse (e : Expr) : GoalM Unit

Given a match-expression condition e that is known to be equal to True, try to close the goal by proving False. We use the following to example to illustrate the purpose of this function.

def f : List Nat → List Nat → Nat
  | _, 1 :: _ :: _ => 1
  | _, _ :: _ => 2
  | _, _  => 0

example : z = a :: as → y = z → f x y > 0 := by
  grind [f.eq_def]

After grind unfolds f, it case splits on the match-expression producing three subgoals. The first two are easily closed by it. In the third one, we have the following two match-expression conditions stating that we are not in the first and second cases.

Lean.Grind.MatchCond (∀ (head : Nat) (tail : List Nat), x✝² = 1 :: head :: tail → False)
Lean.Grind.MatchCond (∀ (head : Nat) (tail : List Nat), x✝² = head :: tail → False)

Moreover, we have the following equivalence class.

{z, y, x✝², a :: as}

Thus, we can close the goal by using the second match-expression condition, we just have to instantiate head and tail with a and as respectively, and use the fact that x✝² is equal to a :: as.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Meta.Grind.tryToProveFalse.go (e : Expr) : GoalM Expr

Returns a term that is equal to e, but containing constructor applications and literal values. e is the left-hand side of the equations in a match-expression condition. Remark: we could use the right-hand side to interrupt the recursion. For example, suppose the equation is x = ?head :: ?tail. We only need to show that x is equal to some term of the form a :: as to satisfy it. This function may return a₁ :: b :: bs, which still allows us to satisfy the equation, but may have a bigger proof (e.g., a proof that as is equal to b::bs)

def Lean.Meta.Grind.propagateMatchCondUp : Propagator

Propagates MatchCond upwards

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.propagateMatchCondDown : Propagator

Propagates MatchCond downwards

Equations

• One or more equations did not get rendered due to their size.