Commit bdfa43b9 authored by Ralf Jung's avatar Ralf Jung
Browse files

show that there are infinitely many locations

parent 5c07c3be
Pipeline #17105 passed with stage
in 13 minutes and 25 seconds
......@@ -11,6 +11,20 @@ Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
Instance loc_countable : Countable loc.
Proof. by apply (inj_countable' loc_car (λ i, {| loc_car := i |})); intros []. Qed.
Program Definition loc_infinite : Infinite loc := {|
infinite_fresh l := {| loc_car := infinite_fresh (loc_car <$> l) |}
Next Obligation.
intros xs Hfresh. unfold fresh in Hfresh.
eapply (infinite_is_fresh (loc_car <$> xs)).
eapply elem_of_list_fmap. eexists. split; last done.
Next Obligation.
intros xs ys Hperm. unfold fresh. f_equal.
eapply infinite_fresh_Permutation. rewrite Hperm //.
Definition loc_add (l : loc) (off : Z) : loc :=
{| loc_car := loc_car l + off|}.
  • This looks like quite a detour, much easier to just use inj_infinite.

  • Ah, I didn't see that. Thanks!

    I wonder if there is a good way to make use of this down in fresh_locs_fresh.

  • In principle we could reuse the fresh function that you get from Infinte loc for defining fresh_locs, but the spec does not say anything about also all bigger locations being fresh.

    That said, I don't think we should even reuse fresh, it's kind of bad practice to rely on the specific implementation that's used there.

Supports Markdown
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