telescopes.v 2.93 KB
 Ralf Jung committed Jul 02, 2018 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 committed Jul 02, 2018 26 27 `````` Lemma bi_tforall_forall (Ψ : TT → PROP) : bi_tforall Ψ ⊣⊢ bi_forall Ψ. `````` Ralf Jung committed Jul 02, 2018 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 committed Jul 02, 2018 39 `````` rewrite 2!forall_elim. done. `````` Ralf Jung committed Jul 02, 2018 40 41 `````` Qed. `````` Ralf Jung committed Jul 02, 2018 42 43 `````` Lemma bi_texist_exist (Ψ : TT → PROP) : bi_texist Ψ ⊣⊢ bi_exist Ψ. `````` Ralf Jung committed Jul 02, 2018 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.``````