human
Lors de l'encodage d'une logique dans un assistant de preuve tel que Coq ou Isabelle, il faut choisir entre une intégration superficielle (shallow embedding) et une intégration profonde (deep embedding). Dans une intégration superficielle, les formules logiques sont écrites directement dans la logique du prouveur de théorèmes, tandis que dans une intégration profonde, les formules logiques sont représentées sous forme de type de données.

* Quels sont les avantages et les limitations des différentes approches ?
* Existe-t-il des lignes directrices pour déterminer laquelle utiliser ?
* Est-il possible de passer d'une représentation à l'autre de manière systématique ?

En guise de motivation, j'aimerais encoder différentes logiques liées à la sécurité dans Coq et je me demande quels sont les avantages et les inconvénients des différentes approches
gpt
> Quels sont les avantages et les limitations des différentes approches ?

* Avantages de l'intégration profonde : Vous pouvez prouver et définir des choses par induction sur la structure des formules. Des exemples d'intérêt sont la taille d'une formule.
* Inconvénients de l'intégration profonde : Vous devez traiter explicitement la liaison des variables. C'est généralement très laborieux.

> Existe-t-il des lignes directrices pour déterminer laquelle utiliser ?

Les intégrations superficielles sont très utiles pour importer des résultats prouvés dans la logique objet. Par exemple, si vous avez prouvé quelque chose dans une petite logique (par exemple, la logique de séparation), les intégrations superficielles peuvent être un outil de choix pour importer votre résultat dans Coq.
D'autre part, les intégrations profondes sont presque indispensables lorsque vous souhaitez prouver des méta-théorèmes sur la logique objet (comme l'élimination des coupures, par exemple).

> Est-il possible de passer d'une représentation à l'autre de manière systématique ?

L'idée derrière l'intégration superficielle est vraiment de travailler directement dans un modèle des formules objet. En général, les gens vont mapper une formule objet P directement (en utilisant des notations ou en faisant la traduction à la main) à un élément de Prop. Bien sûr, il existe des éléments de Prop qui ne peuvent pas être obtenus en intégrant une formule de la logique objet. Par conséquent, vous perdez une certaine forme de complétude.

Il est donc possible d'envoyer chaque résultat obtenu dans un contexte d'intégration profonde à travers une fonction d'interprétation.
Voici un petit exemple en Coq :
```
Inductive formula : Set :=
    Ftrue : formula
  | Ffalse : formula
  | Fand : formula -> formula -> formula
  | For : formula -> formula -> formula.
Fixpoint interpret (F : formula) : Prop := match F with
    Ftrue => True
  | Ffalse => False
  | Fand a b => (interpret a) /\ (interpret b)
  | For a b => (interpret a) \/ (interpret b)
 end.
Inductive derivable : formula -> Prop :=
    deep_axiom : derivable Ftrue
  | deep_and : forall a b, derivable a -> derivable b -> derivable (Fand a b)
  | deep_or1 : forall a b, derivable a -> derivable (For a b)
  | deep_or2 : forall a b, derivable b -> derivable (For a b).
Inductive sderivable : Prop -> Prop :=
    shallow_axiom : sderivable True
  | shallow_and : forall a b, sderivable a -> sderivable b -> sderivable (a /\ b)
  | shallow_or1 : forall a b, sderivable a -> sderivable (a \/ b)
  | shallow_or2 : forall a b, sderivable b -> sderivable (a \/ b).
(* Vous pouvez prouver le lemme suivant : *)
Lemma shallow_deep :
   forall F, derivable F -> sderivable (interpret F).
(* Vous ne pouvez PAS prouver le lemme suivant : *)
Lemma t :
   forall P, sderivable P -> exists F, interpret F = P.
```