(* * Copyright (c) 2009, Andrew Appel, Robert Dockins and Aquinas Hobor. * *) Require Import base. Require Import knot. Require Import sepalg. Require Import sepalg_generators. Require Import sepalg_functors. Require Import knot_sa. Require Import knot_lemmas. (* This file specializes knot and knot_sa to have T = Prop *) Open Local Scope nat_scope. Module Type TY_FUNCTOR_PROP. Parameter F : Type -> Type. Parameter fmap : forall A B, (A -> B) -> F A -> F B. Implicit Arguments fmap [A B]. Axiom fmap_id : forall A, fmap (id A) = id (F A). Axiom fmap_comp : forall A B C (f:B -> C) (g:A -> B), fmap f oo fmap g = fmap (f oo g). Parameter other : Type. End TY_FUNCTOR_PROP. Module Type TY_FUNCTOR_SA_PROP. Declare Module TF:TY_FUNCTOR_PROP. Import TF. Parameter F_sa : forall A, sepalg A -> sepalg (F A). Implicit Arguments F_sa. Axiom fmap_hom : forall A B (sa1: sepalg A) (sa2: sepalg B) (f:A->B), join_hom f -> join_hom (H:=F_sa sa1) (H0:=F_sa sa2) (fmap f). Axiom F_preserves_unmaps : preserves_unmaps F F_sa fmap. Axiom F_identities : forall A B (saA:sepalg A) (saB:sepalg B) (f:A->B) x, @identity _ (F_sa saB) (fmap f x) -> @identity _ (F_sa saA) x. End TY_FUNCTOR_SA_PROP. Module Type KNOT_PROP. Declare Module TF:TY_FUNCTOR_PROP. Import TF. Parameter knot : Type. Definition predicate := (knot * other) -> Prop. Parameter squash : (nat * F predicate) -> knot. Parameter unsquash : knot -> (nat * F predicate). Definition level (x:knot) : nat := fst (unsquash x). Definition approx (n:nat) (p:predicate) : predicate := fun w => level (fst w) < n /\ p w. Axiom squash_unsquash : forall x, squash (unsquash x) = x. Axiom unsquash_squash : forall n x', unsquash (squash (n,x')) = (n,fmap (approx n) x'). 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_unage (k:knot) := let (n,f) := unsquash k in squash (S n,f). End KNOT_PROP. Module Type KNOT_SA_PROP. Declare Module TFSA:TY_FUNCTOR_SA_PROP. Declare Module K:KNOT_PROP with Module TF:=TFSA.TF. Import TFSA.TF. Import TFSA. Import K. Parameter knot_sa : sepalg knot. Existing Instance knot_sa. Definition nat_F_sa : sepalg (nat * F predicate) := sa_prod (sa_equiv nat) (F_sa (sa_fun _ (sa_equiv Prop))). Existing Instance nat_F_sa. Axiom join_unsquash : forall x1 x2 x3, join x1 x2 x3 = join (unsquash x1) (unsquash x2) (unsquash x3). Axiom age_join1 : forall x y z x' : knot, join x y z -> knot_age x x' -> exists y' : knot, exists z' : knot, join x' y' z' /\ knot_age y y' /\ knot_age z z'. Axiom age_join2 : forall x y z z' : knot, join x y z -> knot_age z z' -> exists x' : knot, exists y' : knot, join x' y' z' /\ knot_age x x' /\ knot_age y y'. Axiom unage_join1 : forall x x' y' z', join x' y' z' -> knot_age x x' -> exists y, exists z, join x y z /\ knot_age y y' /\ knot_age z z'. Axiom unage_join2 : forall z x' y' z', join x' y' z' -> knot_age z z' -> exists x, exists y, join x y z /\ knot_age x x' /\ knot_age y y'. Axiom unage_identity : forall x z, knot_age x z -> identity z -> identity x. End KNOT_SA_PROP. (* Coercion *) Module TyFunctorProp2TyFunctor (TF : TY_FUNCTOR_PROP) <: TY_FUNCTOR. (* Export TFP. Does not seem to work? *) Definition F := TF.F. Definition fmap := TF.fmap. Implicit Arguments fmap [A B]. Definition fmap_id := TF.fmap_id. Definition fmap_comp := TF.fmap_comp. Definition T: Type := Prop. Definition T_bot : T := False. Definition other := TF.other. End TyFunctorProp2TyFunctor. Module KnotProp (TF':TY_FUNCTOR_PROP) : KNOT_PROP with Module TF:=TF'. Module TF := TF'. Module TF_G := TyFunctorProp2TyFunctor(TF). Module Knot_G := Knot(TF_G). Import TF. Definition knot : Type := Knot_G.knot. Definition predicate := (knot * other) -> Prop. Definition squash : (nat * F predicate) -> knot := Knot_G.squash. Definition unsquash : knot -> (nat * F predicate) := Knot_G.unsquash. Definition level (x:knot) : nat := fst (unsquash x). Definition approx (n:nat) (p:predicate) : predicate := fun w => level (fst w) < n /\ p w. Lemma squash_unsquash : forall x, squash (unsquash x) = x. Proof. apply Knot_G.squash_unsquash. Qed. Lemma unsquash_squash : forall n x', unsquash (squash (n,x')) = (n,fmap (approx n) x'). Proof. replace approx with Knot_G.approx. apply Knot_G.unsquash_squash. extensionality n p w. unfold approx, Knot_G.approx, TF_G.T_bot. case (le_gt_dec n (Knot_G.level (@fst Knot_G.knot TF_G.other w))); intro; apply prop_ext; firstorder. unfold level, unsquash, Knot_G.level, TF_G.F, predicate, Knot_G.predicate, knot, TF_G.T, TF_G.other in *. omega. 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. Definition knot_unage (k:knot) := let (n,f) := unsquash k in squash (S n,f). End KnotProp. (* Coercion *) Module KnotProp2Knot (TF' : TY_FUNCTOR_PROP) (K : KNOT_PROP with Module TF := TF') <: KNOT. Module TF := TyFunctorProp2TyFunctor(K.TF). Import TF. Definition knot : Type := K.knot. Definition predicate := (knot * other) -> T. Definition squash : (nat * F predicate) -> knot := K.squash. Definition unsquash : knot -> (nat * F predicate) := K.unsquash. Definition level (x:knot) : nat := fst (unsquash x). Definition approx (n:nat) (p:predicate) : predicate := fun w => if le_gt_dec n (level (fst w)) then T_bot else p w. Lemma squash_unsquash : forall x, squash (unsquash x) = x. Proof. apply K.squash_unsquash. Qed. Lemma unsquash_squash : forall n x', unsquash (squash (n,x')) = (n,fmap (approx n) x'). Proof. replace approx with K.approx. apply K.unsquash_squash. extensionality n p w. unfold approx, K.approx, TF.T_bot. case (le_gt_dec n (level (@fst knot other w))); intro; apply prop_ext; firstorder. unfold level, unsquash, K.level, TF.F, predicate, K.predicate, knot, TF.T, TF.other in *. elimtype False. omega. 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. Definition knot_unage (k:knot) := let (n,f) := unsquash k in squash (S n,f). End KnotProp2Knot. Module TyFunctorSaProp2TyFunctorSa (TF' : TY_FUNCTOR_SA_PROP) <: TY_FUNCTOR_SA. Module TF <: TY_FUNCTOR := TyFunctorProp2TyFunctor (TF'.TF). Import TF. Definition F_sa := TF'.F_sa. Definition fmap_hom := TF'.fmap_hom. Definition T_sa : sepalg T := sa_equiv T. Existing Instance T_sa. Lemma T_bot_identity : identity T_bot. Proof. firstorder. Qed. Definition F_preserves_unmaps := TF'.F_preserves_unmaps. Definition F_identities := TF'.F_identities. End TyFunctorSaProp2TyFunctorSa. Module KnotSaProp (TFSA':TY_FUNCTOR_SA_PROP) (K':KNOT_PROP with Module TF:=TFSA'.TF) : KNOT_SA_PROP with Module TFSA:=TFSA' with Module K:=K'. Module TFSA <: TY_FUNCTOR_SA_PROP := TFSA'. Module K <: KNOT_PROP with Module TF:=TFSA'.TF := K'. Import TFSA.TF. Import TFSA. Import K. Module TFSA_G := TyFunctorSaProp2TyFunctorSa(TFSA'). Module K_G <: KNOT with Module TF := TFSA_G.TF := KnotProp2Knot TFSA'.TF K'. Module KnotSa_G := KnotSa TFSA_G K_G. Definition knot_sa : sepalg knot := KnotSa_G.knot_sa. Definition nat_F_sa : sepalg (nat * F predicate) := sa_prod (sa_equiv nat) (F_sa (sa_fun _ (sa_equiv Prop))). Existing Instance nat_F_sa. Lemma join_unsquash : forall x1 x2 x3, join x1 x2 x3 = join (unsquash x1) (unsquash x2) (unsquash x3). Proof. apply KnotSa_G.join_unsquash. Qed. Definition age_join1 := KnotSa_G.age_join1. Definition age_join2 := KnotSa_G.age_join2. Definition unage_join1 := KnotSa_G.unage_join1. Definition unage_join2 := KnotSa_G.unage_join2. Definition unage_identity := KnotSa_G.unage_identity. End KnotSaProp. Module KnotProp_Lemmas (K:KNOT_PROP). Import K. Import K.TF. Module K' := KnotProp2Knot(K.TF)(K). Module KL := Knot_Lemmas(K'). Lemma well_founded_age : well_founded (transp knot knot_age). Proof. apply KL.well_founded_age. Qed. Lemma unsquash_inj : forall k1 k2, unsquash k1 = unsquash k2 -> k1 = k2. Proof. intros. rewrite <- (squash_unsquash k1). rewrite <- (squash_unsquash k2). rewrite H. trivial. Qed. Implicit Arguments unsquash_inj. Lemma squash_surj : forall k, exists n, exists Fp, squash (n, Fp) = k. Proof. intros. remember (unsquash k). destruct p. exists n. exists f. rewrite Heqp. rewrite squash_unsquash. trivial. Qed. Lemma unsquash_approx : forall k n Fp, unsquash k = (n, Fp) -> Fp = fmap (approx n) Fp. Proof. intros. generalize H; intro. rewrite <- (squash_unsquash k) in H. rewrite H0 in H. rewrite unsquash_squash in H. inversion H. rewrite H2. symmetry. trivial. Qed. Implicit Arguments unsquash_approx. Lemma approx_approx1 : forall m n, approx n = approx n oo approx (m+n). Proof. intros. extensionality p x; destruct x as [k o]. unfold approx, compose; simpl. apply prop_ext; intuition. Qed. Lemma approx_approx2 : forall m n, approx n = approx (m+n) oo approx n. Proof. intros. extensionality p x; destruct x as [k o]. unfold approx, compose; simpl. apply prop_ext; intuition. Qed. (* These are provided since sometimes it is tedious to break things out; they are not interesting except as engineering artifacts. *) Lemma unsquash_squash_unfolded : forall nf, unsquash (squash nf) = (fst nf, fmap (approx (fst nf)) (snd nf)). Proof. intros. destruct nf. apply unsquash_squash. Qed. Lemma unsquash_approx_unfolded : forall k, unsquash k = (fst (unsquash k), fmap (approx (fst (unsquash k))) (snd (unsquash k))). Proof. intros. case_eq (unsquash k); intros. simpl. apply injective_projections; simpl; trivial. apply (unsquash_approx H). Qed. Lemma knot_unage_correct : forall k, knot_age (knot_unage k) k. Proof. intros; unfold knot_unage, knot_age, knot_age1. case_eq (unsquash k); intros. rewrite unsquash_squash; simpl. f_equal. apply unsquash_inj. rewrite unsquash_squash. rewrite H. f_equal. change (fmap (approx n) (fmap (approx (S n)) f)) with ((fmap (approx n) oo (fmap (approx (S n)))) f). rewrite fmap_comp. rewrite <- (approx_approx1 1). rewrite <- (unsquash_approx H); auto. Qed. End KnotProp_Lemmas.