diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Coqlib.v | 709 | ||||
-rw-r--r-- | lib/Floats.v | 55 | ||||
-rw-r--r-- | lib/Inclusion.v | 367 | ||||
-rw-r--r-- | lib/Integers.v | 2184 | ||||
-rw-r--r-- | lib/Lattice.v | 331 | ||||
-rw-r--r-- | lib/Maps.v | 1034 | ||||
-rw-r--r-- | lib/Ordered.v | 156 | ||||
-rw-r--r-- | lib/Sets.v | 190 | ||||
-rw-r--r-- | lib/union_find.v | 537 |
9 files changed, 5563 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v new file mode 100644 index 00000000..039dd03b --- /dev/null +++ b/lib/Coqlib.v @@ -0,0 +1,709 @@ +(** This file collects a number of definitions and theorems that are + used throughout the development. It complements the Coq standard + library. *) + +Require Export ZArith. +Require Export List. +Require Import Wf_nat. + +(** * Logical axioms *) + +(** We use two logical axioms that are not provable in Coq but consistent + with the logic: function extensionality and proof irrelevance. + These are used in the memory model to show that two memory states + that have identical contents are equal. *) + +Axiom extensionality: + forall (A B: Set) (f g : A -> B), + (forall x, f x = g x) -> f = g. + +Axiom proof_irrelevance: + forall (P: Prop) (p1 p2: P), p1 = p2. + +(** * Useful tactics *) + +Ltac predSpec pred predspec x y := + generalize (predspec x y); case (pred x y); intro. + +Ltac caseEq name := + generalize (refl_equal name); pattern name at -1 in |- *; case name. + +Ltac destructEq name := + generalize (refl_equal name); pattern name at -1 in |- *; destruct name; intro. + +Ltac decEq := + match goal with + | [ |- (_, _) = (_, _) ] => + apply injective_projections; unfold fst,snd; try reflexivity + | [ |- (@Some ?T _ = @Some ?T _) ] => + apply (f_equal (@Some T)); try reflexivity + | [ |- (?X _ _ _ _ _ = ?X _ _ _ _ _) ] => + apply (f_equal5 X); try reflexivity + | [ |- (?X _ _ _ _ = ?X _ _ _ _) ] => + apply (f_equal4 X); try reflexivity + | [ |- (?X _ _ _ = ?X _ _ _) ] => + apply (f_equal3 X); try reflexivity + | [ |- (?X _ _ = ?X _ _) ] => + apply (f_equal2 X); try reflexivity + | [ |- (?X _ = ?X _) ] => + apply (f_equal X); try reflexivity + | [ |- (?X ?A <> ?X ?B) ] => + cut (A <> B); [intro; congruence | try discriminate] + end. + +Ltac byContradiction := + cut False; [contradiction|idtac]. + +Ltac omegaContradiction := + cut False; [contradiction|omega]. + +(** * Definitions and theorems over the type [positive] *) + +Definition peq (x y: positive): {x = y} + {x <> y}. +Proof. + intros. caseEq (Pcompare x y Eq). + intro. left. apply Pcompare_Eq_eq; auto. + intro. right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate. + intro. right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate. +Qed. + +Lemma peq_true: + forall (A: Set) (x: positive) (a b: A), (if peq x x then a else b) = a. +Proof. + intros. case (peq x x); intros. + auto. + elim n; auto. +Qed. + +Lemma peq_false: + forall (A: Set) (x y: positive) (a b: A), x <> y -> (if peq x y then a else b) = b. +Proof. + intros. case (peq x y); intros. + elim H; auto. + auto. +Qed. + +Definition Plt (x y: positive): Prop := Zlt (Zpos x) (Zpos y). + +Lemma Plt_ne: + forall (x y: positive), Plt x y -> x <> y. +Proof. + unfold Plt; intros. red; intro. subst y. omega. +Qed. +Hint Resolve Plt_ne: coqlib. + +Lemma Plt_trans: + forall (x y z: positive), Plt x y -> Plt y z -> Plt x z. +Proof. + unfold Plt; intros; omega. +Qed. + +Remark Psucc_Zsucc: + forall (x: positive), Zpos (Psucc x) = Zsucc (Zpos x). +Proof. + intros. rewrite Pplus_one_succ_r. + reflexivity. +Qed. + +Lemma Plt_succ: + forall (x: positive), Plt x (Psucc x). +Proof. + intro. unfold Plt. rewrite Psucc_Zsucc. omega. +Qed. +Hint Resolve Plt_succ: coqlib. + +Lemma Plt_trans_succ: + forall (x y: positive), Plt x y -> Plt x (Psucc y). +Proof. + intros. apply Plt_trans with y. assumption. apply Plt_succ. +Qed. +Hint Resolve Plt_succ: coqlib. + +Lemma Plt_succ_inv: + forall (x y: positive), Plt x (Psucc y) -> Plt x y \/ x = y. +Proof. + intros x y. unfold Plt. rewrite Psucc_Zsucc. + intro. assert (A: (Zpos x < Zpos y)%Z \/ Zpos x = Zpos y). omega. + elim A; intro. left; auto. right; injection H0; auto. +Qed. + +Definition plt (x y: positive) : {Plt x y} + {~ Plt x y}. +Proof. + intros. unfold Plt. apply Z_lt_dec. +Qed. + +Definition Ple (p q: positive) := Zle (Zpos p) (Zpos q). + +Lemma Ple_refl: forall (p: positive), Ple p p. +Proof. + unfold Ple; intros; omega. +Qed. + +Lemma Ple_trans: forall (p q r: positive), Ple p q -> Ple q r -> Ple p r. +Proof. + unfold Ple; intros; omega. +Qed. + +Lemma Plt_Ple: forall (p q: positive), Plt p q -> Ple p q. +Proof. + unfold Plt, Ple; intros; omega. +Qed. + +Lemma Ple_succ: forall (p: positive), Ple p (Psucc p). +Proof. + intros. apply Plt_Ple. apply Plt_succ. +Qed. + +Lemma Plt_Ple_trans: + forall (p q r: positive), Plt p q -> Ple q r -> Plt p r. +Proof. + unfold Plt, Ple; intros; omega. +Qed. + +Lemma Plt_strict: forall p, ~ Plt p p. +Proof. + unfold Plt; intros. omega. +Qed. + +Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib. + +(** Peano recursion over positive numbers. *) + +Section POSITIVE_ITERATION. + +Lemma Plt_wf: well_founded Plt. +Proof. + apply well_founded_lt_compat with nat_of_P. + intros. apply nat_of_P_lt_Lt_compare_morphism. exact H. +Qed. + +Variable A: Set. +Variable v1: A. +Variable f: positive -> A -> A. + +Lemma Ppred_Plt: + forall x, x <> xH -> Plt (Ppred x) x. +Proof. + intros. elim (Psucc_pred x); intro. contradiction. + set (y := Ppred x) in *. rewrite <- H0. apply Plt_succ. +Qed. + +Let iter (x: positive) (P: forall y, Plt y x -> A) : A := + match peq x xH with + | left EQ => v1 + | right NOTEQ => f (Ppred x) (P (Ppred x) (Ppred_Plt x NOTEQ)) + end. + +Definition positive_rec : positive -> A := + Fix Plt_wf (fun _ => A) iter. + +Lemma unroll_positive_rec: + forall x, + positive_rec x = iter x (fun y _ => positive_rec y). +Proof. + unfold positive_rec. apply (Fix_eq Plt_wf (fun _ => A) iter). + intros. unfold iter. case (peq x 1); intro. auto. decEq. apply H. +Qed. + +Lemma positive_rec_base: + positive_rec 1%positive = v1. +Proof. + rewrite unroll_positive_rec. unfold iter. case (peq 1 1); intro. + auto. elim n; auto. +Qed. + +Lemma positive_rec_succ: + forall x, positive_rec (Psucc x) = f x (positive_rec x). +Proof. + intro. rewrite unroll_positive_rec. unfold iter. + case (peq (Psucc x) 1); intro. + destruct x; simpl in e; discriminate. + rewrite Ppred_succ. auto. +Qed. + +Lemma positive_Peano_ind: + forall (P: positive -> Prop), + P xH -> + (forall x, P x -> P (Psucc x)) -> + forall x, P x. +Proof. + intros. + apply (well_founded_ind Plt_wf P). + intros. + case (peq x0 xH); intro. + subst x0; auto. + elim (Psucc_pred x0); intro. contradiction. rewrite <- H2. + apply H0. apply H1. apply Ppred_Plt. auto. +Qed. + +End POSITIVE_ITERATION. + +(** * Definitions and theorems over the type [Z] *) + +Definition zeq: forall (x y: Z), {x = y} + {x <> y} := Z_eq_dec. + +Lemma zeq_true: + forall (A: Set) (x: Z) (a b: A), (if zeq x x then a else b) = a. +Proof. + intros. case (zeq x x); intros. + auto. + elim n; auto. +Qed. + +Lemma zeq_false: + forall (A: Set) (x y: Z) (a b: A), x <> y -> (if zeq x y then a else b) = b. +Proof. + intros. case (zeq x y); intros. + elim H; auto. + auto. +Qed. + +Open Scope Z_scope. + +Definition zlt: forall (x y: Z), {x < y} + {x >= y} := Z_lt_ge_dec. + +Lemma zlt_true: + forall (A: Set) (x y: Z) (a b: A), + x < y -> (if zlt x y then a else b) = a. +Proof. + intros. case (zlt x y); intros. + auto. + omegaContradiction. +Qed. + +Lemma zlt_false: + forall (A: Set) (x y: Z) (a b: A), + x >= y -> (if zlt x y then a else b) = b. +Proof. + intros. case (zlt x y); intros. + omegaContradiction. + auto. +Qed. + +Definition zle: forall (x y: Z), {x <= y} + {x > y} := Z_le_gt_dec. + +Lemma zle_true: + forall (A: Set) (x y: Z) (a b: A), + x <= y -> (if zle x y then a else b) = a. +Proof. + intros. case (zle x y); intros. + auto. + omegaContradiction. +Qed. + +Lemma zle_false: + forall (A: Set) (x y: Z) (a b: A), + x > y -> (if zle x y then a else b) = b. +Proof. + intros. case (zle x y); intros. + omegaContradiction. + auto. +Qed. + +(** Properties of powers of two. *) + +Lemma two_power_nat_O : two_power_nat O = 1. +Proof. reflexivity. Qed. + +Lemma two_power_nat_pos : forall n : nat, two_power_nat n > 0. +Proof. + induction n. rewrite two_power_nat_O. omega. + rewrite two_power_nat_S. omega. +Qed. + +(** Properties of [Zmin] and [Zmax] *) + +Lemma Zmin_spec: + forall x y, Zmin x y = if zlt x y then x else y. +Proof. + intros. case (zlt x y); unfold Zlt, Zge; intros. + unfold Zmin. rewrite z. auto. + unfold Zmin. caseEq (x ?= y); intro. + apply Zcompare_Eq_eq. auto. + contradiction. + reflexivity. +Qed. + +Lemma Zmax_spec: + forall x y, Zmax x y = if zlt y x then x else y. +Proof. + intros. case (zlt y x); unfold Zlt, Zge; intros. + unfold Zmax. rewrite <- (Zcompare_antisym y x). + rewrite z. simpl. auto. + unfold Zmax. rewrite <- (Zcompare_antisym y x). + caseEq (y ?= x); intro; simpl. + symmetry. apply Zcompare_Eq_eq. auto. + contradiction. reflexivity. +Qed. + +Lemma Zmax_bound_l: + forall x y z, x <= y -> x <= Zmax y z. +Proof. + intros. generalize (Zmax1 y z). omega. +Qed. +Lemma Zmax_bound_r: + forall x y z, x <= z -> x <= Zmax y z. +Proof. + intros. generalize (Zmax2 y z). omega. +Qed. + +(** Properties of Euclidean division and modulus. *) + +Lemma Zdiv_small: + forall x y, 0 <= x < y -> x / y = 0. +Proof. + intros. assert (y > 0). omega. + assert (forall a b, + 0 <= a < y -> + 0 <= y * b + a < y -> + b = 0). + intros. + assert (b = 0 \/ b > 0 \/ (-b) > 0). omega. + elim H3; intro. + auto. + elim H4; intro. + assert (y * b >= y * 1). apply Zmult_ge_compat_l. omega. omega. + omegaContradiction. + assert (y * (-b) >= y * 1). apply Zmult_ge_compat_l. omega. omega. + rewrite <- Zopp_mult_distr_r in H6. omegaContradiction. + apply H1 with (x mod y). + apply Z_mod_lt. auto. + rewrite <- Z_div_mod_eq. auto. auto. +Qed. + +Lemma Zmod_small: + forall x y, 0 <= x < y -> x mod y = x. +Proof. + intros. assert (y > 0). omega. + generalize (Z_div_mod_eq x y H0). + rewrite (Zdiv_small x y H). omega. +Qed. + +Lemma Zmod_unique: + forall x y a b, + x = a * y + b -> 0 <= b < y -> x mod y = b. +Proof. + intros. subst x. rewrite Zplus_comm. + rewrite Z_mod_plus. apply Zmod_small. auto. omega. +Qed. + +Lemma Zdiv_unique: + forall x y a b, + x = a * y + b -> 0 <= b < y -> x / y = a. +Proof. + intros. subst x. rewrite Zplus_comm. + rewrite Z_div_plus. rewrite (Zdiv_small b y H0). omega. omega. +Qed. + +(** Alignment: [align n amount] returns the smallest multiple of [amount] + greater than or equal to [n]. *) + +Definition align (n: Z) (amount: Z) := + ((n + amount - 1) / amount) * amount. + +Lemma align_le: forall x y, y > 0 -> x <= align x y. +Proof. + intros. unfold align. + generalize (Z_div_mod_eq (x + y - 1) y H). intro. + replace ((x + y - 1) / y * y) + with ((x + y - 1) - (x + y - 1) mod y). + generalize (Z_mod_lt (x + y - 1) y H). omega. + rewrite Zmult_comm. omega. +Qed. + +(** * Definitions and theorems on the data types [option], [sum] and [list] *) + +Set Implicit Arguments. + +(** Mapping a function over an option type. *) + +Definition option_map (A B: Set) (f: A -> B) (x: option A) : option B := + match x with + | None => None + | Some y => Some (f y) + end. + +(** Mapping a function over a sum type. *) + +Definition sum_left_map (A B C: Set) (f: A -> B) (x: A + C) : B + C := + match x with + | inl y => inl C (f y) + | inr z => inr B z + end. + +(** Properties of [List.nth] (n-th element of a list). *) + +Hint Resolve in_eq in_cons: coqlib. + +Lemma nth_error_in: + forall (A: Set) (n: nat) (l: list A) (x: A), + List.nth_error l n = Some x -> In x l. +Proof. + induction n; simpl. + destruct l; intros. + discriminate. + injection H; intro; subst a. apply in_eq. + destruct l; intros. + discriminate. + apply in_cons. auto. +Qed. +Hint Resolve nth_error_in: coqlib. + +Lemma nth_error_nil: + forall (A: Set) (idx: nat), nth_error (@nil A) idx = None. +Proof. + induction idx; simpl; intros; reflexivity. +Qed. +Hint Resolve nth_error_nil: coqlib. + +(** Properties of [List.incl] (list inclusion). *) + +Lemma incl_cons_inv: + forall (A: Set) (a: A) (b c: list A), + incl (a :: b) c -> incl b c. +Proof. + unfold incl; intros. apply H. apply in_cons. auto. +Qed. +Hint Resolve incl_cons_inv: coqlib. + +Lemma incl_app_inv_l: + forall (A: Set) (l1 l2 m: list A), + incl (l1 ++ l2) m -> incl l1 m. +Proof. + unfold incl; intros. apply H. apply in_or_app. left; assumption. +Qed. + +Lemma incl_app_inv_r: + forall (A: Set) (l1 l2 m: list A), + incl (l1 ++ l2) m -> incl l2 m. +Proof. + unfold incl; intros. apply H. apply in_or_app. right; assumption. +Qed. + +Hint Resolve incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib. + +Lemma incl_same_head: + forall (A: Set) (x: A) (l1 l2: list A), + incl l1 l2 -> incl (x::l1) (x::l2). +Proof. + intros; red; simpl; intros. intuition. +Qed. + +(** Properties of [List.map] (mapping a function over a list). *) + +Lemma list_map_exten: + forall (A B: Set) (f f': A -> B) (l: list A), + (forall x, In x l -> f x = f' x) -> + List.map f' l = List.map f l. +Proof. + induction l; simpl; intros. + reflexivity. + rewrite <- H. rewrite IHl. reflexivity. + intros. apply H. tauto. + tauto. +Qed. + +Lemma list_map_compose: + forall (A B C: Set) (f: A -> B) (g: B -> C) (l: list A), + List.map g (List.map f l) = List.map (fun x => g(f x)) l. +Proof. + induction l; simpl. reflexivity. rewrite IHl; reflexivity. +Qed. + +Lemma list_map_nth: + forall (A B: Set) (f: A -> B) (l: list A) (n: nat), + nth_error (List.map f l) n = option_map f (nth_error l n). +Proof. + induction l; simpl; intros. + repeat rewrite nth_error_nil. reflexivity. + destruct n; simpl. reflexivity. auto. +Qed. + +Lemma list_length_map: + forall (A B: Set) (f: A -> B) (l: list A), + List.length (List.map f l) = List.length l. +Proof. + induction l; simpl; congruence. +Qed. + +Lemma list_in_map_inv: + forall (A B: Set) (f: A -> B) (l: list A) (y: B), + In y (List.map f l) -> exists x:A, y = f x /\ In x l. +Proof. + induction l; simpl; intros. + contradiction. + elim H; intro. + exists a; intuition auto. + generalize (IHl y H0). intros [x [EQ IN]]. + exists x; tauto. +Qed. + +Lemma list_append_map: + forall (A B: Set) (f: A -> B) (l1 l2: list A), + List.map f (l1 ++ l2) = List.map f l1 ++ List.map f l2. +Proof. + induction l1; simpl; intros. + auto. rewrite IHl1. auto. +Qed. + +(** [list_disjoint l1 l2] holds iff [l1] and [l2] have no elements + in common. *) + +Definition list_disjoint (A: Set) (l1 l2: list A) : Prop := + forall (x y: A), In x l1 -> In y l2 -> x <> y. + +Lemma list_disjoint_cons_left: + forall (A: Set) (a: A) (l1 l2: list A), + list_disjoint (a :: l1) l2 -> list_disjoint l1 l2. +Proof. + unfold list_disjoint; simpl; intros. apply H; tauto. +Qed. + +Lemma list_disjoint_cons_right: + forall (A: Set) (a: A) (l1 l2: list A), + list_disjoint l1 (a :: l2) -> list_disjoint l1 l2. +Proof. + unfold list_disjoint; simpl; intros. apply H; tauto. +Qed. + +Lemma list_disjoint_notin: + forall (A: Set) (l1 l2: list A) (a: A), + list_disjoint l1 l2 -> In a l1 -> ~(In a l2). +Proof. + unfold list_disjoint; intros; red; intros. + apply H with a a; auto. +Qed. + +Lemma list_disjoint_sym: + forall (A: Set) (l1 l2: list A), + list_disjoint l1 l2 -> list_disjoint l2 l1. +Proof. + unfold list_disjoint; intros. + apply sym_not_equal. apply H; auto. +Qed. + +(** [list_norepet l] holds iff the list [l] contains no repetitions, + i.e. no element occurs twice. *) + +Inductive list_norepet (A: Set) : list A -> Prop := + | list_norepet_nil: + list_norepet nil + | list_norepet_cons: + forall hd tl, + ~(In hd tl) -> list_norepet tl -> list_norepet (hd :: tl). + +Lemma list_norepet_dec: + forall (A: Set) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l: list A), + {list_norepet l} + {~list_norepet l}. +Proof. + induction l. + left; constructor. + destruct IHl. + case (In_dec eqA_dec a l); intro. + right. red; intro. inversion H. contradiction. + left. constructor; auto. + right. red; intro. inversion H. contradiction. +Qed. + +Lemma list_map_norepet: + forall (A B: Set) (f: A -> B) (l: list A), + list_norepet l -> + (forall x y, In x l -> In y l -> x <> y -> f x <> f y) -> + list_norepet (List.map f l). +Proof. + induction 1; simpl; intros. + constructor. + constructor. + red; intro. generalize (list_in_map_inv f _ _ H2). + intros [x [EQ IN]]. generalize EQ. change (f hd <> f x). + apply H1. tauto. tauto. + red; intro; subst x. contradiction. + apply IHlist_norepet. intros. apply H1. tauto. tauto. auto. +Qed. + +Remark list_norepet_append_commut: + forall (A: Set) (a b: list A), + list_norepet (a ++ b) -> list_norepet (b ++ a). +Proof. + intro A. + assert (forall (x: A) (b: list A) (a: list A), + list_norepet (a ++ b) -> ~(In x a) -> ~(In x b) -> + list_norepet (a ++ x :: b)). + induction a; simpl; intros. + constructor; auto. + inversion H. constructor. red; intro. + elim (in_app_or _ _ _ H6); intro. + elim H4. apply in_or_app. tauto. + elim H7; intro. subst a. elim H0. left. auto. + elim H4. apply in_or_app. tauto. + auto. + induction a; simpl; intros. + rewrite <- app_nil_end. auto. + inversion H0. apply H. auto. + red; intro; elim H3. apply in_or_app. tauto. + red; intro; elim H3. apply in_or_app. tauto. +Qed. + +Lemma list_norepet_append: + forall (A: Set) (l1 l2: list A), + list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 -> + list_norepet (l1 ++ l2). +Proof. + induction l1; simpl; intros. + auto. + inversion H. subst hd tl. + constructor. red; intro. apply (H1 a a). auto with coqlib. + elim (in_app_or _ _ _ H2); tauto. auto. + apply IHl1. auto. auto. + red; intros; apply H1; auto with coqlib. +Qed. + +Lemma list_norepet_append_right: + forall (A: Set) (l1 l2: list A), + list_norepet (l1 ++ l2) -> list_norepet l2. +Proof. + induction l1; intros. + assumption. + simpl in H. inversion H. eauto. +Qed. + +Lemma list_norepet_append_left: + forall (A: Set) (l1 l2: list A), + list_norepet (l1 ++ l2) -> list_norepet l1. +Proof. + intros. apply list_norepet_append_right with l2. + apply list_norepet_append_commut. auto. +Qed. + +(** [list_forall2 P [x1 ... xN] [y1 ... yM] holds iff [N = M] and + [P xi yi] holds for all [i]. *) + +Section FORALL2. + +Variable A: Set. +Variable B: Set. +Variable P: A -> B -> Prop. + +Inductive list_forall2: list A -> list B -> Prop := + | list_forall2_nil: + list_forall2 nil nil + | list_forall2_cons: + forall a1 al b1 bl, + P a1 b1 -> + list_forall2 al bl -> + list_forall2 (a1 :: al) (b1 :: bl). + +End FORALL2. + +Lemma list_forall2_imply: + forall (A B: Set) (P1: A -> B -> Prop) (l1: list A) (l2: list B), + list_forall2 P1 l1 l2 -> + forall (P2: A -> B -> Prop), + (forall v1 v2, In v1 l1 -> In v2 l2 -> P1 v1 v2 -> P2 v1 v2) -> + list_forall2 P2 l1 l2. +Proof. + induction 1; intros. + constructor. + constructor. auto with coqlib. apply IHlist_forall2; auto. + intros. auto with coqlib. +Qed. diff --git a/lib/Floats.v b/lib/Floats.v new file mode 100644 index 00000000..b95789e6 --- /dev/null +++ b/lib/Floats.v @@ -0,0 +1,55 @@ +(** Axiomatization of floating-point numbers. *) + +(** In contrast with what we do with machine integers, we do not bother + to formalize precisely IEEE floating-point arithmetic. Instead, we + simply axiomatize a type [float] for IEEE double-precision floats + and the associated operations. *) + +Require Import Bool. +Require Import AST. +Require Import Integers. + +Parameter float: Set. + +Module Float. + +Parameter zero: float. +Parameter one: float. + +Parameter neg: float -> float. +Parameter abs: float -> float. +Parameter singleoffloat: float -> float. +Parameter intoffloat: float -> int. +Parameter floatofint: int -> float. +Parameter floatofintu: int -> float. + +Parameter add: float -> float -> float. +Parameter sub: float -> float -> float. +Parameter mul: float -> float -> float. +Parameter div: float -> float -> float. + +Parameter cmp: comparison -> float -> float -> bool. + +Axiom eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2}. + +(** Below are the only properties of floating-point arithmetic that we + rely on in the compiler proof. *) + +Axiom addf_commut: forall f1 f2, add f1 f2 = add f2 f1. + +Axiom subf_addf_opp: forall f1 f2, sub f1 f2 = add f1 (neg f2). + +Axiom singleoffloat_idem: + forall f, singleoffloat (singleoffloat f) = singleoffloat f. + +Axiom cmp_ne_eq: + forall f1 f2, cmp Cne f1 f2 = negb (cmp Ceq f1 f2). +Axiom cmp_le_lt_eq: + forall f1 f2, cmp Cle f1 f2 = cmp Clt f1 f2 || cmp Ceq f1 f2. +Axiom cmp_ge_gt_eq: + forall f1 f2, cmp Cge f1 f2 = cmp Cgt f1 f2 || cmp Ceq f1 f2. + +Axiom eq_zero_true: cmp Ceq zero zero = true. +Axiom eq_zero_false: forall f, f <> zero -> cmp Ceq f zero = false. + +End Float. diff --git a/lib/Inclusion.v b/lib/Inclusion.v new file mode 100644 index 00000000..1df7517f --- /dev/null +++ b/lib/Inclusion.v @@ -0,0 +1,367 @@ +(** Tactics to reason about list inclusion. *) + +(** This file (contributed by Laurence Rideau) defines a tactic [in_tac] + to reason over list inclusion. It expects goals of the following form: +<< + id : In x l1 + ============================ + In x l2 +>> +and succeeds if it can prove that [l1] is included in [l2]. +The lists [l1] and [l2] must belong to the following sub-language [L] +<< + L ::= L++L | E | E::L +>> +The tactic uses no extra fact. + +A second tactic, [incl_tac], handles goals of the form +<< + ============================= + incl l1 l2 +>> +*) + +Require Import List. +Require Import ArithRing. + +Ltac all_app e := + match e with + | cons ?x nil => constr:(cons x nil) + | cons ?x ?tl => + let v := all_app tl in constr:(app (cons x nil) v) + | app ?e1 ?e2 => + let v1 := all_app e1 with v2 := all_app e2 in + constr:(app v1 v2) + | _ => e + end. + +(** This data type, [flatten], [insert_bin], [sort_bin] and a few theorem + are taken from the CoqArt book, chapt. 16. *) + +Inductive bin : Set := node : bin->bin->bin | leaf : nat->bin. + +Fixpoint flatten_aux (t fin:bin){struct t} : bin := + match t with + | node t1 t2 => flatten_aux t1 (flatten_aux t2 fin) + | x => node x fin + end. + +Fixpoint flatten (t:bin) : bin := + match t with + | node t1 t2 => flatten_aux t1 (flatten t2) + | x => x + end. + +Fixpoint nat_le_bool (n m:nat){struct m} : bool := + match n, m with + | O, _ => true + | S _, O => false + | S n, S m => nat_le_bool n m + end. + +Fixpoint insert_bin (n:nat)(t:bin){struct t} : bin := + match t with + | leaf m => + if nat_le_bool n m then + node (leaf n)(leaf m) + else + node (leaf m)(leaf n) + | node (leaf m) t' => + if nat_le_bool n m then node (leaf n) t else node (leaf m)(insert_bin n t') + | t => node (leaf n) t + end. + +Fixpoint sort_bin (t:bin) : bin := + match t with + | node (leaf n) t' => insert_bin n (sort_bin t') + | t => t + end. + +Section assoc_eq. + Variables (A : Set)(f : A->A->A). + Hypothesis assoc : forall x y z:A, f x (f y z) = f (f x y) z. + + Fixpoint bin_A (l:list A)(def:A)(t:bin){struct t} : A := + match t with + | node t1 t2 => f (bin_A l def t1)(bin_A l def t2) + | leaf n => nth n l def + end. + + Theorem flatten_aux_valid_A : + forall (l:list A)(def:A)(t t':bin), + f (bin_A l def t)(bin_A l def t') = bin_A l def (flatten_aux t t'). + Proof. + intros l def t; elim t; simpl; auto. + intros t1 IHt1 t2 IHt2 t'; rewrite <- IHt1; rewrite <- IHt2. + symmetry; apply assoc. + Qed. + + Theorem flatten_valid_A : + forall (l:list A)(def:A)(t:bin), + bin_A l def t = bin_A l def (flatten t). + Proof. + intros l def t; elim t; simpl; trivial. + intros t1 IHt1 t2 IHt2; rewrite <- flatten_aux_valid_A; rewrite <- IHt2. + trivial. + Qed. + +End assoc_eq. + +Ltac compute_rank l n v := + match l with + | (cons ?X1 ?X2) => + let tl := constr:X2 in + match constr:(X1 = v) with + | (?X1 = ?X1) => n + | _ => compute_rank tl (S n) v + end + end. + +Ltac term_list_app l v := + match v with + | (app ?X1 ?X2) => + let l1 := term_list_app l X2 in term_list_app l1 X1 + | ?X1 => constr:(cons X1 l) + end. + +Ltac model_aux_app l v := + match v with + | (app ?X1 ?X2) => + let r1 := model_aux_app l X1 with r2 := model_aux_app l X2 in + constr:(node r1 r2) + | ?X1 => let n := compute_rank l 0 X1 in constr:(leaf n) + | _ => constr:(leaf 0) + end. + +Theorem In_permute_app_head : + forall A:Set, forall r:A, forall x y l:list A, + In r (x++y++l) -> In r (y++x++l). +intros A r x y l; generalize r; change (incl (x++y++l)(y++x++l)). +repeat rewrite ass_app; auto with datatypes. +Qed. + +Theorem insert_bin_included : + forall x:nat, forall t2:bin, + forall (A:Set) (r:A) (l:list (list A))(def:list A), + In r (bin_A (list A) (app (A:=A)) l def (insert_bin x t2)) -> + In r (bin_A (list A) (app (A:=A)) l def (node (leaf x) t2)). +intros x t2; induction t2. +intros A r l def. +destruct t2_1 as [t2_11 t2_12|y]. +simpl. +repeat rewrite app_ass. +auto. +simpl; repeat rewrite app_ass. +simpl; case (nat_le_bool x y); simpl. +auto. +intros H; apply In_permute_app_head. +elim in_app_or with (1:= H); clear H; intros H. +apply in_or_app; left; assumption. +apply in_or_app; right;apply (IHt2_2 A r l);assumption. +intros A r l def; simpl. +case (nat_le_bool x n); simpl. +auto. +intros H. +rewrite (app_nil_end (nth x l def)) in H. +rewrite (app_nil_end (nth n l def)). +apply In_permute_app_head; assumption. +Qed. + +Theorem in_or_insert_bin : + forall (n:nat) (t2:bin) (A:Set)(r:A)(l:list (list A)) (def:list A), + In r (nth n l def) \/ In r (bin_A (list A)(app (A:=A)) l def t2) -> + In r (bin_A (list A)(app (A:=A)) l def (insert_bin n t2)). +intros n t2 A r l def; induction t2. +destruct t2_1 as [t2_11 t2_12| y]. +simpl; apply in_or_app. +simpl; case (nat_le_bool n y); simpl. +intros H. +apply in_or_app. +exact H. +intros [H|H]. +apply in_or_app; right; apply IHt2_2; auto. +elim in_app_or with (1:= H);clear H; intros H; apply in_or_app; auto. +simpl; intros [H|H]; case (nat_le_bool n n0); simpl; apply in_or_app; auto. +Qed. + +Theorem sort_included : + forall t:bin, forall (A:Set)(r:A)(l:list(list A))(def:list A), + In r (bin_A (list A) (app (A:=A)) l def (sort_bin t)) -> + In r (bin_A (list A) (app (A:=A)) l def t). +induction t. +destruct t1. +simpl;intros; assumption. +intros A r l def H; simpl in H; apply insert_bin_included. +generalize (insert_bin_included _ _ _ _ _ _ H); clear H; intros H. +simpl in H. +elim in_app_or with (1 := H);clear H; intros H; +apply in_or_insert_bin; auto. +simpl;intros;assumption. +Qed. + +Theorem sort_included2 : + forall t:bin, forall (A:Set)(r:A)(l:list(list A))(def:list A), + In r (bin_A (list A) (app (A:=A)) l def t) -> + In r (bin_A (list A) (app (A:=A)) l def (sort_bin t)). +induction t. +destruct t1. +simpl; intros; assumption. +intros A r l def H; simpl in H. +simpl; apply in_or_insert_bin. +elim in_app_or with (1:= H); auto. +simpl; auto. +Qed. + +Theorem in_remove_head : + forall (A:Set)(x:A)(l1 l2 l3:list A), + In x (l1++l2) -> (In x l2 -> In x l3) -> In x (l1++l3). +intros A x l1 l2 l3 H H1. +elim in_app_or with (1:= H);clear H; intros H; apply in_or_app; auto. +Qed. + +Fixpoint check_all_leaves (n:nat)(t:bin) {struct t} : bool := + match t with + leaf n1 => nateq n n1 + | node t1 t2 => andb (check_all_leaves n t1)(check_all_leaves n t2) + end. + +Fixpoint remove_all_leaves (n:nat)(t:bin){struct t} : bin := + match t with + leaf n => leaf n + | node (leaf n1) t2 => + if nateq n n1 then remove_all_leaves n t2 else t + | _ => t + end. + +Fixpoint test_inclusion (t1 t2:bin) {struct t1} : bool := + match t1 with + leaf n => check_all_leaves n t2 + | node (leaf n1) t1' => + check_all_leaves n1 t2 || test_inclusion t1' (remove_all_leaves n1 t2) + | _ => false + end. + +Theorem check_all_leaves_sound : + forall x t2, + check_all_leaves x t2 = true -> + forall (A:Set)(r:A)(l:list(list A))(def:list A), + In r (bin_A (list A) (app (A:=A)) l def t2) -> + In r (nth x l def). +intros x t2; induction t2; simpl. +destruct (check_all_leaves x t2_1); +destruct (check_all_leaves x t2_2); simpl; intros Heq; try discriminate. +intros A r l def H; elim in_app_or with (1:= H); clear H; intros H; auto. +intros Heq A r l def; rewrite (nateq_prop x n); auto. +rewrite Heq; unfold Is_true; auto. +Qed. + +Theorem remove_all_leaves_sound : + forall x t2, + forall (A:Set)(r:A)(l:list(list A))(def:list A), + In r (bin_A (list A) (app(A:=A)) l def t2) -> + In r (bin_A (list A) (app(A:=A)) l def (remove_all_leaves x t2)) \/ + In r (nth x l def). +intros x t2; induction t2; simpl. +destruct t2_1. +simpl; auto. +intros A r l def. +generalize (refl_equal (nateq x n)); pattern (nateq x n) at -1; + case (nateq x n); simpl; auto. +intros Heq_nateq. +assert (Heq_xn : x=n). +apply nateq_prop; rewrite Heq_nateq;unfold Is_true;auto. +rewrite Heq_xn. +intros H; elim in_app_or with (1:= H); auto. +clear H; intros H. +rewrite Heq_xn in IHt2_2; auto. +auto. +Qed. + +Theorem test_inclusion_sound : + forall t1 t2:bin, + test_inclusion t1 t2 = true -> + forall (A:Set)(r:A)(l:list(list A))(def:list A), + In r (bin_A (list A)(app(A:=A)) l def t2) -> + In r (bin_A (list A)(app(A:=A)) l def t1). +intros t1; induction t1. +destruct t1_1 as [t1_11 t1_12|x]. +simpl; intros; discriminate. +simpl; intros t2 Heq A r l def H. +assert + (check_all_leaves x t2 = true \/ + test_inclusion t1_2 (remove_all_leaves x t2) = true). +destruct (check_all_leaves x t2); +destruct (test_inclusion t1_2 (remove_all_leaves x t2)); +simpl in Heq; try discriminate Heq; auto. +elim H0; clear H0; intros H0. +apply in_or_app; left; apply check_all_leaves_sound with (1:= H0); auto. +elim remove_all_leaves_sound with (x:=x)(1:= H); intros H'. +apply in_or_app; right; apply IHt1_2 with (1:= H0); auto. +apply in_or_app; auto. +simpl; apply check_all_leaves_sound. +Qed. + +Theorem inclusion_theorem : + forall t1 t2 : bin, + test_inclusion (sort_bin (flatten t1)) (sort_bin (flatten t2)) = true -> + forall (A:Set)(r:A)(l:list(list A))(def:list A), + In r (bin_A (list A) (app(A:=A)) l def t2) -> + In r (bin_A (list A) (app(A:=A)) l def t1). +intros t1 t2 Heq A r l def H. +rewrite flatten_valid_A with (t:= t1)(1:= (ass_app (A:= A))). +apply sort_included. +apply test_inclusion_sound with (t2 := sort_bin (flatten t2)). +assumption. +apply sort_included2. +rewrite <- flatten_valid_A with (1:= (ass_app (A:= A))). +assumption. +Qed. + +Ltac in_tac := + match goal with + | id : In ?x nil |- _ => elim id + | id : In ?x ?l1 |- In ?x ?l2 => + let t := type of x in + let v1 := all_app l1 in + let v2 := all_app l2 in + (let l := term_list_app (nil (A:=list t)) v2 in + let term1 := model_aux_app l v1 with + term2 := model_aux_app l v2 in + (change (In x (bin_A (list t) (app(A:=t)) l (nil(A:=t)) term2)); + apply inclusion_theorem with (t2:= term1);[apply refl_equal|exact id])) + end. + +Ltac incl_tac := + match goal with + |- incl _ _ => intro; intro; in_tac + end. + +(* Usage examples. + +Theorem ex1 : forall x y z:nat, forall l1 l2 : list nat, + In x (y::l1++l2) -> In x (l2++z::l1++(y::nil)). +intros. +in_tac. +Qed. + +Fixpoint mklist (f:nat->nat)(n:nat){struct n} : list nat := + match n with 0 => nil | S p => mklist f p++(f p::nil) end. + +(* At the time of writing these lines, this example takes about 5 seconds + for 40 elements and 22 seconds for 60 elements. + A variant to the example is to replace mklist f p++(f p::nil) with + f p::mklist f p, in this case the time is 6 seconds for 40 elements and + 35 seconds for 60 elements. *) + +Theorem ex2 : + forall x : nat, In x (mklist (fun y => y) 40) -> + In x (mklist (fun y => (40 - 1) - y) 40). +lazy beta iota zeta delta [mklist minus]. +intros. +in_tac. +Qed. + +(* The tactic could be made more efficient by using binary trees and + numbers of type positive instead of lists and natural numbers. *) + +*) diff --git a/lib/Integers.v b/lib/Integers.v new file mode 100644 index 00000000..6b605bd7 --- /dev/null +++ b/lib/Integers.v @@ -0,0 +1,2184 @@ +(** Formalizations of integers modulo $2^32$ #2<sup>32</sup>#. *) + +Require Import Coqlib. +Require Import AST. + +Definition wordsize : nat := 32%nat. +Definition modulus : Z := two_power_nat wordsize. +Definition half_modulus : Z := modulus / 2. + +(** * Representation of machine integers *) + +(** A machine integer (type [int]) is represented as a Coq arbitrary-precision + integer (type [Z]) plus a proof that it is in the range 0 (included) to + [modulus] (excluded. *) + +Definition in_range (x: Z) := + match x ?= 0 with + | Lt => False + | _ => + match x ?= modulus with + | Lt => True + | _ => False + end + end. + +Record int: Set := mkint { intval: Z; intrange: in_range intval }. + +Module Int. + +Definition max_unsigned : Z := modulus - 1. +Definition max_signed : Z := half_modulus - 1. +Definition min_signed : Z := - half_modulus. + +(** The [unsigned] and [signed] functions return the Coq integer corresponding + to the given machine integer, interpreted as unsigned or signed + respectively. *) + +Definition unsigned (n: int) : Z := intval n. + +Definition signed (n: int) : Z := + if zlt (unsigned n) half_modulus + then unsigned n + else unsigned n - modulus. + +Lemma mod_in_range: + forall x, in_range (Zmod x modulus). +Proof. + intro. + generalize (Z_mod_lt x modulus (two_power_nat_pos wordsize)). + intros [A B]. + assert (C: x mod modulus >= 0). omega. + red. red in C. red in B. + rewrite B. destruct (x mod modulus ?= 0); auto. +Qed. + +(** Conversely, [repr] takes a Coq integer and returns the corresponding + machine integer. The argument is treated modulo [modulus]. *) + +Definition repr (x: Z) : int := + mkint (Zmod x modulus) (mod_in_range x). + +Definition zero := repr 0. +Definition one := repr 1. +Definition mone := repr (-1). + +Lemma mkint_eq: + forall x y Px Py, x = y -> mkint x Px = mkint y Py. +Proof. + intros. subst y. + generalize (proof_irrelevance _ Px Py); intro. + subst Py. reflexivity. +Qed. + +Lemma eq_dec: forall (x y: int), {x = y} + {x <> y}. +Proof. + intros. destruct x; destruct y. case (zeq intval0 intval1); intro. + left. apply mkint_eq. auto. + right. red; intro. injection H. exact n. +Qed. + +(** * Arithmetic and logical operations over machine integers *) + +Definition eq (x y: int) : bool := + if zeq (unsigned x) (unsigned y) then true else false. +Definition lt (x y: int) : bool := + if zlt (signed x) (signed y) then true else false. +Definition ltu (x y: int) : bool := + if zlt (unsigned x) (unsigned y) then true else false. + +Definition neg (x: int) : int := repr (- unsigned x). +Definition cast8signed (x: int) : int := + let y := Zmod (unsigned x) 256 in + if zlt y 128 then repr y else repr (y - 256). +Definition cast8unsigned (x: int) : int := + repr (Zmod (unsigned x) 256). +Definition cast16signed (x: int) : int := + let y := Zmod (unsigned x) 65536 in + if zlt y 32768 then repr y else repr (y - 65536). +Definition cast16unsigned (x: int) : int := + repr (Zmod (unsigned x) 65536). + +Definition add (x y: int) : int := + repr (unsigned x + unsigned y). +Definition sub (x y: int) : int := + repr (unsigned x - unsigned y). +Definition mul (x y: int) : int := + repr (unsigned x * unsigned y). + +Definition Zdiv_round (x y: Z) : Z := + if zlt x 0 then + if zlt y 0 then (-x) / (-y) else - ((-x) / y) + else + if zlt y 0 then -(x / (-y)) else x / y. + +Definition Zmod_round (x y: Z) : Z := + x - (Zdiv_round x y) * y. + +Definition divs (x y: int) : int := + repr (Zdiv_round (signed x) (signed y)). +Definition mods (x y: int) : int := + repr (Zmod_round (signed x) (signed y)). +Definition divu (x y: int) : int := + repr (unsigned x / unsigned y). +Definition modu (x y: int) : int := + repr (Zmod (unsigned x) (unsigned y)). + +(** For bitwise operations, we need to convert between Coq integers [Z] + and their bit-level representations. Bit-level representations are + represented as characteristic functions, that is, functions [f] + of type [nat -> bool] such that [f i] is the value of the [i]-th bit + of the number. The values of characteristic functions for [i] greater + than 32 are ignored. *) + +Definition Z_shift_add (b: bool) (x: Z) := + if b then 2 * x + 1 else 2 * x. + +Definition Z_bin_decomp (x: Z) : bool * Z := + match x with + | Z0 => (false, 0) + | Zpos p => + match p with + | xI q => (true, Zpos q) + | xO q => (false, Zpos q) + | xH => (true, 0) + end + | Zneg p => + match p with + | xI q => (true, Zneg q - 1) + | xO q => (false, Zneg q) + | xH => (true, -1) + end + end. + +Fixpoint bits_of_Z (n: nat) (x: Z) {struct n}: Z -> bool := + match n with + | O => + (fun i: Z => false) + | S m => + let (b, y) := Z_bin_decomp x in + let f := bits_of_Z m y in + (fun i: Z => if zeq i 0 then b else f (i - 1)) + end. + +Fixpoint Z_of_bits (n: nat) (f: Z -> bool) {struct n}: Z := + match n with + | O => 0 + | S m => Z_shift_add (f 0) (Z_of_bits m (fun i => f (i + 1))) + end. + +(** Bitwise logical ``and'', ``or'' and ``xor'' operations. *) + +Definition bitwise_binop (f: bool -> bool -> bool) (x y: int) := + let fx := bits_of_Z wordsize (unsigned x) in + let fy := bits_of_Z wordsize (unsigned y) in + repr (Z_of_bits wordsize (fun i => f (fx i) (fy i))). + +Definition and (x y: int): int := bitwise_binop andb x y. +Definition or (x y: int): int := bitwise_binop orb x y. +Definition xor (x y: int) : int := bitwise_binop xorb x y. + +Definition not (x: int) : int := xor x mone. + +(** Shifts and rotates. *) + +Definition shl (x y: int): int := + let fx := bits_of_Z wordsize (unsigned x) in + let vy := unsigned y in + repr (Z_of_bits wordsize (fun i => fx (i - vy))). + +Definition shru (x y: int): int := + let fx := bits_of_Z wordsize (unsigned x) in + let vy := unsigned y in + repr (Z_of_bits wordsize (fun i => fx (i + vy))). + +(** Arithmetic right shift is defined as signed division by a power of two. + Two such shifts are defined: [shr] rounds towards minus infinity + (standard behaviour for arithmetic right shift) and + [shrx] rounds towards zero. *) + +Definition shr (x y: int): int := + repr (signed x / two_p (unsigned y)). +Definition shrx (x y: int): int := + divs x (shl one y). + +Definition shr_carry (x y: int) := + sub (shrx x y) (shr x y). + +Definition rol (x y: int) : int := + let fx := bits_of_Z wordsize (unsigned x) in + let vy := unsigned y in + repr (Z_of_bits wordsize + (fun i => fx (Zmod (i - vy) (Z_of_nat wordsize)))). + +Definition rolm (x a m: int): int := and (rol x a) m. + +(** Decomposition of a number as a sum of powers of two. *) + +Fixpoint Z_one_bits (n: nat) (x: Z) (i: Z) {struct n}: list Z := + match n with + | O => nil + | S m => + let (b, y) := Z_bin_decomp x in + if b then i :: Z_one_bits m y (i+1) else Z_one_bits m y (i+1) + end. + +Definition one_bits (x: int) : list int := + List.map repr (Z_one_bits wordsize (unsigned x) 0). + +(** Recognition of powers of two. *) + +Definition is_power2 (x: int) : option int := + match Z_one_bits wordsize (unsigned x) 0 with + | i :: nil => Some (repr i) + | _ => None + end. + +(** Recognition of integers that are acceptable as immediate operands + to the [rlwim] PowerPC instruction. These integers are of the form + [000011110000] or [111100001111], that is, a run of one bits + surrounded by zero bits, or conversely. We recognize these integers by + running the following automaton on the bits. The accepting states are + 2, 3, 4, 5, and 6. +<< + 0 1 0 + / \ / \ / \ + \ / \ / \ / + -0--> [1] --1--> [2] --0--> [3] + / + [0] + \ + -1--> [4] --0--> [5] --1--> [6] + / \ / \ / \ + \ / \ / \ / + 1 0 1 +>> +*) + +Inductive rlw_state: Set := + | RLW_S0 : rlw_state + | RLW_S1 : rlw_state + | RLW_S2 : rlw_state + | RLW_S3 : rlw_state + | RLW_S4 : rlw_state + | RLW_S5 : rlw_state + | RLW_S6 : rlw_state + | RLW_Sbad : rlw_state. + +Definition rlw_transition (s: rlw_state) (b: bool) : rlw_state := + match s, b with + | RLW_S0, false => RLW_S1 + | RLW_S0, true => RLW_S4 + | RLW_S1, false => RLW_S1 + | RLW_S1, true => RLW_S2 + | RLW_S2, false => RLW_S3 + | RLW_S2, true => RLW_S2 + | RLW_S3, false => RLW_S3 + | RLW_S3, true => RLW_Sbad + | RLW_S4, false => RLW_S5 + | RLW_S4, true => RLW_S4 + | RLW_S5, false => RLW_S5 + | RLW_S5, true => RLW_S6 + | RLW_S6, false => RLW_Sbad + | RLW_S6, true => RLW_S6 + | RLW_Sbad, _ => RLW_Sbad + end. + +Definition rlw_accepting (s: rlw_state) : bool := + match s with + | RLW_S0 => false + | RLW_S1 => false + | RLW_S2 => true + | RLW_S3 => true + | RLW_S4 => true + | RLW_S5 => true + | RLW_S6 => true + | RLW_Sbad => false + end. + +Fixpoint is_rlw_mask_rec (n: nat) (s: rlw_state) (x: Z) {struct n} : bool := + match n with + | O => + rlw_accepting s + | S m => + let (b, y) := Z_bin_decomp x in + is_rlw_mask_rec m (rlw_transition s b) y + end. + +Definition is_rlw_mask (x: int) : bool := + is_rlw_mask_rec wordsize RLW_S0 (unsigned x). + +(** Comparisons. *) + +Definition cmp (c: comparison) (x y: int) : bool := + match c with + | Ceq => eq x y + | Cne => negb (eq x y) + | Clt => lt x y + | Cle => negb (lt y x) + | Cgt => lt y x + | Cge => negb (lt x y) + end. + +Definition cmpu (c: comparison) (x y: int) : bool := + match c with + | Ceq => eq x y + | Cne => negb (eq x y) + | Clt => ltu x y + | Cle => negb (ltu y x) + | Cgt => ltu y x + | Cge => negb (ltu x y) + end. + +Definition is_false (x: int) : Prop := x = zero. +Definition is_true (x: int) : Prop := x <> zero. +Definition notbool (x: int) : int := if eq x zero then one else zero. + +(** * Properties of integers and integer arithmetic *) + +(** ** Properties of equality *) + +Theorem one_not_zero: Int.one <> Int.zero. +Proof. + compute. congruence. +Qed. + +Theorem eq_sym: + forall x y, eq x y = eq y x. +Proof. + intros; unfold eq. case (zeq (unsigned x) (unsigned y)); intro. + rewrite e. rewrite zeq_true. auto. + rewrite zeq_false. auto. auto. +Qed. + +Theorem eq_spec: forall (x y: int), if eq x y then x = y else x <> y. +Proof. + intros; unfold eq. case (eq_dec x y); intro. + subst y. rewrite zeq_true. auto. + rewrite zeq_false. auto. + destruct x; destruct y. + simpl. red; intro. elim n. apply mkint_eq. auto. +Qed. + +Theorem eq_true: forall x, eq x x = true. +Proof. + intros. generalize (eq_spec x x); case (eq x x); intros; congruence. +Qed. + +Theorem eq_false: forall x y, x <> y -> eq x y = false. +Proof. + intros. generalize (eq_spec x y); case (eq x y); intros; congruence. +Qed. + +(** ** Modulo arithmetic *) + +(** We define and state properties of equality and arithmetic modulo a + positive integer. *) + +Section EQ_MODULO. + +Variable modul: Z. +Hypothesis modul_pos: modul > 0. + +Definition eqmod (x y: Z) : Prop := exists k, x = k * modul + y. + +Lemma eqmod_refl: forall x, eqmod x x. +Proof. + intros; red. exists 0. omega. +Qed. + +Lemma eqmod_refl2: forall x y, x = y -> eqmod x y. +Proof. + intros. subst y. apply eqmod_refl. +Qed. + +Lemma eqmod_sym: forall x y, eqmod x y -> eqmod y x. +Proof. + intros x y [k EQ]; red. exists (-k). subst x. ring. +Qed. + +Lemma eqmod_trans: forall x y z, eqmod x y -> eqmod y z -> eqmod x z. +Proof. + intros x y z [k1 EQ1] [k2 EQ2]; red. + exists (k1 + k2). subst x; subst y. ring. +Qed. + +Lemma eqmod_small_eq: + forall x y, eqmod x y -> 0 <= x < modul -> 0 <= y < modul -> x = y. +Proof. + intros x y [k EQ] I1 I2. + generalize (Zdiv_unique _ _ _ _ EQ I2). intro. + rewrite (Zdiv_small x modul I1) in H. subst k. omega. +Qed. + +Lemma eqmod_mod_eq: + forall x y, eqmod x y -> x mod modul = y mod modul. +Proof. + intros x y [k EQ]. subst x. + rewrite Zplus_comm. apply Z_mod_plus. auto. +Qed. + +Lemma eqmod_mod: + forall x, eqmod x (x mod modul). +Proof. + intros; red. exists (x / modul). + rewrite Zmult_comm. apply Z_div_mod_eq. auto. +Qed. + +Lemma eqmod_add: + forall a b c d, eqmod a b -> eqmod c d -> eqmod (a + c) (b + d). +Proof. + intros a b c d [k1 EQ1] [k2 EQ2]; red. + subst a; subst c. exists (k1 + k2). ring. +Qed. + +Lemma eqmod_neg: + forall x y, eqmod x y -> eqmod (-x) (-y). +Proof. + intros x y [k EQ]; red. exists (-k). rewrite EQ. ring. +Qed. + +Lemma eqmod_sub: + forall a b c d, eqmod a b -> eqmod c d -> eqmod (a - c) (b - d). +Proof. + intros a b c d [k1 EQ1] [k2 EQ2]; red. + subst a; subst c. exists (k1 - k2). ring. +Qed. + +Lemma eqmod_mult: + forall a b c d, eqmod a c -> eqmod b d -> eqmod (a * b) (c * d). +Proof. + intros a b c d [k1 EQ1] [k2 EQ2]; red. + subst a; subst b. + exists (k1 * k2 * modul + c * k2 + k1 * d). + ring. +Qed. + +End EQ_MODULO. + +(** We then specialize these definitions to equality modulo + $2^32$ #2<sup>32</sup>#. *) + +Lemma modulus_pos: + modulus > 0. +Proof. + unfold modulus. apply two_power_nat_pos. +Qed. +Hint Resolve modulus_pos: ints. + +Definition eqm := eqmod modulus. + +Lemma eqm_refl: forall x, eqm x x. +Proof (eqmod_refl modulus). +Hint Resolve eqm_refl: ints. + +Lemma eqm_refl2: + forall x y, x = y -> eqm x y. +Proof (eqmod_refl2 modulus). +Hint Resolve eqm_refl2: ints. + +Lemma eqm_sym: forall x y, eqm x y -> eqm y x. +Proof (eqmod_sym modulus). +Hint Resolve eqm_sym: ints. + +Lemma eqm_trans: forall x y z, eqm x y -> eqm y z -> eqm x z. +Proof (eqmod_trans modulus). +Hint Resolve eqm_trans: ints. + +Lemma eqm_samerepr: forall x y, eqm x y -> repr x = repr y. +Proof. + intros. unfold repr. apply mkint_eq. + apply eqmod_mod_eq. auto with ints. exact H. +Qed. + +Lemma eqm_small_eq: + forall x y, eqm x y -> 0 <= x < modulus -> 0 <= y < modulus -> x = y. +Proof (eqmod_small_eq modulus). +Hint Resolve eqm_small_eq: ints. + +Lemma eqm_add: + forall a b c d, eqm a b -> eqm c d -> eqm (a + c) (b + d). +Proof (eqmod_add modulus). +Hint Resolve eqm_add: ints. + +Lemma eqm_neg: + forall x y, eqm x y -> eqm (-x) (-y). +Proof (eqmod_neg modulus). +Hint Resolve eqm_neg: ints. + +Lemma eqm_sub: + forall a b c d, eqm a b -> eqm c d -> eqm (a - c) (b - d). +Proof (eqmod_sub modulus). +Hint Resolve eqm_sub: ints. + +Lemma eqm_mult: + forall a b c d, eqm a c -> eqm b d -> eqm (a * b) (c * d). +Proof (eqmod_mult modulus). +Hint Resolve eqm_mult: ints. + +(** ** Properties of the coercions between [Z] and [int] *) + +Lemma eqm_unsigned_repr: + forall z, eqm z (unsigned (repr z)). +Proof. + unfold eqm, repr, unsigned; intros; simpl. + apply eqmod_mod. auto with ints. +Qed. +Hint Resolve eqm_unsigned_repr: ints. + +Lemma eqm_unsigned_repr_l: + forall a b, eqm a b -> eqm (unsigned (repr a)) b. +Proof. + intros. apply eqm_trans with a. + apply eqm_sym. apply eqm_unsigned_repr. auto. +Qed. +Hint Resolve eqm_unsigned_repr_l: ints. + +Lemma eqm_unsigned_repr_r: + forall a b, eqm a b -> eqm a (unsigned (repr b)). +Proof. + intros. apply eqm_trans with b. auto. + apply eqm_unsigned_repr. +Qed. +Hint Resolve eqm_unsigned_repr_r: ints. + +Lemma eqm_signed_unsigned: + forall x, eqm (signed x) (unsigned x). +Proof. + intro; red; unfold signed. set (y := unsigned x). + case (zlt y half_modulus); intro. + apply eqmod_refl. red; exists (-1); ring. +Qed. + +Lemma in_range_range: + forall z, in_range z -> 0 <= z < modulus. +Proof. + intros. + assert (z >= 0 /\ z < modulus). + generalize H. unfold in_range, Zge, Zlt. + destruct (z ?= 0). + destruct (z ?= modulus); try contradiction. + intuition congruence. + contradiction. + destruct (z ?= modulus); try contradiction. + intuition congruence. + omega. +Qed. + +Theorem unsigned_range: + forall i, 0 <= unsigned i < modulus. +Proof. + destruct i; simpl. + apply in_range_range. auto. +Qed. +Hint Resolve unsigned_range: ints. + +Theorem unsigned_range_2: + forall i, 0 <= unsigned i <= max_unsigned. +Proof. + intro; unfold max_unsigned. + generalize (unsigned_range i). omega. +Qed. +Hint Resolve unsigned_range_2: ints. + +Theorem signed_range: + forall i, min_signed <= signed i <= max_signed. +Proof. + intros. unfold signed. + generalize (unsigned_range i). set (n := unsigned i). intros. + case (zlt n half_modulus); intro. + unfold max_signed. assert (min_signed < 0). compute. auto. + omega. + unfold min_signed, max_signed. change modulus with (2 * half_modulus). + change modulus with (2 * half_modulus) in H. omega. +Qed. + +Theorem repr_unsigned: + forall i, repr (unsigned i) = i. +Proof. + destruct i; simpl. unfold repr. apply mkint_eq. + apply Zmod_small. apply in_range_range; auto. +Qed. +Hint Resolve repr_unsigned: ints. + +Lemma repr_signed: + forall i, repr (signed i) = i. +Proof. + intros. transitivity (repr (unsigned i)). + apply eqm_samerepr. apply eqm_signed_unsigned. auto with ints. +Qed. +Hint Resolve repr_unsigned: ints. + +Theorem unsigned_repr: + forall z, 0 <= z <= max_unsigned -> unsigned (repr z) = z. +Proof. + intros. unfold repr, unsigned; simpl. + apply Zmod_small. unfold max_unsigned in H. omega. +Qed. +Hint Resolve unsigned_repr: ints. + +Theorem signed_repr: + forall z, min_signed <= z <= max_signed -> signed (repr z) = z. +Proof. + intros. unfold signed. case (zle 0 z); intro. + replace (unsigned (repr z)) with z. + rewrite zlt_true. auto. unfold max_signed in H. omega. + symmetry. apply unsigned_repr. + split. auto. apply Zle_trans with max_signed. tauto. + compute; intro; discriminate. + pose (z' := z + modulus). + replace (repr z) with (repr z'). + replace (unsigned (repr z')) with z'. + rewrite zlt_false. unfold z'. omega. + unfold z'. unfold min_signed in H. + change modulus with (half_modulus + half_modulus). omega. + symmetry. apply unsigned_repr. + unfold z', max_unsigned. unfold min_signed, max_signed in H. + change modulus with (half_modulus + half_modulus). + omega. + apply eqm_samerepr. unfold z'; red. exists 1. omega. +Qed. + +(** ** Properties of addition *) + +Theorem add_unsigned: forall x y, add x y = repr (unsigned x + unsigned y). +Proof. intros; reflexivity. +Qed. + +Theorem add_signed: forall x y, add x y = repr (signed x + signed y). +Proof. + intros. rewrite add_unsigned. apply eqm_samerepr. + apply eqm_add; apply eqm_sym; apply eqm_signed_unsigned. +Qed. + +Theorem add_commut: forall x y, add x y = add y x. +Proof. intros; unfold add. decEq. omega. Qed. + +Theorem add_zero: forall x, add x zero = x. +Proof. + intros; unfold add, zero. change (unsigned (repr 0)) with 0. + rewrite Zplus_0_r. apply repr_unsigned. +Qed. + +Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z). +Proof. + intros; unfold add. + set (x' := unsigned x). + set (y' := unsigned y). + set (z' := unsigned z). + apply eqm_samerepr. + apply eqm_trans with ((x' + y') + z'). + auto with ints. + rewrite <- Zplus_assoc. auto with ints. +Qed. + +Theorem add_permut: forall x y z, add x (add y z) = add y (add x z). +Proof. + intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut. +Qed. + +Theorem add_neg_zero: forall x, add x (neg x) = zero. +Proof. + intros; unfold add, neg, zero. apply eqm_samerepr. + replace 0 with (unsigned x + (- (unsigned x))). + auto with ints. omega. +Qed. + +(** ** Properties of negation *) + +Theorem neg_repr: forall z, neg (repr z) = repr (-z). +Proof. + intros; unfold neg. apply eqm_samerepr. auto with ints. +Qed. + +Theorem neg_zero: neg zero = zero. +Proof. + unfold neg, zero. compute. apply mkint_eq. auto. +Qed. + +Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y). +Proof. + intros; unfold neg, add. apply eqm_samerepr. + apply eqm_trans with (- (unsigned x + unsigned y)). + auto with ints. + replace (- (unsigned x + unsigned y)) + with ((- unsigned x) + (- unsigned y)). + auto with ints. omega. +Qed. + +(** ** Properties of subtraction *) + +Theorem sub_zero_l: forall x, sub x zero = x. +Proof. + intros; unfold sub. change (unsigned zero) with 0. + replace (unsigned x - 0) with (unsigned x). apply repr_unsigned. + omega. +Qed. + +Theorem sub_zero_r: forall x, sub zero x = neg x. +Proof. + intros; unfold sub, neg. change (unsigned zero) with 0. + replace (0 - unsigned x) with (- unsigned x). auto. + omega. +Qed. + +Theorem sub_add_opp: forall x y, sub x y = add x (neg y). +Proof. + intros; unfold sub, add, neg. + replace (unsigned x - unsigned y) + with (unsigned x + (- unsigned y)). + apply eqm_samerepr. auto with ints. omega. +Qed. + +Theorem sub_idem: forall x, sub x x = zero. +Proof. + intros; unfold sub. replace (unsigned x - unsigned x) with 0. + reflexivity. omega. +Qed. + +Theorem sub_add_l: forall x y z, sub (add x y) z = add (sub x z) y. +Proof. + intros. repeat rewrite sub_add_opp. + repeat rewrite add_assoc. decEq. apply add_commut. +Qed. + +Theorem sub_add_r: forall x y z, sub x (add y z) = add (sub x z) (neg y). +Proof. + intros. repeat rewrite sub_add_opp. + rewrite neg_add_distr. rewrite add_permut. apply add_commut. +Qed. + +Theorem sub_shifted: + forall x y z, + sub (add x z) (add y z) = sub x y. +Proof. + intros. rewrite sub_add_opp. rewrite neg_add_distr. + rewrite add_assoc. + rewrite (add_commut (neg y) (neg z)). + rewrite <- (add_assoc z). rewrite add_neg_zero. + rewrite (add_commut zero). rewrite add_zero. + symmetry. apply sub_add_opp. +Qed. + +(** ** Properties of multiplication *) + +Theorem mul_commut: forall x y, mul x y = mul y x. +Proof. + intros; unfold mul. decEq. ring. +Qed. + +Theorem mul_zero: forall x, mul x zero = zero. +Proof. + intros; unfold mul. change (unsigned zero) with 0. + unfold zero. decEq. ring. +Qed. + +Theorem mul_one: forall x, mul x one = x. +Proof. + intros; unfold mul. change (unsigned one) with 1. + transitivity (repr (unsigned x)). decEq. ring. + apply repr_unsigned. +Qed. + +Theorem mul_assoc: forall x y z, mul (mul x y) z = mul x (mul y z). +Proof. + intros; unfold mul. + set (x' := unsigned x). + set (y' := unsigned y). + set (z' := unsigned z). + apply eqm_samerepr. apply eqm_trans with ((x' * y') * z'). + auto with ints. + rewrite <- Zmult_assoc. auto with ints. +Qed. + +Theorem mul_add_distr_l: + forall x y z, mul (add x y) z = add (mul x z) (mul y z). +Proof. + intros; unfold mul, add. + apply eqm_samerepr. + set (x' := unsigned x). + set (y' := unsigned y). + set (z' := unsigned z). + apply eqm_trans with ((x' + y') * z'). + auto with ints. + replace ((x' + y') * z') with (x' * z' + y' * z'). + auto with ints. + ring. +Qed. + +Theorem mul_add_distr_r: + forall x y z, mul x (add y z) = add (mul x y) (mul x z). +Proof. + intros. rewrite mul_commut. rewrite mul_add_distr_l. + decEq; apply mul_commut. +Qed. + +Axiom neg_mul_distr_l: forall x y, neg(mul x y) = mul (neg x) y. +Axiom neg_mul_distr_r: forall x y, neg(mul x y) = mul x (neg y). + +(** ** Properties of binary decompositions *) + +Lemma Z_shift_add_bin_decomp: + forall x, + Z_shift_add (fst (Z_bin_decomp x)) (snd (Z_bin_decomp x)) = x. +Proof. + destruct x; simpl. + auto. + destruct p; reflexivity. + destruct p; try reflexivity. simpl. + assert (forall z, 2 * (z + 1) - 1 = 2 * z + 1). intro; omega. + generalize (H (Zpos p)); simpl. congruence. +Qed. + +Lemma Z_shift_add_inj: + forall b1 x1 b2 x2, + Z_shift_add b1 x1 = Z_shift_add b2 x2 -> b1 = b2 /\ x1 = x2. +Proof. + intros until x2. + unfold Z_shift_add. + destruct b1; destruct b2; intros; + ((split; [reflexivity|omega]) || omegaContradiction). +Qed. + +Lemma Z_of_bits_exten: + forall n f1 f2, + (forall z, 0 <= z < Z_of_nat n -> f1 z = f2 z) -> + Z_of_bits n f1 = Z_of_bits n f2. +Proof. + induction n; intros. + reflexivity. + simpl. rewrite inj_S in H. decEq. apply H. omega. + apply IHn. intros; apply H. omega. +Qed. + +Opaque Zmult. + +Lemma Z_of_bits_of_Z: + forall x, eqm (Z_of_bits wordsize (bits_of_Z wordsize x)) x. +Proof. + assert (forall n x, exists k, + Z_of_bits n (bits_of_Z n x) = k * two_power_nat n + x). + induction n; intros. + rewrite two_power_nat_O. simpl. exists (-x). omega. + rewrite two_power_nat_S. simpl. + caseEq (Z_bin_decomp x). intros b y ZBD. simpl. + replace (Z_of_bits n (fun i => if zeq (i + 1) 0 then b else bits_of_Z n y (i + 1 - 1))) + with (Z_of_bits n (bits_of_Z n y)). + elim (IHn y). intros k1 EQ1. rewrite EQ1. + rewrite <- (Z_shift_add_bin_decomp x). + rewrite ZBD. simpl. + exists k1. + case b; unfold Z_shift_add; ring. + apply Z_of_bits_exten. intros. + rewrite zeq_false. decEq. omega. omega. + intro. exact (H wordsize x). +Qed. + +Lemma bits_of_Z_zero: + forall n x, bits_of_Z n 0 x = false. +Proof. + induction n; simpl; intros. + auto. + case (zeq x 0); intro. auto. auto. +Qed. + +Remark Z_bin_decomp_2xm1: + forall x, Z_bin_decomp (2 * x - 1) = (true, x - 1). +Proof. + intros. caseEq (Z_bin_decomp (2 * x - 1)). intros b y EQ. + generalize (Z_shift_add_bin_decomp (2 * x - 1)). + rewrite EQ; simpl. + replace (2 * x - 1) with (Z_shift_add true (x - 1)). + intro. elim (Z_shift_add_inj _ _ _ _ H); intros. + congruence. unfold Z_shift_add. omega. +Qed. + +Lemma bits_of_Z_mone: + forall n x, + 0 <= x < Z_of_nat n -> + bits_of_Z n (two_power_nat n - 1) x = true. +Proof. + induction n; intros. + simpl in H. omegaContradiction. + unfold bits_of_Z; fold bits_of_Z. + rewrite two_power_nat_S. rewrite Z_bin_decomp_2xm1. + rewrite inj_S in H. case (zeq x 0); intro. auto. + apply IHn. omega. +Qed. + +Lemma Z_bin_decomp_shift_add: + forall b x, Z_bin_decomp (Z_shift_add b x) = (b, x). +Proof. + intros. caseEq (Z_bin_decomp (Z_shift_add b x)); intros b' x' EQ. + generalize (Z_shift_add_bin_decomp (Z_shift_add b x)). + rewrite EQ; simpl fst; simpl snd. intro. + elim (Z_shift_add_inj _ _ _ _ H); intros. + congruence. +Qed. + +Lemma bits_of_Z_of_bits: + forall n f i, + 0 <= i < Z_of_nat n -> + bits_of_Z n (Z_of_bits n f) i = f i. +Proof. + induction n; intros; simpl. + simpl in H. omegaContradiction. + rewrite Z_bin_decomp_shift_add. + case (zeq i 0); intro. + congruence. + rewrite IHn. decEq. omega. rewrite inj_S in H. omega. +Qed. + +Lemma Z_of_bits_range: + forall f, 0 <= Z_of_bits wordsize f < modulus. +Proof. + unfold max_unsigned, modulus. + generalize wordsize. induction n; simpl; intros. + rewrite two_power_nat_O. omega. + rewrite two_power_nat_S. generalize (IHn (fun i => f (i + 1))). + set (x := Z_of_bits n (fun i => f (i + 1))). + intro. destruct (f 0); unfold Z_shift_add; omega. +Qed. +Hint Resolve Z_of_bits_range: ints. + +Lemma Z_of_bits_range_2: + forall f, 0 <= Z_of_bits wordsize f <= max_unsigned. +Proof. + intros. unfold max_unsigned. + generalize (Z_of_bits_range f). omega. +Qed. +Hint Resolve Z_of_bits_range_2: ints. + +Lemma bits_of_Z_below: + forall n x i, i < 0 -> bits_of_Z n x i = false. +Proof. + induction n; simpl; intros. + reflexivity. + destruct (Z_bin_decomp x). rewrite zeq_false. apply IHn. + omega. omega. +Qed. + +Lemma bits_of_Z_above: + forall n x i, i >= Z_of_nat n -> bits_of_Z n x i = false. +Proof. + induction n; intros; simpl. + reflexivity. + destruct (Z_bin_decomp x). rewrite zeq_false. apply IHn. + rewrite inj_S in H. omega. rewrite inj_S in H. omega. +Qed. + +Opaque Zmult. + +Lemma Z_of_bits_excl: + forall n f g h, + (forall i, 0 <= i < Z_of_nat n -> f i && g i = false) -> + (forall i, 0 <= i < Z_of_nat n -> f i || g i = h i) -> + Z_of_bits n f + Z_of_bits n g = Z_of_bits n h. +Proof. + induction n. + intros; reflexivity. + intros. simpl. rewrite inj_S in H. rewrite inj_S in H0. + rewrite <- (IHn (fun i => f(i+1)) (fun i => g(i+1)) (fun i => h(i+1))). + assert (0 <= 0 < Zsucc(Z_of_nat n)). omega. + unfold Z_shift_add. + rewrite <- H0; auto. + set (F := Z_of_bits n (fun i => f(i + 1))). + set (G := Z_of_bits n (fun i => g(i + 1))). + caseEq (f 0); intros; caseEq (g 0); intros; simpl. + generalize (H 0 H1). rewrite H2; rewrite H3. simpl. intros; discriminate. + omega. omega. omega. + intros; apply H. omega. + intros; apply H0. omega. +Qed. + +(** ** Properties of bitwise and, or, xor *) + +Lemma bitwise_binop_commut: + forall f, + (forall a b, f a b = f b a) -> + forall x y, + bitwise_binop f x y = bitwise_binop f y x. +Proof. + unfold bitwise_binop; intros. + decEq. apply Z_of_bits_exten; intros. auto. +Qed. + +Lemma bitwise_binop_assoc: + forall f, + (forall a b c, f a (f b c) = f (f a b) c) -> + forall x y z, + bitwise_binop f (bitwise_binop f x y) z = + bitwise_binop f x (bitwise_binop f y z). +Proof. + unfold bitwise_binop; intros. + repeat rewrite unsigned_repr; auto with ints. + decEq. apply Z_of_bits_exten; intros. + repeat (rewrite bits_of_Z_of_bits; auto). +Qed. + +Lemma bitwise_binop_idem: + forall f, + (forall a, f a a = a) -> + forall x, + bitwise_binop f x x = x. +Proof. + unfold bitwise_binop; intros. + transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))). + decEq. apply Z_of_bits_exten; intros. auto. + transitivity (repr (unsigned x)). + apply eqm_samerepr. apply Z_of_bits_of_Z. apply repr_unsigned. +Qed. + +Theorem and_commut: forall x y, and x y = and y x. +Proof (bitwise_binop_commut andb andb_comm). + +Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z). +Proof (bitwise_binop_assoc andb andb_assoc). + +Theorem and_zero: forall x, and x zero = zero. +Proof. + unfold and, bitwise_binop, zero; intros. + transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize 0))). + decEq. apply Z_of_bits_exten. intros. + change (unsigned (repr 0)) with 0. + rewrite bits_of_Z_zero. apply andb_b_false. + auto with ints. +Qed. + +Lemma mone_max_unsigned: + mone = repr max_unsigned. +Proof. + unfold mone. apply eqm_samerepr. exists (-1). + unfold max_unsigned. omega. +Qed. + +Theorem and_mone: forall x, and x mone = x. +Proof. + unfold and, bitwise_binop; intros. + rewrite mone_max_unsigned. unfold max_unsigned, modulus. + transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))). + decEq. apply Z_of_bits_exten. intros. + rewrite unsigned_repr. rewrite bits_of_Z_mone. + apply andb_b_true. omega. compute. intuition congruence. + transitivity (repr (unsigned x)). + apply eqm_samerepr. apply Z_of_bits_of_Z. + apply repr_unsigned. +Qed. + +Theorem and_idem: forall x, and x x = x. +Proof. + assert (forall b, b && b = b). + destruct b; reflexivity. + exact (bitwise_binop_idem andb H). +Qed. + +Theorem or_commut: forall x y, or x y = or y x. +Proof (bitwise_binop_commut orb orb_comm). + +Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z). +Proof (bitwise_binop_assoc orb orb_assoc). + +Theorem or_zero: forall x, or x zero = x. +Proof. + unfold or, bitwise_binop, zero; intros. + transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))). + decEq. apply Z_of_bits_exten. intros. + change (unsigned (repr 0)) with 0. + rewrite bits_of_Z_zero. apply orb_b_false. + transitivity (repr (unsigned x)); auto with ints. + apply eqm_samerepr. apply Z_of_bits_of_Z. +Qed. + +Theorem or_mone: forall x, or x mone = mone. +Proof. + rewrite mone_max_unsigned. + unfold or, bitwise_binop; intros. + decEq. + transitivity (Z_of_bits wordsize (bits_of_Z wordsize max_unsigned)). + apply Z_of_bits_exten. intros. + change (unsigned (repr max_unsigned)) with max_unsigned. + unfold max_unsigned, modulus. rewrite bits_of_Z_mone; auto. + apply orb_b_true. + apply eqm_small_eq; auto with ints. compute; intuition congruence. +Qed. + +Theorem or_idem: forall x, or x x = x. +Proof. + assert (forall b, b || b = b). + destruct b; reflexivity. + exact (bitwise_binop_idem orb H). +Qed. + +Theorem and_or_distrib: + forall x y z, + and x (or y z) = or (and x y) (and x z). +Proof. + intros; unfold and, or, bitwise_binop. + decEq. repeat rewrite unsigned_repr; auto with ints. + apply Z_of_bits_exten; intros. + repeat rewrite bits_of_Z_of_bits; auto. + apply demorgan1. +Qed. + +Theorem xor_commut: forall x y, xor x y = xor y x. +Proof (bitwise_binop_commut xorb xorb_comm). + +Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z). +Proof. + assert (forall a b c, xorb a (xorb b c) = xorb (xorb a b) c). + symmetry. apply xorb_assoc. + exact (bitwise_binop_assoc xorb H). +Qed. + +Theorem xor_zero: forall x, xor x zero = x. +Proof. + unfold xor, bitwise_binop, zero; intros. + transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))). + decEq. apply Z_of_bits_exten. intros. + change (unsigned (repr 0)) with 0. + rewrite bits_of_Z_zero. apply xorb_false. + transitivity (repr (unsigned x)); auto with ints. + apply eqm_samerepr. apply Z_of_bits_of_Z. +Qed. + +Theorem xor_zero_one: xor zero one = one. +Proof. reflexivity. Qed. + +Theorem xor_one_one: xor one one = zero. +Proof. reflexivity. Qed. + +Theorem and_xor_distrib: + forall x y z, + and x (xor y z) = xor (and x y) (and x z). +Proof. + intros; unfold and, xor, bitwise_binop. + decEq. repeat rewrite unsigned_repr; auto with ints. + apply Z_of_bits_exten; intros. + repeat rewrite bits_of_Z_of_bits; auto. + assert (forall a b c, a && (xorb b c) = xorb (a && b) (a && c)). + destruct a; destruct b; destruct c; reflexivity. + auto. +Qed. + +(** ** Properties of shifts and rotates *) + +Lemma Z_of_bits_shift: + forall n f, + exists k, + Z_of_bits n (fun i => f (i - 1)) = + k * two_power_nat n + Z_shift_add (f (-1)) (Z_of_bits n f). +Proof. + induction n; intros. + simpl. rewrite two_power_nat_O. unfold Z_shift_add. + exists (if f (-1) then (-1) else 0). + destruct (f (-1)); omega. + rewrite two_power_nat_S. simpl. + elim (IHn (fun i => f (i + 1))). intros k' EQ. + replace (Z_of_bits n (fun i => f (i - 1 + 1))) + with (Z_of_bits n (fun i => f (i + 1 - 1))) in EQ. + rewrite EQ. + change (-1 + 1) with 0. + exists k'. + unfold Z_shift_add; destruct (f (-1)); destruct (f 0); ring. + apply Z_of_bits_exten; intros. + decEq. omega. +Qed. + +Lemma Z_of_bits_shifts: + forall m f, + 0 <= m -> + (forall i, i < 0 -> f i = false) -> + eqm (Z_of_bits wordsize (fun i => f (i - m))) + (two_p m * Z_of_bits wordsize f). +Proof. + intros. pattern m. apply natlike_ind. + apply eqm_refl2. transitivity (Z_of_bits wordsize f). + apply Z_of_bits_exten; intros. decEq. omega. + simpl two_p. omega. + intros. rewrite two_p_S; auto. + set (f' := fun i => f (i - x)). + apply eqm_trans with (Z_of_bits wordsize (fun i => f' (i - 1))). + apply eqm_refl2. apply Z_of_bits_exten; intros. + unfold f'. decEq. omega. + apply eqm_trans with (Z_shift_add (f' (-1)) (Z_of_bits wordsize f')). + exact (Z_of_bits_shift wordsize f'). + unfold f'. unfold Z_shift_add. rewrite H0. + rewrite <- Zmult_assoc. apply eqm_mult. apply eqm_refl. + apply H2. omega. assumption. +Qed. + +Lemma shl_mul_two_p: + forall x y, + shl x y = mul x (repr (two_p (unsigned y))). +Proof. + intros. unfold shl, mul. + apply eqm_samerepr. + eapply eqm_trans. + apply Z_of_bits_shifts. + generalize (unsigned_range y). omega. + intros; apply bits_of_Z_below; auto. + rewrite Zmult_comm. apply eqm_mult. + apply Z_of_bits_of_Z. apply eqm_unsigned_repr. +Qed. + +Theorem shl_zero: forall x, shl x zero = x. +Proof. + intros. rewrite shl_mul_two_p. + change (repr (two_p (unsigned zero))) with one. + apply mul_one. +Qed. + +Theorem shl_mul: + forall x y, + shl x y = mul x (shl one y). +Proof. + intros. + assert (shl one y = repr (two_p (unsigned y))). + rewrite shl_mul_two_p. rewrite mul_commut. rewrite mul_one. auto. + rewrite H. apply shl_mul_two_p. +Qed. + +Theorem shl_rolm: + forall x n, + ltu n (repr (Z_of_nat wordsize)) = true -> + shl x n = rolm x n (shl mone n). +Proof. + intros x n. unfold ltu. + rewrite unsigned_repr. case (zlt (unsigned n) (Z_of_nat wordsize)); intros LT XX. + unfold shl, rolm, rol, and, bitwise_binop. + decEq. apply Z_of_bits_exten; intros. + repeat rewrite unsigned_repr; auto with ints. + repeat rewrite bits_of_Z_of_bits; auto. + case (zlt z (unsigned n)); intro LT2. + assert (z - unsigned n < 0). omega. + rewrite (bits_of_Z_below wordsize (unsigned x) _ H0). + rewrite (bits_of_Z_below wordsize (unsigned mone) _ H0). + symmetry. apply andb_b_false. + assert (z - unsigned n < Z_of_nat wordsize). + generalize (unsigned_range n). omega. + replace (unsigned mone) with (two_power_nat wordsize - 1). + rewrite bits_of_Z_mone. rewrite andb_b_true. decEq. + rewrite Zmod_small. auto. omega. omega. + rewrite mone_max_unsigned. reflexivity. + discriminate. + compute; intuition congruence. +Qed. + +Lemma bitwise_binop_shl: + forall f x y n, + f false false = false -> + bitwise_binop f (shl x n) (shl y n) = shl (bitwise_binop f x y) n. +Proof. + intros. unfold bitwise_binop, shl. + decEq. repeat rewrite unsigned_repr; auto with ints. + apply Z_of_bits_exten; intros. + case (zlt (z - unsigned n) 0); intro. + transitivity false. repeat rewrite bits_of_Z_of_bits; auto. + repeat rewrite bits_of_Z_below; auto. + rewrite bits_of_Z_below; auto. + repeat rewrite bits_of_Z_of_bits; auto. + generalize (unsigned_range n). omega. +Qed. + +Lemma and_shl: + forall x y n, + and (shl x n) (shl y n) = shl (and x y) n. +Proof. + unfold and; intros. apply bitwise_binop_shl. reflexivity. +Qed. + +Theorem shru_rolm: + forall x n, + ltu n (repr (Z_of_nat wordsize)) = true -> + shru x n = rolm x (sub (repr (Z_of_nat wordsize)) n) (shru mone n). +Proof. + intros x n. unfold ltu. + rewrite unsigned_repr. + case (zlt (unsigned n) (Z_of_nat wordsize)); intros LT XX. + unfold shru, rolm, rol, and, bitwise_binop. + decEq. apply Z_of_bits_exten; intros. + repeat rewrite unsigned_repr; auto with ints. + repeat rewrite bits_of_Z_of_bits; auto. + unfold sub. + change (unsigned (repr (Z_of_nat wordsize))) + with (Z_of_nat wordsize). + rewrite unsigned_repr. + case (zlt (z + unsigned n) (Z_of_nat wordsize)); intro LT2. + replace (unsigned mone) with (two_power_nat wordsize - 1). + rewrite bits_of_Z_mone. rewrite andb_b_true. + decEq. + replace (z - (Z_of_nat wordsize - unsigned n)) + with ((z + unsigned n) + (-1) * Z_of_nat wordsize). + rewrite Z_mod_plus. symmetry. apply Zmod_small. + generalize (unsigned_range n). omega. omega. omega. + generalize (unsigned_range n). omega. + reflexivity. + rewrite (bits_of_Z_above wordsize (unsigned x) _ LT2). + rewrite (bits_of_Z_above wordsize (unsigned mone) _ LT2). + symmetry. apply andb_b_false. + split. omega. apply Zle_trans with (Z_of_nat wordsize). + generalize (unsigned_range n); omega. compute; intuition congruence. + discriminate. + split. omega. compute; intuition congruence. +Qed. + +Lemma bitwise_binop_shru: + forall f x y n, + f false false = false -> + bitwise_binop f (shru x n) (shru y n) = shru (bitwise_binop f x y) n. +Proof. + intros. unfold bitwise_binop, shru. + decEq. repeat rewrite unsigned_repr; auto with ints. + apply Z_of_bits_exten; intros. + case (zlt (z + unsigned n) (Z_of_nat wordsize)); intro. + repeat rewrite bits_of_Z_of_bits; auto. + generalize (unsigned_range n); omega. + transitivity false. repeat rewrite bits_of_Z_of_bits; auto. + repeat rewrite bits_of_Z_above; auto. + rewrite bits_of_Z_above; auto. +Qed. + +Lemma and_shru: + forall x y n, + and (shru x n) (shru y n) = shru (and x y) n. +Proof. + unfold and; intros. apply bitwise_binop_shru. reflexivity. +Qed. + +Theorem rol_zero: + forall x, + rol x zero = x. +Proof. + intros. unfold rol. transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))). + decEq. + transitivity (repr (unsigned x)). + decEq. apply eqm_small_eq. apply Z_of_bits_of_Z. + auto with ints. auto with ints. auto with ints. +Qed. + +Lemma bitwise_binop_rol: + forall f x y n, + bitwise_binop f (rol x n) (rol y n) = rol (bitwise_binop f x y) n. +Proof. + intros. unfold bitwise_binop, rol. + decEq. repeat (rewrite unsigned_repr; auto with ints). + apply Z_of_bits_exten; intros. + repeat rewrite bits_of_Z_of_bits; auto. + apply Z_mod_lt. compute. auto. +Qed. + +Theorem rol_and: + forall x y n, + rol (and x y) n = and (rol x n) (rol y n). +Proof. + intros. symmetry. unfold and. apply bitwise_binop_rol. +Qed. + +Theorem rol_rol: + forall x n m, + rol (rol x n) m = rol x (modu (add n m) (repr (Z_of_nat wordsize))). +Proof. + intros. unfold rol. decEq. + repeat (rewrite unsigned_repr; auto with ints). + apply Z_of_bits_exten; intros. + repeat rewrite bits_of_Z_of_bits; auto. + decEq. unfold modu, add. + set (W := Z_of_nat wordsize). + set (M := unsigned m); set (N := unsigned n). + assert (W > 0). compute; auto. + assert (forall a, eqmod W a (unsigned (repr a))). + intro. elim (eqm_unsigned_repr a). intros k EQ. + red. exists (k * (modulus / W)). + replace (k * (modulus / W) * W) with (k * modulus). auto. + rewrite <- Zmult_assoc. reflexivity. + apply eqmod_mod_eq. auto. + change (unsigned (repr W)) with W. + apply eqmod_trans with (z - (N + M) mod W). + apply eqmod_trans with ((z - M) - N). + apply eqmod_sub. apply eqmod_sym. apply eqmod_mod. auto. + apply eqmod_refl. + replace (z - M - N) with (z - (N + M)). + apply eqmod_sub. apply eqmod_refl. apply eqmod_mod. auto. + omega. + apply eqmod_sub. apply eqmod_refl. + eapply eqmod_trans; [idtac|apply H1]. + eapply eqmod_trans; [idtac|apply eqmod_mod]. + apply eqmod_sym. eapply eqmod_trans; [idtac|apply eqmod_mod]. + apply eqmod_sym. apply H1. auto. auto. + apply Z_mod_lt. compute; auto. +Qed. + +Theorem rolm_zero: + forall x m, + rolm x zero m = and x m. +Proof. + intros. unfold rolm. rewrite rol_zero. auto. +Qed. + +Theorem rolm_rolm: + forall x n1 m1 n2 m2, + rolm (rolm x n1 m1) n2 m2 = + rolm x (modu (add n1 n2) (repr (Z_of_nat wordsize))) + (and (rol m1 n2) m2). +Proof. + intros. + unfold rolm. rewrite rol_and. rewrite and_assoc. + rewrite rol_rol. reflexivity. +Qed. + +Theorem rol_or: + forall x y n, + rol (or x y) n = or (rol x n) (rol y n). +Proof. + intros. symmetry. unfold or. apply bitwise_binop_rol. +Qed. + +Theorem or_rolm: + forall x n m1 m2, + or (rolm x n m1) (rolm x n m2) = rolm x n (or m1 m2). +Proof. + intros; unfold rolm. symmetry. apply and_or_distrib. +Qed. + +(** ** Relation between shifts and powers of 2 *) + +Fixpoint powerserie (l: list Z): Z := + match l with + | nil => 0 + | x :: xs => two_p x + powerserie xs + end. + +Lemma Z_bin_decomp_range: + forall x n, + 0 <= x < 2 * n -> 0 <= snd (Z_bin_decomp x) < n. +Proof. + intros. rewrite <- (Z_shift_add_bin_decomp x) in H. + unfold Z_shift_add in H. destruct (fst (Z_bin_decomp x)); omega. +Qed. + +Lemma Z_one_bits_powerserie: + forall x, 0 <= x < modulus -> x = powerserie (Z_one_bits wordsize x 0). +Proof. + assert (forall n x i, + 0 <= i -> + 0 <= x < two_power_nat n -> + x * two_p i = powerserie (Z_one_bits n x i)). + induction n; intros. + simpl. rewrite two_power_nat_O in H0. + assert (x = 0). omega. subst x. omega. + rewrite two_power_nat_S in H0. simpl Z_one_bits. + generalize (Z_shift_add_bin_decomp x). + generalize (Z_bin_decomp_range x _ H0). + case (Z_bin_decomp x). simpl. intros b y RANGE SHADD. + subst x. unfold Z_shift_add. + destruct b. simpl powerserie. rewrite <- IHn. + rewrite two_p_is_exp. change (two_p 1) with 2. ring. + auto. omega. omega. auto. + rewrite <- IHn. + rewrite two_p_is_exp. change (two_p 1) with 2. ring. + auto. omega. omega. auto. + intros. rewrite <- H. change (two_p 0) with 1. omega. + omega. exact H0. +Qed. + +Lemma Z_one_bits_range: + forall x i, In i (Z_one_bits wordsize x 0) -> 0 <= i < Z_of_nat wordsize. +Proof. + assert (forall n x i j, + In j (Z_one_bits n x i) -> i <= j < i + Z_of_nat n). + induction n; simpl In. + intros; elim H. + intros x i j. destruct (Z_bin_decomp x). case b. + rewrite inj_S. simpl. intros [A|B]. subst j. omega. + generalize (IHn _ _ _ B). omega. + intros B. rewrite inj_S. generalize (IHn _ _ _ B). omega. + intros. generalize (H wordsize x 0 i H0). omega. +Qed. + +Lemma is_power2_rng: + forall n logn, + is_power2 n = Some logn -> + 0 <= unsigned logn < Z_of_nat wordsize. +Proof. + intros n logn. unfold is_power2. + generalize (Z_one_bits_range (unsigned n)). + destruct (Z_one_bits wordsize (unsigned n) 0). + intros; discriminate. + destruct l. + intros. injection H0; intro; subst logn; clear H0. + assert (0 <= z < Z_of_nat wordsize). + apply H. auto with coqlib. + rewrite unsigned_repr. auto. + assert (Z_of_nat wordsize < max_unsigned). compute. auto. + omega. + intros; discriminate. +Qed. + +Theorem is_power2_range: + forall n logn, + is_power2 n = Some logn -> ltu logn (repr (Z_of_nat wordsize)) = true. +Proof. + intros. unfold ltu. + change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize). + generalize (is_power2_rng _ _ H). + case (zlt (unsigned logn) (Z_of_nat wordsize)); intros. + auto. omegaContradiction. +Qed. + +Lemma is_power2_correct: + forall n logn, + is_power2 n = Some logn -> + unsigned n = two_p (unsigned logn). +Proof. + intros n logn. unfold is_power2. + generalize (Z_one_bits_powerserie (unsigned n) (unsigned_range n)). + generalize (Z_one_bits_range (unsigned n)). + destruct (Z_one_bits wordsize (unsigned n) 0). + intros; discriminate. + destruct l. + intros. simpl in H0. injection H1; intros; subst logn; clear H1. + rewrite unsigned_repr. replace (two_p z) with (two_p z + 0). + auto. omega. elim (H z); intros. + assert (Z_of_nat wordsize < max_unsigned). compute; auto. + omega. auto with coqlib. + intros; discriminate. +Qed. + +Theorem mul_pow2: + forall x n logn, + is_power2 n = Some logn -> + mul x n = shl x logn. +Proof. + intros. generalize (is_power2_correct n logn H); intro. + rewrite shl_mul_two_p. rewrite <- H0. rewrite repr_unsigned. + auto. +Qed. + +Lemma Z_of_bits_shift_rev: + forall n f, + (forall i, i >= Z_of_nat n -> f i = false) -> + Z_of_bits n f = Z_shift_add (f 0) (Z_of_bits n (fun i => f(i + 1))). +Proof. + induction n; intros. + simpl. rewrite H. reflexivity. unfold Z_of_nat. omega. + simpl. rewrite (IHn (fun i => f (i + 1))). + reflexivity. + intros. apply H. rewrite inj_S. omega. +Qed. + +Lemma Z_of_bits_shifts_rev: + forall m f, + 0 <= m -> + (forall i, i >= Z_of_nat wordsize -> f i = false) -> + exists k, + Z_of_bits wordsize f = k + two_p m * Z_of_bits wordsize (fun i => f(i + m)) + /\ 0 <= k < two_p m. +Proof. + intros. pattern m. apply natlike_ind. + exists 0. change (two_p 0) with 1. split. + transitivity (Z_of_bits wordsize (fun i => f (i + 0))). + apply Z_of_bits_exten. intros. decEq. omega. + omega. omega. + intros x POSx [k [EQ1 RANGE1]]. + set (f' := fun i => f (i + x)) in *. + assert (forall i, i >= Z_of_nat wordsize -> f' i = false). + intros. unfold f'. apply H0. omega. + generalize (Z_of_bits_shift_rev wordsize f' H1). intro. + rewrite EQ1. rewrite H2. + set (z := Z_of_bits wordsize (fun i => f (i + Zsucc x))). + replace (Z_of_bits wordsize (fun i => f' (i + 1))) with z. + rewrite two_p_S. + case (f' 0); unfold Z_shift_add. + exists (k + two_p x). split. ring. omega. + exists k. split. ring. omega. + auto. + unfold z. apply Z_of_bits_exten; intros. unfold f'. + decEq. omega. + auto. +Qed. + +Lemma shru_div_two_p: + forall x y, + shru x y = repr (unsigned x / two_p (unsigned y)). +Proof. + intros. unfold shru. + set (x' := unsigned x). set (y' := unsigned y). + elim (Z_of_bits_shifts_rev y' (bits_of_Z wordsize x')). + intros k [EQ RANGE]. + replace (Z_of_bits wordsize (bits_of_Z wordsize x')) with x' in EQ. + rewrite Zplus_comm in EQ. rewrite Zmult_comm in EQ. + generalize (Zdiv_unique _ _ _ _ EQ RANGE). intros. + rewrite H. auto. + apply eqm_small_eq. apply eqm_sym. apply Z_of_bits_of_Z. + unfold x'. apply unsigned_range. + auto with ints. + generalize (unsigned_range y). unfold y'. omega. + intros. apply bits_of_Z_above. auto. +Qed. + +Theorem shru_zero: + forall x, shru x zero = x. +Proof. + intros. rewrite shru_div_two_p. change (two_p (unsigned zero)) with 1. + transitivity (repr (unsigned x)). decEq. apply Zdiv_unique with 0. + omega. omega. auto with ints. +Qed. + +Theorem shr_zero: + forall x, shr x zero = x. +Proof. + intros. unfold shr. change (two_p (unsigned zero)) with 1. + replace (signed x / 1) with (signed x). + apply repr_signed. + symmetry. apply Zdiv_unique with 0. omega. omega. +Qed. + +Theorem divu_pow2: + forall x n logn, + is_power2 n = Some logn -> + divu x n = shru x logn. +Proof. + intros. generalize (is_power2_correct n logn H). intro. + symmetry. unfold divu. rewrite H0. apply shru_div_two_p. +Qed. + +Lemma modu_divu_Euclid: + forall x y, y <> zero -> x = add (mul (divu x y) y) (modu x y). +Proof. + intros. unfold add, mul, divu, modu. + transitivity (repr (unsigned x)). auto with ints. + apply eqm_samerepr. + set (x' := unsigned x). set (y' := unsigned y). + apply eqm_trans with ((x' / y') * y' + x' mod y'). + apply eqm_refl2. rewrite Zmult_comm. apply Z_div_mod_eq. + generalize (unsigned_range y); intro. + assert (unsigned y <> 0). red; intro. + elim H. rewrite <- (repr_unsigned y). unfold zero. congruence. + unfold y'. omega. + auto with ints. +Qed. + +Theorem modu_divu: + forall x y, y <> zero -> modu x y = sub x (mul (divu x y) y). +Proof. + intros. + assert (forall a b c, a = add b c -> c = sub a b). + intros. subst a. rewrite sub_add_l. rewrite sub_idem. + rewrite add_commut. rewrite add_zero. auto. + apply H0. apply modu_divu_Euclid. auto. +Qed. + +Theorem mods_divs: + forall x y, mods x y = sub x (mul (divs x y) y). +Proof. + intros; unfold mods, sub, mul, divs. + apply eqm_samerepr. + unfold Zmod_round. + apply eqm_sub. apply eqm_signed_unsigned. + apply eqm_unsigned_repr_r. + apply eqm_mult. auto with ints. apply eqm_signed_unsigned. +Qed. + +Theorem divs_pow2: + forall x n logn, + is_power2 n = Some logn -> + divs x n = shrx x logn. +Proof. + intros. generalize (is_power2_correct _ _ H); intro. + unfold shrx. rewrite shl_mul_two_p. + rewrite mul_commut. rewrite mul_one. + rewrite <- H0. rewrite repr_unsigned. auto. +Qed. + +Theorem shrx_carry: + forall x y, + add (shr x y) (shr_carry x y) = shrx x y. +Proof. + intros. unfold shr_carry. + rewrite sub_add_opp. rewrite add_permut. + rewrite add_neg_zero. apply add_zero. +Qed. + +Lemma add_and: + forall x y z, + and y z = zero -> + or y z = mone -> + add (and x y) (and x z) = x. +Proof. + intros. unfold add. transitivity (repr (unsigned x)); auto with ints. + decEq. unfold and, bitwise_binop. + repeat rewrite unsigned_repr; auto with ints. + transitivity (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x))). + apply Z_of_bits_excl. intros. + assert (forall a b c, a && b && (a && c) = a && (b && c)). + destruct a; destruct b; destruct c; reflexivity. + rewrite H2. + replace (bits_of_Z wordsize (unsigned y) i && + bits_of_Z wordsize (unsigned z) i) + with (bits_of_Z wordsize (unsigned (and y z)) i). + rewrite H. change (unsigned zero) with 0. + rewrite bits_of_Z_zero. apply andb_b_false. + unfold and, bitwise_binop. + rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits. + reflexivity. auto. + intros. rewrite <- demorgan1. + replace (bits_of_Z wordsize (unsigned y) i || + bits_of_Z wordsize (unsigned z) i) + with (bits_of_Z wordsize (unsigned (or y z)) i). + rewrite H0. change (unsigned mone) with (two_power_nat wordsize - 1). + rewrite bits_of_Z_mone; auto. apply andb_b_true. + unfold or, bitwise_binop. + rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits; auto. + apply eqm_small_eq; auto with ints. apply Z_of_bits_of_Z. +Qed. + +(** To prove equalities involving modulus and bitwise ``and'', we need to + show complicated integer equalities involving one integer variable + that ranges between 0 and 31. Rather than proving these equalities, + we ask Coq to check them by computing the 32 values of the + left and right-hand sides and checking that they are equal. + This is an instance of proving by reflection. *) + +Section REFLECTION. + +Variables (f g: int -> int). + +Fixpoint check_equal_on_range (n: nat) : bool := + match n with + | O => true + | S n => if eq (f (repr (Z_of_nat n))) (g (repr (Z_of_nat n))) + then check_equal_on_range n + else false + end. + +Lemma check_equal_on_range_correct: + forall n, + check_equal_on_range n = true -> + forall z, 0 <= z < Z_of_nat n -> f (repr z) = g (repr z). +Proof. + induction n. + simpl; intros; omegaContradiction. + simpl check_equal_on_range. + set (fn := f (repr (Z_of_nat n))). + set (gn := g (repr (Z_of_nat n))). + generalize (eq_spec fn gn). + case (eq fn gn); intros. + rewrite inj_S in H1. + assert (0 <= z < Z_of_nat n \/ z = Z_of_nat n). omega. + elim H2; intro. + apply IHn. auto. auto. + subst z; auto. + discriminate. +Qed. + +Lemma equal_on_range: + check_equal_on_range wordsize = true -> + forall n, 0 <= unsigned n < Z_of_nat wordsize -> + f n = g n. +Proof. + intros. replace n with (repr (unsigned n)). + apply check_equal_on_range_correct with wordsize; auto. + apply repr_unsigned. +Qed. + +End REFLECTION. + +(** Here are the three equalities that we prove by reflection. *) + +Remark modu_and_masks_1: + forall logn, 0 <= unsigned logn < Z_of_nat wordsize -> + rol (shru mone logn) logn = shl mone logn. +Proof (equal_on_range + (fun l => rol (shru mone l) l) + (fun l => shl mone l) + (refl_equal true)). +Remark modu_and_masks_2: + forall logn, 0 <= unsigned logn < Z_of_nat wordsize -> + and (shl mone logn) (sub (repr (two_p (unsigned logn))) one) = zero. +Proof (equal_on_range + (fun l => and (shl mone l) + (sub (repr (two_p (unsigned l))) one)) + (fun l => zero) + (refl_equal true)). +Remark modu_and_masks_3: + forall logn, 0 <= unsigned logn < Z_of_nat wordsize -> + or (shl mone logn) (sub (repr (two_p (unsigned logn))) one) = mone. +Proof (equal_on_range + (fun l => or (shl mone l) + (sub (repr (two_p (unsigned l))) one)) + (fun l => mone) + (refl_equal true)). + +Theorem modu_and: + forall x n logn, + is_power2 n = Some logn -> + modu x n = and x (sub n one). +Proof. + intros. generalize (is_power2_correct _ _ H); intro. + generalize (is_power2_rng _ _ H); intro. + assert (n <> zero). + red; intro. subst n. change (unsigned zero) with 0 in H0. + assert (two_p (unsigned logn) > 0). apply two_p_gt_ZERO. omega. + omegaContradiction. + generalize (modu_divu_Euclid x n H2); intro. + assert (forall a b c, add a b = add a c -> b = c). + intros. assert (sub (add a b) a = sub (add a c) a). congruence. + repeat rewrite sub_add_l in H5. repeat rewrite sub_idem in H5. + rewrite add_commut in H5; rewrite add_zero in H5. + rewrite add_commut in H5; rewrite add_zero in H5. + auto. + apply H4 with (mul (divu x n) n). + rewrite <- H3. + rewrite (divu_pow2 x n logn H). + rewrite (mul_pow2 (shru x logn) n logn H). + rewrite shru_rolm. rewrite shl_rolm. rewrite rolm_rolm. + rewrite sub_add_opp. rewrite add_assoc. + replace (add (neg logn) logn) with zero. + rewrite add_zero. + change (modu (repr (Z_of_nat wordsize)) (repr (Z_of_nat wordsize))) + with zero. + rewrite rolm_zero. + symmetry. + replace n with (repr (two_p (unsigned logn))). + rewrite modu_and_masks_1; auto. + rewrite and_idem. + apply add_and. apply modu_and_masks_2; auto. apply modu_and_masks_3; auto. + transitivity (repr (unsigned n)). decEq. auto. auto with ints. + rewrite add_commut. rewrite add_neg_zero. auto. + unfold ltu. apply zlt_true. + change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize). + omega. + unfold ltu. apply zlt_true. + change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize). + omega. +Qed. + +(** ** Properties of integer zero extension and sign extension. *) + +Theorem cast8unsigned_and: + forall x, cast8unsigned x = and x (repr 255). +Proof. + intros; unfold cast8unsigned. + change (repr (unsigned x mod 256)) with (modu x (repr 256)). + change (repr 255) with (sub (repr 256) one). + apply modu_and with (repr 8). reflexivity. +Qed. + +Theorem cast16unsigned_and: + forall x, cast16unsigned x = and x (repr 65535). +Proof. + intros; unfold cast16unsigned. + change (repr (unsigned x mod 65536)) with (modu x (repr 65536)). + change (repr 65535) with (sub (repr 65536) one). + apply modu_and with (repr 16). reflexivity. +Qed. + +Lemma eqmod_256_unsigned_repr: + forall a, eqmod 256 a (unsigned (repr a)). +Proof. + intros. generalize (eqm_unsigned_repr a). unfold eqm, eqmod. + intros [k EQ]. exists (k * (modulus / 256)). + replace (k * (modulus / 256) * 256) + with (k * ((modulus / 256) * 256)). + exact EQ. ring. +Qed. + +Lemma eqmod_65536_unsigned_repr: + forall a, eqmod 65536 a (unsigned (repr a)). +Proof. + intros. generalize (eqm_unsigned_repr a). unfold eqm, eqmod. + intros [k EQ]. exists (k * (modulus / 65536)). + replace (k * (modulus / 65536) * 65536) + with (k * ((modulus / 65536) * 65536)). + exact EQ. ring. +Qed. + +Theorem cast8_signed_unsigned: + forall n, cast8signed (cast8unsigned n) = cast8signed n. +Proof. + intros; unfold cast8signed, cast8unsigned. + set (N := unsigned n). + rewrite unsigned_repr. + replace ((N mod 256) mod 256) with (N mod 256). + auto. + symmetry. apply Zmod_small. apply Z_mod_lt. omega. + assert (0 <= N mod 256 < 256). apply Z_mod_lt. omega. + assert (256 < max_unsigned). compute; auto. + omega. +Qed. + +Theorem cast8_unsigned_signed: + forall n, cast8unsigned (cast8signed n) = cast8unsigned n. +Proof. + intros; unfold cast8signed, cast8unsigned. + set (N := unsigned n mod 256). + assert (0 <= N < 256). unfold N; apply Z_mod_lt. omega. + assert (N mod 256 = N). apply Zmod_small. auto. + assert (256 <= max_unsigned). compute; congruence. + decEq. + case (zlt N 128); intro. + rewrite unsigned_repr. auto. omega. + transitivity (N mod 256); auto. + apply eqmod_mod_eq. omega. + apply eqmod_trans with (N - 256). apply eqmod_sym. apply eqmod_256_unsigned_repr. + assert (eqmod 256 (N - 256) (N - 0)). + apply eqmod_sub. apply eqmod_refl. + red. exists 1; reflexivity. + replace (N - 0) with N in H2. auto. omega. +Qed. + +Theorem cast16_unsigned_signed: + forall n, cast16unsigned (cast16signed n) = cast16unsigned n. +Proof. + intros; unfold cast16signed, cast16unsigned. + set (N := unsigned n mod 65536). + assert (0 <= N < 65536). unfold N; apply Z_mod_lt. omega. + assert (N mod 65536 = N). apply Zmod_small. auto. + assert (65536 <= max_unsigned). compute; congruence. + decEq. + case (zlt N 32768); intro. + rewrite unsigned_repr. auto. omega. + transitivity (N mod 65536); auto. + apply eqmod_mod_eq. omega. + apply eqmod_trans with (N - 65536). apply eqmod_sym. apply eqmod_65536_unsigned_repr. + assert (eqmod 65536 (N - 65536) (N - 0)). + apply eqmod_sub. apply eqmod_refl. + red. exists 1; reflexivity. + replace (N - 0) with N in H2. auto. omega. +Qed. + +Theorem cast8_unsigned_idem: + forall n, cast8unsigned (cast8unsigned n) = cast8unsigned n. +Proof. + intros. repeat rewrite cast8unsigned_and. + rewrite and_assoc. reflexivity. +Qed. + +Theorem cast16_unsigned_idem: + forall n, cast16unsigned (cast16unsigned n) = cast16unsigned n. +Proof. + intros. repeat rewrite cast16unsigned_and. + rewrite and_assoc. reflexivity. +Qed. + +Theorem cast8_signed_idem: + forall n, cast8signed (cast8signed n) = cast8signed n. +Proof. + intros; unfold cast8signed. + set (N := unsigned n mod 256). + assert (256 < max_unsigned). compute; auto. + assert (0 <= N < 256). unfold N. apply Z_mod_lt. omega. + case (zlt N 128); intro. + assert (unsigned (repr N) = N). + apply unsigned_repr. omega. + rewrite H1. + replace (N mod 256) with N. apply zlt_true. auto. + symmetry. apply Zmod_small. auto. + set (M := (unsigned (repr (N - 256)) mod 256)). + assert (M = N). + unfold M, N. apply eqmod_mod_eq. omega. + apply eqmod_trans with (unsigned n mod 256 - 256). + apply eqmod_sym. apply eqmod_256_unsigned_repr. + apply eqmod_trans with (unsigned n - 0). + apply eqmod_sub. + apply eqmod_sym. apply eqmod_mod. omega. + unfold eqmod. exists 1; omega. + apply eqmod_refl2. omega. + rewrite H1. rewrite zlt_false; auto. +Qed. + +Theorem cast16_signed_idem: + forall n, cast16signed (cast16signed n) = cast16signed n. +Proof. + intros; unfold cast16signed. + set (N := unsigned n mod 65536). + assert (65536 < max_unsigned). compute; auto. + assert (0 <= N < 65536). unfold N. apply Z_mod_lt. omega. + case (zlt N 32768); intro. + assert (unsigned (repr N) = N). + apply unsigned_repr. omega. + rewrite H1. + replace (N mod 65536) with N. apply zlt_true. auto. + symmetry. apply Zmod_small. auto. + set (M := (unsigned (repr (N - 65536)) mod 65536)). + assert (M = N). + unfold M, N. apply eqmod_mod_eq. omega. + apply eqmod_trans with (unsigned n mod 65536 - 65536). + apply eqmod_sym. apply eqmod_65536_unsigned_repr. + apply eqmod_trans with (unsigned n - 0). + apply eqmod_sub. + apply eqmod_sym. apply eqmod_mod. omega. + unfold eqmod. exists 1; omega. + apply eqmod_refl2. omega. + rewrite H1. rewrite zlt_false; auto. +Qed. + +Theorem cast8_signed_equal_if_unsigned_equal: + forall x y, + cast8unsigned x = cast8unsigned y -> + cast8signed x = cast8signed y. +Proof. + unfold cast8unsigned, cast8signed; intros until y. + set (x' := unsigned x mod 256). + set (y' := unsigned y mod 256). + intro. + assert (eqm x' y'). + apply eqm_trans with (unsigned (repr x')). apply eqm_unsigned_repr. + rewrite H. apply eqm_sym. apply eqm_unsigned_repr. + assert (forall z, 0 <= z mod 256 < modulus). + intros. + assert (0 <= z mod 256 < 256). apply Z_mod_lt. omega. + assert (256 <= modulus). compute. congruence. + omega. + assert (x' = y'). + apply eqm_small_eq; unfold x', y'; auto. + rewrite H2. auto. +Qed. + +Theorem cast16_signed_equal_if_unsigned_equal: + forall x y, + cast16unsigned x = cast16unsigned y -> + cast16signed x = cast16signed y. +Proof. + unfold cast16unsigned, cast16signed; intros until y. + set (x' := unsigned x mod 65536). + set (y' := unsigned y mod 65536). + intro. + assert (eqm x' y'). + apply eqm_trans with (unsigned (repr x')). apply eqm_unsigned_repr. + rewrite H. apply eqm_sym. apply eqm_unsigned_repr. + assert (forall z, 0 <= z mod 65536 < modulus). + intros. + assert (0 <= z mod 65536 < 65536). apply Z_mod_lt. omega. + assert (65536 <= modulus). compute. congruence. + omega. + assert (x' = y'). + apply eqm_small_eq; unfold x', y'; auto. + rewrite H2. auto. +Qed. + +(** ** Properties of [one_bits] (decomposition in sum of powers of two) *) + +Opaque Z_one_bits. (* Otherwise, next Qed blows up! *) + +Theorem one_bits_range: + forall x i, In i (one_bits x) -> ltu i (repr (Z_of_nat wordsize)) = true. +Proof. + intros. unfold one_bits in H. + elim (list_in_map_inv _ _ _ H). intros i0 [EQ IN]. + subst i. unfold ltu. apply zlt_true. + generalize (Z_one_bits_range _ _ IN). intros. + assert (0 <= Z_of_nat wordsize <= max_unsigned). + compute. intuition congruence. + repeat rewrite unsigned_repr; omega. +Qed. + +Fixpoint int_of_one_bits (l: list int) : int := + match l with + | nil => zero + | a :: b => add (shl one a) (int_of_one_bits b) + end. + +Theorem one_bits_decomp: + forall x, x = int_of_one_bits (one_bits x). +Proof. + intros. + transitivity (repr (powerserie (Z_one_bits wordsize (unsigned x) 0))). + transitivity (repr (unsigned x)). + auto with ints. decEq. apply Z_one_bits_powerserie. + auto with ints. + unfold one_bits. + generalize (Z_one_bits_range (unsigned x)). + generalize (Z_one_bits wordsize (unsigned x) 0). + induction l. + intros; reflexivity. + intros; simpl. rewrite <- IHl. unfold add. apply eqm_samerepr. + apply eqm_add. rewrite shl_mul_two_p. rewrite mul_commut. + rewrite mul_one. apply eqm_unsigned_repr_r. + rewrite unsigned_repr. auto with ints. + generalize (H a (in_eq _ _)). + assert (Z_of_nat wordsize < max_unsigned). compute; auto. omega. + auto with ints. + intros; apply H; auto with coqlib. +Qed. + +(** ** Properties of comparisons *) + +Theorem negate_cmp: + forall c x y, cmp (negate_comparison c) x y = negb (cmp c x y). +Proof. + intros. destruct c; simpl; try rewrite negb_elim; auto. +Qed. + +Theorem negate_cmpu: + forall c x y, cmpu (negate_comparison c) x y = negb (cmpu c x y). +Proof. + intros. destruct c; simpl; try rewrite negb_elim; auto. +Qed. + +Theorem swap_cmp: + forall c x y, cmp (swap_comparison c) x y = cmp c y x. +Proof. + intros. destruct c; simpl; auto. apply eq_sym. decEq. apply eq_sym. +Qed. + +Theorem swap_cmpu: + forall c x y, cmpu (swap_comparison c) x y = cmpu c y x. +Proof. + intros. destruct c; simpl; auto. apply eq_sym. decEq. apply eq_sym. +Qed. + +Lemma translate_eq: + forall x y d, + eq (add x d) (add y d) = eq x y. +Proof. + intros. unfold eq. case (zeq (unsigned x) (unsigned y)); intro. + unfold add. rewrite e. apply zeq_true. + apply zeq_false. unfold add. red; intro. apply n. + apply eqm_small_eq; auto with ints. + replace (unsigned x) with ((unsigned x + unsigned d) - unsigned d). + replace (unsigned y) with ((unsigned y + unsigned d) - unsigned d). + apply eqm_sub. apply eqm_trans with (unsigned (repr (unsigned x + unsigned d))). + eauto with ints. apply eqm_trans with (unsigned (repr (unsigned y + unsigned d))). + eauto with ints. eauto with ints. eauto with ints. + omega. omega. +Qed. + +Lemma translate_lt: + forall x y d, + min_signed <= signed x + signed d <= max_signed -> + min_signed <= signed y + signed d <= max_signed -> + lt (add x d) (add y d) = lt x y. +Proof. + intros. repeat rewrite add_signed. unfold lt. + repeat rewrite signed_repr; auto. case (zlt (signed x) (signed y)); intro. + apply zlt_true. omega. + apply zlt_false. omega. +Qed. + +Theorem translate_cmp: + forall c x y d, + min_signed <= signed x + signed d <= max_signed -> + min_signed <= signed y + signed d <= max_signed -> + cmp c (add x d) (add y d) = cmp c x y. +Proof. + intros. unfold cmp. + rewrite translate_eq. repeat rewrite translate_lt; auto. +Qed. + +Theorem notbool_isfalse_istrue: + forall x, is_false x -> is_true (notbool x). +Proof. + unfold is_false, is_true, notbool; intros; subst x. + simpl. discriminate. +Qed. + +Theorem notbool_istrue_isfalse: + forall x, is_true x -> is_false (notbool x). +Proof. + unfold is_false, is_true, notbool; intros. + generalize (eq_spec x zero). case (eq x zero); intro. + contradiction. auto. +Qed. + +End Int. diff --git a/lib/Lattice.v b/lib/Lattice.v new file mode 100644 index 00000000..7adcffba --- /dev/null +++ b/lib/Lattice.v @@ -0,0 +1,331 @@ +(** Constructions of semi-lattices. *) + +Require Import Coqlib. +Require Import Maps. + +(** * Signatures of semi-lattices *) + +(** A semi-lattice is a type [t] equipped with a decidable equality [eq], + a partial order [ge], a smallest element [bot], and an upper + bound operation [lub]. Note that we do not demand that [lub] computes + the least upper bound. *) + +Module Type SEMILATTICE. + + Variable t: Set. + Variable eq: forall (x y: t), {x=y} + {x<>y}. + Variable ge: t -> t -> Prop. + Hypothesis ge_refl: forall x, ge x x. + Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Variable bot: t. + Hypothesis ge_bot: forall x, ge x bot. + Variable lub: t -> t -> t. + Hypothesis lub_commut: forall x y, lub x y = lub y x. + Hypothesis ge_lub_left: forall x y, ge (lub x y) x. + +End SEMILATTICE. + +(** A semi-lattice ``with top'' is similar, but also has a greatest + element [top]. *) + +Module Type SEMILATTICE_WITH_TOP. + + Variable t: Set. + Variable eq: forall (x y: t), {x=y} + {x<>y}. + Variable ge: t -> t -> Prop. + Hypothesis ge_refl: forall x, ge x x. + Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Variable bot: t. + Hypothesis ge_bot: forall x, ge x bot. + Variable top: t. + Hypothesis ge_top: forall x, ge top x. + Variable lub: t -> t -> t. + Hypothesis lub_commut: forall x y, lub x y = lub y x. + Hypothesis ge_lub_left: forall x y, ge (lub x y) x. + +End SEMILATTICE_WITH_TOP. + +(** * Semi-lattice over maps *) + +(** Given a semi-lattice with top [L], the following functor implements + a semi-lattice structure over finite maps from positive numbers to [L.t]. + The default value for these maps is either [L.top] or [L.bot]. *) + +Module LPMap(L: SEMILATTICE_WITH_TOP) <: SEMILATTICE_WITH_TOP. + +Inductive t_ : Set := + | Bot_except: PTree.t L.t -> t_ + | Top_except: PTree.t L.t -> t_. + +Definition t: Set := t_. + +Lemma eq: forall (x y: t), {x=y} + {x<>y}. +Proof. + assert (forall m1 m2: PTree.t L.t, {m1=m2} + {m1<>m2}). + apply PTree.eq. exact L.eq. + decide equality. +Qed. + +Definition get (p: positive) (x: t) : L.t := + match x with + | Bot_except m => + match m!p with None => L.bot | Some x => x end + | Top_except m => + match m!p with None => L.top | Some x => x end + end. + +Definition set (p: positive) (v: L.t) (x: t) : t := + match x with + | Bot_except m => + Bot_except (PTree.set p v m) + | Top_except m => + Top_except (PTree.set p v m) + end. + +Lemma gss: + forall p v x, + get p (set p v x) = v. +Proof. + intros. destruct x; simpl; rewrite PTree.gss; auto. +Qed. + +Lemma gso: + forall p q v x, + p <> q -> get p (set q v x) = get p x. +Proof. + intros. destruct x; simpl; rewrite PTree.gso; auto. +Qed. + +Definition ge (x y: t) : Prop := + forall p, L.ge (get p x) (get p y). + +Lemma ge_refl: forall x, ge x x. +Proof. + unfold ge; intros. apply L.ge_refl. +Qed. + +Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. +Proof. + unfold ge; intros. apply L.ge_trans with (get p y); auto. +Qed. + +Definition bot := Bot_except (PTree.empty L.t). + +Lemma get_bot: forall p, get p bot = L.bot. +Proof. + unfold bot; intros; simpl. rewrite PTree.gempty. auto. +Qed. + +Lemma ge_bot: forall x, ge x bot. +Proof. + unfold ge; intros. rewrite get_bot. apply L.ge_bot. +Qed. + +Definition top := Top_except (PTree.empty L.t). + +Lemma get_top: forall p, get p top = L.top. +Proof. + unfold top; intros; simpl. rewrite PTree.gempty. auto. +Qed. + +Lemma ge_top: forall x, ge top x. +Proof. + unfold ge; intros. rewrite get_top. apply L.ge_top. +Qed. + +Definition lub (x y: t) : t := + match x, y with + | Bot_except m, Bot_except n => + Bot_except + (PTree.combine + (fun a b => + match a, b with + | Some u, Some v => Some (L.lub u v) + | None, _ => b + | _, None => a + end) + m n) + | Bot_except m, Top_except n => + Top_except + (PTree.combine + (fun a b => + match a, b with + | Some u, Some v => Some (L.lub u v) + | None, _ => b + | _, None => None + end) + m n) + | Top_except m, Bot_except n => + Top_except + (PTree.combine + (fun a b => + match a, b with + | Some u, Some v => Some (L.lub u v) + | None, _ => None + | _, None => a + end) + m n) + | Top_except m, Top_except n => + Top_except + (PTree.combine + (fun a b => + match a, b with + | Some u, Some v => Some (L.lub u v) + | _, _ => None + end) + m n) + end. + +Lemma lub_commut: + forall x y, lub x y = lub y x. +Proof. + destruct x; destruct y; unfold lub; decEq; + apply PTree.combine_commut; intros; + (destruct i; destruct j; auto; decEq; apply L.lub_commut). +Qed. + +Lemma ge_lub_left: + forall x y, ge (lub x y) x. +Proof. + unfold ge, get, lub; intros; destruct x; destruct y. + + rewrite PTree.gcombine. + destruct t0!p. destruct t1!p. apply L.ge_lub_left. + apply L.ge_refl. destruct t1!p. apply L.ge_bot. apply L.ge_refl. + auto. + + rewrite PTree.gcombine. + destruct t0!p. destruct t1!p. apply L.ge_lub_left. + apply L.ge_top. destruct t1!p. apply L.ge_bot. apply L.ge_bot. + auto. + + rewrite PTree.gcombine. + destruct t0!p. destruct t1!p. apply L.ge_lub_left. + apply L.ge_refl. apply L.ge_refl. auto. + + rewrite PTree.gcombine. + destruct t0!p. destruct t1!p. apply L.ge_lub_left. + apply L.ge_top. apply L.ge_refl. + auto. +Qed. + +End LPMap. + +(** * Flat semi-lattice *) + +(** Given a type with decidable equality [X], the following functor + returns a semi-lattice structure over [X.t] complemented with + a top and a bottom element. The ordering is the flat ordering + [Bot < Inj x < Top]. *) + +Module LFlat(X: EQUALITY_TYPE) <: SEMILATTICE_WITH_TOP. + +Inductive t_ : Set := + | Bot: t_ + | Inj: X.t -> t_ + | Top: t_. + +Definition t : Set := t_. + +Lemma eq: forall (x y: t), {x=y} + {x<>y}. +Proof. + decide equality. apply X.eq. +Qed. + +Definition ge (x y: t) : Prop := + match x, y with + | Top, _ => True + | _, Bot => True + | Inj a, Inj b => a = b + | _, _ => False + end. + +Lemma ge_refl: forall x, ge x x. +Proof. + unfold ge; destruct x; auto. +Qed. + +Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. +Proof. + unfold ge; destruct x; destruct y; try destruct z; intuition. + transitivity t1; auto. +Qed. + +Definition bot: t := Bot. + +Lemma ge_bot: forall x, ge x bot. +Proof. + destruct x; simpl; auto. +Qed. + +Definition top: t := Top. + +Lemma ge_top: forall x, ge top x. +Proof. + destruct x; simpl; auto. +Qed. + +Definition lub (x y: t) : t := + match x, y with + | Bot, _ => y + | _, Bot => x + | Top, _ => Top + | _, Top => Top + | Inj a, Inj b => if X.eq a b then Inj a else Top + end. + +Lemma lub_commut: forall x y, lub x y = lub y x. +Proof. + destruct x; destruct y; simpl; auto. + case (X.eq t0 t1); case (X.eq t1 t0); intros; congruence. +Qed. + +Lemma ge_lub_left: forall x y, ge (lub x y) x. +Proof. + destruct x; destruct y; simpl; auto. + case (X.eq t0 t1); simpl; auto. +Qed. + +End LFlat. + +(** * Boolean semi-lattice *) + +(** This semi-lattice has only two elements, [bot] and [top], trivially + ordered. *) + +Module LBoolean <: SEMILATTICE_WITH_TOP. + +Definition t := bool. + +Lemma eq: forall (x y: t), {x=y} + {x<>y}. +Proof. decide equality. Qed. + +Definition ge (x y: t) : Prop := x = y \/ x = true. + +Lemma ge_refl: forall x, ge x x. +Proof. unfold ge; tauto. Qed. + +Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. +Proof. unfold ge; intuition congruence. Qed. + +Definition bot := false. + +Lemma ge_bot: forall x, ge x bot. +Proof. destruct x; compute; tauto. Qed. + +Definition top := true. + +Lemma ge_top: forall x, ge top x. +Proof. unfold ge, top; tauto. Qed. + +Definition lub (x y: t) := x || y. + +Lemma lub_commut: forall x y, lub x y = lub y x. +Proof. intros; unfold lub. apply orb_comm. Qed. + +Lemma ge_lub_left: forall x y, ge (lub x y) x. +Proof. destruct x; destruct y; compute; tauto. Qed. + +End LBoolean. + + diff --git a/lib/Maps.v b/lib/Maps.v new file mode 100644 index 00000000..69690918 --- /dev/null +++ b/lib/Maps.v @@ -0,0 +1,1034 @@ +(** Applicative finite maps are the main data structure used in this + project. A finite map associates data to keys. The two main operations + are [set k d m], which returns a map identical to [m] except that [d] + is associated to [k], and [get k m] which returns the data associated + to key [k] in map [m]. In this library, we distinguish two kinds of maps: +- Trees: the [get] operation returns an option type, either [None] + if no data is associated to the key, or [Some d] otherwise. +- Maps: the [get] operation always returns a data. If no data was explicitly + associated with the key, a default data provided at map initialization time + is returned. + + In this library, we provide efficient implementations of trees and + maps whose keys range over the type [positive] of binary positive + integers or any type that can be injected into [positive]. The + implementation is based on radix-2 search trees (uncompressed + Patricia trees) and guarantees logarithmic-time operations. An + inefficient implementation of maps as functions is also provided. +*) + +Require Import Coqlib. + +Set Implicit Arguments. + +(** * The abstract signatures of trees *) + +Module Type TREE. + Variable elt: Set. + Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}. + Variable t: Set -> Set. + Variable eq: forall (A: Set), (forall (x y: A), {x=y} + {x<>y}) -> + forall (a b: t A), {a = b} + {a <> b}. + Variable empty: forall (A: Set), t A. + Variable get: forall (A: Set), elt -> t A -> option A. + Variable set: forall (A: Set), elt -> A -> t A -> t A. + Variable remove: forall (A: Set), elt -> t A -> t A. + + (** The ``good variables'' properties for trees, expressing + commutations between [get], [set] and [remove]. *) + Hypothesis gempty: + forall (A: Set) (i: elt), get i (empty A) = None. + Hypothesis gss: + forall (A: Set) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x. + Hypothesis gso: + forall (A: Set) (i j: elt) (x: A) (m: t A), + i <> j -> get i (set j x m) = get i m. + Hypothesis gsspec: + forall (A: Set) (i j: elt) (x: A) (m: t A), + get i (set j x m) = if elt_eq i j then Some x else get i m. + Hypothesis gsident: + forall (A: Set) (i: elt) (m: t A) (v: A), + get i m = Some v -> set i v m = m. + (* We could implement the following, but it's not needed for the moment. + Hypothesis grident: + forall (A: Set) (i: elt) (m: t A) (v: A), + get i m = None -> remove i m = m. + *) + Hypothesis grs: + forall (A: Set) (i: elt) (m: t A), get i (remove i m) = None. + Hypothesis gro: + forall (A: Set) (i j: elt) (m: t A), + i <> j -> get i (remove j m) = get i m. + + (** Applying a function to all data of a tree. *) + Variable map: + forall (A B: Set), (elt -> A -> B) -> t A -> t B. + Hypothesis gmap: + forall (A B: Set) (f: elt -> A -> B) (i: elt) (m: t A), + get i (map f m) = option_map (f i) (get i m). + + (** Applying a function pairwise to all data of two trees. *) + Variable combine: + forall (A: Set), (option A -> option A -> option A) -> t A -> t A -> t A. + Hypothesis gcombine: + forall (A: Set) (f: option A -> option A -> option A) + (m1 m2: t A) (i: elt), + f None None = None -> + get i (combine f m1 m2) = f (get i m1) (get i m2). + Hypothesis combine_commut: + forall (A: Set) (f g: option A -> option A -> option A), + (forall (i j: option A), f i j = g j i) -> + forall (m1 m2: t A), + combine f m1 m2 = combine g m2 m1. + + (** Enumerating the bindings of a tree. *) + Variable elements: + forall (A: Set), t A -> list (elt * A). + Hypothesis elements_correct: + forall (A: Set) (m: t A) (i: elt) (v: A), + get i m = Some v -> In (i, v) (elements m). + Hypothesis elements_complete: + forall (A: Set) (m: t A) (i: elt) (v: A), + In (i, v) (elements m) -> get i m = Some v. + Hypothesis elements_keys_norepet: + forall (A: Set) (m: t A), + list_norepet (List.map (@fst elt A) (elements m)). + + (** Folding a function over all bindings of a tree. *) + Variable fold: + forall (A B: Set), (B -> elt -> A -> B) -> t A -> B -> B. + Hypothesis fold_spec: + forall (A B: Set) (f: B -> elt -> A -> B) (v: B) (m: t A), + fold f m v = + List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v. +End TREE. + +(** * The abstract signatures of maps *) + +Module Type MAP. + Variable elt: Set. + Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}. + Variable t: Set -> Set. + Variable init: forall (A: Set), A -> t A. + Variable get: forall (A: Set), elt -> t A -> A. + Variable set: forall (A: Set), elt -> A -> t A -> t A. + Hypothesis gi: + forall (A: Set) (i: elt) (x: A), get i (init x) = x. + Hypothesis gss: + forall (A: Set) (i: elt) (x: A) (m: t A), get i (set i x m) = x. + Hypothesis gso: + forall (A: Set) (i j: elt) (x: A) (m: t A), + i <> j -> get i (set j x m) = get i m. + Hypothesis gsspec: + forall (A: Set) (i j: elt) (x: A) (m: t A), + get i (set j x m) = if elt_eq i j then x else get i m. + Hypothesis gsident: + forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m. + Variable map: forall (A B: Set), (A -> B) -> t A -> t B. + Hypothesis gmap: + forall (A B: Set) (f: A -> B) (i: elt) (m: t A), + get i (map f m) = f(get i m). +End MAP. + +(** * An implementation of trees over type [positive] *) + +Module PTree <: TREE. + Definition elt := positive. + Definition elt_eq := peq. + + Inductive tree (A : Set) : Set := + | Leaf : tree A + | Node : tree A -> option A -> tree A -> tree A + . + Implicit Arguments Leaf [A]. + Implicit Arguments Node [A]. + + Definition t := tree. + + Theorem eq : forall (A : Set), + (forall (x y: A), {x=y} + {x<>y}) -> + forall (a b : t A), {a = b} + {a <> b}. + Proof. + intros A eqA. + decide equality. + generalize o o0; decide equality. + Qed. + + Definition empty (A : Set) := (Leaf : t A). + + Fixpoint get (A : Set) (i : positive) (m : t A) {struct i} : option A := + match m with + | Leaf => None + | Node l o r => + match i with + | xH => o + | xO ii => get ii l + | xI ii => get ii r + end + end. + + Fixpoint set (A : Set) (i : positive) (v : A) (m : t A) {struct i} : t A := + match m with + | Leaf => + match i with + | xH => Node Leaf (Some v) Leaf + | xO ii => Node (set ii v Leaf) None Leaf + | xI ii => Node Leaf None (set ii v Leaf) + end + | Node l o r => + match i with + | xH => Node l (Some v) r + | xO ii => Node (set ii v l) o r + | xI ii => Node l o (set ii v r) + end + end. + + Fixpoint remove (A : Set) (i : positive) (m : t A) {struct i} : t A := + match i with + | xH => + match m with + | Leaf => Leaf + | Node Leaf o Leaf => Leaf + | Node l o r => Node l None r + end + | xO ii => + match m with + | Leaf => Leaf + | Node l None Leaf => + match remove ii l with + | Leaf => Leaf + | mm => Node mm None Leaf + end + | Node l o r => Node (remove ii l) o r + end + | xI ii => + match m with + | Leaf => Leaf + | Node Leaf None r => + match remove ii r with + | Leaf => Leaf + | mm => Node Leaf None mm + end + | Node l o r => Node l o (remove ii r) + end + end. + + Theorem gempty: + forall (A: Set) (i: positive), get i (empty A) = None. + Proof. + induction i; simpl; auto. + Qed. + + Theorem gss: + forall (A: Set) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x. + Proof. + induction i; destruct m; simpl; auto. + Qed. + + Lemma gleaf : forall (A : Set) (i : positive), get i (Leaf : t A) = None. + Proof. exact gempty. Qed. + + Theorem gso: + forall (A: Set) (i j: positive) (x: A) (m: t A), + i <> j -> get i (set j x m) = get i m. + Proof. + induction i; intros; destruct j; destruct m; simpl; + try rewrite <- (gleaf A i); auto; try apply IHi; congruence. + Qed. + + Theorem gsspec: + forall (A: Set) (i j: positive) (x: A) (m: t A), + get i (set j x m) = if peq i j then Some x else get i m. + Proof. + intros. + destruct (peq i j); [ rewrite e; apply gss | apply gso; auto ]. + Qed. + + Theorem gsident: + forall (A: Set) (i: positive) (m: t A) (v: A), + get i m = Some v -> set i v m = m. + Proof. + induction i; intros; destruct m; simpl; simpl in H; try congruence. + rewrite (IHi m2 v H); congruence. + rewrite (IHi m1 v H); congruence. + Qed. + + Lemma rleaf : forall (A : Set) (i : positive), remove i (Leaf : t A) = Leaf. + Proof. destruct i; simpl; auto. Qed. + + Theorem grs: + forall (A: Set) (i: positive) (m: t A), get i (remove i m) = None. + Proof. + induction i; destruct m. + simpl; auto. + destruct m1; destruct o; destruct m2 as [ | ll oo rr]; simpl; auto. + rewrite (rleaf A i); auto. + cut (get i (remove i (Node ll oo rr)) = None). + destruct (remove i (Node ll oo rr)); auto; apply IHi. + apply IHi. + simpl; auto. + destruct m1 as [ | ll oo rr]; destruct o; destruct m2; simpl; auto. + rewrite (rleaf A i); auto. + cut (get i (remove i (Node ll oo rr)) = None). + destruct (remove i (Node ll oo rr)); auto; apply IHi. + apply IHi. + simpl; auto. + destruct m1; destruct m2; simpl; auto. + Qed. + + Theorem gro: + forall (A: Set) (i j: positive) (m: t A), + i <> j -> get i (remove j m) = get i m. + Proof. + induction i; intros; destruct j; destruct m; + try rewrite (rleaf A (xI j)); + try rewrite (rleaf A (xO j)); + try rewrite (rleaf A 1); auto; + destruct m1; destruct o; destruct m2; + simpl; + try apply IHi; try congruence; + try rewrite (rleaf A j); auto; + try rewrite (gleaf A i); auto. + cut (get i (remove j (Node m2_1 o m2_2)) = get i (Node m2_1 o m2_2)); + [ destruct (remove j (Node m2_1 o m2_2)); try rewrite (gleaf A i); auto + | apply IHi; congruence ]. + destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf A i); + auto. + destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf A i); + auto. + cut (get i (remove j (Node m1_1 o0 m1_2)) = get i (Node m1_1 o0 m1_2)); + [ destruct (remove j (Node m1_1 o0 m1_2)); try rewrite (gleaf A i); auto + | apply IHi; congruence ]. + destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf A i); + auto. + destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf A i); + auto. + Qed. + + Fixpoint append (i j : positive) {struct i} : positive := + match i with + | xH => j + | xI ii => xI (append ii j) + | xO ii => xO (append ii j) + end. + + Lemma append_assoc_0 : forall (i j : positive), + append i (xO j) = append (append i (xO xH)) j. + Proof. + induction i; intros; destruct j; simpl; + try rewrite (IHi (xI j)); + try rewrite (IHi (xO j)); + try rewrite <- (IHi xH); + auto. + Qed. + + Lemma append_assoc_1 : forall (i j : positive), + append i (xI j) = append (append i (xI xH)) j. + Proof. + induction i; intros; destruct j; simpl; + try rewrite (IHi (xI j)); + try rewrite (IHi (xO j)); + try rewrite <- (IHi xH); + auto. + Qed. + + Lemma append_neutral_r : forall (i : positive), append i xH = i. + Proof. + induction i; simpl; congruence. + Qed. + + Lemma append_neutral_l : forall (i : positive), append xH i = i. + Proof. + simpl; auto. + Qed. + + Fixpoint xmap (A B : Set) (f : positive -> A -> B) (m : t A) (i : positive) + {struct m} : t B := + match m with + | Leaf => Leaf + | Node l o r => Node (xmap f l (append i (xO xH))) + (option_map (f i) o) + (xmap f r (append i (xI xH))) + end. + + Definition map (A B : Set) (f : positive -> A -> B) m := xmap f m xH. + + Lemma xgmap: + forall (A B: Set) (f: positive -> A -> B) (i j : positive) (m: t A), + get i (xmap f m j) = option_map (f (append j i)) (get i m). + Proof. + induction i; intros; destruct m; simpl; auto. + rewrite (append_assoc_1 j i); apply IHi. + rewrite (append_assoc_0 j i); apply IHi. + rewrite (append_neutral_r j); auto. + Qed. + + Theorem gmap: + forall (A B: Set) (f: positive -> A -> B) (i: positive) (m: t A), + get i (map f m) = option_map (f i) (get i m). + Proof. + intros. + unfold map. + replace (f i) with (f (append xH i)). + apply xgmap. + rewrite append_neutral_l; auto. + Qed. + + Fixpoint xcombine_l (A : Set) (f : option A -> option A -> option A) + (m : t A) {struct m} : t A := + match m with + | Leaf => Leaf + | Node l o r => Node (xcombine_l f l) (f o None) (xcombine_l f r) + end. + + Lemma xgcombine_l : + forall (A : Set) (f : option A -> option A -> option A) + (i : positive) (m : t A), + f None None = None -> get i (xcombine_l f m) = f (get i m) None. + Proof. + induction i; intros; destruct m; simpl; auto. + Qed. + + Fixpoint xcombine_r (A : Set) (f : option A -> option A -> option A) + (m : t A) {struct m} : t A := + match m with + | Leaf => Leaf + | Node l o r => Node (xcombine_r f l) (f None o) (xcombine_r f r) + end. + + Lemma xgcombine_r : + forall (A : Set) (f : option A -> option A -> option A) + (i : positive) (m : t A), + f None None = None -> get i (xcombine_r f m) = f None (get i m). + Proof. + induction i; intros; destruct m; simpl; auto. + Qed. + + Fixpoint combine (A : Set) (f : option A -> option A -> option A) + (m1 m2 : t A) {struct m1} : t A := + match m1 with + | Leaf => xcombine_r f m2 + | Node l1 o1 r1 => + match m2 with + | Leaf => xcombine_l f m1 + | Node l2 o2 r2 => Node (combine f l1 l2) (f o1 o2) (combine f r1 r2) + end + end. + + Lemma xgcombine: + forall (A: Set) (f: option A -> option A -> option A) (i: positive) + (m1 m2: t A), + f None None = None -> + get i (combine f m1 m2) = f (get i m1) (get i m2). + Proof. + induction i; intros; destruct m1; destruct m2; simpl; auto; + try apply xgcombine_r; try apply xgcombine_l; auto. + Qed. + + Theorem gcombine: + forall (A: Set) (f: option A -> option A -> option A) + (m1 m2: t A) (i: positive), + f None None = None -> + get i (combine f m1 m2) = f (get i m1) (get i m2). + Proof. + intros A f m1 m2 i H; exact (xgcombine f i m1 m2 H). + Qed. + + Lemma xcombine_lr : + forall (A : Set) (f g : option A -> option A -> option A) (m : t A), + (forall (i j : option A), f i j = g j i) -> + xcombine_l f m = xcombine_r g m. + Proof. + induction m; intros; simpl; auto. + rewrite IHm1; auto. + rewrite IHm2; auto. + rewrite H; auto. + Qed. + + Theorem combine_commut: + forall (A: Set) (f g: option A -> option A -> option A), + (forall (i j: option A), f i j = g j i) -> + forall (m1 m2: t A), + combine f m1 m2 = combine g m2 m1. + Proof. + intros A f g EQ1. + assert (EQ2: forall (i j: option A), g i j = f j i). + intros; auto. + induction m1; intros; destruct m2; simpl; + try rewrite EQ1; + repeat rewrite (xcombine_lr f g); + repeat rewrite (xcombine_lr g f); + auto. + rewrite IHm1_1. + rewrite IHm1_2. + auto. + Qed. + + Fixpoint xelements (A : Set) (m : t A) (i : positive) {struct m} + : list (positive * A) := + match m with + | Leaf => nil + | Node l None r => + (xelements l (append i (xO xH))) ++ (xelements r (append i (xI xH))) + | Node l (Some x) r => + (xelements l (append i (xO xH))) + ++ ((i, x) :: xelements r (append i (xI xH))) + end. + + (* Note: function [xelements] above is inefficient. We should apply + deforestation to it, but that makes the proofs even harder. *) + + Definition elements A (m : t A) := xelements m xH. + + Lemma xelements_correct: + forall (A: Set) (m: t A) (i j : positive) (v: A), + get i m = Some v -> In (append j i, v) (xelements m j). + Proof. + induction m; intros. + rewrite (gleaf A i) in H; congruence. + destruct o; destruct i; simpl; simpl in H. + rewrite append_assoc_1; apply in_or_app; right; apply in_cons; + apply IHm2; auto. + rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. + rewrite append_neutral_r; apply in_or_app; injection H; + intro EQ; rewrite EQ; right; apply in_eq. + rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto. + rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. + congruence. + Qed. + + Theorem elements_correct: + forall (A: Set) (m: t A) (i: positive) (v: A), + get i m = Some v -> In (i, v) (elements m). + Proof. + intros A m i v H. + exact (xelements_correct m i xH H). + Qed. + + Fixpoint xget (A : Set) (i j : positive) (m : t A) {struct j} : option A := + match i, j with + | _, xH => get i m + | xO ii, xO jj => xget ii jj m + | xI ii, xI jj => xget ii jj m + | _, _ => None + end. + + Lemma xget_left : + forall (A : Set) (j i : positive) (m1 m2 : t A) (o : option A) (v : A), + xget i (append j (xO xH)) m1 = Some v -> xget i j (Node m1 o m2) = Some v. + Proof. + induction j; intros; destruct i; simpl; simpl in H; auto; try congruence. + destruct i; congruence. + Qed. + + Lemma xelements_ii : + forall (A: Set) (m: t A) (i j : positive) (v: A), + In (xI i, v) (xelements m (xI j)) -> In (i, v) (xelements m j). + Proof. + induction m. + simpl; auto. + intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H); + apply in_or_app. + left; apply IHm1; auto. + right; destruct (in_inv H0). + injection H1; intros EQ1 EQ2; rewrite EQ1; rewrite EQ2; apply in_eq. + apply in_cons; apply IHm2; auto. + left; apply IHm1; auto. + right; apply IHm2; auto. + Qed. + + Lemma xelements_io : + forall (A: Set) (m: t A) (i j : positive) (v: A), + ~In (xI i, v) (xelements m (xO j)). + Proof. + induction m. + simpl; auto. + intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). + apply (IHm1 _ _ _ H0). + destruct (in_inv H0). + congruence. + apply (IHm2 _ _ _ H1). + apply (IHm1 _ _ _ H0). + apply (IHm2 _ _ _ H0). + Qed. + + Lemma xelements_oo : + forall (A: Set) (m: t A) (i j : positive) (v: A), + In (xO i, v) (xelements m (xO j)) -> In (i, v) (xelements m j). + Proof. + induction m. + simpl; auto. + intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H); + apply in_or_app. + left; apply IHm1; auto. + right; destruct (in_inv H0). + injection H1; intros EQ1 EQ2; rewrite EQ1; rewrite EQ2; apply in_eq. + apply in_cons; apply IHm2; auto. + left; apply IHm1; auto. + right; apply IHm2; auto. + Qed. + + Lemma xelements_oi : + forall (A: Set) (m: t A) (i j : positive) (v: A), + ~In (xO i, v) (xelements m (xI j)). + Proof. + induction m. + simpl; auto. + intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). + apply (IHm1 _ _ _ H0). + destruct (in_inv H0). + congruence. + apply (IHm2 _ _ _ H1). + apply (IHm1 _ _ _ H0). + apply (IHm2 _ _ _ H0). + Qed. + + Lemma xelements_ih : + forall (A: Set) (m1 m2: t A) (o: option A) (i : positive) (v: A), + In (xI i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m2 xH). + Proof. + destruct o; simpl; intros; destruct (in_app_or _ _ _ H). + absurd (In (xI i, v) (xelements m1 2)); auto; apply xelements_io; auto. + destruct (in_inv H0). + congruence. + apply xelements_ii; auto. + absurd (In (xI i, v) (xelements m1 2)); auto; apply xelements_io; auto. + apply xelements_ii; auto. + Qed. + + Lemma xelements_oh : + forall (A: Set) (m1 m2: t A) (o: option A) (i : positive) (v: A), + In (xO i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m1 xH). + Proof. + destruct o; simpl; intros; destruct (in_app_or _ _ _ H). + apply xelements_oo; auto. + destruct (in_inv H0). + congruence. + absurd (In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto. + apply xelements_oo; auto. + absurd (In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto. + Qed. + + Lemma xelements_hi : + forall (A: Set) (m: t A) (i : positive) (v: A), + ~In (xH, v) (xelements m (xI i)). + Proof. + induction m; intros. + simpl; auto. + destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). + generalize H0; apply IHm1; auto. + destruct (in_inv H0). + congruence. + generalize H1; apply IHm2; auto. + generalize H0; apply IHm1; auto. + generalize H0; apply IHm2; auto. + Qed. + + Lemma xelements_ho : + forall (A: Set) (m: t A) (i : positive) (v: A), + ~In (xH, v) (xelements m (xO i)). + Proof. + induction m; intros. + simpl; auto. + destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). + generalize H0; apply IHm1; auto. + destruct (in_inv H0). + congruence. + generalize H1; apply IHm2; auto. + generalize H0; apply IHm1; auto. + generalize H0; apply IHm2; auto. + Qed. + + Lemma get_xget_h : + forall (A: Set) (m: t A) (i: positive), get i m = xget i xH m. + Proof. + destruct i; simpl; auto. + Qed. + + Lemma xelements_complete: + forall (A: Set) (i j : positive) (m: t A) (v: A), + In (i, v) (xelements m j) -> xget i j m = Some v. + Proof. + induction i; simpl; intros; destruct j; simpl. + apply IHi; apply xelements_ii; auto. + absurd (In (xI i, v) (xelements m (xO j))); auto; apply xelements_io. + destruct m. + simpl in H; tauto. + rewrite get_xget_h. apply IHi. apply (xelements_ih _ _ _ _ _ H). + absurd (In (xO i, v) (xelements m (xI j))); auto; apply xelements_oi. + apply IHi; apply xelements_oo; auto. + destruct m. + simpl in H; tauto. + rewrite get_xget_h. apply IHi. apply (xelements_oh _ _ _ _ _ H). + absurd (In (xH, v) (xelements m (xI j))); auto; apply xelements_hi. + absurd (In (xH, v) (xelements m (xO j))); auto; apply xelements_ho. + destruct m. + simpl in H; tauto. + destruct o; simpl in H; destruct (in_app_or _ _ _ H). + absurd (In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho. + destruct (in_inv H0). + congruence. + absurd (In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi. + absurd (In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho. + absurd (In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi. + Qed. + + Theorem elements_complete: + forall (A: Set) (m: t A) (i: positive) (v: A), + In (i, v) (elements m) -> get i m = Some v. + Proof. + intros A m i v H. + unfold elements in H. + rewrite get_xget_h. + exact (xelements_complete i xH m v H). + Qed. + + Lemma in_xelements: + forall (A: Set) (m: t A) (i k: positive) (v: A), + In (k, v) (xelements m i) -> + exists j, k = append i j. + Proof. + induction m; simpl; intros. + tauto. + assert (k = i \/ In (k, v) (xelements m1 (append i 2)) + \/ In (k, v) (xelements m2 (append i 3))). + destruct o. + elim (in_app_or _ _ _ H); simpl; intuition. + replace k with i. tauto. congruence. + elim (in_app_or _ _ _ H); simpl; intuition. + elim H0; intro. + exists xH. rewrite append_neutral_r. auto. + elim H1; intro. + elim (IHm1 _ _ _ H2). intros k1 EQ. rewrite EQ. + rewrite <- append_assoc_0. exists (xO k1); auto. + elim (IHm2 _ _ _ H2). intros k1 EQ. rewrite EQ. + rewrite <- append_assoc_1. exists (xI k1); auto. + Qed. + + Definition xkeys (A: Set) (m: t A) (i: positive) := + List.map (@fst positive A) (xelements m i). + + Lemma in_xkeys: + forall (A: Set) (m: t A) (i k: positive), + In k (xkeys m i) -> + exists j, k = append i j. + Proof. + unfold xkeys; intros. + elim (list_in_map_inv _ _ _ H). intros [k1 v1] [EQ IN]. + simpl in EQ; subst k1. apply in_xelements with A m v1. auto. + Qed. + + Remark list_append_cons_norepet: + forall (A: Set) (l1 l2: list A) (x: A), + list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 -> + ~In x l1 -> ~In x l2 -> + list_norepet (l1 ++ x :: l2). + Proof. + intros. apply list_norepet_append_commut. simpl; constructor. + red; intros. elim (in_app_or _ _ _ H4); intro; tauto. + apply list_norepet_append; auto. + apply list_disjoint_sym; auto. + Qed. + + Lemma append_injective: + forall i j1 j2, append i j1 = append i j2 -> j1 = j2. + Proof. + induction i; simpl; intros. + apply IHi. congruence. + apply IHi. congruence. + auto. + Qed. + + Lemma xelements_keys_norepet: + forall (A: Set) (m: t A) (i: positive), + list_norepet (xkeys m i). + Proof. + induction m; unfold xkeys; simpl; fold xkeys; intros. + constructor. + assert (list_disjoint (xkeys m1 (append i 2)) (xkeys m2 (append i 3))). + red; intros; red; intro. subst y. + elim (in_xkeys _ _ _ H); intros j1 EQ1. + elim (in_xkeys _ _ _ H0); intros j2 EQ2. + rewrite EQ1 in EQ2. + rewrite <- append_assoc_0 in EQ2. + rewrite <- append_assoc_1 in EQ2. + generalize (append_injective _ _ _ EQ2). congruence. + assert (forall (m: t A) j, + j = 2%positive \/ j = 3%positive -> + ~In i (xkeys m (append i j))). + intros; red; intros. + elim (in_xkeys _ _ _ H1); intros k EQ. + assert (EQ1: append i xH = append (append i j) k). + rewrite append_neutral_r. auto. + elim H0; intro; subst j; + try (rewrite <- append_assoc_0 in EQ1); + try (rewrite <- append_assoc_1 in EQ1); + generalize (append_injective _ _ _ EQ1); congruence. + destruct o; rewrite list_append_map; simpl; + change (List.map (@fst positive A) (xelements m1 (append i 2))) + with (xkeys m1 (append i 2)); + change (List.map (@fst positive A) (xelements m2 (append i 3))) + with (xkeys m2 (append i 3)). + apply list_append_cons_norepet; auto. + apply list_norepet_append; auto. + Qed. + + Theorem elements_keys_norepet: + forall (A: Set) (m: t A), + list_norepet (List.map (@fst elt A) (elements m)). + Proof. + intros. change (list_norepet (xkeys m 1)). apply xelements_keys_norepet. + Qed. + + Definition fold (A B : Set) (f: B -> positive -> A -> B) (tr: t A) (v: B) := + List.fold_left (fun a p => f a (fst p) (snd p)) (elements tr) v. + + Theorem fold_spec: + forall (A B: Set) (f: B -> positive -> A -> B) (v: B) (m: t A), + fold f m v = + List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v. + Proof. + intros; unfold fold; auto. + Qed. + +End PTree. + +(** * An implementation of maps over type [positive] *) + +Module PMap <: MAP. + Definition elt := positive. + Definition elt_eq := peq. + + Definition t (A : Set) : Set := (A * PTree.t A)%type. + + Definition init (A : Set) (x : A) := + (x, PTree.empty A). + + Definition get (A : Set) (i : positive) (m : t A) := + match PTree.get i (snd m) with + | Some x => x + | None => fst m + end. + + Definition set (A : Set) (i : positive) (x : A) (m : t A) := + (fst m, PTree.set i x (snd m)). + + Theorem gi: + forall (A: Set) (i: positive) (x: A), get i (init x) = x. + Proof. + intros. unfold init. unfold get. simpl. rewrite PTree.gempty. auto. + Qed. + + Theorem gss: + forall (A: Set) (i: positive) (x: A) (m: t A), get i (set i x m) = x. + Proof. + intros. unfold get. unfold set. simpl. rewrite PTree.gss. auto. + Qed. + + Theorem gso: + forall (A: Set) (i j: positive) (x: A) (m: t A), + i <> j -> get i (set j x m) = get i m. + Proof. + intros. unfold get. unfold set. simpl. rewrite PTree.gso; auto. + Qed. + + Theorem gsspec: + forall (A: Set) (i j: positive) (x: A) (m: t A), + get i (set j x m) = if peq i j then x else get i m. + Proof. + intros. destruct (peq i j). + rewrite e. apply gss. auto. + apply gso. auto. + Qed. + + Theorem gsident: + forall (A: Set) (i j: positive) (m: t A), + get j (set i (get i m) m) = get j m. + Proof. + intros. destruct (peq i j). + rewrite e. rewrite gss. auto. + rewrite gso; auto. + Qed. + + Definition map (A B : Set) (f : A -> B) (m : t A) : t B := + (f (fst m), PTree.map (fun _ => f) (snd m)). + + Theorem gmap: + forall (A B: Set) (f: A -> B) (i: positive) (m: t A), + get i (map f m) = f(get i m). + Proof. + intros. unfold map. unfold get. simpl. rewrite PTree.gmap. + unfold option_map. destruct (PTree.get i (snd m)); auto. + Qed. + +End PMap. + +(** * An implementation of maps over any type that injects into type [positive] *) + +Module Type INDEXED_TYPE. + Variable t: Set. + Variable index: t -> positive. + Hypothesis index_inj: forall (x y: t), index x = index y -> x = y. + Variable eq: forall (x y: t), {x = y} + {x <> y}. +End INDEXED_TYPE. + +Module IMap(X: INDEXED_TYPE). + + Definition elt := X.t. + Definition elt_eq := X.eq. + Definition t : Set -> Set := PMap.t. + Definition init (A: Set) (x: A) := PMap.init x. + Definition get (A: Set) (i: X.t) (m: t A) := PMap.get (X.index i) m. + Definition set (A: Set) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m. + Definition map (A B: Set) (f: A -> B) (m: t A) : t B := PMap.map f m. + + Lemma gi: + forall (A: Set) (x: A) (i: X.t), get i (init x) = x. + Proof. + intros. unfold get, init. apply PMap.gi. + Qed. + + Lemma gss: + forall (A: Set) (i: X.t) (x: A) (m: t A), get i (set i x m) = x. + Proof. + intros. unfold get, set. apply PMap.gss. + Qed. + + Lemma gso: + forall (A: Set) (i j: X.t) (x: A) (m: t A), + i <> j -> get i (set j x m) = get i m. + Proof. + intros. unfold get, set. apply PMap.gso. + red. intro. apply H. apply X.index_inj; auto. + Qed. + + Lemma gsspec: + forall (A: Set) (i j: X.t) (x: A) (m: t A), + get i (set j x m) = if X.eq i j then x else get i m. + Proof. + intros. unfold get, set. + rewrite PMap.gsspec. + case (X.eq i j); intro. + subst j. rewrite peq_true. reflexivity. + rewrite peq_false. reflexivity. + red; intro. elim n. apply X.index_inj; auto. + Qed. + + Lemma gmap: + forall (A B: Set) (f: A -> B) (i: X.t) (m: t A), + get i (map f m) = f(get i m). + Proof. + intros. unfold map, get. apply PMap.gmap. + Qed. + +End IMap. + +Module ZIndexed. + Definition t := Z. + Definition index (z: Z): positive := + match z with + | Z0 => xH + | Zpos p => xO p + | Zneg p => xI p + end. + Lemma index_inj: forall (x y: Z), index x = index y -> x = y. + Proof. + unfold index; destruct x; destruct y; intros; + try discriminate; try reflexivity. + congruence. + congruence. + Qed. + Definition eq := zeq. +End ZIndexed. + +Module ZMap := IMap(ZIndexed). + +Module NIndexed. + Definition t := N. + Definition index (n: N): positive := + match n with + | N0 => xH + | Npos p => xO p + end. + Lemma index_inj: forall (x y: N), index x = index y -> x = y. + Proof. + unfold index; destruct x; destruct y; intros; + try discriminate; try reflexivity. + congruence. + Qed. + Lemma eq: forall (x y: N), {x = y} + {x <> y}. + Proof. + decide equality. apply peq. + Qed. +End NIndexed. + +Module NMap := IMap(NIndexed). + +(** * An implementation of maps over any type with decidable equality *) + +Module Type EQUALITY_TYPE. + Variable t: Set. + Variable eq: forall (x y: t), {x = y} + {x <> y}. +End EQUALITY_TYPE. + +Module EMap(X: EQUALITY_TYPE) <: MAP. + + Definition elt := X.t. + Definition elt_eq := X.eq. + Definition t (A: Set) := X.t -> A. + Definition init (A: Set) (v: A) := fun (_: X.t) => v. + Definition get (A: Set) (x: X.t) (m: t A) := m x. + Definition set (A: Set) (x: X.t) (v: A) (m: t A) := + fun (y: X.t) => if X.eq y x then v else m y. + Lemma gi: + forall (A: Set) (i: elt) (x: A), init x i = x. + Proof. + intros. reflexivity. + Qed. + Lemma gss: + forall (A: Set) (i: elt) (x: A) (m: t A), (set i x m) i = x. + Proof. + intros. unfold set. case (X.eq i i); intro. + reflexivity. tauto. + Qed. + Lemma gso: + forall (A: Set) (i j: elt) (x: A) (m: t A), + i <> j -> (set j x m) i = m i. + Proof. + intros. unfold set. case (X.eq i j); intro. + congruence. reflexivity. + Qed. + Lemma gsspec: + forall (A: Set) (i j: elt) (x: A) (m: t A), + get i (set j x m) = if elt_eq i j then x else get i m. + Proof. + intros. unfold get, set, elt_eq. reflexivity. + Qed. + Lemma gsident: + forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m. + Proof. + intros. unfold get, set. case (X.eq j i); intro. + congruence. reflexivity. + Qed. + Definition map (A B: Set) (f: A -> B) (m: t A) := + fun (x: X.t) => f(m x). + Lemma gmap: + forall (A B: Set) (f: A -> B) (i: elt) (m: t A), + get i (map f m) = f(get i m). + Proof. + intros. unfold get, map. reflexivity. + Qed. + Lemma exten: + forall (A: Set) (m1 m2: t A), + (forall x: X.t, m1 x = m2 x) -> m1 = m2. + Proof. + intros. unfold t. apply extensionality. assumption. + Qed. +End EMap. + +(** * Useful notations *) + +Notation "a ! b" := (PTree.get b a) (at level 1). +Notation "a !! b" := (PMap.get b a) (at level 1). + +(* $Id: Maps.v,v 1.12.4.4 2006/01/07 11:46:55 xleroy Exp $ *) diff --git a/lib/Ordered.v b/lib/Ordered.v new file mode 100644 index 00000000..1747bbb9 --- /dev/null +++ b/lib/Ordered.v @@ -0,0 +1,156 @@ +(** Constructions of ordered types, for use with the [FSet] functors + for finite sets. *) + +Require Import FSet. +Require Import Coqlib. +Require Import Maps. + +(** The ordered type of positive numbers *) + +Module OrderedPositive <: OrderedType. + +Definition t := positive. +Definition eq (x y: t) := x = y. +Definition lt := Plt. + +Lemma eq_refl : forall x : t, eq x x. +Proof (@refl_equal t). +Lemma eq_sym : forall x y : t, eq x y -> eq y x. +Proof (@sym_equal t). +Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. +Proof (@trans_equal t). +Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. +Proof Plt_trans. +Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. +Proof Plt_ne. +Lemma compare : forall x y : t, Compare lt eq x y. +Proof. + intros. case (plt x y); intro. + apply Lt. auto. + case (peq x y); intro. + apply Eq. auto. + apply Gt. red; unfold Plt in *. + assert (Zpos x <> Zpos y). congruence. omega. +Qed. + +End OrderedPositive. + +(** Indexed types (those that inject into [positive]) are ordered. *) + +Module OrderedIndexed(A: INDEXED_TYPE) <: OrderedType. + +Definition t := A.t. +Definition eq (x y: t) := x = y. +Definition lt (x y: t) := Plt (A.index x) (A.index y). + +Lemma eq_refl : forall x : t, eq x x. +Proof (@refl_equal t). +Lemma eq_sym : forall x y : t, eq x y -> eq y x. +Proof (@sym_equal t). +Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. +Proof (@trans_equal t). + +Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. +Proof. + unfold lt; intros. eapply Plt_trans; eauto. +Qed. + +Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. +Proof. + unfold lt; unfold eq; intros. + red; intro. subst y. apply Plt_strict with (A.index x). auto. +Qed. + +Lemma compare : forall x y : t, Compare lt eq x y. +Proof. + intros. case (OrderedPositive.compare (A.index x) (A.index y)); intro. + apply Lt. exact l. + apply Eq. red; red in e. apply A.index_inj; auto. + apply Gt. exact l. +Qed. + +End OrderedIndexed. + +(** The product of two ordered types is ordered. *) + +Module OrderedPair (A B: OrderedType) <: OrderedType. + +Definition t := (A.t * B.t)%type. + +Definition eq (x y: t) := + A.eq (fst x) (fst y) /\ B.eq (snd x) (snd y). + +Lemma eq_refl : forall x : t, eq x x. +Proof. + intros; split; auto. +Qed. + +Lemma eq_sym : forall x y : t, eq x y -> eq y x. +Proof. + unfold eq; intros. intuition auto. +Qed. + +Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. +Proof. + unfold eq; intros. intuition eauto. +Qed. + +Definition lt (x y: t) := + A.lt (fst x) (fst y) \/ + (A.eq (fst x) (fst y) /\ B.lt (snd x) (snd y)). + +Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. +Proof. + unfold lt; intros. + elim H; elim H0; intros. + + left. apply A.lt_trans with (fst y); auto. + + left. elim H1; intros. + case (A.compare (fst x) (fst z)); intro. + assumption. + generalize (A.lt_not_eq H2); intro. elim H5. + apply A.eq_trans with (fst z). auto. auto. + generalize (@A.lt_not_eq (fst z) (fst y)); intro. + elim H5. apply A.lt_trans with (fst x); auto. + apply A.eq_sym; auto. + + left. elim H2; intros. + case (A.compare (fst x) (fst z)); intro. + assumption. + generalize (A.lt_not_eq H1); intro. elim H5. + apply A.eq_trans with (fst x). + apply A.eq_sym. auto. auto. + generalize (@A.lt_not_eq (fst y) (fst x)); intro. + elim H5. apply A.lt_trans with (fst z); auto. + apply A.eq_sym; auto. + + right. elim H1; elim H2; intros. + split. apply A.eq_trans with (fst y); auto. + apply B.lt_trans with (snd y); auto. +Qed. + +Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. +Proof. + unfold lt, eq, not; intros. + elim H0; intros. + elim H; intro. + apply (@A.lt_not_eq _ _ H3 H1). + elim H3; intros. + apply (@B.lt_not_eq _ _ H5 H2). +Qed. + +Lemma compare : forall x y : t, Compare lt eq x y. +Proof. + intros. + case (A.compare (fst x) (fst y)); intro. + apply Lt. red. left. auto. + case (B.compare (snd x) (snd y)); intro. + apply Lt. red. right. tauto. + apply Eq. red. tauto. + apply Gt. red. right. split. apply A.eq_sym. auto. auto. + apply Gt. red. left. auto. +Qed. + +End OrderedPair. + diff --git a/lib/Sets.v b/lib/Sets.v new file mode 100644 index 00000000..bfc49b11 --- /dev/null +++ b/lib/Sets.v @@ -0,0 +1,190 @@ +(** Finite sets. This module implements finite sets over any type + that is equipped with a tree (partial finite mapping) structure. + The set structure forms a semi-lattice, ordered by set inclusion. + + It would have been better to use the [FSet] library, which provides + sets over any totally ordered type. However, there are technical + mismatches between the [FSet] export signature and our signature for + semi-lattices. For now, we keep this somewhat redundant + implementation of sets. +*) + +Require Import Relations. +Require Import Coqlib. +Require Import Maps. +Require Import Lattice. + +Set Implicit Arguments. + +Module MakeSet (P: TREE) <: SEMILATTICE. + +(** Sets of elements of type [P.elt] are implemented as a partial mapping + from [P.elt] to the one-element type [unit]. *) + + Definition elt := P.elt. + + Definition t := P.t unit. + + Lemma eq: forall (a b: t), {a=b} + {a<>b}. + Proof. + unfold t; intros. apply P.eq. + intros. left. destruct x; destruct y; auto. + Qed. + + Definition empty := P.empty unit. + + Definition mem (r: elt) (s: t) := + match P.get r s with None => false | Some _ => true end. + + Definition add (r: elt) (s: t) := P.set r tt s. + + Definition remove (r: elt) (s: t) := P.remove r s. + + Definition union (s1 s2: t) := + P.combine + (fun e1 e2 => + match e1, e2 with + | None, None => None + | _, _ => Some tt + end) + s1 s2. + + Lemma mem_empty: + forall r, mem r empty = false. + Proof. + intro; unfold mem, empty. rewrite P.gempty. auto. + Qed. + + Lemma mem_add_same: + forall r s, mem r (add r s) = true. + Proof. + intros; unfold mem, add. rewrite P.gss. auto. + Qed. + + Lemma mem_add_other: + forall r r' s, r <> r' -> mem r' (add r s) = mem r' s. + Proof. + intros; unfold mem, add. rewrite P.gso; auto. + Qed. + + Lemma mem_remove_same: + forall r s, mem r (remove r s) = false. + Proof. + intros; unfold mem, remove. rewrite P.grs; auto. + Qed. + + Lemma mem_remove_other: + forall r r' s, r <> r' -> mem r' (remove r s) = mem r' s. + Proof. + intros; unfold mem, remove. rewrite P.gro; auto. + Qed. + + Lemma mem_union: + forall r s1 s2, mem r (union s1 s2) = (mem r s1 || mem r s2). + Proof. + intros; unfold union, mem. rewrite P.gcombine. + case (P.get r s1); case (P.get r s2); auto. + auto. + Qed. + + Definition elements (s: t) := + List.map (@fst elt unit) (P.elements s). + + Lemma elements_correct: + forall r s, mem r s = true -> In r (elements s). + Proof. + intros until s. unfold mem, elements. caseEq (P.get r s). + intros. change r with (fst (r, u)). apply in_map. + apply P.elements_correct. auto. + intros; discriminate. + Qed. + + Lemma elements_complete: + forall r s, In r (elements s) -> mem r s = true. + Proof. + unfold mem, elements. intros. + generalize (list_in_map_inv _ _ _ H). + intros [p [EQ IN]]. + destruct p. simpl in EQ. subst r. + rewrite (P.elements_complete _ _ _ IN). auto. + Qed. + + Definition fold (A: Set) (f: A -> elt -> A) (s: t) (x: A) := + P.fold (fun (x: A) (r: elt) (z: unit) => f x r) s x. + + Lemma fold_spec: + forall (A: Set) (f: A -> elt -> A) (s: t) (x: A), + fold f s x = List.fold_left f (elements s) x. + Proof. + intros. unfold fold. rewrite P.fold_spec. + unfold elements. generalize x; generalize (P.elements s). + induction l; simpl; auto. + Qed. + + Definition for_all (f: elt -> bool) (s: t) := + fold (fun b x => andb b (f x)) s true. + + Lemma for_all_spec: + forall f s x, + for_all f s = true -> mem x s = true -> f x = true. + Proof. + intros until x. unfold for_all. rewrite fold_spec. + assert (forall l b0, + fold_left (fun (b : bool) (x : elt) => b && f x) l b0 = true -> + b0 = true). + induction l; simpl; intros. + auto. + generalize (IHl _ H). intro. + elim (andb_prop _ _ H0); intros. auto. + assert (forall l, + fold_left (fun (b : bool) (x : elt) => b && f x) l true = true -> + In x l -> f x = true). + induction l; simpl; intros. + elim H1. + generalize (H _ _ H0); intro. + elim H1; intros. + subst x. auto. + apply IHl. rewrite H2 in H0; auto. auto. + intros. eapply H0; eauto. + apply elements_correct. auto. + Qed. + + Definition ge (s1 s2: t) : Prop := + forall r, mem r s2 = true -> mem r s1 = true. + + Lemma ge_refl: forall x, ge x x. + Proof. + unfold ge; intros. auto. + Qed. + + Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Proof. + unfold ge; intros. auto. + Qed. + + Definition bot := empty. + Definition lub := union. + + Lemma ge_bot: forall (x:t), ge x bot. + Proof. + unfold ge; intros. rewrite mem_empty in H. discriminate. + Qed. + + Lemma lub_commut: forall (x y: t), lub x y = lub y x. + Proof. + intros. unfold lub; unfold union. apply P.combine_commut. + intros; case i; case j; auto. + Qed. + + Lemma ge_lub_left: forall (x y: t), ge (lub x y) x. + Proof. + unfold ge, lub; intros. + rewrite mem_union. rewrite H. reflexivity. + Qed. + + Lemma ge_lub_right: forall (x y: t), ge (lub x y) y. + Proof. + intros. rewrite lub_commut. apply ge_lub_left. + Qed. + +End MakeSet. diff --git a/lib/union_find.v b/lib/union_find.v new file mode 100644 index 00000000..61817d76 --- /dev/null +++ b/lib/union_find.v @@ -0,0 +1,537 @@ +(** A purely functional union-find algorithm *) + +Require Import Wf. + +(** The ``union-find'' algorithm is used to represent equivalence classes + over a given type. It maintains a data structure representing a partition + of the type into equivalence classes. Three operations are provided: +- [empty], which returns the finest partition: each element of the type + is equivalent to itself only. +- [repr part x] returns a canonical representative for the equivalence + class of element [x] in partition [part]. Two elements [x] and [y] + are in the same equivalence class if and only if + [repr part x = repr part y]. +- [identify part x y] returns a new partition where the equivalence + classes of [x] and [y] are merged, and all equivalences valid in [part] + are still valid. + + The partitions are represented by partial mappings from elements + to elements. If [part] maps [x] to [y], this means that [x] and [y] + are in the same equivalence class. The canonical representative + of the class of [x] is obtained by iteratively following these mappings + until an element not mapped to anything is reached; this element is the + canonical representative, as returned by [repr]. + + In algorithm textbooks, the mapping is maintained imperatively by + storing pointers within elements. Here, we give a purely functional + presentation where the mapping is a separate functional data structure. +*) + +Ltac CaseEq name := + generalize (refl_equal name); pattern name at -1 in |- *; case name. + +Ltac IntroElim := + match goal with + | |- (forall id : exists x : _, _, _) => + intro id; elim id; clear id; IntroElim + | |- (forall id : _ /\ _, _) => intro id; elim id; clear id; IntroElim + | |- (forall id : _ \/ _, _) => intro id; elim id; clear id; IntroElim + | |- (_ -> _) => intro; IntroElim + | _ => idtac + end. + +Ltac MyElim n := elim n; IntroElim. + +(** The elements of equivalence classes are represented by the following + signature: a type with a decidable equality. *) + +Module Type ELEMENT. + Variable T: Set. + Variable eq: forall (a b: T), {a = b} + {a <> b}. +End ELEMENT. + +(** The mapping structure over elements is represented by the following + signature. *) + +Module Type MAP. + Variable elt: Set. + Variable T: Set. + Variable empty: T. + Variable get: elt -> T -> option elt. + Variable add: elt -> elt -> T -> T. + + Hypothesis get_empty: forall (x: elt), get x empty = None. + Hypothesis get_add_1: + forall (x y: elt) (m: T), get x (add x y m) = Some y. + Hypothesis get_add_2: + forall (x y z: elt) (m: T), z <> x -> get z (add x y m) = get z m. +End MAP. + +(** Our implementation of union-find is a functor, parameterized by + a structure for elements and a structure for maps. It returns a + module with the following structure. *) + +Module Type UNIONFIND. + Variable elt: Set. + (** The type of partitions. *) + Variable T: Set. + + (** The operations over partitions. *) + Variable empty: T. + Variable repr: T -> elt -> elt. + Variable identify: T -> elt -> elt -> T. + + (** The relation implied by the partition [m]. *) + Definition sameclass (m: T) (x y: elt) : Prop := repr m x = repr m y. + + (* [sameclass] is an equivalence relation *) + Hypothesis sameclass_refl: + forall (m: T) (x: elt), sameclass m x x. + Hypothesis sameclass_sym: + forall (m: T) (x y: elt), sameclass m x y -> sameclass m y x. + Hypothesis sameclass_trans: + forall (m: T) (x y z: elt), + sameclass m x y -> sameclass m y z -> sameclass m x z. + + (* [repr m x] is a canonical representative of the equivalence class + of [x] in partition [m]. *) + Hypothesis repr_repr: + forall (m: T) (x: elt), repr m (repr m x) = repr m x. + Hypothesis sameclass_repr: + forall (m: T) (x: elt), sameclass m x (repr m x). + + (* [empty] is the finest partition *) + Hypothesis repr_empty: + forall (x: elt), repr empty x = x. + Hypothesis sameclass_empty: + forall (x y: elt), sameclass empty x y -> x = y. + + (* [identify] preserves existing equivalences and adds an equivalence + between the two elements provided. *) + Hypothesis sameclass_identify_1: + forall (m: T) (x y: elt), sameclass (identify m x y) x y. + Hypothesis sameclass_identify_2: + forall (m: T) (x y u v: elt), + sameclass m u v -> sameclass (identify m x y) u v. + +End UNIONFIND. + +(** Implementation of the union-find algorithm. *) + +Module Unionfind (E: ELEMENT) (M: MAP with Definition elt := E.T) + <: UNIONFIND with Definition elt := E.T. + +Definition elt := E.T. + +(* A set of equivalence classes over [elt] is represented by a map [m]. +- [M.get a m = Some a'] means that [a] is in the same class as [a']. +- [M.get a m = None] means that [a] is the canonical representative + for its equivalence class. +*) + +(** Such a map induces an ordering over type [elt]: + [repr_order m a a'] if and only if [M.get a' m = Some a]. + This ordering must be well founded (no cycles). *) + +Definition repr_order (m: M.T) (a a': elt) : Prop := + M.get a' m = Some a. + +(** The canonical representative of an element. + Needs Noetherian recursion. *) + +Lemma option_sum: + forall (x: option elt), {y: elt | x = Some y} + {x = None}. +Proof. + intro x. case x. + left. exists e. auto. + right. auto. +Qed. + +Definition repr_rec + (m: M.T) (a: elt) (rec: forall b: elt, repr_order m b a -> elt) := + match option_sum (M.get a m) with + | inleft (exist b P) => rec b P + | inright _ => a + end. + +Definition repr_aux + (m: M.T) (wf: well_founded (repr_order m)) (a: elt) : elt := + Fix wf (fun (_: elt) => elt) (repr_rec m) a. + +Lemma repr_rec_ext: + forall (m: M.T) (x: elt) (f g: forall y:elt, repr_order m y x -> elt), + (forall (y: elt) (p: repr_order m y x), f y p = g y p) -> + repr_rec m x f = repr_rec m x g. +Proof. + intros. unfold repr_rec. + case (option_sum (M.get x m)). + intros. elim s; intros. apply H. + intros. auto. +Qed. + +Lemma repr_aux_none: + forall (m: M.T) (wf: well_founded (repr_order m)) (a: elt), + M.get a m = None -> + repr_aux m wf a = a. +Proof. + intros. + generalize (Fix_eq wf (fun (_:elt) => elt) (repr_rec m) (repr_rec_ext m) a). + intro. unfold repr_aux. rewrite H0. + unfold repr_rec. + case (option_sum (M.get a m)). + intro s; elim s; intros. + rewrite H in p; discriminate. + intros. auto. +Qed. + +Lemma repr_aux_some: + forall (m: M.T) (wf: well_founded (repr_order m)) (a a': elt), + M.get a m = Some a' -> + repr_aux m wf a = repr_aux m wf a'. +Proof. + intros. + generalize (Fix_eq wf (fun (_:elt) => elt) (repr_rec m) (repr_rec_ext m) a). + intro. unfold repr_aux. rewrite H0. unfold repr_rec. + case (option_sum (M.get a m)). + intro s; elim s; intros. + rewrite H in p. injection p; intros. rewrite H1. auto. + intros. rewrite H in e. discriminate. +Qed. + +Lemma repr_aux_canon: + forall (m: M.T) (wf: well_founded (repr_order m)) (a: elt), + M.get (repr_aux m wf a) m = None. +Proof. + intros. + apply (well_founded_ind wf (fun (a: elt) => M.get (repr_aux m wf a) m = None)). + intros. + generalize (Fix_eq wf (fun (_:elt) => elt) (repr_rec m) (repr_rec_ext m) x). + intro. unfold repr_aux. rewrite H0. + unfold repr_rec. + case (option_sum (M.get x m)). + intro s; elim s; intros. + unfold repr_aux in H. apply H. + unfold repr_order. auto. + intro. auto. +Qed. + +(** The empty partition (each element in its own class) is well founded. *) + +Lemma wf_empty: + well_founded (repr_order M.empty). +Proof. + red. intro. apply Acc_intro. + intros b RO. + red in RO. + rewrite M.get_empty in RO. + discriminate. +Qed. + +(** Merging two equivalence classes. *) + +Section IDENTIFY. + +Variable m: M.T. +Hypothesis mwf: well_founded (repr_order m). +Variable a b: elt. +Hypothesis a_diff_b: a <> b. +Hypothesis a_canon: M.get a m = None. +Hypothesis b_canon: M.get b m = None. + +(** Identifying two distinct canonical representatives [a] and [b] + is achieved by mapping one to the other. *) + +Definition identify_base: M.T := M.add a b m. + +Lemma identify_base_b_canon: + M.get b identify_base = None. +Proof. + unfold identify_base. + rewrite M.get_add_2. + auto. + apply sym_not_eq. auto. +Qed. + +Lemma identify_base_a_maps_to_b: + M.get a identify_base = Some b. +Proof. + unfold identify_base. rewrite M.get_add_1. auto. +Qed. + +Lemma identify_base_repr_order: + forall (x y: elt), + repr_order identify_base x y -> + repr_order m x y \/ (y = a /\ x = b). +Proof. + intros x y. unfold identify_base. + unfold repr_order. + case (E.eq a y); intro. + rewrite e. rewrite M.get_add_1. + intro. injection H. intro. rewrite H0. tauto. + rewrite M.get_add_2; auto. +Qed. + +(** [identify_base] preserves well foundation. *) + +Lemma identify_base_order_wf: + well_founded (repr_order identify_base). +Proof. + red. + cut (forall (x: elt), Acc (repr_order m) x -> Acc (repr_order identify_base) x). + intro CUT. intro x. apply CUT. apply mwf. + + induction 1. + apply Acc_intro. intros. + MyElim (identify_base_repr_order y x H1). + apply H0; auto. + rewrite H3. + apply Acc_intro. + intros z H4. + red in H4. rewrite identify_base_b_canon in H4. discriminate. +Qed. + +Lemma identify_aux_decomp: + forall (x: elt), + (M.get x m = None /\ M.get x identify_base = None) + \/ (x = a /\ M.get x m = None /\ M.get x identify_base = Some b) + \/ (exists y, M.get x m = Some y /\ M.get x identify_base = Some y). +Proof. + intro x. + unfold identify_base. + case (E.eq a x); intro. + rewrite <- e. rewrite M.get_add_1. + tauto. + rewrite M.get_add_2; auto. + case (M.get x m); intros. + right; right; exists e; tauto. + tauto. +Qed. + +Lemma identify_base_repr: + forall (x: elt), + repr_aux identify_base identify_base_order_wf x = + (if E.eq (repr_aux m mwf x) a then b else repr_aux m mwf x). +Proof. + intro x0. + apply (well_founded_ind mwf + (fun (x: elt) => + repr_aux identify_base identify_base_order_wf x = + (if E.eq (repr_aux m mwf x) a then b else repr_aux m mwf x))); + intros. + MyElim (identify_aux_decomp x). + + rewrite (repr_aux_none identify_base). + rewrite (repr_aux_none m mwf x). + case (E.eq x a); intro. + subst x. + rewrite identify_base_a_maps_to_b in H1. + discriminate. + auto. auto. auto. + + subst x. rewrite (repr_aux_none m mwf a); auto. + case (E.eq a a); intro. + rewrite (repr_aux_some identify_base identify_base_order_wf a b). + rewrite (repr_aux_none identify_base identify_base_order_wf b). + auto. apply identify_base_b_canon. auto. + tauto. + + rewrite (repr_aux_some identify_base identify_base_order_wf x x1); auto. + rewrite (repr_aux_some m mwf x x1); auto. +Qed. + +Lemma identify_base_sameclass_1: + forall (x y: elt), + repr_aux m mwf x = repr_aux m mwf y -> + repr_aux identify_base identify_base_order_wf x = + repr_aux identify_base identify_base_order_wf y. +Proof. + intros. + rewrite identify_base_repr. + rewrite identify_base_repr. + rewrite H. + auto. +Qed. + +Lemma identify_base_sameclass_2: + forall (x y: elt), + repr_aux m mwf x = a -> + repr_aux m mwf y = b -> + repr_aux identify_base identify_base_order_wf x = + repr_aux identify_base identify_base_order_wf y. +Proof. + intros. + rewrite identify_base_repr. + rewrite identify_base_repr. + rewrite H. + case (E.eq a a); intro. + case (E.eq (repr_aux m mwf y) a); auto. + tauto. +Qed. + +End IDENTIFY. + +(** The union-find data structure is a record encapsulating a mapping + and a proof of well foundation. *) + +Record unionfind : Set := mkunionfind + { map: M.T; wf: well_founded (repr_order map) }. + +Definition T := unionfind. + +Definition repr (uf: unionfind) (a: elt) : elt := + repr_aux (map uf) (wf uf) a. + +Lemma repr_repr: + forall (uf: unionfind) (a: elt), repr uf (repr uf a) = repr uf a. +Proof. + intros. + unfold repr. + rewrite (repr_aux_none (map uf) (wf uf) (repr_aux (map uf) (wf uf) a)). + auto. + apply repr_aux_canon. +Qed. + +Definition empty := mkunionfind M.empty wf_empty. + +(** [identify] computes canonical representatives for the two elements + and adds a mapping from one to the other, unless they are already + equal. *) + +Definition identify (uf: unionfind) (a b: elt) : unionfind := + match E.eq (repr uf a) (repr uf b) with + | left EQ => + uf + | right NOTEQ => + mkunionfind + (identify_base (map uf) (repr uf a) (repr uf b)) + (identify_base_order_wf (map uf) (wf uf) + (repr uf a) (repr uf b) + NOTEQ + (repr_aux_canon (map uf) (wf uf) b)) + end. + +Definition sameclass (uf: unionfind) (a b: elt) : Prop := + repr uf a = repr uf b. + +Lemma sameclass_refl: + forall (uf: unionfind) (a: elt), sameclass uf a a. +Proof. + intros. red. auto. +Qed. + +Lemma sameclass_sym: + forall (uf: unionfind) (a b: elt), sameclass uf a b -> sameclass uf b a. +Proof. + intros. red. symmetry. exact H. +Qed. + +Lemma sameclass_trans: + forall (uf: unionfind) (a b c: elt), + sameclass uf a b -> sameclass uf b c -> sameclass uf a c. +Proof. + intros. red. transitivity (repr uf b). exact H. exact H0. +Qed. + +Lemma sameclass_repr: + forall (uf: unionfind) (a: elt), sameclass uf a (repr uf a). +Proof. + intros. red. symmetry. rewrite repr_repr. auto. +Qed. + +Lemma repr_empty: + forall (a: elt), repr empty a = a. +Proof. + intro a. unfold repr; unfold empty. + simpl. + apply repr_aux_none. + apply M.get_empty. +Qed. + +Lemma sameclass_empty: + forall (a b: elt), sameclass empty a b -> a = b. +Proof. + intros. red in H. rewrite repr_empty in H. + rewrite repr_empty in H. auto. +Qed. + +Lemma sameclass_identify_2: + forall (uf: unionfind) (a b x y: elt), + sameclass uf x y -> sameclass (identify uf a b) x y. +Proof. + intros. + unfold identify. + case (E.eq (repr uf a) (repr uf b)). + intro. auto. + intros; red; unfold repr; simpl. + apply identify_base_sameclass_1. + apply repr_aux_canon. + exact H. +Qed. + +Lemma sameclass_identify_1: + forall (uf: unionfind) (a b: elt), + sameclass (identify uf a b) a b. +Proof. + intros. + unfold identify. + case (E.eq (repr uf a) (repr uf b)). + intro. auto. + intros. + red; unfold repr; simpl. + apply identify_base_sameclass_2. + apply repr_aux_canon. + auto. + auto. +Qed. + +End Unionfind. + +(* Example of use 1: with association lists *) + +(* + +Require Import List. + +Module AListMap(E: ELEMENT) : MAP. + +Definition elt := E.T. +Definition T := list (elt * elt). +Definition empty : T := nil. +Fixpoint get (x: elt) (m: T) {struct m} : option elt := + match m with + | nil => None + | (a,b) :: t => + match E.eq x a with + | left _ => Some b + | right _ => get x t + end + end. +Definition add (x y: elt) (m: T) := (x,y) :: m. + +Lemma get_empty: forall (x: elt), get x empty = None. +Proof. + intro. unfold empty. simpl. auto. +Qed. + +Lemma get_add_1: + forall (x y: elt) (m: T), get x (add x y m) = Some y. +Proof. + intros. unfold add. simpl. + case (E.eq x x); intro. + auto. + tauto. +Qed. + +Lemma get_add_2: + forall (x y z: elt) (m: T), z <> x -> get z (add x y m) = get z m. +Proof. + intros. unfold add. simpl. + case (E.eq z x); intro. + subst z; tauto. + auto. +Qed. + +End AListMap. + +*) + |