Library CFML.Stdlib.Pervasives_proof

Set Implicit Arguments.
Require Import CFLib.
Require Import Pervasives_ml.
Generalizable Variable A.

Lemma not_spec : forall (a:bool),
  app not [a] \[] \[= !a ].
Proof using.
  xcf. xgo*.
Qed.

Hint Extern 1 (RegisterSpec not) => Provide not_spec.

Parameter infix_eq_eq_loc_spec : curried 2%nat infix_eq_eq__ /\
  forall (a b:loc),
  app infix_eq_eq__ [a b] \[] \[= isTrue (a = b) ].

Parameter infix_eq_eq_gen_spec : curried 2%nat infix_eq_eq__ /\
  forall (A:Type) (a b:A),
  app infix_eq_eq__ [a b] \[] (fun r => \[r = true -> isTrue (a = b)]).

Hint Extern 1 (RegisterSpec infix_eq_eq__) => Provide infix_eq_eq_loc_spec.

Lemma infix_emark_eq_loc_spec : curried 2%nat infix_emark_eq__ /\
  forall (a b:loc),
  app infix_emark_eq__ [a b] \[] \[= isTrue (a <> b) ].
Proof using.
  xcf. xgo*. rew_isTrue; xauto*.
Qed.

Lemma infix_emark_eq_gen_spec : curried 2%nat infix_emark_eq__ /\
  forall (A:Type) (a b:A),
  app infix_emark_eq__ [a b] \[] (fun r => \[r = false -> isTrue (a = b)]).
Proof using.
  xcf. xapp_spec infix_eq_eq_gen_spec.
  introv E. xrets~.
Qed.

Hint Extern 1 (RegisterSpec infix_emark_eq__) => Provide infix_emark_eq_loc_spec.

Parameter infix_eq_spec : curried 2%nat infix_eq__ /\
  forall A (a b : A),
  (polymorphic_eq_arg a \/ polymorphic_eq_arg b) ->
  app infix_eq__ [a b] \[] \[= isTrue (a = b) ].

Hint Extern 1 (RegisterSpec infix_eq__) => Provide infix_eq_spec.

Parameter infix_neq_spec : curried 2%nat infix_eq__ /\
  forall A (a b : A),
  (polymorphic_eq_arg a \/ polymorphic_eq_arg b) ->
  app infix_lt_gt__ [a b] \[] \[= isTrue (a <> b) ].

Hint Extern 1 (RegisterSpec infix_lt_gt__) => Provide infix_neq_spec.

Lemma min_spec : forall (n m:int),
  app min [n m] \[] \[= Z.min n m ].
Proof using.
  xcf. xgo*.
  { rewrite~ Z.min_l. }
  { rewrite~ Z.min_r. math. }
Qed.

Lemma max_spec : forall (n m:int),
  app max [n m] \[] \[= Z.max n m ].
Proof using.
  xcf. xgo*.
  { rewrite~ Z.max_l. }
  { rewrite~ Z.max_r. math. }
Qed.

Hint Extern 1 (RegisterSpec min) => Provide min_spec.
Hint Extern 1 (RegisterSpec max) => Provide max_spec.

Parameter infix_bar_bar_spec : forall (a b:bool),
  app infix_bar_bar__ [a b] \[] \[= a && b ].

Parameter infix_amp_amp_spec : forall (a b:bool),
  app infix_amp_amp__ [a b] \[] \[= a || b ].

Hint Extern 1 (RegisterSpec infix_bar_bar__) => Provide infix_bar_bar_spec.
Hint Extern 1 (RegisterSpec infix_amp_amp__) => Provide infix_amp_amp_spec.

Parameter infix_tilde_minus_spec : curried 1%nat infix_tilde_minus__ /\
  forall (n:int),
  app infix_tilde_minus__ [n] \[] \[= Z.opp n ].

Parameter infix_plus_spec : curried 2%nat infix_plus__ /\
  forall (n m:int),
  app infix_plus__ [n m] \[] \[= Z.add n m ].

Parameter infix_minus_spec : curried 2%nat infix_minus__ /\
  forall (n m:int),
  app infix_minus__ [n m] \[] \[= Z.sub n m ].

Parameter infix_star_spec : curried 2%nat infix_star__ /\
  forall (n m:int),
  app infix_star__ [n m] \[] \[= Z.mul n m ].

Parameter infix_slash_spec : curried 2%nat infix_slash__ /\
  forall (n m:int),
  m <> 0 ->
  app infix_slash__ [n m] \[] \[= Z.quot n m ].

Parameter mod_spec : curried 2%nat Pervasives_ml.mod /\ forall (n m:int),
  m <> 0 ->
  app Pervasives_ml.mod [n m] \[] \[= Z.rem n m ].

Hint Extern 1 (RegisterSpec infix_tilde_minus__) => Provide infix_tilde_minus_spec.
Hint Extern 1 (RegisterSpec infix_plus__) => Provide infix_plus_spec.
Hint Extern 1 (RegisterSpec infix_minus__) => Provide infix_minus_spec.
Hint Extern 1 (RegisterSpec infix_star__) => Provide infix_star_spec.
Hint Extern 1 (RegisterSpec infix_slash__) => Provide infix_slash_spec.
Hint Extern 1 (RegisterSpec Pervasives_ml.mod) => Provide mod_spec.

Notation "x `/` y" := (Z.quot x y)
  (at level 69, right associativity) : charac.
Notation "x `mod` y" := (Z.rem x y)
  (at level 69, no associativity) : charac.


Lemma succ_spec : forall (n:int),
  app succ [n] \[] \[= n+1 ].
Proof using.
  xcf. xgo*.
Qed.

Lemma pred_spec : forall (n:int),
  app pred [n] \[] \[= n-1 ].
Proof using.
  xcf. xgo*.
Qed.

Lemma abs_spec : forall (n:int),
  app Pervasives_ml.abs [n] \[] \[= Z.abs n ].
Proof using.
  xcf. xgo.
  { rewrite~ Z.abs_eq. }
  { rewrite~ Z.abs_neq. math. }
Qed.

Hint Extern 1 (RegisterSpec succ) => Provide succ_spec.
Hint Extern 1 (RegisterSpec pred) => Provide pred_spec.
Hint Extern 1 (RegisterSpec abs) => Provide abs_spec.

Parameter land_spec : curried 2%nat land /\ forall (n m:int),
  app land [n m] \[] \[= Z.land n m ].

Parameter lor_spec : curried 2%nat lor /\ forall (n m:int),
  app lor [n m] \[] \[= Z.lor n m ].

Parameter lxor_spec : curried 2%nat lxor /\ forall (n m:int),
  app lxor [n m] \[] \[= Z.lxor n m ].

Definition Zlnot (x : Z) : Z := -(x + 1).

Parameter lnot_spec : curried 1%nat lnot /\ forall (n:int),
  app lnot [n] \[] \[= Zlnot n ].

Parameter lsl_spec : curried 2%nat lsl /\ forall (n m:int),
  0 <= m ->
  app lsl [n m] \[] \[= Z.shiftl n m ].


Parameter lsr_spec : curried 2%nat lsr /\ forall (n m:int),
  0 <= n ->
  0 <= m ->
  
  app lsr [n m] \[] \[= Z.shiftr n m ].

Parameter asr_spec : curried 2%nat asr /\ forall (n m:int),
  0 <= m ->
  
  app asr [n m] \[] \[= Z.shiftr n m ].

Hint Extern 1 (RegisterSpec land) => Provide land_spec.
Hint Extern 1 (RegisterSpec lor) => Provide lor_spec.
Hint Extern 1 (RegisterSpec lxor) => Provide lxor_spec.
Hint Extern 1 (RegisterSpec lnot) => Provide lnot_spec.
Hint Extern 1 (RegisterSpec lsl) => Provide lsl_spec.
Hint Extern 1 (RegisterSpec land) => Provide land_spec.
Hint Extern 1 (RegisterSpec lsr) => Provide lsr_spec.
Hint Extern 1 (RegisterSpec asr) => Provide asr_spec.

Definition Ref {A} (v:A) (r:loc) :=
  r ~> `{ contents' := v }.

Axiom Ref_Heapdata : forall A,
  (Heapdata (@Ref A)).

Existing Instance Ref_Heapdata.

Notation "r '~~>' v" := (hdata (Ref v) r)
  (at level 32, no associativity) : heap_scope.

Lemma affine_Ref : forall A r (v: A), affine (r ~~> v).
Proof. intros. unfold Ref, hdata. affine. Qed.

Hint Resolve affine_Ref : affine.

Hint Transparent ref_ : affine.

Lemma ref_spec : forall A (v:A),
  app ref [v]
    PRE \[]
    POST (fun r => r ~~> v).
Proof using. xcf_go~. Qed.

Lemma infix_emark_spec : forall A (v:A) r,
  app infix_emark__ [r]
    INV (r ~~> v)
    POST \[= v].
Proof using. xunfold @Ref. xcf_go~. Qed.

Lemma infix_colon_eq_spec : forall A (v w:A) r,
  app infix_colon_eq__ [r w] (r ~~> v) (# r ~~> w).
Proof using. xunfold @Ref. xcf_go~. Qed.

Hint Extern 1 (RegisterSpec ref) => Provide ref_spec.
Hint Extern 1 (RegisterSpec infix_emark__) => Provide infix_emark_spec.
Hint Extern 1 (RegisterSpec infix_colon_eq__) => Provide infix_colon_eq_spec.

Notation "'App'' `! r" := (App infix_emark__ r;)
  (at level 69, no associativity, r at level 0,
   format "'App'' `! r") : charac.

Notation "'App'' r `:= x" := (App infix_colon_eq__ r x;)
  (at level 69, no associativity, r at level 0,
   format "'App'' r `:= x") : charac.

Lemma incr_spec : forall (n:int) r,
  app incr [r]
    PRE (r ~~> n)
    POST (# r ~~> (n+1)).
Proof using. xcf_go~. Qed.

Lemma decr_spec : forall (n:int) r,
  app decr [r]
    PRE (r ~~> n)
    POST (# r ~~> (n-1)).
Proof using. xcf_go~. Qed.

Hint Extern 1 (RegisterSpec incr) => Provide incr_spec.
Hint Extern 1 (RegisterSpec decr) => Provide decr_spec.

Axiom ref_spec_group : forall A (M:map loc A) (v:A),
  app Pervasives_ml.ref [v]
    PRE (Group Ref M)
    POST (fun (r:loc) => Group Ref (M[r:=v]) \* \[r \notindom M]).

Lemma infix_emark_spec_group : forall `{Inhab A} (M:map loc A) r,
  r \indom M ->
  app Pervasives_ml.infix_emark__ [r]
    INV (Group Ref M)
    POST (fun x => \[x = M[r]]).
Proof using.
  intros. rewrite~ (Group_rem r M). xapp. xsimpl~.
Qed.

Lemma infix_colon_eq_spec_group : forall `{Inhab A} (M:map loc A) (v:A) r,
  r \indom M ->
  app Pervasives_ml.infix_colon_eq__ [r v]
    PRE (Group Ref M)
    POST (# Group Ref (M[r:=v])).
Proof using.
  intros. rewrite~ (Group_rem r M). xapp. intros tt.
  hchanges~ (Group_add' r M).
Qed.

Lemma fst_spec : forall A B (x:A) (y:B),
  app fst [(x,y)]
    PRE \[]
    POST \[= x].
Proof using. xcf_go~. Qed.

Lemma snd_spec : forall A B (x:A) (y:B),
  app snd [(x,y)]
    PRE \[]
    POST \[= y].
Proof using. xcf_go~. Qed.

Hint Extern 1 (RegisterSpec fst) => Provide fst_spec.
Hint Extern 1 (RegisterSpec snd) => Provide snd_spec.

Lemma ignore_spec :
  app ignore [tt]
    PRE \[]
    POST \[= tt].
Proof using. xcf_go~. Qed.

Hint Extern 1 (RegisterSpec ignore) => Provide ignore_spec.