(* * Copyright (c) 2009, Andrew Appel, Robert Dockins and Aquinas Hobor. * *) (* Knots with all the bells and whistles *) Require Import base. Open Local Scope nat_scope. Module Type TY_FUNCTOR_BELLS. Parameter F : Type -> Type -> Type. Parameter bimap : forall A B C D, (A -> B) -> (C -> D) -> F B C -> F A D. Implicit Arguments bimap [A B C D]. Axiom bimap_id : forall A B, bimap (id A) (id B) = id (F A B). Axiom bimap_comp : forall A B C D E F (f:B -> C) (g:A -> B) (s:F -> E) (t:E -> D), bimap s f oo bimap t g = bimap (t oo s) (f oo g). Parameter other : Type. Parameter Rel : forall A B, F A B -> F A B -> Prop. Parameter Rel_bimap : forall A B C D (f:A->B) (s:C->D) x y, Rel D A x y -> Rel C B (bimap s f x) (bimap s f y). End TY_FUNCTOR_BELLS. Module Type KNOT_BELLS. Declare Module TF:TY_FUNCTOR_BELLS. Import TF. Parameter knot:Type. Parameter hered : (knot * other -> Prop) -> Prop. Definition predicate := { p:knot * other -> Prop | hered p }. Parameter squash : (nat * F predicate predicate) -> knot. Parameter unsquash : knot -> (nat * F predicate predicate). Definition level (x:knot) : nat := fst (unsquash x). Parameter approx : nat -> predicate -> predicate. Axiom squash_unsquash : forall k:knot, squash (unsquash k) = k. Axiom unsquash_squash : forall (n:nat) (f:F predicate predicate), unsquash (squash (n,f)) = (n, bimap (approx n) (approx n) f). Axiom approx_spec : forall n p ko, proj1_sig (approx n p) ko = (level (fst ko) < n /\ proj1_sig p ko). Definition knot_age1 (k:knot) : option knot := match unsquash k with | (O,_) => None | (S n,x) => Some (squash (n,x)) end. Definition knot_age := fun x y => knot_age1 x = Some y. Definition knot_rel (k1 k2:knot) := let (n,f) := unsquash k1 in let (n',f') := unsquash k2 in n = n' /\ Rel predicate predicate f f'. Axiom hered_spec : forall p, hered p = (forall k k' k'' o, knot_age k k' -> knot_rel k' k'' -> p (k,o) -> p (k'',o)). End KNOT_BELLS. Module KnotBells (TF':TY_FUNCTOR_BELLS) : KNOT_BELLS with Module TF:=TF'. Module TF:=TF'. Import TF. Definition sinv_prod X := prod X (F X X * other -> Prop). Definition guppy_sig := (fun T:Type => T * (F T T * other -> Prop) -> Prop). Definition guppy_ty := sigT guppy_sig. Definition guppy_step_ty (Z:guppy_ty) : Type := (sig (fun (x:sinv_prod (projT1 Z)) => projT2 Z x)). Definition guppy_age (Z:guppy_ty) (x:guppy_step_ty Z) : projT1 Z := fst (proj1_sig x). Definition guppy_unage (Z:guppy_ty) (H:forall t, projT2 Z (t,fun _ => False)) (x:projT1 Z) : guppy_step_ty Z := exist (fun z => projT2 Z z) (x, fun _ => False) (H x). Definition guppy_step_prop (Z:guppy_ty) (xf:sinv_prod (guppy_step_ty Z)) := forall (k:F (guppy_step_ty Z) (guppy_step_ty Z)) (k':F (projT1 Z) (projT1 Z)) (o:other) H, snd xf (k,o) -> Rel (projT1 Z) (projT1 Z) (bimap (guppy_unage Z H) (guppy_age Z) k) k' -> snd (proj1_sig (fst xf)) (k',o). Definition guppy_step (Z:guppy_ty) : guppy_ty := existT guppy_sig (guppy_step_ty Z) (guppy_step_prop Z). Definition guppy_base : guppy_ty := existT guppy_sig unit (fun _ => True). Fixpoint guppy (n:nat) : guppy_ty := match n with | 0 => guppy_base | S n' => guppy_step (guppy n') end. Definition sinv (n:nat) : Type := projT1 (guppy n). Definition sinv_prop (n:nat) : prod (sinv n) (F (sinv n) (sinv n) * other -> Prop) -> Prop := projT2 (guppy n). Fixpoint floor (m:nat) (n:nat) (p:sinv (m+n)) : sinv n := match m as m' return forall (p : sinv (m'+n)), sinv n with | O => fun p => p | S m' => fun p => floor m' n (fst (proj1_sig p)) end p. Definition knot := { n:nat & F (sinv n) (sinv n) }. Definition sinv_age n : sinv (S n) -> sinv n := guppy_age (guppy n). Program Definition sinv_unage n : sinv n -> sinv (S n) := guppy_unage (guppy n) _. Next Obligation. revert t; induction n; simpl; auto. repeat intro. simpl in *. inv H0. Qed. Definition F_sinv n := F (sinv n) (sinv n). Definition age1 (k:knot) : option knot := match k with | existT 0 f => None | existT (S m) f => Some (existT F_sinv m (bimap (sinv_unage m) (sinv_age m) f)) end. Inductive knot_rel_inner : knot -> knot -> Prop := | intro_krel : forall n (f f':F_sinv n), Rel _ _ f f' -> knot_rel_inner (existT (F_sinv) n f) (existT (F_sinv) n f'). Definition hered (p:knot * other -> Prop) : Prop := forall k k' k'' o, age1 k = Some k' -> knot_rel_inner k' k'' -> p (k,o) -> p (k'',o). Definition predicate := { p:knot * other -> Prop | hered p }. Definition app_sinv (n:nat) (p:sinv (S n)) (x:F_sinv n * other) := snd (proj1_sig p) x. Section stratifies. Variable Q:knot * other -> Prop. Variable HQ:hered Q. Fixpoint stratifies (n:nat) : sinv n -> Prop := match n as n' return sinv n' -> Prop with | 0 => fun _ => True | S n' => fun (p:sinv (S n')) => stratifies n' (fst (proj1_sig p)) /\ forall (k:F_sinv n') (o:other), snd (proj1_sig p) (k,o) <-> Q (existT F_sinv n' k,o) end. Lemma stratifies_unique : forall n p1 p2, stratifies n p1 -> stratifies n p2 -> p1 = p2. Proof. induction n; simpl; intuition. destruct p1; destruct p2; auto. destruct p1; destruct p2. simpl in *; fold guppy in *. cut (x = x0). intros. revert p p0 H2 H3. rewrite <- H0. intros. replace p0 with p by (apply proof_irr); auto. destruct x; destruct x0; simpl in *. apply injective_projections; simpl. apply IHn; auto. extensionality; intros. simpl in *. destruct x as [x o]. destruct (H2 x o); destruct (H3 x o). apply prop_ext; intuition. Qed. Definition stratify (n:nat) : { x:sinv n | stratifies n x }. Proof. induction n. exists tt; simpl; exact I. assert (HX: projT2 (guppy n) (projT1 IHn, fun v : F_sinv n * other => Q (existT F_sinv n (fst v),snd v))). destruct n. simpl; exact I. simpl; intros. destruct IHn; simpl. simpl in s; destruct s. destruct x; simpl in *; fold guppy in *. destruct x; simpl in *. hnf; simpl; intros. rewrite H0. eapply HQ. 3: apply H2. simpl; reflexivity. constructor; auto. unfold sinv_unage. replace (sinv_unage_obligation_1 n) with H1. auto. apply proof_irr. exists ((exist (fun x => projT2 (guppy n) x) ( projT1 IHn, fun v:F_sinv n * other => Q (existT (F_sinv) n (fst v),snd v) ) HX)). simpl; split. destruct IHn; auto. unfold app_sinv; simpl; intros. split; trivial. Qed. End stratifies. Lemma decompose_nat : forall (x y:nat), { m:nat & y = (m + S x) } + { ge x y }. Proof. intros x y; revert x; induction y; simpl; intros. right; auto with arith. destruct (IHy x) as [[m H]|H]. left; exists (S m); omega. destruct (eq_nat_dec x y). left; exists O; omega. right; omega. Qed. Definition unstratify (n:nat) (p:sinv n) : knot * other -> Prop := fun w => match w with (existT nw w',o) => match decompose_nat nw n with | inleft (existT m Hm) => snd (proj1_sig (floor m (S nw) (eq_rect n _ p (m + S nw) Hm))) (w',o) | inright H => False end end. Lemma floor_shuffle: forall (m1 n : nat) (p1 : sinv (m1 + S n)) (H1 : (m1 + S n) = (S m1 + n)), floor (S m1) n (eq_rect (m1 + S n) sinv p1 (S m1 + n) H1) = fst (proj1_sig (floor m1 (S n) p1)). Proof. intros. remember (fst (proj1_sig (floor m1 (S n) p1))) as p. fold guppy in *. revert n p1 H1 p Heqp. induction m1; simpl; intros. replace H1 with (refl_equal (S n)) by (apply proof_irr); simpl; auto. assert (m1 + S n = S m1 + n) by omega. destruct p1 as [[p1 f'] Hp1]; simpl in *; fold guppy in *. generalize (IHm1 n p1 H p Heqp). clear. revert Hp1 H1; generalize H. revert p1 f'. rewrite H. simpl; intros. replace H1 with (refl_equal (S (S (m1 + n)))) by (apply proof_irr). simpl. replace H0 with (refl_equal (S (m1+n))) in H2 by (apply proof_irr). simpl in H2. trivial. Qed. Lemma unstratify_hered : forall n p, hered (unstratify n p). Proof. intros. hnf; intros. simpl in H. destruct k. destruct x. discriminate. assert (k' = (existT (F_sinv) x (bimap (sinv_unage x) (sinv_age x) f))). inversion H; auto. subst k'. inv H0. revert H1. unfold unstratify. case_eq (decompose_nat (S x) n); intros. destruct s. case_eq (decompose_nat x n); intros. destruct s. destruct n. elimtype False; omega. assert (S x0 = x1) by omega; subst x1. revert H1. generalize e e0; revert p; rewrite e; intros. rewrite floor_shuffle. replace e1 with (refl_equal (x0 + S (S x))) in H1; simpl eq_rect in H1. 2: apply proof_irr. revert H1. generalize (floor x0 (S (S x)) p). intros [[s' fs] Hs] H1; simpl in *; fold guppy in *. apply Eqdep_dec.inj_pair2_eq_dec in H4; auto. subst f1. eapply Hs. simpl; apply H1. apply H5. apply eq_nat_dec. omega. elim H1. Qed. Lemma unstratify_Q : forall n (p:sinv n) Q, stratifies Q n p -> forall (k:knot) (o:other), projT1 k < n -> (unstratify n p (k,o) <-> Q (k,o)). Proof. intros. unfold unstratify. destruct k. destruct (decompose_nat x n). destruct s. simpl in H0. 2: simpl in *; elimtype False; omega. clear H0. revert p H. generalize e. rewrite e. intros. replace e0 with (refl_equal (x0 + S x)) by apply proof_irr. simpl. clear e e0. revert p H. induction x0; simpl; intros. destruct H. auto. destruct H. apply IHx0. auto. Qed. Lemma stratifies_unstratify_more : forall (n m1 m2:nat) (p1:sinv (m1+n)) (p2:sinv (m2+n)), floor m1 n p1 = floor m2 n p2 -> (stratifies (unstratify (m1+n) p1) n (floor m1 n p1) -> stratifies (unstratify (m2+n) p2) n (floor m2 n p2)). Proof. induction n; intuition. split. assert (m2 + S n = S m2 + n) by omega. erewrite <- floor_shuffle. instantiate (1:=H1). replace (unstratify (m2 + S n) p2) with (unstratify (S m2 + n) (eq_rect (m2 + S n) sinv p2 (S m2 + n) H1)). assert (m1 + S n = S m1 + n) by omega. eapply (IHn (S m1) (S m2) (eq_rect (m1 + S n) sinv p1 (S m1 + n) H2)). rewrite floor_shuffle. rewrite floor_shuffle. rewrite H; auto. clear - H0. rewrite floor_shuffle. simpl in H0. destruct H0. clear H0. revert p1 H. generalize H2. rewrite <- H2. intros. replace H0 with (refl_equal (m1 + S n)) by apply proof_irr; auto. clear. revert p2. generalize H1. rewrite H1. intros. replace H0 with (refl_equal (S m2 + n)) by apply proof_irr; auto. intros. simpl. destruct (decompose_nat n (m2 + S n)). destruct s. assert (m2 = x). omega. subst x. replace e with (refl_equal (m2 + S n)). simpl; tauto. apply proof_irr. elimtype False; omega. Qed. Lemma stratify_unstratify : forall n p H, proj1_sig (stratify (unstratify n p) H n) = p. Proof. intros. apply stratifies_unique with (unstratify n p). destruct (stratify _ H n). simpl; auto. clear H. revert p; induction n. simpl; intros; auto. intros. simpl; split. assert (stratifies (unstratify n (fst (proj1_sig p))) n (fst (proj1_sig p))). apply IHn. apply (stratifies_unstratify_more n 0 1 (fst (proj1_sig p)) p). simpl; auto. auto. intros. destruct (decompose_nat n (S n)). destruct s. assert (x = 0) by omega. subst x. simpl. simpl in e. replace e with (refl_equal (S n)) by apply proof_irr. simpl. split; auto. elimtype False; omega. Qed. Definition strat (n:nat) (p:predicate) : sinv n := proj1_sig (stratify (proj1_sig p) (proj2_sig p) n). Definition unstrat (n:nat) (p:sinv n) : predicate := exist hered (unstratify n p) (unstratify_hered n p). Definition squash (x:nat * F predicate predicate) : knot := match x with (n,f) => existT (F_sinv) n (bimap (unstrat n) (strat n) f) end. Definition unsquash (k:knot) : nat * F predicate predicate := match k with existT n f => (n, bimap (strat n) (unstrat n) f) end. Definition level (x:knot) : nat := fst (unsquash x). Program Definition approx (n:nat) (p:predicate) : predicate := fun w => level (fst w) < n /\ p w. Next Obligation. hnf; simpl; intros. intuition. unfold level in *. unfold unsquash in *. destruct k; simpl in H. destruct x; try discriminate. inv H. simpl in H2. inv H0. simpl; omega. destruct p; simpl in *. eapply h; eauto. Qed. Lemma strat_unstrat : forall n, strat n oo unstrat n = id (sinv n). Proof. intros; extensionality p. unfold compose, id. unfold strat, unstrat. simpl. rewrite stratify_unstratify. auto. Qed. Lemma predicate_eq : forall (p1 p2:predicate), proj1_sig p1 = proj1_sig p2 -> p1 = p2. Proof. intros; destruct p1; destruct p2; simpl in H. subst x0. replace h0 with h by apply proof_irr. auto. Qed. Lemma unstrat_strat : forall n, unstrat n oo strat n = approx n. Proof. intros. extensionality. unfold compose. unfold unstrat, strat. unfold approx. apply predicate_eq. simpl. extensionality k. apply prop_ext; intuition. unfold unstratify in H. destruct a. destruct (decompose_nat x0 n). unfold level. simpl. destruct s. omega. elim H. rewrite <- unstratify_Q. apply H. destruct (stratify (proj1_sig x) (proj2_sig x) n); auto. unfold unstratify in H. destruct a; simpl. destruct (decompose_nat x0 n). destruct s; omega. elim H. rewrite unstratify_Q. apply H1. destruct (stratify (proj1_sig x) (proj2_sig x) n); auto. unfold level in H0. destruct a; simpl in *. auto. Qed. Lemma squash_unsquash : forall k, squash (unsquash k) = k. Proof. intros. destruct k; simpl. f_equal. change ((bimap (unstrat x) (strat x) oo (bimap (strat x) (unstrat x))) f = f). rewrite bimap_comp. rewrite strat_unstrat. rewrite bimap_id. auto. Qed. Lemma unsquash_squash : forall n f, unsquash (squash (n,f)) = (n, bimap (approx n) (approx n) f). Proof. intros. unfold unsquash, squash. f_equal. change ((bimap (strat n) (unstrat n) oo (bimap (unstrat n) (strat n))) f = bimap (approx n) (approx n) f). rewrite bimap_comp. rewrite unstrat_strat. auto. Qed. Definition knot_age1 (k:knot) : option knot := match unsquash k with | (O,_) => None | (S n,x) => Some (squash (n,x)) end. Definition knot_age := fun x y => knot_age1 x = Some y. Lemma strat_Sx_unstrat : forall x, sinv_unage x = strat (S x) oo unstrat x. Proof. intros. extensionality k. unfold sinv_unage. generalize (sinv_unage_obligation_1); intro P. unfold guppy_unage. unfold compose, strat, unstrat. simpl. apply stratifies_unique with (unstratify x k). revert k. induction x; simpl; intuition. destruct (decompose_nat 0 0); auto. destruct s; omega. eapply (stratifies_unstratify_more x 0 1). simpl; reflexivity. simpl. simpl in *. destruct (IHx (fst (proj1_sig k))); auto. destruct (decompose_nat x (S x)). destruct s. assert (x0 = 0) by omega; subst x0. simpl in *. replace e with (refl_equal (S x)) by apply proof_irr; auto. omega. destruct (decompose_nat x (S x)). destruct s. assert (x0 = 0) by omega; subst x0. simpl in *. replace e with (refl_equal (S x)) in H by apply proof_irr; auto. elim H. destruct (decompose_nat (S x) (S x)). destruct s; omega. auto. destruct (stratify (unstratify x k) (unstratify_hered x k) (S x)). simpl stratifies in s; case s; intros. simpl stratifies; split; auto. Qed. Lemma strat_unstrat_Sx : forall x, sinv_age x = strat x oo unstrat (S x). Proof. intros. extensionality k. unfold sinv_age, guppy_age. unfold compose. unfold strat, unstrat. simpl. apply stratifies_unique with (unstratify x (fst (proj1_sig k))). revert k; induction x; simpl; auto. intros. split. eapply (stratifies_unstratify_more x 0 1 ). simpl; reflexivity. simpl. apply IHx. intros. destruct (decompose_nat x (S x)). destruct s. assert (x0 = 0) by omega; subst x0. simpl in *. replace e with (refl_equal (S x)) by apply proof_irr; simpl. tauto. elimtype False; omega. destruct (stratify (unstratify (S x) k) (unstratify_hered (S x) k) x). simpl; auto. cut (x0 = (fst (proj1_sig k))); intros. subst x0. eapply (stratifies_unstratify_more x 1 0). simpl; reflexivity. simpl; auto. eapply stratifies_unique. apply s. eapply (stratifies_unstratify_more x 0 1). simpl; reflexivity. simpl. generalize (fst (proj1_sig k) : sinv x). clear. induction x; simpl; intuition. eapply (stratifies_unstratify_more x 0 1). simpl; reflexivity. simpl. apply IHx. destruct (decompose_nat x (S x)). destruct s0. assert (x0 = 0) by omega; subst. simpl in *. replace e with (refl_equal (S x)); simpl; auto. apply proof_irr. omega. destruct (decompose_nat x (S x)). destruct s0. assert (x0 = 0) by omega; subst. simpl in *. replace e with (refl_equal (S x)) in H; simpl; auto. apply proof_irr. elim H. Qed. Lemma knot_age_age1 : forall k k', knot_age k k' <-> age1 k = Some k'. Proof. split; intros. simpl. unfold knot_age in H. unfold knot_age1 in H. unfold unsquash in H. destruct k. destruct x; auto. inv H. unfold age1. f_equal. f_equal. change (bimap (unstrat x) (strat x) (bimap (strat (S x)) (unstrat (S x)) f)) with ((bimap (unstrat x) (strat x) oo bimap (strat (S x)) (unstrat (S x))) f). rewrite bimap_comp. rewrite strat_unstrat_Sx. rewrite strat_Sx_unstrat. auto. hnf; simpl. unfold knot_age1. unfold unsquash; simpl. unfold age1 in H. destruct k. destruct x; auto. inv H. f_equal. f_equal. change (bimap (unstrat x) (strat x) (bimap (strat (S x)) (unstrat (S x)) f)) with ((bimap (unstrat x) (strat x) oo bimap (strat (S x)) (unstrat (S x))) f). rewrite strat_unstrat_Sx. rewrite strat_Sx_unstrat. rewrite bimap_comp. auto. Qed. Definition knot_rel (k1 k2:knot) := let (n,f) := unsquash k1 in let (n',f') := unsquash k2 in n = n' /\ Rel predicate predicate f f'. Lemma hered_spec : forall p, hered p = (forall k k' k'' o, knot_age k k' -> knot_rel k' k'' -> p (k,o) -> p (k'',o)). Proof. intros. apply prop_ext. intuition. eapply H. rewrite <- knot_age_age1. apply H0. destruct k'; destruct k''. unfold knot_rel, unsquash in H1. destruct H1; subst. constructor. apply (Rel_bimap _ _ _ _ (strat x0) (unstrat x0)) in H3. change f with (id _ f). change f0 with (id _ f0). rewrite <- bimap_id. rewrite <- (strat_unstrat x0). rewrite <- bimap_comp. auto. auto. hnf; intros. apply H with k k'; auto. rewrite knot_age_age1; auto. destruct k'; destruct k''. inv H1. simpl. hnf; split; auto. apply Eqdep_dec.inj_pair2_eq_dec in H5; auto. apply Eqdep_dec.inj_pair2_eq_dec in H7; auto. subst. apply Rel_bimap; auto. exact eq_nat_dec. exact eq_nat_dec. Qed. Lemma approx_spec : forall n p k, proj1_sig (approx n p) k = (level (fst k) < n /\ proj1_sig p k). Proof. intros. apply prop_ext. unfold approx; simpl. tauto. Qed. End KnotBells.