Library CFML.CFDemos

Set Implicit Arguments.
Require Import LibCore Shared CFHeaps.

Open Scope heap_scope.

Axiom Ref : int->loc->hprop.

Definition R' n p := p ~> Ref n.

Definition R n p := Hexists m, p ~> R' (n+m) \* \[m = 0].

Lemma xunfold_repr_at_demo_4 :
  forall (F:hprop->(loc->hprop)->Prop),
  forall p n,
  F (p ~> R n) (fun p' => Hexists n', p' ~> R n').
Proof using.
  intros. dup 2.
  xunfold R at 1. unfold R at 1. xunfold R at 1. admit.
  xunfold R at 2. xunfold R at 1.
Abort.

Lemma xunfold_repr_demo_3 :
  forall (F:hprop->(loc->hprop)->Prop),
  forall p n,
  F (p ~> R n \* p ~> Ref n) (fun p' => Hexists n', p' ~> R n').
Proof using.
  intros.
  xunfold R.
  xunfold R'.
Abort.

Lemma xunfold_clean_demo_2 :
  forall (F:hprop->(loc->hprop)->Prop),
  forall p n,
  F (p ~> R n) (fun p' => Hexists n', p' ~> R n').
Proof using.
  intros. dup 2.
  unfold R at 1. xunfold_clean. admit.
  unfold R at 2. xunfold_clean.
Abort.
Lemma xunfold_at_demo_1 :
  forall (F:hprop->(loc->hprop)->Prop),
  forall p n,
  F (p ~> R n) (fun p' => Hexists n', p' ~> R n').
Proof using.
  intros.
  xunfold at 1.
  unfold R at 1.
  xunfold at 1.
  unfold R' at 1.
  xunfold at 2.
  unfold R at 1.
  xunfold at 2.
  unfold R' at 1.
Abort.

Lemma hsimpl_demo_1 : forall H1 H2 H3 H4 H5,
  H1 \* H2 \* H3 \* H4 ==> H4 \* H3 \* H5 \* H2.
Proof using.
  intros. dup.
  hsimpl_setup tt.
  hsimpl_step tt.
  hsimpl_step tt.
  hsimpl_step tt.
  hsimpl_step tt.
  hsimpl_step tt.
  try hsimpl_step tt.
  hsimpl_cleanup tt.
  skip.   hsimpl. skip. Admitted.
Lemma hsimpl_demo_2 : forall (l1 l2:loc) S1 S2 H1 H2 H3 H',
  (forall X S1' HG, X ==> H1 \* l1 ~> S1' \* H2 \* HG -> X ==> H') ->
  H1 \* l1 ~> S1 \* l2 ~> S2 \* H3 ==> H'.
Proof using.
  intros. dup.
  eapply H.
  hsimpl_setup tt.
  hsimpl_step tt.
  hsimpl_step tt.
  hsimpl_step tt.
  hsimpl_step tt.
  hsimpl_step tt.
  try hsimpl_step tt.
  hsimpl_cleanup tt.
  skip.   eapply H.
  hsimpl. skip. Admitted.
Lemma hsimpl_demo_3 : forall (l1 l2:loc) S1 S2 H1 H2 H',
  (forall X S1' HG, X ==> H1 \* l1 ~> S1' \* HG -> HG = HG -> X ==> H') ->
  H1 \* l1 ~> S1 \* l2 ~> S2 \* H2 ==> H'.
Proof using.
  intros. dup.
  eapply H.
  hsimpl_setup tt.
  hsimpl_step tt.
  hsimpl_step tt.
  hsimpl_step tt.
  hsimpl_step tt.
  try hsimpl_step tt.
  hsimpl_cleanup tt.
  skip.
  auto.
  eapply H.
  hsimpl.
  auto.
Admitted.

Require Import CFApp CFTactics.

Definition demo_arglist :=
  forall f (xs:list int) (x y:int) B H (Q:B->hprop),
  app f [ x y ] H Q.

Module RecordDemo.

Definition f := 0%nat.
Definition g := 1%nat.

Definition demo1 r :=
  r ~> `{ f := 1+1 ; g := 1 }.

Lemma demo_get_1 : forall r,
  app_keep record_get [r f] (r ~> `{ f := 1+1 ; g := 1 }) \[= 2].
Proof using.
  intros.
  xspec_record_get_compute tt. intros G. apply G.
Qed.

Lemma demo_get_2 : forall r,
  app_keep record_get [r g] (r ~> `{ f := 1+1 ; g := 1 }) \[= 1].
Proof using.
  intros.
  xspec_record_get_compute tt. intros G. apply G.
Qed.

Lemma demo_get_3 : forall r,
  app_keep record_get [r g] (r ~> `{ g := 1 }) \[= 1].
Proof using.
  intros.
  xspec_record_get_compute tt. intros G. apply G.
Qed.

Lemma demo_set_1 : forall r,
  (forall H',
    app record_set [r f 4] (r ~> `{ f := 1+1 ; g := 1 }) (#H') -> True)
  -> True.
Proof using.
  introv M. applys (rm M).
  xspec_record_set_compute tt. intros G. apply G.
Qed.

End RecordDemo.