phanerozoic/Coq-Iris huggingface dataset:
(* tests/proofmode_siprop.v *)
Lemma test_iIntro_impl P Q R : ⊢ P → Q ∧ R → P ∧ R.
Proof. iIntros "#HP #[HQ HR]". auto. Qed.
(* tests/proofmode_siprop.v *)
Lemma test_iApply_impl_1 P Q R : ⊢ P → (P → Q) → Q.
Proof. iIntros "HP HPQ". by iApply "HPQ". Qed.
(* tests/proofmode_siprop.v *)
Lemma test_iApply_impl_2 P Q R : ⊢ P → (P → Q) → Q.
Proof. iIntros "#HP #HPQ". by iApply "HPQ". Qed.
(* tests/sbi_unfold.v *)
Lemma test_impl {A : ofe} (x y z : A) :
    x ≡ y ⊢@{PROP} y ≡ z → x ≡ z.
Proof. sbi_unfold. Show. Abort.
(* tests/sbi_unfold.v *)
Lemma test_impl_impl_and {A : ofe} (x y z : A) :
    ⊢@{PROP} x ≡ y → y ≡ z → x ≡ z ∧ z ≡ x.
Proof. sbi_unfold. Show. Abort.
(* tests/sbi_unfold.v *)
Lemma test_exist_impl {A : ofe} (x z : A) :
    ⊢@{PROP} (∃ y, x ≡ y ∧ y ≡ z) → x ≡ z.
Proof. sbi_unfold. Show. Abort.
(* tests/sbi_unfold.v *)
Lemma test_exist_impl {A : ofe} (x z : A) :
    ⊢@{PROP} x ≡ z → ∃ y, x ≡ y ∧ y ≡ z.
Proof. sbi_unfold. Show. Abort.
(* tests/sbi_unfold.v *)
Lemma test_si_pure_exist {A : ofe} (x z : A) :
    ⊢@{PROP} <si_pure> (∃ y, <si_pure> (x ≡ y) ∧ y ≡ z) → x ≡ z.
Proof. sbi_unfold. Show. Abort.
(* tests/sbi_unfold.v *)
Lemma test_iff_exist {A : ofe} (x z : A) :
    x ≡ z ⊣⊢@{PROP} ∃ y, x ≡ y ∧ y ≡ z.
Proof. sbi_unfold. Show. Abort.
(* tests/sbi_unfold.v *)
Lemma test_iff_exist {A : ofe} (x z : A) :
    ⊢@{PROP} x ≡ z ↔ ∃ y, x ≡ y ∧ y ≡ z.
Proof. sbi_unfold. Show. Abort.
(* tests/sbi_unfold.v *)
Lemma test_iff_exist {A : ofe} (x z : A) :
    ⊢@{PROP} x ≡ z ∗-∗ ∃ y, x ≡ y ∧ y ≡ z.
Proof. sbi_unfold. Show. Abort.
(* tests/sbi_unfold.v *)
Lemma test_iff_exist_later {A : ofe} (x z : A) :
    ⊢@{PROP} ▷ (x ≡ z) ∗-∗ ∃ y, ▷ (x ≡ y ∧ y ≡ z).
Proof. sbi_unfold. Show. Abort.
(* tests/sbi_unfold.v *)
Lemma test_exist_impl {A : ofe} (x z : A) :
    ⊢@{PROP} x ≡ z → ∃ y, x ≡ y → y ≡ z.
Proof. sbi_unfold. Show. Abort.
(* tests/sbi_unfold.v *)
Lemma test_forall_impl {A : ofe} (x z : A) :
    ⊢@{PROP} (∀ y, x ≡ y → y ≡ z) → x ≡ z.
Proof. sbi_unfold. Show. Abort.
(* tests/siprop.v *)
Lemma unseal_test (P Q : siProp) (Φ : nat → siProp) :
  P ∧ ▷ Q ∧ (∃ x, Φ x) ⊣⊢ ∃ x, P ∗ ▷ Q ∧ emp ∨ Φ x.
Proof.
  siProp.unseal.
  Show.
Abort.
(* tests/siprop.v *)
(* Make sure that [siProp]s are parsed in [bi_scope]. *)
Definition test : siProp
:= ▷ True.
(* tests/siprop.v *)
Definition testI : siPropI
:= ▷ True.
(* tests/string_ident.v *)
Lemma test_basic_ident : ∀ (n:nat), n = n.
Proof.
  let x := fresh in intros x; rename_by_string x "n".
  exact (eq_refl n).
Qed.
(* tests/string_ident.v *)
Lemma test_invalid_ident : ∀ (n:nat), True.
Proof.
  Fail let x := fresh in intros x; rename_by_string x "has a space".
Abort.
(* tests/string_ident.v *)
Lemma test_not_string : ∀ (n:nat), True.
Proof.
  Fail let x := fresh in intros x; rename_by_string x 4.
Abort.
(* tests/string_ident.v *)
Lemma test_not_literal (s:string) : ∀ (n:nat), True.
Proof.
  Fail let x := fresh in intros x; rename_by_string x s.
Abort.
(* tests/string_ident.v *)
Lemma test_string_to_ident_not_fresh (n:nat) : ∀ (n:nat), nat.
Proof.
  (* we want to check that this [string_to_ident "n"] call succeeds even with
  [n] in the context *)
  string_to_ident_cps "n" ltac:(fun x =>
  let x := fresh x in
  intros x).
Abort.
(* tests/telescopes.v *)
Lemma test_iIntros_tforall {TT : tele} (Φ : TT → PROP) :
    ⊢ ∀.. x, Φ x -∗ Φ x.
Proof. iIntros (x) "H". done. Qed.
(* tests/telescopes.v *)
Lemma test_iPoseProof_tforall {TT : tele} P (Φ : TT → PROP) :
    (∀.. x, P ⊢ Φ x) → P -∗ ∀.. x, Φ x.
Proof.
    iIntros (H1) "H2"; iIntros (x).
    iPoseProof (H1) as "H1". by iApply "H1".
  Qed.
(* tests/telescopes.v *)
Lemma test_iApply_tforall {TT : tele} P (Φ : TT → PROP) :
    (∀.. x, P -∗ Φ x) -∗ P -∗ ∀.. x, Φ x.
Proof. iIntros "H1 H2" (x). by iApply "H1". Qed.
(* tests/telescopes.v *)
Lemma test_iAssumption_tforall {TT : tele} (Φ : TT → PROP) :
    (∀.. x, Φ x) -∗ ∀.. x, Φ x.
Proof. iIntros "H" (x). iAssumption. Qed.
(* tests/telescopes.v *)
Lemma test_exist_texist_auto_name {TT : tele} (Φ : TT → PROP) :
    (∃.. y, Φ y) -∗ ∃.. x, Φ x.
Proof. iDestruct 1 as (?) "H". by iExists y. Qed.
(* tests/telescopes.v *)
Lemma test_pure_texist {TT : tele} (φ : TT → Prop) :
    (∃.. x, ⌜ φ x ⌝) -∗ ∃.. x, ⌜ φ x ⌝ : PROP.
Proof. iIntros (H) "!%". done. Qed.
(* tests/telescopes.v *)
Lemma test_pure_tforall `{!BiPureForall PROP} {TT : tele} (φ : TT → Prop) :
    (∀.. x, ⌜ φ x ⌝) -∗ ∀.. x, ⌜ φ x ⌝ : PROP.
Proof. iIntros (H) "!%". done. Qed.
(* tests/telescopes.v *)
Lemma test_pure_tforall_persistent `{!BiPersistentlyForall PROP} {TT : tele} (Φ : TT → PROP) :
    (∀.. x, <pers> (Φ x)) -∗ <pers> ∀.. x, Φ x.
Proof. iIntros "#H !>" (x). done. Qed.
(* tests/telescopes.v *)
Lemma test_pure_texists_intuitionistic {TT : tele} (Φ : TT → PROP) :
    (∃.. x, □ (Φ x)) -∗ □ ∃.. x, Φ x.
Proof. iDestruct 1 as (x) "#H". iExists (x). done. Qed.
(* tests/telescopes.v *)
Lemma test_iMod_tforall {TT : tele} P (Φ : TT → PROP) :
    ◇ P -∗ (∀.. x, Φ x) -∗ ∀.. x, ◇ (P ∗ Φ x).
Proof. iIntros ">H1 H2" (x) "!> {$H1}". done. Qed.
(* tests/telescopes.v *)
Lemma test_timeless_tforall {TT : tele} (φ : TT → Prop) :
    ▷ (∀.. x, ⌜ φ x ⌝) -∗ ◇ ∀.. x, ⌜ φ x ⌝ : PROP.
Proof. iIntros ">H1 !>". done. Qed.
(* tests/telescopes.v *)
Lemma test_timeless_texist {TT : tele} (φ : TT → Prop) :
    ▷ (∃.. x, ⌜ φ x ⌝) -∗ ◇ ∃.. x, ⌜ φ x ⌝ : PROP.
Proof. iIntros ">H1 !>". done. Qed.
(* tests/telescopes.v *)
Lemma test_add_model_texist `{!BiBUpd PROP} {TT : tele} P Q (Φ : TT → PROP) :
    (|==> P) -∗ (P -∗ Q) -∗ ∀.. x, |==> Q ∗ (Φ x -∗ Φ x).
Proof. iIntros "H1 H2". iDestruct ("H2" with "[> $H1]") as "$". auto. Qed.
(* tests/telescopes.v *)
Lemma test_iFrame_tforall {TT : tele} P (Φ : TT → PROP) :
    P -∗ ∀.. x, P ∗ (Φ x -∗ Φ x).
Proof. iIntros "$". auto. Qed.
(* tests/telescopes.v *)
Lemma test_iFrame_texist {TT : tele} P (Φ : TT → PROP) :
    P -∗ (∃.. x, Φ x) -∗ ∃.. x, P ∗ Φ x.
Proof. iIntros "$". auto. Qed.
(* tests/telescopes.v *)
(* 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.
(* tests/telescopes.v *)
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 200, x1 binder, xn binder, only parsing).
(* tests/telescopes.v *)
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.
(* tests/telescopes.v *)
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.
(* tests/telescopes.v *)
(* 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.
(* tests/telescopes.v *)
Definition test1 {PROP : bi} {X : tele} (α : X → PROP) : PROP
:=
  (∃.. x, α x)%I.
(* tests/telescopes.v *)
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 200, x1 binder, xn binder, only parsing).
(* tests/telescopes.v *)
Definition test2 {PROP : bi} {X : tele} (α : X → PROP) : PROP
:=
  (▷ ∃.. x, α x)%I.
(* tests/telescopes.v *)
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 200, x1 binder, xn binder, only parsing).
(* tests/telescopes.v *)
Definition test3 {PROP : bi} {X : tele} (α : X → PROP) : PROP
:=
  (◇ ∃.. x, α x)%I.
(* tests/telescopes.v *)
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 200, x1 binder, xn binder, only parsing).
(* tests/telescopes.v *)
Lemma test1_test {PROP : bi}  :
  TEST1 {{ ∃ a b : nat, <affine> ⌜a = b⌝ }} ⊢@{PROP} ▷ False.
Proof.
  iIntros "H". iDestruct "H" as (x) "H". Show.
Restart. Proof.
  iIntros "H". unfold test1. iDestruct "H" as (x) "H". Show.
Abort.
(* tests/telescopes.v *)
Lemma test2_test {PROP : bi}  :
  TEST2 {{ ∃ a b : nat, <affine> ⌜a = b⌝ }} ⊢@{PROP} ▷ False.
Proof.
  iIntros "H". iModIntro. Show.
  iDestruct "H" as (x) "H". Show.
Restart. Proof.
  iIntros "H". iDestruct "H" as (x) "H". Show.
Abort.
(* tests/telescopes.v *)
Lemma test3_test {PROP : bi}  :
  TEST3 {{ ∃ a b : nat, <affine> ⌜a = b⌝ }} ⊢@{PROP} ▷ False.
Proof.
  iIntros "H". iMod "H".
  iDestruct "H" as (x) "H".
  Show.
Restart. Proof.
  iIntros "H". iDestruct "H" as (x) "H". Show.
Abort.
(* tests/telescopes.v *)
Lemma tele_universe {PROP : bi} (TT : tele@{bi.Quant}) (P : TT → PROP) :
  bi_texist P ⊣⊢ bi_exist P.
Proof. apply bi_texist_exist. Qed.
(* tests/tree_sum.v *)
Inductive tree
:=
  | leaf : Z → tree
  | node : tree → tree → tree.
(* tests/tree_sum.v *)
Fixpoint is_tree `{!heapGS Σ} (v : val) (t : tree) : iProp Σ
:=
  match t with
  | leaf n => ⌜v = InjLV #n⌝
  | node tl tr =>
     ∃ (ll lr : loc) (vl vr : val),
       ⌜v = InjRV (#ll,#lr)⌝ ∗ ll ↦ vl ∗ is_tree vl tl ∗ lr ↦ vr ∗ is_tree vr tr
  end%I.
(* tests/tree_sum.v *)
Fixpoint sum (t : tree) : Z
:=
  match t with
  | leaf n => n
  | node tl tr => sum tl + sum tr
  end.
(* tests/tree_sum.v *)
Definition sum_loop : val
:=
  rec: "sum_loop" "t" "l" :=
    match: "t" with
      InjL "n" => "l" <- "n" + !"l"
    | InjR "tt" => "sum_loop" !(Fst "tt") "l" ;; "sum_loop" !(Snd "tt") "l"
    end.
(* tests/tree_sum.v *)
Definition sum' : val
:= λ: "t",
  let: "l" := ref #0 in
  sum_loop "t" "l";;
  !"l".
(* tests/tree_sum.v *)
Lemma sum_loop_wp `{!heapGS Σ} v t l (n : Z) :
  [[{ l ↦ #n ∗ is_tree v t }]]
    sum_loop v #l
  [[{ RET #(); l ↦ #(sum t + n) ∗ is_tree v t }]].
Proof.
  iIntros (Φ) "[Hl Ht] HΦ".
  iInduction t as [n'|tl IHl tr IHr] forall (v l n Φ); simpl; wp_rec; wp_let.
  - iDestruct "Ht" as "%"; subst.
    wp_load. wp_store.
    by iApply ("HΦ" with "[$Hl]").
  - iDestruct "Ht" as (ll lr vl vr ->) "(Hll & Htl & Hlr & Htr)".
    wp_load. wp_apply ("IHl" with "Hl Htl"). iIntros "[Hl Htl]".
    wp_load. wp_apply ("IHr" with "Hl Htr"). iIntros "[Hl Htr]".
    iApply "HΦ". iSplitL "Hl".
    { by replace (sum tl + sum tr + n)%Z with (sum tr + (sum tl + n))%Z by lia. }
    iExists ll, lr, vl, vr. by iFrame.
Qed.
(* tests/tree_sum.v *)
Lemma sum_wp `{!heapGS Σ} v t :
  [[{ is_tree v t }]] sum' v [[{ RET #(sum t); is_tree v t }]].
Proof.
  iIntros (Φ) "Ht HΦ". rewrite /sum' /=.
  wp_lam. wp_alloc l as "Hl".
  wp_smart_apply (sum_loop_wp with "[$Hl $Ht]").
  rewrite Z.add_0_r.
  iIntros "[Hl Ht]". wp_load. by iApply "HΦ".
Qed.