(* In this file we explain how to do the "list examples" from the Chapter on Separation Logic for Sequential Programs in the Iris Lecture Notes, but where we use the guarded fixed point and Löb induction to define and work with the isList predicate. *) (* Contains definitions of the weakest precondition assertion, and its basic rules. *) From iris.program_logic Require Export weakestpre. (* Instantiation of Iris with the particular language. The notation file contains many shorthand notations for the programming language constructs, and the lang file contains the actual language syntax. *) From iris.heap_lang Require Export notation lang. (* Files related to the interactive proof mode. The first import includes the general tactics of the proof mode. The second provides some more specialized tactics particular to the instantiation of Iris to a particular programming language. *) From iris.proofmode Require Export tactics. From iris.heap_lang Require Import proofmode. (* The following line makes Coq check that we do not use any admitted facts / additional assumptions not in the statement of the theorems being proved. *) Set Default Proof Using "Type". (* ---------------------------------------------------------------------- *) Section list_model. (* This section contains the definition of our model of lists, i.e., definitions relating pointer data structures to our model, which is simply mathematical sequences (Coq lists). *) (* In order to do the proof we need to assume certain things about the instantiation of Iris. The particular, even the heap is handled in an analogous way as other ghost state. This line states that we assume the Iris instantiation has sufficient structure to manipulate the heap, e.g., it allows us to use the points-to predicate. *) Context `{!heapG Σ}. Implicit Types l : loc. (* The variable Σ has to do with what ghost state is available, and the type of Iris propositions (written Prop in the lecture notes) depends on this Σ. But since Σ is the same throughout the development we shall define shorthand notation which hides it. *) Notation iProp := (iProp Σ). (* First we define the is_list representation predicate via a guarded fixed point of the functional is_list_pre. Note the use of the later modality. The arrows -c> express that the arrow is an arrow in the category of COFE's, i.e., it is a non-expansive function. To fully understand the meaning of this it is necessary to understand the model of Iris. Since the type val is discrete the non-expansiveness condition is trivially satisfied in this case, and we might as well have used the ordinary arrow, but in more complex examples the domain of the predicate we are defining will not be a discrete type, and the condition will be meaningful and necessary. *) Definition is_list_pre (Φ : val -c> list val -c> iProp): val -c> list val -c> iProp := λ hd xs, match xs with [] => ⌜hd = NONEV⌝ | (x::xs) => (∃ (ℓ : loc) (hd' : val), ⌜hd = SOMEV #ℓ⌝ ∗ ℓ ↦ (x,hd') ∗ ▷ Φ hd' xs) end%I. (* To construct the fixed point we need to show that the functional we have defined is contractive. Most of the proof is automated via the f_contractive tactic. *) Local Instance is_list_pre_contractive: Contractive is_list_pre. Proof. rewrite /is_list_pre. intros n Φ Φ' Hdist hd ℓ. repeat (f_contractive || f_equiv); apply Hdist. Qed. Definition is_list_def: val → list val → iProp := fixpoint is_list_pre. Definition is_list_aux: seal (@is_list_def). by eexists. Qed. Definition is_list := unseal (@is_list_aux). Definition is_list_eq : @is_list = @is_list_def := seal_eq is_list_aux. Lemma is_list_unfold hd xs: is_list hd xs ⊣⊢ is_list_pre is_list hd xs. Proof. rewrite is_list_eq. apply (fixpoint_unfold is_list_pre). Qed. (* Exercise. Using an approach as above, given a predicate Ψ : val → iProp, define a predicate is_list_Ψ : val → iProp, where is_list_Ψ hd means that hd points to a linked list of elements, all of which satisfy Ψ. *) (* Exercise. Reprove all the specifications from lists.v using the above definition of is_list. *) End list_model.