telescopes.v 3.94 KB
Newer Older
1
2
From stdpp Require Export telescopes.
From iris.bi Require Export bi.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.prelude Require Import options.
4
5
6
7
8
Import bi.

(* This cannot import the proofmode because it is imported by the proofmode! *)

(** Telescopic quantifiers *)
9
Definition bi_texist {PROP : bi} {TT : tele@{Quant}} (Ψ : TT  PROP) : PROP :=
10
  tele_fold (@bi_exist PROP) (λ x, x) (tele_bind Ψ).
Ralf Jung's avatar
Ralf Jung committed
11
Global Arguments bi_texist {_ !_} _ /.
12
Definition bi_tforall {PROP : bi} {TT : tele@{Quant}} (Ψ : TT  PROP) : PROP :=
13
  tele_fold (@bi_forall PROP) (λ x, x) (tele_bind Ψ).
Ralf Jung's avatar
Ralf Jung committed
14
Global Arguments bi_tforall {_ !_} _ /.
15
16
17
18
19
20
21
22

Notation "'∃..' x .. y , P" := (bi_texist (λ x, .. (bi_texist (λ y, P)) .. )%I)
  (at level 200, x binder, y binder, right associativity,
  format "∃..  x  ..  y ,  P") : bi_scope.
Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) .. )%I)
  (at level 200, x binder, y binder, right associativity,
  format "∀..  x  ..  y ,  P") : bi_scope.

23
Section telescopes.
24
  Context {PROP : bi} {TT : tele@{Quant}}.
25
  Implicit Types Ψ : TT  PROP.
26

27
  Lemma bi_tforall_forall Ψ : bi_tforall Ψ  bi_forall Ψ.
28
29
30
31
32
33
34
35
36
  Proof.
    symmetry. unfold bi_tforall. induction TT as [|X ft IH].
    - simpl. apply (anti_symm _).
      + by rewrite (forall_elim TargO).
      + rewrite -forall_intro; first done.
        intros p. rewrite (tele_arg_O_inv p) /= //.
    - simpl. apply (anti_symm _); apply forall_intro; intros a.
      + rewrite /= -IH. apply forall_intro; intros p.
        by rewrite (forall_elim (TargS a p)).
37
      + destruct a=> /=.
38
        setoid_rewrite <- IH.
Ralf Jung's avatar
Ralf Jung committed
39
        rewrite 2!forall_elim. done.
40
41
  Qed.

42
  Lemma bi_texist_exist Ψ : bi_texist Ψ  bi_exist Ψ.
43
44
45
46
47
48
49
  Proof.
    symmetry. unfold bi_texist. induction TT as [|X ft IH].
    - simpl. apply (anti_symm _).
      + apply exist_elim; intros p.
        rewrite (tele_arg_O_inv p) //.
      + by rewrite -(exist_intro TargO).
    - simpl. apply (anti_symm _); apply exist_elim.
50
      + intros p. destruct p => /=.
51
52
53
54
55
56
57
58
        by rewrite -exist_intro -IH -exist_intro.
      + intros x.
        rewrite /= -IH. apply exist_elim; intros p.
        by rewrite -(exist_intro (TargS x p)).
  Qed.

  Global Instance bi_tforall_ne n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_tforall PROP TT).
59
  Proof. intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //. Qed.
60
61
  Global Instance bi_tforall_proper :
    Proper (pointwise_relation _ () ==> ()) (@bi_tforall PROP TT).
62
  Proof. intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //. Qed.
63
64
65

  Global Instance bi_texist_ne n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_texist PROP TT).
66
  Proof. intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //. Qed.
67
68
  Global Instance bi_texist_proper :
    Proper (pointwise_relation _ () ==> ()) (@bi_texist PROP TT).
69
70
71
72
73
  Proof. intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //. Qed.

  Global Instance bi_tforall_absorbing Ψ :
    ( x, Absorbing (Ψ x))  Absorbing (.. x, Ψ x).
  Proof. rewrite bi_tforall_forall. apply _. Qed.
74
  Global Instance bi_tforall_persistent `{!BiPersistentlyForall PROP} Ψ :
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
    ( x, Persistent (Ψ x))  Persistent (.. x, Ψ x).
  Proof. rewrite bi_tforall_forall. apply _. Qed.

  Global Instance bi_texist_affine Ψ :
    ( x, Affine (Ψ x))  Affine (.. x, Ψ x).
  Proof. rewrite bi_texist_exist. apply _. Qed.
  Global Instance bi_texist_absorbing Ψ :
    ( x, Absorbing (Ψ x))  Absorbing (.. x, Ψ x).
  Proof. rewrite bi_texist_exist. apply _. Qed.
  Global Instance bi_texist_persistent Ψ :
    ( x, Persistent (Ψ x))  Persistent (.. x, Ψ x).
  Proof. rewrite bi_texist_exist. apply _. Qed.

  Global Instance bi_tforall_timeless Ψ :
    ( x, Timeless (Ψ x))  Timeless (.. x, Ψ x).
  Proof. rewrite bi_tforall_forall. apply _. Qed.
91

92
93
94
  Global Instance bi_texist_timeless Ψ :
    ( x, Timeless (Ψ x))  Timeless (.. x, Ψ x).
  Proof. rewrite bi_texist_exist. apply _. Qed.
95
End telescopes.