Stream: Coq users

Topic: Value of a subtype


view this post on Zulip 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.

view this post on Zulip 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)).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Julin S (Mar 12 2022 at 09:53):

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

view this post on Zulip Théo Winterhalter (Mar 12 2022 at 09:56):

Julin S said:

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

Yes.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Winterhalter (Mar 12 2022 at 10:01):

This is the proof it generated for you.

view this post on Zulip 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?)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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..)

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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: Jan 28 2023 at 08:02 UTC