text:
(* autogenerated from github.com/mit-pdos/gokv/pb *)
From Perennial.goose_lang Require Import prelude.
From Goose Require github_com.mit_pdos.gokv.urpc.
From Goose Require github_com.tchajed.marshal.

From Perennial.goose_lang Require Import ffi.grove_prelude.

(* 0_common.go *)

Definition Configuration := struct.decl [
  "Replicas" :: slice.T uint64T
].

Definition EncodePBConfiguration: val :=
  rec: "EncodePBConfiguration" "p" :=
    let: "enc" := marshal.NewEnc (#8 + #8 + #8 * slice.len (struct.loadF Configuration "Replicas" "p")) in
    marshal.Enc__PutInt "enc" (slice.len (struct.loadF Configuration "Replicas" "p"));;
    marshal.Enc__PutInts "enc" (struct.loadF Configuration "Replicas" "p");;
    marshal.Enc__Finish "enc".

Definition DecodePBConfiguration: val :=
  rec: "DecodePBConfiguration" "raw_conf" :=
    let: "c" := struct.alloc Configuration (zero_val (struct.t Configuration)) in
    let: "dec" := marshal.NewDec "raw_conf" in
    struct.storeF Configuration "Replicas" "c" (marshal.Dec__GetInts "dec" (marshal.Dec__GetInt "dec"));;
    "c".

(* 1_conf.go *)

Definition VersionedValue := struct.decl [
  "ver" :: uint64T;
  "val" :: slice.T byteT
].

Definition ConfServer := struct.decl [
  "mu" :: ptrT;
  "kvs" :: mapT (struct.t VersionedValue)
].

Definition CONF_PUT : expr := #1.

Definition CONF_GET : expr := #1.

Definition PutArgs := struct.decl [
  "key" :: uint64T;
  "prevVer" :: uint64T;
  "newVal" :: slice.T byteT
].

(* MARSHAL *)
Definition EncodePutArgs: val :=
  rec: "EncodePutArgs" "args" :=
    let: "enc" := marshal.NewEnc (#8 + #8 + slice.len (struct.loadF PutArgs "newVal" "args")) in
    marshal.Enc__PutInt "enc" (struct.loadF PutArgs "key" "args");;
    marshal.Enc__PutInt "enc" (struct.loadF PutArgs "prevVer" "args");;
    marshal.Enc__PutBytes "enc" (struct.loadF PutArgs "newVal" "args");;
    marshal.Enc__Finish "enc".

(* MARSHAL *)
Definition DecodePutArgs: val :=
  rec: "DecodePutArgs" "data" :=
    let: "dec" := marshal.NewDec "data" in
    let: "args" := struct.alloc PutArgs (zero_val (struct.t PutArgs)) in
    struct.storeF PutArgs "key" "args" (marshal.Dec__GetInt "dec");;
    struct.storeF PutArgs "prevVer" "args" (marshal.Dec__GetInt "dec");;
    struct.storeF PutArgs "newVal" "args" (marshal.Dec__GetBytes "dec" (slice.len "data" - #16));;
    "args".

Definition EncodeVersionedValue: val :=
  rec: "EncodeVersionedValue" "v" :=
    let: "enc" := marshal.NewEnc (#8 + slice.len (struct.loadF VersionedValue "val" "v")) in
    marshal.Enc__PutInt "enc" (struct.loadF VersionedValue "ver" "v");;
    marshal.Enc__PutBytes "enc" (struct.loadF VersionedValue "val" "v");;
    marshal.Enc__Finish "enc".

Definition DecodeVersionedValue: val :=
  rec: "DecodeVersionedValue" "data" :=
    let: "dec" := marshal.NewDec "data" in
    let: "v" := struct.alloc VersionedValue (zero_val (struct.t VersionedValue)) in
    struct.storeF VersionedValue "ver" "v" (marshal.Dec__GetInt "dec");;
    struct.storeF VersionedValue "val" "v" (marshal.Dec__GetBytes "dec" (slice.len "data" - #8));;
    "v".

Definition ConfServer__PutRPC: val :=
  rec: "ConfServer__PutRPC" "s" "args" :=
    lock.acquire (struct.loadF ConfServer "mu" "s");;
    let: (<>, "ok") := MapGet (struct.loadF ConfServer "kvs" "s") (struct.loadF PutArgs "key" "args") in
    (if: "ok"
    then
      (if: (struct.get VersionedValue "ver" (Fst (MapGet (struct.loadF ConfServer "kvs" "s") (struct.loadF PutArgs "key" "args"))) = struct.loadF PutArgs "prevVer" "args")
      then
        MapInsert (struct.loadF ConfServer "kvs" "s") (struct.loadF PutArgs "key" "args") (struct.mk VersionedValue [
          "ver" ::= struct.loadF PutArgs "prevVer" "args" + #1;
          "val" ::= struct.loadF PutArgs "newVal" "args"
        ])
      else #())
    else
      MapInsert (struct.loadF ConfServer "kvs" "s") (struct.loadF PutArgs "key" "args") (struct.mk VersionedValue [
        "ver" ::= struct.loadF PutArgs "prevVer" "args" + #1;
        "val" ::= struct.loadF PutArgs "newVal" "args"
      ]));;
    lock.release (struct.loadF ConfServer "mu" "s");;
    #true.

Definition GetReply := struct.decl [
  "ver" :: uint64T;
  "val" :: slice.T byteT
].

Definition ConfServer__GetRPC: val :=
  rec: "ConfServer__GetRPC" "s" "key" "v" :=
    lock.acquire (struct.loadF ConfServer "mu" "s");;
    struct.store VersionedValue "v" (Fst (MapGet (struct.loadF ConfServer "kvs" "s") "key"));;
    lock.release (struct.loadF ConfServer "mu" "s");;
    #().

Definition StartConfServer: val :=
  rec: "StartConfServer" "me" :=
    let: "s" := struct.alloc ConfServer (zero_val (struct.t ConfServer)) in
    struct.storeF ConfServer "mu" "s" (lock.new #());;
    struct.storeF ConfServer "kvs" "s" (NewMap (struct.t VersionedValue) #());;
    let: "handlers" := NewMap ((slice.T byteT -> ptrT -> unitT)%ht) #() in
    MapInsert "handlers" CONF_PUT ((λ: "args" "rep",
      (if: ConfServer__PutRPC "s" (DecodePutArgs "args")
      then
        "rep" <-[slice.T byteT] NewSlice byteT #1;;
        #()
      else
        "rep" <-[slice.T byteT] NewSlice byteT #0;;
        #())
      ));;
    MapInsert "handlers" CONF_GET ((λ: "args" "rep",
      let: "v" := struct.alloc VersionedValue (zero_val (struct.t VersionedValue)) in
      ConfServer__GetRPC "s" (UInt64Get "args") "v";;
      #()
      ));;
    let: "r" := urpc.MakeServer "handlers" in
    urpc.Server__Serve "r" "me";;
    #().

Definition ConfClerk := struct.decl [
  "cl" :: ptrT
].

Definition ConfClerk__Put: val :=
  rec: "ConfClerk__Put" "c" "key" "prevVer" "newVal" :=
    let: "raw_reply" := ref (zero_val (slice.T byteT)) in
    let: "raw_args" := EncodePutArgs (struct.new PutArgs [
      "key" ::= "key";
      "prevVer" ::= "prevVer";
      "newVal" ::= "newVal"
    ]) in
    let: "err" := urpc.Client__Call (struct.loadF ConfClerk "cl" "c") CONF_PUT "raw_args" "raw_reply" #100 in
    (if: ("err" = #0)
    then slice.len (![slice.T byteT] "raw_reply") > #0
    else #false).

Definition ConfClerk__Get: val :=
  rec: "ConfClerk__Get" "c" "key" :=
    let: "raw_reply" := ref (zero_val (slice.T byteT)) in
    let: "raw_args" := NewSlice byteT #8 in
    UInt64Put "raw_args" "key";;
    let: "err" := urpc.Client__Call (struct.loadF ConfClerk "cl" "c") CONF_GET "raw_args" "raw_reply" #100 in
    (if: ("err" = #0)
    then DecodeVersionedValue (![slice.T byteT] "raw_reply")
    else
      control.impl.Assume #false;;
      slice.nil).

Definition MakeConfClerk: val :=
  rec: "MakeConfClerk" "confServer" :=
    struct.new ConfClerk [
      "cl" ::= urpc.MakeClient "confServer"
    ].

(* 2_replica_clerk.go *)

Definition REPLICA_APPEND : expr := #0.

Definition REPLICA_GETLOG : expr := #1.

Definition REPLICA_BECOMEPRIMARY : expr := #2.

Definition REPLICA_HEARTBEAT : expr := #3.

Definition AppendArgs := struct.decl [
  "cn" :: uint64T;
  "commitIdx" :: uint64T;
  "log" :: slice.T byteT
].

Definition EncodeAppendArgs: val :=
  rec: "EncodeAppendArgs" "args" :=
    let: "enc" := marshal.NewEnc (#16 + slice.len (struct.loadF AppendArgs "log" "args")) in
    marshal.Enc__PutInt "enc" (struct.loadF AppendArgs "cn" "args");;
    marshal.Enc__PutInt "enc" (struct.loadF AppendArgs "commitIdx" "args");;
    marshal.Enc__PutBytes "enc" (struct.loadF AppendArgs "log" "args");;
    marshal.Enc__Finish "enc".

Definition DecodeAppendArgs: val :=
  rec: "DecodeAppendArgs" "raw_args" :=
    let: "a" := struct.alloc AppendArgs (zero_val (struct.t AppendArgs)) in
    let: "dec" := marshal.NewDec "raw_args" in
    struct.storeF AppendArgs "cn" "a" (marshal.Dec__GetInt "dec");;
    struct.storeF AppendArgs "commitIdx" "a" (marshal.Dec__GetInt "dec");;
    struct.storeF AppendArgs "log" "a" (marshal.Dec__GetBytes "dec" (slice.len "raw_args" - #16));;
    "a".

Definition BecomePrimaryArgs := struct.decl [
  "Cn" :: uint64T;
  "Conf" :: ptrT
].

Definition EncodeBecomePrimaryArgs: val :=
  rec: "EncodeBecomePrimaryArgs" "args" :=
    let: "encodedConf" := EncodePBConfiguration (struct.loadF BecomePrimaryArgs "Conf" "args") in
    let: "enc" := marshal.NewEnc (#8 + slice.len "encodedConf") in
    marshal.Enc__PutInt "enc" (struct.loadF BecomePrimaryArgs "Cn" "args");;
    marshal.Enc__PutBytes "enc" "encodedConf";;
    marshal.Enc__Finish "enc".

Definition DecodeBecomePrimaryArgs: val :=
  rec: "DecodeBecomePrimaryArgs" "raw_args" :=
    let: "a" := struct.alloc BecomePrimaryArgs (zero_val (struct.t BecomePrimaryArgs)) in
    let: "dec" := marshal.NewDec "raw_args" in
    struct.storeF BecomePrimaryArgs "Cn" "a" (marshal.Dec__GetInt "dec");;
    struct.storeF BecomePrimaryArgs "Conf" "a" (DecodePBConfiguration (SliceSkip byteT "raw_args" #8));;
    "a".

Definition ReplicaClerk := struct.decl [
  "cl" :: ptrT
].

Definition ReplicaClerk__AppendRPC: val :=
  rec: "ReplicaClerk__AppendRPC" "ck" "args" :=
    let: "raw_args" := EncodeAppendArgs "args" in
    let: "reply" := ref (zero_val (slice.T byteT)) in
    let: "err" := urpc.Client__Call (struct.loadF ReplicaClerk "cl" "ck") REPLICA_APPEND "raw_args" "reply" #100 in
    (if: ("err" = #0) && (slice.len (![slice.T byteT] "reply") > #0)
    then #true
    else #false).

Definition ReplicaClerk__BecomePrimaryRPC: val :=
  rec: "ReplicaClerk__BecomePrimaryRPC" "ck" "args" :=
    let: "raw_args" := EncodeBecomePrimaryArgs "args" in
    let: "reply" := ref (zero_val (slice.T byteT)) in
    let: "err" := urpc.Client__Call (struct.loadF ReplicaClerk "cl" "ck") REPLICA_BECOMEPRIMARY "raw_args" "reply" #20000 in
    control.impl.Assume ("err" = #0);;
    #().

Definition ReplicaClerk__HeartbeatRPC: val :=
  rec: "ReplicaClerk__HeartbeatRPC" "ck" :=
    let: "reply" := ref (zero_val (slice.T byteT)) in
    (urpc.Client__Call (struct.loadF ReplicaClerk "cl" "ck") REPLICA_HEARTBEAT (NewSlice byteT #0) "reply" #1000 = #0).

Definition MakeReplicaClerk: val :=
  rec: "MakeReplicaClerk" "host" :=
    let: "ck" := struct.alloc ReplicaClerk (zero_val (struct.t ReplicaClerk)) in
    struct.storeF ReplicaClerk "cl" "ck" (urpc.MakeClient "host");;
    "ck".

(* 3_replica.go *)

Definition LogEntry: ty := byteT.

Definition ReplicaServer := struct.decl [
  "mu" :: ptrT;
  "cn" :: uint64T;
  "conf" :: ptrT;
  "isPrimary" :: boolT;
  "replicaClerks" :: slice.T ptrT;
  "opLog" :: slice.T LogEntry;
  "commitIdx" :: uint64T;
  "commitCond" :: ptrT;
  "matchIdx" :: slice.T uint64T
].

Definition min: val :=
  rec: "min" "l" :=
    let: "m" := ref_to uint64T #18446744073709551615 in
    ForSlice uint64T <> "v" "l"
      ((if: "v" < ![uint64T] "m"
      then "m" <-[uint64T] "v"
      else #()));;
    ![uint64T] "m".

Definition ReplicaServer__postAppendRPC: val :=
  rec: "ReplicaServer__postAppendRPC" "s" "i" "args" :=
    lock.acquire (struct.loadF ReplicaServer "mu" "s");;
    (if: (struct.loadF ReplicaServer "cn" "s" = struct.loadF AppendArgs "cn" "args")
    then
      (if: SliceGet uint64T (struct.loadF ReplicaServer "matchIdx" "s") "i" < slice.len (struct.loadF AppendArgs "log" "args")
      then
        SliceSet uint64T (struct.loadF ReplicaServer "matchIdx" "s") "i" (slice.len (struct.loadF AppendArgs "log" "args"));;
        let: "m" := min (struct.loadF ReplicaServer "matchIdx" "s") in
        (if: "m" > struct.loadF ReplicaServer "commitIdx" "s"
        then struct.storeF ReplicaServer "commitIdx" "s" "m"
        else #())
      else #())
    else #());;
    lock.release (struct.loadF ReplicaServer "mu" "s");;
    #().

(* This should be invoked locally by services to attempt appending op to the
   log *)
Definition ReplicaServer__StartAppend: val :=
  rec: "ReplicaServer__StartAppend" "s" "op" :=
    lock.acquire (struct.loadF ReplicaServer "mu" "s");;
    (if: ~ (struct.loadF ReplicaServer "isPrimary" "s")
    then
      lock.release (struct.loadF ReplicaServer "mu" "s");;
      #false
    else
      struct.storeF ReplicaServer "opLog" "s" (SliceAppend byteT (struct.loadF ReplicaServer "opLog" "s") "op");;
      SliceSet uint64T (struct.loadF ReplicaServer "matchIdx" "s") #0 (slice.len (struct.loadF ReplicaServer "opLog" "s"));;
      let: "clerks" := struct.loadF ReplicaServer "replicaClerks" "s" in
      let: "args" := struct.new AppendArgs [
        "cn" ::= struct.loadF ReplicaServer "cn" "s";
        "log" ::= struct.loadF ReplicaServer "opLog" "s";
        "commitIdx" ::= struct.loadF ReplicaServer "commitIdx" "s"
      ] in
      lock.release (struct.loadF ReplicaServer "mu" "s");;
      ForSlice ptrT "i" "ck" "clerks"
        (let: "ck" := "ck" in
        let: "i" := "i" in
        Fork (ReplicaClerk__AppendRPC "ck" "args";;
              ReplicaServer__postAppendRPC "s" ("i" + #1) "args"));;
      #true).

Definition ReplicaServer__GetCommittedLog: val :=
  rec: "ReplicaServer__GetCommittedLog" "s" :=
    lock.acquire (struct.loadF ReplicaServer "mu" "s");;
    let: "r" := SliceTake (struct.loadF ReplicaServer "opLog" "s") (struct.loadF ReplicaServer "commitIdx" "s") in
    lock.release (struct.loadF ReplicaServer "mu" "s");;
    "r".

Definition ReplicaServer__AppendRPC: val :=
  rec: "ReplicaServer__AppendRPC" "s" "args" :=
    lock.acquire (struct.loadF ReplicaServer "mu" "s");;
    (if: struct.loadF ReplicaServer "cn" "s" > struct.loadF AppendArgs "cn" "args"
    then
      lock.release (struct.loadF ReplicaServer "mu" "s");;
      #false
    else
      (if: (struct.loadF ReplicaServer "cn" "s" < struct.loadF AppendArgs "cn" "args") || (slice.len (struct.loadF AppendArgs "log" "args") > slice.len (struct.loadF ReplicaServer "opLog" "s"))
      then
        struct.storeF ReplicaServer "opLog" "s" (struct.loadF AppendArgs "log" "args");;
        struct.storeF ReplicaServer "cn" "s" (struct.loadF AppendArgs "cn" "args")
      else #());;
      (if: struct.loadF AppendArgs "commitIdx" "args" > struct.loadF ReplicaServer "commitIdx" "s"
      then struct.storeF ReplicaServer "commitIdx" "s" (struct.loadF AppendArgs "commitIdx" "args")
      else #());;
      struct.storeF ReplicaServer "isPrimary" "s" #false;;
      lock.release (struct.loadF ReplicaServer "mu" "s");;
      #true).

(* controller tells the primary to become the primary, and gives it the config *)
Definition ReplicaServer__BecomePrimaryRPC: val :=
  rec: "ReplicaServer__BecomePrimaryRPC" "s" "args" :=
    lock.acquire (struct.loadF ReplicaServer "mu" "s");;
    (* log.Printf("Becoming primary in %d, %+v", args.Cn, args.Conf.Replicas) *)
    (if: struct.loadF ReplicaServer "cn" "s" ≥ struct.loadF BecomePrimaryArgs "Cn" "args"
    then
      lock.release (struct.loadF ReplicaServer "mu" "s");;
      #()
    else
      (if: (struct.loadF BecomePrimaryArgs "Cn" "args" > struct.loadF ReplicaServer "cn" "s" + #1) && (struct.loadF ReplicaServer "cn" "s" = #0)
      then
        control.impl.Assume #false;;
        #()
      else
        struct.storeF ReplicaServer "isPrimary" "s" #true;;
        struct.storeF ReplicaServer "cn" "s" (struct.loadF BecomePrimaryArgs "Cn" "args");;
        struct.storeF ReplicaServer "matchIdx" "s" (NewSlice uint64T (slice.len (struct.loadF Configuration "Replicas" (struct.loadF BecomePrimaryArgs "Conf" "args"))));;
        struct.storeF ReplicaServer "replicaClerks" "s" (NewSlice ptrT (slice.len (struct.loadF Configuration "Replicas" (struct.loadF BecomePrimaryArgs "Conf" "args")) - #1));;
        ForSlice ptrT "i" <> (struct.loadF ReplicaServer "replicaClerks" "s")
          (SliceSet ptrT (struct.loadF ReplicaServer "replicaClerks" "s") "i" (MakeReplicaClerk (SliceGet uint64T (struct.loadF Configuration "Replicas" (struct.loadF BecomePrimaryArgs "Conf" "args")) ("i" + #1))));;
        lock.release (struct.loadF ReplicaServer "mu" "s");;
        #())).

(* used for recovery/adding a new node into the system *)
Definition ReplicaServer__GetCommitLogRPC: val :=
  rec: "ReplicaServer__GetCommitLogRPC" "s" <> "reply" :=
    lock.acquire (struct.loadF ReplicaServer "mu" "s");;
    "reply" <-[slice.T byteT] SliceTake (struct.loadF ReplicaServer "opLog" "s") (struct.loadF ReplicaServer "commitIdx" "s");;
    lock.release (struct.loadF ReplicaServer "mu" "s");;
    #().

Definition StartReplicaServer: val :=
  rec: "StartReplicaServer" "me" :=
    let: "s" := struct.alloc ReplicaServer (zero_val (struct.t ReplicaServer)) in
    struct.storeF ReplicaServer "mu" "s" (lock.new #());;
    struct.storeF ReplicaServer "opLog" "s" (NewSlice LogEntry #0);;
    struct.storeF ReplicaServer "commitIdx" "s" #0;;
    struct.storeF ReplicaServer "cn" "s" #0;;
    struct.storeF ReplicaServer "isPrimary" "s" #false;;
    let: "handlers" := NewMap ((slice.T byteT -> ptrT -> unitT)%ht) #() in
    MapInsert "handlers" REPLICA_APPEND ((λ: "raw_args" "raw_reply",
      let: "a" := DecodeAppendArgs "raw_args" in
      (if: ReplicaServer__AppendRPC "s" "a"
      then
        "raw_reply" <-[slice.T byteT] NewSlice byteT #1;;
        #()
      else
        "raw_reply" <-[slice.T byteT] NewSlice byteT #0;;
        #())
      ));;
    MapInsert "handlers" REPLICA_GETLOG (ReplicaServer__GetCommitLogRPC "s");;
    MapInsert "handlers" REPLICA_BECOMEPRIMARY ((λ: "raw_args" "raw_reply",
      ReplicaServer__BecomePrimaryRPC "s" (DecodeBecomePrimaryArgs "raw_args");;
      #()
      ));;
    MapInsert "handlers" REPLICA_HEARTBEAT ((λ: <> <>,
      #()
      ));;
    let: "r" := urpc.MakeServer "handlers" in
    urpc.Server__Serve "r" "me";;
    "s".

author: mit-pdos

repo: perennial

save_path: github-repos/coq/mit-pdos-perennial


text:
Require Import ReflParam.common.
Require Import ReflParam.templateCoqMisc.
Require Import String.
Require Import List.
Require Import Template.Ast.
Require Import SquiggleEq.terms.
Require Import ReflParam.paramDirect ReflParam.indType.
Require Import SquiggleEq.substitution.
Require Import ReflParam.PiTypeR.
Import ListNotations.
Require Import squiggle5.
Open Scope string_scope.
Require Import Coq.btauto.Btauto.
Require Import SquiggleEq.LibTactics.

Lemma nat_R_Refl (n:nat):
  Coq_Init_Datatypes_nat_pmtcty_RR0 n n.
Proof using.
  induction n; simpl;[constructor|].
  exists IHn. constructor.
Defined.

Require Import ReflParam.Trecord.
Require Import SquiggleEq.terms2.
Require Import SquiggleEq.varImplZ.
Require Import SquiggleEq.wftermSet.

Inductive Opid : Set :=
| lam
| app
| num (n:nat).

Definition V := BinNums.positive.
(** using a library that generically defines substitution and alpha equality: https://github.com/aa755/SquiggleEq *)
Definition Tm : Set := @NTerm V Opid (* for unextracted efficiency, not carrying the proof of well formedness. e.g. [oterm lam []] is allowed *).
Definition BTm : Set := (V*Tm).

Definition elimTerm (t:Tm) :  TmKind Tm BTm :=
match t with
| vterm _ => evar
| oterm o lbt=>
  match o, lbt with
  | lam, [(bterm [v] t)] => elam (v,t)
  | app, [bterm [] f; bterm [] a] => eapp f a
  | num n, [] => enum n
  | _,_ => evar
  (* ill-formed term. from the point of view of evaluation
    (only closed terms) and observational equivalence,
      there is no difference between variables and garbage terms.*)
  end
end.

Definition applyBtm (b:BTm) (u:Tm) :  Tm:=
  let (v,t) := b in (subst t v u).

Require Import SquiggleEq.alphaeq.

Module alphaInst.

Definition Tm_R (t1 t2 :Tm) : Prop:= alpha_eq t1 t2.

Definition BTm_R (bt1 bt2 :BTm) : Prop:=
  let (v1, t1) := bt1 in
  let (v2, t2) := bt2 in
  alpha_eq_bterm (bterm [v1] t1) (bterm [v2] t2).

Lemma totalTm_R : TotalHeteroRel Tm_R.
  split;  intros x; exists x; apply alpha_eq_refl.
Defined.

(** The strong isorel translation reduces away this requirement
Lemma totalBTm_R : TotalHeteroRel BTm_R.
  split;  intros x; exists x; destruct x; apply alphaeqbt_refl.
Defined.
*)

Require Import SquiggleEq.list.

(** show that the the interface operations respect the relation *)

(** on alpha equal terms, elimTerm returns related answers *)
Lemma elimTerm_R :
   (forall (a1 : Tm) (a2 : Tm),
        Tm_R a1 a2 ->
        Top_squiggle5_TmKind_pmtcty_RR0 Tm Tm Tm_R BTm BTm BTm_R (elimTerm a1) (elimTerm a2)).
Proof using.
  intros ? ? Hr.
  hnf in Hr.
  inverts Hr.
  - constructor.
  - rename H into Hlen. rename H0 into Hb.
    destruct op; simpl.
    + destruct lbt1 as [| b lbt1]; simpl in *;
        dlist_len_name lbt2 b2;[constructor|].
      destruct b as [lv nt].
      alphahypsd2.
      destruct b2 as [lv2 nt2].
      pose proof Hb0bt as Hblen.
      apply alpha_eq_bterm_lenbvars in Hblen.
      destruct lv as [| v lv]; simpl in *;
        dlist_len_name lv2 v2;[ constructor |].
      destruct lv as [|]; simpl in *;
        dlist_len_name lv2 vv;[ | constructor].
      destruct lbt1 as [|]; simpl in *;
        dlist_len_name lbt2 b2;[constructor|]; auto; try constructor.

    + destruct lbt1 as [| b lbt1]; simpl in *;
        dlist_len_name lbt2 b2;[constructor|].
      destruct b as [lv nt].
      alphahypsd2.
      destruct b2 as [lv2 nt2].
      pose proof Hb0bt as Hblen.
      apply alpha_eq_bterm_lenbvars in Hblen.
      destruct lv as [|]; simpl in *;
        dlist_len_name lv2 vv;[ | constructor].
      destruct lbt1 as [| al lbt1]; simpl in *;
        dlist_len_name lbt2 ar;[constructor|]; auto; try constructor.
      destruct al as [alvl al].
      destruct ar as [arvl ar].
      unfold tactics.ltac_something in Hb.
      alphahypsd3.
      alphahypsd2.
      alphahypsd3.
      pose proof Hb1bt as Hblen.
      apply alpha_eq_bterm_lenbvars in Hblen.
      destruct alvl as [|]; simpl in *;
        dlist_len_name arvl vv;[ | constructor].
      alphahypsd3.
      destruct lbt1 as [|]; simpl in *;
        dlist_len_name lbt2 ar;[constructor|]; auto; try constructor; auto; constructor.
    + destruct lbt1 as [|]; simpl in *;
      dlist_len_name lbt2 ar;[constructor|];
         auto; try constructor; auto; try constructor.
      exact (nat_R_Refl n).
Qed.

Lemma applyBTerm_R :
(forall (a1 : BTm) (a2 : BTm),
        BTm_R a1 a2 ->
        forall (a3 : Tm) (a4 : Tm), Tm_R a3 a4 -> Tm_R (applyBtm a1 a3) (applyBtm a2 a4)).
Proof using.
  intros.
  destruct a1 as [? sl].
  destruct a2 as [? sr].
  unfold Tm_R in *.
  simpl in *.
  apply apply_bterm_alpha_congr  with (lnt1 := [a3]) (lnt2 := [a4]) in H; auto.
  prove_bin_rel_nterm.
Qed.

(** Above, we showed that all operations in the interface respect the relation alpha
equality. Now, we are ready to get the free theorem *)

Require Import ReflParam.Trecord.

Require Import squiggle5StrongIso.

Lemma obsEqRespectsAlpha :
forall tl tl₂ : Tm,
Tm_R tl tl₂ ->
forall tr tr₂ : Tm,
Tm_R tr tr₂ ->
obseq Tm BTm applyBtm elimTerm tl tr <->
obseq Tm BTm applyBtm elimTerm tl₂ tr₂.
Proof using.
 intros.
 apply IsoRel_implies_iff.
 apply (obseqStrongIso _ _ Tm_R totalTm_R _ _ BTm_R _ _ applyBTerm_R _ _ elimTerm_R);
   assumption.
Qed.

End alphaInst.

repo: paramcoq-iff


text:
Require Import Reals.
Local Open Scope R_scope.
From ValidSDP Require Import validsdp.

Let p (x0 x1 x2 x3 x4 x5 : R) :=
  -4/1
  * (x3 * x3 * x0 + 8/1 * (x4 - x5) * (x1 - x2)
     - x3 * (16/1 * x0 + (x4 - 8/1) * x1 + (x5 - 8/1) * x2)).

Let b1 (x0 x1 x2 x3 x4 x5 : R) :=
  (x0 - 1) * (117547965573/100000000000 - x0).

Let b2 (x0 x1 x2 x3 x4 x5 : R) :=
  (x1 - 1) * (117547965573/100000000000 - x1).

Let b3 (x0 x1 x2 x3 x4 x5 : R) :=
  (x2 - 1) * (117547965573/100000000000 - x2).

Let b4 (x0 x1 x2 x3 x4 x5 : R) :=
  (x3 - 251952632905/100000000000) * (63504/10000 - x3).

Let b5 (x0 x1 x2 x3 x4 x5 : R) :=
  (x4 - 251952632905/100000000000) * (90601/10000 - x4).

Let b6 (x0 x1 x2 x3 x4 x5 : R) :=
  (x5 - 56644/10000) * (16/1 - x5).

Theorem p_nonneg (x0 x1 x2 x3 x4 x5 : R) :
  b1 x0 x1 x2 x3 x4 x5 >= 0 ->
  b2 x0 x1 x2 x3 x4 x5 >= 0 ->
  b3 x0 x1 x2 x3 x4 x5 >= 0 ->
  b4 x0 x1 x2 x3 x4 x5 >= 0 ->
  b5 x0 x1 x2 x3 x4 x5 >= 0 ->
  b6 x0 x1 x2 x3 x4 x5 >= 0 ->
  p x0 x1 x2 x3 x4 x5 >= 0.
Proof.
unfold b1, b2, b3, b4, b5, b6, p.
validsdp.
Qed.

author: validsdp

repo: validsdp

save_path: github-repos/coq/validsdp-validsdp


text:
Require Import Coq.Classes.EquivDec.
Require Import Coq.Lists.List.
Require Import Coq.Program.Equality.
From Equations Require Import Equations.
Import ListNotations.

Set Universe Polymorphism.

Definition signature (K: Type) : Type :=
  list (K * Type).

Section HAList.
  Context {K: Type}.
  Context `{KEqDec: EquivDec.EqDec K eq}.

  Notation signature := (signature K).

  Inductive key : signature -> Type -> Type :=
  | KHd: forall k t s, key ((k, t)::s) t
  | KTl: forall h t s, key s t -> key (h::s) t.
  Derive Signature for key.

  Inductive t: signature -> Type :=
  | REmp: t []
  | RCons: forall {k typ rest} (x:typ),
      t rest ->
      t ((k, typ)::rest).

  Equations get_k {T} {sig: signature} : t sig -> key sig T -> T :=
    {
      get_k (RCons val _) (KHd _ _ _)     := val;
      get_k (RCons _ rec') (KTl _ _ _ pf) := get_k rec' pf
    }.

  Equations set_k {T} {sig: signature} : t sig -> key sig T -> T -> t sig :=
    {
      set_k (RCons val rec) (KHd _ _ _) val'     := RCons val' rec;
      set_k (RCons val rec') (KTl _ _ _ pf) val' := RCons val (set_k rec' pf val')
    }.

  Inductive key_exists : signature -> K -> Type :=
  | KEHd: forall k t sig', key_exists ((k, t)::sig') k
  | KETl: forall k h sig', key_exists sig' k -> key_exists (h::sig') k.

  Equations get_key_type {sig: signature} {k: K} : key_exists sig k -> {T: Type & key sig T} :=
    {
      get_key_type (KEHd k t sig') := existT (key ((k, t)::sig')) t (KHd k t _);
      get_key_type (KETl k h sig' ke') :=
        let '(existT _ t key_rest) := get_key_type ke' in
        existT (key (h::sig')) t (KTl h t _ key_rest)
    }.

  Fixpoint alist_In {A} (k: K) (l: list (K * A)) :=
    match l with
    | (k0, x0) :: l =>
      if KEqDec k0 k
      then True
      else alist_In k l
    | [] => False
    end.

  Definition valid_key {A} (l: list (K * A)) :=
    {k: K | alist_In k l}.

  Definition mk_key {sig: signature} (k: valid_key sig) : key_exists sig (proj1_sig k).
  Proof.
    induction sig as [|[k' T] sig].
    - cbv in k.
      exfalso.
      exact (proj2_sig k).
    - destruct k as [k HIn].
      pose proof (g := HIn).
      simpl in g.
      destruct (KEqDec k' k).
      + unfold equiv in *.
        subst.
        apply KEHd.
      + apply KETl.
        set (Hvalid := exist (fun k => alist_In k sig) k g).
        specialize (IHsig Hvalid).
        eauto.
  Defined.

  Definition get {sig: signature} (rec: t sig) (k: valid_key sig) : (projT1 (get_key_type (mk_key k))) :=
    get_k rec (projT2 (get_key_type (mk_key k))).

  Definition set {sig: signature} (rec: t sig) (k: valid_key sig) (v: (projT1 (get_key_type (mk_key k)))) : t sig :=
    set_k rec (projT2 (get_key_type (mk_key k))) v.

End HAList.

author: verified-network-toolchain

repo: leapfrog


text:
(* Copyright 2022 <anonymized> *)

(* ON SEPARATION LOGIC *)
(* Author: <anonymized> *)

Require Export OnSeparationLogic.Heap.

Module Language (Export HS: HeapSig).

Module H := HeapFacts HS.
Include H.

(* ========= *)
(* VARIABLES *)
(* ========= *)

Definition V := nat.
Definition dummy: V := 0.

(* ========================================= *)
(* FRESHNESS OF VARIABLES AND ITS PROPERTIES *)
(* ========================================= *)

Fixpoint maximum (xs: list V): V :=
  match xs with
  | nil => dummy
  | (x::xs) => max x (maximum xs)
  end.
Proposition maximum_prop (xs: list V):
  forall x, In x xs -> x <= maximum xs.
intros. induction xs. inversion H.
simpl. destruct H.
rewrite H.
apply Nat.le_max_l.
destruct (le_gt_dec a (maximum xs)).
rewrite max_r; try assumption.
apply IHxs; assumption.
unfold gt in g.
apply Nat.lt_le_incl in g.
rewrite max_l; try assumption.
eapply le_trans.
apply IHxs; assumption.
assumption.
Qed.
Proposition maximum_In (xs: list V):
  xs <> nil -> In (maximum xs) xs.
intro. destruct xs.
exfalso; apply H; reflexivity.
induction xs.
simpl. left. unfold dummy.
rewrite Nat.max_0_r; reflexivity.
simpl.
assert (In (maximum (v :: xs)) (v :: xs)).
  apply IHxs. intro. inversion H0. clear IHxs.
inversion H0. simpl in H1.
destruct (Nat.max_dec a (maximum xs)).
rewrite e.
destruct (Nat.max_dec v a).
left. auto.
right. left. auto.
left. rewrite e. auto.
destruct (Nat.max_dec a (maximum xs)).
rewrite e.
destruct (Nat.max_dec v a).
left. auto.
right. left. auto.
rewrite e.
right. right. apply H1.
Qed.

Proposition maximum_app (xs ys: list V):
  maximum (xs ++ ys) = max (maximum xs) (maximum ys).
induction xs; simpl. reflexivity.
rewrite IHxs.
apply Nat.max_assoc.
Qed.

Proposition maximum_subset (xs zs: list V):
  (forall x : V, In x xs -> In x zs) -> maximum xs <= maximum zs.
intro. destruct xs.
simpl. unfold dummy.
apply Nat.le_0_l.
pose proof (maximum_prop zs).
pose proof (maximum_In (v :: xs)).
apply H0. apply H. apply H1. intro. inversion H2.
Qed.

Definition fresh (xs: list V): V := S (maximum xs).
Proposition fresh_prop (xs: list V):
  forall x, In x xs -> x < fresh xs.
unfold fresh.
intros. apply le_lt_n_Sm.
apply maximum_prop; assumption.
Qed.
Proposition fresh_notIn (xs: list V):
  ~In (fresh xs) xs.
intro.
pose proof (fresh_prop xs).
specialize H0 with (fresh xs).
specialize (H0 H).
eapply Nat.lt_irrefl. apply H0.
Qed.

Proposition fresh_app (xs ys: list V):
  fresh (xs ++ ys) = max (fresh xs) (fresh ys).
unfold fresh.
rewrite maximum_app.
simpl. reflexivity.
Qed.

Proposition fresh_notInApp (xs ys: list V):
  ~In (fresh (xs ++ ys)) xs.
rewrite fresh_app.
destruct (Nat.max_dec (fresh xs) (fresh ys)).
rewrite e. apply fresh_notIn.
rewrite e.
pose proof (Max.le_max_l (fresh xs) (fresh ys)).
rewrite e in H.
destruct (Nat.eq_dec (fresh xs) (fresh ys)).
rewrite <- e0. apply fresh_notIn.
apply Nat.le_lteq in H. destruct H. clear n.
intro.
apply fresh_prop in H0.
eapply Nat.lt_irrefl.
eapply Nat.lt_trans. apply H. apply H0.
exfalso. apply n. assumption.
Qed.

Proposition fresh_notInGeneral (xs zs: list V):
  (forall x, In x xs -> In x zs) -> ~In (fresh zs) xs.
intro.
apply maximum_subset in H.
unfold fresh.
intro.
apply maximum_prop in H0.
eapply le_trans in H; [|apply H0].
eapply Nat.nle_succ_diag_l. apply H.
Qed.

(* =========================================== *)
(* THE STORE, STORE UPDATE, AND ITS PROPERTIES *)
(* =========================================== *)

Definition store := V -> Z.

Definition store_update (s: store) (x: V) (v: Z): store :=
  fun y => if Nat.eq_dec x y then v else s y.

Proposition store_update_lookup_same (s: store) (x: V) (v: Z):
  store_update s x v x = v.
unfold store_update.
destruct (Nat.eq_dec x x).
reflexivity.
exfalso. apply n. reflexivity.
Qed.

Proposition store_update_lookup_diff (s: store) (x x': V) (v: Z):
  x <> x' -> store_update s x v x' = s x'.
intros. unfold store_update.
destruct (Nat.eq_dec x x').
exfalso. apply H; assumption.
reflexivity.
Qed.

Proposition store_update_id (s: store) (x: V):
  store_update s x (s x) = s.
apply functional_extensionality; intro.
unfold store_update.
destruct (Nat.eq_dec x x0).
rewrite e; reflexivity.
reflexivity.
Qed.

Proposition store_update_collapse (s: store) (x: V) (v w: Z):
  (store_update (store_update s x v) x w) =
  (store_update s x w).
apply functional_extensionality; intro z.
unfold store_update.
destruct (Nat.eq_dec x z); reflexivity.
Qed.

Proposition store_update_swap (s: store) (e: Z) (x y: V) (v: Z):
  x <> y ->
  (store_update (store_update s x e) y v) =
  (store_update (store_update s y v) x e).
intros G; apply functional_extensionality; intro z.
unfold store_update.
destruct (Nat.eq_dec y z); destruct (Nat.eq_dec x z); try reflexivity.
exfalso. apply G. rewrite e0; rewrite e1. reflexivity.
Qed.

Definition eq_restr (s t: store) (z: list V): Prop :=
  forall (x: V), In x z -> s x = t x.

Proposition eq_restr_split (s t: store) (xs ys: list V):
  eq_restr s t (xs ++ ys) -> eq_restr s t xs /\ eq_restr s t ys.
unfold eq_restr; intro; split; intros;
apply H; apply in_or_app; auto.
Qed.

Proposition eq_restr_comm (s t: store) (xs: list V):
  eq_restr s t xs -> eq_restr t s xs.
unfold eq_restr; intros; symmetry; apply H; assumption.
Qed.

(* ====================== *)
(* EXPRESSIONS AND GUARDS *)
(* ====================== *)

(* Expressions and guards are shallow, but finitely based *)
Record expr: Set := mkexpr {
  eval: store -> Z;
  evar: list V;
  econd: forall (s t: store), eq_restr s t evar -> eval s = eval t
}.
Coercion eval: expr >-> Funclass.

Proposition const_expr_cond (v: Z) (s t : store):
  eq_restr s t nil -> v = v.
intros. reflexivity.
Qed.
Definition const_expr (v: Z): expr :=
  mkexpr (fun s => v) nil (const_expr_cond v).
Coercion const_expr: Z >-> expr.
Proposition var_expr_cond (x: V) (s t : store):
  eq_restr s t (x :: nil) -> s x = t x.
intro. unfold eq_restr in H.
specialize H with x. apply H.
left. reflexivity.
Qed.
Definition var_expr (x: V): expr :=
  mkexpr (fun s => s x) (x :: nil) (var_expr_cond x).
Coercion var_expr: V >-> expr.

Proposition eval_store_update_notInVar (s: store) (e: expr) (x: V) (v: Z):
  ~ In x (evar e) ->
  e s = e (store_update s x v).
intro. apply econd.
intro; intro. unfold store_update.
destruct (Nat.eq_dec x x0).
exfalso; apply H; rewrite e0; assumption.
reflexivity.
Qed.

Proposition esub_cond (e: expr) (x: V) (e': expr) (s t : store):
  eq_restr s t (remove Nat.eq_dec x (evar e) ++ evar e') ->
  eval e (store_update s x (eval e' s)) =
    eval e (store_update t x (eval e' t)).
intro.
assert (eval e' s = eval e' t).
apply (econd e').
intro; intro; apply H.
apply in_or_app; right; assumption.
rewrite <- H0.
unfold store_update.
apply (econd e).
unfold eq_restr.
intro; intro.
destruct (Nat.eq_dec x x0).
reflexivity.
apply H; apply in_or_app; left.
apply In_remove; assumption.
Qed.
Definition esub (e: expr) (x: V) (e': expr): expr :=
  mkexpr (fun s => eval e (store_update s x (eval e' s)))
    (remove Nat.eq_dec x (evar e) ++ evar e') (esub_cond e x e').

Proposition esub_simpl (e: expr) (x: V) (e': expr):
  ~In x (evar e) -> forall s, eval (esub e x e') s = eval e s.
intros. simpl.
apply econd. intro. intro.
unfold store_update.
destruct (Nat.eq_dec x x0).
exfalso. apply H. rewrite e0. assumption.
reflexivity.
Qed.

Proposition esub_notInVar (e: expr) (x: V) (e': expr):
  ~In x (evar e') -> ~ In x (evar (esub e x e')).
intros; simpl; intro.
apply in_app_or in H0; destruct H0.
eapply remove_In; apply H0.
apply H; auto.
Qed.

Proposition expr_eq (e1 e2: expr):
  (eval e1 = eval e2) -> (evar e1 = evar e2) -> e1 = e2.
intros. destruct e1. destruct e2.
simpl in *. revert econd0. rewrite H. rewrite H0.
intro. pose proof (proof_irrelevance _ econd0 econd1).
rewrite H1. reflexivity.
Qed.

Record guard: Set := mkguard {
  gval: store -> bool;
  gvar: list V;
  gcond: forall (s t: store), eq_restr s t gvar -> gval s = gval t
}.
Coercion gval: guard >-> Funclass.

Proposition const_guard_cond (v: bool) (s t : store):
  eq_restr s t nil -> v = v.
intros. reflexivity.
Qed.
Definition const_guard (v: bool): guard :=
  mkguard (fun s => v) nil (const_guard_cond v).
Coercion const_guard: bool >-> guard.

Proposition equals_cond (e1 e2: expr) (s t : store):
  eq_restr s t (evar e1 ++ evar e2) ->
  (if Z.eq_dec (eval e1 s) (eval e2 s) then true else false) =
  (if Z.eq_dec (eval e1 t) (eval e2 t) then true else false).
intro H.
apply eq_restr_split in H; destruct H.
pose proof (econd e1 s t); rewrite H1.
pose proof (econd e2 s t); rewrite H2.
all: auto.
Qed.
Definition equals (e1 e2: expr): guard :=
  mkguard (fun s => if Z.eq_dec (eval e1 s) (eval e2 s) then
    true else false) (evar e1 ++ evar e2) (equals_cond e1 e2).

Proposition gsub_cond (g: guard) (x: V) (e: expr) (s t: store):
  eq_restr s t (remove Nat.eq_dec x (gvar g) ++ evar e) ->
  gval g (store_update s x (eval e s)) =
  gval g (store_update t x (eval e t)).
intro.
assert (eval e s = eval e t).
apply (econd e).
intro; intro; apply H.
apply in_or_app; right; assumption.
rewrite <- H0.
unfold store_update.
apply (gcond g).
unfold eq_restr.
intro; intro.
destruct (Nat.eq_dec x x0).
reflexivity.
apply H; apply in_or_app; left.
apply In_remove; assumption.
Qed.
Definition gsub (g: guard) (x: V) (e: expr): guard :=
  mkguard (fun s => gval g (store_update s x (eval e s)))
    (remove Nat.eq_dec x (gvar g) ++ evar e) (gsub_cond g x e).

Proposition gsub_notInVar (g: guard) (x:V) (e: expr):
  ~In x (evar e) -> ~In x (gvar (gsub g x e)).
intros; simpl; intro.
apply in_app_or in H0; destruct H0.
eapply remove_In; apply H0.
apply H. assumption.
Qed.

Proposition guard_eq (g1 g2: guard):
  (gval g1 = gval g2) -> (gvar g1 = gvar g2) -> g1 = g2.
intros. destruct g1. destruct g2.
simpl in *. revert gcond0. rewrite H. rewrite H0.
intro. pose proof (proof_irrelevance _ gcond0 gcond1).
rewrite H1. reflexivity.
Qed.

(* ================================== *)
(* INDUCTIVE DEFINITION OF ASSERTIONS *)
(* ================================== *)

Inductive assert :=
| test: guard -> assert
| hasval: expr -> expr -> assert
| land: assert -> assert -> assert
| lor: assert -> assert -> assert
| limp: assert -> assert -> assert
| lexists: V -> assert -> assert
| lforall: V -> assert -> assert
| sand: assert -> assert -> assert
| simp: assert -> assert -> assert.
Coercion test: guard >-> assert.

Definition lnot (p: assert): assert := (limp p false).
Definition lequiv (p q: assert): assert := (land (limp p q) (limp q p)).
Definition hasvaldash (e: expr): assert :=
  let y := fresh (evar e) in lexists y (hasval e y).
Definition emp: assert := (lforall dummy (lnot (hasvaldash dummy))).
Definition pointsto (e e': expr): assert :=
  let x := fresh (evar e) in land (hasval e e') (lforall x (limp (hasvaldash x) (equals x e))).
Definition pointstodash (e: expr): assert :=
  let y := fresh (evar e) in lexists y (pointsto e y).
Definition hasval_alt (e e': expr): assert :=
  sand (pointsto e e') true.
Definition hasvaldash_alt (e: expr): assert :=
  sand (pointstodash e) true.

Fixpoint abound (p: assert): list V :=
  match p with
  | test g => nil
  | hasval e e' => nil
  | land p q => abound p ++ abound q
  | lor p q => abound p ++ abound q
  | limp p q => abound p ++ abound q
  | lexists x p => x :: abound p
  | lforall x p => x :: abound p
  | sand p q => abound p ++ abound q
  | simp p q => abound p ++ abound q
  end.

Fixpoint avar (p: assert): list V :=
  match p with
  | test g => gvar g
  | hasval e e' => evar e ++ evar e'
  | land p q => avar p ++ avar q
  | lor p q => avar p ++ avar q
  | limp p q => avar p ++ avar q
  | lexists x p => remove Nat.eq_dec x (avar p)
  | lforall x p => remove Nat.eq_dec x (avar p)
  | sand p q => avar p ++ avar q
  | simp p q => avar p ++ avar q
  end.

Definition aoccur (p: assert): list V := abound p ++ avar p.

Local Ltac aoccur_generic_bin := intros; unfold aoccur; split; intro H;
match goal with
| H: _ |- _ => apply in_app_or in H; simpl in H; destruct H; apply in_app_or in H; destruct H;
    try (apply in_or_app; left; apply in_or_app; auto; fail);
    try (apply in_or_app; right; apply in_or_app; auto; fail)
end.

Proposition aoccur_split_land (p1 p2: assert):
  forall x, In x (aoccur (land p1 p2)) <-> In x (aoccur p1 ++ aoccur p2).
aoccur_generic_bin.
Qed.

Proposition aoccur_split_lor (p1 p2: assert):
  forall x, In x (aoccur (lor p1 p2)) <-> In x (aoccur p1 ++ aoccur p2).
aoccur_generic_bin.
Qed.

Proposition aoccur_split_limp (p1 p2: assert):
  forall x, In x (aoccur (limp p1 p2)) <-> In x (aoccur p1 ++ aoccur p2).
aoccur_generic_bin.
Qed.

Local Ltac aoccur_generic_quan := intros; simpl; split; intro;
match goal with
| H: ?x = ?y \/ _ |- _ => destruct H; auto; apply in_app_or in H; destruct H;
    try (right; apply in_or_app; auto; fail);
    destruct (Nat.eq_dec x y); auto;
    right; apply in_or_app; right;
    try (apply In_remove; assumption; fail);
    match goal with
     | n: x <> y |- _ => eapply In_remove_elim; [apply n | apply H]
    end
end.

Proposition aoccur_split_lexists (x: V) (p: assert):
  forall y, In y (aoccur (lexists x p)) <-> In y (x :: aoccur p).
aoccur_generic_quan.
Qed.

Proposition aoccur_split_lforall (x: V) (p: assert):
  forall y, In y (aoccur (lforall x p)) <-> In y (x :: aoccur p).
aoccur_generic_quan.
Qed.

Proposition aoccur_split_sand (p1 p2: assert):
  forall x, In x (aoccur (sand p1 p2)) <-> In x (aoccur p1 ++ aoccur p2).
aoccur_generic_bin.
Qed.

Proposition aoccur_split_simp (p1 p2: assert):
  forall x, In x (aoccur (simp p1 p2)) <-> In x (aoccur p1 ++ aoccur p2).
aoccur_generic_bin.
Qed.

Definition Some_assert (p: assert): option assert := Some p.
Coercion Some_assert: assert >-> option.

(* ================================================== *)
(* STANDARD FIRST-ORDER CAPTURE-AVOIDING SUBSTITUTION *)
(* ================================================== *)

Fixpoint asub (p: assert) (x: V) (e: expr): option assert :=
  match p with
  | test g => test (gsub g x e)
  | hasval e1 e2 => hasval (esub e1 x e) (esub e2 x e)
  | land p q => option_app (asub p x e) (fun ps =>
      option_app (asub q x e) (fun qs => land ps qs))
  | lor p q => option_app (asub p x e) (fun ps =>
      option_app (asub q x e) (fun qs => lor ps qs))
  | limp p q => option_app (asub p x e) (fun ps =>
      option_app (asub q x e) (fun qs => limp ps qs))
  | lexists y p => if in_dec Nat.eq_dec y (evar e) then None else
      option_app (asub p (if Nat.eq_dec x y then fresh (avar p) else x) e) (fun ps => lexists y ps)
  | lforall y p => if in_dec Nat.eq_dec y (evar e) then None else
      option_app (asub p (if Nat.eq_dec x y then fresh (avar p) else x) e) (fun ps => lforall y ps)
  | sand p q => option_app (asub p x e) (fun ps =>
      option_app (asub q x e) (fun qs => sand ps qs))
  | simp p q => option_app (asub p x e) (fun ps =>
      option_app (asub q x e) (fun qs => simp ps qs))
  end.

Proposition asub_defined_step1 (C: assert -> assert -> assert) (p1 p2: assert) (x: V) (e: expr)
    (IHp1: forall x : V, (forall x : V, In x (evar e) -> ~ In x (abound p1)) <-> (exists q : assert, asub p1 x e = Some q))
    (IHp2: forall x : V, (forall x : V, In x (evar e) -> ~ In x (abound p2)) <-> (exists q : assert, asub p2 x e = Some q)):
  (forall x0 : V, In x0 (evar e) -> ~ In x0 (abound p1 ++ abound p2)) <->
  (exists q : assert, option_app (asub p1 x e) (fun ps : assert => option_app (asub p2 x e) (fun qs : assert => C ps qs)) = Some q).
split; intros; specialize IHp1 with x; specialize IHp2 with x.
- apply In_app_split in H; destruct H.
  apply IHp1 in H; destruct H.
  apply IHp2 in H0; destruct H0.
  exists (C x0 x1); rewrite H; rewrite H0; reflexivity.
- destruct H.
  apply option_app_elim in H; destruct H; destruct H.
  assert (exists q, asub p1 x e = Some q) by (exists x2; assumption).
  apply option_app_elim in H1; destruct H1; destruct H1.
  assert (exists q, asub p2 x e = Some q) by (exists x3; assumption).
  apply not_In_split; split.
  apply <- IHp1; assumption.
  apply <- IHp2; assumption.
Qed.

Proposition asub_defined_step2 (Q: V -> assert -> assert) (p: assert) (x v: V) (e: expr)
    (IHp: forall x : V, (forall x : V, In x (evar e) -> ~ In x (abound p)) <-> (exists q : assert, asub p x e = Some q)):
  (forall x0 : V, In x0 (evar e) -> ~ (v = x0 \/ In x0 (abound p))) <->
  (exists q : assert, (if in_dec Nat.eq_dec v (evar e) then None else
    option_app (asub p (if Nat.eq_dec x v then fresh (avar p) else x) e) (fun ps : assert => Q v ps)) = Some q).
split; intros.
- assert (forall x : V, In x (evar e) -> ~ In x (abound p)) by
    (intros; intro; eapply H; [apply H0 | auto]).
  destruct (in_dec Nat.eq_dec v (evar e)).
  specialize H with v.
  apply H in i; exfalso; apply i; auto.
  destruct (Nat.eq_dec x v).
  specialize IHp with (fresh (avar p)).
  apply IHp in H0; destruct H0.
  exists (Q v x0); rewrite H0; reflexivity.
  specialize IHp with x.
  apply IHp in H0; destruct H0.
  exists (Q v x0); rewrite H0; reflexivity.
- intro; destruct H; destruct H1.
  rewrite H1 in *; clear H1 v.
  destruct (in_dec Nat.eq_dec x0 (evar e)).
  inversion H.
  apply n; assumption.
  destruct (in_dec Nat.eq_dec v (evar e)).
  inversion H.
  apply option_app_elim in H; destruct H; destruct H.
  destruct (Nat.eq_dec x v).
  assert (exists q, asub p (fresh (avar p)) e = Some q) by (exists x2; assumption).
  eapply IHp in H3; [apply H3; apply H1 | assumption].
  assert (exists q, asub p x e = Some q) by (exists x2; assumption).
  eapply IHp in H3; [apply H3; apply H1 | assumption].
Qed.

Proposition asub_defined (p: assert) (x: V) (e: expr):
  (forall x, In x (evar e) -> ~In x (abound p)) <-> exists q, asub p x e = Some q.
generalize dependent x; induction p; intro x; simpl;
  try (apply asub_defined_step1; assumption; fail);
  try (apply asub_defined_step2; assumption; fail).
- split; intros; auto.
  exists (test (gsub g x e)); reflexivity.
- split; intros; auto.
  exists (hasval (esub e0 x e) (esub e1 x e)); reflexivity.
Qed.

Proposition asub_notInVar (p: assert) (x: V) (e: expr):
  ~In x (evar e) -> forall ps, asub p x e = Some ps -> ~In x (avar ps).
intro. induction p; intros;
try (simpl in H0;
  apply option_app_elim in H0; destruct H0; destruct H0;
  apply option_app_elim in H1; destruct H1; destruct H1;
  inversion H2; simpl;
  intro; apply in_app_or in H3; destruct H3;
  [eapply IHp1; [apply H0 | auto] | eapply IHp2; [apply H1 | auto]]; fail);
try (simpl in H0;
  destruct (in_dec Nat.eq_dec v (evar e)); inversion H0;
  apply option_app_elim in H0; destruct H0; destruct H0;
  inversion H1;
  simpl; intro;
  destruct (Nat.eq_dec x v);
  [eapply remove_In; rewrite e0 in H3; apply H3|
   apply In_remove_elim in H3; auto;
   eapply IHp; [apply H0 | auto]]).
- simpl in H0. inversion H0. unfold avar.
  apply gsub_notInVar. assumption.
- simpl in H0. inversion H0. unfold avar.
  intro. apply in_app_or in H1; destruct H1.
  eapply esub_notInVar. apply H. apply H1.
  eapply esub_notInVar. apply H. apply H1.
Qed.

Proposition abound_asub (p: assert) (x: V) (e: expr):
  ~In x (abound p) -> forall ps, asub p x e = Some ps -> ~ In x (abound ps).
generalize dependent x. induction p; intros; inversion H0; auto;
try (rename H2 into H1;
  apply option_app_elim in H1; destruct H1; destruct H1;
  apply option_app_elim in H2; destruct H2; destruct H2;
  inversion H3;
  simpl; intro; apply in_app_or in H4; destruct H4;
  [eapply IHp1; [intro; apply H; apply in_or_app; left; apply H6 | apply H1 | assumption ]|
   eapply IHp2; [intro; apply H; apply in_or_app; right; apply H6 | apply H2 | assumption ]]);
try (destruct (in_dec Nat.eq_dec v (evar e)); inversion H2; clear H2;
  rename H3 into H1;
  apply option_app_elim in H1; destruct H1; destruct H1;
  destruct (Nat.eq_dec x v);
  [exfalso; apply H; simpl; left; auto|];
  inversion H2; simpl; intro; destruct H3; auto;
  eapply IHp; [intro; apply H; simpl; right; apply H5|
  apply H1|assumption]).
Qed.

Fixpoint areplace (p: assert) (x y: V): assert :=
  match p with
  | test g => test (gsub g x y)
  | hasval e1 e2 => hasval (esub e1 x y) (esub e2 x y)
  | land p q => land (areplace p x y) (areplace q x y)
  | lor p q => lor (areplace p x y) (areplace q x y)
  | limp p q => limp (areplace p x y) (areplace q x y)
  | lexists z p => if Nat.eq_dec x z
      then lexists y (areplace p x y)
      else lexists z (areplace p x y)
  | lforall z p => if Nat.eq_dec x z
      then lforall y (areplace p x y)
      else lforall z (areplace p x y)
  | sand p q => sand (areplace p x y) (areplace q x y)
  | simp p q => simp (areplace p x y) (areplace q x y)
  end.

Proposition areplace_no_occur (p: assert) (x y: V):
  x <> y -> ~In y (aoccur p) -> ~In x (aoccur (areplace p x y)).
intros; induction p; simpl;
try (((rewrite aoccur_split_land in H0;
       rewrite aoccur_split_land) +
      (rewrite aoccur_split_lor in H0;
       rewrite aoccur_split_lor) +
      (rewrite aoccur_split_limp in H0;
       rewrite aoccur_split_limp) +
      (rewrite aoccur_split_sand in H0;
       rewrite aoccur_split_sand) +
      (rewrite aoccur_split_simp in H0;
       rewrite aoccur_split_simp));
  apply not_In_split;
  apply not_In_split in H0; tauto; fail).
- intro; apply in_app_or in H1; destruct H1.
  unfold abound in H1. inversion H1.
  pose proof (gsub_notInVar g x y).
  apply H2; auto. simpl; intro. destruct H3; auto.
- unfold aoccur in *; unfold abound in *; unfold avar in *.
  intro.
  apply in_app_or in H1; destruct H1.
  inversion H1.
  apply in_app_or in H1; destruct H1.
  pose proof (esub_notInVar e x y). apply H2; auto.
  simpl. intro. destruct H3; auto.
  pose proof (esub_notInVar e0 x y). apply H2; auto.
  simpl. intro. destruct H3; auto.
- destruct (Nat.eq_dec x v).
  + simpl; intro; destruct H1.
    apply H; auto.
    apply in_app_or in H1; destruct H1.
    * apply IHp. intro. rewrite aoccur_split_lexists in H0. apply H0.
      right. assumption.
      apply in_or_app; auto.
    * apply IHp. intro. rewrite aoccur_split_lexists in H0. apply H0.
      right. assumption.
      apply in_or_app; auto.
      apply In_remove_elim in H1.
      auto. apply Nat.neq_sym; assumption.
  + simpl. intro. destruct H1.
    apply n; symmetry; apply H1.
    apply in_app_or in H1; destruct H1.
    2: apply In_remove_elim in H1.
    3: apply Nat.neq_sym; assumption.
    all: apply IHp; [intro; rewrite aoccur_split_lexists in H0;
    apply H0; right; assumption | apply in_or_app; auto].
- destruct (Nat.eq_dec x v).
  + simpl; intro; destruct H1.
    apply H; auto.
    apply in_app_or in H1; destruct H1.
    * apply IHp. intro. rewrite aoccur_split_lforall in H0. apply H0.
      right. assumption.
      apply in_or_app; auto.
    * apply IHp. intro. rewrite aoccur_split_lforall in H0. apply H0.
      right. assumption.
      apply in_or_app; auto.
      apply In_remove_elim in H1.
      auto. apply Nat.neq_sym; assumption.
  + simpl. intro. destruct H1.
    apply n; symmetry; apply H1.
    apply in_app_or in H1; destruct H1.
    2: apply In_remove_elim in H1.
    3: apply Nat.neq_sym; assumption.
    all: apply IHp; [intro; rewrite aoccur_split_lforall in H0;
    apply H0; right; assumption | apply in_or_app; auto].
Qed.

(* ======================================================= *)
(* HEAP UPDATE SUBSTITUTION, SEE DEFINITION 2 IN THE PAPER *)
(* ======================================================= *)

Fixpoint asub_heap_update (p: assert) (x: V) (e: expr): option assert :=
  match p with
  | test g => test g
  | hasval e1 e2 => (lor (land (equals x e1) (equals e e2)) (land (lnot (equals x e1)) (hasval e1 e2)))
  | land p q => option_app (asub_heap_update p x e) (fun ps =>
      option_app (asub_heap_update q x e) (fun qs => land ps qs))
  | lor p q => option_app (asub_heap_update p x e) (fun ps =>
      option_app (asub_heap_update q x e) (fun qs => lor ps qs))
  | limp p q => option_app (asub_heap_update p x e) (fun ps =>
      option_app (asub_heap_update q x e) (fun qs => limp ps qs))
  | lexists y p => if in_dec Nat.eq_dec y (x :: evar e) then None else
      option_app (asub_heap_update p x e) (fun ps => lexists y ps)
  | lforall y p => if in_dec Nat.eq_dec y (x :: evar e) then None else
      option_app (asub_heap_update p x e) (fun ps => lforall y ps)
  | sand p q => option_app (asub_heap_update p x e) (fun ps =>
      option_app (asub_heap_update q x e) (fun qs => lor (sand ps (land q (lnot (hasvaldash x))))
        (sand (land p (lnot (hasvaldash x))) qs)))
  | simp p q => if sublist_part_dec Nat.eq_dec (x :: evar e) (abound p) then None else
      option_app (asub_heap_update q x e) (fun qs => simp (land p (lnot (hasvaldash x))) qs)
  end.

Proposition asub_heap_update_defined_step1 (C: assert -> assert -> assert) (p1 p2: assert) (x: V) (e: expr)
    (IHp1: (forall y : V, In y (x :: evar e) -> ~ In y (abound p1)) <-> (exists q : assert, asub_heap_update p1 x e = Some q))
    (IHp2: (forall y : V, In y (x :: evar e) -> ~ In y (abound p2)) <-> (exists q : assert, asub_heap_update p2 x e = Some q)):
  (forall y : V, In y (x :: evar e) -> ~ In y (abound p1 ++ abound p2)) <->
  (exists q : assert, option_app (asub_heap_update p1 x e) (fun ps : assert => option_app (asub_heap_update p2 x e) (fun qs : assert => C ps qs)) = Some q).
split; intros.
- apply In_app_split in H; destruct H.
  apply IHp1 in H; destruct H.
  apply IHp2 in H0; destruct H0.
  exists (C x0 x1); rewrite H; rewrite H0; reflexivity.
- destruct H.
  apply option_app_elim in H; destruct H; destruct H.
  assert (exists q, asub_heap_update p1 x e = Some q) by (exists x1; assumption).
  apply option_app_elim in H1; destruct H1; destruct H1.
  assert (exists q, asub_heap_update p2 x e = Some q) by (exists x2; assumption).
  apply not_In_split; split.
  apply <- IHp1; assumption.
  apply <- IHp2; assumption.
Qed.

Proposition asub_heap_update_defined (p: assert) (x: V) (e: expr):
  (forall y, In y (x :: evar e) -> ~In y (abound p)) <-> exists q, asub_heap_update p x e = Some q.
induction p;
try (apply asub_heap_update_defined_step1; assumption; fail).
- simpl; split; intros.
  eexists; reflexivity. tauto.
- simpl; split; intros.
  eexists; reflexivity. tauto.
- unfold asub_heap_update. fold asub_heap_update.
  destruct (in_dec Nat.eq_dec v (x :: evar e)).
  + split; intro. exfalso. eapply H. apply i.
    simpl. left; reflexivity.
    destruct H. inversion H.
  + split; intro.
    assert (forall y : V, In y (x :: evar e) -> ~ In y (abound p)).
    intros. intro. eapply H. apply H0. simpl. right; assumption.
    apply IHp in H0. destruct H0.
    exists (lexists v x0). rewrite H0. reflexivity.
    destruct H.
    apply option_app_elim in H; destruct H; destruct H.
    assert (exists q : assert, asub_heap_update p x e = Some q) by
      (exists x1; assumption).
    intros.
    eapply IHp in H1; [|apply H2].
    intro. simpl in H3. destruct H3.
    apply n. rewrite H3. assumption.
    apply H1. assumption.
- unfold asub_heap_update. fold asub_heap_update.
  destruct (in_dec Nat.eq_dec v (x :: evar e)).
  + split; intro. exfalso. eapply H. apply i.
    simpl. left; reflexivity.
    destruct H. inversion H.
  + split; intro.
    assert (forall y : V, In y (x :: evar e) -> ~ In y (abound p)).
    intros. intro. eapply H. apply H0. simpl. right; assumption.
    apply IHp in H0. destruct H0.
    exists (lforall v x0). rewrite H0. reflexivity.
    destruct H.
    apply option_app_elim in H; destruct H; destruct H.
    assert (exists q : assert, asub_heap_update p x e = Some q) by
      (exists x1; assumption).
    intros.
    eapply IHp in H1; [|apply H2].
    intro. simpl in H3. destruct H3.
    apply n. rewrite H3. assumption.
    apply H1. assumption.
- split; intros.
  + unfold abound in H; fold abound in H.
    apply In_app_split in H. destruct H.
    apply IHp2 in H0; destruct H0.
    exists (simp (land p1 (lnot (hasvaldash x))) x0).
    unfold asub_heap_update. fold asub_heap_update. rewrite H0.
    destruct (sublist_part_dec Nat.eq_dec (x :: evar e) (abound p1)).
    destruct e0 as (x1 & H1 & H2).
    exfalso; eapply H. apply H1. apply H2.
    reflexivity.
  + destruct H.
    unfold asub_heap_update in H; fold asub_heap_update in H.
    destruct (sublist_part_dec Nat.eq_dec (x :: evar e) (abound p1)).
    inversion H.
    apply option_app_elim in H; destruct H; destruct H.
    assert (exists q : assert, asub_heap_update p2 x e = Some q) by
      (exists x1; assumption).
    rewrite <- IHp2 in H2.
    simpl. intro. apply in_app_or in H3; destruct H3.
    eapply n. apply H0. apply H3.
    eapply H2. apply H0. apply H3.
Qed.

(* ====================================================== *)
(* HEAP CLEAR SUBSTITUTION, SEE DEFINITION 3 IN THE PAPER *)
(* ====================================================== *)

Fixpoint asub_heap_clear (p: assert) (x: V): option assert :=
  match p with
  | test g => test g
  | hasval e1 e2 => (land (lnot (equals x e1)) (hasval e1 e2))
  | land p q => option_app (asub_heap_clear p x) (fun ps =>
      option_app (asub_heap_clear q x) (fun qs => land ps qs))
  | lor p q => option_app (asub_heap_clear p x) (fun ps =>
      option_app (asub_heap_clear q x) (fun qs => lor ps qs))
  | limp p q => option_app (asub_heap_clear p x) (fun ps =>
      option_app (asub_heap_clear q x) (fun qs => limp ps qs))
  | lexists y p => if Nat.eq_dec y x then None else
      option_app (asub_heap_clear p x) (fun ps => lexists y ps)
  | lforall y p => if Nat.eq_dec y x then None else
      option_app (asub_heap_clear p x) (fun ps => lforall y ps)
  | sand p q => option_app (asub_heap_clear p x) (fun ps =>
      option_app (asub_heap_clear q x) (fun qs => sand ps qs))
  | simp p q => let y := fresh (x :: aoccur p ++ aoccur q) in
      option_app (asub_heap_clear q x) (fun qs =>
        option_app (asub_heap_update p x y) (fun pss =>
          option_app (asub_heap_update q x y) (fun qss =>
            (land (simp (land p (lnot (hasvaldash x))) qs) (lforall y (simp pss qss))))))
  end.

Proposition asub_heap_clear_defined_step1 (C: assert -> assert -> assert) (p1 p2: assert) (x: V)
    (IHp1: ~ In x (abound p1) <-> (exists q : assert, asub_heap_clear p1 x = Some q))
    (IHp2: ~ In x (abound p2) <-> (exists q : assert, asub_heap_clear p2 x = Some q)):
  ~ In x (abound p1 ++ abound p2) <-> (exists q : assert, option_app (asub_heap_clear p1 x)
    (fun ps : assert => option_app (asub_heap_clear p2 x) (fun qs : assert => C ps qs)) = Some q).
split; intros.
- assert (~In x (abound p1)) by
    (intro; apply H; apply in_or_app; auto).
  assert (~In x (abound p2)) by
    (intro; apply H; apply in_or_app; auto).
  rewrite IHp1 in H0; rewrite IHp2 in H1.
  destruct H0; destruct H1.
  exists (C x0 x1).
  rewrite H0; rewrite H1.
  reflexivity.
- destruct H.
  apply option_app_elim in H; destruct H; destruct H.
  apply option_app_elim in H0; destruct H0; destruct H0.
  intro. apply in_app_or in H2. destruct H2.
  apply <- IHp1; auto. exists x1; auto.
  apply <- IHp2; auto. exists x2; auto.
Qed.

Proposition asub_heap_clear_defined_step2 (Q: V -> assert -> assert) (p: assert) (x v: V)
    (IHp: ~ In x (abound p) <-> (exists q : assert, asub_heap_clear p x = Some q)):
  ~ (v = x \/ In x (abound p)) <->
  (exists q : assert, (if Nat.eq_dec v x then None else option_app (asub_heap_clear p x) (fun ps : assert => Q v ps)) = Some q).
split; intro.
- destruct (Nat.eq_dec v x).
  exfalso; apply H; auto.
  assert (~In x (abound p)) by
    (intro; apply H; auto).
  rewrite IHp in H0; destruct H0.
  exists (Q v x0); rewrite H0; reflexivity.
- destruct (Nat.eq_dec v x); destruct H.
  inversion H.
  apply option_app_elim in H; destruct H; destruct H.
  intro; destruct H1.
  apply n; auto.
  apply <- IHp.
  exists x1; auto.
  auto.
Qed.

Proposition asub_heap_clear_defined (p: assert) (x: V):
  ~In x (abound p) <-> exists q, asub_heap_clear p x = Some q.
induction p;
try (apply asub_heap_clear_defined_step1; assumption; fail);
try (apply asub_heap_clear_defined_step2; assumption; fail).
- simpl; split; intros.
  eexists; reflexivity. tauto.
- simpl; split; intros.
  eexists; reflexivity. tauto.
- simpl. split; intros.
  + assert (~In x (abound p2)) by
    (intro; apply H; apply in_or_app; auto).
    rewrite IHp2 in H0. destruct H0.
    remember (fresh (x :: aoccur p1 ++ aoccur p2)).
    pose proof (asub_heap_update_defined p1 x v).
    assert (forall y : V, In y (x :: evar v) -> ~ In y (abound p1)).
    { intros. inversion H2. rewrite <- H3.
      intro. apply H. apply in_or_app; auto.
      simpl in H3. destruct H3; auto.
      rewrite <- H3. rewrite Heqv.
      unfold aoccur.
      apply fresh_notInGeneral.
        intros. right. apply in_or_app. left.
        apply in_or_app. left. assumption. }
    apply H1 in H2. destruct H2.
    pose proof (asub_heap_update_defined p2 x v).
    assert (forall y : V, In y (x :: evar v) -> ~ In y (abound p2)).
    { intros. inversion H4. rewrite <- H5.
      intro. apply H. apply in_or_app; auto.
      simpl in H5. destruct H5; auto.
      rewrite <- H5. rewrite Heqv.
      unfold aoccur.
      apply fresh_notInGeneral.
        intros. right. apply in_or_app. right.
        apply in_or_app. left. assumption. }
    apply H3 in H4. destruct H4.
    exists (land (simp (land p1 (lnot (hasvaldash x))) x0) (lforall v (simp x1 x2))).
    rewrite H0. simpl. rewrite H2. simpl. rewrite H4. simpl. reflexivity.
  + destruct H.
    apply option_app_elim in H; destruct H; destruct H.
    apply option_app_elim in H0; destruct H0; destruct H0.
    assert (~ In x (abound p1)).
     pose proof (asub_heap_update_defined p1 x (fresh (x :: aoccur p1 ++ aoccur p2))).
      apply <- H2. exists x2; auto. left; auto.
    assert (~ In x (abound p2)).
      apply <- IHp2. exists x1; auto.
    intro. apply in_app_or in H4. destruct H4.
    apply H2; auto. apply H3; auto.
Qed.

(* ==================================== *)
(* CONDITIONAL HEAP UPDATE SUBSTITUTION *)
(* ==================================== *)

Fixpoint asub_cheap_update (p: assert) (x: V) (e: expr): option assert :=
  match p with
  | test g => test g
  | hasval e1 e2 => (lor (land (equals x e1) (equals e e2)) (land (lnot (equals x e1)) (hasval e1 e2)))
  | land p q => option_app (asub_cheap_update p x e) (fun ps =>
      option_app (asub_cheap_update q x e) (fun qs => land ps qs))
  | lor p q => option_app (asub_cheap_update p x e) (fun ps =>
      option_app (asub_cheap_update q x e) (fun qs => lor ps qs))
  | limp p q => option_app (asub_cheap_update p x e) (fun ps =>
      option_app (asub_cheap_update q x e) (fun qs => limp ps qs))
  | lexists y p => if in_dec Nat.eq_dec y (x :: evar e) then None else
      option_app (asub_cheap_update p x e) (fun ps => lexists y ps)
  | lforall y p => if in_dec Nat.eq_dec y (x :: evar e) then None else
      option_app (asub_cheap_update p x e) (fun ps => lforall y ps)
  | sand p q => option_app (asub_cheap_update p x e) (fun ps =>
      option_app (asub_cheap_update q x e) (fun qs =>
        lor (sand (land ps (hasvaldash x)) q) (sand p (land qs (hasvaldash x)))))
  | simp p q => if sublist_part_dec Nat.eq_dec (x :: evar e) (abound p) then None else
      option_app (asub_cheap_update q x e) (fun qs => simp p qs)
  end.

Proposition asub_cheap_update_defined_step1 (C: assert -> assert -> assert) (p1 p2: assert) (x: V) (e: expr)
    (IHp1: (forall y : V, In y (x :: evar e) -> ~ In y (abound p1)) <-> (exists q : assert, asub_cheap_update p1 x e = Some q))
    (IHp2: (forall y : V, In y (x :: evar e) -> ~ In y (abound p2)) <-> (exists q : assert, asub_cheap_update p2 x e = Some q)):
  (forall y : V, In y (x :: evar e) -> ~ In y (abound p1 ++ abound p2)) <->
  (exists q : assert, option_app (asub_cheap_update p1 x e) (fun ps : assert => option_app (asub_cheap_update p2 x e) (fun qs : assert => C ps qs)) = Some q).
split; intros.
- apply In_app_split in H; destruct H.
  apply IHp1 in H; destruct H.
  apply IHp2 in H0; destruct H0.
  exists (C x0 x1); rewrite H; rewrite H0; reflexivity.
- destruct H.
  apply option_app_elim in H; destruct H; destruct H.
  assert (exists q, asub_cheap_update p1 x e = Some q) by (exists x1; assumption).
  apply option_app_elim in H1; destruct H1; destruct H1.
  assert (exists q, asub_cheap_update p2 x e = Some q) by (exists x2; assumption).
  apply not_In_split; split.
  apply <- IHp1; assumption.
  apply <- IHp2; assumption.
Qed.

Proposition asub_cheap_update_defined (p: assert) (x: V) (e: expr):
  (forall y, In y (x :: evar e) -> ~In y (abound p)) <-> exists q, asub_cheap_update p x e = Some q.
induction p;
try (apply asub_cheap_update_defined_step1; assumption; fail).
- simpl; split; intros.
  eexists; reflexivity. tauto.
- simpl; split; intros.
  eexists; reflexivity. tauto.
- unfold asub_cheap_update. fold asub_cheap_update.
  destruct (in_dec Nat.eq_dec v (x :: evar e)).
  + split; intro. exfalso. eapply H. apply i.
    simpl. left; reflexivity.
    destruct H. inversion H.
  + split; intro.
    assert (forall y : V, In y (x :: evar e) -> ~ In y (abound p)).
    intros. intro. eapply H. apply H0. simpl. right; assumption.
    apply IHp in H0. destruct H0.
    exists (lexists v x0). rewrite H0. reflexivity.
    destruct H.
    apply option_app_elim in H; destruct H; destruct H.
    assert (exists q : assert, asub_cheap_update p x e = Some q) by
      (exists x1; assumption).
    intros.
    eapply IHp in H1; [|apply H2].
    intro. simpl in H3. destruct H3.
    apply n. rewrite H3. assumption.
    apply H1. assumption.
- unfold asub_cheap_update. fold asub_cheap_update.
  destruct (in_dec Nat.eq_dec v (x :: evar e)).
  + split; intro. exfalso. eapply H. apply i.
    simpl. left; reflexivity.
    destruct H. inversion H.
  + split; intro.
    assert (forall y : V, In y (x :: evar e) -> ~ In y (abound p)).
    intros. intro. eapply H. apply H0. simpl. right; assumption.
    apply IHp in H0. destruct H0.
    exists (lforall v x0). rewrite H0. reflexivity.
    destruct H.
    apply option_app_elim in H; destruct H; destruct H.
    assert (exists q : assert, asub_cheap_update p x e = Some q) by
      (exists x1; assumption).
    intros.
    eapply IHp in H1; [|apply H2].
    intro. simpl in H3. destruct H3.
    apply n. rewrite H3. assumption.
    apply H1. assumption.
- split; intros.
  + unfold abound in H; fold abound in H.
    apply In_app_split in H. destruct H.
    apply IHp2 in H0; destruct H0.
    exists (simp p1 x0).
    unfold asub_cheap_update. fold asub_cheap_update. rewrite H0.
    destruct (sublist_part_dec Nat.eq_dec (x :: evar e) (abound p1)).
    destruct e0 as (x1 & H1 & H2).
    exfalso; eapply H. apply H1. apply H2.
    reflexivity.
  + destruct H.
    unfold asub_cheap_update in H; fold asub_cheap_update in H.
    destruct (sublist_part_dec Nat.eq_dec (x :: evar e) (abound p1)).
    inversion H.
    apply option_app_elim in H; destruct H; destruct H.
    assert (exists q : assert, asub_cheap_update p2 x e = Some q) by
      (exists x1; assumption).
    rewrite <- IHp2 in H2.
    simpl. intro. apply in_app_or in H3; destruct H3.
    eapply n. apply H0. apply H3.
    eapply H2. apply H0. apply H3.
Qed.

(* ======================================= *)
(* INTUITIONISTIC HEAP UPDATE SUBSTITUTION *)
(* ======================================= *)

Definition asub_iheap_update (p: assert) (x: V) (e: expr): option assert :=
  match asub_cheap_update p x e with
  | None => None
  | Some ps => limp (hasvaldash x) ps
  end.

Proposition asub_iheap_update_defined (p: assert) (x: V) (e: expr):
  (forall y, In y (x :: evar e) -> ~In y (abound p)) <-> exists q, asub_iheap_update p x e = Some q.
split; intro.
- rewrite (asub_cheap_update_defined p x e) in H; destruct H.
  exists (limp (hasvaldash x) x0).
  unfold asub_iheap_update.
  rewrite H; reflexivity.
- destruct H.
  unfold asub_iheap_update in H.
  remember (asub_cheap_update p x e). destruct o.
  symmetry in Heqo.
  assert (exists q, asub_cheap_update p x e = Some q)
    by (exists a; auto).
  rewrite <- (asub_cheap_update_defined p x e) in H0; auto.
  inversion H.
Qed.

(* =================================== *)
(* CONDITIONAL HEAP CLEAR SUBSTITUTION *)
(* =================================== *)

Fixpoint asub_cheap_clear (p: assert) (x: V): option assert :=
  match p with
  | test g => test g
  | hasval e1 e2 => (land (lnot (equals x e1)) (hasval e1 e2))
  | land p q => option_app (asub_cheap_clear p x) (fun ps =>
      option_app (asub_cheap_clear q x) (fun qs => land ps qs))
  | lor p q => option_app (asub_cheap_clear p x) (fun ps =>
      option_app (asub_cheap_clear q x) (fun qs => lor ps qs))
  | limp p q => let y := fresh (x :: aoccur p ++ aoccur q) in
      option_app (asub_cheap_clear p x) (fun ps =>
        option_app (asub_cheap_clear q x) (fun qs =>
          option_app (asub_cheap_update p x y) (fun pss =>
            option_app (asub_cheap_update q x y) (fun qss =>
              (land (limp ps qs) (lforall y (limp pss qss)))))))
  | lexists y p => if Nat.eq_dec y x then None else
      option_app (asub_cheap_clear p x) (fun ps => lexists y ps)
  | lforall y p => if Nat.eq_dec y x then None else
      option_app (asub_cheap_clear p x) (fun ps => lforall y ps)
  | sand p q => if in_dec Nat.eq_dec x (abound p) then None else
      option_app (asub_cheap_clear q x) (fun qs =>
        sand p (land qs (hasvaldash x)))
  | simp p q => let y := fresh (x :: aoccur p ++ aoccur q) in
      option_app (asub_cheap_clear q x) (fun qs =>
        option_app (asub_iheap_update p x y) (fun pss =>
          option_app (asub_iheap_update q x y) (fun qss =>
            (land (simp p qs) (lforall y (simp pss qss))))))
  end.

Proposition asub_cheap_clear_defined_step1 (C: assert -> assert -> assert) (p1 p2: assert) (x: V)
    (IHp1: ~ In x (abound p1) <-> (exists q : assert, asub_cheap_clear p1 x = Some q))
    (IHp2: ~ In x (abound p2) <-> (exists q : assert, asub_cheap_clear p2 x = Some q)):
  ~ In x (abound p1 ++ abound p2) <-> (exists q : assert, option_app (asub_cheap_clear p1 x)
    (fun ps : assert => option_app (asub_cheap_clear p2 x) (fun qs : assert => C ps qs)) = Some q).
split; intros.
- assert (~In x (abound p1)) by
    (intro; apply H; apply in_or_app; auto).
  assert (~In x (abound p2)) by
    (intro; apply H; apply in_or_app; auto).
  rewrite IHp1 in H0; rewrite IHp2 in H1.
  destruct H0; destruct H1.
  exists (C x0 x1).
  rewrite H0; rewrite H1.
  reflexivity.
- destruct H.
  apply option_app_elim in H; destruct H; destruct H.
  apply option_app_elim in H0; destruct H0; destruct H0.
  intro. apply in_app_or in H2. destruct H2.
  apply <- IHp1; auto. exists x1; auto.
  apply <- IHp2; auto. exists x2; auto.
Qed.

Proposition asub_cheap_clear_defined_step2 (Q: V -> assert -> assert) (p: assert) (x v: V)
    (IHp: ~ In x (abound p) <-> (exists q : assert, asub_cheap_clear p x = Some q)):
  ~ (v = x \/ In x (abound p)) <->
  (exists q : assert, (if Nat.eq_dec v x then None else option_app (asub_cheap_clear p x) (fun ps : assert => Q v ps)) = Some q).
split; intro.
- destruct (Nat.eq_dec v x).
  exfalso; apply H; auto.
  assert (~In x (abound p)) by
    (intro; apply H; auto).
  rewrite IHp in H0; destruct H0.
  exists (Q v x0); rewrite H0; reflexivity.
- destruct (Nat.eq_dec v x); destruct H.
  inversion H.
  apply option_app_elim in H; destruct H; destruct H.
  intro; destruct H1.
  apply n; auto.
  apply <- IHp.
  exists x1; auto.
  auto.
Qed.

Proposition asub_cheap_clear_defined (p: assert) (x: V):
  ~In x (abound p) <-> exists q, asub_cheap_clear p x = Some q.
induction p;
try (apply asub_cheap_clear_defined_step1; assumption; fail);
try (apply asub_cheap_clear_defined_step2; assumption; fail).
- simpl; split; intros.
  eexists; reflexivity. tauto.
- simpl; split; intros.
  eexists; reflexivity. tauto.
- simpl. split; intros.
  + assert (~In x (abound p1)) by
    (intro; apply H; apply in_or_app; auto).
    rewrite IHp1 in H0; destruct H0.
    assert (~In x (abound p2)) by
    (intro; apply H; apply in_or_app; auto).
    rewrite IHp2 in H1; destruct H1.
    remember (fresh (x :: aoccur p1 ++ aoccur p2)).
    pose proof (asub_cheap_update_defined p1 x v).
    assert (forall y : V, In y (x :: evar v) -> ~ In y (abound p1)).
    { intros. inversion H3. rewrite <- H4.
      intro. apply H. apply in_or_app; auto.
      simpl in H4. destruct H4; auto.
      rewrite <- H4. rewrite Heqv.
      unfold aoccur.
      apply fresh_notInGeneral.
        intros. right. apply in_or_app. left.
        apply in_or_app. left. assumption. }
    apply H2 in H3; clear H2; destruct H3.
    pose proof (asub_cheap_update_defined p2 x v).
    assert (forall y : V, In y (x :: evar v) -> ~ In y (abound p2)).
    { intros. inversion H4. rewrite <- H5.
      intro. apply H. apply in_or_app; auto.
      simpl in H5. destruct H5; auto.
      rewrite <- H5. rewrite Heqv.
      unfold aoccur.
      apply fresh_notInGeneral.
        intros. right. apply in_or_app. right.
        apply in_or_app. left. assumption. }
    apply H3 in H4; clear H3; destruct H4.
    exists (land (limp x0 x1) (lforall v (limp x2 x3))).
    rewrite H0; simpl.
    rewrite H1; simpl.
    rewrite H2; simpl.
    rewrite H3; simpl.
    reflexivity.
  + destruct H.
    apply option_app_elim in H; destruct H; destruct H.
    apply option_app_elim in H0; destruct H0; destruct H0.
    assert (exists q, asub_cheap_clear p1 x = Some q) by
      (exists x1; auto).
    assert (exists q, asub_cheap_clear p2 x = Some q) by
      (exists x2; auto).
    apply IHp1 in H2.
    apply IHp2 in H3.
    intro. apply in_app_or in H4; destruct H4.
    tauto. tauto.
- simpl. split; intros.
  + assert (~In x (abound p2)) by
    (intro; apply H; apply in_or_app; auto).
    rewrite IHp2 in H0. destruct H0.
    exists (sand p1 (land x0 (hasvaldash x))).
    rewrite H0. simpl.
    destruct (in_dec Nat.eq_dec x (abound p1)).
    exfalso. apply H. apply in_or_app; auto.
    reflexivity.
  + destruct H.
    destruct (in_dec Nat.eq_dec x (abound p1)).
    inversion H.
    intro. apply in_app_or in H0. destruct H0.
    apply n; auto.
    apply option_app_elim in H; destruct H; destruct H.
    assert (exists q, asub_cheap_clear p2 x = Some q).
    exists x1; auto.
    apply IHp2 in H2.
    apply H2; auto.
- simpl. split; intros.
  + assert (~In x (abound p2)) by
    (intro; apply H; apply in_or_app; auto).
    rewrite IHp2 in H0. destruct H0.
    remember (fresh (x :: aoccur p1 ++ aoccur p2)).
    pose proof (asub_iheap_update_defined p1 x v).
    assert (forall y : V, In y (x :: evar v) -> ~ In y (abound p1)).
    { intros. inversion H2. rewrite <- H3.
      intro. apply H. apply in_or_app; auto.
      simpl in H3. destruct H3; auto.
      rewrite <- H3. rewrite Heqv.
      unfold aoccur.
      apply fresh_notInGeneral.
        intros. right. apply in_or_app. left.
        apply in_or_app. left. assumption. }
    apply H1 in H2; clear H1; destruct H2.
    pose proof (asub_iheap_update_defined p2 x v).
    assert (forall y : V, In y (x :: evar v) -> ~ In y (abound p2)).
    { intros. inversion H3. rewrite <- H4.
      intro. apply H. apply in_or_app; auto.
      simpl in H4. destruct H4; auto.
      rewrite <- H4. rewrite Heqv.
      unfold aoccur.
      apply fresh_notInGeneral.
        intros. right. apply in_or_app. right.
        apply in_or_app. left. assumption. }
    apply H2 in H3; clear H2; destruct H3.
    exists (land (simp p1 x0) (lforall v (simp x1 x2))).
    rewrite H0. simpl. rewrite H1. simpl. rewrite H2. simpl. reflexivity.
  + destruct H.
    apply option_app_elim in H; destruct H; destruct H.
    apply option_app_elim in H0; destruct H0; destruct H0.
    apply option_app_elim in H1; destruct H1; destruct H1.
    assert (~ In x (abound p1)).
      pose proof (asub_iheap_update_defined p1 x (fresh (x :: aoccur p1 ++ aoccur p2))).
      apply <- H3. exists x2; auto. left; auto.
    assert (~ In x (abound p2)).
      apply <- IHp2. exists x1; auto.
    intro. apply in_app_or in H5. destruct H5.
    apply H3; auto. apply H4; auto.
Qed.

(* ===================================== *)
(* BASIC INSTRUCTIONS AND WHILE PROGRAMS *)
(* ===================================== *)

Inductive assignment :=
| basic: V -> expr -> assignment
| lookup: V -> expr -> assignment
| mutation: V -> expr -> assignment
| new: V -> expr -> assignment
| dispose: V -> assignment.

Inductive program :=
| assign: assignment -> program
| diverge: program
| skip: program
| comp: program -> program -> program
| ite: guard -> program -> program -> program
| while: guard -> program -> program.
Coercion assign: assignment >-> program.

(* ================================================ *)
(* SEMANTICS OF PROGRAMS, SEE FIGURE 1 IN THE PAPER *)
(* ================================================ *)

Inductive bigstep: program -> heap * store -> option (heap * store) -> Prop :=
| step_basic (x: V) (e: expr) (h: heap) (s: store):
    bigstep (basic x e) (h, s) (Some (h, store_update s x (eval e s)))
| step_lookup (x: V) (e: expr) (h: heap) (s: store) (v: Z):
    h (eval e s) = Some v ->
    bigstep (lookup x e) (h, s) (Some (h, store_update s x v))
| step_lookup_fail (x: V) (e: expr) (h: heap) (s: store):
    h (eval e s) = None ->
    bigstep (lookup x e) (h, s) None
| step_mutation (x: V) (e: expr) (h: heap) (s: store):
    dom h (s x) ->
    bigstep (mutation x e) (h, s) (Some (heap_update h (s x) (eval e s), s))
| step_mutation_fail (x: V) (e: expr) (h: heap) (s: store):
    ~dom h (s x) ->
    bigstep (mutation x e) (h, s) None
| step_new (x: V) (e: expr) (h: heap) (s: store) (n: Z):
    ~(dom h n) ->
    bigstep (new x e) (h, s)
      (Some (heap_update h n (eval e s), store_update s x n))
| step_dispose (x: V) (h: heap) (s: store):
    dom h (s x) ->
    bigstep (dispose x) (h, s) (Some (heap_clear h (s x), s))
| step_dispose_fail (x: V) (h: heap) (s: store):
    ~dom h (s x) ->
    bigstep (dispose x) (h, s) None
| step_skip (h: heap) (s: store):
    bigstep skip (h, s) (Some (h, s))
| step_comp (S1 S2: program) (h h' h'': heap) (s s' s'': store):
    bigstep S1 (h, s) (Some (h', s')) ->
    bigstep S2 (h', s') (Some (h'', s'')) ->
    bigstep (comp S1 S2) (h, s) (Some (h'', s''))
| step_comp_fail1 (S1 S2: program) (h: heap) (s: store):
    bigstep S1 (h, s) None ->
    bigstep (comp S1 S2) (h, s) None
| step_comp_fail2 (S1 S2: program) (h h': heap) (s s': store):
    bigstep S1 (h, s) (Some (h', s')) ->
    bigstep S2 (h', s') None ->
    bigstep (comp S1 S2) (h, s) None
| step_ite_true (g: guard) (S1 S2: program) (h: heap) (s: store) o:
    g s = true ->
    bigstep S1 (h, s) o ->
    bigstep (ite g S1 S2) (h, s) o
| step_ite_false (g: guard) (S1 S2: program) (h: heap) (s: store) o:
    g s = false ->
    bigstep S2 (h, s) o ->
    bigstep (ite g S1 S2) (h, s) o
| step_while_true (g: guard) (S1: program) (h h': heap) (s s': store) o:
    g s = true ->
    bigstep S1 (h, s) (Some (h', s')) ->
    bigstep (while g S1) (h', s') o ->
    bigstep (while g S1) (h, s) o
| step_while_false (g: guard) (S1: program) (h: heap) (s: store):
    g s = false ->
    bigstep (while g S1) (h, s) (Some (h, s))
| step_while_fail (g: guard) (S1: program) (h: heap) (s: store):
    g s = true ->
    bigstep S1 (h, s) None ->
    bigstep (while g S1) (h, s) None.

Proposition diverge_empty (h: heap) (s: store):
  forall o, ~bigstep diverge (h, s) o.
intros; intro; inversion H.
Qed.

Fixpoint approx (n: nat) (g: guard) (S1: program): program :=
  match n with
  | O => diverge
  | S m => ite g (comp S1 (approx m g S1)) skip
  end.

Proposition while_approx (g: guard) (S1: program):
  forall h s o,
    bigstep (while g S1) (h, s) o <->
    exists n, bigstep (approx n g S1) (h, s) o.
intros; split; intro.
- remember (while g S1).
  induction H; try inversion Heqp.
  + apply IHbigstep2 in Heqp.
    destruct Heqp.
    exists (S x).
    simpl.
    apply step_ite_true.
    rewrite <- H3. apply H.
    destruct o; [destruct p|].
    eapply step_comp.
    rewrite <- H4. apply H0. apply H2.
    eapply step_comp_fail2.
    rewrite <- H4. apply H0. apply H2.
  + exists 1.
    simpl.
    apply step_ite_false.
    rewrite <- H1. apply H.
    apply step_skip.
  + exists 1.
    simpl.
    apply step_ite_true.
    rewrite <- H2. apply H.
    apply step_comp_fail1.
    rewrite <- H3. apply H0.
- destruct H.
  generalize dependent h.
  generalize dependent s.
  generalize dependent o.
  induction x; intros.
  + simpl in H.
    exfalso.
    pose proof (diverge_empty h s).
    specialize H0 with o.
    apply H0; auto.
  + simpl in H.
    inversion H.
    inversion H7.
    apply IHx in H14.
    eapply step_while_true.
    apply H6.
    apply H13.
    apply H14.
    apply step_while_fail.
    apply H6.
    apply H13.
    apply IHx in H14.
    eapply step_while_true.
    apply H6.
    apply H13.
    apply H14.
    inversion H7.
    eapply step_while_false.
    apply H6.
Qed.

Definition omega: program := while true skip.

Proposition omega_diverge_equiv:
  forall h s o,
    bigstep omega (h, s) o <->
    bigstep diverge (h, s) o.
intros. unfold omega.
rewrite while_approx.
split; intro.
destruct H.
generalize dependent s.
generalize dependent h.
induction x; intros; simpl in H.
auto.
inversion H.
inversion H7.
rewrite H11.
apply IHx.
inversion H13.
rewrite <- H11. assumption.
inversion H13.
rewrite H11.
apply IHx.
rewrite <- H11.
inversion H13. assumption.
inversion H6.
inversion H.
Qed.

(* ============= *)
(* HOARE TRIPLES *)
(* ============= *)

Inductive hoare :=
| mkhoare: assert -> program -> assert -> hoare.

Definition pre: hoare -> assert := fun '(mkhoare p _ _) => p.
Definition S: hoare -> program := fun '(mkhoare _ x _) => x.
Definition post: hoare -> assert := fun '(mkhoare _ _ q) => q.

Definition restrict_post: hoare -> Prop := fun '(mkhoare _ S1 q) =>
  match S1 with
  | assign S1 => match S1 with
    | basic x e => (forall y, In y (evar e) -> ~In y (abound q))
    | lookup x e => True
    | mutation x e => (forall y, In y (x :: evar e) -> ~In y (abound q))
    | new x e => ~In x (evar e) /\ (forall y, In y (x :: evar e) -> ~In y (abound q))
    | dispose x => ~In x (abound q)
    end
  | _ => False
  end.

Definition restrict_pre: hoare -> Prop := fun '(mkhoare p S1 _) =>
  match S1 with
  | assign S1 => match S1 with
    | basic x e => ~In x (abound p)
    | lookup x e => ~In x (abound p)
    | mutation x e => ~In x (abound p)
    | new x e => ~In x (evar e) /\ ~In x (abound p)
    | dispose x => ~In x (abound p)
    end
  | _ => False
  end.

Definition restrict (pSq: hoare): Prop := restrict_post pSq /\ restrict_pre pSq.

(* ======================================================================= *)
(* WEAKEST PRECONDITION AXIOMATIZATION (WP-CSL), SEE FIGURE 3 IN THE PAPER *)
(* ======================================================================= *)

Inductive WPCSL_FULL (Gamma: assert -> Prop): hoare -> Set :=
(* Rules for assignments *)
| wpcf_basic (p ps: assert) (x: V) (e: expr):
    asub p x e = Some ps ->
    WPCSL_FULL Gamma (mkhoare ps (basic x e) p)
| wpcf_lookup (p ps: assert) (x y: V) (e: expr):
    ~In y (x :: aoccur p ++ evar e) ->
    asub p x y = ps ->
    WPCSL_FULL Gamma (mkhoare (lexists y (land (hasval e y) ps)) (lookup x e) p)
| wpcf_mutation (p ps: assert) (x: V) (e: expr):
    asub_heap_update p x e = ps ->
    WPCSL_FULL Gamma (mkhoare (land (hasvaldash x) ps) (mutation x e) p)
| wpcf_new (p ps: assert) (x: V) (e: expr):
    ~In x (evar e) ->
    asub_heap_update p x e = ps ->
    WPCSL_FULL Gamma (mkhoare (lforall x (limp (lnot (hasvaldash x)) ps)) (new x e) p)
| wpcf_new_util (p q: assert) (x y: V) (e: expr):
    ~In y (x :: aoccur p ++ aoccur q ++ evar e) ->
    WPCSL_FULL Gamma (mkhoare p (comp (basic y e) (new x y)) q) ->
    WPCSL_FULL Gamma (mkhoare p (new x e) q)
| wpcf_dispose (p ps: assert) (x: V):
    asub_heap_clear p x = ps ->
    WPCSL_FULL Gamma (mkhoare (land (hasvaldash x) ps) (dispose x) p)
(* Standard compositional rules *)
| wpcf_skip (p: assert):
    WPCSL_FULL Gamma (mkhoare p skip p)
| wpcf_diverge (p: assert):
    WPCSL_FULL Gamma (mkhoare p diverge false)
| wpcf_compose (p q r: assert) (S1 S2: program):
    WPCSL_FULL Gamma (mkhoare p S1 r) ->
    WPCSL_FULL Gamma (mkhoare r S2 q) ->
    WPCSL_FULL Gamma (mkhoare p (comp S1 S2) q)
| wpcf_ite (p q: assert) (g: guard) (S1 S2: program):
    WPCSL_FULL Gamma (mkhoare (land p g) S1 q) ->
    WPCSL_FULL Gamma (mkhoare (land p (lnot g)) S2 q) ->
    WPCSL_FULL Gamma (mkhoare p (ite g S1 S2) q)
| wpcf_while (p: assert) (g: guard) (S1: program):
    WPCSL_FULL Gamma (mkhoare (land p g) S1 p) ->
    WPCSL_FULL Gamma (mkhoare p (while g S1) (land p (lnot g)))
| wpcf_conseq (p pp q qq: assert) (x: program):
    Gamma (limp pp p) -> WPCSL_FULL Gamma (mkhoare p x q) -> Gamma (limp q qq) ->
    WPCSL_FULL Gamma (mkhoare pp x qq).

Inductive WPCSL (Gamma: assert -> Prop): hoare -> Set :=
| wpc_basic (p ps: assert) (x: V) (e: expr):
    asub p x e = Some ps ->
    WPCSL Gamma (mkhoare ps (basic x e) p)
| wpc_lookup (p ps: assert) (x y: V) (e: expr):
    ~In y (x :: aoccur p ++ evar e) ->
    asub p x y = ps ->
    WPCSL Gamma (mkhoare (lexists y (land (hasval e y) ps)) (lookup x e) p)
| wpc_mutation (p ps: assert) (x: V) (e: expr):
    asub_heap_update p x e = ps ->
    WPCSL Gamma (mkhoare (land (hasvaldash x) ps) (mutation x e) p)
| wpc_new (p ps: assert) (x: V) (e: expr):
    ~In x (evar e) ->
    asub_heap_update p x e = ps ->
    WPCSL Gamma (mkhoare (lforall x (limp (lnot (hasvaldash x)) ps)) (new x e) p)
| wpc_dispose (p ps: assert) (x: V):
    asub_heap_clear p x = ps ->
    WPCSL Gamma (mkhoare (land (hasvaldash x) ps) (dispose x) p)
| wpc_conseq (p pp q qq: assert) (x: program):
    Gamma (limp pp p) -> WPCSL Gamma (mkhoare p x q) -> Gamma (limp q qq) ->
    WPCSL Gamma (mkhoare pp x qq).

(* ======================================================================= *)
(* GLOBAL WEAKEST PRECONDITION AXIOMATIZATION USING SEPARATING CONNECTIVES *)
(* ======================================================================= *)

Inductive WPCSL_SEP (Gamma: assert -> Prop): hoare -> Set :=
| wpcs_basic (p ps: assert) (x: V) (e: expr):
    asub p x e = Some ps ->
    WPCSL_SEP Gamma (mkhoare ps (basic x e) p)
| wpcs_lookup (p ps: assert) (x y: V) (e: expr):
    ~In y (x :: aoccur p ++ evar e) ->
    asub p x y = ps ->
    WPCSL_SEP Gamma (mkhoare (lexists y (land (hasval e y) ps)) (lookup x e) p)
| wpcs_mutation (p: assert) (x: V) (e: expr):
    WPCSL_SEP Gamma (mkhoare (sand (pointstodash x) (simp (pointsto x e) p)) (mutation x e) p)
| wpcs_new (p ps: assert) (x y: V) (e: expr):
    ~In y (x :: aoccur p ++ evar e) ->
    asub p x y = ps ->
    WPCSL_SEP Gamma (mkhoare (lforall y (simp (pointsto y e) ps)) (new x e) p)
| wpcs_dispose (p: assert) (x: V):
    WPCSL_SEP Gamma (mkhoare (sand (pointstodash x) p) (dispose x) p)
| wpcs_conseq (p pp q qq: assert) (x: program):
    Gamma (limp pp p) -> WPCSL_SEP Gamma (mkhoare p x q) -> Gamma (limp q qq) ->
    WPCSL_SEP Gamma (mkhoare pp x qq).

(* ========================================================================== *)
(* STRONGEST POSTCONDITION AXIOMATIZATION (SP-CSL), SEE FIGURE 6 IN THE PAPER *)
(* ========================================================================== *)

Inductive SPCSL (Gamma: assert -> Prop): hoare -> Set :=
| spc_basic (p ps: assert) (x y: V) (e: expr):
    ~In y (x :: aoccur p ++ evar e) ->
    asub p x y = Some ps ->
    SPCSL Gamma (mkhoare p (basic x e) (lexists y (land ps (equals (esub e x y) x))))
| spc_lookup (p ps: assert) (x y: V) (e: expr):
    ~In y (x :: aoccur p ++ evar e) ->
    asub p x y = Some ps ->
    SPCSL Gamma (mkhoare (land p (hasvaldash e)) (lookup x e) (lexists y (land ps (hasval (esub e x y) x))))
| spc_mutation (p ps: assert) (x y: V) (e: expr):
    ~In y (x :: aoccur p ++ evar e) ->
    asub_heap_update p x y = Some ps ->
    SPCSL Gamma (mkhoare (land p (hasvaldash x)) (mutation x e) (land (lexists y ps) (hasval x e)))
| spc_new (p ps pss: assert) (x y: V) (e: expr):
    ~In x (evar e) ->
    ~In y (x :: aoccur p ++ evar e) ->
    asub p x y = Some ps ->
    asub_heap_clear (lexists y ps) x = Some pss ->
    SPCSL Gamma (mkhoare p (new x e) (land pss (hasval x e)))
| spc_dispose (p ps: assert) (x y: V):
    ~In y (x :: aoccur p) ->
    asub_heap_update p x y = Some ps ->
    SPCSL Gamma (mkhoare (land p (hasvaldash x)) (dispose x) (land (lexists y ps) (lnot (hasvaldash x))))
| spc_conseq (p pp q qq: assert) (x: program):
    Gamma (limp pp p) -> SPCSL Gamma (mkhoare p x q) -> Gamma (limp q qq) ->
    SPCSL Gamma (mkhoare pp x qq).

(* ============================================ *)
(* WEAKEST PRECONDITION AXIOMATIZATION (WP-ISL) *)
(* ============================================ *)

Inductive WPISL (Gamma: assert -> Prop): hoare -> Set :=
| wpi_basic (p ps: assert) (x: V) (e: expr):
    asub p x e = Some ps ->
    WPISL Gamma (mkhoare ps (basic x e) p)
| wpi_lookup (p ps: assert) (x y: V) (e: expr):
    ~In y (x :: aoccur p ++ evar e) ->
    asub p x y = ps ->
    WPISL Gamma (mkhoare (lexists y (land (hasval e y) ps)) (lookup x e) p)
| wpi_mutation (p ps: assert) (x: V) (e: expr):
    asub_cheap_update p x e = ps ->
    WPISL Gamma (mkhoare (land (hasvaldash x) ps) (mutation x e) p)
| wpi_new (p ps: assert) (x: V) (e: expr):
    ~In x (evar e) ->
    asub_cheap_update p x e = ps ->
    WPISL Gamma (mkhoare (lforall x (lor (hasvaldash x) (limp (hasvaldash x) ps))) (new x e) p)
| wpi_dispose (p ps: assert) (x: V):
    asub_cheap_clear p x = ps ->
    WPISL Gamma (mkhoare (land (hasvaldash x) ps) (dispose x) p)
| wpi_conseq (p pp q qq: assert) (x: program):
    Gamma (limp pp p) -> WPISL Gamma (mkhoare p x q) -> Gamma (limp q qq) ->
    WPISL Gamma (mkhoare pp x qq).

(* =============================================== *)
(* STRONGEST POSTCONDITION AXIOMATIZATION (SP-ISL) *)
(* =============================================== *)

Inductive SPISL (Gamma: assert -> Prop): hoare -> Set :=
| spi_basic (p ps: assert) (x y: V) (e: expr):
    ~In y (x :: aoccur p ++ evar e) ->
    asub p x y = Some ps ->
    SPISL Gamma (mkhoare p (basic x e) (lexists y (land ps (equals (esub e x y) x))))
| spi_lookup (p ps: assert) (x y: V) (e: expr):
    ~In y (x :: aoccur p ++ evar e) ->
    asub p x y = Some ps ->
    SPISL Gamma (mkhoare (land p (hasvaldash e)) (lookup x e) (lexists y (land ps (hasval (esub e x y) x))))
| spi_mutation (p ps: assert) (x y: V) (e: expr):
    ~In y (x :: aoccur p ++ evar e) ->
    asub_cheap_update p x y = Some ps ->
    SPISL Gamma (mkhoare (land p (hasvaldash x)) (mutation x e) (land (lexists y ps) (hasval x e)))
| spi_new (p ps pss: assert) (x y: V) (e: expr):
    ~In x (evar e) ->
    ~In y (x :: aoccur p ++ evar e) ->
    asub p x y = Some ps ->
    asub_cheap_clear (lexists y ps) x = Some pss ->
    SPISL Gamma (mkhoare p (new x e) (land pss (hasval x e)))
| spi_dispose (p ps: assert) (x y: V):
    ~In y (x :: aoccur p) ->
    asub_cheap_update p x y = Some ps ->
    SPISL Gamma (mkhoare (land p (hasvaldash x)) (dispose x) (limp (hasvaldash x) (lexists y ps)))
| spi_conseq (p pp q qq: assert) (x: program):
    Gamma (limp pp p) -> SPISL Gamma (mkhoare p x q) -> Gamma (limp q qq) ->
    SPISL Gamma (mkhoare pp x qq).

End Language.

author: praalhans

repo: OSL

save_path: github-repos/coq/praalhans-OSL


Require Import List.
Import ListNotations.
Require Import Lia.
Require Import Coq.Arith.PeanoNat.

From Scheduler.Model Require Import PureFunctionModels.
From Scheduler.Model.Interface.Types Require Import TypesModel Jobs.

From Scheduler.Proof Require Import Lib JobsAxioms.

Module  Type AssumptionsMod (J : JobsAxiomsMod).
  Import J.

  Parameter c : nat -> nat -> nat.
  Parameter run : nat -> nat -> bool.

  Axiom at_most_one_runs: forall (i j t : nat),
      i < N -> j < N ->
      run  i t  = true -> run  j t = true -> i = j.

  Axiom c_is_duration_upto_arrival : forall (i t : nat), i < N ->
      t <= arrival (Jobs i) -> c  i t = duration (Jobs i).

  Axiom c_decreases_when_running : forall ( i t : nat), i < N ->
      run  i t  = true -> (c i t  > 0 /\
                        c  i (S t)  = c i t - 1).

  Axiom c_constant_when_not_running : forall ( i t : nat), i < N ->
      run  i t  = false -> c  i (S t) = c  i t.

  Definition sum_counters_arrived( t : nat) :=
    generic_sum
      (fun i  => c  i t)
        (fun i  => arrival(Jobs i) <=? t)
        0 N.

  Axiom sum_arrived_some_running : forall  t,
      sum_counters_arrived t > 0 -> exists j, j < N /\ run  j t = true.

End AssumptionsMod.


text:
(* I suggest you start by reading the comments and some of the definitions in Modeling.v
   Then reading the problem statement and hints in Problem.v *)
Require Import Frap Modeling Helpers.
Require Import Problem.

(* Start by implementing fibonacci recursively. *)
Fixpoint fib (n: nat) : nat := 0.

(* You are not required to prove these lemmas, but they will help you prove the main theorem.
   If you are stuck, use admit and Admitted to skip certain parts of the proofs or certain lemmas.
   You will still be able to use skipped lemmas during other proofs *)
Lemma fib_iterative_buildup: forall (n: nat) (v: valuation),
  repeat_interpreter (S n) fib_loop_body (v $+ ("pre", 0) $+ ("cur", 1)) $! "pre" =
  repeat_interpreter (n) fib_loop_body (v $+ ("pre", 0) $+ ("cur", 1)) $! "cur".
Proof.
Admitted.

Lemma fib_iterative_loop_correct: forall (n: nat) (v: valuation),
  repeat_interpreter n fib_loop_body (v $+ ("pre", 0) $+ ("cur", 1)) $! "cur" = fib n.
Proof.
Admitted.

Lemma fib_iterative_correct': forall (n: nat) (v: valuation),
  (interpret' (fib_iterative n) v) $! "ret_" = fib n.
Proof.
Admitted.

(* Main theorem: Prove this for full credit *)
Theorem fib_iterative_correct: forall (n: nat),
  interpret (fib_iterative n) = fib n.
Proof.
Admitted.

author: KinanBab


text:
(*
    Copyright (C) 2012  G. Gonthier, B. Ziliani, A. Nanevski, D. Dreyer

    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <http://www.gnu.org/licenses/>.
*)

From mathcomp
Require Import ssreflect ssrfun ssrbool ssrnat seq.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(***********************************)
(* option lookup and list prefixes *)
(***********************************)

Section Prefix.
Variable A : Type.

Fixpoint onth (s : seq A) n : option A :=
  if s is x :: s' then
    if n is n'.+1 then onth s' n' else Some x
  else None.

Definition prefix s1 s2 :=
  forall n x, onth s1 n = some x -> onth s2 n = some x.

Lemma size_onth (s : seq A) n : n < size s -> exists x, onth s n = Some x.
Proof.
elim:s n=>[//|x' s' IH] [|n] /=.
- by move=>_; exists x'.
rewrite -(addn1 n) -(addn1 (size s')) ltn_add2r.
by apply: IH.
Qed.

Lemma onth_size (s : seq A) n x : onth s n = Some x -> n < size s.
Proof. by elim:s n=>[//|x' s' IH] [//|n]; apply: IH. Qed.

Lemma prefix_refl s : prefix s s.
Proof. by move=>n x <-. Qed.

Lemma prefix_trans (s2 s1 s3 : seq A) :
        prefix s1 s2 -> prefix s2 s3 -> prefix s1 s3.
Proof. by move=>H1 H2 n x E; apply: H2; apply: H1. Qed.

Lemma prefix_cons x s1 s2 : prefix (x :: s1) (x :: s2) <-> prefix s1 s2.
Proof. by split=>E n; [apply: (E n.+1) | case: n]. Qed.

Lemma prefix_cons' x y s1 s2 : prefix (x :: s1) (y :: s2) -> x = y /\ prefix s1 s2.
Proof.
move=>H; move: (H 0 x (erefl _))=>[H'].
by move: H; rewrite H' prefix_cons.
Qed.

Lemma prefix_size (s t : seq A) : prefix s t -> size s <= size t.
Proof.
elim: s t=>[//|a s IH] [|b t] H; first by move: (H 0 a (erefl _)).
by rewrite ltnS; apply: (IH _ (proj2 (prefix_cons' H))).
Qed.

Lemma prefix_onth (s t : seq A) x : x < size s -> prefix s t -> onth s x = onth t x.
Proof.
elim:s t x =>[//|a s IH] [|b t] x H1 H2; first by move: (H2 0 a (erefl _)).
apply prefix_cons' in H2.
case: x H1=>[_|n H1]; first by rewrite (proj1 H2).
by apply: IH=>//; exact (proj2 H2).
Qed.

End Prefix.

Hint Resolve prefix_refl : core.

author: coq-community

repo: lemma-overloading


text:
Load LFindLoad.
Load LFindLoad.
From adtind Require Import goal80.

From lfind Require Import LFind.
Require Import Extraction.
Extract Inductive nat => nat [ "(O)" "S" ].
Extract Inductive list => list [ "Nil" "Cons" ].
Extraction "/home/yousef/lemmafinder/benchmark/_lfind_clam_lf_goal80_theorem0_59_rev_append/goal80_lfind_orig.ml"  adtind.goal80.rev adtind.goal80.append.
Success.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker