Stream: Coq users

Topic: Choose value based on propositions


view this post on Zulip Julin S (Jun 16 2022 at 06:11):

This might seem like an weird exercise.

I got a set of functions:

I need the defintions to be like

Definition f (a b c:nat) : nat :=
    let r0 := (p0 a b c) in
    (* Would've been easy if this was possible *)
    match r0 with
    | True => 0
    | False =>
        let r1 := (p1 a b c) in
        match r1 with
        | True => 1
        | False =>
            let r2 := (p2 a b c) in
            match r2 with
            | True => 2
            | False => 3
            end
        end
    end

But this can't be done since we can't pattern match on Prop.

Would've been quite convenient if the p functions returned Type, I guess.
But I can't change the signatures of the functions.

What I need to do is to choose the return value of f based on three propositions.

Is there a way to do this?

Is using sigT a possible way?

The type of the functions can't be changed.

view this post on Zulip Julin S (Jun 16 2022 at 06:18):


p0, p1, p2 could've been like:

Definition p0 (a b c:nat):Prop := a < b < c.
Definition p1 (a b c:nat):Prop := a > b > c.
Definition p2 (a b c:nat):Prop := a < b > c.

view this post on Zulip Julien Puydt (Jun 16 2022 at 06:18):

I have the impression you're trying to build an oracle function to get around the incompleteness theorems -- so I don't think that will work.

view this post on Zulip Julin S (Jun 16 2022 at 06:20):

Actually, I was trying to put up a minimal example of a set of formulas that I had. I guess maybe posting it as such would be clearer.

view this post on Zulip Julien Puydt (Jun 16 2022 at 06:23):

Can't your p0, p1 and p2 have boolean values?

view this post on Zulip Julin S (Jun 16 2022 at 06:27):

I don't think so. But I may be wrong. I'll post the whole thing.

view this post on Zulip Julin S (Jun 16 2022 at 06:30):

Give me a few minutes.

view this post on Zulip Julin S (Jun 16 2022 at 06:42):

This is what I had been trying to encode in coq:

f:(nat -> option nat) -> (nat -> option nat) -> (nat -> option nat)
f a b = c
(* a b:nat->option nat *)


x:nat,
  ((c x) <> None) <->
              x':nat, x' < x          ->
                (a x') = (x - x')      /\
                p0 x'                  /\
                p1 x' x

x:nat,
  (c x) = None <->
            x' < x              ->
            (a x') <> (x - x')  \/
            (p2 x')             \/
            (p3 x' x)

-----

p0 : nat -> Prop
p0 x =
    (c x) <> None      \/
    (b x) <> None

p1 : nat -> nat -> Prop
p1 x1 x2 =
  x:nat,
    x1 < x < x2   ->
    (b x) = None

p2 : nat -> Prop
p2 x =
    (c x) = None    /\
    (b x) = None

p3 : nat -> nat -> Prop
p3 x1 x2 =
  x:nat,
    x1 < x < x2   ->
    (b x) <> None

How can I go about it? Been trying for some time, but without success.

view this post on Zulip Julin S (Jun 16 2022 at 06:43):

Throughout, a and b are arguments of f. Likewise c is the return value of f.

view this post on Zulip Julien Puydt (Jun 16 2022 at 06:46):

Your previous question had f compute something with the results of p*, but here it's the reverse, isn't it?

view this post on Zulip Julien Puydt (Jun 16 2022 at 06:47):

The situation here seems much better: I see many x' < x which mean a bounded check, hence something that is a boolean.

view this post on Zulip Julien Puydt (Jun 16 2022 at 06:50):

The declaration b: nat -> nat and the usage (b x) <> None don't seem coherent.

view this post on Zulip Julin S (Jun 16 2022 at 06:55):

Sorry, all the (nat -> nat) should've been (nat -> option nat). Correcting.

view this post on Zulip Julin S (Jun 16 2022 at 06:58):

The p functions got to be returning Prop, right? Since there are <> None usages and we can't have an isNone or isSome function. Or can we?

view this post on Zulip Kenji Maillard (Jun 16 2022 at 07:01):

you can have

Definition isNone {A} (x : option A) : bool := match x with None => true | _ => false end.

view this post on Zulip Kenji Maillard (Jun 16 2022 at 07:03):

and if you want to use isNone x as a proposition transparently, you can make the function is_true : bool -> Prop := fun b => b = true a coercion (that's one of the default setting if you were to load ssreflect)

view this post on Zulip Julin S (Jun 16 2022 at 07:12):

:face_palm: I don't know what I had been thinking when I said we can't have isNone...

view this post on Zulip Julin S (Jun 16 2022 at 08:52):

Oh, I was thinking of getSome: option A -> A.

view this post on Zulip Julin S (Jun 16 2022 at 09:11):

Julien Puydt said:

The situation here seems much better: I see many x' < x which mean a bounded check, hence something that is a boolean.

But those x < x' would have to be part of Prop values though, right?

For instance, p1 is something like:

Definition p1 (b:nat->option nat) (n1 n2:nat) : Prop :=
  forall n:nat,
    (n1 < n < n2)  ->     (*   andb (Nat.ltb n1 n)  (Nat.ltb n n2) *)
    (b n) = None.         (*  (isNone (b n))                                          *)

view this post on Zulip Kenji Maillard (Jun 16 2022 at 09:25):

There are at least 2 variations that are possible around getSome. The first is to take a default value in A, possibly with automation provided by typeclasses/canonical instances. The second is to take as an additional argument a proof that the given option is a Some (so you would have getSome : forall {A} (x : option A), isSome x -> A).

view this post on Zulip Julin S (Jun 16 2022 at 09:31):

How would the version with proof look like:

This was my (incorrect) attempt:

Definition getSome_prf {A:Type} (default:A)
  (x:option A) : isSome x -> A :=
  (* Could we also just say  [(x = Some _) -> A] ? *)
  fun prf:(isSome (Some x')) => x'.

view this post on Zulip Gaëtan Gilbert (Jun 16 2022 at 09:43):

something like

match x with
| Some x => fun _ => x
| None => fun prf => (* use that prf is false in this branch *)
end

view this post on Zulip Julin S (Jun 16 2022 at 09:48):

Can a complete standalone getSome_prf function be made like this?

view this post on Zulip Gaëtan Gilbert (Jun 16 2022 at 09:48):

what does that mean?

view this post on Zulip Julin S (Jun 16 2022 at 09:49):

I mean, I tried:

Definition getSome_prf {A:Type} (x:option A) : isSome x -> A :=
  match x with
  | Some x => fun _ => x
  | None => fun prf =>
  end.

But that gave error at the => of None's case.

view this post on Zulip Gaëtan Gilbert (Jun 16 2022 at 09:49):

I didn't fill it in because I didn't look at what definition you used for isSome

view this post on Zulip Julin S (Jun 16 2022 at 09:49):

where isSome is

Definition isNone {A:Type} (x:option A) : Prop :=
  match x with
  | None => True
  | Some _ => False
  end.
Definition isSome {A:Type} (x:option A) : Prop := not (isNone x).

view this post on Zulip Julin S (Jun 16 2022 at 09:49):

Should it return bool?

view this post on Zulip Gaëtan Gilbert (Jun 16 2022 at 09:51):

match prf I with end should work then

view this post on Zulip Gaëtan Gilbert (Jun 16 2022 at 09:51):

ie full code

Definition isNone {A:Type} (x:option A) : Prop :=
  match x with
  | None => True
  | Some _ => False
  end.
Definition isSome {A:Type} (x:option A) : Prop := not (isNone x).

Definition getSome_prf {A:Type} (x:option A) : isSome x -> A :=
  match x with
  | Some x => fun _ => x
  | None => fun prf => match prf I with end
  end.

view this post on Zulip Kenji Maillard (Jun 16 2022 at 09:54):

One thing you should be warned about this approach mixing programs and proofs (the isSome part) is that you can have multiple proofs of isSome x that won't be convertible/definitionally equal (e.g. take two such proofs as argument) and that will bite you when trying to prove theorems on programs using getSome_prf.
With your approach with Prop, you can still prove that all such proofs are propositionally equal (you can show that if p q : isSome x then p = q).
If you use the boolean version you can reuse some standard function because bool has decidable equality, so by Hedberg theorem it verify UIP (from which the previous statement is immediate).
A third solution that I prefer these days (but more advanced) is to have isSome land in SProp so that any two proofs are definitionally equal by construction.

view this post on Zulip Gaëtan Gilbert (Jun 16 2022 at 09:56):

With your approach with Prop, you can still prove that all such proofs are propositionally equal (you can show that if p q : isSome x then p = q).

nope, because it's defined as not so funext gets in the way

view this post on Zulip Kenji Maillard (Jun 16 2022 at 10:03):

oups, Indeed you need to define isSome primitively (in a way similar to isNone)

view this post on Zulip Kenji Maillard (Jun 16 2022 at 10:03):

So the warning should be taken even more seriously :)

view this post on Zulip Julin S (Jun 16 2022 at 10:06):

This problem won't be there if isSome returned bool, right?

view this post on Zulip Julin S (Jun 16 2022 at 10:09):

And in the prf I part of

  | None => fun prf => match prf I with end

prf has type isSome x which ends up being False, right?

So why is it like match prf I with end and not like match prf with end?

view this post on Zulip Gaëtan Gilbert (Jun 16 2022 at 10:11):

prf has type isSome None which reduces to not True ie True -> False

view this post on Zulip Julin S (Jun 16 2022 at 10:12):

Okay, so prf I ends being of type False.

view this post on Zulip Julin S (Jun 16 2022 at 10:14):

And what if isSome returned bool like:

Definition isNoneT {A:Type} (x:option A) : bool :=
  match x with
  | None => true
  | Some _ => false
  end.
Definition isSomeT {A:Type} (x:option A) : bool :=
   negb (isNoneT x).

How can we do getSome_prf?

Trying

Definition getSome_prf {A:Type} (x:option A) : isSomeT x -> A

gave error saying isSomeT x part needed to Set/Prop/Type.

view this post on Zulip Gaëtan Gilbert (Jun 16 2022 at 10:15):

then you need isSomeT x = true when used as a type

view this post on Zulip Julin S (Jun 16 2022 at 10:17):

So the proof for None part would be false = true.

view this post on Zulip Gaëtan Gilbert (Jun 16 2022 at 10:17):

yes
and you have a lemma somewhere that says false = true -> False

view this post on Zulip Julin S (Jun 16 2022 at 10:23):

How would we define getSome_prf with this?

Definition getSome_prf {A:Type} (x:option A)
  : isSomeT x = true -> A :=
  match x with
  | Some x => fun _ => x
  | None => fun prf => _
  end.

Would it be better to define it in proof mode?

How can we leave holes and fill in later? Was it using refine?

With Program coq somehow figured made the proof by itself, though.

view this post on Zulip Julin S (Jun 16 2022 at 12:42):

Could functions like those mentioned here considered examples of 'proof carrying code'?

view this post on Zulip Paolo Giarrusso (Jun 16 2022 at 14:22):

Possibly not, but the idea is similar. The style has enough problems in Coq that many recommend beginners to avoid it.

view this post on Zulip Paolo Giarrusso (Jun 16 2022 at 14:24):

This thread already contains a few tips on pitfalls to account for, but there are probably more.

view this post on Zulip Paolo Giarrusso (Jun 16 2022 at 14:28):

OTOH, _all of the functions used here_ are decidable — instead of

Definition p1 (b:nat->option nat) (n1 n2:nat) : Prop :=
  forall n:nat,
    (n1 < n < n2)  ->     (*   andb (Nat.ltb n1 n)  (Nat.ltb n n2) *)
    (b n) = None.         (*  (isNone (b n))                                          *)

you can write something like this (I might be using stdpp):

Definition p1b (b:nat->option nat) (n1 n2:nat) : bool :=
  forallb (fun n => isNone (b n)) (seq n1 (n2 - n1)).

and prove p1b reflects p1.

view this post on Zulip Gaëtan Gilbert (Jun 16 2022 at 14:29):

do you mean isNone instead of = None?

view this post on Zulip Paolo Giarrusso (Jun 16 2022 at 14:40):

thanks, fixed

view this post on Zulip Gaëtan Gilbert (Jun 16 2022 at 14:41):

forallb and seq are both in stdlib List.v

view this post on Zulip Julin S (Jun 18 2022 at 18:10):

Thanks! I think forallb, existsb and seq can help. But still couldn't finish it.

I tried making the functions with them.

For simplicity, I am considering the case where the return value of the main function (fn) is None. Some value is returned via an else clause.

(That means p0, p1 aren't needed).

Definition p2 (bval cval:option nat) : bool :=
  andb (isNoneT bval) (isNoneT cval).

Definition p3 (x1 x2:nat) (b:nat->option nat) : bool :=
  forallb (fun x:nat => isSomeT (b x))
          (seq x1 (x2-x1)).

Section sec_sn.
  Variable a b c : nat -> option nat.
  Definition Sn (x:nat) : bool :=
    forallb
      (fun x':nat =>
        (eqSome (a x') (Some (x-x'))) &&
        (p2 (b x') (c x')) && (p3 x' x b)
      )%bool
      (seq 0 (x-1)).
End sec_sn.

Using this, I tried defining the main function:

Fixpoint fn (a b:nat->option nat) : nat -> option nat :=
  fun x:nat =>
  let snval:bool := (Sn a b (fn a b) x) in
  if snval then None
  else (Some 1).

But ran into problem in making the recursion happen on a smaller argument (primitive recursion).

Cannot guess decreasing argument of fix.

How can I get around that?

Or could this be expressed differently?

view this post on Zulip Julin S (Jun 18 2022 at 18:11):

fn is supposed to return option nat.

view this post on Zulip Julin S (Jun 18 2022 at 18:23):

Helper functions used:

Definition eqSome (a b:option nat):bool :=
  match a, b with
  | Some a', Some b' => Nat.eqb a' b'
  | _, _ => false
  end.

Definition isNoneT {A:Type} (x:option A) : bool :=
  match x with
  | None => true
  | Some _ => false
  end.
Definition isSomeT {A:Type} (x:option A) : bool := negb (isNoneT x).

view this post on Zulip Julin S (Jun 18 2022 at 18:24):


And p0 and p1 (not used):

Definition p0 (x:nat) (b c:nat->option nat) : bool :=
  andb (isSomeT (b x)) (isSomeT (c x)).

Definition p1 (x1 x2:nat) (b:nat->option nat) : bool :
  forallb (fun x:nat => isNoneT (b x))
          (seq x1 (x2-x1)).

view this post on Zulip Paolo Giarrusso (Jun 18 2022 at 23:28):

well-founded recursion might be helpful as a last resort, but you should probably make sure that fn is correct first... the recursion you've written is pretty strange (and probably exponential). If the scheme is intended, you might be able to first generate the call tree as an inductive tree (by structural recursion on n), then proceed by structural recursion on the generated tree

view this post on Zulip Paolo Giarrusso (Jun 18 2022 at 23:29):

(but you did warn us this was strange)

view this post on Zulip Julin S (Jun 20 2022 at 04:29):

You mean by making a new inductive type?

view this post on Zulip Julin S (Jun 20 2022 at 05:16):

Can CoInductive types be of any help?

view this post on Zulip Paolo Giarrusso (Jun 20 2022 at 10:34):

Coinductives help represent infinitely deep trees, which shouldn't be necessary?


Last updated: Jan 29 2023 at 06:02 UTC