The code below shows my problem:

```
Definition foo_type := {n : nat | n*n + 24 = 10*n} -> {n : nat | n*n + 35 = 12*n}.
Example foo_plus_one : foo_type.
intros [n Hn]. exists (n+1); lia. Defined.
Example foo_plus_one_proof_indep : forall n m,
proj1_sig n = proj1_sig m -> proj1_sig (foo_plus_one n) = proj1_sig (foo_plus_one m).
Proof. intros [n Hn] [m Hm]; cbn; lia. Qed.
Lemma foo_type_proof_indep : forall (f : foo_type) n m,
proj1_sig n = proj1_sig m -> proj1_sig (f n) = proj1_sig (f m).
Abort.
```

I would like `foo_type`

to denote the type of those functions which, when given an input that satisfies a certain spec, returns an output that satisfies another spec, such that the output does not depend on the proof of the input spec. I imagine that globally asserting proof irrelevance would be one way to do this; another would supercharging the definition of `foo_type`

to explicitly include `foo_type_proof_indep`

as part of its data, something horrific like

```
{foo : {n : nat | n*n + 24 = 10*n} -> {n : nat | n*n + 35 = 12*n} |
forall n m, proj1_sig n = proj1_sig m -> proj1_sig (foo n) = proj1_sig (foo m)}.
```

I presume there's a better way?

yes there's a much better way. make a structure Constrained with these fields: f maps from nat to nat, and outputConstraint: `forall n, n * n + 24 = 10 * n -> f n * f n + 35 = 12 * f n`

don't try to use subtypes for function arguments and return value, just use an independent lemma to constrain this

now of course folks tend to post an oversimplified description of their problems so I can't guarantee my solution makes sense. if this answer makes no sense to you please post more details

Right. In my case, I'm trying to formalize the proof of a winning strategy of a certain combinatorial game. Instead of `nat`

, I'm dealing with `Gamestate`

, an inductive datatype capturing the game at a particular point in time. Rather than `foo_type`

I want to define what is a `Strategy p`

, which is a function that takes an `x : Gamestate`

(satisfying the spec that it's the turn of the correct player `p`

, and also not game over) and returns another `y : Gamestate`

(satisfying the spec that `x ==> y`

, where `==>`

is an inductive Prop describing a legal move).

I want to do this so that I can define what is the outcome of a `Gamestate`

when each player is equipped with a given `Strategy`

, and then define "`x : Gamestate`

is *won by player one* if `exists (s1 : Strategy P1), forall (s2 : Strategy P2), outcome x s1 s2 = P1`

". The gist is, I'm going to have to manipulate statements involving universal quantifications over all functions of correct input-output spec.

By "structure" are you referring to this? If so, I'll have to read up on it and see if it applies to my situation.

no I just mean an ordinary Record lol. I frequently jump between languages and I often mix things up

I apologize for the confusion

yeah looks like my approach is appropriate for your situation

Thank you. You know, I don't even think this is my first time learning that subset types are kind of a huge pain to use in lieu of entire functions + independent lemmas. I recently got back into Coq through *Certified Programming with Dependent Types*, and Chlipala gives a pretty glowing recommendation of the use of subset types in Chapter 6. Maybe I just need better notation and automation to handle this use case? Not sure.

have you tried using Equations? It's the standard recommendation when doing nontrivial definitions.

for example, to take a classic function, I think the following is quite close to the non-sigma-type versions:

```
Equations nsqrt_aux (x : nat) (n : nat) (H : n * n <= x) :
{ r : nat | r * r <= x /\ x < S r * S r } by wf (x - n) lt :=
nsqrt_aux x n H with lt_dec x (S n * S n) := {
| left _ => exist _ n _
| right _ with nsqrt_aux x (S n) _ := { | exist _ r _ => exist _ r _ } }.
Next Obligation. lia. Qed. Next Obligation. lia. Qed.
Equations nsqrt (x : nat) : { r : nat | r * r <= x < S r * S r } :=
nsqrt x with nsqrt_aux x 0 _ := { | exist _ r _ => exist _ r _ }.
Next Obligation. lia. Qed.
```

Justin Kelm said:

I imagine that globally asserting proof irrelevance would be one way to do this

Note that you do not need to assert proof irrelevance. Your specifications are written in a logic fragment where proof irrelevance actually holds:

```
Lemma foo_type_proof_indep : forall (f : foo_type) n m,
proj1_sig n = proj1_sig m -> proj1_sig (f n) = proj1_sig (f m).
Proof.
intros f [n1 H1] [n2 H2] H. simpl in H.
revert H2. rewrite <- H. intros H2.
now rewrite (UIP_nat _ _ H1 H2).
Qed.
```

And in fact, this exact same proof works for a much stronger (and presumably useful) statement:

```
Lemma foo_type_proof_indep : forall (f : foo_type) n m,
proj1_sig n = proj1_sig m -> f n = f m.
Proof.
intros f [n1 H1] [n2 H2] H. simpl in H.
revert H2. rewrite <- H. intros H2.
now rewrite (UIP_nat _ _ H1 H2).
Qed.
```

in general, if `T`

has decidable equality, equality on `T`

is proof irrelevant; in particular, since `bool`

has decidable equality, `boolean_predicate x = true`

is proof-irrelevant as well

stdpp automates much boilerplate about such irrelevance proofs using typeclasses, math-comp achieves similar results by using boolean predicates systematically

Karl Palmskog said:

have you tried using Equations? It's the standard recommendation when doing nontrivial definitions.

I've heard of it but not made the jump to learn it yet. Does it to help alleviate the pain of using sigma types at all? I also don't see how this Equations definition is preferable to one written like this:

```
Require Import Lia Program.Wf Compare_dec.
Program Fixpoint nsqrt_aux (x : nat) (n : nat) (H : n * n <= x) {measure (x-n)} :
{ r : nat | r * r <= x /\ x < S r * S r } :=
if lt_dec x (S n * S n)
then exist _ n _
else nsqrt_aux x (S n) _.
Next Obligation. lia. Qed.
Next Obligation. lia. Qed.
Program Definition nsqrt (x : nat) := nsqrt_aux x 0 _.
Next Obligation. lia. Qed.
Compute (proj1_sig (nsqrt 52)).
(* = 7 *)
```

Guillaume Melquiond said:

Justin Kelm said:

I imagine that globally asserting proof irrelevance would be one way to do this

Note that you do not need to assert proof irrelevance. Your specifications are written in a logic fragment where proof irrelevance actually holds:

That is very interesting to know. Together with Paolo's comment, I can see how this might constitute a more general solution. I think for now I'll stick to classical verification as my approach, though.

actually Equations is quite awesome and does make writing definitions less painful. I don't want to use it though because of LGPL but if you don't mind LGPL then go ahead

stdlib is LGPL too so what are you using?

yeah makes a lot of sense for a plugin to be LGPL-2.1-only since then code can move freely and easily between the plugin and Coq itself. My personal hope is that Equations eventually moves into Coq itself.

Last updated: Jun 13 2024 at 21:01 UTC