ImpAlg.OCA


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 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.

Ordered Combinatory Algebras

Order combinatory algebras are a variant of Hofstra & Van Oosten partial ordered combinatory algebras where the application is total

Class OCA `{O:Order}:=
{
   app : X → X → X;
   k:X;
   s:X;
  
   app_mon : ∀ a a' b b', a ≤ a' → b ≤ b' → app a b ≤ app a' b';
   k_red: ∀ a b, app (app k a) b ≤ a ;
   s_red: ∀ a b c, app (app (app s a) b) c ≤ app (app a c) (app b c )
}.

Notation "a @ b ":=(app a b).

The arrow on P(A) is defined as the sets of realizers of the corresponding implication:
A → B := {r ∈ A : ∀a ∈ A.ra ∈ B}

Definition realize `{O:OCA} (A B:Ens) := fun r => ( ∀a, A a → B (r @ a)).
Definition carreer `{O:OCA}:@Ens X:=fun x=> True.

Induced implicative structure

Proposition 8: P(A) equipped with the arrow above is an implicative structure.

Global Instance OCA_IS `{O:OCA}:
    @ImplicativeStructure _ _ _ (@Powerset_CompleteLattice _ carreer):= {
        arrow := realize
      }.
Proof.
- intros A A' B H r real. unfold In in *. intros a Ha. apply real,H. trivial.
- intros A A' B H r real. intros b Hb. apply H,real. trivial.
- intros A B. apply Extensionality_Ensembles. split; intros r Hr;unfold In,realize in *.
  + intros E [s [Hs HE]]. rewrite HE; simpl.
  intros a Ha. eapply Intersection_set_lb;[ | apply Hr];trivial.
  + intros a Ha S HS.
     unfold arrow_set_r,meet_set,Powerset_CompleteLattice,Intersection_set in Hr.
     specialize (Hr (λ r : X, ∀ a : X, A a → S (r @ a))).
     apply Hr;trivial.
     exists S;split;trivial.
Qed.