Strong Specifications in Coq - wjzz/NotesAndCheatsheets GitHub Wiki

Contents

Basic info about programming with strong specifications (aka subset types) in Coq. Mainly based on http://adam.chlipala.net/cpdt/html/Subset.html

Starter

Print sig.
Print sumbool.
Print sumor.

Basic types and notations

{ A : nat | P A }

Notation "!" := (False_rec _ _).
Notation "[ e ]" := (exist _ e _).

Weak vs. strong

Variable P : (nat * nat) -> Prop.

(** From strong to weak spec **)

Variable foo : forall n, { m : nat | P (m, n) }.

(* Extract the computational content: *)

Definition foo_comp (n : nat) : nat :=
  match foo n with
    | exist x _ => x
  end.

(* Extract the logical content: *)

Theorem foo_prop :
  forall n,
    P (foo_comp n, n).
Proof.
  intro n; unfold foo_comp; destruct (foo n); auto.
Qed.

(** The other direction: from weak to strong spec **)

Variable bar : nat -> nat.
Hypothesis bar_prop : 
  forall n, P (bar n, n).

Definition bar_strong : forall n, { m : nat | P (m, n) }.
  refine (fun n => @exist _ _ (bar n) _); auto.
Defined. 

Print bar_strong.

(* The same but using a notation for readability *) 

Notation "[ e ]" := (exist _ e _).

Definition bar_strong' : forall n, { m : nat | P (m, n) }.
  refine (fun n => [ bar n ]); auto.
Defined. 

(* The same but using the Program feature *)

Obligation Tactic := auto.

Program Definition bar_strong'' : forall n, { m : nat | P (m, n) } :=
  fun n => bar n.