Library Sat

Require Import Lambda.


Definition indexed_relation A A' B (R:B->B->Prop) (f:A->B) (g:A'->B) :=
  (forall x, exists y, R (f x) (g y)) /\
  (forall y, exists x, R (f x) (g y)).


Module Type SAT.
  Parameter SAT : Type.
  Parameter eqSAT : SAT -> SAT -> Prop.
  Parameter inSAT : term -> SAT -> Prop.
  Parameter eqSAT_def : forall X Y,
    eqSAT X Y <-> (forall t, inSAT t X <-> inSAT t Y).
  Parameter inSAT_morph : Proper ((@eq term) ==> eqSAT ==> iff) inSAT.

  Parameter sat_sn : forall t S, inSAT t S -> sn t.
  Parameter daimon : term.
  Parameter varSAT : forall S, inSAT daimon S.

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

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

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


End SAT.

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 := forall t, inSAT t X <-> inSAT t Y.
  Lemma eqSAT_def : forall X Y,
    eqSAT X Y <-> (forall t, inSAT t X <-> inSAT t Y).

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

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

  Definition daimon := Ref 0.

  Lemma varSAT : forall S, inSAT daimon S.

  Definition snSAT : SAT := exist _ sn cand_sn.

  Lemma snSAT_intro : forall t, sn t -> inSAT t snSAT.
  Definition prodSAT (X Y:SAT) : SAT.
Defined.

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

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

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

  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 : forall A A' (F:A->SAT) (G:A'->SAT),
    indexed_relation eqSAT F G ->
    eqSAT (interSAT F) (interSAT G).

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

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

End SatSet.

Export SatSet.

Instance eqSAT_equiv : Equivalence eqSAT.
Qed.

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

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