Hello, I hope this is the right place to ask this question.

I'm working on a project where we are creating operations using subset types, i.e. `{ x : T | P x }`

and I have trouble proving properties of functions that return values but also need the proofs - I'm not sure how to describe this well so let me just paste a simple example:

```
Require Import BinInt.
Open Scope Z.
Definition Foo := { x : Z | x < 100 }.
Definition embed (x : Z) : option Foo.
destruct (Z.ltb x 100) as []eqn:Hg.
- apply Some.
eapply exist with x.
apply Z.ltb_lt in Hg.
assumption.
- apply None.
Defined.
Definition val (x : Foo) : Z := proj1_sig x.
```

We define a datatype Foo which is integers < 100 and I'm creating a function `embed`

which takes an integer, and if it is < 100, returns Foo (wrapped in Some) and otherwise returns None.

Now I want to prove that the embedding is 'full' that is, for every integer that fits, it returns a valid value:

```
Lemma embed_full : forall x,
x < 100 ->
exists r, embed x = Some r /\ val r = x.
```

And here is where I get stuck. How can I try proving this?

I have tried the following strategy - unfold the definition, use the assumption to decide the `<?`

inequality and rewrite it in the definition to be able to partially evaluate the embed function:

```
intros.
unfold embed.
assert (HR: x <? 100 = true).
- apply Z.ltb_lt. assumption.
- rewrite HR.
```

However on the last operation (rewrite), I get the following error:

```
Error: Abstracting over the term "x <? 100" leads to a term
fun b : bool =>
exists r : Foo,
(if b as b0 return (b = b0 -> option Foo)
then
fun Hg : b = true =>
Some
(exist (fun x0 : Z => x0 < 100) x
(match Z.ltb_lt x 100 with
| conj H0 _ => H0
end Hg))
else fun _ : b = false => None) eq_refl = Some r /\ val r = x
which is ill-typed.
Reason is: Incorrect elimination of "Z.ltb_lt x 100" in the inductive type "and":
ill-formed elimination predicate.
```

It seems to me that the issue is that I'm doing this `destruct`

with equations, which creates the `if`

which is abstracted over the equation.

However, I don't know how to define `embed`

in a different way, because that is precisely what it needs to be doing - it needs to check the `<?`

comparison and it needs the additional information about the result to deduce the proof for the `{ _ | x < 100 }`

property.

I'm not sure about your specific issue, but I would define embed differently, and then the problem becomes easy:

```
Require Import BinInt.
Open Scope Z.
Definition Foo := { x : Z | x < 100 }.
Axiom lt100_dec : forall x : Z, {x < 100} + {~ (x < 100)}.
Definition embed (x : Z) : option Foo :=
match lt100_dec x with
| left ltx100 => Some (exist _ x ltx100)
| right _ => None
end.
Definition val (x : Foo) : Z := proj1_sig x.
Lemma embed_full : forall x,
x < 100 ->
exists r, embed x = Some r /\ val r = x.
Proof.
intros x ltx100.
unfold embed.
destruct (lt100_dec x); [| contradiction].
exists (exist _ x l).
split; reflexivity.
Qed.
```

(There must be some lemma that subsumes `lt100_dec`

, I just couldn't find it in a couple of seconds.)

Ana de Almeida Borges said:

I'm not sure about your specific issue, but I would define embed differently, and then the problem becomes easy:

`Require Import BinInt. Open Scope Z. Definition Foo := { x : Z | x < 100 }. Axiom lt100_dec : forall x : Z, {x < 100} + {~ (x < 100)}. Definition embed (x : Z) : option Foo := match lt100_dec x with | left ltx100 => Some (exist _ x ltx100) | right _ => None end. Definition val (x : Foo) : Z := proj1_sig x. Lemma embed_full : forall x, x < 100 -> exists r, embed x = Some r /\ val r = x. Proof. intros x ltx100. unfold embed. destruct (lt100_dec x); [| contradiction]. exists (exist _ x l). split; reflexivity. Qed.`

(There must be some lemma that subsumes

`lt100_dec`

, I just couldn't find it in a couple of seconds.)

Awesome! That seems to be exactly what I needed.

A solution similar to the one above, using a reflection lemma from the library :

```
Require Import BinInt.
Open Scope Z.
Definition Foo := { x : Z | x < 100 }.
Definition embed (x : Z) : option Foo.
Proof.
destruct (Z.ltb_spec0 x 100).
- apply Some.
exists x.
assumption.
- exact None.
Defined.
Definition val (x : Foo) : Z := proj1_sig x.
Lemma embed_full : forall x,
x < 100 ->
exists r, embed x = Some r /\ val r = x.
Proof.
intros.
unfold embed.
destruct (Z.ltb_spec0 x 100).
- now exists (exist _ x l).
- now exfalso.
Qed.
```

In general if you need to use a proof during a definition you can match on `{thing holds} + {thing doesn't hold}`

(assuming it's decidable) and use the proofs stored in the `{_} + {_}`

datatype (called `sumbool`

)

The other possibility (and the one pushed especially by the MathComp library) is to use the `Bool.reflect`

inductive to achieve a goal somewhat similar to what one would obtain using `sumbool`

, ie. working with decidable predicates.

Thanks a lot for the answers!

I think I will try going with the sumbool type as it seems it should be quite easy to handle with extraction to OCaml later on (I assume as the proofs are erased, these functions will become isomorphic with functions returning booleans).

I assume as the proofs are erased, these functions will become isomorphic with functions returning booleans

Yup.

It's typical to include the following line before extraction to take advantage of this:

```
Extract Inductive sumbool => "bool" [ "true" "false" ].
```

i.e., `left`

is mapped to `true`

and `right`

to `false`

Now I’m wondering what `reflect`

is erased to!

Something isomorphic:

```
Require Import Bool Extraction.
Extraction reflect.
(*
type reflect =
| ReflectT
| ReflectF
*)
```

IMHO the solution of @Ana de Almeida Borges with a definition in plain gallina is preferable over the solution of @Meven Lennon-Bertrand . One should avoid to use tactics to create computational definitions, because they might be hard to work with and the exact term might even change with Coq versions, so that your proofs about it break. I would use tactics only, if the actual term is not interesting - as in the case of proofs. In my experience you spend 100x of what you save in time to write your definition with tactics later in proofs - what you witnessed is only the tip of the ice berg.

What I sometimes do if I can't figure it out is to use tactics to create a definition, then print the proof term and learn from it.

When you write functions which shall compute, it does make sense to try something like `Eval cbv in embed 20.`

. You will see that both solutions, the one from Ana and the one from Meven will lead to a term blow up with the size of the 100. If you do the same with `2^32`

instead of 100, the cbv will fail. Have a look at this:

```
Require Import ZArith.
Open Scope Z.
Definition Foo := { x : Z | x < 100 }.
Definition embed (x : Z) : option Foo :=
match Z_lt_le_dec x 100 with
| left ltx100 => Some (exist _ x ltx100)
| right _ => None
end.
Eval cbv in embed 20.
```

which results in

```
= Some
(exist
(fun x : Z =>
match x with
| 100 => Eq
| 0 | 95 | 63 | 79 | 47 | 31 | 87 | 55 | 71 | 39 |
23 | 15 | 91 | 59 | 75 | 43 | 27 | 83 | 51 | 99 |
67 | 35 | 19 | 11 | 7 | 93 | 61 | 77 | 45 | 29 |
85 | 53 | 69 | 37 | 21 | 13 | 89 | 57 | 73 | 41 |
25 | 81 | 49 | 97 | 65 | 33 | 17 | 9 | 5 | 3 |
94 | 62 | 78 | 46 | 30 | 86 | 54 | 70 | 38 | 22 |
14 | 90 | 58 | 74 | 42 | 26 | 82 | 50 | 98 | 66 |
34 | 18 | 10 | 6 | 92 | 60 | 76 | 44 | 28 | 84 |
52 | 68 | 36 | 20 | 12 | 88 | 56 | 72 | 40 | 24 |
80 | 48 | 96 | 64 | 32 | 16 | 8 | 4 | 2 | 1 | Z.neg _ => Lt
| _ => Gt
end = Lt) 20 eq_refl)
: option Foo
```

If you swap the relational operator, magically you get a term which does not increase with the upper limite:

```
Require Import ZArith.
Open Scope Z.
Definition Foo := { x : Z | 10000 > x}.
Definition embed (x : Z) : option Foo :=
match Z_gt_le_dec 10000 x with
| left P => Some (exist _ x P)
| right _ => None
end.
Eval cbv in embed 20.
```

gives

```
= Some
(exist
(fun y : Z =>
match y with
| Z.pos y' =>
(fix compare_cont (r : comparison) (x y0 : positive) {struct y0} :
comparison :=
match x with
| (p~1)%positive =>
match y0 with
| (q~1)%positive => compare_cont r p q
| (q~0)%positive => compare_cont Gt p q
| 1%positive => Gt
end
| (p~0)%positive =>
match y0 with
| (q~1)%positive => compare_cont Lt p q
| (q~0)%positive => compare_cont r p q
| 1%positive => Gt
end
| 1%positive => match y0 with
| 1%positive => r
| _ => Lt
end
end) Eq 10000%positive y'
| _ => Gt
end = Gt) 20 eq_refl)
: option Foo
```

The Z Prop relational operators are well known to be brittle in such situations, because they are computational. You must take care that constants are abstracted or not the one one which the definition recurses.

P.S.: the interesting point is that the computations even blows up with a ground term like `embed 20`

.

If you swap the relational operator, magically you get a term which does not increase with the upper limite:

Interesting! But why? Or rather, is there a way to find out without trying both?

Oh, is it because `compare`

is defined decreasing on the second argument?

Thanks for the detailed infos!

On a side-note though, I would say using tactics to construct terms as I do is not that harmful if you use tactics like `case`

, `exists`

, `assumption`

and the like that behave mostly like `refine`

with some term former (`exists`

or `split`

are inductive constructors, `assumption`

a variable, `case`

a match, `intros`

lambda-abstractions…). But I agree that in general tactics can be quite dangerous.

Ana de Almeida Borges said:

Oh, is it because

`compare`

is defined decreasing on the second argument?

yes, exactly. This kind of thing regularly happens if a term contains variables, but it gets problematic when it happens with ground terms like `embed 20`

, because this means one never can't compute anything if numbers get large. Also note, that vm_compute and cbv might lead to different results here, so one should verify that both work.

Meven Lennon-Bertrand said:

Thanks for the detailed infos!

On a side-note though, I would say using tactics to construct terms as I do is not that harmful if you use tactics like`case`

,`exists`

,`assumption`

and the like that behave mostly like`refine`

with some term former (`exists`

or`split`

are inductive constructors,`assumption`

a variable,`case`

a match,`intros`

lambda-abstractions…). But I agree that in general tactics can be quite dangerous.

this is true, but these are exactly those tactics which are not that hard to write in gallina right away. And one anyway has to think about the structure of the term when one starts to write proofs about it. So why not spend the extra effort when writing the definition rather than each time one writes a proof about it? Usually one writes more proofs than definitions, so shifting development time from definition time to proof time is rarely effective.

Last updated: Oct 05 2023 at 02:01 UTC