telescopes.v 4.2 KB
Newer Older
1 2 3 4
From stdpp Require Import coPset namespaces.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".

5
Section accessor.
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35
(* Just playing around a bit with a telescope version
   of accessors with just one binder list. *)
Definition accessor `{!BiFUpd PROP} {X : tele} (E1 E2 : coPset)
           (α β γ : X  PROP) : PROP :=
  (|={E1,E2}=> .. x, α x  (β x - |={E2,E1}=> (γ x)))%I.

Notation "'ACC' @ E1 , E2 {{ ∃ x1 .. xn , α | β | γ } }" :=
  (accessor (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
            E1 E2
            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
                      fun x1 => .. (fun xn => α%I) ..)
            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
                      fun x1 => .. (fun xn => β%I) ..)
            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
                      fun x1 => .. (fun xn => γ%I) ..))
  (at level 20, α, β, γ at level 200, x1 binder, xn binder, only parsing).

(* Working with abstract telescopes. *)
Section tests.
Context `{!BiFUpd PROP} {X : tele}.
Implicit Types α β γ : X  PROP.

Lemma acc_mono E1 E2 α β γ1 γ2 :
  (.. x, γ1 x - γ2 x) -
  accessor E1 E2 α β γ1 - accessor E1 E2 α β γ2.
Proof.
  iIntros "Hγ12 >Hacc". iDestruct "Hacc" as (x') "[Hα Hclose]". Show.
  iModIntro. iExists x'. iFrame. iIntros "Hβ".
  iMod ("Hclose" with "Hβ") as "Hγ". iApply "Hγ12". auto.
Qed.
36 37 38 39 40 41 42 43 44

Lemma acc_mono_disj E1 E2 α β γ1 γ2 :
  accessor E1 E2 α β γ1 - accessor E1 E2 α β (λ.. x, γ1 x  γ2 x).
Proof.
  Show.
  iApply acc_mono. iIntros (x) "Hγ1". Show.
  rewrite ->tele_app_bind. Show.
  iLeft. done.
Qed.
45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
End tests.

Section printing_tests.
Context `{!BiFUpd PROP}.

(* Working with concrete telescopes: Testing the reduction into normal quantifiers. *)
Lemma acc_elim_test_1 E1 E2 :
  ACC @ E1, E2 {{  a b : nat, <affine> a = b | True | <affine> a  b }}
    @{PROP} |={E1}=> False.
Proof.
  iIntros ">H". Show.
  iDestruct "H" as (a b) "[% Hclose]". iMod ("Hclose" with "[//]") as "%".
  done.
Qed.
End printing_tests.
60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122
End accessor.

(* Robbert's tests *)
Section telescopes_and_tactics.

Definition test1 {PROP : sbi} {X : tele} (α : X  PROP) : PROP :=
  (.. x, α x)%I.

Notation "'TEST1' {{ ∃ x1 .. xn , α } }" :=
  (test1 (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
                      fun x1 => .. (fun xn => α%I) ..))
  (at level 20, α at level 200, x1 binder, xn binder, only parsing).

Definition test2 {PROP : sbi} {X : tele} (α : X  PROP) : PROP :=
  ( .. x, α x)%I.

Notation "'TEST2' {{ ∃ x1 .. xn , α } }" :=
  (test2 (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
                      fun x1 => .. (fun xn => α%I) ..))
  (at level 20, α at level 200, x1 binder, xn binder, only parsing).

Definition test3 {PROP : sbi} {X : tele} (α : X  PROP) : PROP :=
  ( .. x, α x)%I.

Notation "'TEST3' {{ ∃ x1 .. xn , α } }" :=
  (test3 (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
                      fun x1 => .. (fun xn => α%I) ..))
  (at level 20, α at level 200, x1 binder, xn binder, only parsing).

Check "test1_test".
Lemma test1_test {PROP : sbi}  :
  TEST1 {{  a b : nat, <affine> a = b }} @{PROP}  False.
Proof.
  iIntros "H". iDestruct "H" as (x) "H". Show.
Restart.
  iIntros "H". unfold test1. iDestruct "H" as (x) "H". Show.
Abort.

Check "test2_test".
Lemma test2_test {PROP : sbi}  :
  TEST2 {{  a b : nat, <affine> a = b }} @{PROP}  False.
Proof.
  iIntros "H". iModIntro. Show.
  iDestruct "H" as (x) "H". Show.
Restart.
  iIntros "H". iDestruct "H" as (x) "H". Show.
Abort.

Check "test3_test".
Lemma test3_test {PROP : sbi}  :
  TEST3 {{  a b : nat, <affine> a = b }} @{PROP}  False.
Proof.
  iIntros "H". iMod "H".
  iDestruct "H" as (x) "H".
  Show.
Restart.
  iIntros "H". iDestruct "H" as (x) "H". Show.
Abort.

End telescopes_and_tactics.