Library SumLattice
Require Export Lattice.
Section sum.
Variables A B : Set.
Variable PA : Poset A.
Variable PB : Poset B.
Inductive lift (A : Set) : Set :=
| bot_sum : lift A
| top_sum : lift A
| some_sum : A -> lift A.
Inductive sum_order : lift (A + B) -> lift (A + B) -> Prop :=
| sum_order_bot : forall x : lift (A + B), sum_order (bot_sum _) x
| sum_order_top : forall x : lift (A + B), sum_order x (top_sum _)
| sum_order_left :
forall a1 a2 : A,
order PA a1 a2 ->
sum_order (some_sum _ (inl _ a1)) (some_sum _ (inl _ a2))
| sum_order_right :
forall b1 b2 : B,
order PB b1 b2 ->
sum_order (some_sum _ (inr _ b1)) (some_sum _ (inr _ b2)).
Inductive sum_eq : lift (A + B) -> lift (A + B) -> Prop :=
| sum_eq_bot : sum_eq (bot_sum _) (bot_sum _)
| sum_eq_top : sum_eq (top_sum _) (top_sum _)
| sum_eq_left :
forall a1 a2 : A,
eq PA a1 a2 -> sum_eq (some_sum _ (inl _ a1)) (some_sum _ (inl _ a2))
| sum_eq_right :
forall b1 b2 : B,
eq PB b1 b2 -> sum_eq (some_sum _ (inr _ b1)) (some_sum _ (inr _ b2)).
Definition SumPoset : Poset (lift (A + B)).
refine
(poset_constr (lift (A + B))
sum_eq _ _ _
sum_order _ _ _).
simple destruct x; try constructor.
simple destruct s; try constructor; auto.
intros x y H; inversion_clear H; try constructor; auto.
intros x y z H; inversion_clear H; intros H'; inversion_clear H';
try constructor; eauto.
intros x y H; inversion_clear H; try constructor; auto.
intros x y H; inversion_clear H; intros H'; inversion_clear H'; try constructor; auto.
intros x y z H; inversion_clear H; intros H'; inversion_clear H';
try constructor; eauto.
Defined.
End sum.
Implicit Arguments SumPoset [A B].
Section sumlat.
Variables A B : Set.
Variable PA : Lattice A.
Variable PB : Lattice B.
Definition joinSum : lift (A + B) -> lift (A + B) -> lift (A+B) :=
fun x y =>
match x,y with
bot_sum,_ => y
| _,bot_sum => x
| some_sum (inl x1),some_sum (inl y1) => some_sum _ (inl _ (join PA x1 y1))
| some_sum (inr x1),some_sum (inr y1) => some_sum _ (inr _ (join PB x1 y1))
| _,_ => top_sum _
end.
Definition SumLattice : Lattice (lift (A+B)).
refine (lattice_constr _ (SumPoset PA PB)
joinSum _ _ _ _ (bot_sum _) _ (top_sum _) _ _).
destruct x; destruct y; simpl; try constructor.
destruct s; try constructor; auto.
destruct s; try constructor; auto.
destruct s; destruct s0; try constructor; auto.
destruct x; destruct y; simpl; try constructor.
destruct s; try constructor; auto.
destruct s; try constructor; auto.
destruct s; destruct s0; try constructor; auto.
intros x y z H; inversion_clear H; simpl; try constructor.
intros H; inversion_clear H; simpl; try constructor; auto.
intros H; inversion_clear H; simpl; try constructor; auto.
intros H; inversion_clear H; simpl; try constructor; auto.
destruct x.
left; constructor.
destruct y.
right; intros H; inversion H.
left; constructor.
right; intros H; inversion H.
destruct y.
right; intros H; inversion H.
left; constructor.
destruct s; destruct s0; try (right;intros H; inversion H;fail).
case (order_dec PA a a0); intros.
left; constructor; auto.
right; intros H; elim n; inversion_clear H; auto.
case (order_dec PB b b0); intros.
left; constructor; auto.
right; intros H; elim n; inversion_clear H; auto.
constructor.
constructor.
intros x.
cut (Acc
(fun x0 y : lift (A + B) =>
~ eq (SumPoset PA PB) y x0 /\ order (SumPoset PA PB) y x0) (top_sum _)); intros.
cut (forall s, Acc
(fun x0 y : lift (A + B) =>
~ eq (SumPoset PA PB) y x0 /\ order (SumPoset PA PB) y x0) (some_sum _ s)); intros.
constructor; intros y (H1,H2).
destruct y; auto.
elim H1; inversion_clear H2; auto.
destruct s.
induction (acc_property PA a); intros.
clear H0; constructor; intros y (H0,H2).
inversion_clear H2 in H0; auto.
apply H1; split; auto.
red; intros; elim H0; constructor; auto.
induction (acc_property PB b); intros.
clear H0; constructor; intros y (H0,H2).
inversion_clear H2 in H0; auto.
apply H1; split; auto.
red; intros; elim H0; constructor; auto.
constructor; intros y (H1,H2).
elim H1; inversion_clear H2; auto.
Defined.
End sumlat.
Implicit Arguments SumLattice [A B].
Index
This page has been generated by coqdoc