From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- theories/IntMap/Addec.v | 193 ------------------------------------------------ 1 file changed, 193 deletions(-) delete mode 100644 theories/IntMap/Addec.v (limited to 'theories/IntMap/Addec.v') diff --git a/theories/IntMap/Addec.v b/theories/IntMap/Addec.v deleted file mode 100644 index f1a937a3..00000000 --- a/theories/IntMap/Addec.v +++ /dev/null @@ -1,193 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* true - | xO p'1, xO p'2 => ad_eq_1 p'1 p'2 - | xI p'1, xI p'2 => ad_eq_1 p'1 p'2 - | _, _ => false - end. - -Definition ad_eq (a a':ad) := - match a, a' with - | ad_z, ad_z => true - | ad_x p, ad_x p' => ad_eq_1 p p' - | _, _ => false - end. - -Lemma ad_eq_correct : forall a:ad, ad_eq a a = true. -Proof. - destruct a; trivial. - induction p; trivial. -Qed. - -Lemma ad_eq_complete : forall a a':ad, ad_eq a a' = true -> a = a'. -Proof. - destruct a. destruct a'; trivial. destruct p. - discriminate 1. - discriminate 1. - discriminate 1. - destruct a'. intros. discriminate H. - unfold ad_eq in |- *. intros. cut (p = p0). intros. rewrite H0. reflexivity. - generalize dependent p0. - induction p as [p IHp| p IHp| ]. destruct p0; intro H. - rewrite (IHp p0). reflexivity. - exact H. - discriminate H. - discriminate H. - destruct p0; intro H. discriminate H. - rewrite (IHp p0 H). reflexivity. - discriminate H. - destruct p0 as [p| p| ]; intro H. discriminate H. - discriminate H. - trivial. -Qed. - -Lemma ad_eq_comm : forall a a':ad, ad_eq a a' = ad_eq a' a. -Proof. - intros. cut (forall b b':bool, ad_eq a a' = b -> ad_eq a' a = b' -> b = b'). - intros. apply H. reflexivity. - reflexivity. - destruct b. intros. cut (a = a'). - intro. rewrite H1 in H0. rewrite (ad_eq_correct a') in H0. exact H0. - apply ad_eq_complete. exact H. - destruct b'. intros. cut (a' = a). - intro. rewrite H1 in H. rewrite H1 in H0. rewrite <- H. exact H0. - apply ad_eq_complete. exact H0. - trivial. -Qed. - -Lemma ad_xor_eq_true : - forall a a':ad, ad_xor a a' = ad_z -> ad_eq a a' = true. -Proof. - intros. rewrite (ad_xor_eq a a' H). apply ad_eq_correct. -Qed. - -Lemma ad_xor_eq_false : - forall (a a':ad) (p:positive), ad_xor a a' = ad_x p -> ad_eq a a' = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq a a')). intro H0. - rewrite (ad_eq_complete a a' H0) in H. rewrite (ad_xor_nilpotent a') in H. discriminate H. - trivial. -Qed. - -Lemma ad_bit_0_1_not_double : - forall a:ad, - ad_bit_0 a = true -> forall a0:ad, ad_eq (ad_double a0) a = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq (ad_double a0) a)). intro H0. - rewrite <- (ad_eq_complete _ _ H0) in H. rewrite (ad_double_bit_0 a0) in H. discriminate H. - trivial. -Qed. - -Lemma ad_not_div_2_not_double : - forall a a0:ad, - ad_eq (ad_div_2 a) a0 = false -> ad_eq a (ad_double a0) = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq (ad_double a0) a)). intro H0. - rewrite <- (ad_eq_complete _ _ H0) in H. rewrite (ad_double_div_2 a0) in H. - rewrite (ad_eq_correct a0) in H. discriminate H. - intro. rewrite ad_eq_comm. assumption. -Qed. - -Lemma ad_bit_0_0_not_double_plus_un : - forall a:ad, - ad_bit_0 a = false -> forall a0:ad, ad_eq (ad_double_plus_un a0) a = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq (ad_double_plus_un a0) a)). intro H0. - rewrite <- (ad_eq_complete _ _ H0) in H. rewrite (ad_double_plus_un_bit_0 a0) in H. - discriminate H. - trivial. -Qed. - -Lemma ad_not_div_2_not_double_plus_un : - forall a a0:ad, - ad_eq (ad_div_2 a) a0 = false -> ad_eq (ad_double_plus_un a0) a = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq a (ad_double_plus_un a0))). intro H0. - rewrite (ad_eq_complete _ _ H0) in H. rewrite (ad_double_plus_un_div_2 a0) in H. - rewrite (ad_eq_correct a0) in H. discriminate H. - intro H0. rewrite ad_eq_comm. assumption. -Qed. - -Lemma ad_bit_0_neq : - forall a a':ad, - ad_bit_0 a = false -> ad_bit_0 a' = true -> ad_eq a a' = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq a a')). intro H1. rewrite (ad_eq_complete _ _ H1) in H. - rewrite H in H0. discriminate H0. - trivial. -Qed. - -Lemma ad_div_eq : - forall a a':ad, ad_eq a a' = true -> ad_eq (ad_div_2 a) (ad_div_2 a') = true. -Proof. - intros. cut (a = a'). intros. rewrite H0. apply ad_eq_correct. - apply ad_eq_complete. exact H. -Qed. - -Lemma ad_div_neq : - forall a a':ad, - ad_eq (ad_div_2 a) (ad_div_2 a') = false -> ad_eq a a' = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq a a')). intro H0. - rewrite (ad_eq_complete _ _ H0) in H. rewrite (ad_eq_correct (ad_div_2 a')) in H. discriminate H. - trivial. -Qed. - -Lemma ad_div_bit_eq : - forall a a':ad, - ad_bit_0 a = ad_bit_0 a' -> ad_div_2 a = ad_div_2 a' -> a = a'. -Proof. - intros. apply ad_faithful. unfold eqf in |- *. destruct n. - rewrite ad_bit_0_correct. rewrite ad_bit_0_correct. assumption. - rewrite <- ad_div_2_correct. rewrite <- ad_div_2_correct. - rewrite H0. reflexivity. -Qed. - -Lemma ad_div_bit_neq : - forall a a':ad, - ad_eq a a' = false -> - ad_bit_0 a = ad_bit_0 a' -> ad_eq (ad_div_2 a) (ad_div_2 a') = false. -Proof. - intros. elim (sumbool_of_bool (ad_eq (ad_div_2 a) (ad_div_2 a'))). intro H1. - rewrite (ad_div_bit_eq _ _ H0 (ad_eq_complete _ _ H1)) in H. - rewrite (ad_eq_correct a') in H. discriminate H. - trivial. -Qed. - -Lemma ad_neq : - forall a a':ad, - ad_eq a a' = false -> - ad_bit_0 a = negb (ad_bit_0 a') \/ - ad_eq (ad_div_2 a) (ad_div_2 a') = false. -Proof. - intros. cut (ad_bit_0 a = ad_bit_0 a' \/ ad_bit_0 a = negb (ad_bit_0 a')). - intros. elim H0. intro. right. apply ad_div_bit_neq. assumption. - assumption. - intro. left. assumption. - case (ad_bit_0 a); case (ad_bit_0 a'); auto. -Qed. - -Lemma ad_double_or_double_plus_un : - forall a:ad, - {a0 : ad | a = ad_double a0} + {a1 : ad | a = ad_double_plus_un a1}. -Proof. - intro. elim (sumbool_of_bool (ad_bit_0 a)). intro H. right. split with (ad_div_2 a). - rewrite (ad_div_2_double_plus_un a H). reflexivity. - intro H. left. split with (ad_div_2 a). rewrite (ad_div_2_double a H). reflexivity. -Qed. \ No newline at end of file -- cgit v1.2.3