Require Import base. Require Import sepalg. Require Import boolean_alg. (** This module implements a share model via binary trees with boolean-labeled leaves. The development is complicated somewhat by the fact the ordering used defines multiple isomorphic representations of a share. We must therefore chose one to be a canonical representation of the equivalence class in order to get strong antisymmetry (i.e., antisymmetry up to identity). The canonical tree is the one that contains no nonleaf full or empty subtrees. A full subtree has all leaves labeled with true, whereas an empty subtree has all leaves labeled with false. Canonical trees always exists and are unique. Furthermore, they can be straightforwardly calculated. Tree union and intersection may generate noncanonical trees, so the result must be canonicalized. However, split always generates canonical trees when given a canonical tree, as does complement. **) Module TreeLattice : SHARE_MODEL. (* Definition of the trees and operations on them *) Inductive ShareTree : Set := | Leaf : bool -> ShareTree | Node : ShareTree -> ShareTree -> ShareTree . Fixpoint nonFullTree (x:ShareTree) : Prop := match x with | Leaf b => b = false | Node l r => nonFullTree l \/ nonFullTree r end. Fixpoint nonEmptyTree (x:ShareTree) : Prop := match x with | Leaf b => b = true | Node l r => nonEmptyTree l \/ nonEmptyTree r end. Fixpoint canonicalTree (x:ShareTree) : Prop := match x with | Leaf _ => True | Node l r => nonFullTree x /\ nonEmptyTree x /\ canonicalTree l /\ canonicalTree r end. Fixpoint union_tree (x y:ShareTree) { struct x } : ShareTree := match x with | Leaf true => Leaf true | Leaf false => y | Node l1 r1 => match y with | Leaf true => Leaf true | Leaf false => x | Node l2 r2 => Node (union_tree l1 l2) (union_tree r1 r2) end end. Fixpoint intersect_tree (x y:ShareTree) { struct x } : ShareTree := match x with | Leaf false => Leaf false | Leaf true => y | Node l1 r1 => match y with | Leaf false => Leaf false | Leaf true => x | Node l2 r2 => Node (intersect_tree l1 l2) (intersect_tree r1 r2) end end. Fixpoint comp_tree (x:ShareTree) : ShareTree := match x with | Leaf b => Leaf (negb b) | Node l r => Node (comp_tree l) (comp_tree r) end. Fixpoint mkCanon (x:ShareTree) : ShareTree := match x with | Leaf b => Leaf b | Node l r => let l' := mkCanon l in let r' := mkCanon r in match l', r' with | Leaf b1, Leaf b2 => if bool_dec b1 b2 then Leaf b1 else Node l' r' | _, _ => Node l' r' end end. Fixpoint relativ_tree (z a:ShareTree) {struct z} : ShareTree := match z with | Leaf true => a | Leaf false => Leaf false | Node l r => Node (relativ_tree l a) (relativ_tree r a) end. (* The ordering relation on trees, and its induced isomorphism. *) Inductive shareTreeOrd : ShareTree -> ShareTree -> Prop := | Leaf_Ord : forall b1 b2, implb b1 b2 = true -> shareTreeOrd (Leaf b1) (Leaf b2) | LeafNode_Ord : forall b l r, shareTreeOrd (Node (Leaf b) (Leaf b)) (Node l r) -> shareTreeOrd (Leaf b) (Node l r) | NodeLeaf_Ord : forall b l r, shareTreeOrd (Node l r) (Node (Leaf b) (Leaf b)) -> shareTreeOrd (Node l r) (Leaf b) | Node_Ord : forall l1 l2 r1 r2, shareTreeOrd l1 l2 -> shareTreeOrd r1 r2 -> shareTreeOrd (Node l1 r1) (Node l2 r2) . Hint Constructors shareTreeOrd. Definition shareTreeEq (x y:ShareTree) := shareTreeOrd x y /\ shareTreeOrd y x. Hint Unfold shareTreeEq. Ltac destruct_bool := repeat (match goal with [ b:bool |- _ ] => destruct b end). Ltac invert_ord := repeat ( match goal with | [ H:shareTreeEq _ _ |- _ ] => destruct H | [ H:shareTreeOrd (Leaf _) (Leaf _) |- _ ] => inversion H; clear H | [ H:shareTreeOrd (Leaf _) (Node _ _) |- _ ] => inversion H; clear H | [ H:shareTreeOrd (Node _ _) (Leaf _) |- _ ] => inversion H; clear H | [ H:shareTreeOrd (Node _ _) (Node _ _) |- _ ] => inversion H; clear H end; subst). (* Utility lemmas about full and empty trees, and the top and bottom elements. *) Lemma nonEmpty_dec : forall x, {nonEmptyTree x}+{~nonEmptyTree x}. Proof. induction x; simpl; intros; invert_ord; destruct_bool; intuition. Qed. Lemma nonFull_dec : forall x, {nonFullTree x}+{~nonFullTree x}. Proof. induction x; simpl; intros; invert_ord; destruct_bool; intuition. Qed. Lemma geTrueFull : forall x, shareTreeOrd (Leaf true) x -> ~nonFullTree x. Proof. induction x; simpl; intros; invert_ord; destruct_bool; intuition. Qed. Lemma leFalseEmpty : forall x, shareTreeOrd x (Leaf false) -> ~nonEmptyTree x. Proof. induction x; simpl; intros; invert_ord; destruct_bool; intuition. Qed. Lemma emptyLeFalse : forall x, ~nonEmptyTree x -> shareTreeOrd x (Leaf false). Proof. induction x; simpl; intros; invert_ord; destruct_bool; intuition. Qed. Lemma fullGeTrue : forall x, ~nonFullTree x -> shareTreeOrd (Leaf true) x. Proof. induction x; simpl; intros; invert_ord; destruct_bool; intuition. Qed. Lemma falseLeaf_bottom : forall x, shareTreeOrd (Leaf false) x. Proof. induction x; auto. Qed. Lemma trueLeaf_top : forall x, shareTreeOrd x (Leaf true). Proof. induction x; destruct_bool; auto. Qed. Hint Resolve geTrueFull leFalseEmpty emptyLeFalse fullGeTrue falseLeaf_bottom trueLeaf_top. Lemma eqFalseLeaf_empty : forall x, shareTreeEq (Leaf false) x -> ~nonEmptyTree x. Proof. induction x; simpl; intros; invert_ord; destruct_bool; intuition. Qed. Lemma eqTrueLeaf_full : forall x, shareTreeEq (Leaf true) x -> ~nonFullTree x. Proof. induction x; simpl; intros; invert_ord; destruct_bool; intuition. Qed. Lemma emptyTree_canonical_falseLeaf : forall x, ~nonEmptyTree x -> canonicalTree x -> x = Leaf false. Proof. induction x; simpl; intros; invert_ord; destruct_bool; intuition. Qed. Lemma fullTree_canonical_trueLeaf : forall x, ~nonFullTree x -> canonicalTree x -> x = Leaf true. Proof. induction x; simpl; intros; invert_ord; destruct_bool; intuition. Qed. Hint Resolve eqFalseLeaf_empty eqTrueLeaf_full emptyTree_canonical_falseLeaf fullTree_canonical_trueLeaf. (* Show that shareTreeOrd is a preorder (reflexive and transitive). *) Lemma shareTreeOrd_refl : forall x, shareTreeOrd x x. Proof. induction x; simpl; intros; invert_ord; destruct_bool; intuition. Qed. Lemma shareTreeOrd_trans_leaf : forall x1 b x3, shareTreeOrd x1 (Leaf b) -> shareTreeOrd (Leaf b) x3 -> shareTreeOrd x1 x3. Proof. intro x1; induction x1; simpl; intros; invert_ord; destruct_bool; intuition. inv H0; invert_ord; destruct_bool; intuition eauto. discriminate. inv H0; invert_ord; destruct_bool; intuition eauto. Qed. Lemma shareTreeOrd_trans : forall x1 x2 x3, shareTreeOrd x1 x2 -> shareTreeOrd x2 x3 -> shareTreeOrd x1 x3. Proof. intros x1 x2; revert x1; induction x2; simpl; intros. apply shareTreeOrd_trans_leaf with b; auto. inv H; inv H0; invert_ord; eauto. Qed. (* Show that shareTreeEq is an equivalance relation. *) Lemma shareTreeEq_refl : forall x, shareTreeEq x x. Proof. unfold shareTreeEq; intuition; apply shareTreeOrd_refl. Qed. Lemma shareTreeEq_sym : forall x y, shareTreeEq x y -> shareTreeEq y x. Proof. unfold shareTreeEq; intuition. Qed. Lemma shareTreeEq_trans : forall x y z, shareTreeEq x y -> shareTreeEq y z -> shareTreeEq x z. Proof. unfold shareTreeEq; intuition; apply shareTreeOrd_trans with y; auto. Qed. (* Show that mkCanon generates canonical trees that are equivalant to the original. *) Lemma mkCanon_correct : forall x, canonicalTree (mkCanon x). Proof. induction x; simpl; intros; auto. case_eq (mkCanon x1); intros. case_eq (mkCanon x2); intros. case_eq (bool_dec b b0); intros; simpl; auto. destruct_bool; intuition. elim n; auto. rewrite H0 in IHx2. simpl in *; intuition. rewrite H in IHx1. simpl in *; intuition. Qed. Lemma mkCanon_eq : forall x, shareTreeEq x (mkCanon x). Proof. induction x; simpl; intros; auto. split; apply shareTreeOrd_refl. case_eq (mkCanon x1); intros; rewrite H in IHx1; destruct IHx1; case_eq (mkCanon x2); intros; rewrite H2 in IHx2; destruct IHx2; red. destruct (bool_dec b b0); subst; intuition; repeat econstructor; eauto. split; repeat econstructor; auto. split; repeat econstructor; auto. split; repeat econstructor; auto. Qed. Lemma mkCanon_test : forall x y, mkCanon x = mkCanon y -> shareTreeEq x y. Proof. intros. apply shareTreeEq_trans with (mkCanon x). apply mkCanon_eq. rewrite H. apply shareTreeEq_sym. apply mkCanon_eq. Qed. Lemma mkCanon_nonEmpty : forall x, nonEmptyTree x -> nonEmptyTree (mkCanon x). Proof. induction x; simpl; intros; auto. destruct H; [ apply IHx1 in H | apply IHx2 in H ]; clear IHx1 IHx2. destruct (mkCanon x1); destruct (mkCanon x2); simpl in *; auto. destruct (bool_dec b b0); subst; intuition; repeat econstructor; eauto. destruct (mkCanon x1); destruct (mkCanon x2); simpl in *; auto. destruct (bool_dec b b0); subst; intuition; simpl; auto. Qed. Hint Resolve mkCanon_nonEmpty mkCanon_correct mkCanon_eq. (* Show that union and intersection are the LUB and GLB for the lattice, respectively. *) Lemma union_commute : forall x y, union_tree x y = union_tree y x. Proof. intro x; induction x; destruct y; simpl; intros; auto. destruct b; destruct b0; simpl; auto. rewrite IHx1. rewrite IHx2. auto. Qed. Lemma intersect_commute : forall x y, intersect_tree x y = intersect_tree y x. Proof. intro x; induction x; destruct y; simpl; intros; auto. destruct b; destruct b0; simpl; auto. rewrite IHx1. rewrite IHx2. auto. Qed. Lemma union_upper_bound : forall x y, shareTreeOrd x (union_tree x y). Proof. intro x; induction x; simpl; intros. destruct b. apply trueLeaf_top. apply falseLeaf_bottom. destruct y; simpl. destruct b. apply trueLeaf_top. apply shareTreeOrd_refl. apply Node_Ord; auto. Qed. Lemma intersection_lower_bound: forall x y, shareTreeOrd (intersect_tree x y) x. Proof. intro x; induction x; simpl; intros. destruct b. apply trueLeaf_top. apply falseLeaf_bottom. destruct y; simpl. destruct b. apply shareTreeOrd_refl. apply falseLeaf_bottom. apply Node_Ord; auto. Qed. Lemma union_least_bound : forall x y z, shareTreeOrd x z -> shareTreeOrd y z -> shareTreeOrd (union_tree x y) z. Proof. induction x; simpl; intros; invert_ord; try destruct_bool; auto. destruct y; invert_ord; try destruct_bool; auto. destruct z; invert_ord; try destruct_bool; repeat econstructor; auto. Qed. Lemma intersection_greatest_bound : forall x y z, shareTreeOrd z x -> shareTreeOrd z y -> shareTreeOrd z (intersect_tree x y). Proof. induction x; simpl; intros; invert_ord; destruct_bool; auto. destruct y; invert_ord; try destruct_bool; auto. destruct z; invert_ord; try destruct_bool; repeat econstructor; auto. Qed. (* Now prove a few other utility lemmas about union and intersection. *) Lemma union_idem : forall x, x = union_tree x x. Proof. induction x; simpl; intros. destruct b; simpl; auto. congruence. Qed. Lemma intersect_idem : forall x, x = intersect_tree x x. Proof. induction x; simpl; intros. destruct b; simpl; auto. congruence. Qed. Lemma union_absorb : forall x y, x = union_tree x (intersect_tree x y). Proof. intro x; induction x; simpl; intros. destruct b; auto. destruct y; auto. destruct b; auto. repeat rewrite <- union_idem; auto. rewrite <- IHx1. rewrite <- IHx2. auto. Qed. Lemma intersect_absorb : forall x y, x = intersect_tree x (union_tree x y). Proof. intro x; induction x; simpl; intros. destruct b; auto. destruct y; auto. destruct b; auto. repeat rewrite <- intersect_idem; auto. rewrite <- IHx1. rewrite <- IHx2. auto. Qed. (* Demonstrate that intersection distributes over union and vice-versa. *) Lemma intersect_distrib : forall x y z, intersect_tree x (union_tree y z) = union_tree (intersect_tree x y) (intersect_tree x z). Proof. induction x; simpl; intros; try destruct_bool; simpl; auto. case_eq (union_tree y z); intros. destruct y; destruct z; destruct_bool; simpl in *; try discriminate; auto. repeat rewrite <- union_idem; auto. repeat rewrite <- union_absorb; auto. repeat (rewrite union_commute; rewrite <- union_absorb); auto. destruct y; destruct z; destruct_bool; try discriminate; simpl in *. congruence. congruence. rewrite <- IHx1. rewrite <- IHx2. congruence. Qed. Lemma union_distrib : forall x y z, union_tree x (intersect_tree y z) = intersect_tree (union_tree x y) (union_tree x z). Proof. induction x; simpl; intros; try destruct_bool; simpl; auto. case_eq (intersect_tree y z); intros. destruct y; destruct z; destruct_bool; simpl in *; try discriminate; auto. repeat rewrite <- intersect_idem; auto. repeat rewrite <- intersect_absorb; auto. repeat (rewrite intersect_commute; rewrite <- intersect_absorb); auto. destruct y; destruct z; destruct_bool; try discriminate; simpl in *. congruence. congruence. rewrite <- IHx1. rewrite <- IHx2. congruence. Qed. (* Demonstrate that union and intersection are congruences WRT the shareTreeEq relation. *) Lemma Node_Eq : forall x x' y y', shareTreeEq x x' -> shareTreeEq y y' -> shareTreeEq (Node x y) (Node x' y'). Proof. unfold shareTreeEq; intuition; econstructor; auto. Qed. Lemma intersect_cong0 : forall y x x', shareTreeOrd x x' -> shareTreeOrd (intersect_tree x y) (intersect_tree x' y). Proof. induction y; simpl; intros. rewrite (intersect_commute x (Leaf b)). rewrite (intersect_commute x' (Leaf b)). revert b x' H; induction x; simpl; intros; destruct_bool; solve [ auto | apply falseLeaf_bottom ]. induction H; simpl in *; intros; destruct_bool; simpl in *; try discriminate; solve [ apply shareTreeOrd_refl | apply falseLeaf_bottom | invert_ord; repeat econstructor; auto ]. Qed. Lemma union_cong0 : forall y x x', shareTreeOrd x x' -> shareTreeOrd (union_tree x y) (union_tree x' y). Proof. induction y; simpl; intros. rewrite (union_commute x (Leaf b)). rewrite (union_commute x' (Leaf b)). revert b x' H; induction x; simpl; intros; destruct_bool; solve [ auto | apply trueLeaf_top ]. induction H; simpl in *; intros; destruct_bool; simpl in *; try discriminate; solve [ apply shareTreeOrd_refl | apply trueLeaf_top | invert_ord; repeat econstructor; auto ]. Qed. Lemma intersect_cong1 : forall x x' y, shareTreeEq x x' -> shareTreeEq (intersect_tree x y) (intersect_tree x' y). Proof. unfold shareTreeEq; intuition; apply intersect_cong0; auto. Qed. Lemma union_cong1 : forall x x' y, shareTreeEq x x' -> shareTreeEq (union_tree x y) (union_tree x' y). Proof. unfold shareTreeEq; intuition; apply union_cong0; auto. Qed. Lemma intersect_cong : forall x x' y y', shareTreeEq x x' -> shareTreeEq y y' -> shareTreeEq (intersect_tree x y) (intersect_tree x' y'). Proof. intros. apply shareTreeEq_trans with (intersect_tree x' y). apply intersect_cong1; auto. rewrite (intersect_commute x' y). rewrite (intersect_commute x' y'). apply intersect_cong1; auto. Qed. Lemma union_cong : forall x x' y y', shareTreeEq x x' -> shareTreeEq y y' -> shareTreeEq (union_tree x y) (union_tree x' y'). Proof. intros. apply shareTreeEq_trans with (union_tree x' y). apply union_cong1; auto. rewrite (union_commute x' y). rewrite (union_commute x' y'). apply union_cong1; auto. Qed. Lemma comp_cong0 : forall x x', shareTreeOrd x x' -> shareTreeOrd (comp_tree x') (comp_tree x). Proof. induction x; simpl. induction x'; simpl; intros; invert_ord; destruct_bool; repeat econstructor; solve [ auto ]. simpl; intros. inversion H; clear H; subst; invert_ord; destruct_bool; simpl. apply falseLeaf_bottom. repeat econstructor. apply (IHx1 (Leaf false)); auto. apply (IHx2 (Leaf false)); auto. repeat econstructor. apply IHx1; auto. apply IHx2; auto. Qed. Lemma comp_cong : forall x x', shareTreeEq x x' -> shareTreeEq (comp_tree x') (comp_tree x). Proof. unfold shareTreeEq; intuition; apply comp_cong0; auto. Qed. Lemma tree_comp1 : forall x, shareTreeOrd (Leaf true) (union_tree x (comp_tree x)). Proof. induction x; simpl; intros. destruct b; apply shareTreeOrd_refl. apply LeafNode_Ord; apply Node_Ord; auto. Qed. Lemma tree_comp2 : forall x, shareTreeOrd (intersect_tree x (comp_tree x)) (Leaf false). Proof. induction x; simpl; intros. destruct b; apply shareTreeOrd_refl. apply NodeLeaf_Ord; apply Node_Ord; auto. Qed. (* Show that two isomorphic canonical trees are identical. *) Lemma canonicalUnique : forall c1 c2, shareTreeEq c1 c2 -> canonicalTree c1 -> canonicalTree c2 -> c1 = c2. Proof. intro c1; induction c1; simpl; intros; destruct H. destruct c2; invert_ord; destruct_bool; simpl in *; auto. intuition. elim (geTrueFull c2_1); auto. elim (geTrueFull c2_1); auto. elim (geTrueFull c2_2); auto. elim (geTrueFull c2_2); auto. intuition. elim (leFalseEmpty c2_1); auto. elim (leFalseEmpty c2_2); auto. elim (leFalseEmpty c2_1); auto. elim (leFalseEmpty c2_2); auto. destruct c2; invert_ord; destruct_bool; simpl in *; auto. replace c2_1 with c1_1. replace c2_2 with c1_2; auto. intuition. intuition. Qed. Lemma mkCanon_test2 : forall x y, shareTreeEq x y -> mkCanon x = mkCanon y. Proof. intros; apply canonicalUnique; auto. apply shareTreeEq_trans with x; auto. apply shareTreeEq_sym; auto. apply shareTreeEq_trans with y; auto. Qed. (* Some basic facts about the relativization operation: It is injective when a is nonempty; a number of facts about nonemptyness, nonfullness and canonical trees; it commutes with union, intersection, mkCanon; and it is an associative operation. *) Lemma relativ_inv : forall a x y, nonEmptyTree a -> shareTreeOrd (relativ_tree a x) (relativ_tree a y) -> shareTreeOrd x y. Proof. induction a; simpl; intros. destruct b; auto. invert_ord; auto; try discriminate. invert_ord; destruct H; auto. Qed. Lemma relativ_empty : forall a x, nonEmptyTree a -> nonEmptyTree x -> nonEmptyTree (relativ_tree a x). Proof. induction a; simpl; intros; destruct_bool; try discriminate; intuition. Qed. Lemma relativ_empty1 : forall a x, nonEmptyTree (relativ_tree a x) -> nonEmptyTree a. Proof. induction a; simpl; intros; auto. destruct b; try discriminate; auto. intuition; eauto. Qed. Lemma relativ_empty2 : forall a x, nonEmptyTree (relativ_tree a x) -> nonEmptyTree x. Proof. induction a; simpl; intros; auto. destruct b; simpl in *; auto. discriminate. intuition; eauto. Qed. Lemma relativ_full1 : forall a x, nonFullTree a -> nonFullTree (relativ_tree a x). Proof. induction a; simpl; intros; destruct_bool; try discriminate; intuition. Qed. Lemma relativ_full2 : forall a x, nonFullTree x -> nonFullTree (relativ_tree a x). Proof. induction a; simpl; intros; destruct_bool; try discriminate; simpl; intuition. Qed. Lemma relativ_full : forall a, relativ_tree a (Leaf true) = a. Proof. induction a; simpl; intros; auto. destruct b; auto. rewrite IHa1; rewrite IHa2; auto. Qed. Hint Resolve relativ_empty relativ_empty1 relativ_empty2 relativ_full relativ_full1 relativ_full2 relativ_inv. Lemma relativ_almost_canon : forall a x, canonicalTree a -> canonicalTree x -> nonEmptyTree x -> canonicalTree (relativ_tree a x). Proof. induction a; simpl; intros; destruct_bool; auto. intuition auto. Qed. Lemma relativ_cong : forall a x y, shareTreeOrd x y -> shareTreeOrd (relativ_tree a x) (relativ_tree a y). Proof. induction a; simpl; intros; auto. destruct b; repeat econstructor; auto. Qed. Lemma relativ_canon_commute : forall a x, canonicalTree a -> nonEmptyTree x -> mkCanon (relativ_tree a x) = relativ_tree a (mkCanon x). Proof. intros; apply canonicalUnique. 2: apply mkCanon_correct. 2: apply relativ_almost_canon; auto. apply shareTreeEq_trans with (relativ_tree a x). apply shareTreeEq_sym; auto. destruct (mkCanon_eq x). split; apply relativ_cong; auto. Qed. Lemma relativ_intersect : forall a x y, relativ_tree a (intersect_tree x y) = intersect_tree (relativ_tree a x) (relativ_tree a y). Proof. induction a; simpl; intros; auto. destruct b; simpl; auto. rewrite IHa1; rewrite IHa2; auto. Qed. Lemma relativ_union : forall a x y, relativ_tree a (union_tree x y) = union_tree (relativ_tree a x) (relativ_tree a y). Proof. induction a; simpl; intros; auto. destruct b; simpl; auto. rewrite IHa1; rewrite IHa2; auto. Qed. Lemma relativ_assoc : forall x y z, relativ_tree x (relativ_tree y z) = relativ_tree (relativ_tree x y) z. Proof. induction x; simpl; intros. destruct b; auto. rewrite IHx1. rewrite IHx2. auto. Qed. (* Here we have an unfortunate detour to develop a theory of many-hole contexts, which allows us to prove that relativization is injective on the left. *) Inductive ctx : Set := | NodeB : ctx -> ctx -> ctx | NodeR : ShareTree -> ctx -> ctx | NodeL : ctx -> ShareTree -> ctx | Hole : ctx . Fixpoint ctx_app (c1 c2:ctx) {struct c1} : ctx := match c1 with | NodeB l r => NodeB (ctx_app l c2) (ctx_app r c2) | NodeR l r => NodeR l (ctx_app r c2) | NodeL l r => NodeL (ctx_app l c2) r | Hole => c2 end. Fixpoint fill (c:ctx) (x:ShareTree) {struct c} : ShareTree := match c with | NodeR l r => Node l (fill r x) | NodeL l r => Node (fill l x) r | NodeB l r => Node (fill l x) (fill r x) | Hole => x end. Lemma fill_app : forall c1 c2 x, fill c1 (fill c2 x) = fill (ctx_app c1 c2) x. Proof. induction c1; simpl; intros. rewrite <- IHc1_1. rewrite <- IHc1_2. auto. rewrite IHc1; auto. rewrite IHc1; auto. auto. Qed. Lemma fill_id : forall x c, fill c x = x -> c = Hole. Proof. induction x; simpl; intros. destruct c; simpl in *; auto; discriminate. destruct c; auto; simpl in *. inversion H. replace (fill c1 (Node x1 x2)) with (fill (ctx_app c1 (NodeL Hole x2)) x1) in H1. generalize (IHx1 _ H1). destruct c1; simpl; intros; discriminate. rewrite <- fill_app; simpl; auto. inversion H. replace (fill c (Node x1 x2)) with (fill (ctx_app c (NodeR x1 Hole)) x2) in H2. generalize (IHx2 _ H2). destruct c; simpl; intros; discriminate. rewrite <- fill_app; simpl; auto. inversion H. replace (fill c (Node x1 x2)) with (fill (ctx_app c (NodeL Hole x2)) x1) in H1. generalize (IHx1 _ H1). destruct c; simpl; intros; discriminate. rewrite <- fill_app; simpl; auto. Qed. Definition to_ctx (a:ShareTree) : nonEmptyTree a -> ctx. refine (fix f (a:ShareTree) {struct a} : nonEmptyTree a -> ctx := match a as a' return nonEmptyTree a' -> ctx with | Leaf true => fun H => Hole | Leaf false => fun H => False_rec _ _ | Node l r => fun H => match nonEmpty_dec l, nonEmpty_dec r with | left Hl, left Hr => NodeB (f l Hl) (f r Hr) | left Hl, right _ => NodeL (f l Hl) r | right _ , left Hr => NodeR l (f r Hr) | right Hl, right Hr => False_rec _ _ end end). simpl in H; discriminate. simpl in H; intuition. Defined. Lemma relativ_to_ctx : forall a x H, relativ_tree a x = fill (to_ctx a H) x. Proof. induction a; simpl. destruct b; intros; try discriminate. simpl; auto. intros. destruct (nonEmpty_dec a1); destruct (nonEmpty_dec a2); simpl. rewrite <- IHa1; rewrite <- IHa2; auto. rewrite <- IHa1; auto. replace (relativ_tree a2 x) with a2; auto. clear -n0. induction a2; simpl. destruct b; simpl in *; auto. elim n0; auto. rewrite <- IHa2_1. rewrite <- IHa2_2; auto. intro; apply n0; simpl; auto. intro; apply n0; simpl; auto. rewrite <- IHa2. replace (relativ_tree a1 x) with a1; auto. clear -n. induction a1; simpl. destruct b; simpl in *; auto. elim n; auto. rewrite <- IHa1_1. rewrite <- IHa1_2; auto. intro; apply n; simpl; auto. intro; apply n; simpl; auto. elimtype False; intuition. Qed. Lemma relativ_stupid1 : forall x y a, nonEmptyTree x -> x = relativ_tree a (Node x y) -> False. Proof. intros. assert (nonEmptyTree a). apply relativ_empty1 with (Node x y). rewrite <- H0; auto. rewrite (relativ_to_ctx a (Node x y) H1) in H0. replace (fill (to_ctx a H1) (Node x y)) with (fill (ctx_app (to_ctx a H1) (NodeL Hole y)) x) in H0. symmetry in H0. generalize (fill_id _ _ H0). destruct (to_ctx a H1); simpl; intros; discriminate. rewrite <- fill_app; auto. Qed. Lemma relativ_stupid2 : forall x y a, nonEmptyTree y -> y = relativ_tree a (Node x y) -> False. Proof. intros. assert (nonEmptyTree a). apply relativ_empty1 with (Node x y). rewrite <- H0; auto. rewrite (relativ_to_ctx a (Node x y) H1) in H0. replace (fill (to_ctx a H1) (Node x y)) with (fill (ctx_app (to_ctx a H1) (NodeR x Hole)) y) in H0. symmetry in H0. generalize (fill_id _ _ H0). destruct (to_ctx a H1); simpl; intros; discriminate. rewrite <- fill_app; auto. Qed. Lemma relativ_stupid3 : forall a1 a2 x, nonEmptyTree x -> relativ_tree (Node a1 a2) x = x -> False. Proof. intros. assert (nonEmptyTree (Node a1 a2)). rewrite <- H0 in H. simpl in H. destruct H. left; apply relativ_empty1 with x; auto. right; apply relativ_empty1 with x; auto. rewrite (relativ_to_ctx (Node a1 a2) x H1) in H0. generalize (fill_id _ _ H0). simpl. destruct (nonEmpty_dec a1); destruct (nonEmpty_dec a2); intros; try discriminate. clear H0 H2. simpl in H1; destruct H1; auto. Qed. (* detour finished. now we can prove the result of interest, which is that relativization is injective on the left *) Lemma relativ_inv2 : forall a1 a2 x, nonEmptyTree x -> relativ_tree a1 x = relativ_tree a2 x -> a1 = a2. Proof. induction a1; intros. destruct b; simpl in *. revert a2 H0. induction x; simpl in *. subst b; simpl; intros. destruct a2; simpl in *. destruct b; auto. discriminate. intros. destruct a2; simpl in *. destruct b; auto. discriminate. injection H0; intros. destruct H. elim relativ_stupid1 with x1 x2 a2_1; auto. elim relativ_stupid2 with x1 x2 a2_2; auto. destruct a2; simpl in *. destruct b; auto. subst x; simpl in H; discriminate. discriminate. simpl in *. destruct a2; simpl in *. destruct b; try discriminate. elimtype False; clear -H H0. revert H0. intros. apply (relativ_stupid3 _ _ _ H H0). injection H0; intros. rewrite IHa1_1 with a2_1 x; auto. rewrite IHa1_2 with a2_2 x; auto. Qed. (* Define the subset type canonTree and show that it has decidable equality. *) Definition canonTree := { t:ShareTree | canonicalTree t }. Lemma shareTree_dec_eq : forall x y:ShareTree, {x=y}+{x<>y}. Proof. decide equality; apply bool_dec. Qed. Lemma canonTree_eq : forall x y:canonTree, proj1_sig x = proj1_sig y -> x = y. Proof. intros. destruct x as [x Hx]. destruct y as [y Hy]. simpl in *. subst y. replace Hy with Hx by apply proof_irr; auto. Qed. Lemma canonTree_eq_dec : forall x y:canonTree, {x=y}+{x<>y}. Proof. intros. destruct x as [x Hx]. destruct y as [y Hy]. destruct (shareTree_dec_eq x y); [ left | right ]. apply canonTree_eq; simpl; auto. red; intros. injection H. auto. Qed. (* Show that complement preserves canonical trees *) Lemma comp_tree_inv : forall t, comp_tree (comp_tree t) = t. Proof. induction t; simpl; intros; try destruct_bool; auto. rewrite IHt1; rewrite IHt2; auto. Qed. Lemma comp_full_empty : forall x, nonFullTree x -> nonEmptyTree (comp_tree x). Proof. intro x; induction x; simpl; intros; destruct_bool; intuition. Qed. Lemma comp_empty_full : forall x, nonEmptyTree x -> nonFullTree (comp_tree x). Proof. intro x; induction x; simpl; intros; destruct_bool; intuition. Qed. Hint Resolve comp_full_empty comp_empty_full. Lemma comp_canonical : forall x, canonicalTree x -> canonicalTree (comp_tree x). Proof. intro x; induction x; simpl; intros; intuition. Qed. (*** Begin Module Signature Definitions and lemmas ***) (* Here we show that canonical share trees form a boolean algrbra. These proofs mainly involve showing that the results above commute in the proper ways with mkCanon. *) Module BA <: BOOLEAN_ALGEBRA. Definition t := canonTree. Definition Ord (x y:canonTree) := shareTreeOrd (proj1_sig x) (proj1_sig y). Definition lub (x y:canonTree) : canonTree := exist (fun t => canonicalTree t) (mkCanon (union_tree (proj1_sig x) (proj1_sig y))) (mkCanon_correct _). Definition glb (x y:canonTree) : canonTree := exist (fun t => canonicalTree t) (mkCanon (intersect_tree (proj1_sig x) (proj1_sig y))) (mkCanon_correct _). Definition top : canonTree := exist (fun t => canonicalTree t) (Leaf true) I. Definition bot : canonTree := exist (fun t => canonicalTree t) (Leaf false) I. Definition comp (x:canonTree) : canonTree := exist (fun t => canonicalTree t) (comp_tree (proj1_sig x)) (comp_canonical _ (proj2_sig x)). Lemma ord_refl : forall x, Ord x x. Proof. intros [x Hx]; unfold Ord; simpl. apply shareTreeOrd_refl. Qed. Lemma ord_trans : forall x y z, Ord x y -> Ord y z -> Ord x z. Proof. intros [x Hx] [y Hy] [z Hz]; unfold Ord; simpl; intros. apply shareTreeOrd_trans with y; auto. Qed. Lemma ord_antisym : forall x y, Ord x y -> Ord y x -> x = y. Proof. intros [x Hx] [y Hy]; unfold Ord; simpl; intros. apply canonTree_eq; simpl. apply canonicalUnique; try split; auto. Qed. Lemma lub_upper1 : forall x y, Ord x (lub x y). Proof. intros [x Hx] [y Hy]; unfold Ord; simpl; intros. destruct (mkCanon_eq (union_tree x y)). apply shareTreeOrd_trans with (union_tree x y); auto. apply union_upper_bound. Qed. Lemma lub_upper2 : forall x y, Ord y (lub x y). Proof. intros [x Hx] [y Hy]; unfold Ord; simpl; intros. destruct (mkCanon_eq (union_tree x y)). apply shareTreeOrd_trans with (union_tree x y); auto. rewrite union_commute. apply union_upper_bound. Qed. Lemma lub_least : forall x y z, Ord x z -> Ord y z -> Ord (lub x y) z. Proof. intros [x Hx] [y Hy] [z Hz]; unfold Ord; simpl; intros. destruct (mkCanon_eq (union_tree x y)). apply shareTreeOrd_trans with (union_tree x y); auto. apply union_least_bound; auto. Qed. Lemma glb_lower1 : forall x y, Ord (glb x y) x. Proof. intros [x Hx] [y Hy]; unfold Ord; simpl; intros. destruct (mkCanon_eq (intersect_tree x y)). apply shareTreeOrd_trans with (intersect_tree x y); auto. apply intersection_lower_bound. Qed. Lemma glb_lower2 : forall x y, Ord (glb x y) y. Proof. intros [x Hx] [y Hy]; unfold Ord; simpl; intros. destruct (mkCanon_eq (intersect_tree x y)). apply shareTreeOrd_trans with (intersect_tree x y); auto. rewrite intersect_commute. apply intersection_lower_bound. Qed. Lemma glb_greatest : forall x y z, Ord z x -> Ord z y -> Ord z (glb x y). Proof. intros [x Hx] [y Hy] [z Hz]; unfold Ord; simpl; intros. destruct (mkCanon_eq (intersect_tree x y)). apply shareTreeOrd_trans with (intersect_tree x y); auto. apply intersection_greatest_bound; auto. Qed. Lemma top_correct : forall x, Ord x top. Proof. intros [x Hx]; unfold Ord; simpl; auto. Qed. Lemma bot_correct : forall x, Ord bot x. Proof. intros [x Hx]; unfold Ord; simpl; auto. Qed. Lemma comp1 : forall x, lub x (comp x) = top. Proof. intros [x Hx]; simpl. apply canonTree_eq; simpl. apply fullTree_canonical_trueLeaf. 2: apply mkCanon_correct. apply geTrueFull. apply shareTreeOrd_trans with (union_tree x (comp_tree x)). 2: destruct (mkCanon_eq (union_tree x (comp_tree x))); auto. apply tree_comp1. Qed. Lemma comp2 : forall x, glb x (comp x) = bot. Proof. intros [x Hx]; simpl. apply canonTree_eq; simpl. apply emptyTree_canonical_falseLeaf. 2: apply mkCanon_correct. apply leFalseEmpty. apply shareTreeOrd_trans with (intersect_tree x (comp_tree x)). destruct (mkCanon_eq (intersect_tree x (comp_tree x))); auto. apply tree_comp2. Qed. Lemma lat_nontrivial : top <> bot. Proof. discriminate. Qed. Lemma distrib1 : forall x y z, glb x (lub y z) = lub (glb x y) (glb x z). Proof. intros [x Hx] [y Hy] [z Hz]; unfold glb, lub. apply canonTree_eq; simpl. apply canonicalUnique; try apply mkCanon_correct. apply shareTreeEq_trans with (intersect_tree x (mkCanon (union_tree y z))). apply shareTreeEq_sym. apply mkCanon_eq. apply shareTreeEq_trans with (union_tree (mkCanon (intersect_tree x y)) (mkCanon (intersect_tree x z))). 2: apply mkCanon_eq. apply shareTreeEq_trans with (intersect_tree x (union_tree y z)). apply intersect_cong. apply shareTreeEq_refl. apply shareTreeEq_sym. apply mkCanon_eq. apply shareTreeEq_trans with (union_tree (intersect_tree x y) (intersect_tree x z)). rewrite intersect_distrib. apply shareTreeEq_refl. apply union_cong. apply mkCanon_eq. apply mkCanon_eq. Qed. Lemma distrib2 : forall x y z, lub x (glb y z) = glb (lub x y) (lub x z). Proof. intros [x Hx] [y Hy] [z Hz]; unfold glb, lub. apply canonTree_eq; simpl. apply canonicalUnique; try apply mkCanon_correct. apply shareTreeEq_trans with (union_tree x (mkCanon (intersect_tree y z))). apply shareTreeEq_sym. apply mkCanon_eq. apply shareTreeEq_trans with (intersect_tree (mkCanon (union_tree x y)) (mkCanon (union_tree x z))). 2: apply mkCanon_eq. apply shareTreeEq_trans with (union_tree x (intersect_tree y z)). apply union_cong. apply shareTreeEq_refl. apply shareTreeEq_sym. apply mkCanon_eq. apply shareTreeEq_trans with (intersect_tree (union_tree x y) (union_tree x z)). rewrite union_distrib. apply shareTreeEq_refl. apply intersect_cong. apply mkCanon_eq. apply mkCanon_eq. Qed. End BA. Module BAF := BA_Facts BA. (* Now, we prove the axioms about relativization. Again, this mostly involves packing and unpacking the canonTree type and pushing around mkCanon. *) Module Relativ : BA_RELATIV with Module BAF:=BAF. Module BAF:=BAF. Import BAF. Definition rel (a x:t) : t. intros a x. case_eq (proj1_sig x); intros. destruct b. exact a. exact (exist (fun t => canonicalTree t) (Leaf false) I). refine (exist _ (relativ_tree (proj1_sig a) (proj1_sig x)) _). apply relativ_almost_canon. apply (proj2_sig a). apply (proj2_sig x). destruct x; simpl in *; subst; simpl in *; intuition. Defined. Lemma relativ_tree_empty : forall a x, nonEmptyTree a -> nonEmptyTree x -> nonEmptyTree (relativ_tree a x). Proof. induction a; simpl; intros. destruct b; auto. intuition; eauto. Qed. Lemma relativ_tree_nonid : forall a x1 x2, nonEmptyTree a -> a = relativ_tree a (Node x1 x2) -> False. Proof. induction a; simpl; intros; try destruct_bool; try discriminate. injection H0; clear H0; intros. intuition; eauto. Qed. Lemma rel_classification : forall a x, { x = bot /\ rel a x = bot } + { x <> bot /\ proj1_sig (rel a x) = relativ_tree (proj1_sig a) (proj1_sig x) /\ (a = bot <-> rel a x = bot) }. Proof. intros [a ?] [x ?]. simpl. destruct x; try destruct_bool; simpl. right; split. red; intros. discriminate H. split. rewrite relativ_full; auto. split; intros. injection H; clear H; intros. subst a. apply canonTree_eq; simpl; auto. apply canonTree_eq; simpl. injection H; auto. left; split; auto. apply canonTree_eq; auto. right; split. red; intros; discriminate. split; auto. split; intros. apply canonTree_eq; simpl; auto. injection H; clear H; intros. rewrite H; auto. injection H; clear H; intros. apply canonTree_eq; simpl; auto. destruct a; simpl in *; destruct_bool; auto; try discriminate. Qed. Lemma rel_inj_r : forall a1 a2 x, x <> bot -> rel a1 x = rel a2 x -> a1 = a2. Proof. intros. apply canonTree_eq. destruct (rel_classification a1 x); intuition. destruct (rel_classification a2 x); intuition. apply relativ_inv2 with (proj1_sig x); auto. destruct x; simpl. destruct x; simpl. destruct b; auto. elim H; simpl. apply canonTree_eq; auto. generalize c; simpl; intuition. rewrite <- H3. rewrite <- H7. rewrite H0. auto. Qed. Lemma rel_inj_l : forall a x y, a <> bot -> rel a x = rel a y -> x = y. Proof. intros. apply canonTree_eq. destruct a as [a ?]; destruct x as [x ?]; destruct y as [y ?]; simpl. assert (nonEmptyTree a). destruct a; simpl in *. destruct b; auto. elim H; apply canonTree_eq; simpl; auto. decompose [and] c; auto. unfold rel in *; simpl in *. destruct x; destruct y; destruct_bool; auto; injection H0; clear H0; try congruence; intros. elim (relativ_tree_nonid a y1 y2); auto. simpl in c1; decompose [and] c1. generalize (relativ_tree_empty a (Node y1 y2) H1 H4). rewrite <- H0; simpl; intros; discriminate. elim (relativ_tree_nonid a x1 x2); auto. simpl in c0; decompose [and] c0. generalize (relativ_tree_empty a (Node x1 x2) H1 H4). rewrite H0; simpl; intros; discriminate. apply canonicalUnique; auto. split; apply relativ_inv with a; auto; rewrite H0; apply shareTreeOrd_refl. Qed. Lemma rel_assoc : forall x y z, rel x (rel y z) = rel (rel x y) z. Proof. intros. apply canonTree_eq. destruct (rel_classification x (rel y z)); intuition. rewrite H0. destruct (rel_classification (rel x y) z); intuition. rewrite H1. simpl; auto. destruct (rel_classification x y); intuition. rewrite H7; auto. rewrite H3. rewrite H7. rewrite <- relativ_assoc. destruct (rel_classification y z); intuition. rewrite H1. destruct (rel_classification y z); intuition. destruct (rel_classification (rel x y) z); intuition. rewrite H9. destruct (rel_classification x y); intuition. rewrite H13. rewrite H5. apply relativ_assoc. Qed. Lemma rel_bot1 : forall a, rel a bot = bot. Proof. intros [a ?]; auto. Qed. Lemma rel_bot2 : forall x, rel bot x = bot. Proof. intros e. destruct (rel_classification bot e); intuition. Qed. Lemma rel_top1 : forall a, rel a top = a. Proof. intros a. destruct (rel_classification a top); intuition. Qed. Lemma rel_top2 : forall x, rel top x = x. Proof. intro x. destruct (rel_classification top x); intuition. congruence. apply canonTree_eq. rewrite H1. simpl; auto. Qed. Lemma rel_preserves_glb : forall a x y, rel a (glb x y) = glb (rel a x) (rel a y). Proof. intros a x y. destruct (rel_classification a x); intuition. rewrite H0. rewrite H. rewrite glb_commute. rewrite glb_bot. rewrite rel_bot1. rewrite glb_commute. rewrite glb_bot. auto. destruct (rel_classification a y); intuition. rewrite H4. rewrite H2. rewrite glb_bot. rewrite glb_bot. apply rel_bot1. apply canonTree_eq. simpl. rewrite H1. rewrite H5. rewrite <- relativ_intersect. destruct (rel_classification a (glb x y)); intuition. rewrite H8. simpl. injection H6; intros. apply (mkCanon_test2 (Leaf false)). apply shareTreeEq_trans with (relativ_tree (proj1_sig a) (Leaf false)). split. apply falseLeaf_bottom. apply emptyLeFalse. intro G. generalize (relativ_empty2 _ _ G); auto. simpl; intros; discriminate. generalize (mkCanon_test _ (Leaf false) H9). unfold shareTreeEq; intuition; apply relativ_cong; auto. rewrite H9. simpl. rewrite relativ_canon_commute; auto. destruct a; auto. destruct (nonEmpty_dec (intersect_tree (proj1_sig x) (proj1_sig y))); auto. elim H6. apply canonTree_eq; simpl. symmetry. apply (mkCanon_test2 (Leaf false)). split. apply falseLeaf_bottom. apply emptyLeFalse; auto. Qed. Lemma rel_preserves_lub : forall a x y, rel a (lub x y) = lub (rel a x) (rel a y). Proof. intros a x y. destruct (rel_classification a x); intuition. rewrite H0. rewrite H. rewrite lub_commute. rewrite lub_bot. rewrite lub_commute. rewrite lub_bot. auto. destruct (rel_classification a y); intuition. rewrite H4. rewrite H2. rewrite lub_bot. rewrite lub_bot. auto. apply canonTree_eq. simpl. rewrite H1. rewrite H5. rewrite <- relativ_union. destruct (rel_classification a (lub x y)); intuition. rewrite H8. simpl. injection H6; intros. apply (mkCanon_test2 (Leaf false)). apply shareTreeEq_trans with (relativ_tree (proj1_sig a) (Leaf false)). split. apply falseLeaf_bottom. apply emptyLeFalse. intro G. generalize (relativ_empty2 _ _ G). simpl; intros; discriminate. generalize (mkCanon_test _ (Leaf false) H9). unfold shareTreeEq; intuition; apply relativ_cong; auto. rewrite H9. simpl. rewrite relativ_canon_commute; auto. destruct a; auto. destruct (nonEmpty_dec (union_tree (proj1_sig x) (proj1_sig y))); intros; auto. elim H6. apply canonTree_eq; simpl. symmetry. apply (mkCanon_test2 (Leaf false)). split. apply falseLeaf_bottom. apply emptyLeFalse; auto. Qed. End Relativ. (* Axioms about splittability. These follow easily from relativization. *) Module Splittable : SPLITTABLE_LATTICE with Module BAF:=BAF. Module BAF:=BAF. Import BAF. Definition leftTree : canonTree. exists (Node (Leaf true) (Leaf false)). simpl; intuition. Defined. Definition rightTree : canonTree. exists (Node (Leaf false) (Leaf true)). simpl; intuition. Defined. Definition split (x:canonTree) := (Relativ.rel x leftTree, Relativ.rel x rightTree). Lemma split_disjoint : forall x1 x2 x, split x = (x1, x2) -> glb x1 x2 = bot. Proof. unfold split; intros. inv H. rewrite <- Relativ.rel_preserves_glb. replace (glb leftTree rightTree) with bot. apply Relativ.rel_bot1. apply canonTree_eq; simpl; auto. Qed. Lemma split_together : forall x1 x2 x, split x = (x1, x2) -> lub x1 x2 = x. Proof. unfold split; intros. inv H. rewrite <- Relativ.rel_preserves_lub. replace (lub leftTree rightTree) with top. apply Relativ.rel_top1. apply canonTree_eq; simpl; auto. Qed. Lemma split_nontrivial : forall x1 x2 x, split x = (x1, x2) -> (x1 = bot \/ x2 = bot) -> x = bot. Proof. unfold split; intros. inv H; destruct H0. destruct (canonTree_eq_dec x bot); auto. replace bot with (Relativ.rel x bot) in H. apply Relativ.rel_inj_l in H; auto. inv H. apply Relativ.rel_bot1. destruct (canonTree_eq_dec x bot); auto. replace bot with (Relativ.rel x bot) in H. apply Relativ.rel_inj_l in H; auto. inv H. apply Relativ.rel_bot1. Qed. End Splittable. (* Unlike the previous modules, this one contains significant proof development. We want to show that there are two special classe of share trees: those which represent token factories and those which represent tokens. The motivating idea is that token factories are represented as encodings of cofinite sets of natural number , whereas tokesn are represented as encodings of finite sets of natural numbers. We can always remove a finite set (a token) from a cofinite set (a token factory) and get another cofinite set (token factory). Furthermore, we can precicely describe the "size" of tokens and token factories as the number of elements in the set (for finite elements) or in the complement (for cofinite sets). *) Module TokenFactory : TOKEN_FACTORY with Module BAF:=BAF. Module BAF:=BAF. Import BAF. (* Here we define a datatype represneting finite or cofinite sets of natural numbers. The idea is that we have a list of booleans. When the ith element of the list is true, i is in the set. When the ith element is false, or if the list has fewer than i elements, i is not in the set. For finite sets, we take exactily the set described by the list of booleans, but for cofinite sets, we take the complement. However, we want a canonical representation, which means that we cannot allow lists with trailing falses; every list must end with at least one true, or be empty. Rather than carry around this fact as a proof, I have built it into the representation. A 'None' represents and empty list, and thus, the empty set. A 'Some' with list 'l' represents the list l with a single true appended to the end. This means that when we interpret the set as a share tree, we always obtain canonical trees, and we don't have to canonicalize them. *) Inductive natset : Set := | fin : option (list bool) -> natset | cofin : option (list bool) -> natset. (* To interpret a list of booleans as a tree, we use a right-biased tree representation, where the left-side leaf nodes carry the elements of the list. We always add the assumed final "true" node on the left and terminate the list with a "false" node on the right. *) Fixpoint interpBools (t:list bool) : ShareTree := match t with | b::t' => Node (Leaf b) (interpBools t') | nil => Node (Leaf true) (Leaf false) end. (* The number of naturals in the set represented by this list. Remember that we assume a final "true", so the count is always at least 1. *) Fixpoint countBools (t:list bool) : nat := match t with | true::t' => S (countBools t') | false::t' => countBools t' | nil => S O end. Definition interp_natset (ns:natset) : ShareTree := match ns with | fin None => Leaf false | fin (Some x) => interpBools x | cofin None => Leaf true | cofin (Some x) => comp_tree (interpBools x) end. Definition count_natset (ns:natset) : nat := match ns with | fin None => O | cofin None => O | fin (Some x) => countBools x | cofin (Some x) => countBools x end. Lemma count_gt_O : (forall t, countBools t > 0)%nat. Proof. induction t0; simpl; intros; auto. destruct a; omega. Qed. (* Because of our special representation, interpBools always produces nonFull, nonEmpty, canonical trees. *) Lemma interp_nonFull : forall t, nonFullTree (interpBools t). Proof. induction t0; simpl; intuition. Qed. Lemma interp_nonEmpty : forall t, nonEmptyTree (interpBools t). Proof. induction t0; simpl; intuition. Qed. Hint Resolve interp_nonFull interp_nonEmpty. Lemma interp_canon : forall t, canonicalTree (interpBools t). Proof. induction t0; simpl; intuition. Qed. Hint Resolve comp_canonical interp_canon. (* This means that our natsets are always interpreted as canonical trees as well. *) Lemma interp_natset_canon : forall ns, canonicalTree (interp_natset ns). Proof. intro ns; destruct ns; destruct o; simpl; auto. Qed. Hint Resolve interp_natset_canon. (* We then define the token factories of size n as those which represent a cofinite set of size n. *) Definition isTokenFactory (x:t) (n:nat) := (exists o, proj1_sig x = interp_natset (cofin o) /\ count_natset (cofin o) = n). (* Likewise, tokens of size n are trees which represent finite sets of size n. *) Definition isToken (x:t) (n:nat) := (exists o, proj1_sig x = interp_natset (fin o) /\ count_natset (fin o) = n). Lemma fullFactory : forall x, isTokenFactory x 0 <-> x = top. Proof. unfold isTokenFactory; split; intros. destruct x. apply canonTree_eq; simpl. destruct H as [o [Ho1 Ho2]]. destruct o; simpl in *; try discriminate; auto. generalize (count_gt_O l). rewrite Ho2; intro; elimtype False; omega. destruct x; injection H; simpl; intros. subst x; simpl. exists (@None (list bool)); auto. Qed. Lemma identityToken : forall x, isToken x 0 <-> x = bot. Proof. unfold isToken; split; intros. destruct x. apply canonTree_eq; simpl. destruct H as [o [Ho1 Ho2]]. destruct o; simpl in *; try discriminate; auto. generalize (count_gt_O l). rewrite Ho2; intro; elimtype False; omega. destruct x; injection H; simpl; intros. subst x; simpl. exists (@None (list bool)); auto. Qed. Lemma nonidentityToken : forall x n, (n > 0)%nat -> isToken x n -> x <> bot. Proof. unfold isToken; intros. destruct H0 as [o [Ho1 Ho2]]. destruct o; simpl in *. intro H1. destruct x; injection H1; intros. subst x; simpl in *. generalize (interp_nonEmpty l). rewrite <- Ho1. simpl; intro; discriminate. subst n; omega. Qed. Lemma nonidentityFactory : forall x n, isTokenFactory x n -> x <> bot. Proof. unfold isTokenFactory. intros. destruct H as [o [Ho1 Ho2]]. destruct o; simpl in *. destruct x; simpl in *. intro H; injection H; intros. rewrite H0 in Ho1. destruct l; simpl in *; discriminate. destruct x; simpl in *. intro H; injection H; intros. subst x; discriminate. Qed. (* This lemma says that two token factories will always have some area in common. This is because they always end with a true node on the far right. *) Lemma factoryOverlap : forall f1 f2 n1 n2, isTokenFactory f1 n1 -> isTokenFactory f2 n2 -> glb f1 f2 <> bot. Proof. intros. destruct f1; destruct f2; simpl in *. red in H, H0. destruct H as [o1 [H1 H2]]. destruct H0 as [o2 [H3 H4]]. simpl in *. intro H; injection H; clear H; intro H. assert (shareTreeEq (intersect_tree x x0) (Leaf false)). rewrite <- H. apply mkCanon_eq. destruct H0. clear c c0 H H5. destruct o1; subst. destruct o2; subst. revert l0 H0; induction l; simpl; intros; destruct l0; simpl in *; invert_ord; try discriminate. induction l0; simpl in *; invert_ord; auto; discriminate. destruct a; simpl in *. rewrite intersect_commute in H5; simpl in H5. clear -H5; induction l; simpl in *; intros; invert_ord; auto; discriminate. rewrite intersect_commute in H5; simpl in H5. clear -H5; induction l; simpl in *; intros; invert_ord; auto; discriminate. apply IHl with l0; auto. rewrite intersect_commute in H0; simpl in H0. induction l; simpl in *; intros; invert_ord; auto; discriminate. destruct o2; subst; simpl in *. induction l; simpl in *; intros; invert_ord; auto; discriminate. invert_ord; discriminate. Qed. (* This series of lemmas allows us to strengthen non-informative existance statments about natset representations to informative sigma types. *) Lemma ex_sig_bools : forall (x:ShareTree) n, (exists l, x = interpBools l /\ countBools l = n) -> { l:list bool & x = interpBools l /\ countBools l = n }. Proof. induction x; simpl; intros. elimtype False. destruct H as [l [Hl1 Hl2]]. destruct l; discriminate. destruct x1. destruct n. elimtype False. destruct H as [l [Hl1 Hl2]]. generalize (count_gt_O l); rewrite Hl2; intro; omega. destruct x2. assert (b = true /\ b0 = false /\ n = 0%nat). destruct H as [l [Hl1 Hl2]]. destruct l; simpl in *. repeat split; congruence. destruct l; discriminate. intuition; subst. exists (@nil bool); simpl; auto. destruct b. destruct (IHx2 n) as [l [Hl1 Hl2]]; clear IHx1 IHx2. destruct H as [l [Hl1 Hl2]]. destruct l; simpl in *; try discriminate. assert (b = true) by congruence; subst b. exists l; split; congruence. exists (true::l); simpl; split; congruence. destruct (IHx2 (S n)) as [l [Hl1 Hl2]]; clear IHx1 IHx2. destruct H as [l [Hl1 Hl2]]. destruct l; simpl in *; try discriminate. assert (b = false) by congruence; subst b. exists l; split; congruence. exists (false::l); simpl; split; congruence. elimtype False. destruct H as [l [Hl1 Hl2]]. destruct l; discriminate. Qed. Lemma ex_sig_cofin : forall (x:t) n, (exists o, proj1_sig x = interp_natset (cofin o) /\ count_natset (cofin o) = n) -> { o:_ & proj1_sig x = interp_natset (cofin o) /\ count_natset (cofin o) = n }. Proof. intros [x Hx]; simpl; intros. destruct x. destruct b. destruct n. exists (@None (list bool)); auto. elimtype False. destruct H as [o [Ho1 Ho2]]. destruct o. destruct l; discriminate. discriminate. elimtype False. destruct H as [o [Ho1 Ho2]]. destruct o. destruct l; discriminate. discriminate. destruct (ex_sig_bools (comp_tree (Node x1 x2)) n) as [l [Hl1 Hl2]]. destruct H as [o [Ho1 Ho2]]. destruct o; try discriminate. exists l; split; auto. rewrite <- (comp_tree_inv (interpBools l)). rewrite <- Ho1; auto. exists (Some l); split; auto. rewrite <- Hl1. rewrite comp_tree_inv. auto. Qed. Lemma ex_sig_fin : forall (x:t) n, (exists o, proj1_sig x = interp_natset (fin o) /\ count_natset (fin o) = n) -> { o:_ & proj1_sig x = interp_natset (fin o) /\ count_natset (fin o) = n }. Proof. intros [x Hx]; simpl; intros. destruct x. destruct b. elimtype False. destruct H as [o [Ho1 Ho2]]. destruct o. destruct l; discriminate. discriminate. destruct n. exists (@None (list bool)); auto. elimtype False. destruct H as [o [Ho1 Ho2]]. destruct o. destruct l; discriminate. discriminate. destruct (ex_sig_bools (Node x1 x2) n) as [l [Hl1 Hl2]]. destruct H as [o [Ho1 Ho2]]. destruct o; try discriminate. exists l; split; auto. exists (Some l); split; auto. Qed. (* These functions calculate the result of splitting a size 1 token from a token factory. Note we have to account for the phantom trailing "true" node. *) Fixpoint split_fac1 (l:list bool) : list bool := match l with | false :: l' => true :: l' | true :: l' => true :: split_fac1 l' | nil => true :: nil end. Fixpoint split_tok1 (l:list bool) : list bool := match l with | false :: l' => nil | true :: l' => false :: split_tok1 l' | nil => false :: nil end. (* This lemma says that we can chose a size 1 token and remove it from a token factory *) Lemma splitToken1 : forall fac x, isTokenFactory fac x -> { fac':t & {tok:t | isTokenFactory fac' (S x) /\ isToken tok 1 /\ join fac' tok fac}}. Proof. intros fac x H. destruct (ex_sig_cofin fac x H) as [o [Ho1 Ho2]]; clear H. destruct fac; simpl in *. destruct o; simpl in *; subst. exists (exist (fun t => canonicalTree t) (interp_natset (cofin (Some (split_fac1 l)))) (interp_natset_canon _)). exists (exist (fun t => canonicalTree t) (interp_natset (fin (Some (split_tok1 l)))) (interp_natset_canon _)). simpl; repeat split; simpl; try red. exists (Some (split_fac1 l)); simpl; split; auto. clear; induction l; simpl; auto. destruct a; simpl; auto. exists (Some (split_tok1 l)); simpl; split; auto. clear; induction l; simpl; auto. destruct a; simpl; auto. apply canonTree_eq; simpl. apply canonicalUnique; auto. apply shareTreeEq_sym. eapply shareTreeEq_trans; [ | apply mkCanon_eq ]. split; auto. clear; induction l; simpl; auto. destruct a; simpl. do 2 constructor; auto. do 2 constructor; auto. rewrite intersect_commute; simpl; auto. simpl; auto. apply canonTree_eq; simpl. apply canonicalUnique; auto. apply shareTreeEq_sym. eapply shareTreeEq_trans; [ | apply mkCanon_eq ]. clear; induction l. simpl; split; auto. destruct a; simpl; split; auto. constructor; auto. destruct IHl; auto. constructor; auto. destruct IHl; auto. constructor; auto. rewrite union_commute; simpl; auto. apply shareTreeOrd_refl. constructor; auto. rewrite union_commute; simpl; auto. apply shareTreeOrd_refl. exists (exist (fun t => canonicalTree t) (interp_natset (cofin (Some nil))) (interp_natset_canon _)). exists (exist (fun t => canonicalTree t) (interp_natset (fin (Some nil))) (interp_natset_canon _)). repeat split; simpl; try red. exists (Some (@nil bool)); simpl; split; auto. exists (Some (@nil bool)); simpl; split; auto. apply canonTree_eq; simpl; apply canonicalUnique; auto. apply canonTree_eq; simpl; apply canonicalUnique; auto. Qed. (* This lemma says that we can join a size 1 token back into a token factory *) Lemma absorbToken1 : forall fac x, { fac':t & {tok:t | isTokenFactory fac' (S x) /\ isToken tok 1 /\ join fac' tok fac}} -> isTokenFactory fac x. Proof. intros fac x [fac' [tok [H1 [H2 H3]]]]. destruct H1 as [ofac [H4 H5]]. destruct H2 as [otok [H6 H7]]. red. destruct fac'; destruct fac; destruct tok; simpl in *. destruct H3 as [H31 H32]; injection H31; clear H31; injection H32; clear H32. destruct ofac; try discriminate. destruct otok; try discriminate. subst. intros H H0. rewrite union_commute in H. rewrite intersect_commute in H0. assert (shareTreeEq x1 (union_tree (interpBools l0) (comp_tree (interpBools l)))). rewrite <- H. apply shareTreeEq_sym; apply mkCanon_eq. assert (shareTreeEq (Leaf false) (intersect_tree (interpBools l0) (comp_tree (interpBools l)))). rewrite <- H0. apply shareTreeEq_sym; apply mkCanon_eq. destruct H2. revert H1 H3. clear -c0 H5 H7. revert x l x1 c0 H5 H7. induction l0; simpl; intros. destruct l; simpl in *. exists (@None (list bool)); split; auto. apply canonicalUnique; simpl; auto. apply shareTreeEq_trans with (Node (Leaf true) (Leaf true)); auto. destruct b; simpl in *. destruct x1; destruct_bool; invert_ord; try discriminate. elimtype False; clear -H11; induction l; simpl in *; invert_ord; auto; discriminate. assert (x1_1 = Leaf true). apply canonicalUnique; simpl; auto. simpl in *; intuition. subst x1_1. exists (Some (false::l)); split; simpl; auto. replace (comp_tree (interpBools l)) with x1_2; auto. apply canonicalUnique; auto. simpl in *; intuition. invert_ord; discriminate. destruct a; simpl in *. elimtype False; injection H7; clear. induction l0; simpl; intros; destruct_bool; auto; discriminate. destruct l; simpl in *. rewrite intersect_commute in H3. invert_ord. elimtype False; clear -H9. induction l0; simpl in *; invert_ord; auto; discriminate. destruct b; simpl in *. destruct x1; invert_ord. destruct b; try discriminate. elimtype False; revert H9; generalize (comp_tree (interpBools l)); clear. induction l0; simpl; intros. destruct s; destruct_bool; invert_ord; discriminate. destruct s; destruct_bool; invert_ord; auto; try discriminate. apply IHl0 with (Leaf false). rewrite union_commute; auto. apply IHl0 with s2; auto. assert (x1_1 = Leaf false). apply canonicalUnique; simpl; auto. simpl in *; intuition. subst x1_1. destruct x. elimtype False. injection H5; clear. induction l; simpl; destruct_bool; intros; auto; discriminate. destruct (IHl0 x l x1_2); auto. simpl in *; intuition. destruct x0; destruct H. exists (Some (true::l1)); simpl; split; congruence. exists (Some (@nil bool)); simpl; split; congruence. destruct x1; destruct_bool; invert_ord; try discriminate. exists (@None (list bool)). split; auto. clear -H5 H7 H11. revert x l H5 H7 H11. induction l0; simpl; intros. destruct l; simpl in *; try congruence. invert_ord. elimtype False; clear -H6; induction l; simpl in *; invert_ord; auto; discriminate. destruct a. elimtype False; injection H7; clear; induction l0; simpl; intros; destruct_bool; auto; discriminate. destruct l; simpl in *; try congruence. destruct b; invert_ord; try discriminate. apply IHl0 with l; auto. assert (x1_1 = Leaf true). apply canonicalUnique; simpl; auto. simpl in *; intuition. subst x1_1. destruct (IHl0 x l x1_2); auto. simpl in *; intuition. destruct x0; destruct H. exists (Some (false::l1)); simpl; split; congruence. subst x1_2. clear -c0. elimtype False; simpl in *; intuition. Qed. (* These functions calculate the result of splitting a size 1 token off of a token of at least size 2. Note that some of the branches are bogus; they will be pruned in the proof. *) Fixpoint split_tok_tok1 (l:list bool) : list bool := match l with | true :: l => nil | false :: l => false :: split_tok_tok1 l | nil => nil end. Fixpoint split_tok_tok2 (l:list bool) : list bool := match l with | true :: l => false :: l | false :: l => false :: split_tok_tok2 l | nil => nil end. (* This function calculates the result of merging two tokens *) Fixpoint merge_token (l1 l2:list bool) { struct l1 } : list bool := match l1, l2 with | nil, nil => nil | x::l1', nil => true :: l1' | nil, x::l2' => true :: l2' | true::l1', x::l2' => true :: merge_token l1' l2' | false::l1', x::l2' => x :: merge_token l1' l2' end. (* This lemma says that we can split off a size 1 token from any token with size at least 2. *) Lemma unmergeToken1 : forall tok n, isToken tok (S (S n)) -> { tok1:t & { tok2:t & isToken tok1 1 /\ isToken tok2 (S n) /\ join tok1 tok2 tok }}. Proof. intros. red in H. destruct (ex_sig_fin tok (S (S n)) H) as [o [Ho1 Ho2]]; clear H. destruct tok; simpl in *. destruct o; try discriminate. exists (exist (fun t => canonicalTree t) (interp_natset (fin (Some (split_tok_tok1 l)))) (interp_natset_canon _)). exists (exist (fun t => canonicalTree t) (interp_natset (fin (Some (split_tok_tok2 l)))) (interp_natset_canon _)). repeat split; try red; simpl. exists (Some (split_tok_tok1 l)); split; auto. clear; induction l; simpl; auto. destruct a; simpl; auto. exists (Some (split_tok_tok2 l)); split; auto. revert Ho2; clear; induction l; simpl; intros. discriminate. destruct a; simpl in *; auto; congruence. apply canonTree_eq; simpl. apply canonicalUnique; simpl; auto. apply shareTreeEq_sym. eapply shareTreeEq_trans; [ | apply mkCanon_eq ]. clear -Ho2; induction l; simpl in *. discriminate. destruct a; simpl in *; auto. do 3 constructor; auto. apply canonTree_eq; simpl. apply canonicalUnique; simpl; auto. apply shareTreeEq_sym. eapply shareTreeEq_trans; [ | apply mkCanon_eq ]. clear c. revert x n Ho1 Ho2; induction l; simpl in *; intros. discriminate. destruct a; simpl in *; auto. subst x; apply shareTreeEq_refl. destruct x; destruct_bool; try discriminate. replace x1 with (Leaf false) by congruence. apply Node_Eq; auto. apply IHl with n; auto. simpl in *; intuition. congruence. Qed. (* This lemma says that we can join a size 1 token into another token of size at least 1. *) Lemma mergeToken1 : forall tok1 n tok2 tok', isToken tok1 1 -> isToken tok2 (S n) -> join tok1 tok2 tok' -> isToken tok' (S (S n)). Proof. intros. destruct H as [o1 [H3 H4]]. destruct H0 as [o2 [H5 H6]]. destruct H1 as [H7 H8]. destruct tok1; destruct tok2; destruct tok'; simpl in *. injection H7; injection H8; clear H7 H8; intros H7 H8. assert (shareTreeEq x1 (union_tree x x0)). rewrite <- H7. apply shareTreeEq_sym. apply mkCanon_eq. assert (shareTreeEq (Leaf false) (intersect_tree x x0)). rewrite <- H8. apply shareTreeEq_sym. apply mkCanon_eq. destruct H0. clear H7 H8 H0. destruct o1; try discriminate. subst x. destruct o2; try discriminate. red. exists (Some (merge_token l l0)); simpl. clear c c0. revert n x0 x1 c1 H4 l0 H5 H6 H H1. induction l; simpl; intros. destruct l0; simpl in *. subst x0. invert_ord; discriminate. destruct b; simpl in *. subst x0; simpl in *. invert_ord; discriminate. subst x0. rewrite H6; split; auto. apply canonicalUnique; auto. simpl in *; intuition. destruct a. elimtype False; injection H4; clear. induction l; simpl; intros; destruct_bool; auto; discriminate. destruct l0; simpl in *; subst x0. rewrite union_commute in H; simpl in H. split; auto. 2: congruence. apply canonicalUnique; simpl; auto. destruct b; simpl in *. destruct n. elimtype False; injection H6; clear. induction l0; simpl; intros; destruct_bool; auto; discriminate. destruct x1; destruct_bool; invert_ord; try discriminate. clear -H4 H10 H11. elimtype False. revert H4 l0 H10 H11; induction l; simpl; intros. destruct l0; simpl in *; invert_ord; try discriminate. destruct b; try discriminate. clear -H8; induction l0; simpl in *; invert_ord; auto; discriminate. destruct l0; simpl in *; invert_ord; try discriminate. destruct a; simpl in *; invert_ord; try discriminate. rewrite union_commute in H8. simpl in *. clear -H8; induction l; simpl in *; invert_ord; auto; discriminate. destruct a; simpl in *. injection H4; clear; induction l; simpl; intros; destruct_bool; auto; discriminate. destruct b; invert_ord; try discriminate. apply IHl with l0; auto. replace x1_1 with (Leaf true). assert (c12 : canonicalTree x1_2) by (simpl in *; intuition). destruct (IHl n (interpBools l0) x1_2 c12 H4 l0); auto. rewrite H; auto. apply canonicalUnique; simpl; auto. simpl in *; intuition. destruct x1; destruct_bool; invert_ord; try discriminate. clear -H4 H9 H10. elimtype False. revert H4 l0 H9 H10; induction l; simpl; intros. destruct l0; simpl in *; invert_ord; try discriminate. destruct l0; simpl in *; invert_ord; try discriminate. destruct a; invert_ord; discriminate. destruct a; invert_ord; try discriminate. destruct b; try discriminate. apply IHl with l0; auto. replace x1_1 with (Leaf false). assert (c12 : canonicalTree x1_2) by (simpl in *; intuition). destruct (IHl n (interpBools l0) x1_2 c12 H4 l0); auto. rewrite H; auto. apply canonicalUnique; simpl; auto. simpl in *; intuition. Qed. (* Now we take the previous series of results about manipulating size 1 tokens and generalize them to tokens of arbitrary size by simple induction arguments. We usually use the associativity of join to combine results from the induction hypothesis with results obtained from one of the previous lemmas. *) Lemma splitToken : forall fac x n, isTokenFactory fac x -> { fac':t & {tok:t | isTokenFactory fac' (n+x) /\ isToken tok n /\ join fac' tok fac}}. Proof. intros fac x n; revert fac x; induction n. simpl; intros. exists fac. exists bot. split; auto. split. rewrite identityToken; auto. split; auto with ba. intros. destruct (IHn fac x H) as [fac1 [tok1 [? [? ?]]]]. destruct (splitToken1 fac1 (n+x)%nat H0) as [fac2 [tok2 [? [? ?]]]]. destruct (join_assoc _ _ _ _ _ H5 H2) as [tok' [? ?]]. exists fac2; exists tok'; split; auto. split; auto. destruct n. rewrite identityToken in H1. subst tok1. replace tok' with tok2; auto. destruct H6. rewrite lub_bot in H6; auto. apply mergeToken1 with tok2 tok1; auto. Qed. Lemma absorbToken : forall fac x n, { fac':t & {tok:t | isTokenFactory fac' (n+x) /\ isToken tok n /\ join fac' tok fac}} -> isTokenFactory fac x. Proof. intros fac x n; revert fac x; induction n; simpl; intros fac x [fac' [tok' [? [? ?]]]]. replace fac with fac'; auto. rewrite identityToken in H0. subst tok'. destruct H1. rewrite lub_bot in H1; auto. destruct n; simpl in *. apply absorbToken1; exists fac'; exists tok'; auto. destruct (unmergeToken1 tok' n H0) as [tok1 [tok2 [? [? ?]]]]. apply (saf_com ba_saf) in H1. simpl in H4. destruct (saf_assoc ba_saf _ _ _ _ _ H4 H1) as [fac'' [? ?]]. assert (isTokenFactory fac'' (S x)). apply IHn; exists fac'; exists tok2. split. replace (S (n + (S x))) with (S (S (n+x))); auto. split; auto. apply (saf_com ba_saf); auto. apply absorbToken1; exists fac''; exists tok1; split; auto. split; auto. apply (saf_com ba_saf); auto. Qed. Lemma unmergeToken : forall tok n1 n2, isToken tok (n1 + n2) -> { tok1:t & { tok2:t & isToken tok1 n1 /\ isToken tok2 n2 /\ join tok1 tok2 tok }}. Proof. intros tok n1; revert tok; induction n1; simpl; intros. exists bot; exists tok; split. rewrite identityToken; auto. split; auto. split; auto with ba. destruct n1; simpl in *. destruct n2; simpl in *. exists tok; exists bot; split; auto. split. rewrite identityToken; auto. split; auto with ba. apply (unmergeToken1 tok n2 H). destruct (unmergeToken1 tok (n1+n2)%nat H) as [tok1 [tok2 [? [? ?]]]]. destruct (IHn1 tok2 n2) as [tok3 [tok4 [? [? ?]]]]; auto. simpl in H2. apply (saf_com ba_saf) in H2. destruct (saf_assoc ba_saf _ _ _ _ _ H5 H2) as [tok' [? ?]]. apply (saf_com ba_saf) in H7. destruct (saf_assoc ba_saf _ _ _ _ _ H6 H7) as [tok'' [? ?]]. exists tok''; exists tok4. split. apply (mergeToken1 tok1 n1 tok3); auto. split; auto. apply (saf_com ba_saf); auto. Qed. Lemma mergeToken : forall tok1 n1 tok2 n2 tok', isToken tok1 n1 -> isToken tok2 n2 -> join tok1 tok2 tok' -> isToken tok' (n1+n2). Proof. intros. destruct n2. rewrite identityToken in H0. subst tok2. replace tok' with tok1. replace (n1 + 0)%nat with n1 by omega. auto. destruct H1. rewrite lub_bot in H1; auto. revert tok1 tok2 tok' n2 H H0 H1. induction n1; simpl; intros. rewrite identityToken in H. subst tok1. replace tok' with tok2; auto. destruct H1. rewrite lub_commute in H1. rewrite lub_bot in H1; auto. destruct n1; simpl in *. apply mergeToken1 with tok1 tok2; auto. destruct (unmergeToken1 tok1 n1 H) as [tok11 [tok12 [? [? ?]]]]. simpl in H4. destruct (saf_assoc ba_saf _ _ _ _ _ H4 H1) as [tok'' [? ?]]. apply mergeToken1 with tok11 tok''; auto. apply IHn1 with tok12 tok2; auto. Qed. End TokenFactory. Definition eq_dec := canonTree_eq_dec. End TreeLattice.