dexter_util.v
Require Import String.
Require Import Michocoq.macros.
Import syntax.
Import comparable.
Require Import semantics.
Require Import NArith.
Require Import ZArith.
Require Import util.
Import error.
Require List.
Require Import Coq.micromega.Lia.
(*! Logic !*)
Lemma negb_is_true:
forall b : Datatypes.bool, negb b = true <-> ~ is_true b.
Proof.
intros. destruct b.
- intuition. elimtype False. apply H. reflexivity.
- simpl. split; intuition.
Qed.
Lemma bool_false_not b : b = false <-> ~ b.
Proof.
rewrite (iff_sym (Bool.not_true_iff_false _)).
destruct b; simpl; split; auto.
Qed.
Lemma bool_reflect_iff :
forall b1 b2 P Q,
(b1 = true <-> P) ->
(b2 = true <-> Q) ->
(P <-> Q) <-> (b1 = b2).
Proof.
intros b1 b2 P Q H H0.
split; intros Hiff; destruct b1, b2; intuition.
Qed.
Lemma some_equal_inv :
forall A (x y : A),
Some x = Some y <->
y = x.
intuition (f_equal; congruence).
Qed.
Lemma and_both_0_inv { P R S Q } :
Q <-> S -> P <-> R -> P /\ Q <-> R /\ S.
intuition.
Qed.
(* Shim for pair_equal_spec which is not in Coq 8.08 *)
Lemma shim_pair_equal_spec (A B : Type) (a1 a2 : A) (b1 b2 : B) :
(a1, b1) = (a2, b2) <-> a1 = a2 /\ b1 = b2.
Proof with auto.
split; intro H.
- split.
+ replace a1 with (fst (a1, b1)); replace a2 with (fst (a2, b2))...
rewrite H...
+ replace b1 with (snd (a1, b1)); replace b2 with (snd (a2, b2))...
rewrite H...
- destruct H; subst...
Qed.
Lemma iff_both_false :
forall A B : Prop,
(A -> False) ->
(B -> False) ->
A <-> B.
Proof.
(* this works in intuition, but not in Coq 8.11.2 *)
intros A B Ha Hb.
split; intro Hp; exfalso; intuition.
Qed.
(* rename ex_match_error *)
Lemma ex_match :
forall A (m : M A) P,
match m with
| Failed _ _ => False
| Return x => P x
end <-> (exists x, m = Return x /\ P x).
Proof.
intros A m P.
destruct m.
- apply iff_both_false; intuition.
destruct H as [ x [H1 H2] ].
discriminate.
- intuition.
+ exists a. intuition.
+ destruct H as [ x [H1 H2] ]. congruence.
Qed.
(* rename ex_match_option *)
Lemma some_match :
forall A (m : Datatypes.option A) P,
match m with
| None => False
| Some x => P x
end <-> (exists x, m = Some x /\ P x).
intros A m P.
destruct m.
- intuition.
+ exists a. intuition.
+ destruct H as [ x [H1 H2] ]. congruence.
- apply iff_both_false; intuition.
destruct H as [ x [H1 H2] ].
discriminate.
Qed.
(*! compare !*)
Lemma compare_eq_comm : forall t a b,
compare t a b = Eq <-> compare t b a = Eq.
Proof.
intros t a b.
transitivity (a = b).
apply compare_eq_iff.
transitivity (b = a). intuition.
symmetry. apply compare_eq_iff.
Qed.
Lemma compare_antisym :
(forall t a b, compare t a b = CompOpp (compare t b a)).
Proof.
intros t a b.
destruct (compare t a b) eqn:Hcomp; simpl.
- apply compare_eq_comm in Hcomp. now rewrite Hcomp.
- destruct (compare t b a) eqn:Hcomp'; try reflexivity.
+ assert (a <> b). apply compare_diff. intuition.
apply compare_eq_iff in Hcomp'. congruence.
+ apply compare_gt_lt in Hcomp'. congruence.
- destruct (compare t b a) eqn:Hcomp'; try reflexivity.
+ assert (a <> b). apply compare_diff. intuition.
apply compare_eq_iff in Hcomp'. congruence.
+ apply compare_gt_lt in Hcomp'. congruence.
Qed.
Lemma compare_int_compare_spec :
forall a b, CompareSpec (a = b) (a < b)%Z (b < a)%Z (compare int a b).
Proof. apply Z.compare_spec. Qed.
Lemma compare_nat_compare_spec :
forall a b, CompareSpec (a = b) (a < b)%N (b < a)%N (compare nat a b).
Proof. apply N.compare_spec. Qed.
Inductive CompareReflection (Peq Plt Pgt : Prop) (c : comparison) : Prop :=
test : (c = Eq <-> Peq) ->
(c = Lt <-> Plt) ->
(c = Gt <-> Pgt) ->
CompareReflection Peq Plt Pgt c.
Lemma compare_spec_reflection :
forall (t : comparable_type)
(a b : comparable_data t)
(rlt : comparable_data t -> comparable_data t -> Prop),
(forall {x y}, rlt x y -> rlt y x -> False) ->
CompSpec eq rlt a b (compare t a b) ->
CompareReflection (eq a b) (rlt a b) (rlt b a) (compare t a b).
Proof.
intros t a b rlt Hirr Hcompspec.
specialize (Hirr a b).
split.
- split.
+ intro Hcompare.
rewrite Hcompare in Hcompspec.
now inversion Hcompspec.
+ now rewrite compare_eq_iff.
- split.
+ intro Hcompare.
rewrite Hcompare in Hcompspec.
now inversion Hcompspec.
+ intro Hineq.
destruct (compare t a b) eqn:Hcomp; inversion Hcompspec; subst; intuition; try now exfalso.
- split.
+ intro Hcompare.
rewrite Hcompare in Hcompspec.
now inversion Hcompspec.
+ intro Hineq.
destruct (compare t a b) eqn:Hcomp; inversion Hcompspec; subst; intuition; try now exfalso.
Qed.
Definition compare_reflection_nat (n1 n2 : N) :
CompareReflection (n1 = n2) (n1 < n2)%N (n2 < n1)%N (compare nat n1 n2)
:= compare_spec_reflection nat n1 n2 N.lt N.lt_asymm (N.compare_spec n1 n2).
Definition compare_reflection_int (n1 n2 : Z) :
CompareReflection (n1 = n2) (n1 < n2)%Z (n2 < n1)%Z (compare int n1 n2)
:= compare_spec_reflection int n1 n2 Z.lt Z.lt_asymm (Z.compare_spec n1 n2).
Definition mutez_compare_spec :
forall (n1 n2 : tez.mutez),
CompareSpec (n1 = n2)
(tez.to_Z n1 < tez.to_Z n2)%Z
(tez.to_Z n2 < tez.to_Z n1)%Z
(compare mutez n1 n2).
Proof.
intros n1 n2.
assert
(CompareSpec (tez.to_Z n1 = tez.to_Z n2)
(tez.to_Z n1 < tez.to_Z n2)%Z
(tez.to_Z n2 < tez.to_Z n1)%Z
(compare mutez n1 n2))
by apply Z.compare_spec.
destruct (compare mutez n1 n2); inversion H; constructor; try assumption.
now apply tez.to_Z_inj.
Qed.
Definition compare_reflection_mutez (n1 n2 : tez.mutez) :
CompareReflection (n1 = n2)
(tez.to_Z n1 < tez.to_Z n2)%Z
(tez.to_Z n2 < tez.to_Z n1)%Z
(compare mutez n1 n2).
Proof.
apply (compare_spec_reflection mutez
n1
n2
(fun n1 n2 => (tez.to_Z n1 < tez.to_Z n2)%Z)).
- intros x y.
apply Z.lt_asymm.
- apply mutez_compare_spec.
Qed.
Lemma compare_nat_lt : forall (n1 n2 : N), compare nat n1 n2 = Lt <-> (n1 < n2)%N.
Proof. intros n1 n2.
pose proof (N.compare_spec n1 n2).
inversion H; intuition. Qed.
Lemma compare_nat_gt : forall (n1 n2 : N), compare nat n1 n2 = Gt <-> (n1 > n2)%N.
Proof. intros n1 n2.
pose proof (N.compare_spec n1 n2).
inversion H; intuition. Qed.
Lemma compare_int_lt : forall (n1 n2 : Z), compare int n1 n2 = Lt <-> (n1 < n2)%Z.
Proof. intros n1 n2.
pose proof (Z.compare_spec n1 n2).
inversion H; intuition. Qed.
Lemma compare_int_gt : forall (n1 n2 : Z), compare int n1 n2 = Gt <-> (n1 > n2)%Z.
Proof. intros n1 n2.
pose proof (Z.compare_spec n1 n2).
inversion H; intuition. Qed.
Lemma compare_mutez_lt : forall (n1 n2 : tez.mutez), compare mutez n1 n2 = Lt <-> (tez.to_Z n1 < tez.to_Z n2)%Z.
Proof. intros n1 n2.
pose proof (mutez_compare_spec n1 n2).
inversion H; intuition.
Qed.
Lemma compare_mutez_gt : forall (n1 n2 : tez.mutez), compare mutez n1 n2 = Gt <-> (tez.to_Z n1 > tez.to_Z n2)%Z.
Proof.
intros n1 n2.
pose proof (mutez_compare_spec n1 n2).
inversion H; intuition.
Qed.
(*! comparison_to_int !*)
Lemma comp_to_int_Eq c : (comparison_to_int c =? 0)%Z = true <-> c = Eq.
Proof.
destruct c; simpl; split; auto; discriminate.
Qed.
Lemma comp_to_int_Lt c : (comparison_to_int c <? 0)%Z = true <-> c = Lt.
Proof.
destruct c; simpl; split; auto; discriminate.
Qed.
Lemma comp_to_int_Gt c : (comparison_to_int c >? 0)%Z = true <-> c = Gt.
Proof.
destruct c; simpl; split; auto; discriminate.
Qed.
Lemma comparison_to_int_N_compare_le x y : (comparison_to_int (x ?= y)%N >=? 0)%Z = true <-> (x >= y)%N.
Proof.
unfold N.ge; destruct (x ?= y)%N; simpl; unfold Z.geb; simpl; split; auto.
2: discriminate.
all: intros _ H; discriminate.
Qed.
Lemma comparison_to_int_Z_compare_ltb:
forall z1 z2 : Z, (comparison_to_int (z1 ?= z2) <? 0)%Z = (z1 <? z2)%Z.
Proof.
intros z1 z2.
destruct (Z.compare_spec z1 z2); simpl.
- rewrite H.
now repeat rewrite Z.ltb_irrefl.
- apply Z.ltb_lt in H.
rewrite H.
reflexivity.
- apply Z.lt_asymm in H.
apply Z.ltb_nlt in H.
rewrite H.
reflexivity.
Qed.
Lemma comparison_to_int_pos :
forall n,
(comparison_to_int
match n with
| 0%N => Eq
| N.pos _ => Lt
end <? 0)%Z = true <-> (n > 0)%N.
Proof.
intro n. destruct n. simpl. cbv. intuition congruence.
simpl. intuition. lia.
Qed.
Lemma comparison_to_int_N_opp:
forall (n1 n2 : N),
(comparison_to_int (n2 ?= n1)%N >=? 0)%Z =
(comparison_to_int (n1 ?= n2)%N <=? 0)%Z.
Proof.
intros n1 n2.
rewrite N.compare_antisym.
destruct (n1 ?= n2)%N; simpl; tauto.
Qed.
(*! comparison_to_int compare !*)
Lemma comparison_to_int_compare_gt_lt:
forall (t : comparable_type) (a b : comparable_data t),
(comparison_to_int (compare t a b) <? 0)%Z = true <->
(comparison_to_int (compare t b a) >? 0)%Z = true.
Proof.
intros t a b.
rewrite comp_to_int_Lt, comp_to_int_Gt.
apply compare_gt_lt.
Qed.
Lemma comparison_to_int_compare_lt :
forall (t : comparable_type)
(a b : comparable_data t)
(rlt : comparable_data t -> comparable_data t -> Prop),
CompareReflection (eq a b) (rlt a b) (rlt b a) (compare t a b) ->
(comparison_to_int (compare t a b) <? 0)%Z = true <-> (rlt a b)%Z.
Proof.
intros t a b rlt H.
rewrite comp_to_int_Lt.
apply H.
Qed.
Lemma comparison_to_int_compare_gt :
forall (t : comparable_type)
(a b : comparable_data t)
(rlt : comparable_data t -> comparable_data t -> Prop),
CompareReflection (eq a b) (rlt a b) (rlt b a) (compare t a b) ->
(comparison_to_int (compare t a b) >? 0)%Z = true <-> (rlt b a)%Z.
Proof.
intros t a b rlt H.
rewrite comp_to_int_Gt.
apply H.
Qed.
Lemma comparison_to_int_compare_ge :
forall (t : comparable_type)
(a b : comparable_data t),
(comparison_to_int (compare t a b) >=? 0)%Z = true <-> (compare t a b) <> Lt.
Proof.
intros t a b. destruct (compare t a b); simpl; cbv; intuition discriminate.
Qed.
Lemma comparison_to_int_compare_le :
forall (t : comparable_type)
(a b : comparable_data t),
(comparison_to_int (compare t a b) <=? 0)%Z = true <-> (compare t a b) <> Gt.
Proof.
intros t a b. destruct (compare t a b); simpl; cbv; intuition discriminate.
Qed.
Lemma comparison_to_int_compare_int_lt :
forall (z1 z2 : Z),
(comparison_to_int (compare int z1 z2) <? 0)%Z = true <-> (z1 < z2)%Z.
Proof. intros z1 z2.
apply (comparison_to_int_compare_lt int _ _ _ (compare_reflection_int _ _)).
Qed.
Lemma comparison_to_int_compare_int_gt :
forall (z1 z2 : Z),
(comparison_to_int (compare int z1 z2) >? 0)%Z = true <-> (z1 > z2)%Z.
Proof. intros z1 z2.
rewrite Z.gt_lt_iff.
apply (comparison_to_int_compare_gt int _ _ _ (compare_reflection_int _ _)).
Qed.
Lemma comparison_to_int_compare_int_ge :
forall (z1 z2 : Z),
(comparison_to_int (compare int z1 z2) >=? 0)%Z = true <-> (z1 >= z2)%Z.
Proof. intros z1 z2. apply (comparison_to_int_compare_ge int z1 z2). Qed.
Lemma comparison_to_int_compare_int_le :
forall (z1 z2 : Z),
(comparison_to_int (compare int z1 z2) <=? 0)%Z = true <-> (z1 <= z2)%Z.
Proof. intros z1 z2. apply (comparison_to_int_compare_le int z1 z2). Qed.
Lemma comparison_to_int_compare_nat_lt :
forall (z1 z2 : N),
(comparison_to_int (compare nat z1 z2) <? 0)%Z = true <-> (z1 < z2)%N.
Proof. intros z1 z2.
apply (comparison_to_int_compare_lt nat _ _ _ (compare_reflection_nat _ _)).
Qed.
Lemma comparison_to_int_compare_nat_gt :
forall (z1 z2 : N),
(comparison_to_int (compare nat z1 z2) >? 0)%Z = true <-> (z1 > z2)%N.
Proof. intros z1 z2.
rewrite N.gt_lt_iff.
apply (comparison_to_int_compare_gt nat _ _ _ (compare_reflection_nat _ _)).
Qed.
Lemma comparison_to_int_compare_nat_ge :
forall (z1 z2 : N),
(comparison_to_int (compare nat z1 z2) >=? 0)%Z = true <-> (z1 >= z2)%N.
Proof. intros z1 z2. apply (comparison_to_int_compare_ge nat z1 z2). Qed.
Lemma comparison_to_int_compare_nat_le :
forall (z1 z2 : N),
(comparison_to_int (compare nat z1 z2) <=? 0)%Z = true <-> (z1 <= z2)%N.
Proof. intros z1 z2. apply (comparison_to_int_compare_le nat z1 z2). Qed.
Definition mutez_lt n1 n2 := (tez.to_Z n1 < tez.to_Z n2)%Z.
Lemma comparison_to_int_compare_mutez_lt :
forall (z1 z2 : tez.mutez),
(comparison_to_int (compare mutez z1 z2) <? 0)%Z = true <-> (tez.to_Z z1 < tez.to_Z z2)%Z.
Proof. intros z1 z2.
apply (comparison_to_int_compare_lt mutez z1 z2 mutez_lt (compare_reflection_mutez _ _)).
Qed.
Lemma comparison_to_int_compare_mutez_gt :
forall (z1 z2 : tez.mutez),
(comparison_to_int (compare mutez z1 z2) >? 0)%Z = true <-> (tez.to_Z z1 > tez.to_Z z2)%Z.
Proof. intros z1 z2.
rewrite Z.gt_lt_iff.
apply (comparison_to_int_compare_gt mutez z1 z2 mutez_lt (compare_reflection_mutez _ _)).
Qed.
Lemma comparison_to_int_compare_mutez_ge :
forall (z1 z2 : tez.mutez),
(comparison_to_int (compare mutez z1 z2) >=? 0)%Z = true <-> (tez.to_Z z1 >= tez.to_Z z2)%Z.
Proof. intros z1 z2. apply (comparison_to_int_compare_ge mutez z1 z2). Qed.
Lemma comparison_to_int_compare_mutez_le :
forall (z1 z2 : tez.mutez),
(comparison_to_int (compare mutez z1 z2) <=? 0)%Z = true <-> (tez.to_Z z1 <= tez.to_Z z2)%Z.
Proof. intros z1 z2. apply (comparison_to_int_compare_le mutez z1 z2). Qed.
Lemma comparison_to_int_compare_int_geb :
forall (z1 z2 : Z),
(comparison_to_int (compare int z1 z2) >=? 0)%Z = (z1 >=? z2)%Z.
Proof.
intros z1 z2.
apply (bool_reflect_iff _ _ (z1 >= z2)%Z (z1 >= z2)%Z).
apply comparison_to_int_compare_int_ge.
rewrite Z.geb_le.
rewrite Z.ge_le_iff.
reflexivity.
reflexivity.
Qed.
Lemma comparison_to_int_eq_comm : forall t a b,
(comparison_to_int (compare t a b) =? 0)%Z =
(comparison_to_int (compare t b a) =? 0)%Z.
Proof.
intros t a b.
rewrite compare_antisym.
destruct (compare t b a); reflexivity.
Qed.
(* todo: change tez.compare to compare? *)
Lemma tez_to_Z_bij :
forall t1 t2 : tez.mutez, tez.to_Z t1 = tez.to_Z t2 <-> t1 = t2.
Proof.
split. apply tez.to_Z_inj. intro. now f_equal.
Qed.
Lemma comparison_to_int_tez_compare_lt_zero:
forall t,
(comparison_to_int (tez.compare (0 ~Mutez) t) <? 0)%Z = true <->
(t <> (0 ~Mutez)).
Proof.
intros t.
change tez.compare with (compare mutez).
rewrite comparison_to_int_compare_mutez_lt.
rewrite <- tez_to_Z_bij.
split.
- intro Hineq.
apply Z.lt_neq in Hineq. congruence.
- intro Hineq.
destruct (Zle_lt_or_eq _ _ (tez.to_Z_lower_bound t)) as [Hlt | Heq].
+ apply Hlt.
+ change 0%Z with (tez.to_Z (0 ~Mutez)) in Heq.
congruence.
Qed.
Lemma comparison_to_int_tez_compare_mutez_to_nat :
forall t1 t2,
(comparison_to_int (compare mutez t1 t2) <=? 0)%Z = true <->
((Z.to_N (tez.to_Z t1)) <= (Z.to_N (tez.to_Z t2)))%N.
Proof.
intros t t'.
rewrite comparison_to_int_compare_mutez_le.
rewrite Z2N.inj_le; try apply tez.to_Z_lower_bound.
reflexivity.
Qed.
(*! ediv_N !*)
Lemma ediv_spec a b d r :
ediv_N a b = Some (d, r) <-> (d = (a / b)%N /\ r = (a mod b)%N) /\ (0 < b)%N.
Proof.
unfold ediv_N; destruct b; simpl; split.
- discriminate.
- lia.
- intro H; injection H; intros Hr Hd; rewrite Hr, Hd; unfold N.lt; simpl; auto.
- intros [[Hd Hr] _]; rewrite Hd, Hr; auto.
Qed.
Lemma ediv_N_some_iff :
forall (x y : N) Q,
y <> 0%N /\ Q ((x / y)%N, (x mod y)%N) <->
(exists z, ediv_N x y = Some z /\ Q z).
Proof.
intros.
split.
- intros [H1 H2].
exists ((x / y)%N, (x mod y)%N).
split.
apply ediv_spec. intuition lia.
assumption.
- unfold ediv_N.
intros [z [Hdiv Hq]].
rewrite <- N.eqb_eq. rewrite <- bool_not_false.
destruct (y =? 0)%N.
+ discriminate.
+ intuition congruence.
Qed.
Lemma Z_mod_to_N_mod :
forall x y, (Z.of_N (x mod y) =? 0)%Z = true <-> (x mod y)%N = 0%N.
intros x y.
destruct (_ =? _)%Z eqn:Heq.
rewrite Z.eqb_eq in Heq.
rewrite <- N2Z.inj_iff.
now intuition.
intuition. inversion H.
rewrite <- Heq. rewrite H. reflexivity.
Qed.
(*! About tez !*)
Lemma mutez_to_nat :
forall t,
match tez.of_Z (Z.of_N (Z.to_N (tez.to_Z t mod tez.to_Z (1 ~Mutez)))) with
| Failed _ _ => None
| Return rem => Some (Z.to_N (tez.to_Z t / tez.to_Z (1 ~Mutez)), rem)
end = Some (Z.to_N (tez.to_Z t), (0 ~Mutez)).
Proof. intro t. now rewrite Z.mod_1_r, Z.div_1_r. Qed.
Lemma tez_neq_zero_iff_gt_zero t :
t <> (0 ~Mutez) <-> (0 < Z.to_N (tez.to_Z t))%N.
Proof.
change 0%N with (Z.to_N (tez.to_Z (0 ~Mutez))).
rewrite <- tez_to_Z_bij.
rewrite <- Z2N.inj_iff by apply tez.to_Z_lower_bound.
split; simpl; intro H; lia.
Qed.
(*! About N !*)
Lemma nat_neq_zero_iff_gt_zero:
forall m : N,
(m <> 0 <-> 0 < m)%N.
Proof.
(* solved directly by lia in later versions of coq. *)
destruct m; lia.
Qed.
(*! About Z !*)
Lemma match_z_eq :
forall (z : Z),
(match z with
| 0 => 0
| Z.pos y' => Z.pos y'
| Z.neg y' => Z.neg y'
end)%Z = z.
Proof. destruct z; reflexivity. Qed.
Lemma Z_abs_N_sub :
forall (n1 n2 : N),
(0 <= Z.of_N n1 - Z.of_N n2)%Z ->
Z.abs_N (Z.of_N n1 - Z.of_N n2)%Z =
(n1 - n2)%N.
Proof.
intros n1 n2 H.
rewrite Zabs2N.inj_sub.
now do 2 rewrite Zabs2N.id.
lia.
Qed.
(** todo *)
Lemma cmp_nat_lt_zero n :
(comparison_to_int (compare nat 0 n)%N <? 0)%Z = true <->
(n <> 0)%N.
Proof.
rewrite comparison_to_int_compare_nat_lt.
symmetry.
apply nat_neq_zero_iff_gt_zero.
Qed.
(** TODO: could just use comparison_to_int_compare_gt_lt instead *)
Lemma cmp_mutez_gt_lt t :
(comparison_to_int (tez.compare t (0 ~Mutez)) >? 0)%Z = true <->
(comparison_to_int (tez.compare (0 ~Mutez) t) <? 0)%Z = true.
Proof.
change tez.compare with (compare mutez). symmetry.
apply comparison_to_int_compare_gt_lt.
Qed.
Lemma tez_fact_l:
forall (min_x : tez.mutez)
(x' : N)
(x : tez.mutez),
tez.to_Z x = Z.of_N x' ->
(Z.to_N (tez.to_Z min_x) <= Z.to_N (tez.to_Z x))%N ->
(x' >= Z.to_N (tez.to_Z min_x))%N.
Proof.
intros min_x x' x H.
intuition; rewrite H in *; rewrite N2Z.id in *; lia.
Qed.
Lemma tez_fact_r:
forall (min_x : tez.mutez)
(x' : N)
(x : tez.mutez),
tez.to_Z x = Z.of_N x' ->
(x' >= Z.to_N (tez.to_Z min_x))%N ->
(Z.to_N (tez.to_Z min_x) <= Z.to_N (tez.to_Z x))%N.
Proof.
intros min_x x' x H.
intuition; rewrite H in *; rewrite N2Z.id in *; lia.
Qed.
(* Not sure where to put this *)
Definition get_amount_bought_rem x y z
:= ((x * 997 * z) mod (y * 1000 + x * 997))%N.