Hi, I wonder if Coq's Program
tactic supports nested subset types. For example, I have the following:
Variable Foo : Type -> Type.
Variable WF : forall {A}, Foo A -> Prop.
Variable bar : forall {A}, Foo A -> Foo (Foo A).
Definition WFFoo A := { x : Foo A | WF x }.
Program Definition wf_bar {A} (x : WFFoo A) : WFFoo (WFFoo A) := bar x.
Coq rejects this definition but it would have problem if the return type is changed to WFFoo (Foo A)
. Is this intentional? Is there some sort of support for this type of functions? Or maybe this cannot be easily supported?
Hi @Yao Li , Program
can deal with nested subset types up to some elaboration troubles
Require Import Coq.Program.Tactics.
Definition non_empty {A} (l : list A) : Prop :=
match l with | nil => False | _ => True end.
Definition nelist (A : Type) := { l : list A | non_empty l }.
Program Definition nested_nelists : nelist (nelist nat) :=
let l : nelist nat := cons 5 nil in
(* beware that inlining l without a type annontation does not work well with Program's elaboration*)
cons l nil.
However the example that you gave does not hold in general. Consider the following instantiation for your variables:
Definition Foo : Type -> Type := fun _ => bool.
Definition WF : forall {A}, Foo A -> Prop := fun _ b => b = true.
Definition bar : forall {A}, Foo A -> Foo (Foo A) := fun _ _ => false.
Definition WFFoo A := { x : Foo A | WF x }.
Require Import Coq.Program.Tactics.
Program Definition not_wf_bar {A} (x : WFFoo A) : ~ WF (@bar A x) := _.
Thank you @Kenji Maillard for your answer! That is very helpful.
I understand and that my example does not hold in general, but that's a minimization of another example, where I expect WF
would hold because the implementation of bar
has been careful to ensure WF
. I gather from your first example that I cannot just put bar
in my Program Definition
and wish Coq will give me all the proof obligations---it seems that I may need to unfold my bar
definition there (and remember to apply the tip you give in comment). Is that right?
Last updated: Oct 13 2024 at 01:02 UTC