I am struggling with Coq's normalization again. Can I force a definition to not normalize, even in the face of destruct, split, induction etc? I tried Opaque and unfortunately it's not opaque enough. Same for `simpl never`

. I really want to force the user to only interact with `add`

through the `unfold_add`

lemma.

Is it possible to completely block unfolding, normalization etc even on destruct and split?

```
Fixpoint add(a b c: nat): Prop :=
match a, c with
| 0, _ => b = c
| S n, S m => add n b m
| S _, 0 => False
end.
Lemma unfold_add: forall a b c,
add a b c = match a, c with
| 0, _ => b = c
| S n, S m => add n b m
| S _, 0 => False
end.
Proof. destruct a; reflexivity. Qed.
Opaque add.
Arguments add: simpl never.
Goal add 1 2 4 -> add 1 2 4.
intros H.
destruct H. (* Why doesn't this Fail? Can I make it fail? *)
split. (* Same here, can I force split to fail? *)
Abort.
```

Perhaps you're looking for `locking`

: https://coq.inria.fr/doc/V8.19.0/refman/proof-engine/ssreflect-proof-language.html?highlight=lock#locking-unlocking

Without relying on SSReflect, you can reproduce the `lock`

pattern easily.

If you want to make a definition definitely opaque, you can seal it inside a module:

```
Module Type TFoo.
Parameter add : nat -> nat -> nat -> Prop.
Parameter unfold_add : forall a b c, add a ...
End TFoo.
Module Foo : TFoo.
Fixpoint add (a b c: nat) ...
Lemma unfold_add: ...
Proof. destruct a; reflexivity. Qed.
End Foo.
```

And if you are using coq-elpi, it offers the `lock`

and `mlock`

commands to do all the boilerplate for you: https://github.com/LPCIC/coq-elpi/tree/master/apps/locker

Locking/unlocking is precisely what I need, thank you to all!

Last updated: Jun 22 2024 at 15:01 UTC