Maximilian Wuttke

2018-11-18 20:17:08 UTC

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.

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.