Set Implicit Arguments.

(* Set Implicit Arguments. *)

Inductive context Σ : Type :=
    | CEmpty
    | CVar of string & iProp Σ
    | CAnd of context Σ & context Σ
    | CSep of context Σ & context Σ
.

Definition c_sep {Σ} (c1 c2 : context Σ) := 
    if c1 is CEmpty _ then c2 else if c2 is CEmpty _ then c1 else CSep c1 c2.
Definition c_and {Σ} (c1 c2 : context Σ) := 
    if c1 is CEmpty _ then c2 else if c2 is CEmpty _ then c1 else CAnd c1 c2.
    
Fixpoint bind {Σ} (var : string) (c : context Σ) : context Σ 
:= match c with
    | CEmpty _ => CEmpty _
    | CVar var' P => if decide (var = var') then CEmpty _ else CVar var' P
    | CAnd c1 c2 => c_and (bind var c1) (bind var c2)
    | CSep c1 c2 => c_sep (bind var c1) (bind var c2)
end.

(* TODO: Should I put this in a module, with a `:>`? *)
Inductive uses := One | Many.

Fixpoint prop_of_ctx {Σ} (c : context Σ) : iProp Σ := match c with
    | CEmpty _ => True
    | CVar _ P => P
    | CAnd c1 c2 => prop_of_ctx c1 ∧ prop_of_ctx c2
    | CSep c1 c2 => prop_of_ctx c1 ∗ prop_of_ctx c2

Definition uses_prop {Σ} (u : uses) (P : iProp Σ) : iProp Σ := match u with
    | One => P
    | Many => □P

Lemma c_sep_spec {Σ} (c1 c2 : context Σ) 
    : prop_of_ctx (c_sep c1 c2) ⊣⊢ prop_of_ctx (CSep c1 c2).

Definition uses_sep (u : uses) (v : uses) : uses := Many.
Lemma uses_sep_spec {Σ} {P : iProp Σ} u v
    : uses_prop (uses_sep u v) P ⊢ uses_prop u P ∗ uses_prop v P.

    by case c1; case c2; intros; simpl; 
        try rewrite bi.emp_sep; try rewrite bi.sep_emp.

    have: ∀ x, □P ⊢ uses_prop x P by case; [apply: bi.intuitionistically_elim | ].
    move=> lemma.
    simpl.
    rewrite bi.intuitionistically_sep_dup.
    apply: bi.sep_mono; apply: lemma.

Lemma c_and_spec {Σ} (c1 c2 : context Σ) 
    : prop_of_ctx (c_and c1 c2) ⊣⊢ prop_of_ctx (CAnd c1 c2).

Definition uses_and (u : uses) (v : uses) : uses := match u, v with
    | One, One => One
    | _, _ => Many
end.
Lemma uses_and_spec {Σ} {P : iProp Σ} u v
    : uses_prop (uses_and u v) P ⊢ uses_prop u P ∧ uses_prop v P.

    by case c1; case c2; intros; simpl;
        try rewrite bi.True_and; try rewrite bi.and_True.

    apply: bi.and_intro; case u; case v; try done; apply: bi.intuitionistically_elim.

(* Purpose of ctx_uses:

    - Only used in constraint generation
    - Generates equality constraints, if variable is repeated
    - Decides whether the variable needs to be persistent.

    - No, it is also used in bind_spec.

    - MUST determine whether variable needs to be persistent.
    - MUST allow generation of equality constraints.
    - SHOULD allow easy definition of bind_spec.

Module Type contextT.
    (* Describes what must hold for an expression to typecheck.
        Includes:
        - Free variables, associated with their types and usage patterns.
        - Equality constraints, generated during typechecking.
    *)
    Parameter context : gFunctors -> Type.
    Parameter prop : ∀ {Σ}, context Σ -> iProp Σ.

    Parameter var : ∀ {Σ}, string -> iProp Σ -> context Σ.
    Axiom var_spec : ∀ {Σ} v (T : iProp Σ), prop (var v T) ⊢ T.

    option (constraints * iProp * uses)
*)

    Parameter constrain : ∀ {Σ}, Prop -> context Σ -> context Σ.
    Axiom constrain_spec : ∀ {Σ} P (ctx : context Σ),
        prop (constrain P ctx) ⊢ ∃ _ : P, prop ctx.
    (* Combine two expressions, in a separating way. *)
    Parameter sep : ∀ {Σ}, context Σ -> context Σ -> context Σ.
    Axiom sep_spec : ∀ {Σ} (c1 c2 : context Σ),
        prop (sep c1 c2) ⊢ prop c1 ∗ prop c2.
    
    (* Combine two expressions, in a non-separating way. *)
    Parameter and : ∀ {Σ}, context Σ -> context Σ -> context Σ.
    Axiom and_spec : ∀ {Σ} (c1 c2 : context Σ),
        prop (and c1 c2) ⊢ prop c1 ∧ prop c2.
    (* Remove a free variable from the context.
        Used to implement variable patterns.
    *)
    Parameter bind : ∀ {Σ}, string -> context Σ -> context Σ.
    (* Get the type and usage pattern of a variable. *)
    Parameter lookup : ∀ {Σ}, string -> context Σ -> option (iProp Σ * uses).
    
    Axiom bind_spec : ∀ {Σ} var (c : context Σ),
        match lookup var c with
            | None => emp
            | Some (P, uses) => (uses_prop uses P)
        end ∗ prop (bind var c) ⊢ 
        prop c.

Inductive uses := One | Many.

    (* Interpret the expression in the toplevel scope.
        This will return a collection of constraints.
        Note that the constraint may be something like
        (error ("Variables not in scope.", ["x", "y"])).
    *)
    Parameter toplevel : ∀ {Σ}, context Σ -> Prop.
    Axiom toplevel_spec : ∀ {Σ} (ctx : context Σ),
        toplevel ctx -> ⊢ prop ctx.
End contextT.
Module context <: contextT.
    (* It turns out to be easier to carry the equality constraints 
        along with the variables, until they are bound.
        Afterward, I store the constraints separately.
    *)
    Record contextT {Σ} : Type := {
        Constraints : Prop;
        Variables : stringmap (iProp Σ * uses * Prop);
    }.
    Definition context Σ : Type := contextT (Σ := Σ).
    Definition prop {Σ} (ctx : context Σ) : iProp Σ := 
        ∃ _ : Constraints ctx,
        [∗ map] data ∈ Variables ctx, 
            let '(P, u, constraints) := data in 
            ∃ _ : (constraints : Prop), uses_prop u P.
    Definition var {Σ} (var : string) (type : iProp Σ) : context Σ := {|
        Constraints := True;
        Variables := {[var := (type, One, True)]};
    |}.
    Theorem var_spec {Σ} v (T : iProp Σ) : prop (var v T) ⊢ T.
    Proof.
        apply: bi.exist_elim; move=> [].
        rewrite big_sepM_singleton.
        apply: bi.exist_elim; move=> [].
        done.
    Qed.
    Definition constrain {Σ} (constraint : Prop) (ctx : context Σ) : context Σ := {|
        Constraints := constraint ∧ Constraints ctx;
        Variables := Variables ctx;
    |}.
    Theorem constrain_spec {Σ} P (ctx : context Σ)
        : prop (constrain P ctx) ⊢ ∃ _ : P, prop ctx.
    Proof.
        apply: bi.exist_elim. move=> [wP w].
        do 2 apply: bi.exist_intro'.
        done.
    Qed.

(* Returns:
    - Whether the variable must be persistent.
    - The type of the variable.
    - The generated equality constraints.
*)
Fixpoint ctx_uses {Σ} (var : string) (c : context Σ)
    : option (uses * iProp Σ * Prop)
    := match c with
        | CEmpty _ => None
        | CVar var' P =>
            if decide (var = var') 
            then Some (One, P, True)
            else None
        | CAnd c1 c2 =>
            union_with
                (λ '(u1, P1, constraints1) '(u2, P2, constraints2), Some
                    ( match u1, u2 with One, One => One | _, _ => Many end
                    , P1
                    , constraints1 ∧ constraints2 ∧ P1 = P2
                    )
                )
                (ctx_uses var c1)
                (ctx_uses var c2)
        | CSep c1 c2 =>
            union_with
                (λ '(u1, P1, constraints1) '(u2, P2, constraints2), Some
                    ( Many
                    , P1
                    , constraints1 ∧ constraints2 ∧ P1 = P2
                    )
                )
                (ctx_uses var c1)
                (ctx_uses var c2)
    end.

Lemma bind_spec {Σ} var (c : context Σ)
    : match ctx_uses var c with
        | None => prop_of_ctx (bind var c) ⊢ prop_of_ctx c
        | Some (uses, P, constraints) => 
            constraints -> 
            prop_of_ctx (bind var c) ∗ 
            (match uses with One => P | Many => □P end) ⊢ 
            prop_of_ctx c
    end.
Proof.
    have: ∀ u (P : iProp Σ), □ P ⊢ match u with One => P | Many => □ P end.
    { case. apply: bi.intuitionistically_elim. done. }
    move=> lemma1.

        
    Lemma big_sepM_hetero {type : bi} `{countable : Countable K} {V1 V2} 
        (Φ : K -> V1 -> type) (Ψ : K -> V2 -> type)
        (m1 : gmap K V1) (m2 : gmap K V2)
        : (∀ k, 
            (if m1 !! k is Some v then Φ k v else emp) ⊢ 
            (if m2 !! k is Some v then Ψ k v else emp))
        -> ([∗ map] k ↦ v ∈ m1, Φ k v) ⊢ ([∗ map] k ↦ v ∈ m2, Ψ k v).
    Proof.
        move: m2.
        induction m1 as [|k v1 m1' fact1 IH1] using map_ind.
        - move=> m2 H. rewrite big_sepM_empty.
            induction m2 as [|k v2 m2' fact2 IH2] using map_ind.
            + by rewrite big_sepM_empty.
            + rewrite big_sepM_insert; last exact fact2.
                rewrite -(bi.emp_sep emp%I).
                apply: bi.sep_mono.
                * move: (H k) => H'.
                    by rewrite lookup_empty lookup_insert in H'.
                * apply: IH2 => k'.
                    rewrite lookup_empty.
                    case: (decide (k = k')).
                    -- move=><-. by rewrite fact2.
                    -- move=> neq.
                        move: (H k').
                        by rewrite lookup_empty lookup_insert_ne.

    have: ∀ u (P : iProp Σ), match u with One => P | Many => □ P end ⊢ P.
    { case. done. apply: bi.intuitionistically_elim. }
    move=> lemma2.

        - move=> m2 H.
            rewrite big_sepM_insert; last exact fact1.

    elim c; simpl.
    - done.
    - move=> var' P.
        case: (decide (var = var')).
        + by rewrite bi.emp_sep.
        + done.
    - move=> c1; case: (ctx_uses var c1) => [[[u1 P1] constraints1]|] H1;
        move=> c2; case: (ctx_uses var c2) => [[[u2 P2] constraints2]|] H2;
        simpl; rewrite c_and_spec; simpl;
        [ move=>[/H1 w1 [/H2 w2 eq]] 
        | move: H2 => w2 /H1 w1 
        | move: H1 => w1 /H2 w2 
        | move: H1 H2 => w1 w2
        ];
        (apply: transitivity; last (apply: bi.and_mono; [apply: w1 | apply: w2])).
        + rewrite eq.
            apply: transitivity; first apply: bi.sep_and_r.
            apply: bi.and_mono; apply: bi.sep_mono_r.
            * case u1; last done.
                apply: transitivity; last apply: (lemma2 u2).
                by case u2.
            * case u2; last by case u1.
                apply: transitivity; last apply: (lemma2 u1).
                by case u1.
            + apply: transitivity; first apply: bi.sep_and_r.
            apply: bi.and_mono; first done.
            rewrite -{2}[prop_of_ctx _]bi.sep_emp.
            apply: bi.sep_mono; first done.
            apply: bi.True_intro.
        + apply: transitivity; first apply: bi.sep_and_r.
            apply: bi.and_mono; last done.
            rewrite -{2}[prop_of_ctx _]bi.sep_emp.
            apply: bi.sep_mono; first done.
            apply: bi.True_intro.
        + done.
    - move=> c1; case: (ctx_uses var c1) => [[[u1 P1] constraints1]|] H1;
        move=> c2; case: (ctx_uses var c2) => [[[u2 P2] constraints2]|] H2;
        simpl; rewrite c_sep_spec; simpl;
        [ move=>[/H1 w1 [/H2 w2 eq]] 
        | move: H2 => w2 /H1 w1 
        | move: H1 => w1 /H2 w2 
        | move: H1 H2 => w1 w2
        ];
        (apply: transitivity; last (apply: bi.sep_mono; [apply: w1 | apply: w2])).
        + apply: transitivity; 
            last (apply: bi.sep_mono; apply: bi.sep_mono_r; apply: lemma1).
            rewrite eq {1}bi.intuitionistically_sep_dup.
            rewrite bi.sep_assoc bi.sep_assoc; apply: bi.sep_mono_l.
            rewrite -bi.sep_assoc -bi.sep_assoc; apply: bi.sep_mono_r.
            by rewrite bi.sep_comm.
        + by rewrite 
            -bi.sep_assoc 
            [(prop_of_ctx (bind var c2) ∗ _)%I]bi.sep_comm
            bi.sep_assoc.
        + by rewrite bi.sep_assoc.
        + done.
Qed.

            apply: transitivity.
            { 
                apply: bi.sep_mono.
                - move: (H k) => H'.
                    rewrite lookup_insert in H'.
                    exact: H'.
                - apply: (IH1 (delete k m2)) => k'.
                    case: (decide (k = k')).
                    + move=><-. by rewrite fact1 lookup_delete.
                    + move=> neq.
                        rewrite lookup_delete_ne; last exact neq.
                        move: (H k').
                        rewrite lookup_insert_ne; last exact neq.
                        done.
            }

            have: m2 !! k = m2 !! k by []; case: {-1}(m2 !! k) => [v2|] fact2.
            + by rewrite (big_sepM_delete _ m2).
            + by rewrite bi.emp_sep delete_notin.
    Qed.

Inductive expr {Σ : gFunctors} : context Σ -> iProp Σ -> Type :=
    | Pair {c1 c2 T1 T2} : expr c1 T1 -> expr c2 T2 -> expr (c_sep c1 c2) (T1 ∗ T2)
    | Var {T} : ∀ var, expr (CVar var T) T
    | Lam {ctx T1 T2} 
        : ∀ var {constraints : match ctx_uses var ctx with
            | None => True
            | Some (uses, type, constraints) =>
                constraints ∧ type = T1 ∧ match uses with 
                    | Many => error 
                        ( "A linear variable was used multiple times.", var )
                    | One => True
                end
        end },
        expr ctx T2 ->
        expr (bind var ctx) (T1 -∗ T2)

    Definition sep {Σ} (c1 : context Σ) (c2 : context Σ) : context Σ := {| 
        Constraints := Constraints c1 ∧ Constraints c2;
        Variables := union_with
            (λ '(P, u, c1) '(Q, v, c2), Some (P, uses_sep u v, c1 ∧ c2 ∧ P = Q)) 
            (Variables c1) (Variables c2);
    |}.
    Theorem sep_spec {Σ} (c1 c2 : context Σ)
        : prop (sep c1 c2) ⊢ prop c1 ∗ prop c2.
    Proof.
        rewrite /prop.
        apply: bi.exist_elim; move => [w1 w2].
        rewrite bi.sep_exist_l; apply: bi.exist_intro'.
        rewrite bi.sep_exist_r; apply: bi.exist_intro'.
        clear w1 w2.
        
        apply: transitivity; last (
            apply: bi.sep_mono;
            [ apply: (big_sepM_hetero
                (λ k _, 
                    if Variables c1 !! k is Some (P, u, constraints) 
                    then ∃ _ : (constraints : Prop), uses_prop u P 
                    else emp)%I _ 
                (Variables (sep c1 c2))) => k
            | apply: (big_sepM_hetero
                (λ k _, 
                    if Variables c2 !! k is Some (P, u, constraints) 
                    then ∃ _ : (constraints : Prop), uses_prop u P 
                    else emp)%I _ 
                (Variables (sep c1 c2))) => k
            ]
        ).
        - rewrite -big_sepM_sep.
            apply: big_sepM_mono => k [[P u] constraints] fact.
            apply: bi.exist_elim.
            move: fact; rewrite lookup_union_with.
            case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];
            case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];
            simpl; last done;
            move=>w; injection w; clear w;
            move=> <-<-<- w.
            + move: w => [w1 [w2 <-]].
                rewrite bi.sep_exist_l; apply: bi.exist_intro'.
                rewrite bi.sep_exist_r; apply: bi.exist_intro'.
                apply: uses_sep_spec.
            + by rewrite bi.sep_emp; apply: bi.exist_intro'.
            + by rewrite bi.emp_sep; apply: bi.exist_intro'.
        - rewrite lookup_union_with.
            case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];
            case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];
            done.
        - rewrite lookup_union_with.
            case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];
            case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];
            done.
    Qed.
    Definition and {Σ} (c1 : context Σ) (c2 : context Σ) : context Σ := {| 
        Constraints := Constraints c1 ∧ Constraints c2;
        Variables := union_with
            (λ '(P, u, c1) '(Q, v, c2), Some (P, uses_and u v, c1 ∧ c2 ∧ P = Q)) 
            (Variables c1) (Variables c2);
    |}.
    Theorem and_spec {Σ} (c1 c2 : context Σ)
        : prop (and c1 c2) ⊢ prop c1 ∧ prop c2.
    Proof.
        rewrite /prop.
        apply: bi.exist_elim; move => [w1 w2].
        rewrite bi.and_exist_l; apply: bi.exist_intro'.
        rewrite bi.and_exist_r; apply: bi.exist_intro'.
        clear w1 w2.
        apply: transitivity; last (
            apply: bi.and_mono;
            [ apply: (big_sepM_hetero
                (λ k _, 
                    if Variables c1 !! k is Some (P, u, constraints) 
                    then ∃ _ : (constraints : Prop), uses_prop u P 
                    else emp)%I _ 
                (Variables (and c1 c2))) => k
            | apply: (big_sepM_hetero
                (λ k _, 
                    if Variables c2 !! k is Some (P, u, constraints) 
                    then ∃ _ : (constraints : Prop), uses_prop u P 
                    else emp)%I _ 
                (Variables (and c1 c2))) => k
            ]
        ).
        - rewrite -big_sepM_and. 
            apply: big_sepM_mono => k [[P u] constraints] fact.
            apply: bi.exist_elim.
            move: fact; rewrite lookup_union_with.
            case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];
            case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];
            simpl; last done;
            move=>w; injection w; clear w;
            move=> <-<-<- w.
            + move: w => [w1 [w2 <-]].
                rewrite bi.and_exist_l; apply: bi.exist_intro'.
                rewrite bi.and_exist_r; apply: bi.exist_intro'.
                apply: uses_and_spec.
            + by rewrite bi.and_True; apply: bi.exist_intro'.
            + by rewrite bi.True_and; apply: bi.exist_intro'.
        - rewrite lookup_union_with.
            case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];
            case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];
            done.
        - rewrite lookup_union_with.
            case: (Variables c1 !! k) => [[[P1 u1] constraints1]|];
            case: (Variables c2 !! k) => [[[P2 u2] constraints2]|];
            done.
    Qed.
    Definition bind {Σ} (var : string) (ctx : context Σ) : context Σ := {|
        Variables := delete var (Variables ctx);
        Constraints := Constraints ctx ∧ 
            if Variables ctx !! var is Some (_, _, constraints)
            then constraints 
            else True;
    |}.
    Definition lookup {Σ} (var : string) (ctx : context Σ)
        : option (iProp Σ * uses)
    := option_map fst (Variables ctx !! var).
    Theorem bind_spec {Σ} var (c : context Σ)
        : match lookup var c with
            | None => emp
            | Some (P, uses) => (uses_prop uses P)
        end ∗ prop (bind var c) ⊢ 
        prop c.
    Proof.
        rewrite /prop.
        rewrite bi.sep_exist_l; apply: bi.exist_elim.
        move=> [w1 w2].
        apply: bi.exist_intro'.
        rewrite /lookup.
        move: w2.
        have: Variables c !! var = Variables c !! var by [];
            case: {-1}(Variables c !! var) => [[[P u] constraints]|] fact w2.
        - simpl.
            rewrite (big_sepM_delete _ (Variables c)); last exact fact.
            rewrite bi.sep_exist_r. apply: bi.exist_intro'.
            done.
        - simpl. 
            by rewrite bi.emp_sep delete_notin.
    Qed.
    Definition toplevel {Σ} (ctx : context Σ) : Prop :=
        if decide (Variables ctx = ∅) 
        then Constraints ctx
        else error (
            "Variables not in scope.", 
            map fst (map_to_list (Variables ctx))
        ).
    Theorem toplevel_spec {Σ} (ctx : context Σ) :
        toplevel ctx -> ⊢ prop ctx.
    Proof.
        rewrite /toplevel /prop.
        case: (decide (Variables ctx = ∅)) => [-> | _] w.
        - apply: bi.exist_intro'.
            by rewrite big_sepM_empty.
        - by apply: error_elim.
    Qed.
End context.
Inductive expr {Σ : gFunctors} : iProp Σ -> Type :=
    | Var {T} : string -> expr T
    | Lam {T1 T2} : string -> expr T2 -> expr (T1 -∗ T2)
    | Pair {T1 T2} : expr T1 -> expr T2 -> expr (T1 ∗ T2)

Fixpoint check_expr {Σ} {type : iProp Σ} (e : expr type) : context.context Σ := match e with
    | Var var => context.var var type
    | @Lam _ T1 T2 var e =>
        let ctx := check_expr e in
        context.constrain
            (match context.lookup var ctx with
                | Some (T, uses) => T = T1 ∧ uses = One
                | None => True
            end)
            (context.bind var (check_expr e))
    | Pair e1 e2 => context.sep (check_expr e1) (check_expr e2)
end.

Lemma check_expr {Σ ctx} (type : iProp Σ) : 
    expr ctx type -> prop_of_ctx ctx ⊢ type.

Lemma check_expr_spec {Σ} (type : iProp Σ) (e : expr type) : 
    context.prop (check_expr e) ⊢ type.

    elim.
    - move=> ctx1 ctx2 type1 type2 e1 fact1 e2 fact2.
        rewrite c_sep_spec.

    elim e; simpl.
    - move=> T var. apply: context.var_spec.
    - move=> T1 T2 var body H.
        apply: transitivity; first apply: context.constrain_spec.
        apply: bi.exist_elim => w.
        apply: bi.wand_intro_r.
        apply: transitivity; last apply: H.
        apply: transitivity; last apply: (context.bind_spec var).
        rewrite {1}bi.sep_comm.
        apply: bi.sep_mono_l.
        move: w; case: (context.lookup var (check_expr body)) => [[P u]|].
        + by move=>[->->].
        + move=>[]. apply: bi.True_intro.
    - move=> T1 T2 e1 H1 e2 H2.
        apply: transitivity; first apply: context.sep_spec.

    - done.
    - move=> ctx1 type1 type2 var w e fact1.
        move: (bind_spec var ctx1) w.
        case: (ctx_uses var ctx1) => [[[uses P] constraint]|].
        + case uses; last (move=> _ [_ [_ err]]; apply: (error_elim err)).
            move=> H2 [/H2 fact2 [<- []]].
            apply: bi.wand_intro_r.
            apply: transitivity.
            * apply: fact2.
            * apply: fact1.
        + move=> fact2 [].
            apply: bi.wand_intro_r.
            rewrite -[type2]bi.sep_emp.
            apply: bi.sep_mono.
            * apply: transitivity; [apply: fact2 | apply: fact1].
            * apply: bi.True_intro.

Theorem check_program {Σ} (type : iProp Σ) : 
    expr (CEmpty _) type -> ⊢ type.

Definition check_program {Σ} {type : iProp Σ} (e : expr type) : Prop :=
    context.toplevel (check_expr e).
Theorem check_program_spec {Σ} {type : iProp Σ} (e : expr type) : 
    check_program e -> ⊢ type.

    exact: check_expr.

    move=> w.
    apply: transitivity.
    - apply: context.toplevel_spec w.
    - apply: check_expr_spec.
Qed.
(* Example Proof. *)
Goal ∀ {Σ} (P Q : iProp Σ), ⊢ P -∗ P.
    move=> Σ P Q.
    apply: (check_program_spec (Lam "x" (Var "x"))).
    by vm_compute.

Goal forall {Σ} (P Q : iProp Σ), ⊢ P -∗ Q -∗ Q ∗ P.

Goal ∀ {Σ} (P Q : iProp Σ), ⊢ P -∗ Q -∗ Q ∗ P.

    by apply: (check_program (Lam "x" (Lam "y" (Pair (Var "y") (Var "x"))))).

    apply: (check_program_spec (Lam "x" (Lam "y" (Pair (Var "y") (Var "x"))))).
    by vm_compute.

(* Example Proof. *)
Goal ∀ {Σ} (P Q R : iProp Σ), ⊢ P -∗ Q -∗ R -∗ (R ∗ Q) ∗ P.
    move=> Σ P Q R.
    apply: (check_program_spec (Lam "x" (Lam "y" (Lam "z" (Pair (Pair (Var "z") (Var "y")) (Var "x")))))).
    by vm_compute.
Qed.

- Fix the performance issue.