The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Thanks Jason. I just tried `topdown try p` and it ran into stack overflow:

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.
  rewrite_strat (topdown try p). (* stack overflow *)

Abort.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Mon, Oct 11, 2021 at 8:33 PM Jason Gross <jasongross9 AT gmail.com> wrote:

I haven't tried it myself, but I expect topdown try p to work fine.  But it seems like a bug for rewrite_strat try foo to ever fail

On Mon, Oct 11, 2021, 20:11 Samuel Gruetter <gruetter AT mit.edu> wrote:

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/