CODEWITHSUNDEEP
coqcoq-tactic
Siddharth Bhat
Siddharth Bhat

Reputation: 843

deriving facts on pattern matching in coq

Consider the following program

Definition useGt0 (n: nat) (witness: n > 0) : nat :=
  10.


Definition createGt0(n: nat) : nat :=
  match n with
  | O => 42
  | S(n') => useGt0 n  (#???)
  end.

Clearly, n > 0 is inhabited, because n = S n'. However, how do I get access to the proof that n = S n'? From n = S n', we can derive that n > 0.

In general, I wish to understand: How do I extract information from a pattern match?

Upvotes: 1

Views: 99

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15424

The standard way to define createGt0 function is to use the convoy pattern (you can find several explanations using [coq] [convoy-pattern] search query on Stackoverflow). The standard link is A. Chlipala's CPDT book.

Here is a solution:

Definition createGt0 (n : nat) : nat :=
  match n as x return (n = x -> nat) with
  | O => fun _ => 42
  | S n' => fun E => useGt0 n (eq_ind_r (fun n => n > 0) (gt_Sn_O n') E)
  end eq_refl.

Another option is to use Program mechanism, which lets you program in non-dependently-typed style, deferring proof obligations until a later time:

Require Import Program.

Program Definition createGt0 (n : nat) : nat :=
  match n with
  | O => 42
  | S n' => useGt0 n _
  end.
Next Obligation. apply gt_Sn_O. Qed.

At last, you could use tactics to build your function:

Definition createGt0 (n : nat) : nat.
Proof.
  destruct n eqn:E.
  - exact 42.
  - refine (useGt0 n _).
    rewrite E.
    apply gt_Sn_O.
Defined.

If you end your function with Qed, Coq will consider it opaque and won't reduce. Try ending the function with both Qed and Defined and execute the following command:

Compute createGt0 0.

Upvotes: 2

Related Questions