Stream: Coq users

Topic: Tactics split, destruct, induction etc ignore Opaque


view this post on Zulip Lef Ioannidis (Apr 22 2024 at 21:24):

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.

view this post on Zulip Théo Winterhalter (Apr 23 2024 at 06:26):

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

view this post on Zulip Théo Winterhalter (Apr 23 2024 at 06:27):

Without relying on SSReflect, you can reproduce the lock pattern easily.

view this post on Zulip Guillaume Melquiond (Apr 23 2024 at 06:42):

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.

view this post on Zulip Pierre Roux (Apr 23 2024 at 09:37):

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

view this post on Zulip Lef Ioannidis (Apr 24 2024 at 02:06):

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


Last updated: Jun 22 2024 at 15:01 UTC