The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

A related issue is that rewrite also doesn't backtrack if it fails to solve a
sidecondition: https://github.com/coq/coq/issues/7672
That issue (and a few other rewrite issues) made me learn how to write my own
rewrite tactics in Ltac. 
In your case, the following home-made rewrite tactic might work:

Require Import ZArith.

Open Scope Z_scope.

Lemma rew_zoom_bw{T: Type}{lhs rhs: T}:
  lhs = rhs ->
  forall P : T -> Prop, P rhs -> P lhs.
Proof.
  intros. subst. assumption.
Qed.

Ltac rewr equ :=
  match type of equ with
  | ?LHS = _ =>
    match goal with
    | |- context C[LHS] =>
      change ((fun x => ltac:(let b := context C[x] in exact b)) LHS);
      apply (rew_zoom_bw equ)
    end
  end.

Lemma xx  (p:3=4) (n: 3=6 -> Z) : 1= match Z.eq_dec 3 6 return Z with
                                        | left p => n p
                                        | right _ => 7
                                    end + 3.
Proof using.
  rewr p.


Note that usually, I would use "pattern" in my home-made rewrite tactics, but
"pattern" has the same dependent types issue as Coq's and ssr's rewrite, so I
used "context" instead, so that only one occurrence is cut out at a time.


On Mon, 2021-10-11 at 18:31 -0700, Abhishek Anand wrote:
> Is there a Coq rewrite tactic that will try to rewrite as many occurrences 
> as
> possible instead of just failing when one occurrence cannot be rewritten:
> 
> Require Import ZArith.
> 
> Open Scope Z_scope.
> Lemma xx  (p:3=4) (n: 3=6 -> Z) : 1= match Z.eq_dec 3 6 return Z with
>                                         | left p => n p
>                                         | right _ => 7
>                                     end + 3.
> Proof using.
>   Fail rewrite_strat (try topdown p).
>   Fail rewrite_strat (try bottomup p).
>   Fail rewrite_strat (try innermost p).
>   Fail rewrite_strat (try outermost p).
>   Fail rewrite p.
>   rewrite p at 2.
> Abort.
> 
> 
> 
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/