base.v 1.67 KB
Newer Older
 Amin Timany committed Dec 14, 2017 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).``````