CODEWITHSUNDEEP
coqcoq-tacticinduction
Kamyar Mirzavaziri
Kamyar Mirzavaziri

Reputation: 858

Definition by minimization in Coq

Assume P: nat -> T -> Prop is a proposition that for any given t: T,

I want to define min_k : T -> nat + undef to be the minimum number k such that P k t holds, and undef otherwise.

Is that even possible? I tried to define something like

Definition halts (t : T) := exists k : nat, P k t.

Or maybe

Definition halts (t : T) := exists! k : nat, (~ P k t /\ P (S k) t).

and then use it like

Definition min_k (t : T) := match halts T with
  | True => ??
  | False => undef
end.

but I don't know how to go further from there.

Any ideas would be appreciated.

Upvotes: 1

Views: 80

Answers (2)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23622

In addition to Ana's excellent answer, I think it is worth pointing out that option nat is essentially the same thing as {k : nat | ...} + {forall k, ~ P k t} if you erase the proofs of the latter type: in the first case (Some or inleft), you get a natural number out; in the second (None or inright) you get nothing at all.

Upvotes: 1

Ana Borges
Ana Borges

Reputation: 1376

You can't match on a Prop. If you want to do case analysis then you need something in Type, typically bool or something like sumbool or sumor. In other words, you can do what you want as long as you have a pretty strong hypothesis.

Variable T : Type.
Variable P : nat -> T -> Prop.

Hypothesis PProperty : forall (t : T),
  {k : nat | forall n, (k <= n -> P n t) /\ (n < k -> ~ P n t)}
  +
  {forall k, ~ P k t}.

Definition min_k (t : T) : option nat :=
  match PProperty t with
  | inleft kH => Some (proj1_sig kH)
  | inright _ => None
  end.

Crucially, this wouldn't have worked if PProperty was a Prop disjunction, i.e., if it was of the form _ \/ _ instead of the form _ + { _ }.

By the way, the idiomatic way of describing foo + undef in Coq is to use option foo, which is what I did above, but you can adapt it as you wish.

Upvotes: 2

Related Questions