infinite.v 4.68 KB
Newer Older
1
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
2
(* This file is distributed under the terms of the BSD license. *)
3
From stdpp Require Export fin_sets.
4
From stdpp Require Import pretty relations.
5

6
7
8
(** 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. *)
9
10
11
12
Class Infinite A := {
  inject: nat  A;
  inject_injective :> Inj (=) (=) inject;
}.
13

14
15
16
17
(** Instances *)
Program Definition inj_infinite `{Infinite A} {B} (f : A  B) `{!Inj (=) (=) f} :
  Infinite B := {| inject := f  inject |}.

18
19
20
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 |}.
21
Instance positive_infinite: Infinite positive := {| inject_injective := SuccNat2Pos.inj |}.
22
Instance Z_infinite: Infinite Z := {| inject_injective := Nat2Z.inj |}.
23

24
25
26
27
28
29
30
31
Instance option_infinite `{Infinite A} : Infinite (option A) := inj_infinite Some.
Instance sum_infinite_l `{Infinite A} {B} : Infinite (A + B) := inj_infinite inl.
Instance sum_infinite_r {A} `{Infinite B} : Infinite (A + B) := inj_infinite inr.
Instance prod_infinite_l `{Infinite A, Inhabited B} : Infinite (A * B) :=
  inj_infinite (,inhabitant).
Instance prod_infinite_r `{Inhabited A, Infinite B} : Infinite (A * B) :=
  inj_infinite (inhabitant,).

32
33
34
Program Instance list_infinite `{Inhabited A}: Infinite (list A) :=
  {| inject := λ i, replicate i inhabitant |}.
Next Obligation.
35
36
  intros A * i j Heqrep%(f_equal length).
  rewrite !replicate_length in Heqrep; done.
37
38
Qed.

39
(** * Fresh elements *)
40
41
42
43
(** We do not make [fresh_generic] an instance because it leads to overlap. For
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
Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
46
47
48
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. *)
49
Section fresh_generic.
50
  Context `{FinSet A C, Infinite A, !RelDecision (@{C})}.
51

52
  Definition fresh_generic_body (s : C) (rec :  s', s'  s  nat  A) (n : nat) : A :=
53
54
    let cand := inject n in
    match decide (cand  s) with
55
    | left H => rec _ (subset_difference_elem_of H) (S n)
56
57
58
    | right _ => cand
    end.

Robbert Krebbers's avatar
Robbert Krebbers committed
59
  Definition fresh_generic_fix_aux :
60
    seal (Fix set_wf (const (nat  A)) fresh_generic_body). by eexists. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  Definition fresh_generic_fix := fresh_generic_fix_aux.(unseal).
62

63
64
  Lemma fresh_generic_fixpoint_unfold s n:
    fresh_generic_fix s n = fresh_generic_body s (λ s' _, fresh_generic_fix s') n.
65
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
    unfold fresh_generic_fix. rewrite fresh_generic_fix_aux.(seal_eq).
67
68
    refine (Fix_unfold_rel _ _ (const (pointwise_relation nat (=))) _ _ s n).
    intros s' f g Hfg i. unfold fresh_generic_body. case_decide; naive_solver.
69
70
  Qed.

71
72
73
  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.
74
75
  Proof.
    revert n.
76
    induction s as [s IH] using (well_founded_ind set_wf); intros n.
77
    setoid_rewrite fresh_generic_fixpoint_unfold; unfold fresh_generic_body.
Ralf Jung's avatar
Ralf Jung committed
78
    destruct decide as [Hcase|Hcase]; [|by eauto with lia].
79
80
    destruct (IH _ (subset_difference_elem_of Hcase) (S n))
      as (m & Hmbound & Heqfix & Hnotin & Hinbelow).
Ralf Jung's avatar
Ralf Jung committed
81
    exists m; repeat split; auto with lia.
82
    - rewrite not_elem_of_difference, elem_of_singleton in Hnotin.
Ralf Jung's avatar
Ralf Jung committed
83
      destruct Hnotin as [?|?%inject_injective]; auto with lia.
84
85
    - intros i Hibound.
      destruct (decide (i = n)) as [<-|Hneq]; [by auto|].
Ralf Jung's avatar
Ralf Jung committed
86
      assert (inject i  s  {[inject n]}) by auto with lia.
87
      set_solver.
88
89
  Qed.

90
  Instance fresh_generic : Fresh A C := λ s, fresh_generic_fix s 0.
91

92
  Instance fresh_generic_spec : FreshSpec A C.
93
94
95
  Proof.
    split.
    - apply _.
96
97
98
99
100
    - 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).
101
      destruct (Nat.lt_trichotomy mX mY) as [case|[->|case]]; auto.
Ralf Jung's avatar
Ralf Jung committed
102
103
      + contradict HnotinX. rewrite HeqXY. apply HbelowinY; lia.
      + contradict HnotinY. rewrite <-HeqXY. apply HbelowinX; lia.
104
105
106
    - intros X. unfold fresh, fresh_generic.
      destruct (fresh_generic_fixpoint_spec X 0)
        as (m & _ & -> & HnotinX & HbelowinX); auto.
107
  Qed.
108
End fresh_generic.