## Stream: Coq users

### Topic: Value of a subtype

#### Julin S (Mar 12 2022 at 09:20):

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.

#### Karl Palmskog (Mar 12 2022 at 09:27):

here is one:

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

#### Karl Palmskog (Mar 12 2022 at 09:29):

but I recommend building the thing with tactics for understanding:

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

#### Kenji Maillard (Mar 12 2022 at 09:45):

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

#### Julin S (Mar 12 2022 at 09:50):

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

#### Julin S (Mar 12 2022 at 09:53):

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

#### Julin S (Mar 12 2022 at 09:53):

And is `#[program]` a new way instead of writing `Program Definition ....`?

#### Théo Winterhalter (Mar 12 2022 at 09:56):

Julin S said:

And is `#[program]` a new way instead of writing `Program Definition ....`?

Yes.

#### Théo Winterhalter (Mar 12 2022 at 09:57):

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.

#### Julin S (Mar 12 2022 at 09:59):

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

#### Théo Winterhalter (Mar 12 2022 at 10:01):

This is the proof it generated for you.

#### Julin S (Mar 12 2022 at 10:07):

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

#### Julin S (Mar 12 2022 at 10:09):

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

#### Gaëtan Gilbert (Mar 12 2022 at 10:16):

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

#### Kenji Maillard (Mar 12 2022 at 10:18):

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.

#### Kenji Maillard (Mar 12 2022 at 10:24):

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.

#### Kenji Maillard (Mar 12 2022 at 10:29):

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

#### Julin S (Mar 12 2022 at 10:30):

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

#### Kenji Maillard (Mar 12 2022 at 18:20):

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

#### Michael Soegtrop (Mar 14 2022 at 09:29):

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.

#### Enrico Tassi (Mar 14 2022 at 09:55):

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

#### Michael Soegtrop (Mar 14 2022 at 11:29):

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

#### Michael Soegtrop (Mar 14 2022 at 11:37):

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: Jun 18 2024 at 23:01 UTC