Stream: Coq users

Topic: Correct type for functions involving specifications?


view this post on Zulip Justin Kelm (Oct 19 2023 at 21:49):

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?

view this post on Zulip Huỳnh Trần Khanh (Oct 20 2023 at 00:01):

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

view this post on Zulip Huỳnh Trần Khanh (Oct 20 2023 at 00:01):

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

view this post on Zulip Huỳnh Trần Khanh (Oct 20 2023 at 00:03):

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

view this post on Zulip Justin Kelm (Oct 20 2023 at 00:46):

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.

view this post on Zulip Huỳnh Trần Khanh (Oct 20 2023 at 01:01):

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

view this post on Zulip Huỳnh Trần Khanh (Oct 20 2023 at 01:01):

I apologize for the confusion

view this post on Zulip Huỳnh Trần Khanh (Oct 20 2023 at 01:02):

yeah looks like my approach is appropriate for your situation

view this post on Zulip Justin Kelm (Oct 20 2023 at 06:01):

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.

view this post on Zulip Karl Palmskog (Oct 20 2023 at 07:11):

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

view this post on Zulip Karl Palmskog (Oct 20 2023 at 07:16):

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.

view this post on Zulip Guillaume Melquiond (Oct 20 2023 at 08:37):

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.

view this post on Zulip Guillaume Melquiond (Oct 20 2023 at 08:40):

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.

view this post on Zulip Paolo Giarrusso (Oct 20 2023 at 17:02):

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

view this post on Zulip Paolo Giarrusso (Oct 20 2023 at 17:02):

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

view this post on Zulip Justin Kelm (Oct 21 2023 at 02:15):

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 *)

view this post on Zulip Justin Kelm (Oct 21 2023 at 02:19):

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.

view this post on Zulip Huỳnh Trần Khanh (Oct 21 2023 at 02:26):

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

view this post on Zulip Gaëtan Gilbert (Oct 21 2023 at 07:27):

stdlib is LGPL too so what are you using?

view this post on Zulip Karl Palmskog (Oct 21 2023 at 07:35):

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