The Coq mailing list

[Edwin Westbrook <westbrook AT kestrel.edu>]

All,

In case it is useful, here is a slight modification I wrote recently that does always terminate:

Ltac all_rewrites :=

  match goal with

    | hyp:_ |- _ => rewrite hyp; revert hyp; all_rewrites

    | _ => intros

  end.

Each time a hypothesis is used to perform a rewrite, it is "reverted", so that it will not get matched again.

-Eddy

On Nov 13, 2013, at 1:39 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

Here is autorewrite using just hypotheses (it may loop, just like autorewrite):

repeat match goal with

            | [ H : _ |- _ ] => rewrite H

          end.

-Jason

On Wed, Nov 13, 2013 at 4:24 AM, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Coq users,

 

I wonder if there is something like autorewrite, which can use hypothesis. This would be handy e.g. in the proof below from the SW foundations course. Something like “Hint Rewrite Hd1 Hd2: base“ doesn’t seem to work. I know that autorewrite can be dangerous because it can loop forever, but couldn’t one make an autorewrite tactic, which uses all equality hypothesis but only such that the goal gets shorter, possibly using only hypothesis with no or trivial pre-conditions? Then it would be guaranteed to terminate and this might be handy in quite a few situations.

 

Best regards,

 

Michael

 

Theorem bool_fn_applied_thrice:

  forall (f : bool -> bool) (b : bool),

  f (f (f b)) = f b.

Proof.

  intros.

  destruct (f true) eqn:Hd1.

    destruct (f false) eqn:Hd2.

      destruct b.

        rewrite -> Hd1. rewrite -> Hd1. rewrite -> Hd1. reflexivity.

        rewrite -> Hd2. rewrite -> Hd1. rewrite -> Hd1. reflexivity.

      destruct b.

        rewrite -> Hd1. rewrite -> Hd1. rewrite -> Hd1. reflexivity.

        rewrite -> Hd2. rewrite -> Hd2. rewrite -> Hd2. reflexivity.

    destruct (f false) eqn:Hd2.

      destruct b.

        rewrite -> Hd1. rewrite -> Hd2. rewrite -> Hd1. reflexivity.

        rewrite -> Hd2. rewrite -> Hd1. rewrite -> Hd2. reflexivity.

      destruct b.

        rewrite -> Hd1. rewrite -> Hd2. rewrite -> Hd2. reflexivity.

        rewrite -> Hd2. rewrite -> Hd2. rewrite -> Hd2. reflexivity.

Qed.

 

P.S.: I know that this can be done shorter, but this way the proof is closer to how I would do it mentally.