Stream: Coq users

Topic: Program Definiton use

Julin S (Mar 17 2023 at 07:21):

I was trying to use Program Definiton to leave some holes to be filled in later in this function:

Program Definition foo (num:{n:nat|n<2}):string:=
  match num with
  | exist _ 0 _ => "0"
  | exist _ 1 _ => "1"
  | _ => ""                           (* TODO *)
  end.

But coq complains saying:

Found a constructor of inductive type sig while a constructor of nat  is expected.

Why is this happening? I mean, num is of type sig.

Julin S (Mar 17 2023 at 07:29):

Does Program sort of unwrap the sig type?

Théo Winterhalter (Mar 17 2023 at 07:39):

I think Program has some facility for subset types (sig). So the following works:

Program Definition foo (num : { n : nat | n < 2 }) : string :=
  match num with
  | 0 => "0"
  | 1 => "1"
  | _ => ""                           (* TODO *)
  end.

Basically, it makes the subset type transparent.

Théo Winterhalter (Mar 17 2023 at 07:40):

This seems to be the subject of the first section of the Program chapter of the reference manual: https://coq.inria.fr/refman/addendum/program.html

Paolo Giarrusso (Mar 17 2023 at 08:28):

as an alternative, there is refine, even if that is far from a drop-in replacement (so I often stick to Program):

Definition foo (num:{n:nat|n<2}):string.
refine (
  match num with
  | exist _ 0 _ => "0"
  | exist _ 1 _ => "1"
  | _ => _
  end
).

Last updated: Oct 13 2024 at 01:02 UTC