Julin S (Mar 12 2022 at 09:20): 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)).
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
Programto 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 writingProgram Definition ....?
Yes.
Théo Winterhalter (Mar 12 2022 at 09:57):Julin S said:
Kenji Maillard said:
Or using
Programto 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
liaon 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.
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.
Gaëtan Gilbert said:
in
append_obligation_2 append A l1 l2 x xs y Heq_l1 Heq_l2appendis 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:
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 Definitionexists 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).
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