Indeterminate value for partial functions trick

Using Coq
1

There’s an old truck for encoding partial functions with opaque or postulated values.

Axiom unknown: nat -> nat.

Fixpoint sub m n :=
   match m, n with
   | _, O => m
   | S m', S n' => sub m' n'
   | O, S n' => unknown n'
   end.

Instead of axiom I think you can do

Definition unknown (n: nat) := n.
#[global]
Opaque unknown.

But I’m not quite sure how opaque values work in Coq.

I think you might need Qed?

A more honest encoding might use modules I think?

2

Yes, you can do it as follows;

Definition unknown(n: nat): nat.
Proof. exact n. Qed.
1 Like
3

Slightly annoying there’s not a better way to do this. But this is good enough definitely.

Maybe you could call into ltac and define with Qed?

Notation "'OPAQUE' p" := (ltac:(mkopaque p)).
4

Bleh abstract looks like what I want but seems problematic

https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.abstract

5

Ahah! I found a genuine evil trick.

Define

Definition opaque {A} (x: A): A.
Proof.
  exact x.
Qed.

Then elsewhere define

Definition unknown = opaque (fun n: nat => n).

So you don’t really even need tactics or notations to cleanup the trick.

There’s some tricky weirdness with the trick though.

I think it doesn’t really work with strict prop or homotopy type theory stuff. Extensional type theory makes id equivalent to unit right?

Definition opaque: unit.
Proof.
  exact tt.
Qed.

Definition unknown: nat -> nat :=
  match opaque with
  | _ => fun n => n
  end.

Is a similar way of doing the same thing. But you can prove all units are the same so it doesn’t quite work. You can stack on top of this private inductive types devilry?

#[private]
Variant fence: Set := post.

Definition opaque: fence.
Proof.
  exact post.
Qed.

Definition unknown: nat -> nat :=
   match opaque with
   | _ => fun n => n
   end.