Commit f0b073ee authored by Robbert Krebbers's avatar Robbert Krebbers

Seal `fresh_generic`.

Since `fresh_generic` is too inefficient for all practical purposes, we seal
off its definition. That way, Coq will not accidentally unfold it during
unification or other tactics.

This issue actually occurred in iGPS, as reported by Hai.
parent a99446f9
......@@ -41,7 +41,11 @@ Qed.
various set implementations, e.g. [Pset] and [natset], we have an efficient
implementation of [Fresh], which should always be used. Only for specific set
implementations like [gset], which are not meant to be computationally
efficient in the first place, we make [fresh_generic] an instance. *)
efficient in the first place, we make [fresh_generic] an instance.
Since [fresh_generic] is too inefficient for all practical purposes, we seal
off its definition. That way, Coq will not accidentally unfold it during
unification or other tactics. *)
Section fresh_generic.
Context `{FinCollection A C, Infinite A, !RelDecision (@{C})}.
......@@ -52,12 +56,14 @@ Section fresh_generic.
| right _ => cand
end.
Definition fresh_generic_fix : C nat A :=
Fix (wf_guard 20 collection_wf) (const (nat A)) fresh_generic_body.
Definition fresh_generic_fix_aux :
seal (Fix collection_wf (const (nat A)) fresh_generic_body). by eexists. Qed.
Definition fresh_generic_fix := fresh_generic_fix_aux.(unseal).
Lemma fresh_generic_fixpoint_unfold s n:
fresh_generic_fix s n = fresh_generic_body s (λ s' _, fresh_generic_fix s') n.
Proof.
unfold fresh_generic_fix. rewrite fresh_generic_fix_aux.(seal_eq).
refine (Fix_unfold_rel _ _ (const (pointwise_relation nat (=))) _ _ s n).
intros s' f g Hfg i. unfold fresh_generic_body. case_decide; naive_solver.
Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment