Library NumAlgebraImplem_const
Require Export AlgebraType.
Section Num.
Inductive AbNumConst : Set :=
| top : AbNumConst
| const : nat -> AbNumConst
| bot : AbNumConst.
Inductive AbNumConstOrder : AbNumConst -> AbNumConst -> Prop :=
| top_order : forall (v:AbNumConst), (AbNumConstOrder v top)
| const_order : forall (n:nat), (AbNumConstOrder (const n) (const n))
| bot_order : forall (v:AbNumConst), (AbNumConstOrder bot v).
Definition AbNumConstjoin := fun v1 v2:AbNumConst =>
match v1,v2 with
| bot,_ => v2
| _,bot => v1
| (const n),(const m) =>
match (eq_nat_dec n m) with
(left _) => (const n)
| (right _) => top
end
| _,_ => top
end.
Let eq:= fun x y:AbNumConst => x=y.
Let order:=AbNumConstOrder.
Definition acc_property_top : (Acc (fun 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 : forall (n:nat), (Acc (fun 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 AbNumConstPoset : (Poset AbNumConst).
refine (poset_constr _ eq _ _ _ AbNumConstOrder _ _ _).
unfold eq; intuition.
unfold eq; intuition.
unfold eq; intuition.
subst; auto.
intuition; rewrite H; case y; intros; constructor.
unfold eq; 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.
Defined.
Definition AbNumConstLattice : (Lattice AbNumConst).
refine (lattice_constr _ AbNumConstPoset AbNumConstjoin _ _ _ _ bot _ top _ _).
destruct x; destruct y; simpl; try constructor.
case eq_nat_dec; constructor.
destruct x; destruct y; simpl; try constructor.
case eq_nat_dec; try constructor.
intros H; rewrite H; constructor.
intros x y z H; inversion_clear H; intros H1; inversion_clear H1; simpl; try constructor.
case eq_nat_dec; try constructor; intros.
elim n0; auto.
destruct y.
left; constructor.
destruct x.
right; intros H; inversion H.
case (eq_nat_dec n0 n); intros.
subst; left; constructor.
right; intros H; elim n1; inversion_clear H; auto.
left; constructor.
destruct x.
right; intros H; inversion H.
right; intros H; inversion H.
left; constructor.
constructor.
constructor.
intros a.
destruct a.
apply acc_property_top.
apply acc_property_const.
constructor; destruct y; intros (H1,H2).
apply acc_property_top.
apply acc_property_const.
elim H1; constructor.
Defined.
Definition gammaNumConst : Gamma (PowPoset nat) AbNumConstLattice.
refine (gamma_constr _ _
(fun a => match a with
bot => fun _ => False
| const n => fun x => x=n
| top => fun _ => True
end)
_).
intros b1 b2 H; inversion_clear H; intros x; intuition.
Defined.
Definition gammaTopNumConst : GammaTop (PowPoset nat) AbNumConstLattice.
refine (gammatop_constr gammaNumConst _).
simpl; intros; auto.
Defined.
Definition NumconstAlgebra : Num.Connect.
intros.
refine (Num.Build_Connect
gammaTopNumConst
(fun n => const n) _
(fun op n1 n2 => match n1 with
bot => bot
| top => top
| const x1 =>
match n2 with
bot => bot
| top => top
| const x2 => const (sem_binop op x1 x2)
end
end) _).
simpl; auto.
intros op n1 n2 x H; unfold gammaNumConst; simpl.
inversion_clear H.
inversion_clear H0 in H1.
destruct n1; auto.
destruct n2; auto.
Defined.
End Num.
Index
This page has been generated by coqdoc