Commit cb25928e authored by Michael Sammler's avatar Michael Sammler
Browse files

Upstreaming a small collection of lemmas

parent f370d2fe
Pipeline #57862 passed with stage
in 4 minutes and 42 seconds
......@@ -3,6 +3,18 @@ API-breaking change is listed.
## std++ master
- Rename `Is_true_false``Is_true_false_2` and `eq_None_ne_Some``eq_None_ne_Some_1`.
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
Note that the script is not idempotent, do not run it twice.
```
sed -i -E -f- $(find theories -name "*.v") <<EOF
s/\bIs_true_false\b/Is_true_false_2/g
s/\beq_None_ne_Some\b/eq_None_ne_Some_1/g
EOF
```
## std++ 1.6.0 (2021-11-05)
Coq 8.14 is newly supported by this release, and Coq 8.10 to 8.13 remain
......
......@@ -642,8 +642,18 @@ Lemma orb_True b1 b2 : b1 || b2 ↔ b1 ∨ b2.
Proof. destruct b1, b2; simpl; tauto. Qed.
Lemma negb_True b : negb b ¬b.
Proof. destruct b; simpl; tauto. Qed.
Lemma Is_true_false (b : bool) : b = false ¬b.
Proof. now intros -> ?. Qed.
Lemma Is_true_true (b : bool) : b b = true.
Proof. now destruct b. Qed.
Lemma Is_true_true_1 (b : bool) : b b = true.
Proof. apply Is_true_true. Qed.
Lemma Is_true_true_2 (b : bool) : b = true b.
Proof. apply Is_true_true. Qed.
Lemma Is_true_false (b : bool) : ¬ b b = false.
Proof. now destruct b; simpl. Qed.
Lemma Is_true_false_1 (b : bool) : ¬b b = false.
Proof. apply Is_true_false. Qed.
Lemma Is_true_false_2 (b : bool) : b = false ¬b.
Proof. apply Is_true_false. Qed.
(** ** Unit *)
Global Instance unit_equiv : Equiv unit := λ _ _, True.
......
......@@ -535,6 +535,13 @@ Proof.
- etrans; [|apply Z.pow_pos_nonneg]; lia.
Qed.
Lemma Z_add_nocarry_lor a b :
Z.land a b = 0
a + b = Z.lor a b.
Proof. intros ?. rewrite <-Z.lxor_lor by done. by rewrite Z.add_nocarry_lxor. Qed.
Lemma Z_opp_lnot a : -a - 1 = Z.lnot a.
Proof. pose proof (Z.add_lnot_diag a). lia. Qed.
Local Close Scope Z_scope.
......
......@@ -13,8 +13,12 @@ Lemma None_ne_Some {A} (x : A) : None ≠ Some x.
Proof. congruence. Qed.
Lemma Some_ne_None {A} (x : A) : Some x None.
Proof. congruence. Qed.
Lemma eq_None_ne_Some {A} (mx : option A) x : mx = None mx Some x.
Proof. congruence. Qed.
Lemma eq_None_ne_Some {A} (mx : option A) : ( x, mx Some x) mx = None.
Proof. destruct mx; split; congruence. Qed.
Lemma eq_None_ne_Some_1 {A} (mx : option A) x : mx = None mx Some x.
Proof. intros ?. by apply eq_None_ne_Some. Qed.
Lemma eq_None_ne_Some_2 {A} (mx : option A) : ( x, mx Some x) mx = None.
Proof. intros ?. by apply eq_None_ne_Some. Qed.
Global Instance Some_inj {A} : Inj (=) (=) (@Some A).
Proof. congruence. Qed.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment