infinite.v 3.53 KB
Newer Older
1 2
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
Johannes Kloos's avatar
Johannes Kloos committed
3
From stdpp Require Import pretty fin_collections relations prelude gmap.
4

5 6 7 8 9 10 11
(** The class [Infinite] axiomatizes types with infinitely many elements
by giving an injection from the natural numbers into the type. It is mostly
used to provide a generic [fresh] algorithm. *)
Class Infinite A :=
  { inject: nat  A;
    inject_injective:> Inj (=) (=) inject }.

12 13 14
Instance string_infinite: Infinite string := {| inject := λ x, "~" +:+ pretty x |}.
Instance nat_infinite: Infinite nat := {| inject := id |}.
Instance N_infinite: Infinite N := {| inject_injective := Nat2N.inj |}.
15
Instance positive_infinite: Infinite positive := {| inject_injective := SuccNat2Pos.inj |}.
16
Instance Z_infinite: Infinite Z := {| inject_injective := Nat2Z.inj |}.
17

18 19 20 21 22
Instance option_infinite `{Infinite A}: Infinite (option A) := {| inject := Some  inject |}.
Program Instance list_infinite `{Inhabited A}: Infinite (list A) :=
  {| inject := λ i, replicate i inhabitant |}.
Next Obligation.
Proof.
23 24
  intros A * i j Heqrep%(f_equal length).
  rewrite !replicate_length in Heqrep; done.
25 26
Qed.

27 28
(** * Fresh elements *)
Section Fresh.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
  Context `{FinCollection A C, Infinite A, !RelDecision (@{C})}.
30

31
  Definition fresh_generic_body (s : C) (rec :  s', s'  s  nat  A) (n : nat) : A :=
32 33
    let cand := inject n in
    match decide (cand  s) with
34
    | left H => rec _ (subset_difference_elem_of H) (S n)
35 36 37
    | right _ => cand
    end.

38 39
  Definition fresh_generic_fix : C  nat  A :=
    Fix (wf_guard 20 collection_wf) (const (nat  A)) fresh_generic_body.
40

41 42
  Lemma fresh_generic_fixpoint_unfold s n:
    fresh_generic_fix s n = fresh_generic_body s (λ s' _, fresh_generic_fix s') n.
43
  Proof.
44 45
    refine (Fix_unfold_rel _ _ (const (pointwise_relation nat (=))) _ _ s n).
    intros s' f g Hfg i. unfold fresh_generic_body. case_decide; naive_solver.
46 47
  Qed.

48 49 50
  Lemma fresh_generic_fixpoint_spec s n :
     m, n  m  fresh_generic_fix s n = inject m  inject m  s 
          i, n  i < m  inject i  s.
51 52
  Proof.
    revert n.
53
    induction s as [s IH] using (well_founded_ind collection_wf); intros n.
54
    setoid_rewrite fresh_generic_fixpoint_unfold; unfold fresh_generic_body.
55 56 57
    destruct decide as [Hcase|Hcase]; [|by eauto with omega].
    destruct (IH _ (subset_difference_elem_of Hcase) (S n))
      as (m & Hmbound & Heqfix & Hnotin & Hinbelow).
58
    exists m; repeat split; auto with omega.
59 60 61 62 63 64
    - rewrite not_elem_of_difference, elem_of_singleton in Hnotin.
      destruct Hnotin as [?|?%inject_injective]; auto with omega.
    - intros i Hibound.
      destruct (decide (i = n)) as [<-|Hneq]; [by auto|].
      assert (inject i  s  {[inject n]}) by auto with omega.
      set_solver.
65 66
  Qed.

67
  Instance fresh_generic : Fresh A C := λ s, fresh_generic_fix s 0.
68

69
  Instance fresh_generic_spec : FreshSpec A C.
70 71 72
  Proof.
    split.
    - apply _.
73 74 75 76 77
    - intros X Y HeqXY. unfold fresh, fresh_generic.
      destruct (fresh_generic_fixpoint_spec X 0)
        as (mX & _ & -> & HnotinX & HbelowinX).
      destruct (fresh_generic_fixpoint_spec Y 0)
        as (mY & _ & -> & HnotinY & HbelowinY).
78
      destruct (Nat.lt_trichotomy mX mY) as [case|[->|case]]; auto.
79 80 81 82 83
      + contradict HnotinX. rewrite HeqXY. apply HbelowinY; omega.
      + contradict HnotinY. rewrite <-HeqXY. apply HbelowinX; omega.
    - intros X. unfold fresh, fresh_generic.
      destruct (fresh_generic_fixpoint_spec X 0)
        as (m & _ & -> & HnotinX & HbelowinX); auto.
84 85
  Qed.
End Fresh.