Microexperiment with linera hoas

linear.v

Require Import Coq.Unicode.Utf8.
Require Import Coq.Classes.SetoidClass.

Inductive type := set | unit | prod (_ _: type).
Infix "*" := prod.

Inductive function: type → Set :=
| emptyset: function unit
| infinity: function unit
| succ: function set
| union: function set
| power: function set.

Inductive relation: type → Set :=
| mem: relation (set * set).

Class Heyting := {
    H: Set ;

    true: H ;
    false: H ;

    and: H → H → H ;
    or: H → H → H ;
    impl: H → H → H ;

    and_true_l P: and true P = P ;
    or_false_l P: or false P = P ;

    and_assoc P Q R: and (and P Q) R = and P (and Q R) ;
    or_assoc P Q R: or (or P Q) R = or P (or Q R) ;

    and_comm P Q: and P Q = and Q P ;
    or_comm P Q: and P Q = and Q P ;

    and_idem P: and P P = P ;
    or_idem P: or P P = P ;

    or_and P Q: or P (and P Q) = P ;
    and_or P Q: and P (or P Q) = P ;

    eval P Q: and (and (impl P Q) P) Q = and (impl P Q) P ;
    curry P Q: and P (impl Q (and P Q)) = P ;
  }.

Coercion H: Heyting >-> Sortclass.

Notation "⊤" := true.
Notation "⊥" := false.

Infix "∧" := and.
Infix "∨" := or.
Infix "→" := impl.

Notation "P ↔ Q" := (impl P Q ∧ impl Q P).

Definition entail `{H:Heyting} (P Q: H): Prop := (P ∧ Q) = P.
Infix "⊢" := entail (at level 90).

Class Linear := {
    E: type → Heyting ;

    once: ∀ {τ1 τ2}, (E τ1 → E τ2) → Prop ;

    tt: E unit ;
    step {τ}: E unit → E τ → E τ ;

    fanout {τ1 τ2}: E τ1 → E τ2 → E (τ1 * τ2) ;
    letBe {τ1 τ2 τ3}: E (τ1 * τ2) → ∀ (f: E τ1 → E τ2 → E τ3), (∀ y, once (λ x, f x y)) →  (∀ x, once (λ y, f x y))  → E τ3 ;

    lam {τ1 τ2}: ∀ (f: E τ1 → E τ2), once f → E (τ1 * τ2) ;
    app {τ1 τ2}: E (τ1 * τ2) → E τ1 → E τ2 ;

    del {τ}: E τ → E unit ;
    dup {τ}: E τ → E (τ * τ) ;

    fn {τ}: function τ → E τ → E set ;
    rel {τ}: relation τ → E τ → E unit ;

    step_Proper {τ}: Proper (entail ==> entail ==> entail) (@step τ) ;

    fanout_Proper {τ1 τ2}: Proper (entail ==> entail ==> entail) (@fanout τ1 τ2) ;
    (* letBe_Proper {τ1 τ2 τ3}: Proper (entail ==> pointwise_relation _ (pointwise_relation _ entail) ==> entail) *)
    (*                                 (λ x f, @letBe τ1 τ2 τ3 x f p q) ; *)

    (* lam_Proper {τ1 τ2}: Proper (pointwise_relation _ entail ==> entail) (@lam τ1 τ2) ; *)
    app_Proper {τ1 τ2}: Proper (entail ==> entail ==> entail) (@app τ1 τ2) ;

    del_Proper {τ}: Proper (entail ==> entail) (@del τ) ;
    dup_Proper {τ}: Proper (entail ==> entail) (@dup τ) ;

    fn_Proper {τ} F: Proper (entail ==> entail) (@fn τ F) ;
    rel_Proper {τ} F: Proper (entail ==> entail) (@rel τ F) ;

    once_var {τ}: once (λ x:E τ, x) ;

    once_and_l {τ1 τ2} (f: E τ1 → E τ2) y: once f → once (λ x, f x ∧ y) ;
    once_and_r {τ1 τ2} (f: E τ1 → E τ2) y: once f → once (λ x, y ∧ f x) ;

    once_or_l {τ1 τ2} (f: E τ1 → E τ2) y: once f → once (λ x, f x ∨ y) ;
    once_or_r {τ1 τ2} (f: E τ1 → E τ2) y: once f → once (λ x, y ∨ f x) ;

    once_impl_l {τ1 τ2} (f: E τ1 → E τ2) y: once f → once (λ x, f x → y) ;
    once_impl_r {τ1 τ2} (f: E τ1 → E τ2) y: once f → once (λ x, y → f x) ;

    once_fanout_l {τ1 τ2 τ3} (f: E τ1 → E τ2) (y: E τ3): once f → once (λ x, fanout (f x) y) ;
    once_fanout_r {τ1 τ2 τ3} (f: E τ1 → E τ2) (y: E τ3): once f → once (λ x, fanout y (f x)) ;

    once_letBe_l {τ1 τ2 τ3 τ4} (f: _ → E (τ2 * τ3)) (g: _ → _ → E τ4) p q:
      once f →
      once (λ x: E τ1, letBe (f x) g p q) ;

    once_app_l {τ1 τ2 τ3} (f: E τ1 → E (τ2 * τ3)) y: once f → once (λ x, app (f x) y) ;
    once_app_r {τ1 τ2 τ3} (f: E τ1 → E τ2) (y: E (τ2 * τ3)): once f → once (λ x, app y (f x)) ;

    (* not sure here *)
    once_lam {τ1 τ2 τ3} (f: E τ1 → E τ2 → E τ3) p:
      (∀ y, once (f y)) →
      once (λ x, lam (f x) (p x)) ;
    once_letBe_r {τ1 τ2 τ3 τ4} y (g: E τ1 → E τ2 → E τ3 → E τ4) p q:
      once (λ x, letBe y (g x) (p x) (q x)) ;

    once_dup {τ1 τ2} (f: E τ1 → E τ2): once (λ x, dup (f x)) ;
    once_del {τ1 τ2} (f: E τ1 → E τ2): once (λ x, del (f x)) ;

    once_fn {τ1 τ2} F (f: E τ1 → E τ2): once (λ x, fn F (f x)) ;
    once_rel {τ1 τ2} R (f: E τ1 → E τ2): once (λ x, rel R (f x)) ;
}.

Coercion E: Linear >-> Funclass.

Notation "⟨ x , y , .. , z ⟩" := (fanout .. (fanout x y) .. z).

Notation "'LET' ( x , y ) ':=' e1 'in' e2" := (letBe e1 (λ x y, e2) _ _) (x name, y name, at level 100).


Existing Class once.

Existing Instance once_var.

Existing Instance once_and_l.
Existing Instance once_and_r.
Existing Instance once_or_l.
Existing Instance once_or_r.
Existing Instance once_impl_l.
Existing Instance once_impl_r.

Existing Instance once_fanout_l.
Existing Instance once_fanout_r.
Existing Instance once_letBe_l.
Existing Instance once_letBe_r.
Existing Instance once_lam.
Existing Instance once_app_l.
Existing Instance once_app_r.
Existing Instance once_del.
Existing Instance once_dup.
Existing Instance once_fn.
Existing Instance once_rel.

Declare Instance L: Linear.

Definition transpose {τ1 τ2} (e: L (τ1 * τ2)): L (τ2 * τ1) :=
  LET (x, y) := e in
  ⟨y, x⟩.

Instance once_transpose {τ1 τ2 τ3} (f: L τ1 → L (τ2 * τ3)) `(@once _ τ1 (τ2 * τ3) f): once (λ x: L τ1, transpose (f x)) := _.

Definition eq {τ} (e e': L τ): L unit := app ⟨e, ⊤⟩ e'.
Infix "=" := eq.

Instance once_eq_r {τ1 τ2} (y: L τ2) (f: L τ1 → L τ2) `(@once _ τ1 τ2 f): once (λ x, eq y (f x)) := _.

Instance once_eq_l {τ1 τ2} (y: L τ2) (f: L τ1 → L τ2) `(@once _ τ1 τ2 f): once (λ x, eq (f x) y) := _.

Definition indef {τ} (f: L τ → L unit) p: L τ := app (transpose (lam f p)) ⊤.

Instance once_indef {τ1 τ2} (f: L τ1 → L τ2 → L unit) p: once (λ x, indef (f x) (p x)) := _.

Definition colim {τ} (f: L τ → L unit) p: L unit :=
  LET (x, y) := dup (lam f p) in
  app x (app (transpose y) ⊤).

Instance once_colim {τ1 τ2} (f: L τ1 → L τ2 → L unit) p: once (λ x, colim (f x) (p x)) := _.

#[program]
Definition lim {τ} (f: L τ → L unit) p: L unit := lam f p = lam del _.

Next Obligation.
Proof.
  apply once_del.
Defined.

#[program]
Instance once_lim {τ1 τ2} (f: L τ1 → L τ2 → L unit) p: once (λ x, lim (f x) (p x)) := _.

Next Obligation.
Proof.
  unfold lim.
  apply once_eq_l.
  apply once_lam.
  apply p.
Defined.

Notation "∅" := (fn emptyset ⊤).
Notation "∞" := (fn infinity ⊤).
Notation "'S' x" := (fn succ x) (at level 1).
Notation "'⋃' x" := (fn union x) (at level 1).

Notation "x ∈ y" := (rel mem ⟨x, y⟩) (at level 30).

Inductive axiom: L unit → Prop :=
| axiom_empty: axiom (lim (λ x, x ∈ ∅ → ⊥) _)

(* | axiom_union: axiom (lim (λ x, lim (λ z, x ∈ ⋃ z ↔ colim (λ y, x ∈ y ∧ y ∈ z) _) _) _) *)

| axiom_infinity_1: axiom (∅ ∈ ∞)
(* | axiom_infinity_2: axiom ( *)
(*                         lim (λ x, *)
(*                               LET (y, z) := dup x in *)
(*                                y ∈ ∞ → S z ∈ ∞) _) *)
.

Existing Class axiom.

Existing Instance axiom_empty.
Existing Instance axiom_infinity_1.
(* Existing Instance axiom_infinity_2. *)