Variant of repeat match! goal (and maybe repeat match goal) that processes hypotheses in a more efficient ordering

[JasonGross]

Is your feature request related to a problem?

In light of #18770, I think the default semantics of repeat match goal is asymptotically suboptimal, because it rescans all hypotheses any time a branch succeeds.

Proposed solution

I think a useful alternative semantics would be to have variants that replace

coq/user-contrib/Ltac2/Pattern.v

Line 99 in cbc9fab

Control.plus p next

with something like Control.plus p (fun _ => ()); next () in

coq/user-contrib/Ltac2/Pattern.v

Lines 82 to 101 in cbc9fab

	Ltac2 lazy_match0 t (pats:'a constr_matching) :=
	let rec interp m := match m with
	| [] => Control.zero Match_failure
	| p :: m =>
	let next _ := interp m in
	let (knd, pat, f) := p in
	let p := match knd with
	| MatchPattern =>
	(fun _ =>
	let context := empty_context in
	let bind := matches_vect pat t in
	fun _ => f context bind)
	| MatchContext =>
	(fun _ =>
	let (context, bind) := matches_subterm_vect pat t in
	fun _ => f context bind)
	end in
	Control.plus p next
	end in
	Control.once (fun () => interp pats) ().

That is, I want to be able to get all the matches from a match statement, and then execute all the branches that succeed. Is there some version of this that would be generally useful to have in the standard library?

Alternative solutions

No response

Additional context

No response

[SkySkimmer]

Not sure I understand, can you write some example tactics with some comments about what match! goal does on them vs what your new thing would do?

[JasonGross]

In most cases, the behavior would be the same, though for something like repeat match goal with H : True |- _ => idtac | H : _ |- _ => clear H end, the new tactic would clear hypotheses while the existing tactic would not.

The main use case is to improve the performance of match statements. Consider something like repeat match goal with H : _ |- _ => progress cbv in H end. If there are n hypotheses and all of them can be reduced, this tactic executes cbv n(n+1)/2 times. The new tactic would execute cbv 2n times.

The tactic should basically just be nicer syntax for repeat (List.iter (fun (h, body, type) => try match! ... end) (Control.hyps ())), except that it would support matches with multiple hypotheses, non-linear matches against the goal, etc.

[SkySkimmer]

I think a useful alternative semantics would be to have variants that replace ...

Consider something like repeat match goal with H : _ |- _ => progress cbv in H end.

That only has 1 branch so I don't think your proposed change would do what you want.

[JasonGross]

That only has 1 branch so I don't think your proposed change would do what you want.

Surely the length of the constr_matching for match! goal with h : _ |- _ => printf "%I" h; Control.zero Tactic_failure end is the number of hypotheses, since backtracking will print every hypothesis, right?

[SkySkimmer]

Require Import Ltac2.Ltac2 Ltac2.Printf.

Ltac2 Globalize match! goal with [ h : _ |- _ ] => printf "%I" h; Control.zero Tactic_failure end.
(*
let (m : '__α Pattern.goal_matching) :=
  [(([(None, (Pattern.MatchPattern, pat:(_)))], (Pattern.MatchPattern, pat:(_))),
    (fun h =>
     let h := Array.get h 0 in
     fun _ =>
     fun _ =>
     fun _ =>
     fun _ =>
     (let (fmt : ('__α0, unit, message, unit) format) := Message.Format.ident Message.Format.stop in
      printf fmt
      :'__α0) h; Control.zero Tactic_failure))] : _ Pattern.goal_matching in
Pattern.one_goal_match0 false m
:'__α
*)

[JasonGross]

Ah, is it matches_vect that is multi success? Maybe the thing to do is to have a "run all successes in sequence" tactic built on Control.case?