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.

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

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.

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.

Can't your `p0`

, `p1`

and `p2`

have boolean values?

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

Give me a few minutes.

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.

Throughout, `a`

and `b`

are arguments of `f`

. Likewise `c`

is the return value of `f`

.

Your previous question had `f`

compute something with the results of `p*`

, but here it's the reverse, isn't it?

The situation here seems much better: I see many `x' < x`

which mean a **bounded** check, hence something that is a boolean.

The declaration `b: nat -> nat`

and the usage `(b x) <> None`

don't seem coherent.

Sorry, all the `(nat -> nat)`

should've been `(nat -> option nat)`

. Correcting.

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?

you can have

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

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)

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

...

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

.

Julien Puydt said:

The situation here seems much better: I see many

`x' < x`

which mean aboundedcheck, 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)) *)
```

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`

).

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

something like

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

Can a complete standalone `getSome_prf`

function be made like this?

what does that mean?

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.

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

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

Should it return `bool`

?

`match prf I with end`

should work then

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

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.

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

oups, Indeed you need to define `isSome`

primitively (in a way similar to `isNone`

)

So the warning should be taken even more seriously :)

This problem won't be there if `isSome`

returned `bool`

, right?

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`

?

`prf`

has type `isSome None`

which reduces to `not True`

ie `True -> False`

Okay, so `prf I`

ends being of type `False`

.

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.

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

So the proof for `None`

part would be `false = true`

.

yes

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

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.

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

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

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

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`

.

do you mean isNone instead of = None?

thanks, fixed

forallb and seq are both in stdlib List.v

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?

`fn`

is supposed to return `option nat`

.

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

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

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

(but you did warn us this was strange)

You mean by making a new inductive type?

Can CoInductive types be of any help?

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

Last updated: Jan 29 2023 at 06:02 UTC