The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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.