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