scilib documentation

tactic.congrm

congrm: congr with pattern-matching

congrm e gives to the use the functionality of using congr with an expression e "guiding" congr through the matching. This allows more flexibility than congr' n, which enters uniformly through n iterations. Instead, we can guide the matching deeper on some parts of the expression and stop earlier on other parts.

Implementation notes #

Function underscores #

See the doc-string to tactic.interactive.congrm for more details. Here we describe how to add more "function underscores".

The pattern for generating a function underscore is to define a "generic" n-ary function, for some number n. You can take a look at tactic.congrm_fun_1, ..., tactic.congrm_fun_4. These implement the "function underscores" _₁, ..., _₄. If you want a different arity for your function, simply introduce

@[nolint unused_arguments]
def congrm_fun_n {α₁ … αₙ ρ} {r : ρ} : α₁ → ⋯ → aₙ → ρ := λ _ … _, r
notation `_ₙ` := congrm_fun_n

Warning: convert_to_explicit checks that the first 18 characters in the name of _ₙ are identical to tactic.congrm_fun_ to perform its job. Thus, if you want to implement "function underscores" with different arity, either make sure that their names begin with tactic.congrm_fun_ or you should change convert_to_explicit accordingly.

source
@[nolint]
def tactic.congrm_fun_1 {α : Sort u_1} {ρ : Sort u_2} {r : ρ} :
α → ρ

A generic function with one argument. It is the "function underscore" input to congrm.

Equations
source
@[nolint]
def tactic.congrm_fun_2 {α : Sort u_1} {β : Sort u_2} {ρ : Sort u_3} {r : ρ} :
α → β → ρ

A generic function with two arguments. It is the "function underscore" input to congrm.

Equations
  • _₂ = λ (_x : α) (_x : β), r
source
@[nolint]
def tactic.congrm_fun_3 {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {ρ : Sort u_4} {r : ρ} :
α → β → γ → ρ

A generic function with three arguments. It is the "function underscore" input to congrm.

Equations
  • _₃ = λ (_x : α) (_x : β) (_x : γ), r
source
@[nolint]
def tactic.congrm_fun_4 {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {ρ : Sort u_5} {r : ρ} :
α → β → γ → δ → ρ

A generic function with four arguments. It is the "function underscore" input to congrm.

Equations
  • _₄ = λ (_x : α) (_x : β) (_x : γ) (_x : δ), r
source
meta def tactic.convert_to_explicit (pat lhs : expr) :
tactic expr

Replaces a "function underscore" input to congrm into the correct expression, read off from the left-hand-side of the target expression.

source
meta def tactic.equate_with_pattern_core  :
expr → tactic (list expr)

equate_with_pattern_core pat solves a single goal of the form lhs = rhs (assuming that lhs and rhs are unifiable with pat) by applying congruence lemmas until pat is a metavariable. Returns the list of metavariables for the new subgoals at the leafs. Calls set_goals [] at the end.

source
meta def tactic.equate_with_pattern (pat : expr) :
tactic unit

equate_with_pattern pat solves a single goal of the form lhs = rhs (assuming that lhs and rhs are unifiable with pat) by applying congruence lemmas until pat is a metavariable. The subgoals for the leafs are prepended to the goals.

source
meta def tactic.interactive.congrm (arg : interactive.parse interactive.types.texpr) :
tactic unit

Assume that the goal is of the form lhs = rhs or lhs ↔ rhs. congrm e takes an expression e containing placeholders _ and scans e, lhs, rhs in parallel.

It matches both lhs and rhs to the pattern e, and produces one goal for each placeholder, stating that the corresponding subexpressions in lhs and rhs are equal.

Examples:

example {a b c d : ℕ} :
  nat.pred a.succ * (d + (c + a.pred)) = nat.pred b.succ * (b + (c + d.pred)) :=
begin
  congrm nat.pred (nat.succ _) * (_ + _),
/-  Goals left:
⊢ a = b
⊢ d = b
⊢ c + a.pred = c + d.pred
-/
  sorry,
  sorry,
  sorry,
end

example {a b : ℕ} (h : a = b) : (λ y : ℕ, ∀ z, a + a = z) = (λ x, ∀ z, b + a = z) :=
begin
  congrm λ x, ∀ w, _ + a = w,
  -- produces one goal for the underscore: ⊢ a = b
  exact h,
end

The tactic also allows for "function underscores", denoted by _₁, ..., _₄. The index denotes the number of explicit arguments of the function to be matched. If e has a "function underscore" in a location, then the tactic reads off the function f that appears in lhs at the current location, replacing the explicit arguments of f by the user inputs to the "function underscore". After that, congrm continues with its matching.

source
def tactic_doc.tactic.congrm  :
tactic_doc_entry

Assume that the goal is of the form lhs = rhs or lhs ↔ rhs. congrm e takes an expression e containing placeholders _ and scans e, lhs, rhs in parallel.

It matches both lhs and rhs to the pattern e, and produces one goal for each placeholder, stating that the corresponding subexpressions in lhs and rhs are equal.

Examples:

example {a b c d : ℕ} :
  nat.pred a.succ * (d + (c + a.pred)) = nat.pred b.succ * (b + (c + d.pred)) :=
begin
  congrm nat.pred (nat.succ _) * (_ + _),
/-  Goals left:
⊢ a = b
⊢ d = b
⊢ c + a.pred = c + d.pred
-/
  sorry,
  sorry,
  sorry,
end

example {a b : ℕ} (h : a = b) : (λ y : ℕ, ∀ z, a + a = z) = (λ x, ∀ z, b + a = z) :=
begin
  congrm λ x, ∀ w, _ + a = w,
  -- produces one goal for the underscore: ⊢ a = b
  exact h,
end

The tactic also allows for "function underscores", denoted by _₁, ..., _₄. The index denotes the number of explicit arguments of the function to be matched. If e has a "function underscore" in a location, then the tactic reads off the function f that appears in lhs at the current location, replacing the explicit arguments of f by the user inputs to the "function underscore". After that, congrm continues with its matching.