Documentation

Add auxiliary annotation to indicate the match-expression e must be reduced when performing smart unfolding.

Add auxiliary annotation to indicate expression e (a match alternative rhs) was successfully reduced by smart unfolding.

Create the ith projection major. It tries to use the auto-generated projection functions if available. Otherwise falls back to Expr.proj.

The "match" compiler uses if-then-else expressions and other auxiliary declarations to compile match-expressions such as

match v with
| 'a' => 1
| 'b' => 2
| _   => 3

because it is more efficient than using casesOn recursors. The method reduceMatcher? fails if these auxiliary definitions (e.g., ite) cannot be unfolded in the current transparency setting. This is problematic because tactics such as simp use TransparencyMode.reducible, and most users assume that expressions such as

match 0 with
| 0 => 1
| 100 => 2
| _ => 3

should reduce in any transparency mode. Thus, we define a custom canUnfoldAtMatcher predicate for whnfMatcher.

This solution is not very modular because modications at the match compiler require changes here. We claim this is defensible because it is reducing the auxiliary declaration defined by the match compiler.

Alternative solution: tactics that use TransparencyMode.reducible should rely on the equations we generated for match-expressions. This solution is also not perfect because the match-expression above will not reduce during type checking when we are not using TransparencyMode.default or TransparencyMode.all.

Reduce kernel projection Expr.proj .. expression.

Recall that _sunfold auxiliary definitions contains the markers: markSmartUnfoldingMatch (*) and markSmartUnfoldingMatchAlt (**). For example, consider the following definition

def r (i j : Nat) : Nat :=
  i +
    match j with
    | Nat.zero => 1
    | Nat.succ j =>
      i + match j with
          | Nat.zero => 2
          | Nat.succ j => r i j

produces the following _sunfold auxiliary definition with the markers

def r._sunfold (i j : Nat) : Nat :=
  i +
    (*) match j with
    | Nat.zero => (**) 1
    | Nat.succ j =>
      i + (*) match j with
          | Nat.zero => (**) 2
          | Nat.succ j => (**) r i j

match expressions marked with markSmartUnfoldingMatch (*) must be reduced, otherwise the resulting term is not definitionally equal to the given expression. The recursion may be interrupted as soon as the annotation markSmartUnfoldingAlt (**) is reached.

For example, the term r i j.succ.succ reduces to the definitionally equal term i + i * r i j

Try to reduce matcher/recursor/quot applications. We say they are all "morally" recursor applications.

If e is a projection function that satisfies p, then reduce it