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 writingProgram 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:
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
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: Oct 13 2024 at 01:02 UTC