Library PosInf
Require Export ZArith.
Lemma positive_dec : forall (p1 p2:positive), {p1=p2}+{~p1=p2}.
decide equality.
Qed.
Inductive inf_log : positive -> nat -> Prop :=
inf_log_xH : forall (n:nat), (inf_log xH n)
| inf_log_xO : forall (p:positive) (n:nat),
(inf_log p n) -> (inf_log (xO p) (S n))
| inf_log_xI : forall (p:positive) (n:nat),
(inf_log p n) -> (inf_log (xI p) (S n)).
Lemma inf_log_dec : forall (p:positive) (n:nat), {(inf_log p n)}+{~(inf_log p n)}.
induction p; intros.
destruct n.
right; intros H; inversion H.
case (IHp n); intros.
left; constructor; auto.
right; intros H; elim n0; inversion_clear H; auto.
destruct n.
right; intros H; inversion H.
case (IHp n); intros.
left; constructor; auto.
right; intros H; elim n0; inversion_clear H; auto.
left; constructor.
Qed.
Definition posInf := fun (n:nat) => {p:positive | inf_log p n}.
Definition WordSize : nat := (32).
Definition Word : Set := posInf WordSize.
Definition Word_1 : Word.
exists xH.
constructor.
Qed.
Definition eq_word : Word -> Word -> Prop := fun w1 w2 =>
let (p1,_):=w1 in let (p2,_):=w2 in p1=p2.
Lemma eq_word_dec : forall (w1 w2:Word), {eq_word w1 w2}+{~eq_word w1 w2}.
destruct w1; destruct w2; simpl; apply positive_dec.
Qed.
Definition word2pos : Word -> positive := fun w =>
let (p,_):= w in p.
Coercion word2pos : Word >-> positive.
Definition succ_word : Word -> Word.
intros (p,H).
set (r:= Psucc p).
case (inf_log_dec r WordSize); intros.
exists r; auto.
exists p; auto.
Defined.
Lemma eq_word_refl : forall p, eq_word p p.
destruct p; simpl; auto.
Qed.
Lemma eq_word_sym : forall p q, eq_word p q -> eq_word q p.
destruct p; destruct q; simpl; auto.
Qed.
Lemma eq_word_trans : forall x y z,
eq_word x y -> eq_word y z -> eq_word x z.
destruct x; destruct y; destruct z; simpl; intros; subst; auto.
Qed.
Hint Resolve eq_word_refl.
Hint Immediate eq_word_sym.
Index
This page has been generated by coqdoc