Library CFML.CFLibCredits

Require Export CFLib.

Implicit Types x y z : int.

Additional lemmas on credits

Lemma credits_eq : forall x y,
  x = y ->
  \$ x = \$ y.
Proof. apply (args_eq_1 heap_is_credits). Qed.

Lemma credits_int_zero_eq_prove : forall (x:int),
  x = 0 -> \$ x = \[].
Proof. intros. subst. apply credits_zero_eq. Qed.

Tactic simpl_ineq

simpl_ineq simplifies inequalities of the form: a1 + a2 - a3 + a4 <= b1 + b2 - b3 or (with >=), by cancelling out identical terms on both sides

Section SimplIneq.

Lemma ineq_le_refl : forall x,
  x <= x.
Proof using. intros. math. Qed.

Lemma ineq_add_assoc : forall x y z,
  x + (y + z ) = (x + y ) + z.
Proof using. intros. math. Qed.

Lemma ineq_le_to_ge : forall x y,
  x <= y ->
  y >= x.
Proof using. intros. math. Qed.

Lemma ineq_ge_to_le : forall x y,
  x >= y ->
  y <= x.
Proof using. intros. math. Qed.

Lemma ineq_sub_to_add : forall x y,
  x - y = x + (-y ).
Proof using. intros. math. Qed.

Lemma ineq_remove_zero_r : forall x,
  x + 0 = x.
Proof using. intros. math. Qed.

Lemma ineq_remove_zero_l : forall x,
  0 + x = x.
Proof using. intros. math. Qed.

Lemma simpl_ineq_start_1 : forall x1 y,
  0 + x1 <= y ->
  x1 <= y.
Proof using. intros. math. Qed.

Lemma simpl_ineq_start_2 : forall x1 x2 y,
  0 + x1 + x2 <= y ->
  x1 + x2 <= y.
Proof using. intros. math. Qed.

Lemma simpl_ineq_start_3 : forall x1 x2 x3 y,
  0 + x1 + x2 + x3 <= y ->
  x1 + x2 + x3 <= y.
Proof using. intros. math. Qed.

Lemma simpl_ineq_start_4 : forall x1 x2 x3 x4 y,
  0 + x1 + x2 + x3 + x4 <= y ->
  x1 + x2 + x3 + x4 <= y.
Proof using. intros. math. Qed.

Lemma simpl_ineq_zero_r1 : forall x y1,
  x <= y1 + 0 ->
  x <= y1.
Proof using. intros. math. Qed.

Lemma simpl_ineq_zero_r2 : forall x y1 y2,
  x <= 0 + y1 + y2 ->
  x <= y1 + y2.
Proof using. intros. math. Qed.

Lemma simpl_ineq_next : forall x y1 y2 y3,
  x <= y1 + (y2 + y3 ) ->
  x <= (y1 + y2 ) + y3.
Proof using. intros. math. Qed.

Lemma simpl_ineq_zero : forall x y1 y3,
  x <= y1 + y3 ->
  x <= (y1 + 0) + y3.
Proof using. intros. math. Qed.

Lemma simpl_ineq_cancel_00 : forall y1 y2 y3,
  0 <= y1 + y3 ->
  y2 <= y1 + y2 + y3.
Proof using. intros. math. Qed.

Lemma simpl_ineq_cancel_0 : forall x1 y1 y2 y3,
  x1 <= y1 + y3 ->
  y2 + x1 <= y1 + y2 + y3.
Proof using. intros. math. Qed.

Lemma simpl_ineq_cancel_1 : forall x0 y1 y2 y3,
  x0 <= y1 + y3 ->
  x0 + y2 <= y1 + y2 + y3.
Proof using. intros. math. Qed.

Lemma simpl_ineq_cancel_2 : forall x0 x1 y1 y2 y3,
  x0 + x1 <= y1 + y3 ->
  x0 + y2 + x1 <= y1 + y2 + y3.
Proof using. intros. math. Qed.

Lemma simpl_ineq_cancel_3 : forall x0 x1 x2 y1 y2 y3,
  x0 + x1 + x2 <= y1 + y3 ->
  x0 + y2 + x1 + x2 <= y1 + y2 + y3.
Proof using. intros. math. Qed.

Lemma simpl_ineq_cancel_4 : forall x0 x1 x2 x3 y1 y2 y3,
  x0 + x1 + x2 + x3 <= y1 + y3 ->
  x0 + y2 + x1 + x2 + x3 <= y1 + y2 + y3.
Proof using. intros. math. Qed.

Lemma int_le_mul_pos_l : forall x y z,
  z >= 0 ->
  x <= y ->
  z * x <= z * y.
Proof using. intros. applys~ Z.mul_le_mono_nonneg_l. Qed.

Lemma int_le_mul_pos_r : forall x y z,
  z >= 0 ->
  x <= y ->
  x * z <= y * z.
Proof using. intros. applys~ Z.mul_le_mono_nonneg_r. Qed.

End SimplIneq.

Hint Rewrite ineq_sub_to_add : ineq_sub_to_add_rew.
Hint Rewrite <- ineq_sub_to_add : ineq_add_to_sub_rew.

Ltac simpl_ineq_left_zero tt :=
  match goal with |- (?HL <= _)%I =>
  match HL with
  | (_ + _ + _ + _)%I => apply simpl_ineq_start_4
  | (_ + _ + _)%I => apply simpl_ineq_start_3
  | (_ + _)%I => apply simpl_ineq_start_2
  | _ => apply simpl_ineq_start_1
  end end.

Ltac simpl_ineq_setup tt :=
  try (match goal with |- (_ >= _)%I => apply ineq_le_to_ge end);
  autorewrite with ineq_sub_to_add_rew;
  try simpl_ineq_left_zero tt;
  apply simpl_ineq_zero_r1.

Hint Rewrite ineq_remove_zero_r ineq_remove_zero_l ineq_add_assoc
  : simpl_ineq_clean_rew.

Ltac simpl_ineq_cleanup tt :=
  autorewrite with simpl_ineq_clean_rew;
  autorewrite with ineq_add_to_sub_rew;
  try apply ineq_le_refl.

Ltac simpl_ineq_find_same Y VL :=
  match VL with
  | Y => apply simpl_ineq_cancel_0
  | (_ + Y)%I => apply simpl_ineq_cancel_1
  | (_ + Y + _)%I => apply simpl_ineq_cancel_2
  | (_ + Y + _ + _)%I => apply simpl_ineq_cancel_3
  | (_ + Y + _ + _ + _)%I => apply simpl_ineq_cancel_4
  end.

Ltac simpl_ineq_step tt :=
  match goal with |- (?VL <= ?VF + ?VR)%I =>
  match VF with
  | (_ + ?VA)%I =>
    match VA with
    | (0%I) => apply simpl_ineq_zero
    | ?Y => simpl_ineq_find_same Y VL
    | _ => apply simpl_ineq_next
    end
  | 0%I => fail 1
  | _ => apply simpl_ineq_zero_r2
  end end.

Ltac simpl_ineq_main tt :=
  simpl_ineq_setup tt;
  (repeat (simpl_ineq_step tt));
  simpl_ineq_cleanup tt.

Tactic Notation "simpl_ineq" := simpl_ineq_main tt.
Tactic Notation "simpl_ineq" "~" := simpl_ineq; auto_tilde.
Tactic Notation "simpl_ineq" "*" := simpl_ineq; auto_star.

Ltac simpl_ineq_mul_core :=
  try apply ineq_le_to_ge;
  repeat (first
    [ apply int_le_mul_pos_r
    | apply int_le_mul_pos_l ]).

Tactic Notation "simpl_ineq_mul" :=
  simpl_ineq_mul_core.

Lemma simpl_ineq_demo : forall (n:nat) (x y z : int),
  ((x + (n * x)%I)%I + y)%I >= ((x + z)%I + (n * x)%I)%I.
Proof.
  intros. dup.
  simpl_ineq_setup tt.
  simpl_ineq_step tt.
  simpl_ineq_step tt.
  simpl_ineq_step tt.
  simpl_ineq_step tt.
  simpl_ineq_cleanup tt.
  demo.
  simpl_ineq. demo.
Qed.

Tactic rew_ineq

rew_ineq H where H is of the form x <= y applies to a goal of the form a1 + x + a2 <= b and replaces it with a1 + y + a2 <= b. (works also with >= in the other direction; rew_ineq <- H also works)

Section RewIneq.

Lemma rew_ineq_l0 : forall x0 x0',
  x0 <= x0' -> forall y,
  x0' <= y ->
  x0 <= y.
Proof using. intros. math. Qed.

Lemma rew_ineq_l1f : forall x0 x0',
  x0 <= x0' -> forall x1 y,
  x0' + x1 <= y ->
  x0 + x1 <= y.
Proof using. intros. math. Qed.

Lemma rew_ineq_l2f : forall x0 x0',
  x0 <= x0' -> forall x1 x2 y,
  x0' + x1 + x2 <= y ->
  x0 + x1 + x2 <= y.
Proof using. intros. math. Qed.

Lemma rew_ineq_l3f : forall x0 x0',
  x0 <= x0' -> forall x1 x2 x3 y,
  x0' + x1 + x2 + x3 <= y ->
  x0 + x1 + x2 + x3 <= y.
Proof using. intros. math. Qed.

Lemma rew_ineq_l1 : forall x0 x0',
  x0 <= x0' -> forall x1 y,
  x1 + x0' <= y ->
  x1 + x0 <= y.
Proof using. intros. math. Qed.

Lemma rew_ineq_l2 : forall x0 x0',
  x0 <= x0' -> forall x1 x2 y,
  x1 + x0' + x2 <= y ->
  x1 + x0 + x2 <= y.
Proof using. intros. math. Qed.

Lemma rew_ineq_l3 : forall x0 x0',
  x0 <= x0' -> forall x1 x2 x3 y,
  x1 + x0' + x2 + x3 <= y ->
  x1 + x0 + x2 + x3 <= y.
Proof using. intros. math. Qed.

Lemma rew_ineq_r0 : forall x0 x0',
  x0 <= x0' -> forall y,
  y <= x0 ->
  y <= x0'.
Proof using. intros. math. Qed.

Lemma rew_ineq_r1f : forall x0 x0',
  x0 <= x0' -> forall x1 y,
  y <= x0 + x1 ->
  y <= x0' + x1.
Proof using. intros. math. Qed.

Lemma rew_ineq_r2f : forall x0 x0',
  x0 <= x0' -> forall x1 x2 y,
  y <= x0 + x1 + x2 ->
  y <= x0' + x1 + x2.
Proof using. intros. math. Qed.

Lemma rew_ineq_r3f : forall x0 x0',
  x0 <= x0' -> forall x1 x2 x3 y,
  y <= x0 + x1 + x2 + x3 ->
  y <= x0' + x1 + x2 + x3.
Proof using. intros. math. Qed.

Lemma rew_ineq_r1 : forall x0 x0',
  x0 <= x0' -> forall x1 y,
  y <= x1 + x0 ->
  y <= x1 + x0'.
Proof using. intros. math. Qed.

Lemma rew_ineq_r2 : forall x0 x0',
  x0 <= x0' -> forall x1 x2 y,
  y <= x1 + x0 + x2 ->
  y <= x1 + x0' + x2.
Proof using. intros. math. Qed.

Lemma rew_ineq_r3 : forall x0 x0',
  x0 <= x0' -> forall x1 x2 x3 y,
  y <= x1 + x0 + x2 + x3 ->
  y <= x1 + x0' + x2 + x3.
Proof using. intros. math. Qed.

End RewIneq.

Ltac ineq_ensure_goal_le tt :=
  try (match goal with |- (_ >= _)%I => apply ineq_le_to_ge end).

Ltac ineq_ensure_le H :=
  match type of H with
  | (_ >= _)%I => constr:(@ineq_ge_to_le _ _ H)
  | (_ <= _)%I => constr:(H)
  end.

Ltac rew_ineq_l H' :=
  ineq_ensure_goal_le tt;
  let H := ineq_ensure_le H' in
  first
  [ apply (@rew_ineq_l0 _ _ H)
  | apply (@rew_ineq_l1 _ _ H)
  | apply (@rew_ineq_l2 _ _ H)
  | apply (@rew_ineq_l3 _ _ H)
  | apply (@rew_ineq_l1f _ _ H)
  | apply (@rew_ineq_l2f _ _ H)
  | apply (@rew_ineq_l3f _ _ H)
  ].

Ltac rew_ineq_r H' :=
  ineq_ensure_goal_le tt;
  let H := ineq_ensure_le H' in
  first
  [ apply (@rew_ineq_r0 _ _ H)
  | apply (@rew_ineq_r1 _ _ H)
  | apply (@rew_ineq_r2 _ _ H)
  | apply (@rew_ineq_r3 _ _ H)
  | apply (@rew_ineq_r1f _ _ H)
  | apply (@rew_ineq_r2f _ _ H)
  | apply (@rew_ineq_r3f _ _ H)
  ].

Tactic Notation "rew_ineq" constr(H) :=
  rew_ineq_l H.
Tactic Notation "rew_ineq" "->" constr(H) :=
  rew_ineq_l H.
Tactic Notation "rew_ineq" "<-" constr(H) :=
  rew_ineq_r H.

Demos of tactics

Section Ineq_demos.

Lemma simpl_ineq_demo_1 : forall x1 x2 x3 x4 x5,
  x1 + x2 + x3 + x4 <= x2 + x3 + x5.
Proof.
  intros. dup.
  simpl_ineq_setup tt.
  simpl_ineq_step tt.
  simpl_ineq_step tt.
  simpl_ineq_step tt.
  simpl_ineq_step tt.
  try simpl_ineq_step tt.
  simpl_ineq_cleanup tt.
  skip.   simpl_ineq.
  demo.
Qed.

Lemma simpl_ineq_demo_2 : forall x1 x2 x3 x4 x5,
  0 + x2 + x4 - x1 - x2 /x3 + 0 + x5 >= x1 - x2 /x3 + x4.
Proof.
  intros. dup.
  simpl_ineq_setup tt.
  simpl_ineq_step tt.
  simpl_ineq_step tt.
  simpl_ineq_step tt.
  simpl_ineq_step tt.
  simpl_ineq_step tt.
  simpl_ineq_step tt.
  simpl_ineq_cleanup tt.
  skip.   simpl_ineq.
  demo.
Qed.

Lemma rew_ineq_demo : forall x1 x2 x3 x4 x5 x6 x7 x8,
  x1 <= x2 ->
  x3 <= x4 ->
  x5 + x1 + x6 <= x7 + x4 + x8.
Proof.
  introv H1 H2. rew_ineq H1. rew_ineq <- H2.
  demo.
Qed.

End Ineq_demos.

Nat into Z

Lemma int_mul_zero_l : forall x,
  (0 * x ) = 0.
Proof using. math. Qed.

Lemma int_mul_zero_r : forall x,
  (x * 0) = 0.
Proof using. math. Qed.

Lemma int_mul_one_l : forall x,
  (1 * x ) = x.
Proof using. math. Qed.

Lemma int_mul_one_r : forall x,
  (x * 1) = x.
Proof using. math. Qed.

Lemma int_mul_zero_nat_l : forall x,
  (0%nat * x ) = 0.
Proof using. math. Qed.

Lemma int_mul_zero_nat_r : forall x,
  (x * 0%nat) = 0.
Proof using. math. Qed.

Lemma int_mul_one_nat_l : forall x,
  (1%nat * x ) = x.
Proof using. math. Qed.

Lemma int_mul_one_nat_r : forall x,
  (x * 1%nat) = x.
Proof using. math. Qed.

Lemma int_add_nat : forall n m,
  (n +m)%nat = n + m :> int.
Proof using. math. Qed.

Lemma int_mul_succ_nat : forall (n:nat) x,
  (S n)%nat * x = x + n *x.
Proof using. intros. math_setup. ring. Qed.

Lemma int_mul_plus_one_nat : forall (n:nat) x,
  (1+n)%nat * x = x + n *x.
Proof using. intros. math_setup. ring. Qed.

Lemma int_mul_assoc : forall x y z,
  x * (y *z ) = x * y * z.
Proof using. intros. math_setup. ring. Qed.

Lemma int_add_assoc : forall x y z,
  x + (y +z ) = x + y + z.
Proof using. math. Qed.

Lemma int_mul_plus_one_l : forall n x,
  (1+n ) * x = x + n *x.
Proof using. intros. math_setup. ring. Qed.

Lemma int_mul_plus_one_r : forall n x,
  x * (1+n ) = x + x *n.
Proof using. intros. math_setup. ring. Qed.

Hint Rewrite int_mul_assoc int_add_assoc
  int_mul_zero_l int_mul_one_l int_mul_zero_nat_l int_mul_one_nat_l
  int_mul_zero_r int_mul_one_r int_mul_zero_nat_r int_mul_one_nat_r
  int_add_nat int_mul_succ_nat int_mul_plus_one_nat
  int_mul_plus_one_l int_mul_plus_one_r : rew_nat_to_int.

Tactic Notation "rew_nat_to_int" :=
  autorewrite with rew_nat_to_int.

Tactics simpl_credits

simpl_credits to simplify an expression or inequality involving credits

Ltac simpl_credits_core :=
  rew_nat_to_int;
  match goal with
  | |- (_ <= _)%I => try simpl_ineq
  | |- (_ >= _)%I => try simpl_ineq
  | |- (_ = _ :> int) => idtac
  end.

Tactic Notation "simpl_credits" :=
  simpl_credits_core.
Tactic Notation "simpl_credits" "~" :=
  simpl_credits; auto_tilde.
Tactic Notation "simpl_credits" "*" :=
  simpl_credits; auto_star.

Demo

Lemma simpl_credits_demo : forall (n:nat) (x y z : int),
(1+n)%nat * x + y >= x + z + n * x.
Proof. intros. simpl_credits. demo. Qed.

Tactic simpl_nonneg

simpl_nonneg simplifies inequalities of the form: e >= 0 or 0 <= e where e is an arithmetic expression whose components are all nonnegative.

Section SimplNonneg.

Lemma nonneg_nat : forall (n:nat),
  (0 <= n)%I.
Proof using. intros. math. Qed.

Lemma nonneg_add : forall x y,
  0 <= x ->
  0 <= y ->
  0 <= (x + y ).
Proof using. intros. math. Qed.

Lemma nonneg_mul : forall x y,
  0 <= x ->
  0 <= y ->
  0 <= (x * y ).
Proof using. introv H1 H2. lets: BinInt.Z.mul_nonneg_nonneg H1 H2. math. Qed.

End SimplNonneg.

Ltac simpl_nonneg_step tt :=
  match goal with |- ?G => match G with
  | ?x >= ?y => apply ineq_le_to_ge
  | (0 <= nat_to_Z ?n)%I => apply nonneg_nat
  | (0 <= Z.of_nat)%I => apply nonneg_nat
  | (0 <= ?x + ?y) => apply nonneg_add
  | (0 <= ?x * ?y) => apply nonneg_mul
  end end.

Ltac simpl_nonneg_repeat tt :=
  repeat (simpl_nonneg_step tt).

Hint Resolve nonneg_nat : simpl_nonneg.
Tactic Notation "simpl_nonneg" :=
  simpl_nonneg_repeat tt.

Tactic Notation "simpl_nonneg_auto" :=
  simpl_nonneg_repeat tt; auto with simpl_nonneg.

Tactic Notation "simpl_nonneg" "~" :=
  simpl_nonneg; xauto~.
Tactic Notation "simpl_nonneg" "*" :=
  simpl_nonneg; xauto*.

Hint Resolve nonneg_nat ineq_le_to_ge nonneg_add nonneg_mul : nonneg.

Tactic csimpl

csimpl combines hsimpl_credits and simpl_credits, and tries to solve goals using simpl_nonneg (for ?x >= 0) or math.

Ltac csimpl_core :=
  try hsimpl_credits; try simpl_credits;
  try solve [ simpl_nonneg | math ].

Tactic Notation "csimpl" :=
  csimpl_core.

Tactic ximpl_credits

Tactic Notation "xsimpl_credits" :=
  hsimpl_credits_core.
Tactic Notation "xsimpl_credits" "~" :=
  xsimpl_credits; auto_tilde.
Tactic Notation "xsimpl_credits" "*" :=
  xsimpl_credits; auto_star.