Skip to content
Snippets Groups Projects
Commit 74e1565e authored by Chloé Braud's avatar Chloé Braud
Browse files

Update slot_mereology.v (<chloe)

parent ac99d60e
Branches main
No related tags found
No related merge requests found
......@@ -16,12 +16,12 @@ Definition Os x y := exists z, Ps z x /\ Ps z y.
Definition PPs x y := Ps x y /\ ~ F y x.
(* Only Slots are Filled *)
Axiom only_slots_are_filled : forall x y,
F x y -> exists z, Ps y z.
Axiom only_slots_are_filled : forall a s,
F a s -> exists b, Ps s b.
(* Slots Cannot Fill *)
Axiom slots_cannot_fill : forall x y,
F x y -> ~exists z, Ps x z.
Axiom slots_cannot_fill : forall a s,
F a s -> ~exists b, Ps a b.
(* Slots Dont Have Slots *)
Axiom slots_dont_have_slots : forall x y,
......@@ -106,17 +106,17 @@ Axiom mutual_occupancy : forall x y z1 z2,
Axiom single_occupancy : forall x y,
Ps x y -> exists! z, F z x.
(* Single Owner *)
Lemma single_filler : forall s x,
F x s -> forall y, F y s -> x = y.
Proof.
intros s x Fxs y Fys.
pose proof (only_slots_are_filled x s Fxs) as (z & Pssz).
pose proof (single_occupancy s z Pssz) as (z' & Fz's & UniqueFs).
apply UniqueFs in Fys as ->.
apply UniqueFs in Fxs.
auto.
Qed.
Ltac unify_filler F1 F2 :=
let a := fresh "a" in
let Pssa := fresh "Pssa" in
let UniqueF := fresh "UniqueF" in
let a' := fresh "a'" in
pose proof (only_slots_are_filled _ _ F2) as (a & Pssa);
pose proof (single_occupancy _ _ Pssa) as (a' & _ & UniqueF);
apply UniqueF in F1 as eq1;
apply UniqueF in F2 as eq2;
symmetry in eq2;
subst; clear a Pssa UniqueF F2.
(* Parthood Transitivity *)
Theorem parthood_transitivity : forall x y z,
......@@ -182,9 +182,7 @@ Proof.
pose proof (Uc a Fac). subst.
pose proof (Uc b Fbc). subst.
apply nPba.
exists c; split.
apply Fbc.
apply Pscb.
exists c; split; assumption.
(* right to left *)
- intros [a [Psab nFba]].
pose proof (single_occupancy _ _ Psab) as [c [Fca Uc]].
......@@ -201,10 +199,18 @@ Proof.
Qed.
(* Slot Strong Supplementation *)
Axiom BA8 : forall x y,
(exists z, Ps z x) /\ (exists z, Ps z y) ->
((~exists z, Ps z x /\ F y z) ->
(exists z, Ps z y /\ ~Ps z x)).
Theorem BA8 : forall a b,
(exists s, Ps s a) /\ (exists t, Ps t b) ->
(~(exists u, Ps u a /\ F b u) ->
(exists v, Ps v b /\ ~Ps v a)).
Proof.
intros a b ((s & Pssa) & (t & Pstb)) nPba.
pose proof (whole_improper_slots b (ex_intro _ t (Pstb))) as (u & Psub & Fbu).
exists u; split; auto.
intros Psua.
destruct nPba.
exists u; split; assumption.
Qed.
(* Slot Weak Supplementation *)
Theorem BT13 : forall x y,
......@@ -239,292 +245,330 @@ Abort.
* *
**********************)
Definition S s := exists x, Ps s x.
(*******************
* Slot Definition *
*******************)
Definition S s := exists a, Ps s a.
Axiom single_owner : forall a b s, Ps s a -> Ps s b -> a = b.
(* Single Owner *)
Axiom single_owner : forall s x,
Ps s x -> forall y, Ps s y -> x = y.
Ltac unify_owner Ps1 Ps2 :=
pose proof (single_owner _ _ _ Ps2 Ps1);
subst; clear Ps2.
(* Anti-Inheritance *)
Theorem anti_inheritance : forall x y s t,
x <> y /\ Ps s y /\ F x s /\ Ps t x -> ~Ps t y.
Theorem anti_inheritance : forall a b s t,
a <> b -> Ps s b -> F a s -> Ps t a -> ~Ps t b.
Proof.
intros x y s t (x_neq_y & Pssy & Fxs & Pstx).
intro h.
apply x_neq_y.
apply single_owner with (s:=t); assumption.
intros a b s t a_neq_b Pssb Fas Psta h.
unify_owner Psta h.
contradiction.
Qed.
Definition IPs x y := Ps x y /\ F y x.
Definition IPs s a := Ps s a /\ F a s.
(* Slots are either proper or improper. *)
Theorem either_proper_or_improper : forall s,
S s -> exists x, PPs s x /\ ~ IPs s x \/ ~ PPs s x /\ IPs s x.
Lemma either_proper_or_improper : forall s,
S s -> exists a, PPs s a /\ ~ IPs s a \/ ~ PPs s a /\ IPs s a.
Proof.
intros s [x Pssx].
exists x.
destruct (classic (F x s)) as [Fxs|NFxs].
- right.
split.
+ intros [_ NFxs].
contradiction.
+ split; assumption.
- left.
split.
+ split; assumption.
+ intros [_ Fxs].
contradiction.
intros s (a & Pssa); exists a.
destruct (classic (F a s)) as [Fas|NFas];
[right|left]; split.
- intros [_ NFxs]; contradiction.
- split; assumption.
- split; assumption.
- intros [_ Fxs]; contradiction.
Qed.
(* Improper Slots are only owned by their Filler *)
Lemma unique_owner_improper_slot : forall x s,
IPs s x -> forall y, Ps s y -> x = y.
Lemma proper_part_in_proper_slot : forall a b,
PP b a <-> (exists s, PPs s a /\ F b s).
Proof.
intros x s [Pssx _].
apply single_owner.
assumption.
intros a b.
split.
- intros ((s & Fbs & Pssa) & nPab).
exists s; repeat split; auto.
intros Fas; destruct nPab.
unify_filler Fas Fbs.
apply BT9; exists s; assumption.
- intros (s & [Pssa nFas] & Fbs).
split.
exists s; split; auto.
intros Pab; destruct nFas.
assert (a = b) as <-.
apply BT8; split; auto.
split with (x:=s); split; auto.
assumption.
Qed.
(* *)
Theorem proper_part_in_proper_slot : forall x y,
PP y x -> (exists s, Ps s x /\ F y s /\ ~Ps s y).
Proof.
intros x y [[s [Fys Pssx]] nPxy].
exists s.
repeat split; try assumption.
intro Pssy.
destruct nPxy.
pose proof (single_owner s x Pssx) as UniqueSOwner.
apply UniqueSOwner in Pssy.
rewrite <- Pssy.
apply BT9.
exists s; assumption.
Qed.
(* Additional Improper Parthood Slots *)
Axiom filler_has_imp_slot : forall x s, F x s -> exists t, IPs t x.
Axiom filler_has_imp_slot : forall a s, F a s -> exists t, IPs t a.
(* General Conditional Reflexivity *)
Lemma general_conditional_refl : forall x s,
Ps s x \/ F x s -> P x x.
Lemma general_conditional_refl : forall a s,
Ps s a \/ F a s -> P a a.
Proof.
intros x s Ps_or_F.
intros a s Ps_or_F.
apply BT9.
destruct Ps_or_F as [Pssx|Fxs].
destruct Ps_or_F as [Pssa|Fas].
- exists s; assumption.
- pose proof (filler_has_imp_slot x s Fxs) as (t & Pstx & _).
- pose proof (filler_has_imp_slot a s Fas) as (t & Psta & _).
exists t; assumption.
Qed.
(* Only One Improper Slot per Filler *)
Axiom unique_improper_slot : forall x s t,
IPs s x -> IPs t x -> s = t.
Axiom unique_improper_slot : forall a s t,
IPs s a -> IPs t a -> s = t.
Ltac unify_improper_slot IPs1 IPs2 :=
pose proof (unique_improper_slot _ _ _ IPs2 IPs1);
subst; clear IPs2.
Theorem mutual_occupancy_is_slot_identity : forall s t x y,
Ps s y -> F x s -> Ps t x -> F y t -> s = t.
Theorem mutual_occupancy_is_slot_identity : forall a b s t,
Ps s b -> F a s -> Ps t a -> F b t -> s = t.
Proof.
intros s t x y Pssy Fxs Pstx Fyt.
pose proof (mutual_occupancy x y s t (conj (conj Pssy Fxs) (conj Pstx Fyt))) as <-.
apply unique_improper_slot with (x:=x); split; assumption.
intros a b s t Pssb Fas Psta Fbt.
pose proof (mutual_occupancy a b s t (conj (conj Pssb Fas) (conj Psta Fbt))) as <-.
apply unique_improper_slot with (a:=a); split; assumption.
Qed.
(***************
* Composition *
***************)
(*********************
* Contextualisation *
*********************)
Parameter C : Entity -> Entity -> Entity -> Prop.
Axiom compo_domains : forall u s t, C u s t -> S u /\ S s /\ S t.
Axiom context_domains : forall u s t, C u s t -> S u /\ S s /\ S t.
(* Composition Existence *)
Axiom composition_existence : forall s t x,
F x s -> Ps t x -> exists u, C u s t.
Definition Cb s t := exists a, F a t /\ Ps s a.
Axiom composition_constraints : forall s t u,
C u s t -> exists x, F x s /\ Ps t x.
Axiom context_existence : forall s t,
Cb t s -> exists u, C u s t.
(* Composition Unicity *)
Axiom composition_unicity : forall s t u v,
C u s t -> C v s t -> u = v.
Axiom context_constraints : forall s t u,
C u s t -> Cb t s.
Axiom compo_left_inject : forall s t u v,
C v s t -> C v s u -> t = u.
Axiom context_unicity : forall s t u v,
C u s t -> C v s t -> u = v.
Axiom compo_right_inject : forall s t u v x,
C v t s -> C v u s -> IPs s x -> t = u.
Ltac unify_context C1 C2 :=
pose proof (context_unicity _ _ _ _ C2 C1);
subst; clear C2.
Theorem symmetric_compositions_are_slot_identity :
Theorem symmetric_context_are_slot_identity :
forall s t u v, C u s t -> C v t s -> s = t.
Proof.
intros s t u v Cust Cvts.
pose proof (composition_constraints s t u Cust) as (x & Fxs & Pstx).
pose proof (composition_constraints t s v Cvts) as (y & Fyt & Pssy).
apply mutual_occupancy_is_slot_identity with (x:=x) (y:=y); assumption.
pose proof (context_constraints s t u Cust) as (a & Fas & Psta).
pose proof (context_constraints t s v Cvts) as (b & Fbt & Pssb).
apply mutual_occupancy_is_slot_identity with (a:=a) (b:=b); assumption.
Qed.
Axiom compo_asso_lr : forall a b c d e,
C a b c -> C b d e -> exists f, C a d f /\ C f e c.
Axiom context_left_inject : forall s t u v,
C v s t -> C v s u -> t = u.
Axiom compo_asso_rl : forall a c d e f,
C a d f -> C f e c -> exists b, C a b c /\ C b d e.
Axiom context_right_inject : forall s t u v a,
C v t s -> C v u s -> IPs s a -> t = u.
(* Composition Associativity *)
Theorem compo_asso_eq : forall s t u a b c d,
(C a s t -> C b a u -> C d s c -> C c t u -> b = d).
Proof.
intros s t u a b c d Cast Cbau Cdsc Cctu.
pose proof (compo_asso_lr b a u s t Cbau Cast) as (x & Cbsx & Cxtu).
pose proof (composition_unicity t u c x Cctu Cxtu) as <-.
apply composition_unicity with (s:=s) (t:=c); assumption.
Qed.
Axiom context_asso : forall s t u v,
(exists w, C v s w /\ C w t u) <-> (exists x, C v x u /\ C x s t).
Ltac context_asso s := apply context_asso; exists s; auto.
(* Improper-Improper Composition *)
(* Improper-Improper Contextualisation *)
(* v = s o s *)
(* u = (s o s) o t *)
Theorem imp_imp_composition : forall s a,
IPs s a -> C s s s.
Proof.
intros s a (Pssa & Fas).
pose proof (composition_existence s s a Fas Pssa) as (v & Cvss).
pose proof (compo_domains v s s Cvss) as [(b & Psvb) _].
pose proof (single_occupancy v b Psvb) as (c & Fcv & _).
clear Psvb b.
(* Proof of a = c *)
pose proof (filler_has_imp_slot c v Fcv) as (t & Pstc & Fct).
pose proof (composition_existence v t c Fcv Pstc) as (u & Cuvt).
pose proof (compo_asso_lr u v t s s Cuvt Cvss) as (d & Cusd & Cdst).
pose proof (composition_constraints s t d Cdst) as (y & Fys & Psty).
pose proof (single_occupancy s a Pssa) as (z & Fzs & FsUnique).
apply FsUnique in Fas as ->, Fys as <-.
clear FsUnique.
pose proof (single_owner t a Psty) as PstUnique.
apply PstUnique in Pstc as <-.
clear PstUnique.
pose proof (unique_improper_slot a s t (conj Pssa Fzs) (conj Psty Fct)) as <-.
(* Proof of a = b *)
pose proof (compo_asso_lr u v s s s Cuvt Cvss) as (v' & Cusv' & Cv'ss).
pose proof (composition_unicity s s v v' Cvss Cv'ss) as <-.
pose proof (symmetric_compositions_are_slot_identity s v u u Cusv' Cuvt) as <-.
assumption.
Qed.
Theorem imp_imp_compo_rev : forall s,
C s s s -> exists x, IPs s x.
Proof.
intros s Csss.
pose proof (composition_constraints s s s Csss) as (x & Fxs & Pssx).
exists x; split; assumption.
Theorem imp_imp_context : forall s,
(exists a, IPs s a) <-> C s s s.
Proof.
intros s; split.
+ intros (a & Pssa & Fas).
pose proof (context_existence s s (ex_intro _ a (conj Fas Pssa))) as (v & Cvss).
pose proof (context_domains v s s Cvss) as [(b & Psvb) _].
pose proof (single_occupancy v b Psvb) as (c & Fcv & _).
clear Psvb b.
(* Proof of a = c *)
pose proof (filler_has_imp_slot c v Fcv) as (t & Pstc & Fct).
pose proof (context_existence v t (ex_intro _ _ (conj Fcv Pstc))) as (u & Cuvt).
assert (exists d, C u s d /\ C d s t) as (d & Cust & Cdst).
context_asso v.
pose proof (context_constraints s t d Cdst) as (y & Fys & Psty).
unify_filler Fas Fys.
unify_owner Psty Pstc.
pose proof (unique_improper_slot a s t (conj Pssa Fas) (conj Psty Fct)) as <-.
(* Proof of a = b *)
assert (exists v', C u s v' /\ C v' s s) as (v' & Cusv' & Cv'ss).
context_asso v.
unify_context Cvss Cv'ss.
pose proof (symmetric_context_are_slot_identity s v u u Cusv' Cuvt) as <-.
assumption.
+ intros Csss.
pose proof (context_constraints _ _ _ Csss) as (a & Fas & Pssa).
exists a; split; auto.
Qed.
(* Proper-Improper Composition *)
Theorem right_imp_composition : forall s t x,
IPs s x -> F x t -> C t t s.
Theorem right_imp_composition : forall s t a,
IPs s a -> F a t -> C t t s.
Proof.
intros s t x (Pssx & Fxs) Fxt.
pose proof (imp_imp_composition s x (conj Pssx Fxs)) as Csss.
pose proof (composition_existence t s x Fxt Pssx) as (u & Cuts).
pose proof (compo_asso_rl u s t s s Cuts Csss) as (v & Cuvs & Cvts).
pose proof (composition_unicity t s u v Cuts Cvts) as <-.
pose proof (composition_constraints u s u Cuvs) as (y & Fyu & Pssy).
pose proof (single_owner s x Pssx y Pssy) as <-.
pose proof (compo_right_inject s t u u x Cuts Cuvs (conj Pssx Fxs)) as <-.
assert (Csss: C s s s). apply imp_imp_context; exists x; split; auto.
pose proof (context_existence t s (ex_intro _ _ (conj Fxt Pssx))) as (u & Cuts).
assert (exists v, C u v s /\ C v t s) as (v & Cuvs & Cvts). context_asso s.
unify_context Cuts Cvts.
pose proof (context_constraints u s u Cuvs) as (y & Fyu & Pssy).
unify_owner Pssx Pssy.
pose proof (context_right_inject s t u u x Cuts Cuvs (conj Pssx Fxs)) as <-.
assumption.
Qed.
(* Improper-Proper Composition *)
Theorem left_imp_composition : forall s t x,
IPs s x -> Ps t x -> C t s t.
Theorem left_imp_composition : forall s t a,
IPs s a -> Ps t a -> C t s t.
Proof.
intros s t x (Pssx & Fxs) Pstx.
pose proof (imp_imp_composition s x (conj Pssx Fxs)) as Csss.
pose proof (composition_existence s t x Fxs Pstx) as (u & Cust).
pose proof (compo_asso_lr u s t s s Cust Csss) as (v & Cusv & Cvst).
pose proof (composition_unicity s t u v Cust Cvst) as <-.
pose proof (compo_left_inject s t u u Cust Cusv) as <-.
assert (Csss : C s s s). apply imp_imp_context; exists x; split; auto.
pose proof (context_existence s t (ex_intro _ _ (conj Fxs Pstx))) as (u & Cust).
assert (exists v, C u s v /\ C v s t) as (v & Cusv & Cvst). context_asso s.
pose proof (context_unicity s t u v Cust Cvst) as <-.
pose proof (context_left_inject s t u u Cust Cusv) as <-.
assumption.
Qed.
Lemma mutual_context_are_identity : forall s t u v,
C s t u -> C t s v -> s = t.
Proof.
intros s t u v Cstu Ctsv.
assert (exists x, C s s x /\ C x v u) as (x & Cssx & Cxvu).
context_asso t.
assert (exists y, C t t y /\ C y u v) as (y & Cttx & Cyuv).
context_asso s.
pose proof (symmetric_context_are_slot_identity v u x y Cxvu Cyuv) as ->.
pose proof (context_constraints u u y Cyuv) as (z & Fzu & Psuz).
assert (Cuuu: C u u u). apply imp_imp_context; exists z; split; auto.
unify_context Cuuu Cyuv.
unify_context Cxvu Cuuu.
unify_context Ctsv Cssx.
reflexivity.
Qed.
Definition SO s t := exists x, Ps s x /\ Ps t x.
Theorem composition_same_owner : forall u s t,
C u s t -> exists x, Ps u x /\ Ps s x.
Lemma SO_refl : forall s, S s -> SO s s.
Proof.
intros s (x & Pssx).
exists x; split; auto.
Qed.
Lemma SO_symm : forall s t, SO s t -> SO t s.
Proof.
intros s t (x & Pssx & Pstx).
exists x; split; auto.
Qed.
Lemma SO_trans : forall s t u, SO s t -> SO t u -> SO s u.
Proof.
intros s t u (x & Pssx & Pstx) (y & Psty & Psuy).
unify_owner Pstx Psty.
exists x; split; auto.
Qed.
Theorem context_same_owner : forall u s t,
C u s t -> SO u s.
Proof.
intros u s t Cust.
pose proof (compo_domains u s t Cust) as ([x Psux] & _).
pose proof (context_domains u s t Cust) as ([x Psux] & _).
exists x.
split; trivial.
pose proof (whole_improper_slots x) as (v & Psvx & Fxv).
exists u; assumption.
pose proof (left_imp_composition v u x (conj Psvx Fxv) Psux) as Cuvu.
pose proof (compo_asso_rl u t v s u Cuvu Cust) as [z []].
pose proof (composition_constraints v s z H0) as [x0 [Fx0v Pssx0]].
pose proof (single_occupancy v x Psvx) as [v' [_ eq]].
apply eq in Fxv as ->, Fx0v as <-.
assert (exists z, C u z t /\ C z v s) as (z & _ & Czvs).
context_asso u.
pose proof (context_constraints v s z Czvs) as (x0 & Fx0v & Pssx0).
unify_filler Fxv Fx0v.
assumption.
Qed.
(* Same Filler *)
Theorem composition_same_filler : forall u s t,
C u s t -> exists x, F x u /\ F x t.
Theorem context_same_filler : forall u s t,
C u s t -> exists a, F a u /\ F a t.
Proof.
intros u s t Cust.
pose proof (compo_domains u s t Cust) as ([x Psux] & _ & [z Pstz]).
pose proof (context_domains u s t Cust) as ([x Psux] & _ & [z Pstz]).
pose proof (single_occupancy t z Pstz) as (a & Fat & _).
clear z Pstz.
exists a; split; trivial.
pose proof (filler_has_imp_slot a t Fat) as (v & Psva & _).
pose proof (composition_existence t v a Fat Psva) as (u' & Cu'tv).
pose proof (composition_constraints s t u Cust) as (z & Fzs & Pstz).
pose proof (composition_same_owner u' t v Cu'tv) as (z' & Psu'z' & Pstz').
pose proof (single_owner t z Pstz) as PstUnique.
apply PstUnique in Pstz' as <-.
clear PstUnique.
pose proof (context_existence t v (ex_intro _ _ (conj Fat Psva))) as (u' & Cu'tv).
pose proof (context_constraints s t u Cust) as (z & Fzs & Pstz).
pose proof (context_same_owner u' t v Cu'tv) as (z' & Psu'z' & Pstz').
unify_owner Pstz Pstz'.
rename Psu'z' into Psu'z.
pose proof (composition_existence s u' z Fzs Psu'z) as (w & Cwsu').
pose proof (compo_asso_rl w v s t u' Cwsu' Cu'tv) as (w' & Cww'v & Cw'st).
pose proof (composition_unicity s t u w' Cust Cw'st) as <-.
rename Cww'v into Cwuv.
pose proof (composition_constraints u v w Cwuv) as (a' & Fa'u & Psva').
pose proof (single_owner v a Psva a' Psva') as <-.
pose proof (context_existence s u' (ex_intro _ _ (conj Fzs Psu'z))) as (w & Cwsu').
assert (exists w', C w w' v /\ C w' s t) as (w' & Cww'v & Cw'st).
context_asso u'.
unify_context Cust Cw'st.
pose proof (context_constraints u v w Cww'v) as (a' & Fa'u & Psva').
unify_owner Psva Psva'.
assumption.
Qed.
Theorem right_imp_composition_rev : forall s t,
C t t s -> exists x, IPs s x /\ F x t.
(* BT7 *)
Theorem parthood_transitivity_2 : forall a b c,
P a b -> P b c -> P a c.
Proof.
intros a b c (s & Fas & Pssb) (t & Fbt & Pstc).
pose proof (context_existence t s (ex_intro _ _ (conj Fbt Pssb))) as (u & Cuts).
exists u.
pose proof (context_same_filler _ _ _ Cuts) as (d & Fdu & Fds).
unify_filler Fas Fds.
pose proof (context_same_owner _ _ _ Cuts) as (d & Psud & Pstd).
unify_owner Pstc Pstd.
split; auto.
Qed.
Theorem right_imp_context_rev : forall s t,
C t t s -> exists a, IPs s a /\ F a t.
Proof.
intros s t Ctts.
pose proof (composition_constraints t s t Ctts) as (x & Fxt & Pssx).
pose proof (context_constraints t s t Ctts) as (x & Fxt & Pssx).
exists x; repeat split; trivial.
pose proof (composition_same_filler t t s Ctts) as (y & Fyt & Fys).
pose proof (compo_domains t t s Ctts) as ((z & Pstz) & _).
pose proof (single_occupancy t z Pstz) as (a & Fat & FtUnique).
apply FtUnique in Fxt as ->, Fyt as <-.
pose proof (context_same_filler t t s Ctts) as (y & Fyt & Fys).
pose proof (context_domains t t s Ctts) as ((z & Pstz) & _).
unify_filler Fxt Fyt.
assumption.
Qed.
Theorem imp_pro_compo_rev : forall s t,
C t s t -> exists x, IPs s x /\ Ps t x.
C t s t -> exists a, IPs s a /\ Ps t a.
Proof.
intros s t Ctst.
pose proof (composition_constraints s t t Ctst) as (x & Fxs & Pstx).
pose proof (context_constraints s t t Ctst) as (x & Fxs & Pstx).
exists x; repeat split; trivial.
pose proof (composition_same_owner t s t Ctst) as (y & Psty & Pssy).
pose proof (single_owner t x Pstx y Psty) as <-.
pose proof (context_same_owner t s t Ctst) as (y & Psty & Pssy).
unify_owner Pstx Psty.
assumption.
Qed.
Lemma mutual_compositions_are_identity : forall s t u v,
C s t u -> C t s v -> s = t.
Theorem compo_stability : forall s t v s' t',
C s' v s -> C t' v t -> (forall u, C s t u <-> C s' t' u).
Proof.
intros s t u v Cstu Ctsv.
pose proof (compo_asso_lr s t u s v Cstu Ctsv) as (x & Cssx & Cxvu).
pose proof (compo_asso_lr t s v t u Ctsv Cstu) as (y & Cttx & Cyuv).
pose proof (symmetric_compositions_are_slot_identity v u x y Cxvu Cyuv) as ->.
pose proof (composition_unicity s t).
pose proof (composition_constraints u u y Cyuv) as (z & Fzu & Psuz).
pose proof (imp_imp_composition u z (conj Psuz Fzu)) as Cuuu.
pose proof (composition_unicity u u u y Cuuu Cyuv) as <-.
apply composition_unicity with (s:=t) (t:=u); assumption.
intros s t v s' t' Cs'vs Ct'vt u.
split.
- intros Cstu.
assert (exists u', C u' t' u) as (u' & Cu't'u).
{ pose proof (context_constraints _ _ _ Cstu) as (x & Fxt & Psux).
apply context_existence; exists x; split; auto.
pose proof (context_same_filler _ _ _ Ct'vt) as (y & Fyt' & Fyt).
unify_filler Fxt Fyt; auto.
}
enough (s' = u') as <-; auto.
assert (exists w, C u' v w /\ C w t u) as (w & Cu'vw & Cwtu).
context_asso t'.
unify_context Cstu Cwtu.
unify_context Cs'vs Cu'vw.
reflexivity.
- intros Cs't'u.
assert (exists w, C s' v w /\ C w t u) as (w & Cs'vw & Cwtu).
context_asso t'.
pose proof (context_left_inject _ _ _ _ Cs'vs Cs'vw) as <-.
auto.
Qed.
(****************
......@@ -536,7 +580,7 @@ Definition PoS s t := exists u, C s t u.
Lemma pos_domains : forall s t, PoS s t -> S s /\ S t.
Proof.
intros s t [u Cstu].
pose proof (compo_domains s t u Cstu) as (Ss & St & _).
pose proof (context_domains s t u Cstu) as (Ss & St & _).
split; assumption.
Qed.
......@@ -545,7 +589,7 @@ Theorem conditional_pos_refl : forall s, S s -> PoS s s.
Proof.
intros s (x & Pssx).
unfold PoS.
pose proof (single_occupancy s x Pssx) as (z & Fzs & UniqueFzs).
pose proof (single_occupancy s x Pssx) as (z & Fzs & _).
pose proof (general_conditional_refl z s) as [].
right.
assumption.
......@@ -563,7 +607,7 @@ Theorem pos_antisym : forall s t,
PoS s t -> PoS t s -> s = t.
Proof.
intros s t [u Cstu] [v Ctsv].
apply mutual_compositions_are_identity with (u:=u) (v:=v); assumption.
apply mutual_context_are_identity with (u:=u) (v:=v); assumption.
Qed.
(* PoS Transitivity *)
......@@ -571,82 +615,62 @@ Theorem pos_trans : forall s t u,
PoS s t -> PoS t u -> PoS s u.
Proof.
intros s t u [v Cstv] [w Ctuw]; move w before v.
pose proof (compo_asso_lr s t v u w Cstv Ctuw) as (x & Csux & _).
assert (exists x, C s u x /\ C x w v) as (x & Csux & _).
context_asso t.
exists x; assumption.
Qed.
Theorem pos_same_owner : forall s t,
PoS s t -> exists x, Ps s x /\ Ps t x.
PoS s t -> SO s t.
Proof.
intros s t [u Cstu].
apply composition_same_owner with (u:=s) (s:=t) (t:=u).
apply context_same_owner with (u:=s) (s:=t) (t:=u).
assumption.
Qed.
Lemma slots_are_parts_of_imp_slot : forall a s t,
IPs s a -> Ps t a -> PoS t s.
Theorem ips_eq : forall a s, IPs s a -> (forall t, Ps t a <-> PoS t s).
Proof.
intros a s t IPssa Psta.
exists t.
apply left_imp_composition with (x:=a); assumption.
Qed.
(* *)
Theorem slots_constrain_fillers : forall a b s t,
F b t /\ F a s /\ PoS t s -> P b a.
Proof.
intros a b s t [Fbt [Fas [u Ctsu]]].
pose proof (composition_constraints s u t Ctsu) as [a' [H H0]].
pose proof (composition_same_owner t s u Ctsu) as [z [Pstz Pssz]].
pose proof (single_occupancy s z Pssz) as [a'' [H1 H2]].
apply H2 in Fas as a''_eq_a, H as a''_eq_a'.
rewrite a''_eq_a in a''_eq_a'.
rewrite <- a''_eq_a' in H0.
clear a''_eq_a a''_eq_a' H1 H2 H a'' a'.
pose proof (composition_same_filler t s u Ctsu) as [x [H H1]].
pose proof (single_occupancy t z Pstz) as [x0 [H2 H3]].
apply H3 in Fbt as x0_eq_b, H as x0_eq_x.
rewrite x0_eq_x in x0_eq_b.
rewrite x0_eq_b in H1.
clear H2 H3 x0_eq_b x0_eq_x H.
unfold P.
exists u.
split; assumption.
intros a s.
intros IPssa t; split.
intros Psta; exists t; apply left_imp_composition with (a:=a); assumption.
intros PoSts; destruct IPssa as (Pssa & Fas).
pose proof (pos_same_owner _ _ PoSts) as (b & H & H1);
unify_owner Pssa H1; assumption.
Qed.
(* *)
Theorem fillers_constrain_slots : forall a b s,
P b a -> IPs s a -> exists t, F b t /\ PoS t s.
Theorem slots_constrain_fillers : forall a b,
(exists s t, F b t /\ F a s /\ PoS t s) <-> P b a.
Proof.
intros a b s (t & Fbt & Psta) (PSsa & Fas).
exists t.
split; trivial.
exists t.
apply left_imp_composition with (x:=a); trivial.
split; trivial.
intros a b; split.
+ intros (s & t & Fbt & Fas & [u Ctsu]).
pose proof (context_constraints s u t Ctsu) as (a' & Fa's & Psua).
unify_filler Fas Fa's.
pose proof (context_same_filler t s u Ctsu) as (b' & Fb't & Fb'u).
unify_filler Fbt Fb't.
exists u; split; auto.
+ intros (t & Fbt & Psta).
pose proof (whole_improper_slots a) as (s & Pssa & Fas).
{ exists t; auto. }
exists s, t; repeat split; auto.
exists t.
apply left_imp_composition with (a:=a); auto.
split; auto.
Qed.
(* PoS is stable under composition. *)
Theorem pos_stability : forall s t u v w,
C v s t -> C w s u -> (PoS u t <-> PoS w v).
Theorem pos_stability : forall s t u t' u',
C t' s t -> C u' s u -> (PoS u t <-> PoS u' t').
Proof.
intros s t u v w Cvst Cwsu.
intros s t u t' u' Ct'st Cu'su.
pose proof (compo_stability _ _ _ _ _ Cu'su Ct'st).
unfold PoS.
split.
(* Left-to-right *)
- intros (u' & Cutu').
exists u'.
pose proof (compo_asso_rl w u' s t u Cwsu Cutu') as (x & Cwxu' & Cxst).
pose proof (composition_unicity s t v x Cvst Cxst) as <-.
assumption.
(* Right-to-left *)
- intros (w' & Cwvw').
exists w'.
pose proof (compo_asso_lr w v w' s t Cwvw' Cvst) as (x & Cwsx & Cxtw).
pose proof (compo_left_inject s u x w Cwsu Cwsx) as <-.
assumption.
setoid_rewrite H.
reflexivity.
Qed.
(***************
* Proper Part *
***************)
Definition PPoS s t := PoS s t /\ s <> t.
Theorem ppos_irrefl : forall s, ~ PPoS s s.
......@@ -675,34 +699,85 @@ Proof.
contradiction.
Qed.
Theorem ppos_same_owner: forall s t, PPoS s t -> SO s t.
Proof.
intros s t [H _].
apply pos_same_owner; auto.
Qed.
Theorem proper_slots_are_parts_of_imp_slot :
forall s t x, IPs s x -> PPs t x -> PPoS t s.
Theorem proper_slots_iff_parts_of_imp_slot :
forall s a, IPs s a -> (forall t, PPs t a <-> PPoS t s).
Proof.
intros s t x IPssx [Pstx NFxt].
intros s a IPssa t.
pose proof (ips_eq a s IPssa).
unfold PPs, PPoS.
rewrite <- H.
destruct IPssa as (Pssa & Fas).
split.
exists t.
apply left_imp_composition with (x:=x); assumption.
intros ->.
destruct IPssx.
contradiction.
+ intros (Psta & nFat); split; auto.
intros ->; contradiction.
+ intros (Psta & t_neq_s); split; auto.
intros Fat.
assert (IPssa: IPs s a) by (split; auto).
assert (IPsta: IPs t a) by (split; auto).
unify_improper_slot IPssa IPsta.
contradiction.
Qed.
Theorem slots_constrain_fillers_ppos : forall a b,
(exists s t, F b t /\ F a s /\ PPoS t s) <-> PP b a.
Proof.
intros a b; split.
+ intros (s & t & Fbt & Fas & (PoSts & t_neq_s)).
assert (Pba: P b a) by (apply slots_constrain_fillers; exists s, t; auto).
split; auto.
intros Pab.
pose proof (BT8 a b (conj Pab Pba)) as <-.
destruct PoSts as (u & Ctsu).
pose proof (context_constraints _ _ _ Ctsu) as (c & Fcs & Psua).
unify_filler Fas Fcs.
pose proof (context_same_filler _ _ _ Ctsu) as (c & Fct & Fau).
unify_filler Fbt Fct.
assert (IPsua: IPs u a) by (split; auto).
pose proof (right_imp_composition u s a IPsua Fas) as Cssu.
unify_context Ctsu Cssu.
contradiction.
+ intros (Pba & nPab).
apply slots_constrain_fillers in Pba as (s & t & Fbt & Fas & PoSts).
exists s, t; repeat split; auto.
intros ->.
unify_filler Fas Fbt.
destruct nPab.
apply BT9.
pose proof (filler_has_imp_slot _ _ Fas) as (t & Psta & _).
exists t; auto.
Qed.
(* PPoS is stable under composition. *)
Theorem ppos_stability : forall s t u v w,
PPoS u t -> C v s t -> C w s u -> PPoS w v.
C v s t -> C w s u -> (PPoS u t <-> PPoS w v).
Proof.
intros s t u v w [(u' & Cutu') u_neq_t] Cvst Cwsu.
unfold PPoS.
intros s t u v w Cvst Cwsu.
split.
exists u'.
pose proof (compo_asso_rl w u' s t u Cwsu Cutu') as (x & Cwxu' & Cxst).
pose proof (composition_unicity s t v x Cvst Cxst) as <-.
assumption.
intro h.
rewrite h in Cwsu.
pose proof (compo_left_inject s t u v Cvst Cwsu).
intuition.
- intros [(u' & Cutu') u_neq_t].
unfold PPoS.
split.
exists u'.
assert (exists x, C w x u' /\ C x s t) as (x & Cwxu' & Cxst).
context_asso u.
pose proof (context_unicity s t v x Cvst Cxst) as <-.
assumption.
intro h.
rewrite h in Cwsu.
pose proof (context_left_inject s t u v Cvst Cwsu).
intuition.
- intros [].
split.
pose proof (pos_stability s t u v w Cvst Cwsu) as ut_eq_wv.
+ apply ut_eq_wv; assumption.
+ intros ->.
apply H0.
apply context_unicity with (s:=s) (t:=t); assumption.
Qed.
(********************
......@@ -712,12 +787,9 @@ Qed.
Definition OoS s t := exists u, PoS u s /\ PoS u t.
(* Conditional OoS Reflexivity *)
Theorem cond_oos_refl : forall s,
S s -> OoS s s.
Theorem cond_oos_refl : forall s, S s -> OoS s s.
Proof.
intros s Ss.
unfold OoS.
exists s.
intros s Ss; exists s.
pose proof (conditional_pos_refl s Ss).
split; assumption.
Qed.
......@@ -734,24 +806,15 @@ Proof.
assumption.
Qed.
Corollary oos_comm : forall s t,
OoS s t <-> OoS t s.
Proof.
split; apply oos_symmetry.
Qed.
(* OoS Same Owner *)
Theorem oos_same_owner : forall s t,
OoS s t -> (exists x, Ps s x /\ Ps t x).
OoS s t -> SO s t.
Proof.
intros s t [x [PoSxs PoSxt]].
apply pos_same_owner in PoSxs as [sOwner []].
apply pos_same_owner in PoSxt as [tOwner []].
pose proof (single_owner x sOwner H).
apply H3 in H1.
rewrite <- H1 in H2.
exists sOwner.
split; assumption.
unify_owner H H1.
exists sOwner; split; assumption.
Qed.
Lemma part_overlap_implies_whole_overlap: forall s t u,
......@@ -763,18 +826,18 @@ Proof.
Qed.
Theorem slots_overlap_with_imp_slot :
forall s t x, IPs s x -> Ps t x -> OoS s t.
forall s t a, IPs s a -> Ps t a -> OoS s t.
Proof.
intros s t x IPssx Pstx.
unfold OoS, PoS.
exists t.
split.
- exists t.
apply left_imp_composition with (x:=x) ; assumption.
apply left_imp_composition with (a:=x) ; assumption.
- pose proof (single_occupancy t x Pstx) as [y [Fyt _]].
pose proof (filler_has_imp_slot y t Fyt) as [u IPsuy].
exists u.
apply right_imp_composition with (x:=y); assumption.
apply right_imp_composition with (a:=y); assumption.
Qed.
Theorem pos_implies_overlap :
......@@ -789,36 +852,43 @@ Qed.
(* Overlap is stable under composition. *)
(* OoS t u <-> OoS (s o t) (s o u) *)
Lemma oos_stability : forall s t u v w,
C v s t -> C w s u -> (OoS t u <-> OoS v w).
Lemma oos_stability : forall s t u t' u',
C t' s t -> C u' s u -> (OoS t u <-> OoS t' u').
Proof.
intros s t u v w Cvst Cwsu.
intros s t u t' u' Ct'st Cu'su.
split.
(* Left-to-right *)
- intros (q & PoSqt & PoSqu).
- intros (v & PoSvt & PoSvu).
unfold OoS.
pose proof (composition_constraints s t v Cvst) as (x & Fxs & Pstx).
pose proof (pos_same_owner q t PoSqt) as (y & Psqy & Psty).
pose proof (single_owner t x Pstx) as UniquePst.
apply UniquePst in Psty as <-.
rename Psqy into Psqx.
clear UniquePst.
pose proof (composition_existence s q x Fxs Psqx) as (q' & Cq'sq).
exists q'.
pose proof (context_constraints s t t' Ct'st) as (a & Fas & Psta).
pose proof (pos_same_owner v t PoSvt) as (b & Psva & Pstb).
unify_owner Psta Pstb.
pose proof (context_existence s v (ex_intro _ _ (conj Fas Psva))) as (v' & Cv'sv).
exists v'.
split.
pose proof (pos_stability s t q v q' Cvst Cq'sq) as [Hstab _].
pose proof (pos_stability s t v t' v' Ct'st Cv'sv) as [Hstab _].
apply Hstab; assumption.
pose proof (pos_stability s u q w q' Cwsu Cq'sq) as [Hstab _].
pose proof (pos_stability s u v u' v' Cu'su Cv'sv) as [Hstab _].
apply Hstab; assumption.
- intros (x & PoSxv & PoSxw).
destruct PoSxv as (v' & Cxvv').
destruct PoSxw as (w' & Cxww').
pose proof (compo_asso_lr x v v' s t Cxvv' Cvst) as (x' & Cxsx' & Cx'tv').
pose proof (compo_asso_lr x w w' s u Cxww' Cwsu) as (x'' & Cxsx'' & Cx'uw').
pose proof (compo_left_inject s x' x'' x Cxsx' Cxsx'') as <-.
clear Cxsx''.
exists x'.
split; [exists v'|exists w']; assumption.
- intros (v' & (vt & Cv't'vt) & (vu & Cv'u'vu)).
assert (exists v, C v' s v /\ C v t vt) as (v1 & Cv'sv1 & Cv1tvt).
context_asso t'.
assert (exists v, C v' s v /\ C v u vu) as (v2 & Cv'sv2 & Cv2uvu).
context_asso u'.
pose proof (context_left_inject _ _ _ _ Cv'sv1 Cv'sv2) as <-.
clear Cv'sv2.
exists v1.
split; [exists vt|exists vu]; assumption.
Qed.
Theorem oos_constrains_o: forall a b s t,
OoS s t -> F a s -> F b t -> O a b.
Proof.
intros a b s t (u & PoSus & PoSut) Fas Fbt.
pose proof (pos_domains _ _ PoSus) as ((d & Psud) & _).
pose proof (single_occupancy _ _ Psud) as (c & Fcu & _).
exists c; split; apply slots_constrain_fillers;
[ exists s, u | exists t, u]; auto.
Qed.
(*******************
......@@ -826,70 +896,38 @@ Qed.
*******************)
Axiom slot_strong_supp : forall s t,
~ PoS t s -> exists u, PoS u t /\ ~ OoS u s.
S s -> S t -> (~ PoS t s -> exists u, PoS u t /\ ~ OoS u s).
Theorem slot_weak_supp : forall s t,
PPoS s t -> exists u, PoS u t /\ ~ OoS u s.
Proof.
intros s t [].
apply slot_strong_supp.
pose proof (pos_domains _ _ H) as (Ss & St).
apply slot_strong_supp; auto.
intro h.
pose proof (pos_antisym s t H h).
contradiction.
Qed.
Theorem slot_company : forall s t,
PPoS s t -> exists u, PPoS u t /\ u <> s.
Proof.
intros s t [PoSst s_neq_t].
pose proof (slot_weak_supp s t (conj PoSst s_neq_t)) as (u & PoSut & NOus).
pose proof (pos_same_owner s t PoSst) as (x & H2 & _).
exists u.
repeat split; trivial;
intros ->; apply NOus.
apply oos_symmetry, pos_implies_overlap; assumption.
pose proof (conditional_pos_refl s) as [].
exists x; assumption.
exists s; split; trivial; exists x0; assumption.
Qed.
Theorem slot_strong_company : forall s t,
PPoS s t -> exists u, PPoS u t /\ ~PoS u s.
Proof.
intros s t [PoSst s_neq_t].
pose proof (slot_weak_supp s t (conj PoSst s_neq_t)) as (u & PoSut & NOus).
exists u.
split.
- split; trivial.
intros ->.
apply NOus.
apply oos_symmetry, pos_implies_overlap.
assumption.
- intros PoSus.
apply NOus.
apply pos_implies_overlap.
assumption.
Qed.
Theorem oos_extensionality:
forall s t, S s -> S t -> (forall u, OoS s u <-> OoS t u) -> s = t.
Proof.
intros s t _ _ s_eq_t.
intros s t Ss St s_eq_t.
apply NNPP.
intro s_ne_t.
assert (~ PoS t s) as NPoSts.
{ intros PoSts.
destruct (slot_weak_supp t s) as (u & PoSus & NOoSut). split; congruence.
apply NOoSut.
rewrite oos_comm.
apply oos_symmetry.
rewrite <- s_eq_t.
exists u. split; trivial.
pose proof (pos_same_owner u s PoSus) as (x & Psux & Pssx).
apply conditional_pos_refl.
exists x; assumption. }
pose proof (slot_strong_supp s t NPoSts) as (u & PoSut & NOoSus).
pose proof (slot_strong_supp _ _ Ss St NPoSts) as (u & PoSut & NOoSus).
apply NOoSus.
rewrite oos_comm.
apply oos_symmetry.
rewrite s_eq_t.
exists u. split; trivial.
pose proof (pos_same_owner u t PoSut) as (x & Psux & Pstx).
......@@ -901,6 +939,7 @@ Theorem ppos_extensionality:
forall s t, (exists u, PPoS u s \/ PPoS u t) -> (forall u, PPoS u s <-> PPoS u t) -> s = t.
Proof.
intros s t (u & H) s_eq_t.
assert (ppos_domains : forall s t, PPoS s t -> S s /\ S t) by (intros s' t' []; apply pos_domains; assumption).
apply NNPP.
intro s_ne_t.
assert (~ PoS t s) as NPoSts.
......@@ -909,7 +948,12 @@ Proof.
split; congruence.
apply s_eq_t in PPoSts as [_ t_neq_t].
contradiction. }
pose proof (slot_strong_supp s t NPoSts) as (v & PoSvt & NOoSvs).
assert (Ss: S s) by (destruct H as [PPoSus|PPoSus]; [|apply s_eq_t in PPoSus];
pose proof (ppos_domains _ _ PPoSus) as [_ Ss]; assumption).
assert (St: S t)
by (destruct H as [PPoSut|PPoSut]; [apply s_eq_t in PPoSut|];
pose proof (ppos_domains _ _ PPoSut) as [_ St]; assumption).
pose proof (slot_strong_supp _ _ Ss St NPoSts) as (v & PoSvt & NOoSvs).
assert (t = v) as <-.
{ apply NNPP.
intros t_neq_v.
......@@ -929,52 +973,34 @@ Qed.
(****************
* Sum of Slots *
****************)
Definition SoS u s t := PoS s u /\ PoS t u /\ forall v,
(PoS v u -> (OoS s v \/ OoS t v)).
Definition SoS2 u s t := forall v, (OoS u v <-> (OoS s v \/ OoS t v)).
Theorem SoS_equal_SoS2 : forall u u' s t,
S u -> S u' -> SoS u s t -> SoS2 u' s t -> u = u'.
Lemma sum_domains: forall s t u, SoS s t u -> S s /\ S t /\ S u.
Proof.
intros u u' s t Su Su' (PoSsu & PoStu & H) H1.
unfold SoS2 in H1.
apply oos_extensionality; trivial.
intros w.
split.
- intros (x & PoSxu & PoSxw).
apply H in PoSxu.
apply H1 in PoSxu.
apply part_overlap_implies_whole_overlap with (t:=x); assumption.
- intros OoSu'w.
apply H1 in OoSu'w.
apply oos_comm.
destruct OoSu'w;
apply oos_comm in H0;
[apply part_overlap_implies_whole_overlap with (t:=s)|
apply part_overlap_implies_whole_overlap with (t:=t)];
assumption.
Qed.
Lemma SoS2_imp_Pos: forall s t u, SoS2 u s t -> PoS s u.
Proof.
intros s t u H.
apply NNPP.
intros NPoSsu.
pose proof (slot_strong_supp u s NPoSsu) as (v & PoSvs & NOoSvu).
apply pos_implies_overlap in PoSvs.
destruct H with (v:=v).
destruct H1.
left; apply oos_comm; assumption.
apply NOoSvu.
exists x; apply and_comm; assumption.
intros s t u (PoSts & PoSus & _).
pose proof (pos_domains t s PoSts) as [].
pose proof (pos_domains u s PoSus) as [].
repeat split; assumption.
Qed.
Theorem SoS_equiv_SoS2: forall u s t,
(SoS u s t <-> SoS2 u s t).
Theorem SoS_equiv_SoS2: forall s t, SO s t -> (forall u, SoS u s t <-> SoS2 u s t).
Proof.
intros u s t.
assert (SoS2_imp_Pos: forall s t u, S s -> S u -> SoS2 u s t -> PoS s u).
{
intros s t u Ss Su H; apply NNPP; intros NPoSsu.
pose proof (slot_strong_supp _ _ Su Ss NPoSsu) as (v & PoSvs & NOoSvu).
apply pos_implies_overlap in PoSvs.
destruct H with (v:=v).
destruct H1.
left; apply oos_symmetry; assumption.
apply NOoSvu.
exists x; apply and_comm; assumption.
}
intros s t SOst u.
split.
- intros (PoSsu & PoStu & H) v.
split.
......@@ -984,92 +1010,71 @@ Proof.
apply part_overlap_implies_whole_overlap with (t:=w);
assumption.
+ intros [|];
apply oos_comm in H0;
apply oos_comm;
apply oos_symmetry in H0;
apply oos_symmetry;
[apply part_overlap_implies_whole_overlap with (t:=s)|
apply part_overlap_implies_whole_overlap with (t:=t)];
assumption.
- intros H.
assert (S s /\ S t /\ S u) as (Ss & St & Su).
{ destruct SOst as (a & Pssa & Psta).
repeat split.
exists a; auto.
exists a; auto.
destruct H with (v:=s) as [_ H1].
destruct H1 as (v & PoSvu & PoSvs). left; apply cond_oos_refl; exists a; auto.
pose proof (pos_domains _ _ PoSvu) as (_ & Su); auto. }
repeat split.
+ apply SoS2_imp_Pos with (t:=t); assumption.
+ apply SoS2_imp_Pos with (t:=s).
+ apply SoS2_imp_Pos with (t:=s); auto.
unfold SoS2 in *.
setoid_rewrite (or_comm (OoS s _)) in H.
assumption.
+ intros v PoSvu.
apply H.
apply oos_comm.
apply oos_symmetry.
apply pos_implies_overlap.
assumption.
Qed.
Theorem sum_domains: forall s t u, SoS s t u -> S s /\ S t /\ S u.
Proof.
intros s t u (PoSts & PoSus & _).
pose proof (pos_domains t s PoSts) as [].
pose proof (pos_domains u s PoSus) as [].
repeat split; assumption.
Qed.
Theorem sum_implies_full_overlap: forall s t u,
SoS u s t -> (forall v, OoS v u <-> OoS s v \/ OoS t v).
Proof.
intros s t u (PoSsu & PoStu & H_sum) w.
split.
- intros (x & PoSxw & PoSxu).
pose proof (H_sum x PoSxu).
destruct H as [OoSsx|OoStx];
[left|right];
apply part_overlap_implies_whole_overlap with (t:=x);
assumption.
- intros [|];
apply oos_symmetry in H;
[apply part_overlap_implies_whole_overlap with (t:=s)|apply part_overlap_implies_whole_overlap with (t:=t)];
assumption.
Qed.
(* Sum Existence *)
Axiom sum_existence : forall s t x,
Ps s x /\ Ps t x -> exists u, SoS u s t.
(* Sum Unicity *)
Theorem sum_unicity : forall s t u v,
(SoS u s t -> SoS v s t -> u = v).
Proof.
intros s t u v SoSust SoSvst.
apply oos_extensionality.
destruct SoSust as [[] _].
apply compo_domains in H as (_ & H & _).
assumption.
destruct SoSvst as [[] _].
apply compo_domains in H as (_ & H & _).
assumption.
pose proof (sum_implies_full_overlap s t u SoSust).
pose proof (sum_implies_full_overlap s t v SoSvst).
intros w.
split.
- intros OoSuw.
apply oos_comm, H, H0, oos_comm in OoSuw.
assumption.
- intros OoSuw.
apply oos_comm, H0, H, oos_comm in OoSuw.
assumption.
Qed.
(* Sum Same Owner *)
Theorem sum_same_owner : forall s t u,
SoS u s t -> exists x, Ps u x /\ Ps s x /\ Ps t x.
SoS u s t -> exists a, Ps u a /\ Ps s a /\ Ps t a.
Proof.
intros s t u (PoSsu & PoStu & _).
pose proof (pos_same_owner s u PoSsu) as [x []].
pose proof (pos_same_owner t u PoStu) as [x0 []].
pose proof (single_owner u x H0).
apply H3 in H2.
rewrite <- H2 in H1.
unify_owner H0 H2.
exists x.
repeat split; assumption.
Qed.
(* Sum Unicity *)
Theorem sum_unicity : forall s t u v,
(SoS u s t -> SoS v s t -> u = v).
Proof.
intros s t u v SoSust SoSvst.
apply oos_extensionality.
- destruct SoSust as [H _].
apply pos_domains in H as (_ & H).
assumption.
- destruct SoSvst as [[] _].
apply context_domains in H as (_ & H & _).
assumption.
- pose proof (sum_domains _ _ _ SoSust) as (Su & Ss & St).
pose proof (sum_domains _ _ _ SoSvst) as (Sv & _).
pose proof (sum_same_owner _ _ _ SoSust) as (a & Psua & Pssa & Psta).
apply SoS_equiv_SoS2 in SoSust, SoSvst; auto.
intros w; split; intros OoSuw;
[apply SoSvst, SoSust | apply SoSust, SoSvst];
assumption.
all: exists a; split; auto.
Qed.
(* Sum Idempotence *)
Theorem sum_idempotence : forall s,
S s -> SoS s s s.
......@@ -1079,7 +1084,7 @@ Proof.
repeat split; try (apply conditional_pos_refl; assumption).
intros v PoSvs.
apply pos_implies_overlap in PoSvs.
apply oos_comm in PoSvs.
apply oos_symmetry in PoSvs.
left; assumption.
Qed.
......@@ -1093,54 +1098,27 @@ Proof.
split; intros [H []]; repeat split; assumption.
Qed.
(* PoS t s -> s = s + t*)
Theorem T1 : forall s t,
PoS t s -> SoS s s t.
Lemma L47 : forall s t u, SO s t -> SoS u s t -> PoS s u.
Proof.
intros s t PoSts.
pose proof (pos_same_owner t s PoSts) as [x []].
unfold SoS; repeat split.
apply conditional_pos_refl; exists x; assumption.
intros s t u SOst (PoSsu & _).
assumption.
intros.
left.
unfold OoS.
exists v.
split; try assumption.
pose proof (pos_same_owner v s H1) as [x0 []].
apply conditional_pos_refl; exists x0; assumption.
Qed.
Theorem sum_imp_slot : forall s t x,
IPs s x -> Ps t x -> SoS s s t.
Proof.
intros.
apply T1.
unfold PoS.
exists t.
apply left_imp_composition with (x:=x); assumption.
Qed.
Theorem T134 : forall s t u, SoS u s t -> PoS s u.
Theorem L48 : forall s t u v, SO t u -> PoS s t -> SoS v t u -> PoS s v.
Proof.
intros s t u (PoSsu & _).
assumption.
Qed.
Theorem T34 : forall s t u v, PoS s t -> SoS v t u -> PoS s v.
Proof.
intros s t u v PoSst (PoStv & PoSuv & _).
intros s t u v _ PoSst (PoStv & PoSuv & _).
apply pos_trans with (t:=t); assumption.
Qed.
Theorem T35 : forall s t u v,
SoS v s t -> PoS v u -> PoS s u.
Lemma L49 : forall s t u v,
SO s t -> SoS v s t -> PoS v u -> PoS s u.
Proof.
intros s t u v (PoSsv & _) PoSvu.
intros s t u v _ (PoSsv & _) PoSvu.
apply pos_trans with (t:=v) ; assumption.
Qed.
Theorem T36 : forall s t, PoS s t <-> SoS t s t.
(* PoS t s <-> s = s + t*)
Theorem subpotence : forall s t, PoS s t <-> SoS t s t.
Proof.
intros s t.
split.
......@@ -1151,14 +1129,156 @@ Proof.
apply PoStt; exists x; assumption.
intros v PoSvt.
right.
apply oos_comm.
apply oos_symmetry.
apply pos_implies_overlap.
trivial.
- intros (PoSst & _).
trivial.
Qed.
(* OoS v s -> OoS v (s + t) *)
Theorem overlap_sum_iff_operands: forall s t u,
(exists a, F a s /\ Ps t a /\ Ps u a) ->
forall tPu tPu' t' u', SoS tPu t u -> C tPu' s tPu -> C t' s t -> C u' s u ->
(forall v, OoS v tPu' <-> OoS v t' \/ OoS v u').
Proof.
intros s t u (a & Fas & Psta & Psua) tPu tPu' t' u'
SoStPu C_tPu'_s_tPu Ct'st Cu'su v.
split.
- intros (w & PoSwv & [w1 C_w_tPu'_w1]).
assert (exists w2, C w s w2 /\ C w2 tPu w1) as (w2 & Cwsw2 & Cw2_tPu_w1)
by (context_asso tPu').
assert (PoS w2 tPu) as PoS_w2_tPu by (exists w1; auto).
destruct SoStPu as (PoSt_tPu & PoSu_tPu & H).
apply H in PoS_w2_tPu as [OoStw2|OoSuw2].
+ pose proof (oos_stability _ _ _ _ _ Cwsw2 Ct'st) as oos_stab.
apply oos_symmetry in OoStw2.
apply oos_stab in OoStw2 as (w3 & PoSw3w & PoSw3t').
pose proof (pos_trans _ _ _ PoSw3w PoSwv) as PoSw3v.
left; exists w3; auto.
+ pose proof (oos_stability _ _ _ _ _ Cwsw2 Cu'su) as oos_stab.
apply oos_symmetry in OoSuw2.
apply oos_stab in OoSuw2 as (w3 & PoSw3w & PoSw3u').
pose proof (pos_trans _ _ _ PoSw3w PoSwv) as PoSw3v.
right; exists w3; auto.
- intros [(w & PoSwv & PoSwt')|(w & PoSwv & PoSwu')].
+ exists w; split; auto.
destruct PoSwt' as (w' & Cwt'w').
assert (exists w2, C w s w2 /\ C w2 t w') as (w2 & Cwsw2 & Cw2tw')
by (context_asso t').
destruct SoStPu as (PoSt & _).
destruct PoSt as (t2 & Ct_tPu_t2).
assert (exists w3, C w2 tPu w3 /\ C w3 t2 w') as (w3 & Cw2_tPu_w3 & Cw3t2w')
by (context_asso t).
pose proof (context_asso s tPu w3 w) as [(x & Cwxw3 & CxstPu) _].
exists w2; split; auto.
unify_context C_tPu'_s_tPu CxstPu.
exists w3; auto.
+ exists w; split; auto.
destruct PoSwu' as (w' & Cwu'w').
assert (exists w2, C w s w2 /\ C w2 u w') as (w2 & Cwsw2 & Cw2uw')
by (context_asso u').
destruct SoStPu as (_ & PoSu & _).
destruct PoSu as (u2 & Cu_tPu_u2).
assert (exists w3, C w2 tPu w3 /\ C w3 u2 w') as (w3 & Cw2_tPu_w3 & Cw3u2w')
by (context_asso u).
pose proof (context_asso s tPu w3 w) as [(x & Cwxw3 & CxstPu) _].
exists w2; split; auto.
unify_context C_tPu'_s_tPu CxstPu.
exists w3; auto.
Qed.
Theorem left_distributivity: forall s t u tPu tPu'1 t' u' tPu'2,
(exists a, F a s /\ Ps t a /\ Ps u a) ->
SoS tPu t u -> C tPu'1 s tPu -> C t' s t -> C u' s u -> SoS tPu'2 t' u' ->
tPu'1 = tPu'2.
Proof.
intros s t u tPu tPu'1 t' u' tPu'2 H SoStu C_tPu'1 Ct'st Cu'su SoStPu'2.
apply oos_extensionality.
- pose proof (context_domains _ _ _ C_tPu'1) as (StPu'1 & _); auto.
- pose proof (sum_domains _ _ _ SoStPu'2) as (StPu'2 & _); auto.
- pose proof (overlap_sum_iff_operands s t u H
tPu tPu'1 t' u' SoStu C_tPu'1 Ct'st Cu'su).
apply SoS_equiv_SoS2 in SoStPu'2.
unfold SoS2 in SoStPu'2.
intros w.
rewrite SoStPu'2.
assert (oos_comm: forall s t, OoS s t <-> OoS t s)
by (intros s0 t0; split; apply oos_symmetry).
setoid_rewrite (oos_comm).
apply H0.
pose proof (sum_same_owner _ _ _ SoStPu'2) as (a & _ & Pst'a & Psu'a).
exists a; auto.
Qed.
Lemma L53 : forall a s t u, F a s -> SoS u s t -> F a u -> s = u.
Proof.
intros a s t u Fas ((s' & Csus') & PoStu & H) Fau.
pose proof (context_same_filler _ _ _ Csus') as (a' & Fa's & Fas').
unify_filler Fas Fa's.
pose proof (context_constraints _ _ _ Csus') as (a' & Fa'u & Pss'a).
unify_filler Fau Fa'u.
pose proof (right_imp_composition _ _ _ (conj Pss'a Fas') Fau) as Cuus'.
unify_context Csus' Cuus'.
reflexivity.
Qed.
Theorem right_distrib: forall s t u v w x y,
SoS v s t -> C w v u -> C x s u -> C y t u -> s = t.
Proof.
intros s t u v w x y ((s' & Csvs') & (t' & Ctvt') & _) Cwvu Cxsu Cytu.
pose proof (context_constraints _ _ _ Cwvu) as (a & Fav & Psua).
assert (s = v).
{ pose proof (context_same_filler _ _ _ Csvs') as (e & Fes & Fes').
pose proof (context_constraints _ _ _ Cxsu) as (b & Fbs & Psub).
unify_owner Psua Psub.
unify_filler Fbs Fes.
pose proof (context_constraints _ _ _ Csvs') as (f & Ffv & Pss'f).
unify_filler Fav Ffv.
pose proof (right_imp_composition s' v a (conj Pss'f Fes') Fav) as Cvvs'.
pose proof (context_unicity _ _ _ _ Csvs' Cvvs') as s_eq_v.
assumption. }
assert (t = v).
{ pose proof (context_same_filler _ _ _ Ctvt') as (i & Fit & Fit').
pose proof (context_constraints _ _ _ Cytu) as (c & Fcy & Psuc).
unify_owner Psua Psuc.
unify_filler Fcy Fit.
pose proof (context_constraints _ _ _ Ctvt') as (g & Fgv & Pst'g).
unify_filler Fav Fgv.
pose proof (right_imp_composition _ _ _ (conj Pst'g Fit') Fav) as Cvvt'.
pose proof (context_unicity _ _ _ _ Ctvt' Cvvt') as t_eq_v.
assumption. }
rewrite H, H0.
reflexivity.
Qed.
Lemma left_distrib_ref: forall a b c s t u,
C a s t -> C b s u -> SoS c a b -> (exists d, SoS d t u /\ C c s d).
Proof.
intros a b c s t u Cast Cbsu SoScab.
pose proof (context_constraints s t a Cast) as (x & Fxs & Pstx).
pose proof (context_constraints s u b Cbsu) as (y & Fys & Psuy).
unify_filler Fxs Fys.
rename Psuy into Psux.
pose proof (sum_existence t u x (conj Pstx Psux)) as (d & SoSdtu).
exists d.
split; trivial.
pose proof (sum_same_owner t u d SoSdtu) as (y & Psdx & Psty & _).
unify_owner Pstx Psty.
pose proof (context_existence s d (ex_intro _ _ (conj Fxs Psdx))) as (e & Cesd).
pose proof (left_distributivity s t u d e a b c (ex_intro _ _ (conj Fxs (conj Pstx Psux)) ) SoSdtu Cesd Cast Cbsu SoScab) as <-.
assumption.
Qed.
Lemma pos_sum : forall s t u v,
PoS s v -> PoS t v -> SoS u s t -> PoS u v.
Proof.
intros s t u v [s' Csvs'] [t' Ctvt'] SoSust.
pose proof (left_distrib_ref s t u v s' t' Csvs' Ctvt' SoSust) as (w & SoSws't' & Cuvw).
exists w; assumption.
Qed.
Lemma L1 : forall s t u v,
SoS u s t -> OoS v s -> OoS v u.
Proof.
......@@ -1171,21 +1291,6 @@ Proof.
apply pos_trans with (t:=s) ; assumption.
Qed.
(* OoS v (s o t) -> OoS v (s o (t + u)) *)
Lemma L2 : forall s t u v a b c,
C a s t -> SoS b t u -> C c s b -> OoS v a -> OoS v c.
Proof.
intros s t u v a b c Cast ([t' Ctbt'] & _) Ccsb [x [PoSxv [x1 Cxax1]]].
exists x.
split; trivial.
pose proof (compo_asso_lr x a x1 s t Cxax1 Cast) as [x2 [Cxsx2 Cx2tx1]].
pose proof (compo_asso_lr x2 t x1 b t' Cx2tx1 Ctbt') as [x3 [Cx2bx3 _]].
exists x3.
pose proof (compo_asso_rl x x3 s b x2 Cxsx2 Cx2bx3) as [x4 [Cxx4x3 Cx4sb]].
pose proof (composition_unicity s b c x4 Ccsb Cx4sb) as <-.
assumption.
Qed.
(* OoS v (s + t) -> OoS s v \/ OoS t v *)
Lemma L3 : forall s t u v,
SoS u s t -> OoS v u -> OoS s v \/ OoS t v.
......@@ -1197,87 +1302,6 @@ Proof.
assumption.
Qed.
(* OoS v (s o (t + u)) -> OoS (v, s o t) \/ OoS(v, s o u) *)
Lemma L4 : forall s t u v a b c d,
SoS a t u -> C b s a -> OoS v b -> C c s t -> C d s u -> OoS v c \/ OoS v d.
Proof.
intros s t u v a b c d ([t' Ctat'] & [u' Cuau'] & H_sum) Cbsa (r & [w Crvw] & [q' Crbq']) Ccst Cdsu.
pose proof (compo_asso_lr r b q' s a Crbq' Cbsa) as (q & Crsq & Cqaq').
assert (PoSqa : PoS q a) by (exists q'; assumption).
pose proof (H_sum q PoSqa) as [OoStq|OoSuq].
- left.
apply oos_stability with (s:=s) (v:=c) (w:=r) in OoStq as (x & PoSxc & PoSxr); trivial.
exists x.
split; trivial.
apply pos_trans with (t:=r); trivial.
exists w; assumption.
- right.
apply oos_stability with (s:=s) (v:=d) (w:=r) in OoSuq as (x & PoSxc & PoSxr); trivial.
exists x.
split; trivial.
apply pos_trans with (t:=r); trivial.
exists w; assumption.
Qed.
(* OoS v (s o t + s o u) <-> OoS v (s o (t + u)) *)
Lemma L5 : forall s t u a b c d e,
C b s t -> C c s u -> SoS a b c -> SoS d t u -> C e s d -> (forall v, OoS v a <-> OoS v e).
Proof.
intros s t u a b c d e Cbst Ccsu SoSabc SoSdtu Cesd v.
split.
(* Left to right *)
- intro OoSva.
pose proof (L3 b c a v SoSabc OoSva) as [OoSbv|OoScv].
+ apply oos_symmetry in OoSbv as OoSvb.
pose proof (L2 s t u v b d e Cbst SoSdtu Cesd OoSvb).
assumption.
+ apply oos_symmetry in OoScv as OoSvc.
apply sum_commutativity in SoSdtu as SoSdut.
pose proof (L2 s u t v c d e Ccsu SoSdut Cesd OoSvc).
assumption.
(* Right to left *)
- intro OoSve.
pose proof (L4 s t u v d e b c SoSdtu Cesd OoSve Cbst Ccsu) as [OoSvb|OoSvc].
+ pose proof (L1 b c a v SoSabc OoSvb).
assumption.
+ apply sum_commutativity in SoSabc as SoSacb.
pose proof (L1 c b a v SoSacb OoSvc).
assumption.
Qed.
Theorem left_distributivity: forall s t u a b c d e,
SoS a t u -> C b s a -> C c s t -> C d s u -> SoS e c d -> b = e.
Proof.
Admitted.
Theorem left_distrib_ref: forall a b c s t u,
C a s t -> C b s u -> SoS c a b -> (exists d, SoS d t u /\ C c s d).
Proof.
intros a b c s t u Cast Cbsu SoScab.
pose proof (composition_constraints s t a Cast) as (x & Fxs & Pstx).
pose proof (composition_constraints s u b Cbsu) as (y & Fys & Psuy).
pose proof (single_filler s x Fxs y Fys) as <-.
rename Psuy into Psux.
clear Fys.
pose proof (sum_existence t u x (conj Pstx Psux)) as (d & SoSdtu).
exists d.
split; trivial.
pose proof (sum_same_owner t u d SoSdtu) as (y & Psdx & Psty & _).
pose proof (single_owner t x Pstx y Psty) as <-.
clear Psty.
pose proof (composition_existence s d x Fxs Psdx) as (e & Cesd).
pose proof (left_distributivity s t u d e a b c SoSdtu Cesd Cast Cbsu SoScab) as <-.
assumption.
Qed.
Lemma pos_sum : forall s t u v,
PoS s v -> PoS t v -> SoS u s t -> PoS u v.
Proof.
intros s t u v [s' Csvs'] [t' Ctvt'] SoSust.
pose proof (left_distrib_ref s t u v s' t' Csvs' Ctvt' SoSust) as (w & SoSws't' & Cuvw).
exists w; assumption.
Qed.
(* Sum Associativity *)
Theorem sum_associativity : forall s t u a b c d,
SoS a s t -> SoS b a u -> SoS d s c -> SoS c t u -> b = d.
......@@ -1297,75 +1321,174 @@ Proof.
destruct SoSdsc as (PoSsd & PoScd & H).
apply H in PoSvd as [OoSsv|OoScv].
+ left.
apply oos_comm.
apply oos_symmetry.
apply L1 with (s:=s) (t:=t); trivial.
apply oos_comm; assumption.
+ apply oos_comm in OoScv.
apply oos_symmetry; assumption.
+ apply oos_symmetry in OoScv.
pose proof (L3 t u c v SoSctu OoScv) as [OoStv|OoSuv].
* left.
apply oos_comm.
apply oos_symmetry.
apply L1 with (s:=t) (t:=s).
apply sum_commutativity; assumption.
apply oos_comm; assumption.
apply oos_symmetry; assumption.
* right; assumption.
Qed.
Theorem sum_asso2: forall s t u a b c d,
SoS a s t -> SoS b a u -> SoS d s c -> SoS c t u -> b = d.
Theorem sum_stability: forall u s t v, Cb u v -> Cb s v -> Cb t v ->
(forall u' s' t', C u' v u /\ C s' v s /\ C t' v t -> SoS u s t <-> SoS u' s' t').
Proof.
intros u s t v (a & Fav & Psua) (b & Fbv & Pssa) (c & Fcv & Psta) u' s' t' (Cu'vu & Cs'vs & Ct'vt).
unify_filler Fav Fbv.
unify_filler Fav Fcv.
pose proof (pos_stability _ _ _ _ _ Cu'vu Cs'vs) as PoSsu_stab.
pose proof (pos_stability _ _ _ _ _ Cu'vu Ct'vt) as PoStu_stab.
unfold SoS; rewrite PoSsu_stab, PoStu_stab; repeat apply and_iff_compat_l.
split; intros H.
- intros w' [x Cwu'x].
assert (exists w, C w' v w /\ C w u x) as (w & Cw'vw & Cwux) by (context_asso u') .
pose proof (oos_stability _ _ _ _ _ Cs'vs Cw'vw) as H1.
pose proof (oos_stability _ _ _ _ _ Ct'vt Cw'vw) as H2.
rewrite <- H1, <- H2.
apply H; exists x; auto.
- intros w PoSwu.
pose proof (pos_same_owner _ _ PoSwu) as (b & Pswb & Psub).
unify_owner Psua Psub.
assert (exists w', C w' v w) as [w' Cw'vw].
apply context_existence; exists a; split; auto.
pose proof (oos_stability v _ _ _ _ Cs'vs Cw'vw) as H2.
rewrite H2.
pose proof (oos_stability v _ _ _ _ Ct'vt Cw'vw) as H3.
rewrite H3.
apply H.
pose proof (pos_stability v _ _ _ _ Cu'vu Cw'vw) as H1.
rewrite <- H1.
auto.
Qed.
(**********
* Fusion *
**********)
Definition FoS z (phi: Entity -> Prop) :=
(forall w, phi w -> PoS w z) /\ (forall v, PoS v z -> (exists w, phi w /\ OoS v w)).
Axiom FoS_existence:
forall phi, (exists w, phi w /\ (forall v, phi v -> SO w v))
-> (exists z, FoS z phi).
Theorem FoS_unicity:
forall (phi : Entity -> Prop) s t, (exists w, phi w)
-> FoS s phi -> FoS t phi -> s = t.
Proof.
intros phi s t [w phiW] [H1 H2] [H3 H4].
apply oos_extensionality.
{ apply H1, pos_domains in phiW as [_ Ss].
assumption. }
{ apply H3, pos_domains in phiW as [_ St].
assumption. }
intros u; split.
- intros (a & PoSas & PoSau).
pose proof (H2 a PoSas) as (b & phiB & (c & PoSca & PoScb)).
pose proof (H3 b phiB) as PoSbt.
pose proof (pos_trans c a u PoSca PoSau) as PoScu.
pose proof (pos_trans c b t PoScb PoSbt) as PoSct.
exists c; split; assumption.
- intros (a & PoSat & PoSau).
pose proof (H4 a PoSat) as (b & phiB & (c & PoSca & PoScb)).
pose proof (H1 b phiB) as PoSbs.
pose proof (pos_trans c a u PoSca PoSau) as PoScu.
pose proof (pos_trans c b s PoScb PoSbs) as PoScs.
exists c; split; assumption.
Qed.
Ltac unify_fusion FoS1 Fos2 :=
pose proof (FoS_unicity _ _ _ FoS1 Fos2);
subst; clear Fos2.
Theorem conditioned_FoS_iff_SoS: forall s t u, FoS u (fun w => w = s \/ w = t) <-> SoS u s t.
Proof.
intros s t u.
split.
+ intros [H H0].
repeat split; try apply H; auto.
intros v PoSvu.
pose proof (H0 v PoSvu) as (w & H1).
destruct H1.
apply oos_symmetry in H2.
destruct H1 as [-> | ->]; auto.
+ intros (PoSsu & PoStu & H).
split.
intros w [-> | ->]; auto.
intros v PoSvu.
pose proof (H v PoSvu) as []; apply oos_symmetry in H0; [exists s | exists t ]; split; auto.
Qed.
Theorem slot_is_fusion_of_its_slots: forall s, FoS s (fun w => PoS w s).
Proof.
intros s.
split; auto.
intros v PoSvs.
exists v; split; auto.
apply cond_oos_refl.
pose proof (pos_same_owner _ _ PoSvs) as (a & Psva & _).
exists a; auto.
Qed.
Lemma sss_contra : forall s t,
(forall u, ~ PoS u t \/ OoS u s) -> PoS t s.
Theorem ips_is_fusion: forall a s, Ps s a -> (exists t, IPs t a /\ FoS t (fun w => Ps w a)).
Proof.
intros s t H.
apply NNPP.
intros NPoSts.
pose proof (slot_strong_supp s t NPoSts) as (u & PoSut & NOoSus).
pose proof (H u).
destruct H0; contradiction.
Qed.
Theorem test_1 : forall a s t u tPu,
IPs s a -> PPs t a -> PPs u a -> SoS tPu t u ->
(forall v, PPs v a -> v = t \/ v = u) -> s = tPu.
Proof.
intros a s t u tPu [Pssa Fas] [Psta NFat] [Psua NFau] SoStPu v_eq_t_or_u.
pose proof (sum_same_owner t u tPu SoStPu) as (a' & PspTua' & Psta' & _).
pose proof (single_owner t a Psta a' Psta') as <-.
clear Psta'.
rename PspTua' into PspTua.
pose proof (sum_domains tPu t u SoStPu) as (StPu & St & Su).
apply pos_antisym.
(* Proof of PoS s (t + u) *)
* apply sss_contra.
intros v.
apply imply_to_or.
intros PoSvs.
destruct (classic (v = s)) as [v_eq_s|v_neq_s].
- rewrite v_eq_s.
exists tPu.
split.
+ exists tPu.
apply left_imp_composition with (x:=a).
split. all: assumption.
+ apply conditional_pos_refl; assumption.
- assert (PPs v a) as PPsva.
(* Proof of PPs v a *)
{ pose proof (pos_same_owner v s PoSvs) as (a' & Psva' & Pssa').
pose proof (single_owner s a Pssa a' Pssa') as <-.
clear Pssa'.
rename Psva' into Psva.
split. assumption.
intros Fav.
pose proof (unique_improper_slot a s v (conj Pssa Fas) (conj Psva Fav)) as <-.
contradiction. }
pose proof (v_eq_t_or_u v PPsva).
destruct SoStPu as (PoSttPu & PoSutPu & H2).
destruct H as [->| ->];
[exists t|exists u]; split; trivial;
apply conditional_pos_refl;
exists a; assumption.
(* Proof of PoS (t+u) s *)
* apply slots_are_parts_of_imp_slot with (a:=a).
split. all: assumption.
intros a s Pssa.
pose proof (whole_improper_slots a) as (t & IPsta).
exists s; assumption.
exists t; split; auto.
pose proof (ips_eq a t IPsta).
unfold FoS.
setoid_rewrite H.
apply slot_is_fusion_of_its_slots.
Qed.
Theorem fusion_stability : forall (phi : Entity -> Prop) s s' t,
C s' t s -> (forall w, phi w -> exists w', C w' t w ) -> (FoS s phi <-> FoS s' (fun w' => exists w, C w' t w /\ phi w)).
Proof.
intros phi s s' t Cs'ts H.
split.
- intros [H1 H2].
split.
+ intros w (w' & Cwtw' & phi_w').
pose proof (H1 _ phi_w') as PoSw's.
pose proof (pos_stability _ _ _ _ _ Cs'ts Cwtw') as pos_stab.
rewrite pos_stab in PoSw's; auto.
+ intros v (v' & Cvs'v').
assert (exists v'', C v t v'' /\ C v'' s v') as (v'' & Cvtv'' & Cv''sv).
context_asso s'.
pose proof (H2 v'') as (w'' & phiw'' & OoSv''w'').
exists v'; auto.
pose proof (H1 w'' phiw'') as PoSw''s.
pose proof (pos_same_owner w'' s PoSw''s) as (a & Psw''a & Pssa).
pose proof (context_constraints _ _ _ Cs'ts) as (b & Fat & Pssb).
unify_owner Pssa Pssb.
pose proof (context_existence t w'' (ex_intro _ _ (conj Fat Psw''a))) as (w''' & Cw'''tw'').
exists w'''; split.
exists w''; auto.
pose proof (oos_stability t v'' w'' v w''' Cvtv'' Cw'''tw'') as oos_stab.
apply oos_stab; auto.
- intros [H1 H2].
split.
+ intros w phiW.
pose proof (H w phiW) as (w' & Cw'tw).
pose proof (pos_stability t s w s' w' Cs'ts Cw'tw) as pos_stab.
apply pos_stab, H1.
exists w; split; auto.
+ intros v' (v & Cv'sv).
assert (exists v'', C v'' s' v) as (v'' & Cv''s'v).
{ pose proof (context_constraints _ _ _ Cv'sv) as (a & Fas & Psua).
pose proof (context_same_filler _ _ _ Cs'ts) as (b & Fas' & Fbs).
unify_filler Fas Fbs.
apply context_existence; exists a; split; auto. }
pose proof (H2 v'') as (w & (w' & Cwtw' & phiw') & OoSv''w).
exists v; auto.
exists w'; split; auto.
assert (exists u, C v'' t u /\ C u s v) as (u & Cv''tu & Cusv).
context_asso s'.
unify_context Cv'sv Cusv.
pose proof (oos_stability _ _ _ _ _ Cv''tu Cwtw') as oos_stab.
apply oos_stab; auto.
Qed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment