The Coq mailing list

[Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de>]

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.

Attachment: signature.asc
Description: OpenPGP digital signature