ImpAlg.ImplicativeStructures

Set Implicit Arguments.
Set Contextual Implicit.

Require Import Utf8.
Require Import Morphisms.
Require Import ImpAlg.Ens.
Require Import ImpAlg.Lattices.

We define the lifting of the arrow (a ↦ b) for sets (A ↦ b, a ↦ B, A ↦ B)

Definition arrow_set_l `{X:Set} `{arrow:X → X → X} (A:Ens) (b:X):Ens :=
  fun x => ∃a, A a ∧ x = arrow a b.
Definition arrow_set_r `{X:Set} `{arrow:X → X → X} (a:X) (B:Ens):Ens :=
    fun x => ∃b, B b ∧ x = arrow a b.
Definition arrow_set `{X:Set} `{arrow:X → X → X} (A:Ens) (B:Ens):Ens :=
    fun x => ∃a,∃b, A a ∧ B b ∧ x = arrow a b.

Global Instance arrow_set_Proper `{X:Set} `{arrow:X → X → X} a:
  Proper ((@same_set X ) ==> (@same_set X )) ((@arrow_set_r X arrow) a).
Proof.
  intros A B HAB.
  split;intros Hx; destruct Hx as [b [Hb Hx]];
  exists b;
  split;[apply HAB,Hb| assumption|apply HAB,Hb| assumption].
Qed.

Implicative Structures

Definition

Class ImplicativeStructure `{CL:CompleteLattice} :=
  {
    arrow:X → X → X;

    arrow_mon_l: ∀ a a' b, ord a a' -> ord (arrow a' b ) (arrow a b );
    arrow_mon_r: ∀ a b b', ord b b' -> ord (arrow a b ) (arrow a b');

    arrow_meet: ∀ a B, arrow a (meet_set B) = meet_set (@arrow_set_r _ arrow a B)
  }.

Infix "↦" := arrow (at level 60, right associativity):ia_scope.
Notation "a ↪ B":= (@arrow_set_r _ _ a B) (at level 69):ia_scope.

Generalizable Variables X ord join meet arrow L meet_set join_set.

Properties

Lemma arrow_mon `{IS:ImplicativeStructure}: ∀ a a' b b' , a' ≤ a -> b ≤ b' -> arrow a b ≤ arrow a' b'.
Proof.
  intros.
  apply (ord_trans _ (a' ↦ b)).
  - apply arrow_mon_l; auto.
  - apply arrow_mon_r; auto.
Qed.

Lemma arrow_prenex `{IS:ImplicativeStructure}:
  ∀ a f, (λ y:X , ∃ b : X , y = a ↦ f a b ) ≅ (@arrow_set_r X arrow a (λ y : X , ∃ b : X , y = f a b)).
Proof.
  intros.
  unfold arrow_set_l.
  split;intros;
  destruct H as [b Hb].
  - exists (f a b).
    split;[exists b | rewrite Hb];reflexivity.
  - destruct Hb as [Hb Hy].
    destruct Hb as [c Hc].
    exists c;rewrite Hy,Hc;reflexivity.
Qed.

Lemma arrow_bot `{IS:ImplicativeStructure}:
  ∀ a, a ↦ ⊤ = ⊤.
Proof.
  intros a.
  rewrite <- meet_emptyset.
  rewrite arrow_meet.
  apply meet_same_set;split.
  - intros (b,(Hb,_)).
    contradict Hb.
  - intros H.
    contradict H.
Qed.

Encoding the λ-calculus

Application

We begin by defining the application of "a" to "b", denoted by "a@b".

Definition app `{IS:ImplicativeStructure} a b:= ⊓ (fun x => a ≤ b ↦ x).
Infix "@" := app (at level 59, left associativity).

Properties of the application

Lemma app_mon_l `{IS:ImplicativeStructure}:
  ∀ a b c, a ≤ b → a @ c ≤ b @ c.
Proof.
  intros a b c Hab.
  unfold app.
  apply meet_subset.
  intros x Hx.
  apply (ord_trans _ _ _ Hab Hx).
Qed.

Lemma app_mon_r `{IS:ImplicativeStructure}:
  ∀ a b c, b ≤ c → a @ b ≤ a @ c.
Proof.
  intros a b c Hbc.
  apply meet_subset.
  intros x Hx.
  apply (ord_trans _ _ _ Hx).
  now apply arrow_mon_l.
Qed.

Lemma app_mon `{IS:ImplicativeStructure}:
  ∀ a a' b b', a ≤ a' → b ≤ b' → a @ b ≤ a' @ b'.
Proof.
  intros a a' b b' Ha Hb.
  eapply ord_trans;[apply (app_mon_l _ _ _ Ha)|].
  apply (app_mon_r _ _ _ Hb).
Qed.

Lemma app_beta `{IS:ImplicativeStructure}:
  ∀ a b, (a ↦ b ) @ a ≤ b.
Proof.
  intros a b.
  apply meet_elim.
  reflexivity.
Qed.

Lemma app_eta `{IS:ImplicativeStructure}:
  ∀ a b, a ≤ b ↦ (a@b ).
Proof.
  intros a b. unfold app.
  rewrite arrow_meet.
  apply meet_intro.
  intros x (c,(Hx,Hc)).
  now subst x.
Qed.

Lemma app_min `{IS:ImplicativeStructure}:
  ∀ a b, min (fun x => a ≤ b ↦ x) (a@b).
Proof.
intros a b.
split.
- unfold lb,app. intros y Hy. now apply meet_elim.
- apply app_eta.
Qed.

Lemma adjunction `{IS:ImplicativeStructure}:
  ∀ a b c, a @ b ≤ c ↔ a ≤ b ↦ c.
Proof.
  intros.
  split;intros.
  - apply (ord_trans _ _ _ (app_eta a b)).
    now apply arrow_mon_r.
  - apply meet_elim.
    assumption.
Qed.

Abstraction

We now define the abstraction of a function "f", which we denote by "λ' f".

Definition abs `{IS:ImplicativeStructure} f:= ⊓ (fun x => ∃ a, x = a ↦ f a).
Notation "λ- f":= (abs f) (at level 60):ia_scope.

Properties of the abstraction

Lemma abs_mon `{IS:ImplicativeStructure}:
   ∀ f g, (∀a, f a ≤ g a ) → (λ - f ) ≤ (λ - g ).
Proof.
intros f g H.
auto_meet_leq.
now apply arrow_mon_r.
Qed.

Lemma betarule `{IS:ImplicativeStructure}:
  ∀ f a, (λ - f ) @ a ≤ f a.
Proof.
  intros f a.
  apply meet_elim.
  apply meet_elim.
  exists a;reflexivity.
Qed.

Definition eta `{IS:ImplicativeStructure}a := fun x => a @ x .
Lemma etarule `{IS:ImplicativeStructure}:
   ∀ a, a ≤ (λ - (eta a )).
Proof.
  intros a.
  unfold eta,app,abs.
  apply meet_intro.
  intros b (x,Hb);subst.
  rewrite arrow_meet.
  apply meet_intro.
  intros z (b,(Hz,Hb)).
  subst.
  assumption.
Qed.

Lemma beta_red `{IS:ImplicativeStructure}:
  ∀ f t u, f t ≤ u → (λ - f )@t ≤ u.
Proof.
  intros f t u H.
  eapply ord_trans;[apply betarule|exact H].
Qed.

Properties of closure

Definition upwards_closure `{IS:ImplicativeStructure} (A:Ens):= ∀ a b, a ≤ b → A a → A b .
Definition app_closure `{IS:ImplicativeStructure} (A:Ens):= ∀ a b, A a → A b → A (a@b).
Definition mod_pon_closure `{IS:ImplicativeStructure} (A:Ens):= ∀ a b, A a → A (a ↦b) → A b.

Remark mod_pon_app `{IS:ImplicativeStructure}:
  ∀ A:Ens , upwards_closure A → (app_closure A <-> mod_pon_closure A ).
Proof.
  intros A UpC. split;intros H a b Ha Hb.
  - apply (UpC ((a↦b)@a)).
    + now apply adjunction.
    + now apply H.
  - apply (H b);intuition.
    apply (UpC a).
    + now apply adjunction.
    + assumption.
Qed.