lists_guarded.v 4.2 KB
Newer Older
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 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
(* 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.