(** * INITIATION A ROCQ (3) : types dépendants et arbres de preuve *)

(** Objectif : illustrer l'idée suivant laquelle
    - développer un programme dans un langage fonctionnel typé, et
    - construire une démonstration
    correspondent à des activités identiques.
    C'est encore plus frappant lorsque l'on considère un système de types
    enrichi, par rapport à OCaml, avec des *types dépendants*,
    comme illustré avec les fonctions "ouf" ci-dessous.

*)

(* ------------------------------------------------------------ *)
(** ** I. Prélimilaires et révisions *)
(** Type [coulfeu] et fonction [coul_suiv] (comme rocq1_B_A_BA.v). *)
Inductive coulfeu : Set :=
  | Vert : coulfeu
  | Orange : coulfeu
  | Rouge : coulfeu
.

Definition coul_suiv : coulfeu -> coulfeu :=
  fun c =>
    match c with
    | Vert => Orange
    | Orange => Rouge
    | Rouge => Vert
    end.

(** Définition interactive (comme rocq2_B_A_BA.v).   *)
(** On énonce d'abord le type du programme attendu *)
Definition coul_suiv2 : coulfeu -> coulfeu.
Proof.
  intro c.
  destruct c as [ (*Vert*) | (*Orange*) | (*Rouge*) ].
  Show Proof.
  - exact Orange.
  - exact Rouge.
  - exact Vert.
Defined.

(** C'est bien la même *)
Print coul_suiv2.

(** Définition interactive avec refine (comme rocq2_B_A_BA.v). *)
Definition coul_suiv3 : coulfeu -> coulfeu.
Proof.
  refine (fun c => _).
  refine (match c with
          | Vert => _
          | Orange => Rouge
          | Rouge => _
          end).
  - refine Orange.
(*  - refine Rouge.*)
  - refine Vert.
Defined.

(* ------------------------------------------------------------ *)
(** ** II. Petite nouveauté : la tactique apply *)

(** Une fonction sans importance qui appelle [coul_suiv]. *)
Definition appelle_cs : coulfeu -> coulfeu :=
  fun c =>
    match c with
    | Vert => Orange
    | Orange => coul_suiv Rouge
    | Rouge => Vert
    end.

(** En mode interactif, utiliser la tactique apply. *)
Definition appelle_cs2 : coulfeu -> coulfeu.
Proof.
  intro c.
  destruct c as [ (*Vert*) | (*Orange*) | (*Rouge*) ].
  Show Proof.
  - exact Orange.
  - apply coul_suiv. Show Proof.  exact Rouge.
  - refine (coul_suiv _). exact Vert.
Defined.

(** C'est bien la même sauf sur le dernier cas *)
Print appelle_cs2.

(** La tactique refine pour la construction explicite incrémentale du code. *)
Definition appelle_cs3 : coulfeu -> coulfeu.
Proof.
  refine (fun c => _).
  refine (match c with
          | Vert => Orange
          | Orange => _
          | Rouge => Vert
          end).
  - refine (coul_suiv _). refine Rouge.
Defined.

(** C'est bien la même. *)
Print appelle_cs3.


(* -------------------------------------------------------------- *)
(** ** III. Construction pas à pas d'une preuve vue comme un programme *)

(** On peut aussi utiliser refine pour écrire des arbres de preuve. *)
(** À la place du type [coulfeu -> coulfeu], on énonce la formule du
    lemme à prouver. *)
Lemma suivsuivsuivp_id :
  forall c:coulfeu, coul_suiv (coul_suiv (coul_suiv c)) = c.
Proof.
  (** On fabrique une fonction qui rend une preuve d'égalité pour tout [c] *)
  refine (fun c => _).
  (** Raisonnement par cas (comme destruct) *)
    refine (match c with
          | Vert => _
          | Orange => _
          | Rouge => _
          end).
  - cbn [coul_suiv]. refine eq_refl (** ce que fabrique reflexivity *).
  - reflexivity (** marche même sans cbn *).
  - refine eq_refl (** de même *).
Qed.


(* -------------------------------------------------------------- *)
(** Oublions les preuves et revenons à la programmation ordinaire *)
(** ... enfin, presque ordinaire :
    on commence par un programme  calculant non pas une donnée,
    mais un type (qui s'écrit [Set] en Rocq : le type de [nat], etc.)

    Ici on sort des possibilités de OCaml *)
Definition ouf : coulfeu -> Set :=
  fun c =>
    match c with
    | Vert => nat
    | Orange => bool
    | Rouge => bool -> nat
    end.

(** On l'utilise pour écrire une fonction de c dont le résultat dépend de c :
    c'est ce qu'on appelle un type dépendant :
    on ne peut pas l'écrire avec une flèche comme d'habitude, c-à-d.
    [coulfeu -> "quelque_chose"], car ce "quelque_chose" dépend de l'entrée.
    Là encore, on sort des possibilités de OCaml (dans un match le type
    retourné est le même dans chaque cas).   *)
Definition ouf_ouf : forall c : coulfeu, ouf c :=
  fun c =>
    match c with
    | Vert => 2
    | Orange => true
    | Rouge => fun b => match b with true => 8 | false => 5  end
    end.

(** En fait, [A -> B] peut s'écrire [forall a: A, B], exemple : *)
Check (forall c : coulfeu, nat).

(** Développement interactif de [ouf_ouf]. *)
Definition ouf_ouf2 : forall c, ouf c.
Proof.
  refine (fun c => _).
  refine (match c with
    | Vert => _
    | Orange => _
    | Rouge => _
    end).
  - cbn [ouf]. refine 2.
  - cbn [ouf]. refine true.
  - cbn [ouf]. refine (fun b => _). destruct b as [ | ].
    + refine 8.
    + refine 5.
Defined.

Compute (ouf_ouf2 Vert).
Compute (ouf_ouf2 Orange).
Compute (ouf_ouf2 Rouge).
Compute (ouf_ouf2 Rouge false).

(** [ouf_ouf2] est bien le la même chose que [ouf_ouf]. *)
Lemma meme_ouf_ouf : ouf_ouf2 = ouf_ouf.
Proof. reflexivity. Qed.

(** L'affichage fait apparaître une clause "return" dans le match.
    On voit alors explicitement que le programme reste bien typé. *)
Print ouf_ouf.
Print ouf_ouf2.

(* Soyons joueur : écriture directe du lemme [suivsuivsuiv_id]. *)
Definition suivsuivsuiv_id_direct :
  forall c:coulfeu, coul_suiv (coul_suiv (coul_suiv c)) = c :=
  fun c =>
    match c with
    | Vert => eq_refl
    | Orange => eq_refl
    | Rouge => eq_refl
    end.

(**
<<
  +-----------------------+
  | En résumé, à retenir. |
  +-----------------------+
>>
  En Rocq on a deux activités : poser des définitions et démontrer des théorèmes.
  En réalité il s'agit d'une seule et même activité, car une démonstration n'est au fond
  rien d'autre qu'une fonction qui fabrique une preuve de la conclusion pour tout paramètre
  effectif donné en entrée, par exemple une preuve de  [coul_suiv (coul_suiv (coul_suiv c)) = c]
  pour tout [c].
  On est ici dans un univers où les preuves sont matérialisées par des arbres appelés arbres 
  de preuve. Ces derniers sont, d'une manière générale, des structures de données
  dont on a vu jusqu'ici quelques espèces, notamment :
  - des feuilles étiquetées "réflexivité de l'égalité" fabriquant des preuves de formules [x = x] ;
  - des nœuds binaires étiquetés "rewrite" fabriquant une preuve de [P y] à partir
    d'un sous-arbre prouvant une égalité de la forme [x = y]
    et d'un sous-arbre prouvant [P x] ;
  - des nœuds étiquetés "intro" permettant de prouver des propriétés de la forme [P -> Q],
    ou plus généralement [∀x, P x] ;
    on obtient ainsi des (AST de) programmes fonctionnels manipulant des (arbres de) preuves.

  Les types de tous ces arbres de preuve sont exprimés avec une formule logique,
  comprenant notamment la flèche (se lisant indifféremment comme l'implication ou comme un type
  fonctionnel) et le quantificateur ∀.

  Les formules [Q -> R] et [P -> Q -> R] sont des types de fonctions ayant respectivement 1 
  et 2 arguments. Pour l'uniformité, on considérera que [R] est également le type d'une fonction, 
  ayant 0 argument, ce qui permet de voir tous les arbres de preuve comme des (AST de) 
  programmes fonctionnels.

  On a également vu la notion de *type dépendant* sur l'exemple de la fonction [ouf_ouf] qui 
  rend un résultat dont *le type* (et non seulement le résultat) dépend de l'entrée,
  ce qui est au-delà des possibilités des langages usuels y compris OCaml.

  On observe alors qu'en tant que type, une proposition à démontrer telle que
  [coul_suiv (coul_suiv (coul_suiv c)) = c] est un type dépendant :
  d'une manière générale [P vert] et [P rouge] sont des propriétés distinctes,
  et en particulier [coul_suiv (coul_suiv (coul_suiv Vert)) = Vert] est une égalité distincte
  de [coul_suiv (coul_suiv (coul_suiv Rouge)) = Rouge], même s'il se trouve que leurs
  preuves sont analogues du fait de la simplicité de l'exemple.

  Plus profondément, on a illustré la correspondance suivante, dite de Curry-Howard :
<<
            preuve         =   programme fonctionnel (sous forme d'AST)
            formule        =   type
     prouver une formule   =   programmer
>>
  La correspondance de Curry-Howard est une avancée conceptuelle majeure qui fonde
  les assistants modernes à la preuve comme Rocq.

  *)