should `clear_` tactic also clear inaccessible hypotheses?

[dwrensha]

trafficstars

In mathlib3, pairwise_and_iff has a usage of clear_ with this context:

α : Type u_1,
R S : α → α → Prop,
l : list α,
_x : pairwise R l ∧ pairwise S l,
_fun_match : pairwise R l ∧ pairwise S l → pairwise (λ (a b : α), R a b ∧ S a b) l,
hR : pairwise R l,
hS : pairwise S l
⊢ pairwise (λ (a b : α), R a b ∧ S a b) l

(see https://github.com/leanprover-community/mathlib/blob/aff61c0f687c5d366edb248791f26fa69a4adfe2/src/data/list/pairwise.lean#L67)

A direct translation into Lean 4 leads to this context in the same place:

α : Type u_1
R : α → α → Prop
a : α
l : List α
S : α → α → Prop
: Pairwise R l ∧ Pairwise S l
hR : Pairwise R l
hS : Pairwise S l
⊢ Pairwise (fun a b => R a b ∧ S a b) l

In this case, the current version of mathlib4's clear_ won't drop the Pairwise R l ∧ Pairwise S l hypothesis, because it is ~anonymous~ inaccessible. We need to drop that hypothesis to get the later induction to work. It's easy enough to work around this problem by adapting the proof a bit, but it would be nice if we could have a direct translation. What would make most sense to me is for mathlib4's clear_ to also drop unnamed hypotheses (in addition to hypotheses whose names start with _). We could even make the behavior configurable.

[gebner]

I see what you mean. The inaccessible (that's how they're called) hypothesis ‹Pairwise R l ∧ Pairwise S l› is a leftover from pattern matching AFAICT. So it should be treated the same as _fun_match in Lean 3, i.e., dropped.

BTW, thank you for pointing out a nice example for the interaction of pattern matching, inaccessible hypothesis, and the induction tactic.