The Coq mailing list

[Eric Mullen <emullen AT cs.washington.edu>]

How about subst? Have you tried that tactic?

Best!

Eric

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

Thanks Jason!

 

if other Coq beginners (like me) wonder how to make a named tactic out of this:

 

    Ltac rewritehyp := repeat match goal with | [ H : _ |- _ ] => rewrite H end.

 

seems to be the right way of doing it.

 

Best regards,

 

Michael

 

From: Jason Gross

Sent: Wednesday, November 13, 2013 10:39 AM

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.