ImpAlg.AKS


Set Implicit Arguments.
Set Contextual Implicit.

Require Import Utf8.
Require Import Setoid.
Require Import Morphisms.
Require Export Relation_Definitions.
Require Import Sets.Ensembles.
Require Import Sets.Powerset.
Require Import ImpAlg.Lattices.
Require Import ImpAlg.HeytingAlgebras.
Require Import ImpAlg.ImplicativeStructures.
Require Import ImpAlg.ImplicativeAlgebras.
Require Import ImpAlg.Adequacy.
Require Import ImpAlg.Combinators.
Require Import ImpAlg.Powerset.

Abstract Krivine Structures


Class AKS `{Λ:Type} `{Π:Type}:=
{
  app : Λ → Λ → Λ;
  push: Λ → Π → Π;
  cont: Π → Λ;
  k: Λ; s: Λ; cc: Λ;
  PL : Λ → Prop;
  pole : Λ → Π → Prop;

  red_push: ∀ t u π, pole t (push u π) → pole (app t u) π;
  red_k:∀ t u π, pole t π → pole k (push t (push u π));
  red_s:∀ t u v π, pole (app (app t v) (app u v)) π → pole s (push t (push u (push v π)));
  red_cc: ∀ t π, pole t (push (cont π) π) → pole cc (push t π);
  red_cont: ∀ t π π0, pole t π → pole (cont π ) (push t π0);

  PL_s: PL s; PL_k: PL k; PL_cc: PL cc;
  PL_app_closed: ∀ t u, PL t → PL u → PL (app t u);
}.

Hint Resolve PL_s PL_k PL_cc PL_app_closed.
Notation "a @ b ":=(app a b).
Notation "a · b ":=(push a b) (at level 75).
Notation "k[ π ]":=(cont π).

We define the main notions related to the definition of realizability models.
Orthogonality relation with respect to the pole.

Definition orth `{O:AKS} (A:@Ens Π) := fun r => ( ∀a, A a → pole r a).

Definition of the arrow in P(A) as the sets of realizers of the correspoding implication in the AKS:
a → b := {t · π : t ⊥⊥ a ∧ π ∈ b}

Definition arrow `{O:AKS} (A B:@Ens Π):=fun r=> ∃ t π, (r = (t · π) ∧ (orth A) t ∧ B π).

The ordering will be defined by reverse inclusion of sets of stacks.

Definition revinc `{O:AKS} (A B:@Ens Π):= Included Π B A.

Lemma revinc_orth `{O:AKS} (A A':@Ens Π) : revinc A A' → Included Λ (orth A) (orth A').
Proof.
  intros Rev a Ha a' Ha'.
  apply Ha,Rev. trivial.
Qed.

Induced implicative structure.


(* Proposition 9: any AKS induces an implicative structures 
   by considering the powerset of stacks as carrerr. *)

Global Instance AKS_IS `{O:AKS}:
  @ImplicativeStructure _ _ _
      (@RevCompleteLattice _ _ _ (@Powerset_CompleteLattice _ (λ x:Π, True))):= {
        arrow := arrow
      }.
Proof.
  - intros A A' B H r (t,(π,(Hr,(Ht,Hπ)))). unfold In,arrow.
    exists t. exists π. repeat split;trivial.
    intros s Hs. apply Ht,H. trivial.
  - intros A A' B H r (t,(π,(Hr,(Ht,Hπ)))). unfold In,arrow.
    exists t. exists π. repeat split;trivial.
    apply H;trivial.
  - intros A B. apply Extensionality_Ensembles.
    split; intros r Hr;unfold In,arrow in *.
    + destruct Hr as (t,(π,(Hr,(Ht,(B0,(HB,Hπ)))))).
      unfold arrow_set_r,meet_set,RevCompleteLattice,Powerset_CompleteLattice,Union_set in *.
      simpl in *.
      repeat (later;split);[exact HB|reflexivity|].
      simpl. exists t. exists π; repeat split;trivial.
    + destruct Hr as (B0,((b,(Hb,HB0)),Ht)). subst.
      destruct Ht as (t,(π,(Hr,(Orth,Hπ)))).
      exists t. exists π. repeat (split;trivial).
      exists b;split ;assumption.
Defined.

Ltac in_arrow:= later;later;split;[reflexivity| ];split;auto.

Properties of the combinators

Lemma 21: combinatory terms realize their principal types
k realizes ∀ab.a ⇒ b ⇒ a, ie K

Lemma Kreal `{O:AKS}: orth (@K _ _ _ _ AKS_IS) k.
Proof.
  intros π Hπ. destruct Hπ as [X [[A HX] Hπ]]. subst.
  destruct Hπ as [X [[B HX] Hπ]]. subst.
  destruct Hπ as [t [π0 [H1 [Ht [u [τ [H [Hu Hτ]]]]]]]]. subst.
  apply red_k,Ht;auto.
Qed.

s realizes ∀abc.(a ⇒ b ⇒ c ) ⇒ (a ⇒ b) ⇒ a ⇒ c), ie S.

Lemma Sreal `{O:AKS}: orth (@S _ _ _ _ AKS_IS) s.
Proof.
  intros π Hπ. destruct Hπ as [X [[A HX] Hπ]]. subst.
  destruct Hπ as [X [[B HX] Hπ]]. subst.
  destruct Hπ as [X [[C HX] Hπ]]. subst.
  destruct Hπ as [t [π0 [H1 [Ht [u [π2 [H [Hu [v [τ [H2 [Hv Hτ]]]]]]]]]]]]. subst.
  apply red_s,red_push,red_push.
  apply Ht;auto.
  in_arrow. in_arrow.
  intros π Hπ. apply red_push,Hu.
  in_arrow.
Qed.

cc realizes ∀ab.((a ⇒ b) ⇒ a )⇒ a.

Lemma CCreal `{O:AKS}: orth (@Adequacy.cc _ _ _ _ AKS_IS) cc.
Proof.
    intros π Hπ. destruct Hπ as [X [[A HX] Hπ]]. subst.
    destruct Hπ as [X [[B HX] Hπ]]. subst.
    destruct Hπ as [t [τ [H1 [Ht Hτ]]]]. subst.
    apply red_cc. apply Ht.
    in_arrow.
    intros π [u [ρ [H1 [Hu Hρ]]]]. subst.
    apply red_cont,Hu;trivial.
Qed.

Induced implicative algebra

Example 27: Any AKS gives rise to an implicative algebra

Global Instance AKS_IA `{O:AKS}:
  @ImplicativeAlgebra _ _ _ _ AKS_IS:= {
        separator:= (λ A, ∃t,(PL t ∧ orth A t))
      }.
Proof.
  - intros A B [u [PLu Hu]] [t [PLt Ht]].
    exists (t@u). split;auto.
    intros π Hπ. apply red_push. apply Ht.
    unfold arrow;simpl.
    in_arrow.
  - intros A B HAB [t [PLt Ht]].
    exists t. split;trivial.
    intros π Hπ. apply Ht.
    apply HAB,Hπ.
  - exists k. split;auto. apply Kreal.
  - exists s. split;auto. apply Sreal.
  - exists cc;split;auto. apply CCreal.
Defined.