telescopes.v 2.93 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
From stdpp Require Export telescopes.
From iris.bi Require Export bi.
Set Default Proof Using "Type*".
Import bi.

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

(** Telescopic quantifiers *)
Definition bi_texist {PROP : bi} {TT : tele} (Ψ : TT  PROP) : PROP :=
  tele_fold (@bi_exist PROP) (λ x, x) (tele_bind Ψ).
Arguments bi_texist {_ !_} _ /.
Definition bi_tforall {PROP : bi} {TT : tele} (Ψ : TT  PROP) : PROP :=
  tele_fold (@bi_forall PROP) (λ x, x) (tele_bind Ψ).
Arguments bi_tforall {_ !_} _ /.

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.

Section telescope_quantifiers.
  Context {PROP : bi} {TT : tele}.

Ralf Jung's avatar
Ralf Jung committed
26 27
  Lemma bi_tforall_forall (Ψ : TT  PROP) :
    bi_tforall Ψ  bi_forall Ψ.
28 29 30 31 32 33 34 35 36 37 38
  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)).
      + move/tele_arg_inv : (a) => [x [pf ->]] {a} /=.
        setoid_rewrite <- IH.
Ralf Jung's avatar
Ralf Jung committed
39
        rewrite 2!forall_elim. done.
40 41
  Qed.

Ralf Jung's avatar
Ralf Jung committed
42 43
  Lemma bi_texist_exist (Ψ : TT  PROP) :
    bi_texist Ψ  bi_exist Ψ.
44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82
  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.
      + intros p. move/tele_arg_inv: (p) => [x [pf ->]] {p} /=.
        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).
  Proof.
    intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //.
  Qed.

  Global Instance bi_tforall_proper :
    Proper (pointwise_relation _ () ==> ()) (@bi_tforall PROP TT).
  Proof.
    intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //.
  Qed.

  Global Instance bi_texist_ne n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_texist PROP TT).
  Proof.
    intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //.
  Qed.

  Global Instance bi_texist_proper :
    Proper (pointwise_relation _ () ==> ()) (@bi_texist PROP TT).
  Proof.
    intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //.
  Qed.

End telescope_quantifiers.