## Stream: Coq users

### Topic: Choose value based on propositions

#### Julin S (Jun 16 2022 at 06:11):

This might seem like an weird exercise.

I got a set of functions:

• f : nat -> nat -> nat -> nat
• p0: nat -> nat -> nat -> Prop
• p1: nat -> nat -> nat -> Prop
• p2: nat -> nat -> nat -> Prop

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.

• If the first propostion is provable, return `0`
• If the second propostion is provable, return `1`
• If the third propostion is provable, return `2`
• If none of the 3 propostions are provable, return `3`

Is there a way to do this?

Is using `sigT` a possible way?

The type of the functions can't be changed.

#### 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.
``````

#### 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.

#### 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.

#### Julien Puydt (Jun 16 2022 at 06:23):

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

#### Julin S (Jun 16 2022 at 06:27):

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

#### Julin S (Jun 16 2022 at 06:30):

Give me a few minutes.

#### 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.

#### Julin S (Jun 16 2022 at 06:43):

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

#### 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?

#### 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.

#### Julien Puydt (Jun 16 2022 at 06:50):

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

#### Julin S (Jun 16 2022 at 06:55):

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

#### 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?

#### 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.
``````

#### 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), that is

``````Definition is_true : bool -> Prop := fun b => b = true.
Coercion is_true : bool >-> Sortclass.
``````

#### 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`...

#### Julin S (Jun 16 2022 at 08:52):

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

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

#### 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`).

#### 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'.
``````

#### 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
``````

#### Julin S (Jun 16 2022 at 09:48):

Can a complete standalone `getSome_prf` function be made like this?

#### Gaëtan Gilbert (Jun 16 2022 at 09:48):

what does that mean?

#### 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.

#### 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

#### 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).
``````

#### Julin S (Jun 16 2022 at 09:49):

Should it return `bool`?

#### Gaëtan Gilbert (Jun 16 2022 at 09:51):

`match prf I with end` should work then

#### 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.
``````

#### 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.

#### 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

#### Kenji Maillard (Jun 16 2022 at 10:03):

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

#### Kenji Maillard (Jun 16 2022 at 10:03):

So the warning should be taken even more seriously :)

#### Julin S (Jun 16 2022 at 10:06):

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

#### 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`?

#### Gaëtan Gilbert (Jun 16 2022 at 10:11):

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

#### Julin S (Jun 16 2022 at 10:12):

Okay, so `prf I` ends being of type `False`.

#### 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.

#### Gaëtan Gilbert (Jun 16 2022 at 10:15):

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

#### Julin S (Jun 16 2022 at 10:17):

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

#### Gaëtan Gilbert (Jun 16 2022 at 10:17):

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

#### 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.

#### Julin S (Jun 16 2022 at 12:42):

Could functions like`getSome_prf` be considered examples of 'proof carrying code'?

#### 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.

#### 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.

#### 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`.

#### Gaëtan Gilbert (Jun 16 2022 at 14:29):

do you mean isNone instead of = None?

thanks, fixed

#### Gaëtan Gilbert (Jun 16 2022 at 14:41):

forallb and seq are both in stdlib List.v

#### 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?

#### Julin S (Jun 18 2022 at 18:11):

`fn` is supposed to return `option nat`.

#### 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).
``````

#### 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)).
``````

#### 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

#### Paolo Giarrusso (Jun 18 2022 at 23:29):

(but you did warn us this was strange)

#### Julin S (Jun 20 2022 at 04:29):

You mean by making a new inductive type?

#### Julin S (Jun 20 2022 at 05:16):

Can CoInductive types be of any help?

#### Paolo Giarrusso (Jun 20 2022 at 10:34):

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

Last updated: Jun 24 2024 at 01:01 UTC