(************************************************************************** * A user-customizable auto-naming scheme for hypothesis in Coq * * Author: Pierre Courtieu * * Distributed under the terms of the LGPL-v3 license * ***************************************************************************) (** 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. *) (* Comment this and the Z-dependent lines below if you don't want ZArith to be loaded *) Require Import ZArith FunInd. (** ** 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.>> *) Ltac rename_hyp h ht := match true with true => fail | _ => fresh "hh" end. Ltac rename_hyp_prefx h ht := let res := rename_hyp h ht in fresh "h_" res. (** ** 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. *) Ltac fallback_rename_hyp h th := match th with | _ => rename_hyp h th | true = beq_nat _ _ => fresh "beqnat_true" | beq_nat _ _ = true => fresh "beqnat_true" | false = beq_nat _ _ => fresh "beqnat_false" | beq_nat _ _ = false => fresh "beqnat_false" | beq_nat _ _ = _ => fresh "beqnat" | Zeq_bool _ _ = true => fresh "eq_Z_true" | Zeq_bool _ _ = false => fresh "eq_Z_false" | true = Zeq_bool _ _ => fresh "eq_Z_true" | false = Zeq_bool _ _ => fresh "eq_Z_false" | Zeq_bool _ _ = _ => fresh "eq_Z" | _ = Zeq_bool _ _ => fresh "eq_Z" | ?f = _ => fresh "eq_" f | ?f _ = _ => fresh "eq_" f | ?f _ _ = _ => fresh "eq_" f | ?f _ _ _ = _ => fresh "eq_" f | ?f _ _ _ _ = _ => fresh "eq_" f | ?f _ _ _ _ _ = _ => fresh "eq_" f | ?f _ _ _ _ _ _ = _ => fresh "eq_" f | ?f _ _ _ _ _ _ _ = _ => fresh "eq_" f | ?f _ _ _ _ _ _ _ _ = _ => fresh "eq_" f | _ = ?f => fresh "eq_" f | _ = ?f _ => fresh "eq_" f | _ = ?f _ _ => fresh "eq_" f | _ = ?f _ _ _ => fresh "eq_" f | _ = ?f _ _ _ _ => fresh "eq_" f | _ = ?f _ _ _ _ _ => fresh "eq_" f | _ = ?f _ _ _ _ _ _ => fresh "eq_" f | _ = ?f _ _ _ _ _ _ _ => fresh "eq_" f | _ = ?f _ _ _ _ _ _ _ _ => fresh "eq_" f | @eq bool _ true => fresh "eq_bool_true" | @eq bool _ false => fresh "eq_bool_false" | @eq bool true _ => fresh "eq_bool_true" | @eq bool false _ => fresh "eq_bool_false" | @eq bool _ _ => fresh "eq_bool" | @eq nat _ true => fresh "eq_nat_true" | @eq nat _ false => fresh "eq_nat_false" | @eq nat true _ => fresh "eq_nat_true" | @eq nat false _ => fresh "eq_nat_false" | @eq nat _ _ => fresh "eq_nat" | ?x <> _ => fresh "neq_" x | _ <> ?x => fresh "neq_" x | _ <> _ => fresh "neq" | _ = _ => fresh "eq" | _ /\ _ => fresh "and" | _ \/ _ => fresh "or" | @ex _ _ => fresh "ex" | ?x < ?y => fresh "lt_" x "_" y | ?x < _ => fresh "lt_" x | _ < _ => fresh "lt" | ?x <= ?y => fresh "le_" x "_" y | ?x <= _ => fresh "le_" x | _ <= _ => fresh "le" | ?x > ?y => fresh "gt_" x "_" y | ?x > _ => fresh "gt_" x | _ > _ => fresh "gt" | ?x >= ?y => fresh "ge_" x "_" y | ?x >= _ => fresh "ge_" x | _ >= _ => fresh "ge" | (?x < ?y)%Z => fresh "lt_" x "_" y | (?x < _)%Z => fresh "lt_" x | (_ < _)%Z => fresh "lt" | (?x <= ?y)%Z => fresh "le_" x "_" y | (?x <= _)%Z => fresh "le_" x | (_ <= _)%Z => fresh "le" | (?x > ?y)%Z => fresh "gt_" x "_" y | (?x > _)%Z => fresh "gt_" x | (_ > _)%Z => fresh "gt" | (?x >= ?y)%Z => fresh "ge_" x "_" y | (?x >= _)%Z => fresh "ge_" x | (_ >= _)%Z => fresh "ge" | ~ (_ = _) => fail 1(* h_neq already dealt by fallback *) | ~ ?th' => let sufx := fallback_rename_hyp h th' in fresh "neg_" sufx | ~ ?th' => fresh "neg" (* Order is important here: *) | ?A -> ?B => let nme := fallback_rename_hyp h B in fresh "impl_" nme | forall z:?A , ?B => fresh "forall_" z end. Inductive HypPrefixes := | HypNone | HypH_ | HypH. (* One should rename this if needed *) Ltac prefixable_eq_neq h th := match th with | eq _ _ => HypH | ~ (eq _ _) => HypH | _ => HypH_ end. Ltac prefixable h th := prefixable_eq_neq h th. (* Add prefix except if not a Prop or if prefixable says otherwise. *) Ltac add_prefix h th nme := match type of th with | Prop => match prefixable h th with | HypH_ => fresh "h_" nme | HypH => fresh "h" nme | HypNone => nme end | _ => nme end. Ltac fallback_rename_hyp_prefx h th := let res := fallback_rename_hyp h th in add_prefix h th res. (* fresh "h_" res. *) (* Add this if you want hyps of typr ~ P to be renamed like if of type P but prefixed by "neg_" *) Ltac rename_hyp_neg h th := match th with | ~ (_ = _) => fail 1(* h_neq already dealt by fallback *) | ~ ?th' => let sufx := fallback_rename_hyp h th' in fresh "neg_" sufx | ~ ?th' => fresh "neg" | _ => fail end. (* Credit for the harvesting of hypothesis: Jonathan Leivant *) Ltac harvest_hyps harvester := constr:(ltac:(harvester; constructor) : True). Ltac revert_clearbody_all := repeat lazymatch goal with H:_ |- _ => try clearbody H; revert H end. Ltac all_hyps := harvest_hyps revert_clearbody_all. Ltac next_hyp hs step last := lazymatch hs with | (?hs' ?H) => step H hs' | _ => last end. Ltac map_hyps tac hs := idtac; let rec step H hs := next_hyp hs step idtac; tac H in next_hyp hs step idtac. (* Renames hypothesis H if it is not in old_hyps. Use user defined renaming scheme, and fall back to the default one of it fails. *) Ltac rename_if_not_old old_hyps H := lazymatch old_hyps with | context[H] => idtac | _ => match type of H with (* | ?th => let dummy_name := fresh "dummy" in rename H into dummy_name; (* this renaming makes the renaming more or less idempotent, it is backtracked if the rename_hyp below fails. *) let newname := rename_hyp dummy_name th in rename dummy_name into newname*) | ?th => let dummy_name := fresh "dummy" in rename H into dummy_name; (* this renaming makes the renaming more or less idempotent, it is backtracked if the rename_hyp below fails. *) let newname := fallback_rename_hyp_prefx dummy_name th in rename dummy_name into newname | _ => idtac (* "no renaming pattern for " H *) end end. Ltac rename_new_hyps tac := let old_hyps := all_hyps in let renam H := rename_if_not_old old_hyps H in tac; let new_hyps := all_hyps in map_hyps renam new_hyps. Ltac rename_all_hyps := let renam H := rename_if_not_old (I) H in let hyps := all_hyps in map_hyps renam hyps. Ltac autorename H := rename_if_not_old (I) H. Tactic Notation "!!" tactic3(Tac) := (rename_new_hyps Tac). Tactic Notation "!!" tactic3(Tac) constr(h) := (rename_new_hyps (Tac h)). Ltac subst_if_not_old old_hyps H := match old_hyps with | context [H] => idtac | _ => match type of H with | ?x = ?y => subst x | ?x = ?y => subst y | _ => idtac end end. Ltac subst_new_hyps tac := let old_hyps := all_hyps in let substnew H := subst_if_not_old old_hyps H in tac ; let new_hyps := all_hyps in map_hyps substnew new_hyps. (* do we need a syntax for this. *) (* Tactic Notation "" tactic3(Tac) := subst_new_hyps Tac. *) (* !!! tac performs tac, then subst with new hypothesis, then rename remaining new hyps. *) 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 <>. We might try to find a better way to mark hypothesis. *) (* Tactic Notation "!!" tactic3(T) := idall; T ; rename_hyps. *) (* Tactic Notation "!!" tactic3(T) constr(h) := *) (* idall; try unid h; (T h) ; try id_ify h; rename_hyps. *) (* begin hide *) (* Tactic Notation "!!" tactic3(T) constr(h) constr(h2) := *) (* idall; try unid h;try unid h2; (T h h2) ; *) (* try id_ify h;try id_ify h2; rename_hyps. *) (* end hide *) (** ** 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. *) Ltac decomp_ex h := match type of h with | @ex _ (fun x => _) => let x' := fresh x in let h1 := fresh in destruct h as [x' h1]; decomp_ex h1 | @sig _ (fun x => _) => let x' := fresh x in let h1 := fresh in destruct h as [x' h1]; decomp_ex h1 | @sig2 _ (fun x => _) (fun _ => _) => let x' := fresh x in let h1 := fresh in let h2 := fresh in destruct h as [x' h1 h2]; decomp_ex h1; decomp_ex h2 | @sigT _ (fun x => _) => let x' := fresh x in let h1 := fresh in destruct h as [x' h1]; decomp_ex h1 | @sigT2 _ (fun x => _) (fun _ => _) => let x' := fresh x in let h1 := fresh in let h2 := fresh in destruct h as [x' h1 h2]; decomp_ex h1; decomp_ex h2 | and _ _ => let h1 := fresh in let h2 := fresh in destruct h as [h1 h2]; decomp_ex h1; decomp_ex h2 | or _ _ => let h' := fresh in destruct h as [h' | h']; [decomp_ex h' | decomp_ex h' ] | _ => idtac end. (* decompose and ex and or at once. TODO: generalize. *) (* clear may fail if h is not a hypname *) (* Tactic Notation "decomp" hyp(h) := (!! (idtac;decomp_ex h)). *) (* Why do I need this idtac? Without it no rename happens. *) 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 (* Why do I need this idtac? Without it no rename happens. *) end. (* Lemma foo : forall x, { aa:nat | (aa = x /\ x=aa) & (aa = aa /\ aa= x) } -> False. Proof. intros x H. decomp H. Abort. Lemma foo : { aa:False & True } -> False. Proof. intros H. decomp H. Abort. Lemma foo : { aa:False & True & False } -> False. Proof. intros H. decomp H. Abort. *) Tactic Notation "!induction" constr(h) := !! (induction h). Tactic Notation "!functional" "induction" constr(h) := !! (functional induction h). Tactic Notation "!functional" "inversion" constr(h) := !! (functional inversion 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. *) (* This performs the map from "top" to "bottom" (from older to younger hyps). *) Ltac map_hyps_rev tac hs := idtac; let rec step H hs := tac H ; next_hyp hs step idtac in next_hyp hs step idtac. Ltac map_all_hyps tac := map_hyps tac all_hyps. Ltac map_all_hyps_rev tac := map_hyps_rev tac all_hyps. (* A tactic which moves up a hypothesis if it sort is Type or Set. *) Ltac move_up_types H := match type of H with | ?T => match type of T with | Prop => idtac | Set => move H at top | Type => move H at top end end. (* Iterating the tactic on all hypothesis. Moves up all Set/Type variables to the top. Really useful with [Set Compact Context] which is no yet commited in coq-trunk. *) Ltac up_type := map_all_hyps_rev move_up_types. (* A full example: *) (* Ltac rename_hyp_2 h th := match th with | true = false => fresh "trueEQfalse" end. Ltac rename_hyp ::= rename_hyp_2. Lemma foo: forall x y, x <= y -> x = y -> ~1 < 0 -> (0 < 1 -> ~(true=false)) -> (forall w w',w < w' -> ~(true=false)) -> (0 < 1 -> ~(1<0)) -> (0 < 1 -> 1<0) -> 0 < 1. (* auto naming at intro: *) !intros. Undo. (* intros first, rename after: *) intros. rename_all_hyps. Undo. (* intros first, rename some hyp only: *) intros. autorename H0. (* put !! before a tactic to rename all new hyps: *) rename_all_hyps. !!destruct h_le_x_y eqn:?. - auto with arith. - auto with arith. Qed. *)