CODEWITHSUNDEEP
coq
user1868607
user1868607

Reputation: 2600

In-place simplification for Coq

I want this goal:

f (S j') = f (j' + 1)

to be proven automatically by Coq. Currently I have to write:

apply f_equal. omega.

But in general it can be more difficult and I might need to assert for instance that m-0 = m and then rewrite. Is there a way to rewrite a term in-place, as Isabelle has?

Upvotes: 0

Views: 135

Answers (2)

Vilhelm Sjöberg
Vilhelm Sjöberg

Reputation: 503

Coq has an autorewrite tactic which is similar to Isabelle's simplifiers (though in general my impression is that it will not be as high-performance, and Coq users tend to not rely as much on it). Your example could be done like this:

Require Import Arith.

Hint Rewrite Nat.add_1_r : myhints.

Theorem blah : forall (f: nat->nat) j',
    f (S j') = f (j' + 1).
Proof.
  intros.
  autorewrite with myhints.
  reflexivity.
Qed.

Upvotes: 1

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

I'm not sure exactly what you want. Perhaps the replace tactic can be of help to you.

Basically you would write

replace (S j') with (j' + 1).
- (* f (j' + 1) = f (j' + 1) *)
  reflexivity.
- (* j' + 1 = S j' *)
  lia.

(Note that I'm using lia and not omega as omega is deprecated in favour of lia.)

You can even discharge the replacement directly by lia:

replace (S j') with (j' + 1) by lia.
reflexivity.

This way the replacement only succeeds if lia is able to solve the needed equality.

Upvotes: 2

Related Questions