(** * INITIATION TO COQ: dependent types and proofs *)

(** Additional material to coq01_init_theory1.v, developing the idea
    saying that
    - develop a typed functional program, and
    - build a proof
    are identical activities.
    (Curry-Howard correspondence).
    This is especially amazing when we consider *dependent types*
    and the computations of types.
    We also introduce Prop/Set and discuss subtle points
    related to conversion.
*)

(* ------------------------------------------------------------ *)
(** ** I. Our usual definitions *)

Inductive tlcolor : Set :=
  | Green  : tlcolor
  | Orange : tlcolor
  | Red    : tlcolor
.

Definition next_col : tlcolor -> tlcolor :=
  fun c =>
    match c with
    | Green  => Orange
    | Orange => Red
    | Red    => Green
    end.

(** Interactive definition *)
Definition next_col2 : tlcolor -> tlcolor.
Proof.
  intro c.
  destruct c as [ (*Green*) | (*Orange*) | (*Red*) ].
  Show Proof.
  -Show Proof.
    exact Orange.
  - exact Red.
  - exact Green.
Defined.

(** Using the tactic [refine]. *)
Definition next_col3 : tlcolor -> tlcolor.
Proof.
  refine (fun c =>
            match c with
            | Green => _
            | Orange => Red
            | Red => _
            end).
  - refine Orange.
  - refine Green.
Defined.

(* ------------------------------------------------------------ *)
(** ** II. A very common tactic:  [apply] *)

(** A meaningless function calling [next_col]. *)
Definition call_nc : tlcolor -> tlcolor :=
  fun c =>
    match c with
    | Green => Orange
    | Orange => next_col Red
    | Red => Green
    end.

(** In interactive mode, use the tactic [apply]. *)
Definition call_nc2 : tlcolor -> tlcolor.
Proof.
  intro c.
  destruct c as [ (*Green*) | (*Orange*) | (*Red*) ].
  Show Proof.
  - exact Orange.
  - apply next_col. Show Proof.  exact Red.
  - refine (next_col _). exact Green.
Defined.

(** It is the expected code *)
Print call_nc2.

(** Using [refine] for developing code in an incremental manner. *)
Definition call_nc3 : tlcolor -> tlcolor.
Proof.
  refine (fun c => _).
  refine (match c with
          | Green => Orange
          | Orange => _
          | Red => Green
          end).
  - refine (next_col _). refine Red.
Defined.

(** It is the same. *)
Print call_nc3.


(* --------------------------------------------------------------- *)
(** ** III. Step-by-step construction of a proof seen as a program *)

(** [refine] can also be used for writing proofs. *)
(** Instead of the type [tlcolor -> tlcolor], we state the formula
    to be proven. *)
Lemma nextnextnext_id :
  forall c:tlcolor, next_col (next_col (next_col c)) = c.
Proof.
  (** We make a function returning an equality proof for all [c] *)
  refine (fun c => _).
  (** Reasoning by case ([destruct]) *)
  refine (match c with
          | Green => _
          | Orange => _
          | Red => _
          end).
  all:exact refl_equal.
Qed.

(* -------------------------------------------------------- *)
(** Forget about proofs and go back to ordinary programming *)
(** ... well, almost ordinary:
    we start with a program  computing not a data,
    but a type (written [Set] in Coq : the type of [nat], [nat -> nat] etc.)

    Here we go beyond OCaml *)
Definition waow : tlcolor -> Set :=
  fun c =>
    match c return Set with
    | Green => nat
    | Orange => tlcolor
    | Red => tlcolor -> nat
    end.

(** We use it to write a function of [c] whose result depends on [c]:
    hence the name *dependent type*.
    It cannot be written with an arrow as usual, i.e..
    [tlcolor -> "some_type"], because this "some_type" depends on the input
    Again, this is beyond then capabilities of OCaml (in a match the type
    to be returned is the same in each case).   *)
Definition waow_waow : forall c : tlcolor, waow c :=
  fun c =>
    match c return waow c with
    | Green => 2
    | Orange => Green
    | Red => fun c' => match c' with Orange => 6 | _ => 1 end
    end.

(** Computations *)
Compute (waow_waow Green).
Compute (waow_waow Orange).
Compute (waow_waow Red).
(** So waow_waow may be applied to TWO arguments in this case *)
Compute (waow_waow Red Green).

(** Actually, [A -> B] can be written [forall a: A, B], example : *)
Check (forall c : tlcolor, nat).

(** Let us see the full pattern-matching, using a "return" clause.
    It makes it clearer that the program is well-typed. *)
Print waow_waow.

(** Back to proofs:
    let us play with Theorem [id_nextnextnext]. *)
Definition id_nextnextnext_pgm :
  forall c, c = next_col (next_col (next_col c)) :=
  fun c => 
    match c with
    | Green  => eq_refl
    | Orange => eq_refl
    | Red    => eq_refl
    end.

(** [eq_refl] is convenient (reminiscent of "by reflexivity"
    without further ado, but misleading here; the complete body
    can be obtained using the nest command. *)
Set Printing All.
Print id_nextnextnext_pgm.
(** We see that eq_refl has actual parameters fro saying that it
    is actually specialized to Green or Orange or Red.
    And the types for each case, though similar, are distinct.
*)
Unset Printing All.

(** Go back now to the original theorem.
    We can either use tactics [intro] etc. or [refine]
    with the above piece of code.
    The important point is that for a theorem we usually
    finish with [Qed] instead of [Defined].
*) 

Theorem id_nextnextnext_pgm_qed :
  forall c, c = next_col (next_col (next_col c)).
Proof. intro c; destruct c; reflexivity. Qed.

(** The code is the same. Let us try computations *)
Compute id_nextnextnext_pgm (next_col Red)       (** complete reduction *).
Compute id_nextnextnext_pgm_qed (next_col Red)   (** only [next_col Red] is reduced *).

(** Interpretation.

    The Curry-Howard correspondence provides a uniform framework
    for developing functional programs and proofs.

    Verifying that a proof is properly written becomes just an
    instance of type-checking.

    However, proofs of theorems are seen as functions that *could* be
    computed when they are called, but in most of the time the final
    results of such computations are not useful at all.  Trying to
    get them would then just be a waste of resource.
    Still, it is crucial to ensure that those results actually exist:
    computations must always terminate, otherwise we run into logical
    inconsistencies.
    This is a major difference with real programming languages, including
    typed functional programming languages like OCaml: the latter allow
    the definition of "looping" programs such as, say,
<<
    let rec f (c: tlcolor) := next_col (f c) 
>>
    whereas similar programs are strictly forbidden in Coq.
    In particular, only *structural recursive* programs are allowed
    (recursive call can only be performed on strict sub-terms of the 
    special input argument).
 *)

(**
   The typing system of Coq provides a non-interference mechanism
   which ensures that proofs have no impact on the result of meaningful
   computations: we saw that the latter are typed in a universe called [Set];
   in contrast, theorems are typed in another universe called [Prop], the
   universe of propositions.
 *)

Check forall c, c = next_col (next_col (next_col c)).

(** For illustrating the idea, let us define an "invisible" color in Prop. *)
Inductive invi_col : Prop :=
| IGreen : invi_col
| IOrange : invi_col
| IRed: invi_col
.

(** Computing an [invi_col] from a [tlcolor] is allowed because
    we want to be able to reason by case on a result of type [tlcolor]. *)
Definition possible : tlcolor -> invi_col :=
  fun c =>
    match c with
    | Green  => IOrange
    | Orange => IRed
    | Red    => IGreen
    end.

(** But the converse is not allowed. *)
Fail Definition impossible : invi_col -> tlcolor :=
  fun c =>
    match c with
    | IGreen  => Orange
    | IOrange => Red
    | IRed    => Green
    end.

(** Additional subtle key point: 
    reductions are performed during type-checking.
    This is why [waow_waow] could be accepted.
  
    To see this, Consider a variant of waow where [Qed] is used. *)
Definition waow_qed : tlcolor -> Set.
  refine(
  fun c =>
    match c return Set with
    | Green => nat
    | Orange => tlcolor
    | Red => tlcolor -> nat
    end).
Qed.

(** The same code as for [waow_waow] is rejected, because for instance,
    [waow_qed Green] does not reduce to [nat] any longer. *)
Fail Definition waow_waow_qed : forall c : tlcolor, waow_qed c :=
  fun c =>
    match c return waow_qed c with
    | Green => 2
    | Orange => Green
    | Red => fun c' => match c' with Orange => 6 | _ => 1 end
    end.

(** 
    So, in addition to what has been said before on logical consistency,
    the (desirable) decidability of type-checking requires that termination
    of computations is guaranteed.
 *)

(** 
<<
  +--------------------------+
  | Summary to be remembered |
  +--------------------------+
>>
  In Coq we have two activities : write definitions, and prove theorems.
  Though definitions are usually in [Set] while theorems are in [Prop],
  it is actually the very same activity, because a proof is just
  a function that builds a proof of a conclusion for all actual parameters
  provided in input, for example a proof of
  [next_col (next_col (next_col c)) = c]  for all [c].

  Curry-Howard correspondence :
<<
                                      proof   =   functional program
                                    formula   =   type
           provide a proof p of a formula T   =   write a program
     checking that p is indeed a proof of T   =   type checking
>>

  In order to see interesting theorems as types, we need dependent types.
  Dependent types can also be used for programming, providing very accurate
  information on inputs and outputs and additional programming facilities.
  This is particularly interesting in combination with the capability to
  write programs returning a type, whereas usual programs return a data,
  because type-checking makes no difference between types that are
  convertible (that is, computationally the same).
  Formally, Type Theory includes a very powerful rule, called the conversion rule,
  stating that if [p] has the type [T], then [p] has also any type [T'] such that 
  [T] reduces do [T'] or conversely (more generally: [T] and [T'] are convertible).
 *)