semantics.ord.prop
Require Import base
protype ordtype clat frame
mono adj cont.
Section PropOrder.
Implicit Types (P Q R : Prop).
Definition prop_le P Q := P -> Q.
Lemma prop_le_refl P : prop_le P P. by []. Qed.
Lemma prop_le_trans P Q R : prop_le P Q -> prop_le Q R -> prop_le P R.
Proof. rewrite/prop_le. tauto. Qed.
Canonical prop_proMixin := ProMixin prop_le_refl prop_le_trans.
Canonical prop_proType := Eval hnf in ProType Prop prop_proMixin.
Lemma prop_leE P Q : (P ≤ Q) = (P -> Q).
Proof. by []. Qed.
Lemma prop_le_eq P Q : P ≤ Q -> Q ≤ P -> P = Q.
Proof. move=> le_p_q le_q_p. exact: pext. Qed.
Canonical prop_ordMixin := OrdMixin prop_le_eq.
Canonical prop_ordType := Eval hnf in OrdType Prop prop_ordMixin.
Definition prop_inf I (F : I -> Prop) : Prop := forall i, F i.
Lemma prop_infP I (F : I -> Prop) : is_glb F (prop_inf F).
Proof. apply: mk_glb => [i|/=P h1 h2 i]. exact. exact: h1. Qed.
Canonical prop_clatMixin := CLatMixin prop_infP.
Canonical prop_clat := Eval hnf in CLat Prop prop_clatMixin.
Lemma prop_topE : ⊤ = True.
Proof. exact: top_def. Qed.
Lemma prop_botE : ⊥ = False.
Proof. exact: bot_def. Qed.
Lemma prop_joinE (P Q : Prop) : (P ∨ Q) = (P \/ Q).
Proof. apply: join_def; intros; hnf; intuition. Qed.
Lemma prop_meetE (P Q : Prop) : (P ∧ Q) = (P /\ Q).
Proof. apply: meet_def; intros; hnf; intuition. Qed.
Lemma prop_exE I (F : I -> Prop) : sup F = exists i, F i.
Proof.
apply: ex_def => [i|/=P h]; hnf. eauto. by case=> i /h.
Qed.
Lemma prop_allE I (F : I -> Prop) : inf F = forall i, F i.
Proof. by []. Qed.
Lemma prop_exEc I (P : I -> Prop) (F : I -> Prop) :
(∃ i | P i, F i) = exists2 i, P i & F i.
Proof.
rewrite prop_exE. apply: pext => [[i]|[i pi fi]].
rewrite/supguard prop_exE => -[pi fi]. by exists i.
exists i. rewrite/supguard prop_exE. by exists pi.
Qed.
Lemma prop_allEc I (P : I -> Prop) (F : I -> Prop) :
(∀ i | P i, F i) = (forall i, P i -> F i).
Proof.
rewrite prop_allE. apply: le_eq; hnf=> H i; [move: (H i)|];
rewrite/infguard prop_allE //. exact: H.
Qed.
Lemma prop_frameP I (F : I -> Prop) (P : Prop) :
P ∧ sup F ≤ ∃ i, P ∧ F i.
Proof.
rewrite prop_meetE prop_leE !prop_exE => -[p [i fi]].
exists i. rewrite prop_meetE. by split.
Qed.
Canonical prop_frameMixin := FrameMixin prop_frameP.
Canonical prop_frame := Eval hnf in Frame Prop prop_frameMixin.
Lemma prop_impE P Q : (P → Q) = (P -> Q).
Proof.
apply: imp_def. rewrite prop_meetE; hnf=> -[]. exact.
move=> /= R H; hnf=> r p. apply: H. rewrite prop_meetE. by split.
Qed.
End PropOrder.
Instance prop_impl_subrelation : subrelation (@ord_op prop_proType) Basics.impl.
Proof. by []. Qed.
Instance impl_prop_subrelation : subrelation Basics.impl (@ord_op prop_proType).
Proof. by []. Qed.
Section PurePropositions.
Variable (T : frame).
Implicit Types (P Q : Prop) (x y : T).
Definition pure P : T := ∃ (p : P), ⊤.
Notation "'⌈' P '⌉'" := (pure P) : ord_scope.
Lemma pureE P x : (P -> ⊤ ≤ x) -> ⌈ P ⌉ ≤ x.
Proof. move=> H. exact: exE. Qed.
Lemma pureI P x : P -> x ≤ ⌈ P ⌉.
Proof. move=> p. exact: exI. Qed.
Lemma pure_eq P : P -> ⌈ P ⌉ = ⊤.
Proof. move=> p. apply: le_eq. exact: topI. exact: pureI. Qed.
Global Instance pure_is_adjunction :
is_adjunction pure (ord_op ⊤).
Proof.
split=>[<-p|H]. exact: pureI. exact: pureE.
Qed.
Lemma pureT : ⌈ True ⌉ = ⊤.
Proof. apply: top_eq. exact: pureI. Qed.
Lemma pureM P Q : (⌈ P ⌉ ∧ ⌈ Q ⌉) = ⌈ P /\ Q ⌉.
Proof.
rewrite -prop_meetE. apply: le_eq; last by exact: monoM.
apply/impP. apply: pureE => p.
apply/impP. rewrite meetTx. apply: pureE => q.
apply: pureI. rewrite prop_meetE. by split.
Qed.
Global Instance pure_is_continuous :
is_continuous pure.
Proof.
apply: mk_is_continuous. by rewrite prop_topE pureT.
move=>/= P Q. by rewrite prop_meetE pureM.
Qed.
Lemma pureB : ⌈ False ⌉ = ⊥.
Proof. rewrite -prop_botE. exact: contB. Qed.
Lemma pureJ P Q : (⌈ P ⌉ ∨ ⌈ Q ⌉) = ⌈ P \/ Q ⌉.
Proof. by rewrite -prop_joinE contJ. Qed.
Lemma pureS I (P : I -> Prop) : (∃ i, ⌈ P i ⌉) = ⌈ exists i, P i ⌉.
Proof. by rewrite -prop_exE contE. Qed.
Lemma pureA I (P : I -> Prop) : ⌈ forall i, P i ⌉ ≤ (∀ i, ⌈ P i ⌉).
Proof. exact: monoA. Qed.
Lemma pureH P Q : ⌈ P -> Q ⌉ ≤ (⌈ P ⌉ → ⌈ Q ⌉).
Proof. rewrite -prop_impE. exact: contH. Qed.
Lemma pure_inf P x : (∀ (_ : P), x) = (⌈ P ⌉ → x).
Proof.
apply: le_eq. apply/impP. rewrite meetC. apply/impP. apply: pureE => p.
apply/impP. rewrite meetTx. apply: allE (p) le_refl. focus=> p.
rewrite pure_eq //. by rewrite impTx.
Qed.
Lemma pure_sup P x : (∃ (_ : P), x) = (⌈ P ⌉ ∧ x).
Proof.
apply: le_eq. focus=> p. exact: pureI. apply/impP.
apply: pureE => p. apply/impP. rewrite meetTx.
exact: exI (p) _.
Qed.
End PurePropositions.
Notation "'⌈' P '⌉'" := (@pure _ P) : ord_scope.
Section PropInitial.
Variables (X : frame) (f : Prop -> X).
Context {fP : is_continuous f}.
Lemma prop_initial :
f = (@pure X).
Proof.
fext=> P /=. apply: le_eq.
- apply/adjP => p. by rewrite pure_eq // adjT prop_topE.
- apply: pureE => p. have->: P = ⊤ by exact: top_eq. by rewrite contT.
Qed.
End PropInitial.
protype ordtype clat frame
mono adj cont.
Section PropOrder.
Implicit Types (P Q R : Prop).
Definition prop_le P Q := P -> Q.
Lemma prop_le_refl P : prop_le P P. by []. Qed.
Lemma prop_le_trans P Q R : prop_le P Q -> prop_le Q R -> prop_le P R.
Proof. rewrite/prop_le. tauto. Qed.
Canonical prop_proMixin := ProMixin prop_le_refl prop_le_trans.
Canonical prop_proType := Eval hnf in ProType Prop prop_proMixin.
Lemma prop_leE P Q : (P ≤ Q) = (P -> Q).
Proof. by []. Qed.
Lemma prop_le_eq P Q : P ≤ Q -> Q ≤ P -> P = Q.
Proof. move=> le_p_q le_q_p. exact: pext. Qed.
Canonical prop_ordMixin := OrdMixin prop_le_eq.
Canonical prop_ordType := Eval hnf in OrdType Prop prop_ordMixin.
Definition prop_inf I (F : I -> Prop) : Prop := forall i, F i.
Lemma prop_infP I (F : I -> Prop) : is_glb F (prop_inf F).
Proof. apply: mk_glb => [i|/=P h1 h2 i]. exact. exact: h1. Qed.
Canonical prop_clatMixin := CLatMixin prop_infP.
Canonical prop_clat := Eval hnf in CLat Prop prop_clatMixin.
Lemma prop_topE : ⊤ = True.
Proof. exact: top_def. Qed.
Lemma prop_botE : ⊥ = False.
Proof. exact: bot_def. Qed.
Lemma prop_joinE (P Q : Prop) : (P ∨ Q) = (P \/ Q).
Proof. apply: join_def; intros; hnf; intuition. Qed.
Lemma prop_meetE (P Q : Prop) : (P ∧ Q) = (P /\ Q).
Proof. apply: meet_def; intros; hnf; intuition. Qed.
Lemma prop_exE I (F : I -> Prop) : sup F = exists i, F i.
Proof.
apply: ex_def => [i|/=P h]; hnf. eauto. by case=> i /h.
Qed.
Lemma prop_allE I (F : I -> Prop) : inf F = forall i, F i.
Proof. by []. Qed.
Lemma prop_exEc I (P : I -> Prop) (F : I -> Prop) :
(∃ i | P i, F i) = exists2 i, P i & F i.
Proof.
rewrite prop_exE. apply: pext => [[i]|[i pi fi]].
rewrite/supguard prop_exE => -[pi fi]. by exists i.
exists i. rewrite/supguard prop_exE. by exists pi.
Qed.
Lemma prop_allEc I (P : I -> Prop) (F : I -> Prop) :
(∀ i | P i, F i) = (forall i, P i -> F i).
Proof.
rewrite prop_allE. apply: le_eq; hnf=> H i; [move: (H i)|];
rewrite/infguard prop_allE //. exact: H.
Qed.
Lemma prop_frameP I (F : I -> Prop) (P : Prop) :
P ∧ sup F ≤ ∃ i, P ∧ F i.
Proof.
rewrite prop_meetE prop_leE !prop_exE => -[p [i fi]].
exists i. rewrite prop_meetE. by split.
Qed.
Canonical prop_frameMixin := FrameMixin prop_frameP.
Canonical prop_frame := Eval hnf in Frame Prop prop_frameMixin.
Lemma prop_impE P Q : (P → Q) = (P -> Q).
Proof.
apply: imp_def. rewrite prop_meetE; hnf=> -[]. exact.
move=> /= R H; hnf=> r p. apply: H. rewrite prop_meetE. by split.
Qed.
End PropOrder.
Instance prop_impl_subrelation : subrelation (@ord_op prop_proType) Basics.impl.
Proof. by []. Qed.
Instance impl_prop_subrelation : subrelation Basics.impl (@ord_op prop_proType).
Proof. by []. Qed.
Section PurePropositions.
Variable (T : frame).
Implicit Types (P Q : Prop) (x y : T).
Definition pure P : T := ∃ (p : P), ⊤.
Notation "'⌈' P '⌉'" := (pure P) : ord_scope.
Lemma pureE P x : (P -> ⊤ ≤ x) -> ⌈ P ⌉ ≤ x.
Proof. move=> H. exact: exE. Qed.
Lemma pureI P x : P -> x ≤ ⌈ P ⌉.
Proof. move=> p. exact: exI. Qed.
Lemma pure_eq P : P -> ⌈ P ⌉ = ⊤.
Proof. move=> p. apply: le_eq. exact: topI. exact: pureI. Qed.
Global Instance pure_is_adjunction :
is_adjunction pure (ord_op ⊤).
Proof.
split=>[<-p|H]. exact: pureI. exact: pureE.
Qed.
Lemma pureT : ⌈ True ⌉ = ⊤.
Proof. apply: top_eq. exact: pureI. Qed.
Lemma pureM P Q : (⌈ P ⌉ ∧ ⌈ Q ⌉) = ⌈ P /\ Q ⌉.
Proof.
rewrite -prop_meetE. apply: le_eq; last by exact: monoM.
apply/impP. apply: pureE => p.
apply/impP. rewrite meetTx. apply: pureE => q.
apply: pureI. rewrite prop_meetE. by split.
Qed.
Global Instance pure_is_continuous :
is_continuous pure.
Proof.
apply: mk_is_continuous. by rewrite prop_topE pureT.
move=>/= P Q. by rewrite prop_meetE pureM.
Qed.
Lemma pureB : ⌈ False ⌉ = ⊥.
Proof. rewrite -prop_botE. exact: contB. Qed.
Lemma pureJ P Q : (⌈ P ⌉ ∨ ⌈ Q ⌉) = ⌈ P \/ Q ⌉.
Proof. by rewrite -prop_joinE contJ. Qed.
Lemma pureS I (P : I -> Prop) : (∃ i, ⌈ P i ⌉) = ⌈ exists i, P i ⌉.
Proof. by rewrite -prop_exE contE. Qed.
Lemma pureA I (P : I -> Prop) : ⌈ forall i, P i ⌉ ≤ (∀ i, ⌈ P i ⌉).
Proof. exact: monoA. Qed.
Lemma pureH P Q : ⌈ P -> Q ⌉ ≤ (⌈ P ⌉ → ⌈ Q ⌉).
Proof. rewrite -prop_impE. exact: contH. Qed.
Lemma pure_inf P x : (∀ (_ : P), x) = (⌈ P ⌉ → x).
Proof.
apply: le_eq. apply/impP. rewrite meetC. apply/impP. apply: pureE => p.
apply/impP. rewrite meetTx. apply: allE (p) le_refl. focus=> p.
rewrite pure_eq //. by rewrite impTx.
Qed.
Lemma pure_sup P x : (∃ (_ : P), x) = (⌈ P ⌉ ∧ x).
Proof.
apply: le_eq. focus=> p. exact: pureI. apply/impP.
apply: pureE => p. apply/impP. rewrite meetTx.
exact: exI (p) _.
Qed.
End PurePropositions.
Notation "'⌈' P '⌉'" := (@pure _ P) : ord_scope.
Section PropInitial.
Variables (X : frame) (f : Prop -> X).
Context {fP : is_continuous f}.
Lemma prop_initial :
f = (@pure X).
Proof.
fext=> P /=. apply: le_eq.
- apply/adjP => p. by rewrite pure_eq // adjT prop_topE.
- apply: pureE => p. have->: P = ⊤ by exact: top_eq. by rewrite contT.
Qed.
End PropInitial.