Library MetaCoq.Checker.LibHypsNaming


This file is a set of tactical (mainly "!! t" where t is a tactic) and tactics (!intros, !destruct etc), that automatically rename new hypothesis after applying a tactic. The names chosen for hypothesis is programmable using Ltac. See examples in comment below.
Comments welcome.


The custom renaming tactic

This tactic should be redefined along a coq development, it should return a fresh name build from an hypothesis h and its type th. It should fail if no name is found, so that the fallback scheme is called.
Typical use, in increasing order of complexity, approximatively equivalent to the decreasing order of interest. 
Ltac my_rename_hyp h th :=
  match th with
    | (ind1 _ _ _ _) => fresh "ind1"
    | (ind2 _ _) => fresh "ind2"
    | f1 _ _ = true => fresh "f_eq_true"
    | f1 _ _ = false => fresh "f_eq_false"
    | f1 _ _ = _ => fresh "f_eq"
    | ind3 ?h ?x => fresh "ind3_" h
    | ind3 _ ?x => fresh "ind3" (* if fresh h failed above *)

    (* Sometime we want to look for the name of another hypothesis to
       name h. For example here we want to rename hypothesis h into
       "type_of_foo" if there is some H of type [type_of foo = Some
       h]. *)
    | type => (* See if we find something of which h is the type: *)
              match reverse goal with
              | H: type_of ?x = Some h => fresh "type_of_" x
              end

    | _ => previously_defined_renaming_tac1 th (* cumulative with previously defined renaming tactics *)
    | _ => previously_defined_renaming_tac2 th
  end.

(* Overwrite the definition of rename_hyp using the ::= operator. :*)

Ltac rename_hyp ::= my_rename_hyp.



The default fallback renaming strategy

This is used if the user-defined renaming scheme fails to give a name to a hypothesis. th is the type of the hypothesis.

Inductive HypPrefixes :=
  | HypNone
  | HypH_
  | HypH.















Tactic Notation "!!" tactic3(Tac) := (rename_new_hyps Tac).
Tactic Notation "!!" tactic3(Tac) constr(h) :=
  (rename_new_hyps (Tac h)).




Tactic Notation "!!!" tactic3(Tac) := !! (subst_new_hyps Tac).

Renaming Tacticals

!! tactic (resp. !! tactic h and ☐:: tactic h1 h2) performs tactic (resp. tactic h and tactic h1 h2) and renames all new hypothesis. During the process all previously known hypothesis (but h, h1 and h2) are marked. It may happen that this mark get in the way during the execution of tactic. We might try to find a better way to mark hypothesis.


Specific redefinition of usual tactics.

Note that for example !!induction h doesn not work because "destruct" is not a ltac function by itself, it is already a notation. Hence the special definitions below for this kind of tactics: induction ddestruct inversion etc.



 Tactic Notation "decomp" constr(c) :=
   match goal with
   | _ ⇒
     let h := fresh "h_decomp" in
     pose proof c as h;
     (!! (idtac;decomp_ex c)); try clear h
   end.

Tactic Notation "!induction" constr(h) := !! (induction h).
Tactic Notation "!destruct" constr(h) := !! (destruct h).

Tactic Notation "!destruct" constr(h) "!eqn:" ident(id) :=
  (!!(destruct h eqn:id; revert id));intro id.
Tactic Notation "!destruct" constr(h) "!eqn:?" := (!!(destruct h eqn:?)).

Tactic Notation "!inversion" hyp(h) := !!! (inversion h).
Tactic Notation "!invclear" hyp(h) := !!! (inversion h;clear h).
Tactic Notation "!assert" constr(h) := !! (assert h).

Tactic Notation "!intros" := !!intros.

Tactic Notation "!intro" := !!intro.

Tactic Notation "!intros" "until" ident(id)
  := intros until id; !intros.

Tactic Notation "!intros" simple_intropattern(id1)
  := !! intro id1.

Tactic Notation "!intros" ident(id1) ident(id2)
  := intros id1 id2; !intros.
Tactic Notation "!intros" ident(id1) ident(id2) ident(id3)
  := intros id1 id2 id3; !!intros.
Tactic Notation "!intros" ident(id1) ident(id2) ident(id3) ident(id4)
  := intros id1 id2 id3 id4; !!intros.

Tactic Notation "!intros" ident(id1) ident(id2) ident(id3) ident(id4) ident(id5)
  := intros id1 id2 id3 id4 id5; !!intros.
Tactic Notation "!intros" ident(id1) ident(id2) ident(id3) ident(id4) ident(id5) ident(id6)
  := intros id1 id2 id3 id4 id5 id6; !!intros.

Some more tactic not specially dedicated to renaming.