Hi.

What could be a value of the type `{n : nat | n < 5}`

?

I guess it's not as simple as saying:

```
Check (3 : {n:nat | n < 5}).
(*
The term "3" has type "nat" while it is expected to have type
"{n : nat | n < 5}".
*)
```

I was trying to understand subtypes with Coq.

here is one:

```
Definition three_lt_5 : {n : nat | n < 5} := exist _ 3 (le_S 4 4 (le_n 4)).
```

but I recommend building the thing with tactics for understanding:

```
Definition three_lt_5 : {n : nat | n < 5}.
Proof.
exists 3.
(* ... *)
Defined.
```

Or using `Program`

to explicitly separate the computationally relevant part from opaque proofs:

```
#[program]
Definition three_lt_5 : {n : nat | n < 5 } := exist _ 3 _.
Next Obligation. (* ... *) Qed.
```

Karl Palmskog said:

but I recommend building the thing with tactics for understanding:

`Definition three_lt_5 : {n : nat | n < 5}. Proof. exists 3. (* ... *) Defined.`

The one involving a proof (for understanding how it works) as simple as using lia tactic like:

```
Require Import Lia.
Definition three_lt_5 : {n : nat | n < 5}.
Proof.
exists 3.
lia.
Qed.
```

Kenji Maillard said:

Or using

`Program`

to explicitly separate the computationally relevant part from opaque proofs:`#[program] Definition three_lt_5 : {n : nat | n < 5 } := exist _ 3 _. Next Obligation. (* ... *) Qed.`

For the program-obligation version, it got over with just

```
Program Definition three_lt_5 : {n : nat | n < 5} := exist _ 3 _.
(*
three_lt_5 has type-checked, generating 1 obligation
Solving obligations automatically...
three_lt_5_obligation_1 is defined
No more obligations remaining
three_lt_5 is defined
*)
```

Is it because coq was smart enough to figure out the rest? That we didn't have to give further guidance with `Next Obligation`

?

And is `#[program]`

a new way instead of writing `Program Definition ....`

?

Julin S said:

And is

`#[program]`

a new way instead of writing`Program Definition ....`

?

Yes.

Julin S said:

Kenji Maillard said:

Or using

`Program`

to explicitly separate the computationally relevant part from opaque proofs:`#[program] Definition three_lt_5 : {n : nat | n < 5 } := exist _ 3 _. Next Obligation. (* ... *) Qed.`

For the program-obligation version, it got over with just

`Program Definition three_lt_5 : {n : nat | n < 5} := exist _ 3 _. (* three_lt_5 has type-checked, generating 1 obligation Solving obligations automatically... three_lt_5_obligation_1 is defined No more obligations remaining three_lt_5 is defined *)`

Is it because coq was smart enough to figure out the rest? That we didn't have to give further guidance with

`Next Obligation`

?

There is an obligation tactic trying to solve obligations automatically and it probably uses `lia`

on its own.

Théo Winterhalter said:

There is an obligation tactic trying to solve obligations automatically and it probably uses

`lia`

on its own.

Yeah. I guess this could be it?:

```
three_lt_5_po_obligation_1 = le_S 4 4 (le_n 4)
: 3 < 5
```

This is the proof it generated for you.

I tried out 'Program-obligation' way to prove a definition for list appending. Like

```
#[program]
Fixpoint append {A : Type} (l1 l2 : list A)
: {l : list A | length l = length l1 + length l2} :=
match l1, l2 with
| [], y => y
| (x::xs), y => x :: append xs y
end.
Next Obligation.
simpl.
rewrite e.
reflexivity.
Qed.
```

This gave error saying: `Cannot guess decreasing argument of fix`

.

So I tried adding a `struct`

like:

```
#[program]
Fixpoint append {A : Type} (l1 l2 : list A) {struct l1}
: {l : list A | length l = length l1 + length l2} :=
```

But now it gave another error saying:

```
Recursive definition of append is ill-formed.
In environment
append :
forall (A : Type) (l1 l2 : list A),
{l : list A | length l = length l1 + length l2}
A : Type
l1 : list A
l2 : list A
x : A
xs : list A
Heq_l1 : x :: xs = l1
Heq_l2 : l2 = l2
Recursive call to append has not enough arguments.
Recursive definition is:
"fun (A : Type) (l1 l2 : list A) =>
let program_branch_0 :=
fun (y : list A) (Heq_l1 : [] = l1) (Heq_l2 : y = l2) =>
exist (fun l : list A => length l = length l1 + length l2) y
(append_obligation_1 A l1 l2 y Heq_l1 Heq_l2) in
let program_branch_1 :=
fun (x : A) (xs y : list A) (Heq_l1 : x :: xs = l1) (Heq_l2 : y = l2) =>
exist (fun l : list A => length l = length l1 + length l2)
(x :: proj1_sig (append A xs y))
(append_obligation_2 append A l1 l2 x xs y Heq_l1 Heq_l2) in
match
l1 as l2'
return
(l2' = l1 -> l2 = l2 -> {l : list A | length l = length l1 + length l2})
with
| [] => program_branch_0 l2
| x :: xs => program_branch_1 x xs l2
end eq_refl eq_refl".
```

I couldn't make sense of this error except that I did something wrong..:grimacing:

How can this be fixed?

(Should I make another topic for this?)

It said `append`

doesn't have enough parameters. But it takes only 2 arguments and `append xs y`

has 2 args.

in `append_obligation_2 append A l1 l2 x xs y Heq_l1 Heq_l2`

`append`

is not applied

In this specific case, a feature of `program`

is shooting in your foot, the fact that it enriches pattern matches with "logical" refinements.

If you disable this feature (actually often a better default) using `Unset Program Cases.`

your program wont be instrumented the same way and can be defined without troubles.

Hm.. actually that only worked in my buffer because `Program`

discharged the obligation automatically and kept them transparent. If I explicitly prove the obligations, ending them with `Qed`

will of course fail.

Here's a hackish solution, if anyone actually care

```
From Coq Require Import List.
Import ListNotations.
Obligation Tactic := idtac.
Unset Program Cases.
#[program]
Fixpoint append {A : Type} (l1 l2 : list A)
{struct l1} : {l : list A | length l = length l1 + length l2} :=
match l1, l2 with
| [], y => exist _ y _
| (x::xs), y => (fun z => exist _ (x :: proj1_sig z) _) (append xs y)
end.
Next Obligation. reflexivity. Qed.
Next Obligation.
intros A _ k2 x xs ? z; cbn.
rewrite (proj2_sig z).
reflexivity.
Qed.
```

Gaëtan Gilbert said:

in

`append_obligation_2 append A l1 l2 x xs y Heq_l1 Heq_l2`

`append`

is not applied

How can we fix that?

(I couldn't figure out how we could figure out append wasn't even applied there..)

`append`

is just passed as an argument to `append_obligation_2`

, so it is not applied to anything at that point, and could be applied to something arbitrary inside `append_obligation_2`

. Since that obligation is opaque (ended with `Qed`

), the guard checker (that ensures termination) cannot inspect `append_obligation_2`

to see whether `append`

is correctly applied or not.

My hack above adds a beta redex so that `program`

does not have to capture `append`

when creating the obligation.

Here are a few lines which I find instructive:

```
Require Import Lia.
Fail Definition three_lt_5a : {n : nat | n < 5} :=
exist (fun n => n<5) 3 ltac:(match goal with |- ?a => idtac "GOAL=" a end; lia).
(*
GOAL= ((fun n : nat => lt n 5) 3)
The command has indeed failed with message:
Tactic failure: Cannot find witness.
*)
Definition three_lt_5b : {n : nat | n < 5} :=
exist (fun n => n<5) 3 ltac:(cbv beta; match goal with |- ?a => idtac "GOAL=" a end; lia).
(* GOAL= (lt 3 5) *)
Fail Definition three_lt_5c : {n : nat | n < 5} :=
exist _ _ ltac:(cbv beta; match goal with |- ?a => idtac "GOAL=" a end; lia).
(*
GOAL= (?P ?x)
The command has indeed failed with message:
Tactic failure: Cannot find witness.
*)
Program Definition three_lt_5d : {n : nat | n < 5} :=
exist _ 3 ltac:(cbv beta; match goal with |- ?a => idtac "GOAL=" a end; lia).
(* GOAL= (lt 3 5) *)
```

This shows two things:

- The type checker of
`Program Definition`

is bidirectional, while the type checker of`Definition`

is not. For this reason one has to give an explicit first argument`(fun n => n<5)`

with`Definition`

, but not with`Program Definition`

- The proof goal for the 3rd argument of
`exists`

needs beta conversion before`lia`

can understand it.

IIRC the type checker of `Program`

is bidirectional on parameters of inductive types by default, like the predicate here. With `bidirectional hints`

one can obtain the same behavior (without necessarily using Program), see https://coq.inria.fr/refman/language/extensions/arguments-command.html?highlight=bidirectional%20hints#bidirectionality-hints

@Enrico Tassi : cool, thanks for the hint - I didn't notice this change!

So this does also work:

```
Require Import Lia.
Arguments exist _ _ & _ _.
Definition three_lt_5c : {n : nat | n < 5} := exist _ 3 ltac:(cbv beta; lia).
```

P.S.: the downside of this solution might be that the proof is not abstracted into a separate opaque lemma - as with `Program Definition`

. This might have bad effects on performance in some cases. Using `abstract`

in `ltac:()`

does not work (it creates a local function rather than a global opaque definition).

Last updated: Jan 28 2023 at 08:02 UTC