How can I construct a proof that the decryption of a certain encrypted file matches a hash? Let's say Alice has file $F$ and she generates key $K$. She widely publishes the $hash(F)$ for identification. She wants to sell the file to Bob. She encrypts the file with $K$ and sends both $E_f = E(F, K)$ and $hash(K)$ to Bob. However, Bob wants to verify that this encrypted file really is the one he has asked to buy.

How can Bob verify that $hash(Dec(E_f, K)) = hash(f)$ knowing only $hash(K)$ and $E_f$? He shouldn't be able to decrypt the file, but should be able to prove that the encrypted file Alice sent, when decrypted, matches the hash, $hash(f)$.

It seems like I might need to use some sort of ZK-proof, but that may not work because the proof would be prohibitively large.

This question may be similar to: Proof that a hash matches an encrypted file, however, knowing only the hash of the key seems to present a different problem.

This could also be looked at as a Proof-of-Knowledge of a key $K$ such that $hash(K)$ matches the one Alice revealed to Bob and $Dec(E_f, K) = hash(f)$.
What you describe is very close to Zero Knowledge Contingent Payment (ZKCP) proposed for exchanging digital goods for bitcoins.

The setting is that Alice has a file $F$ and Bob would pay to have it. However they don't trust each other. So Alice generates a key $k$ and encrypts the file $E_f=E_{K}(F)$ using a cipher $E$, and hashes the key $y=H(K)$. Then she sends $(E_f,y)$ to Bob, along with a proof of knowledge $(F,k)$ such that $c$ is an encryption of $F$ under the key $K$ which satisfies $H(K) = y$. If Bob is satisfied with the proof, he will publish a transaction on the bitcoin network saying that there are some bitcoins locked in an account such that whoever can submit the pre-image of $H(K)$ to the account address can take the coins. 

In your case, you have an additional hash value $z$ of the file published by Alice. It seems that you want Bob to also be able to verify the file matches $z$. In this case, Alice's proof would be a conjunction, i.e. $c$ is an encryption of $F$ under the key $K$ such that $H(K) = y$ AND $z=hash(F)$.  

To do such proof, you would need SNARK (Succinct Non-Interactive Arguments of Knowledge). Conceptually it is simple, the prover shows that some secrets he knows, if computed correctly by some publicly known functions, will produce some values which the verifier knows. However the actual implementation can be quite complicated, and there are some caveats as well regarding the security properties.

A paper that contains more details and is worthy reading: Zero-Knowledge Contingent Payments Revisited: Attacks and Payments for Services by Campanelli et al, published in CCS 2017.