introduce_var.v 1.19 KB
Newer Older
1
From iris.proofmode Require Import base coq_tactics reduction tactics.
2
From diaframe Require Import solve_defs.
3
4
5
6
From iris.bi Require Import bi telescopes.

Import bi.

7
8
(* This file contains 'case 1' of Diaframe's proof search strategy: introducing foralls. *)

9
10
11
12
13
14
15
16

Section introduce_var.

  Context {PROP : bi}.
  Implicit Types TT : tele.

  Lemma introduce_vars {TT} Q :
    (.. (tt : TT), tele_app Q tt)  IntroduceVars (PROP := PROP) (TT := TT) Q.
17
  Proof. by unseal_diaframe. Qed.
18
19
20
21
22
23
24
25
26
27
28
29
30

  Lemma tac_introduce_vars_teleS {T} {b : T  tele} Δ Q :
    (.. (tt : TeleS b), envs_entails Δ $ tele_app Q tt) 
    envs_entails Δ $ IntroduceVars (PROP := PROP) (TT := TeleS b) Q.
  Proof.
    rewrite -introduce_vars envs_entails_eq bi_tforall_forall tforall_forall => Htt.
    apply forall_intro => tt.
    apply Htt.
  Qed.

  Lemma tac_introduce_vars_teleO  Δ Q :
    envs_entails Δ $ Q 
    envs_entails Δ $ IntroduceVars (PROP := PROP) (TT := [tele]) Q.
31
  Proof. by unseal_diaframe. Qed.
32

33
34
35
36
37
End introduce_var.



Ltac introduceVarStep :=
38
  first                               (* is this subst necessary? *)
39
40
  [apply tac_introduce_vars_teleS; simpl; intros; subst; simpl
  |apply tac_introduce_vars_teleO].