~ubuntu-branches/ubuntu/hardy/coq-doc/hardy

<code class="keyword">Fixpoint</code> <a name="iter_nat"></a>iter_nat (n:<a href="Coq.Init.Datatypes.html#nat">nat</a>) (A:Set) (f:A -> A) (x:A) {struct n} : A :=

match n with

| <a href="Coq.Init.Datatypes.html#O">O</a> => x

| <a href="Coq.Init.Datatypes.html#S">S</a> n' => f (iter_nat n' A f x)

end.

<code class="keyword">Fixpoint</code> <a name="iter_pos"></a>iter_pos (n:<a href="Coq.NArith.BinPos.html#positive">positive</a>) (A:Set) (f:A -> A) (x:A) {struct n} : A :=

match n with

| <a href="Coq.NArith.BinPos.html#xH">xH</a> => f x

| <a href="Coq.NArith.BinPos.html#xO">xO</a> n' => iter_pos n' A f (iter_pos n' A f x)

| <a href="Coq.NArith.BinPos.html#xI">xI</a> n' => f (iter_pos n' A f (iter_pos n' A f x))

end.

<code class="keyword">Definition</code> <a name="iter"></a>iter (n:<a href="Coq.ZArith.BinInt.html#Z">Z</a>) (A:Set) (f:A -> A) (x:A) :=

match n with

| <a href="Coq.ZArith.BinInt.html#Z0">Z0</a> => x

| <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> p => <a href="Coq.ZArith.Zmisc.html#iter_pos">iter_pos</a> p A f x

| <a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> p => x

end.

<code class="keyword">Theorem</code> <a name="iter_nat_plus"></a>iter_nat_plus :

forall (n m:<a href="Coq.Init.Datatypes.html#nat">nat</a>) (A:Set) (f:A -> A) (x:A),

<a href="Coq.ZArith.Zmisc.html#iter_nat">iter_nat</a> (n + m) A f x = <a href="Coq.ZArith.Zmisc.html#iter_nat">iter_nat</a> n A f (<a href="Coq.ZArith.Zmisc.html#iter_nat">iter_nat</a> m A f x).

<code class="keyword">Proof</code>.

simple induction n;

[ simpl in |- *; auto with arith

| intros; simpl in |- *; apply <a href="Coq.Init.Logic.html#f_equal">f_equal</a> with (f:= f); apply H ].

<code class="keyword">Qed</code>.

<code class="keyword">Theorem</code> <a name="iter_nat_of_P"></a>iter_nat_of_P :

forall (p:<a href="Coq.NArith.BinPos.html#positive">positive</a>) (A:Set) (f:A -> A) (x:A),

<a href="Coq.ZArith.Zmisc.html#iter_pos">iter_pos</a> p A f x = <a href="Coq.ZArith.Zmisc.html#iter_nat">iter_nat</a> (<a href="Coq.NArith.BinPos.html#nat_of_P">nat_of_P</a> p) A f x.

<code class="keyword">Proof</code>.

intro n; induction n as [p H| p H| ];

[ intros; simpl in |- *; rewrite (H A f x);

rewrite (H A f (<a href="Coq.ZArith.Zmisc.html#iter_nat">iter_nat</a> (<a href="Coq.NArith.BinPos.html#nat_of_P">nat_of_P</a> p) A f x));

rewrite (<a href="Coq.NArith.Pnat.html#ZL6">ZL6</a> p); symmetry in |- *; apply <a href="Coq.Init.Logic.html#f_equal">f_equal</a> with (f:= f);

apply <a href="Coq.ZArith.Zmisc.html#iter_nat_plus">iter_nat_plus</a>

| intros; unfold nat_of_P in |- *; simpl in |- *; rewrite (H A f x);

rewrite (H A f (<a href="Coq.ZArith.Zmisc.html#iter_nat">iter_nat</a> (<a href="Coq.NArith.BinPos.html#nat_of_P">nat_of_P</a> p) A f x));

rewrite (<a href="Coq.NArith.Pnat.html#ZL6">ZL6</a> p); symmetry in |- *; apply <a href="Coq.ZArith.Zmisc.html#iter_nat_plus">iter_nat_plus</a>

| simpl in |- *; auto with arith ].

<code class="keyword">Qed</code>.

<code class="keyword">Theorem</code> <a name="iter_pos_plus"></a>iter_pos_plus :

forall (p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>) (A:Set) (f:A -> A) (x:A),

<a href="Coq.ZArith.Zmisc.html#iter_pos">iter_pos</a> (p + q) A f x = <a href="Coq.ZArith.Zmisc.html#iter_pos">iter_pos</a> p A f (<a href="Coq.ZArith.Zmisc.html#iter_pos">iter_pos</a> q A f x).

<code class="keyword">Proof</code>.

intros n m; intros.

rewrite (<a href="Coq.ZArith.Zmisc.html#iter_nat_of_P">iter_nat_of_P</a> m A f x).

rewrite (<a href="Coq.ZArith.Zmisc.html#iter_nat_of_P">iter_nat_of_P</a> n A f (<a href="Coq.ZArith.Zmisc.html#iter_nat">iter_nat</a> (<a href="Coq.NArith.BinPos.html#nat_of_P">nat_of_P</a> m) A f x)).

rewrite (<a href="Coq.ZArith.Zmisc.html#iter_nat_of_P">iter_nat_of_P</a> (n + m) A f x).

rewrite (<a href="Coq.NArith.Pnat.html#nat_of_P_plus_morphism">nat_of_P_plus_morphism</a> n m).

apply <a href="Coq.ZArith.Zmisc.html#iter_nat_plus">iter_nat_plus</a>.

<code class="keyword">Qed</code>.

</code>

Preservation of invariants : if <code>f : A->A</code> preserves the invariant <code>Inv</code>,

then the iterates of <code>f</code> also preserve it.

</td></tr></table>

100

<code>

101

102

103

<code class="keyword">Theorem</code> <a name="iter_nat_invariant"></a>iter_nat_invariant :

104

forall (n:<a href="Coq.Init.Datatypes.html#nat">nat</a>) (A:Set) (f:A -> A) (Inv:A -> Prop),

105

(forall x:A, Inv x -> Inv (f x)) ->

106

forall x:A, Inv x -> Inv (<a href="Coq.ZArith.Zmisc.html#iter_nat">iter_nat</a> n A f x).

107

<code class="keyword">Proof</code>.

108

simple induction n; intros;

109

[ trivial with arith

110

| simpl in |- *; apply H0 with (x:= <a href="Coq.ZArith.Zmisc.html#iter_nat">iter_nat</a> n0 A f x); apply H;

111

trivial with arith ].

112

<code class="keyword">Qed</code>.

113

114

115

<code class="keyword">Theorem</code> <a name="iter_pos_invariant"></a>iter_pos_invariant :

116

forall (p:<a href="Coq.NArith.BinPos.html#positive">positive</a>) (A:Set) (f:A -> A) (Inv:A -> Prop),

117

(forall x:A, Inv x -> Inv (f x)) ->

118

forall x:A, Inv x -> Inv (<a href="Coq.ZArith.Zmisc.html#iter_pos">iter_pos</a> p A f x).

119

<code class="keyword">Proof</code>.

120

intros; rewrite <a href="Coq.ZArith.Zmisc.html#iter_nat_of_P">iter_nat_of_P</a>; apply <a href="Coq.ZArith.Zmisc.html#iter_nat_invariant">iter_nat_invariant</a>; trivial with arith.

121

<code class="keyword">Qed</code>.

122

</code>

123

<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://www.lri.fr/~filliatr/coqdoc/">coqdoc</a>

124

</body>

125

</html>

b'\\ No newline at end of file'

Older »