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: Jun 20 2024 at 13:02 UTC