How to prove in K $\vdash_{p \rightarrow \lozenge \square p} (\square p \rightarrow \lozenge p)$?

Let us denote $$C$$ the modal system obtained by adding the axiom $$\alpha \rightarrow \lozenge \square \alpha$$ to the axiom $$K$$ and all the propositional tautologies.

As said in the title, I'm looking for a K-proof for $$\vdash_C (\square p \rightarrow \lozenge p),$$ but also for $$\vdash_C (\lozenge p \rightarrow \square p).$$

I know these proofs should exist since a Kripke frame verifies the formula $$p \rightarrow \lozenge \square p$$ if and only if it verifies $$(1) \ \ \forall x ( \exists y : (x \mathrel{R} y) \text{ and } (y \mathrel{R} z \Rightarrow z = x) ).$$

It particular $$(1)$$ implies that the frame is serial ( i.e. $$\forall x (\exists y : x \mathrel{R} y)$$), that is $$\square p \rightarrow \lozenge p$$ is true, and that the frame is functional ( i.e. ($$x \mathrel{R} y \text{ and } x \mathrel{R} z) \Rightarrow y =z$$), that is $$\lozenge p \rightarrow \square p$$ is true.

Thank you for any answer !

(For the first): Consider the set up where $$\neg p$$ holds at the actual world and where no world is accessible from that world. Then the lhs of your sequent evaluates as true, and the right false ... (since $$\Box p$$ is vacuously true, and $$\Diamond p$$ is false).
(For the second): Consider the two-world set-up where in the actual self-accessible world $$\neg p$$, and there is one other accessible world where $$p$$. The lhs of your sequent evaluates as true, and the right false ...
• I might be mistaken, but I think we can't deduct $p$ from $\square p$ unless we are working with reflexive Kripke frames, which is not the case in general. – L.DeR Dec 13 '18 at 16:15
• Agree on nomenclature of en.wikipedia.org/wiki/Kripke_semantics Then K is sound w.r.t. the inferences valid in every K frame, so in particular if $\alpha \vdash_K \beta$, then given any K frame, and any valuation of the relevant atoms in that frame, if $\alpha$ comes out true, so does $\beta$. So it suffices to refute $\alpha \vdash_K \beta$ to find one K frame and one valuation on that frame which makes $\alpha$ true and $\beta$ false. No? – Peter Smith Dec 13 '18 at 23:14
• I'd have said "Let C be the modal system you get by adding to K all axioms of the form $\alpha \to \Diamond\Box\alpha$. Then how do we show $\vdash_C \Box p \to \Diamond p$, etc." [I've plucked the label "C" out of the air -- I don't know off-hand if there is a label already in use.] – Peter Smith Dec 14 '18 at 10:42