(** * "Partial functions (×)", code extraction *)

(** (×) in the extensional (set-theoretical) sense *)

Inductive color : Set :=
| Purple : color
| Indigo : color
| Blue   : color
| Green  : color
| Yellow : color
| Orange : color
| Red    : color
.

Inductive nextcolor : color -> color -> Prop :=
| CSv : nextcolor Green Orange
| CSo : nextcolor Orange Red
| CSr : nextcolor Red Green
.

(** Constraint defined in sort Set *)
Inductive is_tlcolor : color -> Set :=
| Tgre : is_tlcolor Green
| Tora : is_tlcolor Orange
| Tred : is_tlcolor Red
.

Definition fct_nxtcol c (t : is_tlcolor c) : color :=
  match t with
  | Tgre => Orange
  | Tora => Red
  | Tred => Green
  end.

(** The intended algorithm is NOT as expected *)

Require Import Extraction.
Recursive Extraction fct_nxtcol.

(*
let fct_nxtcol _ = function
| Tgre -> Orange
| Tora -> Red
| Tred -> Green


let fct_nxtcol c = fun t -> 
match t with
| Tgre -> Orange
| Tora -> Red
| Tred -> Green

let fct_nxtcol c = 
match c with
| Green -> Orange
| Orange -> Red
| Read -> Green
| _ -> failwith "not allowed"

*)

Reset is_tlcolor.

(** Constraint defined in sort Prop *)
Inductive is_tlcolor : color -> Prop :=
| Tgre : is_tlcolor Green
| Tora : is_tlcolor Orange
| Tred : is_tlcolor Red
.

Fail Definition fct_nxtcol c (t : is_tlcolor c) : color :=
  match t with
  | Tgre => Orange
  | Tora => Red
  | Tred => Green
  end.

(** Pieces of information available in Prop are not available at the Set level *)

(* -------------------------------- *)
(** Small inversion of [is_tlcolor] *)

Inductive is_Green : Prop := Tgre' : is_Green.
Inductive is_Orange : Prop := Tora' : is_Orange.
Inductive is_Red : Prop := Tred' : is_Red.
Inductive is_tlcother : Prop :=.

Definition is_tlcolor_dispatch (c : color) :=
  match c with
  | Green => is_Green
  | Orange => is_Orange
  | Red => is_Red
  | _ => is_tlcother
  end.

Lemma is_tlcolor_inv {c} (it : is_tlcolor c) : is_tlcolor_dispatch c.
Proof. destruct it; constructor. Qed.
(* -------------------------------- *)

Definition fct_nxtcol c (t : is_tlcolor c) : color :=
  match c return is_tlcolor c -> _ with
  | Green  => fun t => Orange
  | Orange => fun t => Red
  | Red    => fun t => Green
  | _      => fun t => match is_tlcolor_inv t with end
  end t.

Definition fct_nxtcol_script c (t : is_tlcolor c) : color.
Proof.
  destruct c.
  - Check (is_tlcolor_inv t).
    destruct (is_tlcolor_inv t).
  - destruct (is_tlcolor_inv t).
  - destruct (is_tlcolor_inv t).
  - exact Orange.
  - destruct (is_tlcolor_inv t).
  - exact Red.
  - exact Green.
Defined.

(** Better to check that we defined the expected one *)
Lemma fct_nxtcol_corr : forall c (t : is_tlcolor c), nextcolor c (fct_nxtcol_script c t).
Proof.
  intros c t. destruct t; cbn. Undo. destruct t; cbn; constructor.
Qed.

(** Alternative: correctness-by-construction *)

Inductive nxtcol_spec (c : color) : Set :=
  | NC_mk : forall c', nextcolor c c' -> nxtcol_spec c.

Definition fct_nxtcol_cbc c (t : is_tlcolor c) : nxtcol_spec c.
Proof.
  destruct c.
  - destruct (is_tlcolor_inv t).
  - destruct (is_tlcolor_inv t).
  - destruct (is_tlcolor_inv t).
  - refine (NC_mk Green Orange _) (** NO OTHER CHOICE *). constructor.
  - destruct (is_tlcolor_inv t).
  - refine (NC_mk _ Red _). constructor.
  - exists Green. constructor.
Defined.


Definition fct_nxtcol_cbc_refine c (t : is_tlcolor c) : nxtcol_spec c.
Proof.
  refine(
  match c return is_tlcolor c -> _ with
  | Green  => fun t => NC_mk Green Orange _
  | Orange => fun t => NC_mk _ Red _
  | Red    => fun t => _
  | _      => fun t => match is_tlcolor_inv t with end
  end t).
  - constructor.
  - constructor.
  - exact (NC_mk _ Green CSr).
Defined.

Compute (fct_nxtcol_cbc Orange Tora).

Definition resu_nxtcol c t := let (c', _) := fct_nxtcol_cbc c t in c'.

Compute (resu_nxtcol Orange Tora).

Theorem resu_nxtcol_correct c t : nextcolor c (resu_nxtcol c t).
Proof.
  unfold resu_nxtcol. destruct (fct_nxtcol_cbc c t) as [c' nc]. exact nc.
Qed.

(** The general [sig] type *)
Print sig.
Print prod.

Definition fct_nxtcol_cbc_sig c (t : is_tlcolor c) : {c' | nextcolor c c'}.
Proof.
  refine(
  match c return is_tlcolor c -> _ with
  | Green  => fun t => _
  | Orange => fun t => _
  | Red    => fun t => _
  | _      => fun t => match is_tlcolor_inv t with end
  end t).
  - exists Orange. constructor.
  - exists Red. constructor.
  - exists Green. constructor.
Defined.

Definition resu_nxtcol_sig_real c t :=
  match fct_nxtcol_cbc_sig c t with exist _ c' _ => c' end.

Definition resu_nxtcol_sig c t :=
  let (c', _) := fct_nxtcol_cbc_sig c t in c'.

Compute (resu_nxtcol_sig Orange Tora).

(* ------------------------------------------------------------------------------ *)

(** Extraction of a correct-by-construction OCaml program *)

Require Import Extraction.

Recursive Extraction fct_nxtcol fct_nxtcol_cbc_sig.


(* --------------------------------------------------------------------- *)
(** Exception to the Prop/Set elimination rule: 
    inductive propositions with 0 case can be eliminated to Set *)

(** Reminder
Inductive is_tlcother : Prop :=.
*)

Lemma exception0_Prop_Set : is_tlcother -> color.
Proof.
  intro t. refine (match t with end).
Qed.
  
(** Inductive is_Red : Prop := Tred' : is_Red. *)
Lemma exception1_Prop_Set : is_Red -> color.
Proof.
  intro t. refine (match t with Tred' => Blue end).
Qed.

Print True.

Inductive twovals : Prop :=
| tv1 : twovals
| tv2 : twovals.
  
Lemma exception2_Prop_Set : twovals -> color.
Proof.
  intro t. Fail refine (match t with tv1 => Blue | tv2 => Green end).
Abort.

Lemma ok : twovals -> twovals.
Proof.  intro t. refine (match t with tv1 => tv2 | tv2 => tv1 end).


  
(**
   General principle: no information can leak from Prop to Set.
*)

(** Remark: 0-case elimination Prop/Set can be avoided using some tricks presented 
    in the paper on the Braga method *)