[Coq-Club] Make constants/functions opaque for [rewrite]

[Maximilian Wuttke]

Hi Coq Club members,


In my project I have some functions on natural numbers. Two of them are
coincidently equal, although the contexts in which I use them are not
related to each other. I also have shown lemmas about these functions.
(Yes, these lemmas are duplicated for the duplicated functions.)

What can I do, so that [rewrite] _does_ distinguish between these
functions, i.e. [rewrite] sees the names of the two functions as
distinct constants? Below is a minimal example.

The reasons for wanting this are two-fold:
1. It can confuse the user of my library. ("Why is there suddenly a
totally unrelated function after [autorewrite]?" ~> this may break
proofs with [omega])
2. It is more efficient to not unfold the constants.

I already tried out some things that I found while reading the refman,
but mabye I missed something.

In case it matters:

```
$ coqtop --version
The Coq Proof Assistant, version 8.8.2 (November 2018)
compiled on Nov 18 2018 20:32:22 with OCaml 4.07.1

```


Sincerely
Maximilian Wuttke



(* I have two totally unrelated function, that just happen to be
coincidently equal. (They actually occur at different parts of the
project) *)
Definition tam (x : nat) := S x.
Definition tam'(x : nat) := S x.

(* Both functions are compatible w.r.t. some function, e.g. [S] *)
Lemma tam_S (x : nat) : tam (S x) = S (tam x).
Proof. reflexivity. Qed.
Lemma tam'_S (x : nat) : tam' (S x) = S (tam' x).
Proof. reflexivity. Qed.

(* Now I want that [rewrite] sees them as distinct constants. *)

(* But nothing of this solves my problem *)
Arguments tam : simpl never. Arguments tam' : simpl never.
Hint Opaque tam tam'.
Typeclasses Opaque tam tam'.
Opaque tam tam'.

(* I also expect this to not simplify. This works, thanks to the above
[Arguments] vernacular: *)
Eval cbn in tam 42.

(* I DO NOT want to be able to proof this with [rewrite] *)
Goal forall x, tam (S x) = tam' (S x).
Proof.
intros.
(* This should change the goal to [tam (S x) = S (tam' x)] *)
rewrite tam'_S.
(* It reduces to [S (tam' x) = tam' (S x)] instead. I.e. it saw that
[tam=tam'] and rewrote [tam'_S] in [tam (S n)]. This is exactly what I
want to prevent. *)
Abort.


(* At a later part of the project, I want to be able to unfold the
constants though. So making them completly opaque (i.e. with [Qed]) is
no option. *)
Goal forall (x : nat), tam x <= tam (x+x). (* (actually we want to show
that a function using [tam] is in some complexity class) *)
Proof.
Require Import Omega.
Transparent tam.
intros. unfold tam. omega.
Qed.

[Li-yao Xia]

That's quite a surprising behavior of rewrite. One way to get what you
want is to abstract one of them with the remember tactic before rewriting.

remember tam as tam0. rewrite tam'_S. subst tam0.

Li-yao

Post by Maximilian Wuttke
Hi Coq Club members,
In my project I have some functions on natural numbers. Two of them are
coincidently equal, although the contexts in which I use them are not
related to each other. I also have shown lemmas about these functions.
(Yes, these lemmas are duplicated for the duplicated functions.)
What can I do, so that [rewrite] _does_ distinguish between these
functions, i.e. [rewrite] sees the names of the two functions as
distinct constants? Below is a minimal example.
1. It can confuse the user of my library. ("Why is there suddenly a
totally unrelated function after [autorewrite]?" ~> this may break
proofs with [omega])
2. It is more efficient to not unfold the constants.
I already tried out some things that I found while reading the refman,
but mabye I missed something.
```
$ coqtop --version
The Coq Proof Assistant, version 8.8.2 (November 2018)
compiled on Nov 18 2018 20:32:22 with OCaml 4.07.1
```
Sincerely
Maximilian Wuttke
(* I have two totally unrelated function, that just happen to be
coincidently equal. (They actually occur at different parts of the
project) *)
Definition tam (x : nat) := S x.
Definition tam'(x : nat) := S x.
(* Both functions are compatible w.r.t. some function, e.g. [S] *)
Lemma tam_S (x : nat) : tam (S x) = S (tam x).
Proof. reflexivity. Qed.
Lemma tam'_S (x : nat) : tam' (S x) = S (tam' x).
Proof. reflexivity. Qed.
(* Now I want that [rewrite] sees them as distinct constants. *)
(* But nothing of this solves my problem *)
Arguments tam : simpl never. Arguments tam' : simpl never.
Hint Opaque tam tam'.
Typeclasses Opaque tam tam'.
Opaque tam tam'.
(* I also expect this to not simplify. This works, thanks to the above
[Arguments] vernacular: *)
Eval cbn in tam 42.
(* I DO NOT want to be able to proof this with [rewrite] *)
Goal forall x, tam (S x) = tam' (S x).
Proof.
intros.
(* This should change the goal to [tam (S x) = S (tam' x)] *)
rewrite tam'_S.
(* It reduces to [S (tam' x) = tam' (S x)] instead. I.e. it saw that
[tam=tam'] and rewrote [tam'_S] in [tam (S n)]. This is exactly what I
want to prevent. *)
Abort.
(* At a later part of the project, I want to be able to unfold the
constants though. So making them completly opaque (i.e. with [Qed]) is
no option. *)
Goal forall (x : nat), tam x <= tam (x+x). (* (actually we want to show
that a function using [tam] is in some complexity class) *)
Proof.
Require Import Omega.
Transparent tam.
intros. unfold tam. omega.
Qed.

[Jason -Zhong Sheng- Hu]

I suppose this is a bug. If you try

rewrite (tam'_S x).

then the RHS is rewritten. The refman doesn't mention rewrite will try to be this smart either.

However, this only looks feasible when you have two definitionally equal functions. Is it the case in your actual use case?

Sincerely Yours,

Jason Hu
________________________________
From: coq-club-***@inria.fr <coq-club-***@inria.fr> on behalf of Li-yao Xia <***@gmail.com>
Sent: November 18, 2018 5:18 PM
To: coq-***@inria.fr
Subject: Re: [Coq-Club] Make constants/functions opaque for [rewrite]

That's quite a surprising behavior of rewrite. One way to get what you
want is to abstract one of them with the remember tactic before rewriting.

remember tam as tam0. rewrite tam'_S. subst tam0.

Li-yao

Post by Maximilian Wuttke
Hi Coq Club members,
In my project I have some functions on natural numbers. Two of them are
coincidently equal, although the contexts in which I use them are not
related to each other. I also have shown lemmas about these functions.
(Yes, these lemmas are duplicated for the duplicated functions.)
What can I do, so that [rewrite] _does_ distinguish between these
functions, i.e. [rewrite] sees the names of the two functions as
distinct constants? Below is a minimal example.
1. It can confuse the user of my library. ("Why is there suddenly a
totally unrelated function after [autorewrite]?" ~> this may break
proofs with [omega])
2. It is more efficient to not unfold the constants.
I already tried out some things that I found while reading the refman,
but mabye I missed something.
```
$ coqtop --version
The Coq Proof Assistant, version 8.8.2 (November 2018)
compiled on Nov 18 2018 20:32:22 with OCaml 4.07.1
```
Sincerely
Maximilian Wuttke
(* I have two totally unrelated function, that just happen to be
coincidently equal. (They actually occur at different parts of the
project) *)
Definition tam (x : nat) := S x.
Definition tam'(x : nat) := S x.
(* Both functions are compatible w.r.t. some function, e.g. [S] *)
Lemma tam_S (x : nat) : tam (S x) = S (tam x).
Proof. reflexivity. Qed.
Lemma tam'_S (x : nat) : tam' (S x) = S (tam' x).
Proof. reflexivity. Qed.
(* Now I want that [rewrite] sees them as distinct constants. *)
(* But nothing of this solves my problem *)
Arguments tam : simpl never. Arguments tam' : simpl never.
Hint Opaque tam tam'.
Typeclasses Opaque tam tam'.
Opaque tam tam'.
(* I also expect this to not simplify. This works, thanks to the above
[Arguments] vernacular: *)
Eval cbn in tam 42.
(* I DO NOT want to be able to proof this with [rewrite] *)
Goal forall x, tam (S x) = tam' (S x).
Proof.
intros.
(* This should change the goal to [tam (S x) = S (tam' x)] *)
rewrite tam'_S.
(* It reduces to [S (tam' x) = tam' (S x)] instead. I.e. it saw that
[tam=tam'] and rewrote [tam'_S] in [tam (S n)]. This is exactly what I
want to prevent. *)
Abort.
(* At a later part of the project, I want to be able to unfold the
constants though. So making them completly opaque (i.e. with [Qed]) is
no option. *)
Goal forall (x : nat), tam x <= tam (x+x). (* (actually we want to show
that a function using [tam] is in some complexity class) *)
Proof.
Require Import Omega.
Transparent tam.
intros. unfold tam. omega.
Qed.