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.PreMatchCond. Grind.PreMatchCond uses the default reducibility setting and cannot be accidentally reduced by simp. After simp is applied, it is replaced with Grind.MatchCond which is reducible. This Grind.MatchCond 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.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 heterogeneous equalities.

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

(∀ (x : Vec α 0), n = 0 → as ≍ Vec.nil → 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 → x_1 ≍ Vec.nil → 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 type errors because heterogeneous equality is used for as and bs.

Equations

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

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.

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.