Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 336 insertions, 301 deletions

diff --git a/theories/IntMap/Addr.v b/theories/IntMap/Addr.v
index cff8936b6f..fcab8b565c 100644
--- a/theories/IntMap/Addr.v
+++ b/theories/IntMap/Addr.v
@@ -9,448 +9,483 @@
 
 (** Representation of adresses by the [positive] type of binary numbers *)
 
-Require Bool.
-Require ZArith.
+Require Import Bool.
+Require Import ZArith.
 
 Inductive ad : Set :=
-    ad_z : ad
+  | ad_z : ad
   | ad_x : positive -> ad.
 
-Lemma ad_sum : (a:ad) {p:positive | a=(ad_x p)}+{a=ad_z}.
-Proof.
-  NewDestruct a; Auto.
-  Left; Exists p; Trivial.
-Qed.
-
-Fixpoint p_xor [p:positive] : positive -> ad :=
-  [p2] Cases p of
-      xH => Cases p2 of
-	        xH => ad_z
-	      | (xO p'2) => (ad_x (xI p'2))
-	      | (xI p'2) => (ad_x (xO p'2))
-	    end
-    | (xO p') => Cases p2 of
-                     xH => (ad_x (xI p'))
-		   | (xO p'2) => Cases (p_xor p' p'2) of
-		                     ad_z => ad_z
-				   | (ad_x p'') => (ad_x (xO p''))
-				 end
-		   | (xI p'2) => Cases (p_xor p' p'2) of
-		                     ad_z => (ad_x xH)
-				   | (ad_x p'') => (ad_x (xI p''))
-				 end
-                 end
-    | (xI p') => Cases p2 of
-		     xH => (ad_x (xO p'))
-		   | (xO p'2) => Cases (p_xor p' p'2) of
-		                     ad_z => (ad_x xH)
-				   | (ad_x p'') => (ad_x (xI p''))
-				 end
-		   | (xI p'2) => Cases (p_xor p' p'2) of
-		                     ad_z => ad_z
-				   | (ad_x p'') => (ad_x (xO p''))
-				 end
-                 end
+Lemma ad_sum : forall a:ad, {p : positive | a = ad_x p} + {a = ad_z}.
+Proof.
+  destruct a; auto.
+  left; exists p; trivial.
+Qed.
+
+Fixpoint p_xor (p p2:positive) {struct p} : ad :=
+  match p with
+  | xH =>
+      match p2 with
+      | xH => ad_z
+      | xO p'2 => ad_x (xI p'2)
+      | xI p'2 => ad_x (xO p'2)
+      end
+  | xO p' =>
+      match p2 with
+      | xH => ad_x (xI p')
+      | xO p'2 =>
+          match p_xor p' p'2 with
+          | ad_z => ad_z
+          | ad_x p'' => ad_x (xO p'')
+          end
+      | xI p'2 =>
+          match p_xor p' p'2 with
+          | ad_z => ad_x 1
+          | ad_x p'' => ad_x (xI p'')
+          end
+      end
+  | xI p' =>
+      match p2 with
+      | xH => ad_x (xO p')
+      | xO p'2 =>
+          match p_xor p' p'2 with
+          | ad_z => ad_x 1
+          | ad_x p'' => ad_x (xI p'')
+          end
+      | xI p'2 =>
+          match p_xor p' p'2 with
+          | ad_z => ad_z
+          | ad_x p'' => ad_x (xO p'')
+          end
+      end
   end.
 
-Definition ad_xor := [a,a':ad]
-  Cases a of
-      ad_z => a'
-    | (ad_x p) => Cases a' of
-                      ad_z => a
-	            | (ad_x p') => (p_xor p p')
-                  end
+Definition ad_xor (a a':ad) :=
+  match a with
+  | ad_z => a'
+  | ad_x p => match a' with
+              | ad_z => a
+              | ad_x p' => p_xor p p'
+              end
   end.
 
-Lemma ad_xor_neutral_left : (a:ad) (ad_xor ad_z a)=a.
+Lemma ad_xor_neutral_left : forall a:ad, ad_xor ad_z a = a.
 Proof.
-  Trivial.
+  trivial.
 Qed.
 
-Lemma ad_xor_neutral_right : (a:ad) (ad_xor a ad_z)=a.
+Lemma ad_xor_neutral_right : forall a:ad, ad_xor a ad_z = a.
 Proof.
-  NewDestruct a; Trivial.
+  destruct a; trivial.
 Qed.
 
-Lemma ad_xor_comm : (a,a':ad) (ad_xor a a')=(ad_xor a' a).
+Lemma ad_xor_comm : forall a a':ad, ad_xor a a' = ad_xor a' a.
 Proof.
-  NewDestruct a; NewDestruct a'; Simpl; Auto.
-  Generalize p0; Clear p0; NewInduction p as [p Hrecp|p Hrecp|]; Simpl; Auto.
-  NewDestruct p0; Simpl; Trivial; Intros.
-  Rewrite Hrecp; Trivial.
-  Rewrite Hrecp; Trivial.
-  NewDestruct p0; Simpl; Trivial; Intros.
-  Rewrite Hrecp; Trivial.
-  Rewrite Hrecp; Trivial.
-  NewDestruct p0; Simpl; Auto.
+  destruct a; destruct a'; simpl in |- *; auto.
+  generalize p0; clear p0; induction p as [p Hrecp| p Hrecp| ]; simpl in |- *;
+   auto.
+  destruct p0; simpl in |- *; trivial; intros.
+  rewrite Hrecp; trivial.
+  rewrite Hrecp; trivial.
+  destruct p0; simpl in |- *; trivial; intros.
+  rewrite Hrecp; trivial.
+  rewrite Hrecp; trivial.
+  destruct p0 as [p| p| ]; simpl in |- *; auto.
 Qed.
 
-Lemma ad_xor_nilpotent : (a:ad) (ad_xor a a)=ad_z.
+Lemma ad_xor_nilpotent : forall a:ad, ad_xor a a = ad_z.
 Proof.
-  NewDestruct a; Trivial.
-  Simpl. NewInduction p as [p IHp|p IHp|]; Trivial.
-  Simpl. Rewrite IHp; Reflexivity.
-  Simpl. Rewrite IHp; Reflexivity.
+  destruct a; trivial.
+  simpl in |- *. induction p as [p IHp| p IHp| ]; trivial.
+  simpl in |- *. rewrite IHp; reflexivity.
+  simpl in |- *. rewrite IHp; reflexivity.
 Qed.
 
-Fixpoint ad_bit_1 [p:positive] : nat -> bool :=
-  Cases p of
-      xH => [n:nat] Cases n of
-                        O => true
-		      | (S _) => false
-		    end
-    | (xO p) => [n:nat] Cases n of
-                            O => false
-			  | (S n') => (ad_bit_1 p n')
-		        end
-    | (xI p) => [n:nat] Cases n of
-                            O => true
-			  | (S n') => (ad_bit_1 p n')
-		        end
+Fixpoint ad_bit_1 (p:positive) : nat -> bool :=
+  match p with
+  | xH => fun n:nat => match n with
+                       | O => true
+                       | S _ => false
+                       end
+  | xO p =>
+      fun n:nat => match n with
+                   | O => false
+                   | S n' => ad_bit_1 p n'
+                   end
+  | xI p => fun n:nat => match n with
+                         | O => true
+                         | S n' => ad_bit_1 p n'
+                         end
   end.
 
-Definition ad_bit := [a:ad]
-  Cases a of
-      ad_z => [_:nat] false
-    | (ad_x p) => (ad_bit_1 p)
+Definition ad_bit (a:ad) :=
+  match a with
+  | ad_z => fun _:nat => false
+  | ad_x p => ad_bit_1 p
   end.
 
-Definition eqf := [f,g:nat->bool] (n:nat) (f n)=(g n).
+Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n.
 
-Lemma ad_faithful_1 : (a:ad) (eqf (ad_bit ad_z) (ad_bit a)) -> ad_z=a.
+Lemma ad_faithful_1 : forall a:ad, eqf (ad_bit ad_z) (ad_bit a) -> ad_z = a.
 Proof.
-  NewDestruct a. Trivial.
-  NewInduction p as [p IHp|p IHp|];Intro H. Absurd ad_z=(ad_x p). Discriminate.
-  Exact (IHp [n:nat](H (S n))).
-  Absurd ad_z=(ad_x p). Discriminate.
-  Exact (IHp [n:nat](H (S n))).
-  Absurd false=true. Discriminate.
-  Exact (H O).
+  destruct a. trivial.
+  induction p as [p IHp| p IHp| ]; intro H. absurd (ad_z = ad_x p). discriminate.
+  exact (IHp (fun n:nat => H (S n))).
+  absurd (ad_z = ad_x p). discriminate.
+  exact (IHp (fun n:nat => H (S n))).
+  absurd (false = true). discriminate.
+  exact (H 0).
 Qed.
 
-Lemma ad_faithful_2 : (a:ad) (eqf (ad_bit (ad_x xH)) (ad_bit a)) -> (ad_x xH)=a.
+Lemma ad_faithful_2 :
+ forall a:ad, eqf (ad_bit (ad_x 1)) (ad_bit a) -> ad_x 1 = a.
 Proof.
-  NewDestruct a. Intros. Absurd true=false. Discriminate.
-  Exact (H O).
-  NewDestruct p. Intro H. Absurd ad_z=(ad_x p). Discriminate.
-  Exact (ad_faithful_1 (ad_x p) [n:nat](H (S n))).
-  Intros. Absurd true=false. Discriminate.
-  Exact (H O).
-  Trivial.
+  destruct a. intros. absurd (true = false). discriminate.
+  exact (H 0).
+  destruct p. intro H. absurd (ad_z = ad_x p). discriminate.
+  exact (ad_faithful_1 (ad_x p) (fun n:nat => H (S n))).
+  intros. absurd (true = false). discriminate.
+  exact (H 0).
+  trivial.
 Qed.
 
 Lemma ad_faithful_3 :
-    (a:ad) (p:positive)
-      ((p':positive) (eqf (ad_bit (ad_x p)) (ad_bit (ad_x p'))) -> p=p') ->
-        (eqf (ad_bit (ad_x (xO p))) (ad_bit a)) ->
-          (ad_x (xO p))=a.
+ forall (a:ad) (p:positive),
+   (forall p':positive, eqf (ad_bit (ad_x p)) (ad_bit (ad_x p')) -> p = p') ->
+   eqf (ad_bit (ad_x (xO p))) (ad_bit a) -> ad_x (xO p) = a.
 Proof.
-  NewDestruct a. Intros. Cut (eqf (ad_bit ad_z) (ad_bit (ad_x (xO p)))).
-  Intro. Rewrite (ad_faithful_1 (ad_x (xO p)) H1). Reflexivity.
-  Unfold eqf. Intro. Unfold eqf in H0. Rewrite H0. Reflexivity.
-  Case p. Intros. Absurd false=true. Discriminate.
-  Exact (H0 O).
-  Intros. Rewrite (H p0 [n:nat](H0 (S n))). Reflexivity.
-  Intros. Absurd false=true. Discriminate.
-  Exact (H0 O).
+  destruct a. intros. cut (eqf (ad_bit ad_z) (ad_bit (ad_x (xO p)))).
+  intro. rewrite (ad_faithful_1 (ad_x (xO p)) H1). reflexivity.
+  unfold eqf in |- *. intro. unfold eqf in H0. rewrite H0. reflexivity.
+  case p. intros. absurd (false = true). discriminate.
+  exact (H0 0).
+  intros. rewrite (H p0 (fun n:nat => H0 (S n))). reflexivity.
+  intros. absurd (false = true). discriminate.
+  exact (H0 0).
 Qed.
 
 Lemma ad_faithful_4 :
-    (a:ad) (p:positive)
-      ((p':positive) (eqf (ad_bit (ad_x p)) (ad_bit (ad_x p'))) -> p=p') ->
-        (eqf (ad_bit (ad_x (xI p))) (ad_bit a)) ->
-          (ad_x (xI p))=a.
+ forall (a:ad) (p:positive),
+   (forall p':positive, eqf (ad_bit (ad_x p)) (ad_bit (ad_x p')) -> p = p') ->
+   eqf (ad_bit (ad_x (xI p))) (ad_bit a) -> ad_x (xI p) = a.
 Proof.
-  NewDestruct a. Intros. Cut (eqf (ad_bit ad_z) (ad_bit (ad_x (xI p)))).
-  Intro. Rewrite (ad_faithful_1 (ad_x (xI p)) H1). Reflexivity.
-  Unfold eqf. Intro. Unfold eqf in H0. Rewrite H0. Reflexivity.
-  Case p. Intros. Rewrite (H p0 [n:nat](H0 (S n))). Reflexivity.
-  Intros. Absurd true=false. Discriminate.
-  Exact (H0 O).
-  Intros. Absurd ad_z=(ad_x p0). Discriminate.
-  Cut (eqf (ad_bit (ad_x xH)) (ad_bit (ad_x (xI p0)))).
-  Intro. Exact (ad_faithful_1 (ad_x p0) [n:nat](H1 (S n))).
-  Unfold eqf. Unfold eqf in H0. Intro. Rewrite H0. Reflexivity.
+  destruct a. intros. cut (eqf (ad_bit ad_z) (ad_bit (ad_x (xI p)))).
+  intro. rewrite (ad_faithful_1 (ad_x (xI p)) H1). reflexivity.
+  unfold eqf in |- *. intro. unfold eqf in H0. rewrite H0. reflexivity.
+  case p. intros. rewrite (H p0 (fun n:nat => H0 (S n))). reflexivity.
+  intros. absurd (true = false). discriminate.
+  exact (H0 0).
+  intros. absurd (ad_z = ad_x p0). discriminate.
+  cut (eqf (ad_bit (ad_x 1)) (ad_bit (ad_x (xI p0)))).
+  intro. exact (ad_faithful_1 (ad_x p0) (fun n:nat => H1 (S n))).
+  unfold eqf in |- *. unfold eqf in H0. intro. rewrite H0. reflexivity.
 Qed.
 
-Lemma ad_faithful : (a,a':ad) (eqf (ad_bit a) (ad_bit a')) -> a=a'.
+Lemma ad_faithful : forall a a':ad, eqf (ad_bit a) (ad_bit a') -> a = a'.
 Proof.
-  NewDestruct a. Exact ad_faithful_1.
-  NewInduction p. Intros a' H. Apply ad_faithful_4. Intros. Cut (ad_x p)=(ad_x p').
-  Intro. Inversion H1. Reflexivity.
-  Exact (IHp (ad_x p') H0).
-  Assumption.
-  Intros. Apply ad_faithful_3. Intros. Cut (ad_x p)=(ad_x p'). Intro. Inversion H1. Reflexivity.
-  Exact (IHp (ad_x p') H0).
-  Assumption.
-  Exact ad_faithful_2.
+  destruct a. exact ad_faithful_1.
+  induction p. intros a' H. apply ad_faithful_4. intros. cut (ad_x p = ad_x p').
+  intro. inversion H1. reflexivity.
+  exact (IHp (ad_x p') H0).
+  assumption.
+  intros. apply ad_faithful_3. intros. cut (ad_x p = ad_x p'). intro. inversion H1. reflexivity.
+  exact (IHp (ad_x p') H0).
+  assumption.
+  exact ad_faithful_2.
 Qed.
 
-Definition adf_xor := [f,g:nat->bool; n:nat] (xorb (f n) (g n)).
+Definition adf_xor (f g:nat -> bool) (n:nat) := xorb (f n) (g n).
 
-Lemma ad_xor_sem_1 : (a':ad) (ad_bit (ad_xor ad_z a') O)=(ad_bit a' O).
+Lemma ad_xor_sem_1 : forall a':ad, ad_bit (ad_xor ad_z a') 0 = ad_bit a' 0.
 Proof.
-  Trivial.
+  trivial.
 Qed.
 
-Lemma ad_xor_sem_2 : (a':ad) (ad_bit (ad_xor (ad_x xH) a') O)=(negb (ad_bit a' O)).
+Lemma ad_xor_sem_2 :
+ forall a':ad, ad_bit (ad_xor (ad_x 1) a') 0 = negb (ad_bit a' 0).
 Proof.
-  Intro. Case a'. Trivial.
-  Simpl. Intro. 
-  Case p; Trivial.
+  intro. case a'. trivial.
+  simpl in |- *. intro. 
+  case p; trivial.
 Qed.
 
 Lemma ad_xor_sem_3 :
-    (p:positive) (a':ad) (ad_bit (ad_xor (ad_x (xO p)) a') O)=(ad_bit a' O).
+ forall (p:positive) (a':ad),
+   ad_bit (ad_xor (ad_x (xO p)) a') 0 = ad_bit a' 0.
 Proof.
-  Intros. Case a'. Trivial.
-  Simpl. Intro. 
-  Case p0; Trivial. Intro. 
-  Case (p_xor p p1); Trivial.
-  Intro. Case (p_xor p p1); Trivial.
+  intros. case a'. trivial.
+  simpl in |- *. intro. 
+  case p0; trivial. intro. 
+  case (p_xor p p1); trivial.
+  intro. case (p_xor p p1); trivial.
 Qed.
 
-Lemma ad_xor_sem_4 : (p:positive) (a':ad)
-    (ad_bit (ad_xor (ad_x (xI p)) a') O)=(negb (ad_bit a' O)).
+Lemma ad_xor_sem_4 :
+ forall (p:positive) (a':ad),
+   ad_bit (ad_xor (ad_x (xI p)) a') 0 = negb (ad_bit a' 0).
 Proof.
-  Intros. Case a'. Trivial.
-  Simpl. Intro. Case p0; Trivial. Intro. 
-  Case (p_xor p p1); Trivial.
-  Intro. 
-  Case (p_xor p p1); Trivial.
+  intros. case a'. trivial.
+  simpl in |- *. intro. case p0; trivial. intro. 
+  case (p_xor p p1); trivial.
+  intro. 
+  case (p_xor p p1); trivial.
 Qed.
 
 Lemma ad_xor_sem_5 :
-    (a,a':ad) (ad_bit (ad_xor a a') O)=(adf_xor (ad_bit a) (ad_bit a') O).
-Proof.
-  NewDestruct a. Intro. Change (ad_bit a' O)=(xorb false (ad_bit a' O)). Rewrite false_xorb. Trivial.
-  Case p. Exact ad_xor_sem_4.
-  Intros. Change (ad_bit (ad_xor (ad_x (xO p0)) a') O)=(xorb false (ad_bit a' O)).
-  Rewrite false_xorb. Apply ad_xor_sem_3. Exact ad_xor_sem_2.
-Qed.
-
-Lemma ad_xor_sem_6 : (n:nat)
-    ((a,a':ad) (ad_bit (ad_xor a a') n)=(adf_xor (ad_bit a) (ad_bit a') n)) ->
-      (a,a':ad) (ad_bit (ad_xor a a') (S n))=(adf_xor (ad_bit a) (ad_bit a') (S n)).
-Proof.
-  Intros. Case a. Unfold adf_xor. Unfold 2 ad_bit. Rewrite false_xorb. Reflexivity.
-  Case a'. Unfold adf_xor. Unfold 3 ad_bit. Intro. Rewrite xorb_false. Reflexivity.
-  Intros. Case p0. Case p. Intros.
-  Change (ad_bit (ad_xor (ad_x (xI p2)) (ad_x (xI p1))) (S n))
-        =(adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n).
-  Rewrite <- H. Simpl. 
-  Case (p_xor p2 p1); Trivial.
-  Intros.
-  Change (ad_bit (ad_xor (ad_x (xI p2)) (ad_x (xO p1))) (S n))
-        =(adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n).
-  Rewrite <- H. Simpl. 
-  Case (p_xor p2 p1); Trivial.
-  Intro. Unfold adf_xor. Unfold 3 ad_bit. Unfold ad_bit_1. Rewrite xorb_false. Reflexivity.
-  Case p. Intros.
-  Change (ad_bit (ad_xor (ad_x (xO p2)) (ad_x (xI p1))) (S n))
-        =(adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n).
-  Rewrite <- H. Simpl. 
-  Case (p_xor p2 p1); Trivial.
-  Intros.
-  Change (ad_bit (ad_xor (ad_x (xO p2)) (ad_x (xO p1))) (S n))
-        =(adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n).
-  Rewrite <- H. Simpl. 
-  Case (p_xor p2 p1); Trivial.
-  Intro. Unfold adf_xor. Unfold 3 ad_bit. Unfold ad_bit_1. Rewrite xorb_false. Reflexivity.
-  Unfold adf_xor. Unfold 2 ad_bit. Unfold ad_bit_1. Rewrite false_xorb. Simpl.   Case p; Trivial.
+ forall a a':ad, ad_bit (ad_xor a a') 0 = adf_xor (ad_bit a) (ad_bit a') 0.
+Proof.
+  destruct a. intro. change (ad_bit a' 0 = xorb false (ad_bit a' 0)) in |- *. rewrite false_xorb. trivial.
+  case p. exact ad_xor_sem_4.
+  intros. change (ad_bit (ad_xor (ad_x (xO p0)) a') 0 = xorb false (ad_bit a' 0))
+  in |- *.
+  rewrite false_xorb. apply ad_xor_sem_3. exact ad_xor_sem_2.
+Qed.
+
+Lemma ad_xor_sem_6 :
+ forall n:nat,
+   (forall a a':ad, ad_bit (ad_xor a a') n = adf_xor (ad_bit a) (ad_bit a') n) ->
+   forall a a':ad,
+     ad_bit (ad_xor a a') (S n) = adf_xor (ad_bit a) (ad_bit a') (S n).
+Proof.
+  intros. case a. unfold adf_xor in |- *. unfold ad_bit at 2 in |- *. rewrite false_xorb. reflexivity.
+  case a'. unfold adf_xor in |- *. unfold ad_bit at 3 in |- *. intro. rewrite xorb_false. reflexivity.
+  intros. case p0. case p. intros.
+  change
+    (ad_bit (ad_xor (ad_x (xI p2)) (ad_x (xI p1))) (S n) =
+     adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n) 
+   in |- *.
+  rewrite <- H. simpl in |- *. 
+  case (p_xor p2 p1); trivial.
+  intros.
+  change
+    (ad_bit (ad_xor (ad_x (xI p2)) (ad_x (xO p1))) (S n) =
+     adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n) 
+   in |- *.
+  rewrite <- H. simpl in |- *. 
+  case (p_xor p2 p1); trivial.
+  intro. unfold adf_xor in |- *. unfold ad_bit at 3 in |- *. unfold ad_bit_1 in |- *. rewrite xorb_false. reflexivity.
+  case p. intros.
+  change
+    (ad_bit (ad_xor (ad_x (xO p2)) (ad_x (xI p1))) (S n) =
+     adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n) 
+   in |- *.
+  rewrite <- H. simpl in |- *. 
+  case (p_xor p2 p1); trivial.
+  intros.
+  change
+    (ad_bit (ad_xor (ad_x (xO p2)) (ad_x (xO p1))) (S n) =
+     adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n) 
+   in |- *.
+  rewrite <- H. simpl in |- *. 
+  case (p_xor p2 p1); trivial.
+  intro. unfold adf_xor in |- *. unfold ad_bit at 3 in |- *. unfold ad_bit_1 in |- *. rewrite xorb_false. reflexivity.
+  unfold adf_xor in |- *. unfold ad_bit at 2 in |- *. unfold ad_bit_1 in |- *. rewrite false_xorb. simpl in |- *.   case p; trivial.
 Qed.
 
 Lemma ad_xor_semantics :
-    (a,a':ad) (eqf (ad_bit (ad_xor a a')) (adf_xor (ad_bit a) (ad_bit a'))).
+ forall a a':ad, eqf (ad_bit (ad_xor a a')) (adf_xor (ad_bit a) (ad_bit a')).
 Proof.
-  Unfold eqf. Intros. Generalize a a'. Elim n. Exact ad_xor_sem_5.
-  Exact ad_xor_sem_6.
+  unfold eqf in |- *. intros. generalize a a'. elim n. exact ad_xor_sem_5.
+  exact ad_xor_sem_6.
 Qed.
 
-Lemma eqf_sym : (f,f':nat->bool) (eqf f f') -> (eqf f' f).
+Lemma eqf_sym : forall f f':nat -> bool, eqf f f' -> eqf f' f.
 Proof.
-  Unfold eqf. Intros. Rewrite H. Reflexivity.
+  unfold eqf in |- *. intros. rewrite H. reflexivity.
 Qed.
 
-Lemma eqf_refl :  (f:nat->bool) (eqf f f).
+Lemma eqf_refl : forall f:nat -> bool, eqf f f.
 Proof.
-  Unfold eqf. Trivial.
+  unfold eqf in |- *. trivial.
 Qed.
 
-Lemma eqf_trans : (f,f',f'':nat->bool) (eqf f f') -> (eqf f' f'') -> (eqf f f'').
+Lemma eqf_trans :
+ forall f f' f'':nat -> bool, eqf f f' -> eqf f' f'' -> eqf f f''.
 Proof.
-  Unfold eqf. Intros. Rewrite H. Exact (H0 n).
+  unfold eqf in |- *. intros. rewrite H. exact (H0 n).
 Qed.
 
-Lemma adf_xor_eq : (f,f':nat->bool) (eqf (adf_xor f f') [n:nat] false) -> (eqf f f').
+Lemma adf_xor_eq :
+ forall f f':nat -> bool, eqf (adf_xor f f') (fun n:nat => false) -> eqf f f'.
 Proof.
-  Unfold eqf. Unfold adf_xor. Intros. Apply xorb_eq. Apply H.
+  unfold eqf in |- *. unfold adf_xor in |- *. intros. apply xorb_eq. apply H.
 Qed.
 
-Lemma ad_xor_eq : (a,a':ad) (ad_xor a a')=ad_z -> a=a'.
+Lemma ad_xor_eq : forall a a':ad, ad_xor a a' = ad_z -> a = a'.
 Proof.
-  Intros. Apply ad_faithful. Apply adf_xor_eq. Apply eqf_trans with f':=(ad_bit (ad_xor a a')).
-  Apply eqf_sym. Apply ad_xor_semantics.
-  Rewrite H. Unfold eqf. Trivial.
+  intros. apply ad_faithful. apply adf_xor_eq. apply eqf_trans with (f' := ad_bit (ad_xor a a')).
+  apply eqf_sym. apply ad_xor_semantics.
+  rewrite H. unfold eqf in |- *. trivial.
 Qed.
 
-Lemma adf_xor_assoc : (f,f',f'':nat->bool)
-    (eqf (adf_xor (adf_xor f f') f'') (adf_xor f (adf_xor f' f''))).
+Lemma adf_xor_assoc :
+ forall f f' f'':nat -> bool,
+   eqf (adf_xor (adf_xor f f') f'') (adf_xor f (adf_xor f' f'')).
 Proof.
-  Unfold eqf. Unfold adf_xor. Intros. Apply xorb_assoc.
+  unfold eqf in |- *. unfold adf_xor in |- *. intros. apply xorb_assoc.
 Qed.
 
-Lemma eqf_xor_1 : (f,f',f'',f''':nat->bool) (eqf f f') -> (eqf f'' f''') ->
-    (eqf (adf_xor f f'') (adf_xor f' f''')).
+Lemma eqf_xor_1 :
+ forall f f' f'' f''':nat -> bool,
+   eqf f f' -> eqf f'' f''' -> eqf (adf_xor f f'') (adf_xor f' f''').
 Proof.
-  Unfold eqf. Intros. Unfold adf_xor. Rewrite H. Rewrite H0. Reflexivity.
+  unfold eqf in |- *. intros. unfold adf_xor in |- *. rewrite H. rewrite H0. reflexivity.
 Qed.
 
 Lemma ad_xor_assoc :
-    (a,a',a'':ad) (ad_xor (ad_xor a a') a'')=(ad_xor a (ad_xor a' a'')).
-Proof.
-  Intros. Apply ad_faithful.
-  Apply eqf_trans with f':=(adf_xor (adf_xor (ad_bit a) (ad_bit a')) (ad_bit a'')).
-  Apply eqf_trans with f':=(adf_xor (ad_bit (ad_xor a a')) (ad_bit a'')).
-  Apply ad_xor_semantics.
-  Apply eqf_xor_1. Apply ad_xor_semantics.
-  Apply eqf_refl.
-  Apply eqf_trans with f':=(adf_xor (ad_bit a) (adf_xor (ad_bit a') (ad_bit a''))).
-  Apply adf_xor_assoc.
-  Apply eqf_trans with f':=(adf_xor (ad_bit a) (ad_bit (ad_xor a' a''))).
-  Apply eqf_xor_1. Apply eqf_refl.
-  Apply eqf_sym. Apply ad_xor_semantics.
-  Apply eqf_sym. Apply ad_xor_semantics.
-Qed.
-
-Definition ad_double := [a:ad]
-  Cases a of
-      ad_z => ad_z
-    | (ad_x p) => (ad_x (xO p))
+ forall a a' a'':ad, ad_xor (ad_xor a a') a'' = ad_xor a (ad_xor a' a'').
+Proof.
+  intros. apply ad_faithful.
+  apply eqf_trans with
+   (f' := adf_xor (adf_xor (ad_bit a) (ad_bit a')) (ad_bit a'')).
+  apply eqf_trans with (f' := adf_xor (ad_bit (ad_xor a a')) (ad_bit a'')).
+  apply ad_xor_semantics.
+  apply eqf_xor_1. apply ad_xor_semantics.
+  apply eqf_refl.
+  apply eqf_trans with
+   (f' := adf_xor (ad_bit a) (adf_xor (ad_bit a') (ad_bit a''))).
+  apply adf_xor_assoc.
+  apply eqf_trans with (f' := adf_xor (ad_bit a) (ad_bit (ad_xor a' a''))).
+  apply eqf_xor_1. apply eqf_refl.
+  apply eqf_sym. apply ad_xor_semantics.
+  apply eqf_sym. apply ad_xor_semantics.
+Qed.
+
+Definition ad_double (a:ad) :=
+  match a with
+  | ad_z => ad_z
+  | ad_x p => ad_x (xO p)
   end.
 
-Definition ad_double_plus_un := [a:ad]
-  Cases a of
-      ad_z => (ad_x xH)
-    | (ad_x p) => (ad_x (xI p))
+Definition ad_double_plus_un (a:ad) :=
+  match a with
+  | ad_z => ad_x 1
+  | ad_x p => ad_x (xI p)
   end.
 
-Definition ad_div_2 := [a:ad]
-  Cases a of
-      ad_z => ad_z
-    | (ad_x xH) => ad_z
-    | (ad_x (xO p)) => (ad_x p)
-    | (ad_x (xI p)) => (ad_x p)
+Definition ad_div_2 (a:ad) :=
+  match a with
+  | ad_z => ad_z
+  | ad_x xH => ad_z
+  | ad_x (xO p) => ad_x p
+  | ad_x (xI p) => ad_x p
   end.
 
-Lemma ad_double_div_2 : (a:ad) (ad_div_2 (ad_double a))=a.
+Lemma ad_double_div_2 : forall a:ad, ad_div_2 (ad_double a) = a.
 Proof.
-  NewDestruct a; Trivial.
+  destruct a; trivial.
 Qed.
 
-Lemma ad_double_plus_un_div_2 : (a:ad) (ad_div_2 (ad_double_plus_un a))=a.
+Lemma ad_double_plus_un_div_2 :
+ forall a:ad, ad_div_2 (ad_double_plus_un a) = a.
 Proof.
-  NewDestruct a; Trivial.
+  destruct a; trivial.
 Qed.
 
-Lemma ad_double_inj : (a0,a1:ad) (ad_double a0)=(ad_double a1) -> a0=a1.
+Lemma ad_double_inj : forall a0 a1:ad, ad_double a0 = ad_double a1 -> a0 = a1.
 Proof.
-  Intros. Rewrite <- (ad_double_div_2 a0). Rewrite H. Apply ad_double_div_2.
+  intros. rewrite <- (ad_double_div_2 a0). rewrite H. apply ad_double_div_2.
 Qed.
 
 Lemma ad_double_plus_un_inj :
-    (a0,a1:ad) (ad_double_plus_un a0)=(ad_double_plus_un a1) -> a0=a1.
+ forall a0 a1:ad, ad_double_plus_un a0 = ad_double_plus_un a1 -> a0 = a1.
 Proof.
-  Intros. Rewrite <- (ad_double_plus_un_div_2 a0). Rewrite H. Apply ad_double_plus_un_div_2.
+  intros. rewrite <- (ad_double_plus_un_div_2 a0). rewrite H. apply ad_double_plus_un_div_2.
 Qed.
 
-Definition ad_bit_0 := [a:ad]
-  Cases a of
-      ad_z => false
-    | (ad_x (xO _)) => false
-    | _ => true
+Definition ad_bit_0 (a:ad) :=
+  match a with
+  | ad_z => false
+  | ad_x (xO _) => false
+  | _ => true
   end.
 
-Lemma ad_double_bit_0 : (a:ad) (ad_bit_0 (ad_double a))=false.
+Lemma ad_double_bit_0 : forall a:ad, ad_bit_0 (ad_double a) = false.
 Proof.
-  NewDestruct a; Trivial.
+  destruct a; trivial.
 Qed.
 
-Lemma ad_double_plus_un_bit_0 : (a:ad) (ad_bit_0 (ad_double_plus_un a))=true.
+Lemma ad_double_plus_un_bit_0 :
+ forall a:ad, ad_bit_0 (ad_double_plus_un a) = true.
 Proof.
-  NewDestruct a; Trivial.
+  destruct a; trivial.
 Qed.
 
-Lemma ad_div_2_double : (a:ad) (ad_bit_0 a)=false -> (ad_double (ad_div_2 a))=a.
+Lemma ad_div_2_double :
+ forall a:ad, ad_bit_0 a = false -> ad_double (ad_div_2 a) = a.
 Proof.
-  NewDestruct a. Trivial. NewDestruct p. Intro H. Discriminate H.
-  Intros. Reflexivity.
-  Intro H. Discriminate H.
+  destruct a. trivial. destruct p. intro H. discriminate H.
+  intros. reflexivity.
+  intro H. discriminate H.
 Qed.
 
 Lemma ad_div_2_double_plus_un :
-    (a:ad) (ad_bit_0 a)=true -> (ad_double_plus_un (ad_div_2 a))=a.
+ forall a:ad, ad_bit_0 a = true -> ad_double_plus_un (ad_div_2 a) = a.
 Proof.
-  NewDestruct a. Intro. Discriminate H.
-  NewDestruct p. Intros. Reflexivity.
-  Intro H. Discriminate H.
-  Intro. Reflexivity.
+  destruct a. intro. discriminate H.
+  destruct p. intros. reflexivity.
+  intro H. discriminate H.
+  intro. reflexivity.
 Qed.
 
-Lemma ad_bit_0_correct : (a:ad) (ad_bit a O)=(ad_bit_0 a).
+Lemma ad_bit_0_correct : forall a:ad, ad_bit a 0 = ad_bit_0 a.
 Proof.
-  NewDestruct a; Trivial.
-  NewDestruct p; Trivial.
+  destruct a; trivial.
+  destruct p; trivial.
 Qed.
 
-Lemma ad_div_2_correct : (a:ad) (n:nat) (ad_bit (ad_div_2 a) n)=(ad_bit a (S n)).
+Lemma ad_div_2_correct :
+ forall (a:ad) (n:nat), ad_bit (ad_div_2 a) n = ad_bit a (S n).
 Proof.
-  NewDestruct a; Trivial.
-  NewDestruct p; Trivial.
+  destruct a; trivial.
+  destruct p; trivial.
 Qed.
 
 Lemma ad_xor_bit_0 :
-    (a,a':ad) (ad_bit_0 (ad_xor a a'))=(xorb (ad_bit_0 a) (ad_bit_0 a')).
+ forall a a':ad, ad_bit_0 (ad_xor a a') = xorb (ad_bit_0 a) (ad_bit_0 a').
 Proof.
-  Intros. Rewrite <- ad_bit_0_correct. Rewrite (ad_xor_semantics a a' O).
-  Unfold adf_xor. Rewrite ad_bit_0_correct. Rewrite ad_bit_0_correct. Reflexivity.
+  intros. rewrite <- ad_bit_0_correct. rewrite (ad_xor_semantics a a' 0).
+  unfold adf_xor in |- *. rewrite ad_bit_0_correct. rewrite ad_bit_0_correct. reflexivity.
 Qed.
 
 Lemma ad_xor_div_2 :
-    (a,a':ad) (ad_div_2 (ad_xor a a'))=(ad_xor (ad_div_2 a) (ad_div_2 a')).
+ forall a a':ad, ad_div_2 (ad_xor a a') = ad_xor (ad_div_2 a) (ad_div_2 a').
 Proof.
-  Intros. Apply ad_faithful. Unfold eqf. Intro.
-  Rewrite (ad_xor_semantics (ad_div_2 a) (ad_div_2 a') n).
-  Rewrite ad_div_2_correct.
-  Rewrite (ad_xor_semantics a a' (S n)).
-  Unfold adf_xor. Rewrite ad_div_2_correct. Rewrite ad_div_2_correct.
-  Reflexivity.
+  intros. apply ad_faithful. unfold eqf in |- *. intro.
+  rewrite (ad_xor_semantics (ad_div_2 a) (ad_div_2 a') n).
+  rewrite ad_div_2_correct.
+  rewrite (ad_xor_semantics a a' (S n)).
+  unfold adf_xor in |- *. rewrite ad_div_2_correct. rewrite ad_div_2_correct.
+  reflexivity.
 Qed.
 
-Lemma ad_neg_bit_0 : (a,a':ad) (ad_bit_0 (ad_xor a a'))=true ->
-    (ad_bit_0 a)=(negb (ad_bit_0 a')).
+Lemma ad_neg_bit_0 :
+ forall a a':ad,
+   ad_bit_0 (ad_xor a a') = true -> ad_bit_0 a = negb (ad_bit_0 a').
 Proof.
-  Intros. Rewrite <- true_xorb. Rewrite <- H. Rewrite ad_xor_bit_0.
-  Rewrite xorb_assoc. Rewrite xorb_nilpotent. Rewrite xorb_false. Reflexivity.
+  intros. rewrite <- true_xorb. rewrite <- H. rewrite ad_xor_bit_0.
+  rewrite xorb_assoc. rewrite xorb_nilpotent. rewrite xorb_false. reflexivity.
 Qed.
 
 Lemma ad_neg_bit_0_1 :
-    (a,a':ad) (ad_xor a a')=(ad_x xH) -> (ad_bit_0 a)=(negb (ad_bit_0 a')).
+ forall a a':ad, ad_xor a a' = ad_x 1 -> ad_bit_0 a = negb (ad_bit_0 a').
 Proof.
-  Intros. Apply ad_neg_bit_0. Rewrite H. Reflexivity.
+  intros. apply ad_neg_bit_0. rewrite H. reflexivity.
 Qed.
 
-Lemma ad_neg_bit_0_2 : (a,a':ad) (p:positive) (ad_xor a a')=(ad_x (xI p)) ->
-    (ad_bit_0 a)=(negb (ad_bit_0 a')).
+Lemma ad_neg_bit_0_2 :
+ forall (a a':ad) (p:positive),
+   ad_xor a a' = ad_x (xI p) -> ad_bit_0 a = negb (ad_bit_0 a').
 Proof.
-  Intros. Apply ad_neg_bit_0. Rewrite H. Reflexivity.
+  intros. apply ad_neg_bit_0. rewrite H. reflexivity.
 Qed.
 
-Lemma ad_same_bit_0 : (a,a':ad) (p:positive) (ad_xor a a')=(ad_x (xO p)) ->
-    (ad_bit_0 a)=(ad_bit_0 a').
+Lemma ad_same_bit_0 :
+ forall (a a':ad) (p:positive),
+   ad_xor a a' = ad_x (xO p) -> ad_bit_0 a = ad_bit_0 a'.
 Proof.
-  Intros. Rewrite <- (xorb_false (ad_bit_0 a)). Cut (ad_bit_0 (ad_x (xO p)))=false.
-  Intro. Rewrite <- H0. Rewrite <- H. Rewrite ad_xor_bit_0. Rewrite <- xorb_assoc.
-  Rewrite xorb_nilpotent. Rewrite false_xorb. Reflexivity.
-  Reflexivity.
-Qed.
+  intros. rewrite <- (xorb_false (ad_bit_0 a)). cut (ad_bit_0 (ad_x (xO p)) = false).
+  intro. rewrite <- H0. rewrite <- H. rewrite ad_xor_bit_0. rewrite <- xorb_assoc.
+  rewrite xorb_nilpotent. rewrite false_xorb. reflexivity.
+  reflexivity.
+Qed.
\ No newline at end of file