https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: b0c90bc030195f20f5e704eb8f944ca18350964e authored by nmm5055 on 23 April 2021, 01:50:42 UTC
Merge branch 'nmm5055-master-patch-57340' into 'master'
Merge branch 'nmm5055-master-patch-57340' into 'master'
Tip revision: b0c90bc
util.v
(* Open Source License *)
(* Copyright (c) 2019 Nomadic Labs. <contact@nomadic-labs.com> *)
(* Permission is hereby granted, free of charge, to any person obtaining a *)
(* copy of this software and associated documentation files (the "Software"), *)
(* to deal in the Software without restriction, including without limitation *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)
(* and/or sell copies of the Software, and to permit persons to whom the *)
(* Software is furnished to do so, subject to the following conditions: *)
(* The above copyright notice and this permission notice shall be included *)
(* in all copies or substantial portions of the Software. *)
(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR *)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER *)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)
(* DEALINGS IN THE SOFTWARE. *)
Require Import ZArith.
Require Import Michocoq.macros.
Import syntax.
Import comparable.
Require Import semantics.
Ltac more_fuel :=
match goal with
| Hfuel : (_ <= ?fuel) |- _ =>
destruct fuel as [|fuel];
[inversion Hfuel; fail
| apply le_S_n in Hfuel]
end.
Lemma forall_ex {A : Set} {phi psi : A -> Prop} :
(forall x, phi x <-> psi x) -> ((exists x, phi x) <-> (exists x, psi x)).
Proof.
intro Hall.
split; intros (x, Hx); exists x; specialize (Hall x); intuition.
Qed.
Lemma and_comm_3 {A B C} : A /\ (B /\ C) <-> B /\ (A /\ C).
Proof.
tauto.
Qed.
Lemma ex_and_comm {A : Set} {P : Prop} {Q : A -> Prop} :
P /\ (exists x, Q x) <-> (exists x, P /\ Q x).
Proof.
split.
- intros (p, (x, q)).
exists x.
auto.
- intros (x, (p, q)).
split.
+ auto.
+ exists x.
auto.
Qed.
Lemma ex_and_comm2 {A B : Set} {P : Prop} {Q : A -> B -> Prop} :
P /\ (exists x y, Q x y) <-> (exists x y, P /\ Q x y).
Proof.
rewrite ex_and_comm.
apply forall_ex; intro x.
apply ex_and_comm.
Qed.
Lemma and_both {P Q R : Prop} : (Q <-> R) -> (P /\ Q <-> P /\ R).
Proof.
intuition.
Qed.
Lemma ex_and_comm_both {A : Set} {P Q R}:
(Q <-> exists x : A, R x) ->
((P /\ Q) <-> exists x : A, P /\ R x).
Proof.
intro H.
transitivity (P /\ exists x, R x).
- apply and_both; assumption.
- apply ex_and_comm.
Qed.
Lemma ex_and_comm_both2 {A B : Set} {P Q R}:
(Q <-> exists (x : A) (y : B), R x y) ->
((P /\ Q) <-> exists x y, P /\ R x y).
Proof.
intro H.
transitivity (P /\ exists x y, R x y).
- apply and_both; assumption.
- apply ex_and_comm2.
Qed.
Lemma and_both_2 (P Q R : Prop):
(P -> (Q <-> R)) ->
((P /\ Q) <-> (P /\ R)).
Proof.
intuition.
Qed.
Lemma and_both_0 {P Q R S : Prop} : (P <-> R) -> (Q <-> S) -> (P /\ Q) <-> (R /\ S).
Proof.
intuition.
Qed.
Lemma and_left {P Q R : Prop} : P -> (Q <-> R) -> ((P /\ Q) <-> R).
Proof.
intuition.
Qed.
Lemma and_right {P Q R : Prop} : P -> (Q <-> R) -> (Q <-> (P /\ R)).
Proof.
intuition.
Qed.
Lemma eqb_eq a c1 c2 :
BinInt.Z.eqb (comparison_to_int (compare a c1 c2)) Z0 = true <->
c1 = c2.
Proof.
rewrite BinInt.Z.eqb_eq.
rewrite comparison_to_int_Eq.
apply comparable.compare_eq_iff.
Qed.
Lemma leb_le a c1 c2 :
BinInt.Z.leb (comparison_to_int (compare a c1 c2)) Z0 = true <->
(lt a c1 c2 \/ c1 = c2).
Proof.
case_eq (compare a c1 c2); intro Hleb.
- rewrite compare_eq_iff in Hleb.
simpl.
generalize (BinInt.Z.leb_refl Z0).
intuition.
- simpl.
rewrite BinInt.Z.leb_le.
generalize (BinInt.Pos2Z.neg_is_nonpos 1).
unfold lt.
intuition.
- simpl.
rewrite Zbool.Zone_pos.
unfold lt.
split.
+ discriminate.
+ rewrite <- compare_eq_iff.
intros [|]; congruence.
Qed.
Lemma leb_gt a c1 c2 :
BinInt.Z.leb (comparison_to_int (compare a c1 c2)) Z0 = false <->
(gt a c1 c2).
Proof.
unfold gt, gt_comp.
case_eq (compare a c1 c2); intro Hleb.
- simpl.
rewrite BinInt.Z.leb_refl.
split; discriminate.
- simpl.
assert (BinInt.Z.leb (Zneg 1) Z0 = true) as H.
+ rewrite BinInt.Z.leb_le.
apply (BinInt.Pos2Z.neg_is_nonpos 1).
+ rewrite H.
split; discriminate.
- simpl.
case_eq (BinInt.Z.leb (Zpos 1) Z0).
+ intro H.
rewrite BinInt.Z.leb_le in H.
apply Zorder.Zle_not_lt in H.
destruct (H BinInt.Z.lt_0_1).
+ intro; split; reflexivity.
Qed.
Lemma lt_is_leb a c1 c2 :
BinInt.Z.gtb (comparison_to_int (compare a c1 c2)) Z0 =
negb (BinInt.Z.leb (comparison_to_int (compare a c1 c2)) Z0).
Proof.
generalize (comparison_to_int (compare a c1 c2)).
intro z.
rewrite Z.gtb_ltb.
apply Z.ltb_antisym.
Qed.
Lemma if_false_is_and (b : Datatypes.bool) A : (if b then A else False) <-> (b = true /\ A).
Proof.
destruct b.
- apply and_right.
+ reflexivity.
+ intuition.
- split.
+ intro H; inversion H.
+ intros (H, _); inversion H.
Qed.
Lemma if_false_not (b : Datatypes.bool) A : (if b then False else A) <-> (b = false /\ A).
Proof.
destruct b.
- split.
+ intro H; inversion H.
+ intros (H, _); inversion H.
- apply and_right.
+ reflexivity.
+ intuition.
Qed.
Lemma eq_sym_iff {A : Type} (x y : A) : x = y <-> y = x.
Proof.
split; apply eq_sym.
Qed.