Target minimal changes in proof / goal outputs with --minimize-for-first-proof-diff

[JasonGross]

Extend the minimizer with a --minimize-for-first-proof-diff which can (a) insert Show. between every statement in the proof, and (b) replace ; with . all:. Then it can look for the first line where the goals differ, run Set Printing All. and write an Ltac2 tactic to check that the goal and hyps match the succeeding version, and insert that tactic check in the code. Probably there can even be another pass that attempts to generalize over evars to ensure the behavior is not tied to some complicated issue with evars, shelve irrelevant goals, and then to look for the last evar-free goal before the error behavior, and write that out explicitly as a Goal.

Originally posted by @JasonGross in rocq-prover/rocq#20177 (comment)

[JasonGross]

I think the strategy I'm suggesting is independent of what's going on in the proof. (But, broadly, there's some pre-processing, then a big repeat match that handles all but one case (checked by all: [ > ].), then some semi-automation to handle the remaining case in a somewhat ad-hoc way.)

Roughly what I'm suggesting is:

1. is it the case that the number of goals is the same before the final all: try congruence. both before and after this PR?

• If no, then we can replace all: try congruence. with all: let n := numgoals in guard numgoals = <whatever>. to detect the difference.
• If yes, then are all goals identical under Set Printing All. Set Printing Depth 10000000. Show. shelve. Show. shelve. ....?
  • If yes, then just identify which goal congruence fails to solve, and do coqbot resume ci minimize with ```Goal . intros. congruence.`
  • If no, then replace all: congruence with a match statement that does idtac on the goal that differs (the version of it that occurs after this PR) and admit on all other goals, and check that there are no open goals after this tactic)

2. repeat 1 on all: handle_eval_eval.
3. keep going until you can identify the single goal and single step of automation which differs before and after.

A quicker way to find this is to do Set Printing All. Set Printing Depth 10000000000. and insert Show. between each line (perhaps with idtac "<the next tactic>". before) and run coqc on it, then use vimdiff or some other tool to determine the step at which the goals first differ. Or for more control do something like (untested)

Ltac2 pr_hyp (h : ident * constr option * constr) :=
  let (n, body, ty) := h in
  match body with
  | Some body => fprintf "%I : %t := %t" n ty body
  | None => fprintf "%I : %t" n ty
  end.
Ltac2 rec pr_list_with_sep (sep : message) (pr : 'a -> message) (ls : 'a list) :=
  match ls with
  | [] => fprintf ""
  | x :: xs => fprintf "%a%a%a" (fun () => pr) x (fun () a => a) sep (fun () => pr_list_with_sep sep pr) xs
  end.
Ltac2 print_goal_and_hyps () :=
  printf
    "==============================%a%a%a==============================%a%t"
    (fun () a => a) Message.force_new_line 
    (pr_list_with_sep Message.force_new_line pr_hyp)
    (Control.hyps ()))
    (fun () a => a) Message.force_new_line 
    (fun () a => a) Message.force_new_line 
    (Control.goal ()).
Ltac print_goal_and_hyps := ltac2:(Control.enter print_goal_and_hyps).

And then do Set Printing All. all: print_goal_and_hyps. or something.

Originally posted by @JasonGross in rocq-prover/rocq#20177 (comment)