base.v 1.67 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
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 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
From iris.algebra Require Export base.
From iris.base_logic Require Import upred.
From iris.program_logic Require Import weakestpre.
From iris.base_logic Require Import invariants.
From Autosubst Require Export Autosubst.
Import uPred.

Canonical Structure varC := leibnizC var.

Section Autosubst_Lemmas.
  Context {term : Type} {Ids_term : Ids term}
          {Rename_term : Rename term} {Subst_term : Subst term}
          {SubstLemmas_term : SubstLemmas term}.

  Lemma iter_up (m x : nat) (f : var  term) :
    upn m f x = if lt_dec x m then ids x else rename (+m) (f (x - m)).
  Proof.
    revert x; induction m as [|m IH]=> -[|x];
      repeat (case_match || asimpl || rewrite IH); auto with omega.
  Qed.
End Autosubst_Lemmas.

Ltac properness :=
  repeat match goal with
  | |- ( _: _, _)%I  ( _: _, _)%I => apply exist_proper =>?
  | |- ( _: _, _)%I  ( _: _, _)%I => apply forall_proper =>?
  | |- (_  _)%I  (_  _)%I => apply and_proper
  | |- (_  _)%I  (_  _)%I => apply or_proper
  | |- (_  _)%I  (_  _)%I => apply impl_proper
  | |- (WP _ {{ _ }})%I  (WP _ {{ _ }})%I => apply wp_proper =>?
  | |- ( _)%I  ( _)%I => apply later_proper
  | |- ( _)%I  ( _)%I => apply persistently_proper
  | |- (_  _)%I  (_  _)%I => apply sep_proper
  | |- (inv _ _)%I  (inv _ _)%I => apply (contractive_proper _)
  end.

Ltac solve_proper_alt :=
  repeat intro; (simpl + idtac);
  by repeat match goal with H : _ {_} _|- _ => rewrite H end.

Reserved Notation "⟦ τ ⟧" (at level 0, τ at level 70).
Reserved Notation "⟦ τ ⟧ₑ" (at level 0, τ at level 70).
Reserved Notation "⟦ Γ ⟧*" (at level 0, Γ at level 70).