diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Floats/PrimFloat.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CarryType.v | 18 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/DoubleType.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/Int63.v | 88 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/PrimInt63.v | 82 | ||||
| -rw-r--r-- | theories/ssr/ssrbool.v | 114 |
6 files changed, 245 insertions, 67 deletions
diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v index ed7947aa63..4c818a7e52 100644 --- a/theories/Floats/PrimFloat.v +++ b/theories/Floats/PrimFloat.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Int63 FloatClass. +Require Import PrimInt63 FloatClass. (** * Definition of the interface for primitive floating-point arithmetic diff --git a/theories/Numbers/Cyclic/Abstract/CarryType.v b/theories/Numbers/Cyclic/Abstract/CarryType.v new file mode 100644 index 0000000000..a21a1c8022 --- /dev/null +++ b/theories/Numbers/Cyclic/Abstract/CarryType.v @@ -0,0 +1,18 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +Set Implicit Arguments. + +#[universes(template)] +Variant carry (A : Type) := +| C0 : A -> carry A +| C1 : A -> carry A. diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v index 165f9893ca..e399bcfc0f 100644 --- a/theories/Numbers/Cyclic/Abstract/DoubleType.v +++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v @@ -13,15 +13,15 @@ Set Implicit Arguments. Require Import BinInt. +Require Import CarryType. Local Open Scope Z_scope. Definition base digits := Z.pow 2 (Zpos digits). Arguments base digits: simpl never. -#[universes(template)] -Variant carry (A : Type) := -| C0 : A -> carry A -| C1 : A -> carry A. +Notation carry := carry (only parsing). +Notation C0 := C0 (only parsing). +Notation C1 := C1 (only parsing). Definition interp_carry {A} (sign:Z)(B:Z)(interp:A -> Z) c := match c with diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index dbca2f0947..c469a49903 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -17,55 +17,25 @@ Require Import Zpow_facts. Require Import Zgcd_alt. Require ZArith. Import Znumtheory. - -Register bool as kernel.ind_bool. -Register prod as kernel.ind_pair. -Register carry as kernel.ind_carry. -Register comparison as kernel.ind_cmp. +Require Export PrimInt63. Definition size := 63%nat. -Primitive int := #int63_type. -Register int as num.int63.type. -Declare Scope int63_scope. -Definition id_int : int -> int := fun x => x. -Declare ML Module "int63_syntax_plugin". - -Module Import Int63NotationsInternalA. -Delimit Scope int63_scope with int63. -Bind Scope int63_scope with int. -End Int63NotationsInternalA. - -(* Logical operations *) -Primitive lsl := #int63_lsl. - -Primitive lsr := #int63_lsr. - -Primitive land := #int63_land. - -Primitive lor := #int63_lor. - -Primitive lxor := #int63_lxor. - -(* Arithmetic modulo operations *) -Primitive add := #int63_add. - -Primitive sub := #int63_sub. - -Primitive mul := #int63_mul. - -Primitive mulc := #int63_mulc. - -Primitive div := #int63_div. - -Primitive mod := #int63_mod. - -(* Comparisons *) -Primitive eqb := #int63_eq. - -Primitive ltb := #int63_lt. - -Primitive leb := #int63_le. +Notation int := int (only parsing). +Notation lsl := lsl (only parsing). +Notation lsr := lsr (only parsing). +Notation land := land (only parsing). +Notation lor := lor (only parsing). +Notation lxor := lxor (only parsing). +Notation add := add (only parsing). +Notation sub := sub (only parsing). +Notation mul := mul (only parsing). +Notation mulc := mulc (only parsing). +Notation div := div (only parsing). +Notation mod := mod (only parsing). +Notation eqb := eqb (only parsing). +Notation ltb := ltb (only parsing). +Notation leb := leb (only parsing). Local Open Scope int63_scope. @@ -139,34 +109,29 @@ Register Inline subcarry. Definition addc_def x y := let r := x + y in if r <? x then C1 r else C0 r. -(* the same but direct implementation for efficiency *) -Primitive addc := #int63_addc. +Notation addc := addc (only parsing). Definition addcarryc_def x y := let r := addcarry x y in if r <=? x then C1 r else C0 r. -(* the same but direct implementation for efficiency *) -Primitive addcarryc := #int63_addcarryc. +Notation addcarryc := addcarryc (only parsing). Definition subc_def x y := if y <=? x then C0 (x - y) else C1 (x - y). -(* the same but direct implementation for efficiency *) -Primitive subc := #int63_subc. +Notation subc := subc (only parsing). Definition subcarryc_def x y := if y <? x then C0 (x - y - 1) else C1 (x - y - 1). -(* the same but direct implementation for efficiency *) -Primitive subcarryc := #int63_subcarryc. +Notation subcarryc := subcarryc (only parsing). Definition diveucl_def x y := (x/y, x mod y). -(* the same but direct implementation for efficiency *) -Primitive diveucl := #int63_diveucl. +Notation diveucl := diveucl (only parsing). -Primitive diveucl_21 := #int63_div21. +Notation diveucl_21 := diveucl_21 (only parsing). Definition addmuldiv_def p x y := (x << p) lor (y >> (digits - p)). -Primitive addmuldiv := #int63_addmuldiv. +Notation addmuldiv := addmuldiv (only parsing). Module Import Int63NotationsInternalC. Notation "- x" := (opp x) : int63_scope. @@ -188,7 +153,7 @@ Definition compare_def x y := if x <? y then Lt else if (x =? y) then Eq else Gt. -Primitive compare := #int63_compare. +Notation compare := compare (only parsing). Import Bool ZArith. (** Translation to Z *) @@ -371,8 +336,8 @@ Axiom leb_spec : forall x y, (x <=? y)%int63 = true <-> φ x <= φ y. (** Exotic operations *) (** I should add the definition (like for compare) *) -Primitive head0 := #int63_head0. -Primitive tail0 := #int63_tail0. +Notation head0 := head0 (only parsing). +Notation tail0 := tail0 (only parsing). (** Axioms on operations which are just short cut *) @@ -1950,7 +1915,6 @@ Module Export Int63Notations. Notation "m <= n" := (m <=? n) : int63_scope. #[deprecated(since="8.13",note="use infix ≤? instead")] Notation "m ≤ n" := (m <=? n) (at level 70, no associativity) : int63_scope. - Export Int63NotationsInternalA. Export Int63NotationsInternalB. Export Int63NotationsInternalC. Export Int63NotationsInternalD. diff --git a/theories/Numbers/Cyclic/Int63/PrimInt63.v b/theories/Numbers/Cyclic/Int63/PrimInt63.v new file mode 100644 index 0000000000..64c1b862c7 --- /dev/null +++ b/theories/Numbers/Cyclic/Int63/PrimInt63.v @@ -0,0 +1,82 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Export CarryType. + +Register bool as kernel.ind_bool. +Register prod as kernel.ind_pair. +Register carry as kernel.ind_carry. +Register comparison as kernel.ind_cmp. + +Primitive int := #int63_type. +Register int as num.int63.type. +Declare Scope int63_scope. +Definition id_int : int -> int := fun x => x. +Declare ML Module "int63_syntax_plugin". + +Module Export Int63NotationsInternalA. +Delimit Scope int63_scope with int63. +Bind Scope int63_scope with int. +End Int63NotationsInternalA. + +(* Logical operations *) +Primitive lsl := #int63_lsl. + +Primitive lsr := #int63_lsr. + +Primitive land := #int63_land. + +Primitive lor := #int63_lor. + +Primitive lxor := #int63_lxor. + +(* Arithmetic modulo operations *) +Primitive add := #int63_add. + +Primitive sub := #int63_sub. + +Primitive mul := #int63_mul. + +Primitive mulc := #int63_mulc. + +Primitive div := #int63_div. + +Primitive mod := #int63_mod. + +(* Comparisons *) +Primitive eqb := #int63_eq. + +Primitive ltb := #int63_lt. + +Primitive leb := #int63_le. + +(** Exact arithmetic operations *) + +Primitive addc := #int63_addc. + +Primitive addcarryc := #int63_addcarryc. + +Primitive subc := #int63_subc. + +Primitive subcarryc := #int63_subcarryc. + +Primitive diveucl := #int63_diveucl. + +Primitive diveucl_21 := #int63_div21. + +Primitive addmuldiv := #int63_addmuldiv. + +(** Comparison *) +Primitive compare := #int63_compare. + +(** Exotic operations *) + +Primitive head0 := #int63_head0. +Primitive tail0 := #int63_tail0. diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index a563dcbf95..d8eb005ab2 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -1944,7 +1944,121 @@ Proof. by move=> subD [g' fK g'K]; exists g' => x; move/subD; [apply: fK | apply: g'K]. Qed. +Lemma in_on1P : {in D1, {on D2, allQ1 f}} <-> + {in [pred x in D1 | f x \in D2], allQ1 f}. +Proof. +split => allf x; have := allf x; rewrite inE => Q1f; first by case/andP. +by move=> ? ?; apply: Q1f; apply/andP. +Qed. + +Lemma in_on1lP : {in D1, {on D2, allQ1l f & h}} <-> + {in [pred x in D1 | f x \in D2], allQ1l f h}. +Proof. +split => allf x; have := allf x; rewrite inE => Q1f; first by case/andP. +by move=> ? ?; apply: Q1f; apply/andP. +Qed. + +Lemma in_on2P : {in D1 &, {on D2 &, allQ2 f}} <-> + {in [pred x in D1 | f x \in D2] &, allQ2 f}. +Proof. +split => allf x y; have := allf x y; rewrite !inE => Q2f. + by move=> /andP[? ?] /andP[? ?]; apply: Q2f. +by move=> ? ? ? ?; apply: Q2f; apply/andP. +Qed. + +Lemma on1W_in : {in D1, allQ1 f} -> {in D1, {on D2, allQ1 f}}. +Proof. by move=> D1f ? /D1f. Qed. + +Lemma on1lW_in : {in D1, allQ1l f h} -> {in D1, {on D2, allQ1l f & h}}. +Proof. by move=> D1f ? /D1f. Qed. + +Lemma on2W_in : {in D1 &, allQ2 f} -> {in D1 &, {on D2 &, allQ2 f}}. +Proof. by move=> D1f ? ? ? ? ? ?; apply: D1f. Qed. + +Lemma in_on1W : allQ1 f -> {in D1, {on D2, allQ1 f}}. +Proof. by move=> allf ? ? ?; apply: allf. Qed. + +Lemma in_on1lW : allQ1l f h -> {in D1, {on D2, allQ1l f & h}}. +Proof. by move=> allf ? ? ?; apply: allf. Qed. + +Lemma in_on2W : allQ2 f -> {in D1 &, {on D2 &, allQ2 f}}. +Proof. by move=> allf ? ? ? ? ? ?; apply: allf. Qed. + +Lemma on1S : (forall x, f x \in D2) -> {on D2, allQ1 f} -> allQ1 f. +Proof. by move=> ? fD1 ?; apply: fD1. Qed. + +Lemma on1lS : (forall x, f x \in D2) -> {on D2, allQ1l f & h} -> allQ1l f h. +Proof. by move=> ? fD1 ?; apply: fD1. Qed. + +Lemma on2S : (forall x, f x \in D2) -> {on D2 &, allQ2 f} -> allQ2 f. +Proof. by move=> ? fD1 ? ?; apply: fD1. Qed. + +Lemma on1S_in : {homo f : x / x \in D1 >-> x \in D2} -> + {in D1, {on D2, allQ1 f}} -> {in D1, allQ1 f}. +Proof. by move=> fD fD1 ? ?; apply/fD1/fD. Qed. + +Lemma on1lS_in : {homo f : x / x \in D1 >-> x \in D2} -> + {in D1, {on D2, allQ1l f & h}} -> {in D1, allQ1l f h}. +Proof. by move=> fD fD1 ? ?; apply/fD1/fD. Qed. + +Lemma on2S_in : {homo f : x / x \in D1 >-> x \in D2} -> + {in D1 &, {on D2 &, allQ2 f}} -> {in D1 &, allQ2 f}. +Proof. by move=> fD fD1 ? ? ? ?; apply: fD1 => //; apply: fD. Qed. + +Lemma in_on1S : (forall x, f x \in D2) -> {in T1, {on D2, allQ1 f}} -> allQ1 f. +Proof. by move=> fD2 fD1 ?; apply: fD1. Qed. + +Lemma in_on1lS : (forall x, f x \in D2) -> + {in T1, {on D2, allQ1l f & h}} -> allQ1l f h. +Proof. by move=> fD2 fD1 ?; apply: fD1. Qed. + +Lemma in_on2S : (forall x, f x \in D2) -> + {in T1 &, {on D2 &, allQ2 f}} -> allQ2 f. +Proof. by move=> fD2 fD1 ? ?; apply: fD1. Qed. + End LocalGlobal. +Arguments in_on1P {T1 T2 D1 D2 f Q1}. +Arguments in_on1lP {T1 T2 T3 D1 D2 f h Q1l}. +Arguments in_on2P {T1 T2 D1 D2 f Q2}. +Arguments on1W_in {T1 T2 D1} D2 {f Q1}. +Arguments on1lW_in {T1 T2 T3 D1} D2 {f h Q1l}. +Arguments on2W_in {T1 T2 D1} D2 {f Q2}. +Arguments in_on1W {T1 T2} D1 D2 {f Q1}. +Arguments in_on1lW {T1 T2 T3} D1 D2 {f h Q1l}. +Arguments in_on2W {T1 T2} D1 D2 {f Q2}. +Arguments on1S {T1 T2} D2 {f Q1}. +Arguments on1lS {T1 T2 T3} D2 {f h Q1l}. +Arguments on2S {T1 T2} D2 {f Q2}. +Arguments on1S_in {T1 T2 D1} D2 {f Q1}. +Arguments on1lS_in {T1 T2 T3 D1} D2 {f h Q1l}. +Arguments on2S_in {T1 T2 D1} D2 {f Q2}. +Arguments in_on1S {T1 T2} D2 {f Q1}. +Arguments in_on1lS {T1 T2 T3} D2 {f h Q1l}. +Arguments in_on2S {T1 T2} D2 {f Q2}. + +Section in_sig. + +Variables T1 T2 T3 : Type. +Variables (D1 : {pred T1}) (D2 : {pred T2}) (D3 : {pred T3}). +Variable P1 : T1 -> Prop. +Variable P2 : T1 -> T2 -> Prop. +Variable P3 : T1 -> T2 -> T3 -> Prop. + +Lemma in1_sig : {in D1, {all1 P1}} -> forall x : sig D1, P1 (sval x). +Proof. by move=> DP [x Dx]; have := DP _ Dx. Qed. + +Lemma in2_sig : {in D1 & D2, {all2 P2}} -> + forall (x : sig D1) (y : sig D2), P2 (sval x) (sval y). +Proof. by move=> DP [x Dx] [y Dy]; have := DP _ _ Dx Dy. Qed. + +Lemma in3_sig : {in D1 & D2 & D3, {all3 P3}} -> + forall (x : sig D1) (y : sig D2) (z : sig D3), P3 (sval x) (sval y) (sval z). +Proof. by move=> DP [x Dx] [y Dy] [z Dz]; have := DP _ _ _ Dx Dy Dz. Qed. + +End in_sig. +Arguments in1_sig {T1 D1 P1}. +Arguments in2_sig {T1 T2 D1 D2 P2}. +Arguments in3_sig {T1 T2 T3 D1 D2 D3 P3}. Lemma sub_in2 T d d' (P : T -> T -> Prop) : sub_mem d d' -> forall Ph : ph {all2 P}, prop_in2 d' Ph -> prop_in2 d Ph. |