Commit 38d09de5 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Adapt to Coq 8.5 by introducing custom versions of iter_nat and iter_pos.

parent 88e92db3
......@@ -697,7 +697,7 @@ Qed.
Definition shr mrs e n :=
match n with
| Zpos p => (iter_pos p _ shr_1 mrs, (e + n)%Z)
| Zpos p => (iter_pos shr_1 p mrs, (e + n)%Z)
| _ => (mrs, e)
end.
......@@ -748,24 +748,24 @@ destruct n as [|n|n].
now destruct l as [|[| |]].
2: now destruct l as [|[| |]].
unfold shr.
rewrite iter_nat_of_P.
rewrite iter_pos_nat.
rewrite Zpos_eq_Z_of_nat_o_nat_of_P.
induction (nat_of_P n).
simpl.
rewrite Zplus_0_r.
now destruct l as [|[| |]].
simpl nat_rect.
rewrite iter_nat_S.
rewrite inj_S.
unfold Zsucc.
rewrite Zplus_assoc.
rewrite Zplus_assoc.
revert IHn0.
apply inbetween_shr_1.
clear -Hm.
induction n0.
now destruct l as [|[| |]].
simpl.
rewrite iter_nat_S.
revert IHn0.
generalize (iter_nat n0 shr_record shr_1 (shr_record_of_loc m l)).
generalize (iter_nat shr_1 n0 (shr_record_of_loc m l)).
clear.
intros (m, r, s) Hm.
now destruct m as [|[m|m|]|m] ; try (now elim Hm) ; destruct r as [|] ; destruct s as [|].
......
......@@ -617,7 +617,7 @@ apply refl_equal.
Qed.
Definition default_nan_pl32 : bool * nan_pl 24 :=
(false, exist _ (iter_nat 22 _ xO xH) (refl_equal true)).
(false, exist _ (iter_nat xO 22 xH) (refl_equal true)).
Definition unop_nan_pl32 (f : binary32) : bool * nan_pl 24 :=
match f with
......@@ -660,7 +660,7 @@ apply refl_equal.
Qed.
Definition default_nan_pl64 : bool * nan_pl 53 :=
(false, exist _ (iter_nat 51 _ xO xH) (refl_equal true)).
(false, exist _ (iter_nat xO 51 xH) (refl_equal true)).
Definition unop_nan_pl64 (f : binary64) : bool * nan_pl 53 :=
match f with
......
......@@ -927,3 +927,65 @@ intros [|a|a] [|b|b] ; try rewrite Zpos_div_eucl_aux_correct ; easy.
Qed.
End faster_div.
Section Iter.
Context {A : Type}.
Variable (f : A -> A).
Fixpoint iter_nat (n : nat) (x : A) {struct n} : A :=
match n with
| S n' => iter_nat n' (f x)
| O => x
end.
Lemma iter_nat_plus :
forall (p q : nat) (x : A),
iter_nat (p + q) x = iter_nat p (iter_nat q x).
Proof.
induction q.
now rewrite plus_0_r.
intros x.
rewrite <- plus_n_Sm.
apply IHq.
Qed.
Lemma iter_nat_S :
forall (p : nat) (x : A),
iter_nat (S p) x = f (iter_nat p x).
Proof.
induction p.
easy.
simpl.
intros x.
apply IHp.
Qed.
Fixpoint iter_pos (n : positive) (x : A) {struct n} : A :=
match n with
| xI n' => iter_pos n' (iter_pos n' (f x))
| xO n' => iter_pos n' (iter_pos n' x)
| xH => f x
end.
Lemma iter_pos_nat :
forall (p : positive) (x : A),
iter_pos p x = iter_nat (Pos.to_nat p) x.
Proof.
induction p ; intros x.
rewrite Pos2Nat.inj_xI.
simpl.
rewrite plus_0_r.
rewrite iter_nat_plus.
rewrite (IHp (f x)).
apply IHp.
rewrite Pos2Nat.inj_xO.
simpl.
rewrite plus_0_r.
rewrite iter_nat_plus.
rewrite (IHp x).
apply IHp.
easy.
Qed.
End Iter.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment