The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  Consider the following snipplet:

== begin

  Ltac subst_goal :=
    match goal with
      | H: ?a = _ |- context[?a] => rewrite H
    end.

  Ltac subst_hyp :=
    match goal with
      | H: ?a = _, H2: context[?a] |- _=>  rewrite H in H2
    end.

  Ltac subst_all := repeat(subst_goal || subst_hyp || autorewrite with lib).

== end

  Assuming that:

  (1) no path infinite loops (i.e. we don't have "A = B, B = A" , "n = (n+1)-1" or the likes)

  (2) all paths terminate

  (3) all paths terminate to the same goal state

  Then:

  (1) is there an optimal way to write subst_all ? [it's possible that such an optimal does not exist in that for different goal states, diferent orderings are ideal]

  (2) if an optimal approach exists, what is it? (for example, would "repeat (autorewrite with lib || subst_goal || subst_hyp)" be faster?)

  Lastly, is there some Coq builtin which will do this for me? (the "subst" commands sounds similar, but it apperas to do diferent things.)

Thanks!