Stream: Coq users

Topic: Nested subset type with program tactic

view this post on Zulip Yao Li (Jun 10 2020 at 03:21):

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?

view this post on Zulip Kenji Maillard (Jun 10 2020 at 06:25):

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) := _.

view this post on Zulip Yao Li (Jun 10 2020 at 15:30):

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