Require Lattice.
Require Arith.
Require semantic.
Section AbNum.
Inductive AbNum : Set :=
| top : AbNum
| const : nat -> AbNum
| bot : AbNum.
Inductive AbNumOrder : AbNum -> AbNum -> Prop :=
| top_order : (v:AbNum) (AbNumOrder v top)
| const_order : (n:nat) (AbNumOrder (const n) (const n))
| bot_order : (v:AbNum) (AbNumOrder bot v).
Definition AbNumjoin := [v1,v2:AbNum]
Cases v1 v2 of
| bot _ => v2
| _ bot => v1
| (const n) (const m) =>
Cases (eq_nat_dec n m) of
(left _) => (const n)
| (right _) => top
end
| _ _ => top
end.
Local eq:=[x,y:AbNum]x=y.
Local order:=AbNumOrder.
Definition acc_property_top : (Acc AbNum ([x,y] ~(eq y x)/\(order y x)) top).
Constructor; Intros y (H1,H2); Generalize H1; Clear H1;
Inversion_clear H2; Intros H1; Try (Elim H1; Unfold eq; Reflexivity).
Qed.
Definition acc_property_const : (n:nat)(Acc AbNum ([x,y] ~(eq y x)/\(order y x)) (const n)).
Constructor; Intros y (H1,H2); Generalize H1; Clear H1;
Inversion_clear H2; Intros H1; Try (Elim H1; Unfold eq; Reflexivity);
Apply acc_property_top.
Qed.
Definition LatAbNum : (Lattice AbNum).
Refine (poset_constr ? AbNumOrder [x,y]x=y AbNumjoin
? ? ? ? ? ? ? ? ? ? bot ? top ? ?).
Intuition; Rewrite H; Case y; Intros; Constructor.
Intros x y H0; Inversion_clear H0; Intros H1; Auto; Inversion_clear H1; Auto.
Intros x y z H0; Inversion_clear H0; Intros H1; Auto; Inversion_clear H1; Try Constructor; Auto.
Intuition.
Intuition.
Intuition; Rewrite H; Auto.
Intros x y; Case x; Case y; Intros; Simpl; Try Constructor.
Case eq_nat_dec; Constructor.
Intros x y; Case x; Case y; Intros; Simpl; Try Constructor.
Case eq_nat_dec; Try Constructor.
Intros H; Subst; Constructor.
Intros x y; Case x; Case y; Intros; Simpl; Auto; Try Constructor.
Generalize H; Inversion_clear H0; Simpl; Try Constructor.
Intros H'; Inversion_clear H'.
Case eq_nat_dec; Intros; Try Constructor.
Elim n1; Reflexivity.
Decide Equality.
Apply eq_nat_dec; Auto.
Constructor.
Constructor.
Unfold well_founded.
Destruct a.
Apply acc_property_top.
Apply acc_property_const.
Constructor; Destruct y.
Intros (H1,H2).
Apply acc_property_top.
Intros n (H1,H2).
Apply acc_property_const.
Intros (H1,H2).
Elim H1; Unfold eq; Reflexivity.
Defined.
Definition AbIf_Z : (A:Set)(Lattice A)->A->AbNum->A :=
[A,PA,x,b]
Cases b of
| top => x
| (const (0)) => x
| (const n) => (bottom PA)
| bot => (bottom PA)
end.
Implicits AbIf_Z [1].
Definition AbIf_NZ : (A:Set)(Lattice A)->A->AbNum->A :=
[A,PA,x,b]
Cases b of
| top => x
| (const (0)) => (bottom PA)
| (const n) => x
| bot => (bottom PA)
end.
Implicits AbIf_NZ [1].
Lemma AbIf_Z_monotone : (A:Set;PA:(Lattice A);a1,a2:A;b1,b2:AbNum)
(Lattice.order PA a1 a2) -> (Lattice.order LatAbNum b1 b2) ->
(Lattice.order PA (AbIf_Z PA a1 b1) (AbIf_Z PA a2 b2)).
Intros.
Inversion_clear H0; Simpl; Auto.
Case b1; Simpl; Auto.
Destruct n; Simpl; Auto.
Case n; Simpl; Auto.
Qed.
Lemma AbIf_NZ_monotone : (A:Set;PA:(Lattice A);a1,a2:A;b1,b2:AbNum)
(Lattice.order PA a1 a2) -> (Lattice.order LatAbNum b1 b2) ->
(Lattice.order PA (AbIf_NZ PA a1 b1) (AbIf_NZ PA a2 b2)).
Intros.
Inversion_clear H0; Simpl; Auto.
Case b1; Simpl; Auto.
Destruct n; Simpl; Auto.
Case n; Simpl; Auto.
Qed.
Definition betaNum : nat -> AbNum :=
[n:nat]
(const n).
Definition R_Num : nat -> AbNum -> Prop :=
[n,N](Lattice.order LatAbNum (betaNum n) N).
Lemma R_Num_monotonicity : (n:nat;N1,N2:AbNum)
(R_Num n N1) -> (Lattice.order LatAbNum N1 N2) -> (R_Num n N2).
Unfold R_Num; Intros; EAuto.
Qed.
Lemma AbIf_NZ_prop : (A:Set;PA:(Lattice A);n:nat;a:A)
~n=(0) ->
(AbIf_NZ PA a (betaNum n))=a.
Unfold betaNum; Intros A PA n a.
Case n; Intros; Auto.
Elim H; Auto.
Qed.
Lemma AbIf_Z_prop : (A:Set;PA:(Lattice A);b:AbNum;a:A)
(R_Num (0) b) ->
(AbIf_Z PA a b)=a.
Unfold R_Num betaNum; Intros A PA b a H.
Inversion_clear H; Auto.
Qed.
Definition AbMult : AbNum -> AbNum -> AbNum :=
[v1,v2]Cases v1 v2 of
| bot _ => bot
| _ bot => bot
| (const (0)) _ => (const (0))
| (const n) (const m) => (const (mult n m))
| _ _ => top
end.
Definition AbPlus : AbNum -> AbNum -> AbNum :=
[v1,v2]Cases v1 v2 of
| bot _ => bot
| _ bot => bot
| (const n) (const m) => (const (plus n m))
| _ _ => top
end.
Definition AbComp : AbNum -> AbNum -> AbNum :=
[v1,v2]Cases v1 v2 of
| bot _ => bot
| _ bot => bot
| (const n) (const m) => (const (comp n m))
| _ _ => top
end.
Definition AbMinus : AbNum -> AbNum -> AbNum :=
[v1,v2]Cases v1 v2 of
| bot _ => bot
| _ bot => bot
| (const n) (const m) => (const (minus n m))
| _ _ => top
end.
Lemma AbMult_monotone :
(x1,x2,y1,y2:AbNum)
(Lattice.order LatAbNum x1 x2) ->
(Lattice.order LatAbNum y1 y2) ->
(Lattice.order LatAbNum (AbMult x1 y1) (AbMult x2 y2)).
Unfold LatAbNum; Simpl.
Destruct x1; Destruct x2; Destruct y1; Destruct y2;
(Match Context With
[|-(x:nat)?] -> Intros N H1 H2
| _ -> Intros H1 H2);
(Inversion H1;Fail) Orelse (Inversion H2;Fail) Orelse (Constructor;Fail)
Orelse Intros.
Case n; Simpl; Constructor.
Inversion_clear H1.
Case n0; Simpl; Constructor.
Inversion_clear H1.
Case n0; Simpl; Constructor.
Inversion_clear H2; Inversion_clear H1.
Case n0; Case N; Simpl; Constructor.
Inversion_clear H1.
Case n0; Simpl; Constructor.
Inversion_clear H1.
Case n0; Simpl; Constructor.
Inversion_clear H1.
Case n0; Simpl; Constructor.
Qed.
Lemma AbPlus_monotone :
(x1,x2,y1,y2:AbNum)
(Lattice.order LatAbNum x1 x2) ->
(Lattice.order LatAbNum y1 y2) ->
(Lattice.order LatAbNum (AbPlus x1 y1) (AbPlus x2 y2)).
Unfold LatAbNum; Simpl.
Destruct x1; Destruct x2; Destruct y1; Destruct y2;
Intros H1 H2; Simpl;
(Inversion H1;Fail) Orelse (Inversion H2;Fail) Orelse Constructor
Orelse Intros.
Inversion H.
Inversion_clear H2; Inversion_clear H; Constructor.
Qed.
Lemma AbComp_monotone :
(x1,x2,y1,y2:AbNum)
(Lattice.order LatAbNum x1 x2) ->
(Lattice.order LatAbNum y1 y2) ->
(Lattice.order LatAbNum (AbComp x1 y1) (AbComp x2 y2)).
Unfold LatAbNum; Simpl.
Destruct x1; Destruct x2; Destruct y1; Destruct y2;
Intros H1 H2; Simpl;
(Inversion H1;Fail) Orelse (Inversion H2;Fail) Orelse Constructor
Orelse Intros.
Inversion H.
Inversion_clear H2; Inversion_clear H; Constructor.
Qed.
Lemma AbMinus_monotone :
(x1,x2,y1,y2:AbNum)
(Lattice.order LatAbNum x1 x2) ->
(Lattice.order LatAbNum y1 y2) ->
(Lattice.order LatAbNum (AbMinus x1 y1) (AbMinus x2 y2)).
Unfold LatAbNum; Simpl.
Destruct x1; Destruct x2; Destruct y1; Destruct y2;
Intros H1 H2; Simpl;
(Inversion H1;Fail) Orelse (Inversion H2;Fail) Orelse Constructor
Orelse Intros.
Inversion H.
Inversion_clear H2; Inversion_clear H; Constructor.
Qed.
Lemma AbMult_correct : (n1,n2:nat)
(Lattice.order LatAbNum (betaNum (mult n1 n2))
(AbMult (betaNum n1) (betaNum n2))).
Unfold betaNum; Intros.
Case (eq_nat_dec n1 (0));
Case (eq_nat_dec n2 (0)); Intros.
Subst.
Simpl.
Constructor.
Case (eq_nat_dec (mult n1 n2) (0)); Simpl; Intros.
Subst.
Rewrite e0; Constructor.
Elim n0; Subst; Auto.
Case (eq_nat_dec (mult n1 n2) (0)); Simpl; Intros.
Subst; Rewrite e0.
Case n1; Constructor.
Elim n0; Subst.
Rewrite <- mult_n_O; Reflexivity.
Case (eq_nat_dec (mult n1 n2) (0)); Simpl; Intros.
Generalize n0; Case n1; Intros; Simpl.
Constructor.
Constructor.
Generalize n0; Case n1; Intros; Simpl.
Elim n4; Auto.
Constructor.
Qed.
Lemma AbPlus_correct : (n1,n2:nat)
(Lattice.order LatAbNum (betaNum (plus n1 n2))
(AbPlus (betaNum n1) (betaNum n2))).
Unfold betaNum; Intros.
Case (eq_nat_dec n1 (0));
Case (eq_nat_dec n2 (0)); Intros.
Subst.
Simpl.
Constructor.
Case (eq_nat_dec (plus n1 n2) (0)); Simpl; Intros.
Subst ; Simpl in e0 ; Subst ; Elim n ;Trivial.
Constructor.
Case (eq_nat_dec (plus n1 n2) (0)); Simpl; Intros.
Subst.
Rewrite plus_sym in e0 ; Simpl in e0 ; Subst ; Elim n ; Trivial.
Constructor.
Case (eq_nat_dec (plus n1 n2) (0)); Simpl; Intros ; Constructor.
Qed.
Lemma AbComp_correct : (n1,n2:nat)
(Lattice.order LatAbNum (betaNum (comp n1 n2))
(AbComp (betaNum n1) (betaNum n2))).
Unfold betaNum; Intros.
Case (eq_nat_dec n1 (0));
Case (eq_nat_dec n2 (0)); Intros.
Subst.
Simpl.
Constructor.
Subst.
Case (eq_nat_dec (comp (0) n2) (0)); Simpl; Intros.
Constructor.
Unfold comp in n0 ; Simpl in n0.
Generalize n0 ;Clear n0.
Case (le_gt_dec n2 (0)); Intros.
Red in n ; Apply False_ind ; Apply n ; Auto with arith.
Elim n0 ; Auto.
Subst.
Case (eq_nat_dec (comp n1 (0)) (0)); Simpl; Intros.
Generalize e ; Clear e ; Unfold comp.
Case le_gt_dec ; Intros.
Discriminate e.
Apply False_ind ; Omega.
Constructor.
Case (eq_nat_dec (comp n1 n2) (0)); Simpl; Intros ; Constructor.
Qed.
Lemma AbMinus_correct : (n1,n2:nat)
(Lattice.order LatAbNum (betaNum (minus n1 n2))
(AbMinus (betaNum n1) (betaNum n2))).
Unfold betaNum AbMinus; Intros ;Auto.
Qed.
End AbNum.