Library Sat

Require Import Lambda.

A somehow abstract interface to work with reducibility candidates or saturated sets.

Theory of saturated sets

Module Type SAT.

The type of "saturated sets" and basic relations: equality and membership

  Parameter SAT : Type.
  Parameter eqSAT : SAT -> SAT -> Prop.
  Parameter inSAT : term -> SAT -> Prop.
  Parameter eqSAT_def : ∀ X Y,
    eqSAT X Y <-> (∀ t, inSAT t X <-> inSAT t Y ).
  Definition inclSAT A B := ∀ t, inSAT t A -> inSAT t B.

  Parameter inSAT_morph : Proper ((@eq term ) ==> eqSAT ==> iff) inSAT.

Essential properties of saturated sets :

they are sets of SN terms
they are closed by head expansion

  Parameter sat_sn : ∀ t S, inSAT t S -> sn t.
  Parameter inSAT_exp : ∀ S u m,
    boccur 0 m = true \/ sn u ->
    inSAT (subst u m) S ->
    inSAT (App (Abs m) u) S.

A term that belongs to all saturated sets (e.g. variables)

Parameter daimon : term.
Parameter varSAT : ∀ S, inSAT daimon S.

Closure properties are preserved by head contexts

  Parameter inSAT_context : ∀ u u' v,
    (∀ S, inSAT u S -> inSAT u' S) ->
    ∀ S, inSAT (App u v) S -> inSAT (App u' v) S.

The set of strongly normalizing terms

Parameter snSAT : SAT.
Parameter snSAT_intro : ∀ t, sn t -> inSAT t snSAT.

Non-depenent products

  Parameter prodSAT : SAT -> SAT -> SAT.
  Parameter prodSAT_morph : Proper (eqSAT ==> eqSAT ==> eqSAT) prodSAT.
  Parameter prodSAT_intro : ∀ A B m,
    (∀ v, inSAT v A -> inSAT (subst v m) B) ->
    inSAT (Abs m) (prodSAT A B).
  Parameter prodSAT_elim : ∀ A B u v,
    inSAT u (prodSAT A B) ->
    inSAT v A ->
    inSAT (App u v) B.

Intersection

  Parameter interSAT : ∀ A:Type, (A -> SAT) -> SAT.
  Parameter interSAT_morph : ∀ A A' (F:A->SAT) (G:A'->SAT),
    indexed_relation eqSAT F G ->
    eqSAT (interSAT F) (interSAT G).
  Parameter interSAT_intro : ∀ A F u,
    A ->
    (∀ x:A, inSAT u (F x)) ->
    inSAT u (interSAT F).
  Parameter interSAT_elim : ∀ A F u,
    inSAT u (interSAT F) ->
    ∀ x:A, inSAT u (F x).

End SAT.

Instantiating this signature with Girard's reducibility candidates

Require Import Can.

Module SatSet <: SAT.

  Definition SAT := {P:term->Prop|is_cand P}.
  Definition inSAT t (S:SAT) := proj1_sig S t.
  Definition eqSAT X Y := ∀ t, inSAT t X <-> inSAT t Y.
  Lemma eqSAT_def : ∀ X Y,
    eqSAT X Y <-> (∀ t, inSAT t X <-> inSAT t Y ).

  Instance inSAT_morph : Proper ((@eq term ) ==> eqSAT ==> iff) inSAT.
Qed.

  Definition inclSAT A B := ∀ t, inSAT t A -> inSAT t B.

  Global Instance inclSAT_ord : PreOrder inclSAT.

Qed.

  Lemma sat_sn : ∀ t S, inSAT t S -> sn t.

  Definition daimon := Ref 0.

  Lemma varSAT : ∀ S, inSAT daimon S.

  Lemma inSAT_exp : ∀ S u m,
    boccur 0 m = true \/ sn u ->
    inSAT (subst u m) S ->
    inSAT (App (Abs m) u) S.

  Lemma inSAT_context : ∀ u u' v,
    (∀ S, inSAT u S -> inSAT u' S) ->
    ∀ S, inSAT (App u v) S -> inSAT (App u' v) S.

  Definition snSAT : SAT := exist _ sn cand_sn.

  Lemma snSAT_intro : ∀ t, sn t -> inSAT t snSAT.

  Definition prodSAT (X Y:SAT) : SAT.
exists (Arr (proj1_sig X) (proj1_sig Y)).
Defined.

  Lemma prodSAT_intro : ∀ A B m,
    (∀ v, inSAT v A -> inSAT (subst v m) B) ->
    inSAT (Abs m) (prodSAT A B).

  Lemma prodSAT_elim : ∀ A B u v,
    inSAT u (prodSAT A B) ->
    inSAT v A ->
    inSAT (App u v) B.

  Instance prodSAT_morph : Proper (eqSAT ==> eqSAT ==> eqSAT) prodSAT.
Qed.

  Instance prodSAT_mono : Proper (inclSAT --> inclSAT ++> inclSAT) prodSAT.
Qed.

  Definition interSAT (A:Type) (F:A -> SAT) : SAT :=
    exist _ (Inter A (fun x => proj1_sig (F x)))
      (is_can_Inter _ _ (fun x => proj2_sig (F x))).

  Lemma interSAT_morph : ∀ A A' (F:A->SAT) (G:A'->SAT),
    indexed_relation eqSAT F G ->
    eqSAT (interSAT F) (interSAT G).

  Lemma interSAT_intro : ∀ A F u,
    A ->
    (∀ x:A, inSAT u (F x)) ->
    inSAT u (interSAT F).

Lemma interSAT_intro' : ∀ A (P:A->Prop) F t,
  sn t ->
  (∀ x, P x -> inSAT t (F x)) ->
  inSAT t (interSAT (fun p:sig P => F (proj1_sig p))).

  Lemma interSAT_elim : ∀ A F u,
    inSAT u (interSAT F) ->
    ∀ x:A, inSAT u (F x).

  Lemma interSAT_mono A (F G:A->SAT):
    (∀ x, inclSAT (F x) (G x)) ->
    inclSAT (interSAT F) (interSAT G).

End SatSet.

Export SatSet.

Derived facts

Instance eqSAT_equiv : Equivalence eqSAT.
Qed.

Lemma interSAT_morph_subset :
  ∀ A (P Q:A->Prop) (F:sig P->SAT) (G:sig Q->SAT),
  (∀ x, P x <-> Q x) ->
  (∀ x Px Qx,
   eqSAT (F (exist P x Px)) (G (exist Q x Qx))) ->
  eqSAT (interSAT F) (interSAT G).

  Lemma KSAT_intro : ∀ A t m,
    sn t ->
    inSAT m A ->
    inSAT (App2 K m t) A.

  Lemma SAT_daimon1 : ∀ S u,
    sn u ->
    inSAT (App daimon u) S.

Dependent product The realizability relation of a dependent product. It is the intersection of all reducibility candidates {x}F -> {f(x)}G(x) when x ranges A.

Definition piSAT0 A B (F:A->SAT) (G:A->B->SAT) (f:A->B) :=
  interSAT (fun x => prodSAT (F x) (G x (f x))).

Lemma piSAT0_intro : ∀ A B F G (f:A->B) t,
  sn t ->
  (∀ x u, inSAT u (F x) -> inSAT (App t u) (G x (f x))) ->
  inSAT t (piSAT0 F G f).

Lemma piSAT0_elim : ∀ A B F G (f:A->B) x t u,
  inSAT t (piSAT0 F G f) ->
  inSAT u (F x) ->
  inSAT (App t u) (G x (f x)).