Require Lattice.
Section sum.
Variable A,B:Set.
Variable PA:(Lattice A).
Variable PB:(Lattice 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 : (x:(lift A+B))(sum_order (bot_sum ?) x)
| sum_order_top : (x:(lift A+B))(sum_order x (top_sum ?))
| sum_order_left : (a1,a2:A) (order PA a1 a2) ->
(sum_order (some_sum ? (inl ? ? a1)) (some_sum ? (inl ? ? a2)))
| sum_order_right : (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 : (a1,a2:A) (eq PA a1 a2) ->
(sum_eq (some_sum ? (inl ? ? a1)) (some_sum ? (inl ? ? a2)))
| sum_eq_right : (b1,b2:B) (eq PB b1 b2) ->
(sum_eq (some_sum ? (inr ? ? b1)) (some_sum ? (inr ? ? b2))).
Definition join_sum : (lift A+B) -> (lift A+B) -> (lift A+B) :=
[x,y]
Cases x y of
| bot_sum _ => y
| _ bot_sum => x
| top_sum _ => (top_sum ?)
| _ top_sum => (top_sum ?)
| (some_sum s1) (some_sum s2) =>
Cases s1 s2 of
| (inl a1) (inl a2) => (some_sum ? (inl ? ? (join PA a1 a2)))
| (inr b1) (inr b2) => (some_sum ? (inr ? ? (join PB b1 b2)))
| _ _ => (top_sum ?)
end
end.
Definition sum_Lattice : (Lattice (lift A+B)).
Refine (poset_constr
(lift A+B)
sum_order
sum_eq
join_sum
? ? ? ? ? ? ? ? ?
? (bot_sum ?) ? (top_sum ?) ? ?).
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.
Destruct x; Try Constructor.
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.
Destruct x; Destruct y; Intros; Simpl; Try Constructor.
Case s; Try Constructor; Auto.
Case s; Case s0; Try Constructor; Auto.
Destruct x; Destruct y; Intros; Simpl; Try Constructor.
Case s; Try Constructor; Auto.
Case s; Case s0; Try Constructor; Auto.
Intros x y z H; Inversion_clear H; Intros H'; Inversion_clear H'; Simpl; Try Constructor; Auto.
Destruct x; Destruct y; Try (Right; Red; Intros H'; Inversion H'; Fail).
Left; Constructor.
Left; Constructor.
Case s; Destruct s0; Intros; Try (Right; Red; Intros H'; Inversion H'; Fail).
Case (eq_dec PA a a0); Intros.
Left; Constructor ;Auto.
Right; Red; Intros H'; Inversion_clear H'; Elim n; Auto.
Case (eq_dec PB b b0); Intros.
Left; Constructor ;Auto.
Right; Red; Intros H'; Inversion_clear H'; Elim n; Auto.
Constructor.
Constructor.
Unfold well_founded; Intros.
Cut (Acc (lift A+B) [x,y:(lift A+B)]~(sum_eq y x)/\(sum_order y x) (top_sum ?)).
Intros acc_top.
Cut (s:A+B)(Acc (lift A+B) [x,y:(lift A+B)]~(sum_eq y x)/\(sum_order y x) (some_sum ? s)).
Intros acc_s.
Case a; Auto.
Constructor; Intros.
Elim H; Clear H; Intros.
Generalize H; Clear H H0; Case y; Intros; Auto.
Elim H; Constructor.
Clear a; Destruct s; Intros.
NewInduction (acc_property PA a); Intros.
Constructor; Intros.
Elim H1; Clear H1; Intros.
Generalize H1; Clear H1; Inversion_clear H2; Intros; Auto.
Apply H0; Auto.
Split; Auto.
Red; Intros; Elim H2; Constructor; Auto.
NewInduction (acc_property PB b); Intros.
Constructor; Intros.
Elim H1; Clear H1; Intros.
Generalize H1; Clear H1; Inversion_clear H2; Intros; Auto.
Apply H0; Auto.
Split; Auto.
Red; Intros; Elim H2; Constructor; Auto.
Constructor; Intros.
Elim H; Clear H; Intros.
Elim H; Clear H; Inversion_clear H0; Constructor.
Defined.
Definition injLeft := [a:A] (some_sum A+B (inl A B a)).
Definition injRight := [b:B] (some_sum A+B (inr A B b)).
Section lift_unop.
Variable C:Set.
Variable PC:(Lattice C).
Variable f:A->C.
Definition lift_left_unop :=
[x:(lift A+B)]
Cases x of
| (some_sum (inl a)) => (f a)
| top_sum => (top PC)
| _ => (bottom PC)
end.
Variable g:B->C.
Definition lift_right_unop :=
[x:(lift A+B)]
Cases x of
| (some_sum (inr b)) => (g b)
| top_sum => (top PC)
| _ => (bottom PC)
end.
End lift_unop.
Section lift_binop.
Variable f:A->A->A.
Definition lift_left_binop :=
[x,y:(lift A+B)]
Cases x y of
| (some_sum (inl a)) (some_sum (inl b)) => (some_sum ? (inl ? ? (f a b)))
| top_sum _ => (top_sum A+B)
| _ top_sum => (top_sum A+B)
| _ _ => (bot_sum A+B)
end.
Variable g:B->B->B.
Definition lift_right_binop :=
[x,y:(lift A+B)]
Cases x y of
| (some_sum (inr a)) (some_sum (inr b)) => (some_sum ? (inr ? ? (g a b)))
| top_sum _ => (top_sum A+B)
| _ top_sum => (top_sum A+B)
| _ _ => (bot_sum A+B)
end.
End lift_binop.
End sum.
Section monotone.
Variable A,B:Set.
Variable PA:(Lattice A).
Variable PB:(Lattice B).
Lemma injLeft_monotone : (x,y:A)
(order PA x y) ->
(order (sum_Lattice A B PA PB) (injLeft A B x) (injLeft A B y)).
Unfold injLeft; Simpl.
Constructor; Auto.
Qed.
Lemma injRight_monotone : (x,y:B)
(order PB x y) ->
(order (sum_Lattice A B PA PB) (injRight A B x) (injRight A B y)).
Unfold injRight; Simpl.
Constructor; Auto.
Qed.
Lemma lift_right_binop_monotone : (f,g:B->B->B)
((x,y:B)(order PB (f x y) (g x y))) ->
(x,y:(lift A+B))
(order (sum_Lattice A B PA PB) (lift_right_binop ? ? f x y)
(lift_right_binop ? ? g x y)).
Intros.
Case x; Case y; Cbv Beta Iota Delta [lift_right_binop]; Auto.
Intros s s0; Case s0; Auto.
Case s; Auto.
Constructor; Auto.
Qed.
Lemma lift_left_binop_monotone : (f,g:A->A->A)
((x,y:A)(order PA (f x y) (g x y))) ->
(x,y:(lift A+B))
(order (sum_Lattice A B PA PB) (lift_left_binop ? ? f x y)
(lift_left_binop ? ? g x y)).
Intros.
Case x; Case y; Cbv Beta Iota Delta [lift_left_binop]; Auto.
Intros s s0; Case s0; Auto.
Case s; Auto.
Constructor; Auto.
Qed.
Variable C:Set.
Variable PC:(Lattice C).
Lemma lift_left_unop_unfold : (f:A->C;x:(lift A+B);c:C)
(order PC (lift_left_unop A B C PC f x) c) ->
((x,y:A) (order PA x y) -> (order PC (f x) (f y))) ->
(a:A) (order (sum_Lattice A B PA PB) (some_sum ? (inl ? ? a)) x) ->
(order PC (f a) c).
Intros.
Generalize H; Clear H.
Unfold lift_left_unop.
Inversion_clear H1; Intros.
Apply order_trans with (top PC); Auto.
Apply order_trans with (f a2); Auto.
Qed.
Lemma lift_right_unop_unfold : (f:B->C;x:(lift A+B);c:C)
(order PC (lift_right_unop A B C PC f x) c) ->
((x,y:B) (order PB x y) -> (order PC (f x) (f y))) ->
(a:B) (order (sum_Lattice A B PA PB) (some_sum ? (inr ? ? a)) x) ->
(order PC (f a) c).
Intros.
Generalize H; Clear H.
Unfold lift_right_unop.
Inversion_clear H1; Intros.
Apply order_trans with (top PC); Auto.
Apply order_trans with (f b2); Auto.
Qed.
Lemma lift_left_unop_keep_monotone :
(f,g:A->C)
((x,y:A) (order PA x y) -> (order PC (f x) (g y))) ->
(x,y:(lift A+B))
(order (sum_Lattice A B PA PB) x y) ->
(order PC (lift_left_unop A B C PC f x) (lift_left_unop A B C PC g y)).
Intros.
Unfold lift_left_unop.
Inversion_clear H0; Auto.
Qed.
Lemma lift_right_unop_keep_monotone :
(f,g:B->C)
((x,y:B) (order PB x y) -> (order PC (f x) (g y))) ->
(x,y:(lift A+B))
(order (sum_Lattice A B PA PB) x y) ->
(order PC (lift_right_unop A B C PC f x) (lift_right_unop A B C PC g y)).
Intros.
Unfold lift_right_unop.
Inversion_clear H0; Auto.
Qed.
Lemma lift_right_binop_keep_monotone : (f:B->B->B)
((x1,x2,y1,y2:B)
(order PB x1 x2) ->
(order PB y1 y2) -> (order PB (f x1 y1) (f x2 y2))) ->
(x1,x2,y1,y2:(lift A+B))
(order (sum_Lattice A B PA PB) x1 x2) ->
(order (sum_Lattice A B PA PB) y1 y2) ->
(order (sum_Lattice A B PA PB) (lift_right_binop ? ? f x1 y1)
(lift_right_binop ? ? f x2 y2)).
Intros.
Unfold order in H0; Simpl in H0.
Unfold order in H1; Simpl in H1.
Inversion_clear H0.
Inversion_clear H1.
Replace (lift_right_binop A B f (bot_sum A+B) (bot_sum A+B)) with
(bottom (sum_Lattice A B PA PB)); Auto.
Replace (lift_right_binop A B f x2 (top_sum A+B)) with
(top (sum_Lattice A B PA PB)); Auto.
Case x2; Simpl; Auto.
Intros s; Case s; Auto.
Replace (lift_right_binop A B f (bot_sum A+B) (some_sum A+B (inl A B a1))) with
(bottom (sum_Lattice A B PA PB)); Auto.
Replace (lift_right_binop A B f (bot_sum A+B) (some_sum A+B (inr A B b1))) with
(bottom (sum_Lattice A B PA PB)); Auto.
Replace (lift_right_binop A B f (top_sum A+B) y2) with
(top (sum_Lattice A B PA PB)); Auto.
Inversion_clear H1; Cbv Beta Iota Delta [lift_right_binop]; Auto.
Replace (bot_sum A+B) with (bottom (sum_Lattice A B PA PB)); Auto.
Replace (top_sum A+B) with (top (sum_Lattice A B PA PB)); Auto.
Inversion_clear H1; Cbv Beta Iota Delta [lift_right_binop]; Auto.
Replace (bot_sum A+B) with (bottom (sum_Lattice A B PA PB)); Auto.
Replace (top_sum A+B) with (top (sum_Lattice A B PA PB)); Auto.
Constructor; Auto.
Qed.
Lemma lift_left_binop_keep_monotone : (f:A->A->A)
((x1,x2,y1,y2:A)
(order PA x1 x2) ->
(order PA y1 y2) -> (order PA (f x1 y1) (f x2 y2))) ->
(x1,x2,y1,y2:(lift A+B))
(order (sum_Lattice A B PA PB) x1 x2) ->
(order (sum_Lattice A B PA PB) y1 y2) ->
(order (sum_Lattice A B PA PB) (lift_left_binop ? ? f x1 y1)
(lift_left_binop ? ? f x2 y2)).
Intros.
Unfold order in H0; Simpl in H0.
Unfold order in H1; Simpl in H1.
Inversion_clear H0.
Inversion_clear H1.
Replace (lift_left_binop A B f (bot_sum A+B) (bot_sum A+B)) with
(bottom (sum_Lattice A B PA PB)); Auto.
Replace (lift_left_binop A B f x2 (top_sum A+B)) with
(top (sum_Lattice A B PA PB)); Auto.
Case x2; Simpl; Auto.
Intros s; Case s; Auto.
Replace (lift_left_binop A B f (bot_sum A+B) (some_sum A+B (inl A B a1))) with
(bottom (sum_Lattice A B PA PB)); Auto.
Replace (lift_left_binop A B f (bot_sum A+B) (some_sum A+B (inr A B b1))) with
(bottom (sum_Lattice A B PA PB)); Auto.
Replace (lift_left_binop A B f (top_sum A+B) y2) with
(top (sum_Lattice A B PA PB)); Auto.
Inversion_clear H1; Cbv Beta Iota Delta [lift_left_binop]; Auto.
Replace (bot_sum A+B) with (bottom (sum_Lattice A B PA PB)); Auto.
Replace (top_sum A+B) with (top (sum_Lattice A B PA PB)); Auto.
Constructor; Auto.
Inversion_clear H1; Cbv Beta Iota Delta [lift_left_binop]; Auto.
Replace (bot_sum A+B) with (bottom (sum_Lattice A B PA PB)); Auto.
Replace (top_sum A+B) with (top (sum_Lattice A B PA PB)); Auto.
Qed.
End monotone.
Implicits lift_left_unop [1 2 3].
Implicits lift_right_unop [1 2 3].