Library PosInf
Require Export ZArith.
Axiom physical_eq : forall (A:Set) (x y : A), {x=y}+{True}.
Implicit Arguments physical_eq [A].
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.
Lemma inf_log_le : forall p2 p1 n,
inf_log p2 n -> (nat_of_P p1)<=(nat_of_P p2) -> inf_log p1 n.
Proof.
induction p2; simpl; intros.
inversion_clear H.
rewrite nat_of_P_xI in H0.
destruct p1; constructor.
rewrite nat_of_P_xI in H0; apply IHp2; auto.
omega.
rewrite nat_of_P_xO in H0; apply IHp2; auto.
omega.
inversion_clear H.
rewrite nat_of_P_xO in H0.
destruct p1; constructor.
rewrite nat_of_P_xI in H0; apply IHp2; auto.
omega.
rewrite nat_of_P_xO in H0; apply IHp2; auto.
omega.
replace (nat_of_P 1) with 1 in H0; auto.
generalize (lt_O_nat_of_P p1); intros.
assert (nat_of_P p1 = 1).
omega.
replace 1 with (nat_of_P xH) in H2; auto.
rewrite (nat_of_P_inj _ _ H2); 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.
Defined.
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 succ_word_eq_word : forall p1 p2,
eq_word p1 p2 -> eq_word (succ_word p1) (succ_word p2).
destruct p1; destruct p2; simpl; intros.
subst; case inf_log_dec; simpl; auto.
Qed.
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 eq_word_sym.
Lemma eq_word_def' : forall p1 p2,
word2pos p1 = word2pos p2 ->
eq_word p1 p2.
Proof.
destruct p1; destruct p2; simpl; auto.
Qed.
Definition exP := exist (fun p:positive => inf_log p 32).
Fixpoint succ_word_n (n:nat) : Word -> Word :=
match n with
O => fun w => w
| S p => fun w => succ_word_n p (succ_word w)
end.
Index
This page has been generated by coqdoc