Feature Request: Show current path (call stack) in proof

[cpitclaudel]

Description of the problem

Hi folks,

How hard would it be to implement a proof-mode command that displays a "breadcrumbs" trail describing where you are in the proof, i.e. the list of all functions (lemmas) that dominate the current point in the proof tree?

Something like this (see comments embedded in the code):

Require Import Coq.Lists.List.

Lemma in_flat_map {A B} (f:A->list B) (l: list A) (y: B) :
  In y (flat_map f l) <-> exists x, In x l /\ In y (f x).
Proof.
  induction l; simpl; split; intros H.
  (* list_ind#2 > conj#1
       exists x : A, False /\ In y (f x)
     list_ind#2 > conj#2
       False
     list_ind#3 > conj#1
       exists x : A, (a = x \/ In x l) /\ In y (f x)
     list_ind#3 > conj#2
       In y (f a ++ flat_map f l) *)
  - contradiction.
  - destruct H as (x,(H,_)); contradiction.
  - destruct (in_app_or _ _ _ H) as [H0|H0].
    (* list_ind#3 > conj#1 > match(in_app_or)#or_introl
         exists x : A, (a = x \/ In x l) /\ In y (f x)
       list_ind#3 > conj#1 > match(in_app_or)#or_intror
         exists x : A, (a = x \/ In x l) /\ In y (f x)
       in_app_or *)
    exists a; auto.
    destruct IHl as (H1,_); destruct (H1 H0) as (x,(H2,H3)).
    exists x; auto.
  - apply in_or_app.
    destruct H as (x,(H0,H1)); destruct H0; subst; auto.
    right; destruct IHl as (_,H2).
    Show Proof.
    (* list_ind#3 > conj#2 > in_or_app#4 > match#or_intror
         In y (flat_map f l) *)
    apply H2.
    exists x; auto.
Qed.

Here's an image showing what these paths correspond to:

There are many cases where this would be useful:

• Understanding how an automated tactic got to a given point in a proof. My current process for orienting myself is stepping through the tactic in the ltac debugger or step by step by copying its contents.
• Understanding where a particular goal comes from. For example, I often mistakenly add an unnecessary argument to a lemma, and then at the end of my proof I have a goal like |- nat. My current process is to use exact 4242 and then Set Printing Depth 1000., Show Proof., and search for 4242.

I ran into the second one with @DIJamner again today.

I like to think of this as the Coq equivalent of setting a breakpoint and looking at a backtrace, only we're already at the breakpoint (currently proving a goal) and we already have the complete "call tree" of the program (the proof term), and what we want is the current "call stack", namely the path that led to this point in the program.

(Btw, this way of thinking about the issue makes it easy to see how we should handle evars that are repeated in multiple places in the call tree: namely, show a list of all "call sites", ie breadcrumbs for each branch in the call tree that lead to that evar.)

(Lean 3 has something a bit similar to this, where doing two levels of induction shows you which case you're in for each constructor, so it shows list.cons > nat.zero, more or less)