(*B 
{section 3|Prelude}

We start with this classical command, everything else
we need for now is already in Coq's pre-loaded module of the standard
library
(the {link http://coq.inria.fr/stdlib/Coq.Init.Prelude.html
|Prelude} module). B*)
Set Implicit Arguments.

(*B 

The type {t|sig}{note|The name comes from {q|Sigma};
{link http://en.wikipedia.org/wiki/Intuitionistic_type_theory#.CE.A3-types
|Σ-Types}.}
is defined in the
{link http://coq.inria.fr/stdlib/Coq.Init.Specif.html
|Specif} module  together with the associated notations:
[coq[
Inductive sig (A : Type) (P : A -> Prop) : Type :=
    exist : forall x : A, P x -> sig P
    
Notation "{ x | P }" := (sig (fun x => P)) : type_scope.
Notation "{ x : A | P }" :=
    (sig (fun x:A => P)) : type_scope.
]coq]
For instance, {t|{text}{x : nat | x > 42}{end}} is the type of the
naturals strictly bigger than {i|42}.
{p}

We also need {t|False_rec} (defined while defining the {t|False}
#proposition:
#{t|Inductive False : Prop :=.}
in the
{link http://coq.inria.fr/stdlib/Coq.Init.Logic.html |Logic} module).
It will be useful to be able to put {q|something}
for the cases which {i|never} happen 
(i.e. an {q|{t|assert false}} in OCaml).
{p}

This deserves a few more notations:
 B*)
Notation "'Sig_no'"  := (False_rec _ _) (at level 42).
Notation "'Sig_yes' e" := (exist _ e _) (at level 42).
Notation "'Sig_take' e" := 
  (match e with Sig_yes ex => ex end) (at level 42). 

(*B {section 3|Examples} 

{section 4|The Trivial One}

Let's start with the simplest example I could find.
A function returning the successor of a natural number, and telling so in
its type:
B*)
Definition succ_strong: forall (n : nat), {m : nat | m = S n}.
  refine (fun n => Sig_yes (S n)). trivial.
Defined.
(*B
It uses the
{link http://coq.inria.fr/refman/Reference-Manual011.html#@tactic5 |refine}
tactic
{note|see also
this
{link http://coq.inria.fr/refman/Reference-Manual013.html#@tactic186 |example}}
which
{quote|{i|allows to give an exact proof, [{...}] like {t|exact},
with a big difference: the user can leave
some holes (denoted by {t|_} or {t|(_:type)}) in the term. {t|refine} will
generate as many subgoals as they are holes in the term.}}
The {i|hack} is to use {t|refine} to provide the {i|body} of the
function definition
while in proof mode; and hence be able to provide the
proof(s) of the specification part later.

In our case, there is only one generated subgoal (by the second
{q|{t|_}} in the {t|Sig_yes} notation) and it is (solved by)
{i|trivial}. {p}

Without the {t|refine} tactic we would have to provide
the {t|(P x)} argument
of the {t|exist} constructor {q|by hand}: B*)
Definition succ_strong_by_hand: 
  forall (n : nat), {m : nat | m = S n} :=
    fun n => 
      exist (* The P : A -> Prop  *) _ 
            (* The x : A   *) (S n)
            (* The P x *) (eq_refl (S n)).
(*B The first underscore is inferred by Coq (not through {t|refine}): B*)
Definition succ_strong_no_inference_at_all: 
  forall (n : nat), {m : nat | m = S n} :=
    fun n => 
      exist (* The P : A -> Prop  *) (fun t => eq t (S n)) 
            (* The x : A   *) (S n)
            (* The P x *) (eq_refl (S n)).
(*B
Anyway, this would not scale to more complex types
(it took me already quite some time to come up with the right {t|eq}
and {t|eq_refl}).
With {t|refine} instead, we let
{i|underscores} for the {q|proofs} and we provide them later
with usual Coq tactics.
{p}

Do not forget the {t|Defined} instead of {t|Qed}, so that Coq keeps
the {i|proof} of the definition (with {t|Qed}, 
{link http://coq.inria.fr/refman/Reference-Manual003.html#@command26
|it would become} {q|Opaque}). {p}

We can already check the generated OCaml code:
B*)
Extraction succ_strong.
(*B [caml[
(** val succ_strong : nat -> nat **)
let succ_strong n =
  S n
]caml]
{p}
 B*)

(*B 

{section 4|A Non-Total Function}

Let's see another example:
{t|pred_strong} which can be called only for {t|n > 0}.
 B*)
Definition pred_strong :
    forall n : nat, n > 0 -> {m : nat | n = S m}.
  refine (fun n =>
    match n with
      | O => fun _ => Sig_no
      | S pn => fun _ => Sig_yes pn
    end).
  (*B
    # The function has two arguments, {t|n} and a proof that {t|n > 0}.
    This time two goals remain to fill{~}{...} B*)
  (* n : nat    _H : 0 > 0  |-   False *)
  inversion _H.
  (*  n : nat   pn : nat    _H : S pn > 0 |-    S pn = S pn *)
  reflexivity. 
  (* Proof Completed. *)
  (*B
     {t|pred_strong} would be now perfectly usable, but
     we are not yet completely 
     happy because the proof is not {q|well engineered}:
     it references internal-state stuff like {q|{t|_H}}, and it
     depends on the order of the
     subgoals{note|CPDT has plenty of very interesting discussions and 
     justifications about the subject, e.g. in the
     {q|{link http://adam.chlipala.net/cpdt/html/Intro.html |Intro}} or the
     {q|{link http://adam.chlipala.net/cpdt/html/Large.html |Large}} chapters.}.
     B*)
  Restart.
  (*B We can  put everything together in one {q|chain of tactics}
  without having references to local variables. We use the
  {t|{link http://coq.inria.fr/refman/Reference-Manual012.html#@tactic181 |solve}}
  tactic which simply tries to {i|solve} the goal with one of the branches
  given as arguments.
  We match the goal looking for hypotheses looking like the previous
  {t|_H} to invert them, for the other goal, we call {t|auto}.
  B*)
  refine (fun n =>
    match n with
      | O => fun _ => Sig_no
      | S pn => fun _ => Sig_yes pn
    end);
  solve 
  [ match goal with H: 0 > 0 |- _ =>  inversion H end
    | auto ].
  (* Proof Completed. *)
  (*B That's nicer.
  For posterity, we can also define the two following pieces of {t|Ltac}
  which are reusable and {i|mostly} clean.
  B*)
  Restart.
  (*B 
     {t|solve_by_inversion} will try to solve the goal by inverting
     all the hypotheses{note|There is a more complete/searching one {link
     http://coq.inria.fr/cocorico/solve%20by%20inversion%20%28tactic%29
     |on Cocorico}, the Coq wiki.}.
  B*)
  Ltac solve_by_inversion :=
    match goal with
      | H:_ |- _ =>
        solve [  inversion H | clear H; solve_by_inversion
          | fail 2 "Could not solve by inversion" ]
    end.
  (*B {t|invert_or_auto} tries the previous one, and if it fails then
  {t|auto}. B*)
  Ltac invert_or_auto := 
    try solve_by_inversion;
      solve [ auto 
        | fail 2 "Could not solve by inversion nor auto" ].
  (*B With them, we can solve this even more elegantly: B*)
  refine (fun n =>
    match n with
      | O => fun _ => Sig_no
      | S pn => fun _ => Sig_yes pn
    end); invert_or_auto.
  (* Proof Completed. *)
Defined.

(*B {ignore} B*)
(*
   Test the tactics
   Lemma ttt: forall (n : nat), False.  invert_or_auto. *)
(*B {end} B*)

(*B {p}

Now the funny part:
the function {t|pred_strong} takes as input
an implicit natural number {i|n} and a {q|proof that {i|n > 0}}: B*)
Theorem two_gt_0 : 2 > 0.
  auto.
Qed.
Eval compute in pred_strong two_gt_0.
(*B {code}
= Sig_yes 1
: {m : nat | 2 = S m}
{end} B*)

(*B Anyway, in OCaml, it still looks pretty {i|normal}: B*)
Extraction pred_strong.
(*B [caml[
(** val pred_strong : nat -> nat **)

let pred_strong = function
| O -> assert false (* absurd case *)
| S pn -> pn ]caml] B*)

(*B 
The eager reader can continue with CPDT's
{link http://adam.chlipala.net/cpdt/html/Subset.html
|Subset} chapter to see more implementations of {q|{t|pred}} with
other rich dependent types.
B*)

(*B {section 4|A {t|List.map}}

Here is an implementation of {t|List.map} with a {t|sig} return type
specifying what the result actually {i|is}.

B*)
Section List_map.
(*B We use Coq's basic lists B*)
  Require Import List.
  
  (*B and we describe what the map function should do with an
     inductive proposition. {t|map_spec} links
     the input list, the input function and the resulting function.
     B*)
  Inductive map_spec (A B: Set):
    (A -> B) -> (list A) -> (list B) -> Prop :=
  | ms_empty: forall f, map_spec  f nil nil
  | ms_step: forall f a la b lb,
    (b = f a) -> map_spec f la lb ->
    map_spec f (a :: la) (b :: lb).

  (*B  {p}
     Here is the signature of the {t|specified_map}: B*)
  Definition specified_map (A B: Set): 
    forall (f: A -> B) (l: list A),
      { lm : list B | map_spec f l lm }.
  (*B 
     Simply because it is fun, we use the
     {t|{link http://coq.inria.fr/refman/Reference-Manual011.html#@command230
     |Proof with}} command which gives a meaning to the {q|{t|...}} notation.
     We feed {t|auto} with the constructors of {t|map_spec} (this
     could have been done also with a
      {link http://coq.inria.fr/refman/Reference-Manual011.html#@command218 |Hint}).
     B*)
  Proof with eauto using ms_empty, ms_step.
  (*B Without the notation {t|Sig_take}, we simply do pattern matching
     with one case: B*)
    refine (fix fx (f: A -> B) (l: list A):
      { lm : list B | map_spec f l lm } :=
      match l with
        | nil => Sig_yes nil
        | cons h t =>
          match fx f t with
            | Sig_yes ll => Sig_yes (f h :: ll)  
          end
      end)...
    (* Proof Completed. *)

    (*B and that's {i|done}.
       But If we want to play with the notation, we
       introduce a tiny problem: B*)
    Restart.
    refine (fix fx (f: A -> B) (l: list A):
      { lm : list B | map_spec f l lm } :=
      match l with
        | nil => Sig_yes nil
        | cons h t => Sig_yes (f h :: (Sig_take fx f t))
      end)... 
    (*B There we are stuck with a {t|(let (ex, _) := fx f t in ex)}
       in the middle of the goal 
       which {t|auto} does not want to expand any more{~}{...} B*)
    Restart.
    
    (*B We can ask Coq to force it: B*)
    refine (fix fx (f: A -> B) (l: list A):
      { lm : list B | map_spec f l lm } :=
      match l with
        | nil => Sig_yes nil
        | cons h t => Sig_yes (f h :: (Sig_take fx f t))
      end);
    try (destruct (fx f t))...
    (*B And get the {q|{t|Proof Completed}} 
       but we can still try to make something cleaner. B*) 
    Restart.
    (*B
       After a bit of 
       {link
http://thread.gmane.org/gmane.science.mathematics.logic.coq.club/1115/focus=1119
       |googling}-trial-and-error, we get a tactic to force the {t|destruct}
       on our notation.
       B*)
    Ltac with_sig_take :=
      repeat
        match goal with
          | [ |- context[ match ?E with Sig_yes x => _ end ] ] =>
            idtac "Destructing" E; destruct E
        end.
    refine (fix fx (f: A -> B) (l: list A):
      { lm : list B | map_spec f l lm } :=
      match l with
        | nil => Sig_yes nil
        | cons h t => Sig_yes (f h :: (Sig_take fx f t))
      end);
      with_sig_take...
    (* Proof Completed. *)  
  Defined.

End List_map.

(*B
{p}
Let's do some tests{~}{...} B*)
Eval compute in
  (specified_map (fun x => x + 42) (0 :: 1 :: 2 :: 4 :: nil)).
(*B {code}
= Sig_yes (42 :: 43 :: 44 :: 46 :: nil)
: {lm : list nat |
 map_spec (fun x : nat => x + 42) (0 :: 1 :: 2 :: 4 :: nil) lm}
{end}
{p}

We can also call {t|pred_strong} on a list of {i|wrapped} positive
naturals: B*)
Inductive strictly_positive : Set :=
| gt_0: forall n : nat, (n > 0) -> strictly_positive.

Lemma one_gt_0: 1 > 0. auto. Qed.
Lemma three_gt_0: 3 > 0. auto. Qed.

Eval compute in 
  (specified_map 
    (fun t => 
      match t with
        | gt_0 x x_gt_0 => Sig_take pred_strong x_gt_0
      end)
    ((gt_0 one_gt_0) :: (gt_0 two_gt_0) :: 
      (gt_0 three_gt_0) :: nil)).
(*B {code}
= Sig_yes (0 :: 1 :: 2 :: nil)
: {lm : list nat |
  map_spec
    (fun t : strictly_positive =>
     match t with
     | gt_0 x x_gt_0 => let (ex, _) := pred_strong x_gt_0 in ex
     end) (gt_0 one_gt_0 :: gt_0 two_gt_0 :: gt_0 three_gt_0 :: nil) lm}
{end} B*)

(*B {p}
Finally, let's have a look at the OCaml code: B*)
Recursive Extraction specified_map.
(*B [caml[
type 'a list =
| Nil
| Cons of 'a * 'a list

type 'a sig0 =
  'a
  (* singleton inductive, whose constructor was exist *)

(** val specified_map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)

let rec specified_map f = function
| Nil -> Nil
| Cons (h, t) -> Cons ((f h), (specified_map f t))
]caml] B*)