named_intros.v

Require Import Coq.Strings.String.
Open Scope string_scope.

Definition with_name (n : string) {T} (v : T) := v.

(* ensures that the name [H] is free by renaming existing hypotheses *)
Ltac ensure_free H :=
  try (* not sure how many [fresh]es I need, probably not more than 3 *)
    let H' := fresh H in
    let H' := fresh H' in
    let H' := fresh H' in
    rename H into H'.

Module Context.
  Inductive list :=
  | nil
  | cons (name : string) (name_ident : Set -> Set) (rest : list).
End Context.

Ltac find_and_intro ctx str :=
  lazymatch ctx with
  | context[Context.cons str (fun n => _) _] => ensure_free n; intro n; cbv beta delta [with_name] in n
  | _ => fail 0 "No ident found for string" str
  end.

Ltac intros_named' ctx :=
  lazymatch goal with
  | [ |- let n : string := ?v in _ ]
    => let ctx := constr:(Context.cons v (fun n => n) ctx) in
       intro;
       intros_named' ctx
  | [ |- let n : with_name ?str _ := _ in _ ]
    => find_and_intro ctx str; intros_named' ctx
  | [ |- let n := with_name ?str _ in _ ]
    => find_and_intro ctx str; intros_named' ctx
  | [ |- forall n : with_name ?str _, _ ]
    => find_and_intro ctx str; intros_named' ctx
  | _ => idtac
  end.
Ltac intros_named := intros_named' Context.nil.

Goal let y := "y" in let x := "x" in forall (a : with_name "x" nat) (b : with_name "y" nat), a + b = b + a.
Proof.
  intros_named.
(* 1 subgoal (ID 16)
  
  y0 := "y" : string
  x0 := "x" : string
  x, y : nat
  ============================
  x + y = y + x
 *)