diff options
Diffstat (limited to 'theories')
24 files changed, 720 insertions, 255 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 6978fa1ddf..a1a4da6f37 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -87,7 +87,7 @@ Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left. Next Obligation. Proof. - destruct x ; destruct y. + do 2 match goal with [ x : () |- _ ] => destruct x end. reflexivity. Qed. @@ -142,7 +142,10 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq := | _, _ => in_right end }. - Next Obligation. destruct y ; unfold not in *; eauto. Defined. + Next Obligation. + match goal with y : list _ |- _ => destruct y end ; + unfold not in *; eauto. + Defined. Solve Obligations with unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto). diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 6a98af39aa..3e71a60fa6 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -87,7 +87,7 @@ Tactic Notation "clsubst" "*" := clsubst_nofail. Lemma nequiv_equiv_trans : forall `{Setoid A} (x y z : A), x =/= y -> y == z -> x =/= z. Proof with auto. - intros; intro. + intros A ? x y z H H0 H1. assert(z == y) by (symmetry ; auto). assert(x == y) by (transitivity z ; eauto). contradiction. @@ -95,7 +95,7 @@ Qed. Lemma equiv_nequiv_trans : forall `{Setoid A} (x y z : A), x == y -> y =/= z -> x =/= z. Proof. - intros; intro. + intros A ? x y z **; intro. assert(y == x) by (symmetry ; auto). assert(y == z) by (transitivity x ; eauto). contradiction. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 2947c4831f..f4220e3aa1 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -96,7 +96,7 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) := Next Obligation. Proof. - destruct x ; destruct y. + do 2 match goal with x : () |- _ => destruct x end. reflexivity. Qed. diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 826815410a..69b158a87e 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -71,7 +71,7 @@ Hint Constructors NoDupA : core. Lemma NoDupA_altdef : forall l, NoDupA l <-> ForallOrdPairs (complement eqA) l. Proof. - split; induction 1; constructor; auto. + split; induction 1 as [|a l H rest]; constructor; auto. rewrite Forall_forall. intros b Hb. intro Eq; elim H. rewrite InA_alt. exists b; auto. rewrite InA_alt; intros (a' & Haa' & Ha'). @@ -85,7 +85,7 @@ Definition inclA l l' := forall x, InA x l -> InA x l'. Definition equivlistA l l' := forall x, InA x l <-> InA x l'. Lemma incl_nil l : inclA nil l. -Proof. intro. intros. inversion H. Qed. +Proof. intros a H. inversion H. Qed. #[local] Hint Resolve incl_nil : list. @@ -128,7 +128,7 @@ Qed. Global Instance eqlistA_equiv : Equivalence eqlistA. Proof. constructor; red. - induction x; auto. + intros x; induction x; auto. induction 1; auto. intros x y z H; revert z; induction H; auto. inversion 1; subst; auto. invlist eqlistA; eauto with *. @@ -138,9 +138,9 @@ Qed. Global Instance eqlistA_equivlistA : subrelation eqlistA equivlistA. Proof. - intros x x' H. induction H. + intros x x' H. induction H as [|? ? ? ? H ? IHeqlistA]. intuition. - red; intros. + red; intros x0. rewrite 2 InA_cons. rewrite (IHeqlistA x0), H; intuition. Qed. @@ -165,7 +165,7 @@ Hint Immediate InA_eqA : core. Lemma In_InA : forall l x, In x l -> InA x l. Proof. - simple induction l; simpl; intuition. + intros l; induction l; simpl; intuition. subst; auto. Qed. #[local] @@ -174,8 +174,9 @@ Hint Resolve In_InA : core. Lemma InA_split : forall l x, InA x l -> exists l1 y l2, eqA x y /\ l = l1++y::l2. Proof. -induction l; intros; inv. +intros l; induction l as [|a l IHl]; intros x H; inv. exists (@nil A); exists a; exists l; auto. +match goal with H' : InA x l |- _ => rename H' into H0 end. destruct (IHl x H0) as (l1,(y,(l2,(H1,H2)))). exists (a::l1); exists y; exists l2; auto. split; simpl; f_equal; auto. @@ -184,9 +185,10 @@ Qed. Lemma InA_app : forall l1 l2 x, InA x (l1 ++ l2) -> InA x l1 \/ InA x l2. Proof. - induction l1; simpl in *; intuition. + intros l1; induction l1 as [|a l1 IHl1]; simpl in *; intuition. inv; auto. - elim (IHl1 l2 x H0); auto. + match goal with H0' : InA _ (l1 ++ _) |- _ => rename H0' into H0 end. + elim (IHl1 _ _ H0); auto. Qed. Lemma InA_app_iff : forall l1 l2 x, @@ -194,7 +196,7 @@ Lemma InA_app_iff : forall l1 l2 x, Proof. split. apply InA_app. - destruct 1; generalize H; do 2 rewrite InA_alt. + destruct 1 as [H|H]; generalize H; do 2 rewrite InA_alt. destruct 1 as (y,(H1,H2)); exists y; split; auto. apply in_or_app; auto. destruct 1 as (y,(H1,H2)); exists y; split; auto. @@ -240,11 +242,12 @@ Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' -> (forall x, InA x l -> InA x l' -> False) -> NoDupA (l++l'). Proof. -induction l; simpl; auto; intros. +intros l; induction l as [|a l IHl]; simpl; auto; intros l' H H0 H1. inv. constructor. rewrite InA_alt; intros (y,(H4,H5)). destruct (in_app_or _ _ _ H5). +match goal with H2' : ~ InA a l |- _ => rename H2' into H2 end. elim H2. rewrite InA_alt. exists y; auto. @@ -253,13 +256,13 @@ auto. rewrite InA_alt. exists y; auto. apply IHl; auto. -intros. +intros x ? ?. apply (H1 x); auto. Qed. Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l). Proof. -induction l. +intros l; induction l. simpl; auto. simpl; intros. inv. @@ -270,17 +273,17 @@ intros x. rewrite InA_alt. intros (x1,(H2,H3)). intro; inv. -destruct H0. -rewrite <- H4, H2. +match goal with H0 : ~ InA _ _ |- _ => destruct H0 end. +match goal with H4 : eqA x ?x' |- InA ?x' _ => rewrite <- H4, H2 end. apply In_InA. rewrite In_rev; auto. Qed. Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l'). Proof. - induction l; simpl in *; intros; inv; auto. + intros l; induction l; simpl in *; intros; inv; auto. constructor; eauto. - contradict H0. + match goal with H0 : ~ InA _ _ |- _ => contradict H0 end. rewrite InA_app_iff in *. rewrite InA_cons. intuition. @@ -288,17 +291,17 @@ Qed. Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l'). Proof. - induction l; simpl in *; intros; inv; auto. + intros l; induction l as [|a l IHl]; simpl in *; intros l' x H; inv; auto. constructor; eauto. - assert (H2:=IHl _ _ H1). + match goal with H1 : NoDupA (l ++ x :: l') |- _ => assert (H2:=IHl _ _ H1) end. inv. rewrite InA_cons. red; destruct 1. - apply H0. + match goal with H0 : ~ InA a (l ++ x :: l') |- _ => apply H0 end. rewrite InA_app_iff in *; rewrite InA_cons; auto. - apply H; auto. + auto. constructor. - contradict H0. + match goal with H0 : ~ InA a (l ++ x :: l') |- _ => contradict H0 end. rewrite InA_app_iff in *; rewrite InA_cons; intuition. eapply NoDupA_split; eauto. Qed. @@ -356,19 +359,21 @@ Lemma equivlistA_NoDupA_split l l1 l2 x y : eqA x y -> NoDupA (x::l) -> NoDupA (l1++y::l2) -> equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2). Proof. - intros; intro a. + intros H H0 H1 H2; intro a. generalize (H2 a). rewrite !InA_app_iff, !InA_cons. inv. assert (SW:=NoDupA_swap H1). inv. - rewrite InA_app_iff in H0. + rewrite InA_app_iff in *. split; intros. - assert (~eqA a x) by (contradict H3; rewrite <- H3; auto). + match goal with H3 : ~ InA x l |- _ => + assert (~eqA a x) by (contradict H3; rewrite <- H3; auto) + end. assert (~eqA a y) by (rewrite <- H; auto). tauto. - assert (OR : eqA a x \/ InA a l) by intuition. clear H6. + assert (OR : eqA a x \/ InA a l) by intuition. destruct OR as [EQN|INA]; auto. - elim H0. + match goal with H0 : ~ (InA y l1 \/ InA y l2) |- _ => elim H0 end. rewrite <-H,<-EQN; auto. Qed. @@ -448,7 +453,7 @@ Qed. Lemma ForallOrdPairs_inclA : forall l l', NoDupA l' -> inclA l' l -> ForallOrdPairs R l -> ForallOrdPairs R l'. Proof. -induction l' as [|x l' IH]. +intros l l'. induction l' as [|x l' IH]. constructor. intros ND Incl FOP. apply FOP_cons; inv; unfold inclA in *; auto. rewrite Forall_forall; intros y Hy. @@ -476,7 +481,7 @@ Lemma fold_right_commutes_restr : forall s1 s2 x, ForallOrdPairs R (s1++x::s2) -> eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))). Proof. -induction s1; simpl; auto; intros. +intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x H. reflexivity. transitivity (f a (f x (fold_right f i (s1++s2)))). apply Comp; auto. @@ -484,7 +489,9 @@ apply IHs1. invlist ForallOrdPairs; auto. apply TraR. invlist ForallOrdPairs; auto. -rewrite Forall_forall in H0; apply H0. +match goal with H0 : Forall (R a) (s1 ++ x :: s2) |- R a x => + rewrite Forall_forall in H0; apply H0 +end. apply in_or_app; simpl; auto. Qed. @@ -492,14 +499,14 @@ Lemma fold_right_equivlistA_restr : forall s s', NoDupA s -> NoDupA s' -> ForallOrdPairs R s -> equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s'). Proof. - simple induction s. - destruct s'; simpl. + intros s; induction s as [|x l Hrec]. + intros s'; destruct s' as [|a s']; simpl. intros; reflexivity. - unfold equivlistA; intros. + unfold equivlistA; intros H H0 H1 H2. destruct (H2 a). assert (InA a nil) by auto; inv. - intros x l Hrec s' N N' F E; simpl in *. - assert (InA x s') by (rewrite <- (E x); auto). + intros s' N N' F E; simpl in *. + assert (InA x s') as H by (rewrite <- (E x); auto). destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))). subst s'. transitivity (f x (fold_right f i (s1++s2))). @@ -520,7 +527,7 @@ Lemma fold_right_add_restr : forall s' s x, NoDupA s -> NoDupA s' -> ForallOrdPairs R s' -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)). Proof. - intros; apply (@fold_right_equivlistA_restr s' (x::s)); auto. + intros s' s x **; apply (@fold_right_equivlistA_restr s' (x::s)); auto. Qed. End Fold_With_Restriction. @@ -532,7 +539,7 @@ Variable Tra :transpose f. Lemma fold_right_commutes : forall s1 s2 x, eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))). Proof. -induction s1; simpl; auto; intros. +intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x. reflexivity. transitivity (f a (f x (fold_right f i (s1++s2)))); auto. apply Comp; auto. @@ -542,7 +549,7 @@ Lemma fold_right_equivlistA : forall s s', NoDupA s -> NoDupA s' -> equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s'). Proof. -intros; apply fold_right_equivlistA_restr with (R:=fun _ _ => True); +intros; apply (fold_right_equivlistA_restr (R:=fun _ _ => True)); repeat red; auto. apply ForallPairs_ForallOrdPairs; try red; auto. Qed. @@ -551,7 +558,7 @@ Lemma fold_right_add : forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)). Proof. - intros; apply (@fold_right_equivlistA s' (x::s)); auto. + intros s' s x **; apply (@fold_right_equivlistA s' (x::s)); auto. Qed. End Fold. @@ -571,7 +578,7 @@ Lemma fold_right_eqlistA2 : eqB (fold_right f i s) (fold_right f j s'). Proof. intros s. - induction s;intros. + induction s as [|a s IHs];intros s' i j heqij heqss'. - inversion heqss'. subst. simpl. @@ -604,7 +611,7 @@ Lemma fold_right_commutes_restr2 : forall s1 s2 x (i j:B) (heqij: eqB i j), ForallOrdPairs R (s1++x::s2) -> eqB (fold_right f i (s1++x::s2)) (f x (fold_right f j (s1++s2))). Proof. -induction s1; simpl; auto; intros. +intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x i j heqij ?. - apply Comp. + destruct eqA_equiv. apply Equivalence_Reflexive. + eapply fold_right_eqlistA2. @@ -617,7 +624,9 @@ induction s1; simpl; auto; intros. invlist ForallOrdPairs; auto. apply TraR. invlist ForallOrdPairs; auto. - rewrite Forall_forall in H0; apply H0. + match goal with H0 : Forall (R a) (s1 ++ x :: s2) |- _ => + rewrite Forall_forall in H0; apply H0 + end. apply in_or_app; simpl; auto. reflexivity. Qed. @@ -628,14 +637,14 @@ Lemma fold_right_equivlistA_restr2 : equivlistA s s' -> eqB i j -> eqB (fold_right f i s) (fold_right f j s'). Proof. - simple induction s. - destruct s'; simpl. + intros s; induction s as [|x l Hrec]. + intros s'; destruct s' as [|a s']; simpl. intros. assumption. - unfold equivlistA; intros. + unfold equivlistA; intros ? ? H H0 H1 H2 **. destruct (H2 a). assert (InA a nil) by auto; inv. - intros x l Hrec s' i j N N' F E eqij; simpl in *. - assert (InA x s') by (rewrite <- (E x); auto). + intros s' i j N N' F E eqij; simpl in *. + assert (InA x s') as H by (rewrite <- (E x); auto). destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))). subst s'. transitivity (f x (fold_right f j (s1++s2))). @@ -663,7 +672,7 @@ Lemma fold_right_add_restr2 : forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ForallOrdPairs R s' -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)). Proof. - intros; apply (@fold_right_equivlistA_restr2 s' (x::s) i j); auto. + intros s' s i j x **; apply (@fold_right_equivlistA_restr2 s' (x::s) i j); auto. Qed. End Fold2_With_Restriction. @@ -674,7 +683,7 @@ Lemma fold_right_commutes2 : forall s1 s2 i x x', eqA x x' -> eqB (fold_right f i (s1++x::s2)) (f x' (fold_right f i (s1++s2))). Proof. - induction s1;simpl;intros. + intros s1; induction s1 as [|a s1 IHs1];simpl;intros s2 i x x' H. - apply Comp;auto. reflexivity. - transitivity (f a (f x' (fold_right f i (s1++s2)))); auto. @@ -688,7 +697,7 @@ Lemma fold_right_equivlistA2 : equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s'). Proof. red in Tra. -intros; apply fold_right_equivlistA_restr2 with (R:=fun _ _ => True); +intros; apply (fold_right_equivlistA_restr2 (R:=fun _ _ => True)); repeat red; auto. apply ForallPairs_ForallOrdPairs; try red; auto. Qed. @@ -697,9 +706,9 @@ Lemma fold_right_add2 : forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)). Proof. - intros. + intros s' s i j x **. replace (f x (fold_right f j s)) with (fold_right f j (x::s)) by auto. - eapply fold_right_equivlistA2;auto. + eapply fold_right_equivlistA2;auto. Qed. End Fold2. @@ -710,7 +719,7 @@ Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}. Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }. Proof. -induction l. +intros x l; induction l as [|a l IHl]. right; auto. intro; inv. destruct (eqA_dec x a). @@ -729,28 +738,30 @@ Fixpoint removeA (x : A) (l : list A) : list A := Lemma removeA_filter : forall x l, removeA x l = filter (fun y => if eqA_dec x y then false else true) l. Proof. -induction l; simpl; auto. +intros x l; induction l as [|a l IHl]; simpl; auto. destruct (eqA_dec x a); auto. rewrite IHl; auto. Qed. Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y. Proof. -induction l; simpl; auto. -split. +intros l; induction l as [|a l IHl]; simpl; auto. +intros x y; split. intro; inv. destruct 1; inv. -intros. +intros x y. destruct (eqA_dec x a) as [Heq|Hnot]; simpl; auto. rewrite IHl; split; destruct 1; split; auto. inv; auto. -destruct H0; transitivity a; auto. +match goal with H0 : ~ eqA x y |- _ => destruct H0 end; transitivity a; auto. split. intro; inv. split; auto. contradict Hnot. transitivity y; auto. -rewrite (IHl x y) in H0; destruct H0; auto. +match goal with H0 : InA y (removeA x l) |- _ => + rewrite (IHl x y) in H0; destruct H0; auto +end. destruct 1; inv; auto. right; rewrite IHl; auto. Qed. @@ -758,7 +769,7 @@ Qed. Lemma removeA_NoDupA : forall s x, NoDupA s -> NoDupA (removeA x s). Proof. -simple induction s; simpl; intros. +intros s; induction s as [|a s IHs]; simpl; intros x ?. auto. inv. destruct (eqA_dec x a); simpl; auto. @@ -770,16 +781,16 @@ Qed. Lemma removeA_equivlistA : forall l l' x, ~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l'). Proof. -unfold equivlistA; intros. +unfold equivlistA; intros l l' x H H0 x0. rewrite removeA_InA. -split; intros. +split; intros H1. rewrite <- H0; split; auto. contradict H. apply InA_eqA with x0; auto. rewrite <- (H0 x0) in H1. destruct H1. inv; auto. -elim H2; auto. +match goal with H2 : ~ eqA x x0 |- _ => elim H2; auto end. Qed. End Remove. @@ -806,7 +817,7 @@ Hint Constructors lelistA sort : core. Lemma InfA_ltA : forall l x y, ltA x y -> InfA y l -> InfA x l. Proof. - destruct l; constructor. inv; eauto. + intros l; destruct l; constructor. inv; eauto. Qed. Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA. @@ -815,8 +826,8 @@ Proof using eqA_equiv ltA_compat. (* and not ltA_strorder *) inversion_clear Hll'. intuition. split; intro; inv; constructor. - rewrite <- Hxx', <- H; auto. - rewrite Hxx', H; auto. + match goal with H : eqA _ _ |- _ => rewrite <- Hxx', <- H; auto end. + match goal with H : eqA _ _ |- _ => rewrite Hxx', H; auto end. Qed. (** For compatibility, can be deduced from [InfA_compat] *) @@ -830,9 +841,9 @@ Hint Immediate InfA_ltA InfA_eqA : core. Lemma SortA_InfA_InA : forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x. Proof. - simple induction l. - intros. inv. - intros. inv. + intros l; induction l as [|a l IHl]. + intros x a **. inv. + intros x a0 **. inv. setoid_replace x with a; auto. eauto. Qed. @@ -840,13 +851,13 @@ Qed. Lemma In_InfA : forall l x, (forall y, In y l -> ltA x y) -> InfA x l. Proof. - simple induction l; simpl; intros; constructor; auto. + intros l; induction l; simpl; intros; constructor; auto. Qed. Lemma InA_InfA : forall l x, (forall y, InA y l -> ltA x y) -> InfA x l. Proof. - simple induction l; simpl; intros; constructor; auto. + intros l; induction l; simpl; intros; constructor; auto. Qed. (* In fact, this may be used as an alternative definition for InfA: *) @@ -861,7 +872,7 @@ Qed. Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2). Proof. - induction l1; simpl; auto. + intros l1; induction l1; simpl; auto. intros; inv; auto. Qed. @@ -870,7 +881,7 @@ Lemma SortA_app : (forall x y, InA x l1 -> InA y l2 -> ltA x y) -> SortA (l1 ++ l2). Proof. - induction l1; simpl in *; intuition. + intros l1; induction l1; intros l2; simpl in *; intuition. inv. constructor; auto. apply InfA_app; auto. @@ -879,8 +890,8 @@ Qed. Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l. Proof. - simple induction l; auto. - intros x l' H H0. + intros l; induction l as [|x l' H]; auto. + intros H0. inv. constructor; auto. intro. @@ -922,7 +933,7 @@ Qed. Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A). Proof. -repeat red. intros. +repeat red. intros x y ?. rewrite <- (app_nil_r (rev x)), <- (app_nil_r (rev y)). apply eqlistA_rev_app; auto. Qed. @@ -936,15 +947,15 @@ Qed. Lemma SortA_equivlistA_eqlistA : forall l l', SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'. Proof. -induction l; destruct l'; simpl; intros; auto. -destruct (H1 a); assert (InA a nil) by auto; inv. +intros l; induction l as [|a l IHl]; intros l'; destruct l' as [|a0 l']; simpl; intros H H0 H1; auto. +destruct (H1 a0); assert (InA a0 nil) by auto; inv. destruct (H1 a); assert (InA a nil) by auto; inv. inv. assert (forall y, InA y l -> ltA a y). -intros; eapply SortA_InfA_InA with (l:=l); eauto. +intros; eapply (SortA_InfA_InA (l:=l)); eauto. assert (forall y, InA y l' -> ltA a0 y). -intros; eapply SortA_InfA_InA with (l:=l'); eauto. -clear H3 H4. +intros; eapply (SortA_InfA_InA (l:=l')); eauto. +do 2 match goal with H : InfA _ _ |- _ => clear H end. assert (eqA a a0). destruct (H1 a). destruct (H1 a0). @@ -953,13 +964,19 @@ assert (eqA a a0). elim (StrictOrder_Irreflexive a); eauto. constructor; auto. apply IHl; auto. -split; intros. +intros x; split; intros. destruct (H1 x). assert (InA x (a0::l')) by auto. inv; auto. -rewrite H9,<-H3 in H4. elim (StrictOrder_Irreflexive a); eauto. +match goal with H3 : eqA a a0, H4 : InA x l, H9 : eqA x a0 |- InA x l' => + rewrite H9,<-H3 in H4 +end. +elim (StrictOrder_Irreflexive a); eauto. destruct (H1 x). assert (InA x (a::l)) by auto. inv; auto. -rewrite H9,H3 in H4. elim (StrictOrder_Irreflexive a0); eauto. +match goal with H3 : eqA a a0, H4 : InA x l', H9 : eqA x a |- InA x l => + rewrite H9,H3 in H4 +end. +elim (StrictOrder_Irreflexive a0); eauto. Qed. End EqlistA. @@ -970,12 +987,12 @@ Section Filter. Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l). Proof. -induction l; simpl; auto. +intros f l; induction l as [|a l IHl]; simpl; auto. intros; inv; auto. destruct (f a); auto. constructor; auto. apply In_InfA; auto. -intros. +intros y H. rewrite filter_In in H; destruct H. eapply SortA_InfA_InA; eauto. Qed. @@ -984,12 +1001,14 @@ Arguments eq {A} x _. Lemma filter_InA : forall f, Proper (eqA==>eq) f -> forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true. Proof. +(* Unset Mangle Names. *) clear sotrans ltA ltA_strorder ltA_compat. -intros; do 2 rewrite InA_alt; intuition. -destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition. -destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition. +intros f H l x; do 2 rewrite InA_alt; intuition; + match goal with Hex' : exists _, _ |- _ => rename Hex' into Hex end. +destruct Hex as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition. +destruct Hex as (y,(H0,H1)); rewrite filter_In in H1; intuition. rewrite (H _ _ H0); auto. -destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition. +destruct Hex as (y,(H0,H1)); exists y; rewrite filter_In; intuition. rewrite <- (H _ _ H0); auto. Qed. @@ -997,19 +1016,20 @@ Lemma filter_split : forall f, (forall x y, f x = true -> f y = false -> ltA x y) -> forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l. Proof. -induction l; simpl; intros; auto. +intros f H l; induction l as [|a l IHl]; simpl; intros H0; auto. inv. +match goal with H1' : SortA l, H2' : InfA a l |- _ => rename H1' into H1, H2' into H2 end. rewrite IHl at 1; auto. case_eq (f a); simpl; intros; auto. -assert (forall e, In e l -> f e = false). - intros. +assert (forall e, In e l -> f e = false) as H3. + intros e H3. assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)). case_eq (f e); simpl; intros; auto. elim (StrictOrder_Irreflexive e). transitivity a; auto. replace (List.filter f l) with (@nil A); auto. -generalize H3; clear; induction l; simpl; auto. -case_eq (f a); auto; intros. +generalize H3; clear; induction l as [|a l IHl]; simpl; auto. +case_eq (f a); auto; intros H H3. rewrite H3 in H; auto; try discriminate. Qed. @@ -1043,23 +1063,24 @@ Lemma findA_NoDupA : Proof. set (eqk := fun p p' : A*B => eqA (fst p) (fst p')). set (eqke := fun p p' : A*B => eqA (fst p) (fst p') /\ snd p = snd p'). -induction l; intros; simpl. -split; intros; try discriminate. +intros l; induction l as [|a l IHl]; intros a0 b H; simpl. +split; intros H0; try discriminate. invlist InA. destruct a as (a',b'); rename a0 into a. invlist NoDupA. split; intros. invlist InA. -compute in H2; destruct H2. subst b'. +match goal with H2 : eqke (a, b) (a', b') |- _ => compute in H2; destruct H2 end. +subst b'. destruct (eqA_dec a a'); intuition. destruct (eqA_dec a a') as [HeqA|]; simpl. -contradict H0. -revert HeqA H2; clear - eqA_equiv. +match goal with H0 : ~ InA eqk (a', b') l |- _ => contradict H0 end. +match goal with H2 : InA eqke (a, b) l |- _ => revert HeqA H2; clear - eqA_equiv end. induction l. intros; invlist InA. intros; invlist InA; auto. -destruct a0. -compute in H; destruct H. +match goal with |- InA eqk _ (?p :: _) => destruct p as [a0 b0] end. +match goal with H : eqke (a, b) (a0, b0) |- _ => compute in H; destruct H end. subst b. left; auto. compute. diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v index 131668154e..7560ea96b5 100644 --- a/theories/Logic/ProofIrrelevanceFacts.v +++ b/theories/Logic/ProofIrrelevanceFacts.v @@ -27,7 +27,7 @@ Module ProofIrrelevanceTheory (M:ProofIrrelevance). forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. Proof. - intros; rewrite M.proof_irrelevance with (p1:=h) (p2:=eq_refl p). + intros U p Q x h; rewrite (M.proof_irrelevance _ h (eq_refl p)). reflexivity. Qed. End Eq_rect_eq. @@ -45,8 +45,8 @@ Module ProofIrrelevanceTheory (M:ProofIrrelevance). forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y), x = y -> exist P x p = exist P y q. Proof. - intros. - rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H). + intros U P x y p q H. + rewrite (M.proof_irrelevance _ q (eq_rect x P p y H)). elim H using eq_indd. reflexivity. Qed. @@ -55,8 +55,8 @@ Module ProofIrrelevanceTheory (M:ProofIrrelevance). forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y), x = y -> existT P x p = existT P y q. Proof. - intros. - rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H). + intros U P x y p q H. + rewrite (M.proof_irrelevance _ q (eq_rect x P p y H)). elim H using eq_indd. reflexivity. Qed. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 7bb725538b..a3ebe67325 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -205,6 +205,7 @@ Qed. Corollary to_Z_bounded : forall x, (0 <= φ x < wB)%Z. Proof. apply to_Z_rec_bounded. Qed. + (* =================================================== *) Local Open Scope Z_scope. (* General arithmetic results *) @@ -1904,6 +1905,22 @@ Qed. Lemma lxor0_r i : i lxor 0 = i. Proof. rewrite lxorC; exact (lxor0 i). Qed. +Lemma opp_to_Z_opp (x : int) : + φ x mod wB <> 0 -> + (- φ (- x)) mod wB = (φ x) mod wB. +Proof. + intros neqx0. + rewrite opp_spec. + rewrite (Z_mod_nz_opp_full (φ x%int63)) by assumption. + rewrite (Z.mod_small (φ x%int63)) by apply to_Z_bounded. + rewrite <- Z.add_opp_l. + rewrite Z.opp_add_distr, Z.opp_involutive. + replace (- wB) with (-1 * wB) by easy. + rewrite Z_mod_plus by easy. + now rewrite Z.mod_small by apply to_Z_bounded. +Qed. + + Module Export Int63Notations. Local Open Scope int63_scope. #[deprecated(since="8.13",note="use infix mod instead")] diff --git a/theories/Numbers/Cyclic/Int63/PrimInt63.v b/theories/Numbers/Cyclic/Int63/PrimInt63.v index 64c1b862c7..98127ef0ac 100644 --- a/theories/Numbers/Cyclic/Int63/PrimInt63.v +++ b/theories/Numbers/Cyclic/Int63/PrimInt63.v @@ -17,11 +17,21 @@ Register comparison as kernel.ind_cmp. Primitive int := #int63_type. Register int as num.int63.type. +Variant pos_neg_int63 := Pos (d:int) | Neg (d:int). +Register pos_neg_int63 as num.int63.pos_neg_int63. Declare Scope int63_scope. Definition id_int : int -> int := fun x => x. -Declare ML Module "int63_syntax_plugin". - -Module Export Int63NotationsInternalA. +Record int_wrapper := wrap_int {int_wrap : int}. +Register wrap_int as num.int63.wrap_int. +Definition printer (x : int_wrapper) : pos_neg_int63 := Pos (int_wrap x). +Definition parser (x : pos_neg_int63) : option int := + match x with + | Pos p => Some p + | Neg _ => None + end. +Number Notation int parser printer : int63_scope. + +Module Import Int63NotationsInternalA. Delimit Scope int63_scope with int63. Bind Scope int63_scope with int. End Int63NotationsInternalA. @@ -37,6 +47,9 @@ Primitive lor := #int63_lor. Primitive lxor := #int63_lxor. + +Primitive asr := #int63_asr. + (* Arithmetic modulo operations *) Primitive add := #int63_add. @@ -50,6 +63,10 @@ Primitive div := #int63_div. Primitive mod := #int63_mod. +Primitive divs := #int63_divs. + +Primitive mods := #int63_mods. + (* Comparisons *) Primitive eqb := #int63_eq. @@ -57,6 +74,10 @@ Primitive ltb := #int63_lt. Primitive leb := #int63_le. +Primitive ltsb := #int63_lts. + +Primitive lesb := #int63_les. + (** Exact arithmetic operations *) Primitive addc := #int63_addc. @@ -76,7 +97,13 @@ Primitive addmuldiv := #int63_addmuldiv. (** Comparison *) Primitive compare := #int63_compare. +Primitive compares := #int63_compares. + (** Exotic operations *) Primitive head0 := #int63_head0. Primitive tail0 := #int63_tail0. + +Module Export PrimInt63Notations. + Export Int63NotationsInternalA. +End PrimInt63Notations. diff --git a/theories/Numbers/Cyclic/Int63/Sint63.v b/theories/Numbers/Cyclic/Int63/Sint63.v new file mode 100644 index 0000000000..c0239ae3db --- /dev/null +++ b/theories/Numbers/Cyclic/Int63/Sint63.v @@ -0,0 +1,407 @@ +(************************************************************************) +(* * 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 Import ZArith. +Import Znumtheory. +Require Export Int63. +Require Import Lia. + +Declare Scope sint63_scope. +Definition printer (x : int_wrapper) : pos_neg_int63 := + if (int_wrap x <? 4611686018427387904)%int63 then (* 2^62 *) + Pos (int_wrap x) + else + Neg ((int_wrap x) lxor max_int + 1)%int63. +Definition parser (x : pos_neg_int63) : option int := + match x with + | Pos p => if (p <? 4611686018427387904)%int63 then Some p else None + | Neg n => if (n <=? 4611686018427387904)%int63 + then Some ((n - 1) lxor max_int)%int63 else None + end. +Number Notation int parser printer : sint63_scope. + + +Module Import Sint63NotationsInternalA. +Delimit Scope sint63_scope with sint63. +Bind Scope sint63_scope with int. +End Sint63NotationsInternalA. + + +Module Import Sint63NotationsInternalB. +Infix "<<" := Int63.lsl (at level 30, no associativity) : sint63_scope. +(* TODO do we want >> to be asr or lsr? And is there a notation for the other one? *) +Infix ">>" := asr (at level 30, no associativity) : sint63_scope. +Infix "land" := Int63.land (at level 40, left associativity) : sint63_scope. +Infix "lor" := Int63.lor (at level 40, left associativity) : sint63_scope. +Infix "lxor" := Int63.lxor (at level 40, left associativity) : sint63_scope. +Infix "+" := Int63.add : sint63_scope. +Infix "-" := Int63.sub : sint63_scope. +Infix "*" := Int63.mul : sint63_scope. +Infix "/" := divs : sint63_scope. +Infix "mod" := mods (at level 40, no associativity) : sint63_scope. +Infix "=?" := Int63.eqb (at level 70, no associativity) : sint63_scope. +Infix "<?" := ltsb (at level 70, no associativity) : sint63_scope. +Infix "<=?" := lesb (at level 70, no associativity) : sint63_scope. +Infix "≤?" := lesb (at level 70, no associativity) : sint63_scope. +Notation "- x" := (opp x) : sint63_scope. +Notation "n ?= m" := (compares n m) (at level 70, no associativity) : sint63_scope. +End Sint63NotationsInternalB. + +Definition min_int := Eval vm_compute in (lsl 1 62). +Definition max_int := Eval vm_compute in (min_int - 1)%sint63. + +(** Translation to and from Z *) +Definition to_Z (i:int) := + if (i <? min_int)%int63 then + φ i%int63 + else + (- φ (- i)%int63)%Z. + +Lemma to_Z_0 : to_Z 0 = 0. +Proof. easy. Qed. + +Lemma to_Z_min : to_Z min_int = - (wB / 2). +Proof. easy. Qed. + +Lemma to_Z_max : to_Z max_int = wB / 2 - 1. +Proof. easy. Qed. + +Lemma to_Z_bounded : forall x, (to_Z min_int <= to_Z x <= to_Z max_int)%Z. +Proof. + intros x; unfold to_Z. + case ltbP; [> lia | intros _]. + case (ltbP max_int); [> intros _ | now intros H; exfalso; apply H]. + rewrite opp_spec. + rewrite Z_mod_nz_opp_full by easy. + rewrite Z.mod_small by apply Int63.to_Z_bounded. + case ltbP. + - intros ltxmin; split. + + now transitivity 0%Z; [>| now apply Int63.to_Z_bounded]. + + replace (φ min_int%int63) with (φ max_int%int63 + 1)%Z in ltxmin. + * lia. + * now compute. + - rewrite Z.nlt_ge; intros leminx. + rewrite opp_spec. + rewrite Z_mod_nz_opp_full. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + split. + * rewrite <- Z.opp_le_mono. + now rewrite <- Z.sub_le_mono_l. + * transitivity 0%Z; [>| now apply Int63.to_Z_bounded]. + rewrite Z.opp_nonpos_nonneg. + apply Zle_minus_le_0. + apply Z.lt_le_incl. + now apply Int63.to_Z_bounded. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + now intros eqx0; rewrite eqx0 in leminx. +Qed. + +Lemma of_to_Z : forall x, of_Z (to_Z x) = x. +Proof. + unfold to_Z, of_Z. + intros x. + generalize (Int63.to_Z_bounded x). + case ltbP. + - intros ltxmin [leq0x _]. + generalize (Int63.of_to_Z x). + destruct (φ x%int63). + + now intros <-. + + now intros <-; unfold Int63.of_Z. + + now intros _. + - intros nltxmin leq0xltwB. + rewrite (opp_spec x). + rewrite Z_mod_nz_opp_full. + + rewrite Zmod_small by easy. + destruct (wB - φ x%int63) eqn: iswbmx. + * lia. + * simpl. + apply to_Z_inj. + rewrite opp_spec. + generalize (of_Z_spec (Z.pos p)). + simpl Int63.of_Z; intros ->. + rewrite <- iswbmx. + rewrite <- Z.sub_0_l. + rewrite <- (Zmod_0_l wB). + rewrite <- Zminus_mod. + replace (0 - _) with (φ x%int63 - wB) by ring. + rewrite <- Zminus_mod_idemp_r. + rewrite Z_mod_same_full. + rewrite Z.sub_0_r. + now rewrite Z.mod_small. + * lia. + + rewrite Z.mod_small by easy. + intros eqx0; revert nltxmin; rewrite eqx0. + now compute. +Qed. + +Lemma to_Z_inj (x y : int) : to_Z x = to_Z y -> x = y. +Proof. exact (fun e => can_inj of_to_Z e). Qed. + +Lemma to_Z_mod_Int63to_Z (x : int) : to_Z x mod wB = φ x%int63. +Proof. + unfold to_Z. + case ltbP; [> now rewrite Z.mod_small by now apply Int63.to_Z_bounded |]. + rewrite Z.nlt_ge; intros gexmin. + rewrite opp_to_Z_opp; rewrite Z.mod_small by now apply Int63.to_Z_bounded. + - easy. + - now intros neqx0; rewrite neqx0 in gexmin. +Qed. + + +(** Centered modulo *) +Definition cmod (x d : Z) : Z := + (x + d / 2) mod d - (d / 2). + +Lemma cmod_mod (x d : Z) : + cmod (x mod d) d = cmod x d. +Proof. + now unfold cmod; rewrite Zplus_mod_idemp_l. +Qed. + +Lemma cmod_small (x d : Z) : + - (d / 2) <= x < d / 2 -> cmod x d = x. +Proof. + intros bound. + unfold cmod. + rewrite Zmod_small; [> lia |]. + split; [> lia |]. + rewrite Z.lt_add_lt_sub_r. + apply (Z.lt_le_trans _ (d / 2)); [> easy |]. + now rewrite <- Z.le_add_le_sub_r, Z.add_diag, Z.mul_div_le. +Qed. + +Lemma to_Z_cmodwB (x : int) : + to_Z x = cmod (φ x%int63) wB. +Proof. + unfold to_Z, cmod. + case ltbP; change φ (min_int)%int63 with (wB / 2). + - intros ltxmin. + rewrite Z.mod_small; [> lia |]. + split. + + now apply Z.add_nonneg_nonneg; try apply Int63.to_Z_bounded. + + change wB with (wB / 2 + wB / 2) at 2; lia. + - rewrite Z.nlt_ge; intros gexmin. + rewrite Int63.opp_spec. + rewrite Z_mod_nz_opp_full. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + rewrite <- (Z_mod_plus_full _ (-1)). + change (-1 * wB) with (- (wB / 2) - wB / 2). + rewrite <- Z.add_assoc, Zplus_minus. + rewrite Z.mod_small. + * change wB with (wB / 2 + wB / 2) at 1; lia. + * split; [> lia |]. + apply Z.lt_sub_lt_add_r. + transitivity wB; [>| easy]. + now apply Int63.to_Z_bounded. + + rewrite Z.mod_small by now apply Int63.to_Z_bounded. + now intros not0; rewrite not0 in gexmin. +Qed. + +Lemma of_Z_spec (z : Z) : to_Z (of_Z z) = cmod z wB. +Proof. now rewrite to_Z_cmodwB, Int63.of_Z_spec, cmod_mod. Qed. + +Lemma of_Z_cmod (z : Z) : of_Z (cmod z wB) = of_Z z. +Proof. now rewrite <- of_Z_spec, of_to_Z. Qed. + +Lemma is_int (z : Z) : + to_Z min_int <= z <= to_Z max_int -> + z = to_Z (of_Z z). +Proof. + rewrite to_Z_min, to_Z_max. + intros bound; rewrite of_Z_spec, cmod_small; lia. +Qed. + +(** Specification of operations that differ on signed and unsigned ints *) + +Axiom asr_spec : forall x p, to_Z (x >> p) = (to_Z x) / 2 ^ (to_Z p). + +Axiom div_spec : forall x y, + to_Z x <> to_Z min_int \/ to_Z y <> (-1)%Z -> + to_Z (x / y) = Z.quot (to_Z x) (to_Z y). + +Axiom mod_spec : forall x y, to_Z (x mod y) = Z.rem (to_Z x) (to_Z y). + +Axiom ltb_spec : forall x y, (x <? y)%sint63 = true <-> to_Z x < to_Z y. + +Axiom leb_spec : forall x y, (x <=? y)%sint63 = true <-> to_Z x <= to_Z y. + +Axiom compare_spec : forall x y, (x ?= y)%sint63 = (to_Z x ?= to_Z y). + +(** Specification of operations that coincide on signed and unsigned ints *) + +Lemma add_spec (x y : int) : + to_Z (x + y)%sint63 = cmod (to_Z x + to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.add_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Z.add_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma sub_spec (x y : int) : + to_Z (x - y)%sint63 = cmod (to_Z x - to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.sub_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Zminus_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma mul_spec (x y : int) : + to_Z (x * y)%sint63 = cmod (to_Z x * to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.mul_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Zmult_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma succ_spec (x : int) : + to_Z (succ x)%sint63 = cmod (to_Z x + 1) wB. +Proof. now unfold succ; rewrite add_spec. Qed. + +Lemma pred_spec (x : int) : + to_Z (pred x)%sint63 = cmod (to_Z x - 1) wB. +Proof. now unfold pred; rewrite sub_spec. Qed. + +Lemma opp_spec (x : int) : + to_Z (- x)%sint63 = cmod (- to_Z x) wB. +Proof. + rewrite to_Z_cmodwB, Int63.opp_spec. + rewrite <- Z.sub_0_l, <- to_Z_mod_Int63to_Z, Zminus_mod_idemp_r. + now rewrite cmod_mod. +Qed. + +(** Behaviour when there is no under or overflow *) + +Lemma add_bounded (x y : int) : + to_Z min_int <= to_Z x + to_Z y <= to_Z max_int -> + to_Z (x + y) = to_Z x + to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite add_spec, cmod_small; [>| lia]. +Qed. + +Lemma sub_bounded (x y : int) : + to_Z min_int <= to_Z x - to_Z y <= to_Z max_int -> + to_Z (x - y) = to_Z x - to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite sub_spec, cmod_small; [>| lia]. +Qed. + +Lemma mul_bounded (x y : int) : + to_Z min_int <= to_Z x * to_Z y <= to_Z max_int -> + to_Z (x * y) = to_Z x * to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite mul_spec, cmod_small; [>| lia]. +Qed. + +Lemma succ_bounded (x : int) : + to_Z min_int <= to_Z x + 1 <= to_Z max_int -> + to_Z (succ x) = to_Z x + 1. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite succ_spec, cmod_small; [>| lia]. +Qed. + +Lemma pred_bounded (x : int) : + to_Z min_int <= to_Z x - 1 <= to_Z max_int -> + to_Z (pred x) = to_Z x - 1. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite pred_spec, cmod_small; [>| lia]. +Qed. + +Lemma opp_bounded (x : int) : + to_Z min_int <= - to_Z x <= to_Z max_int -> + to_Z (- x) = - to_Z x. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite opp_spec, cmod_small; [>| lia]. +Qed. + +(** Relationship with of_Z *) + +Lemma add_of_Z (x y : int) : + (x + y)%sint63 = of_Z (to_Z x + to_Z y). +Proof. now rewrite <- of_Z_cmod, <- add_spec, of_to_Z. Qed. + +Lemma sub_of_Z (x y : int) : + (x - y)%sint63 = of_Z (to_Z x - to_Z y). +Proof. now rewrite <- of_Z_cmod, <- sub_spec, of_to_Z. Qed. + +Lemma mul_of_Z (x y : int) : + (x * y)%sint63 = of_Z (to_Z x * to_Z y). +Proof. now rewrite <- of_Z_cmod, <- mul_spec, of_to_Z. Qed. + +Lemma succ_of_Z (x : int) : + (succ x)%sint63 = of_Z (to_Z x + 1). +Proof. now rewrite <- of_Z_cmod, <- succ_spec, of_to_Z. Qed. + +Lemma pred_of_Z (x : int) : + (pred x)%sint63 = of_Z (to_Z x - 1). +Proof. now rewrite <- of_Z_cmod, <- pred_spec, of_to_Z. Qed. + +Lemma opp_of_Z (x : int) : + (- x)%sint63 = of_Z (- to_Z x). +Proof. now rewrite <- of_Z_cmod, <- opp_spec, of_to_Z. Qed. + +(** Comparison *) +Import Bool. + +Lemma eqbP x y : reflect (to_Z x = to_Z y) (x =? y)%sint63. +Proof. + apply iff_reflect; rewrite Int63.eqb_spec. + now split; [> apply to_Z_inj | apply f_equal]. +Qed. + +Lemma ltbP x y : reflect (to_Z x < to_Z y) (x <? y)%sint63. +Proof. now apply iff_reflect; symmetry; apply ltb_spec. Qed. + +Lemma lebP x y : reflect (to_Z x <= to_Z y) (x ≤? y)%sint63. +Proof. now apply iff_reflect; symmetry; apply leb_spec. Qed. + +(** ASR *) +Lemma asr_0 (i : int) : (0 >> i)%sint63 = 0%sint63. +Proof. now apply to_Z_inj; rewrite asr_spec. Qed. + +Lemma asr_0_r (i : int) : (i >> 0)%sint63 = i. +Proof. now apply to_Z_inj; rewrite asr_spec, Zdiv_1_r. Qed. + +Lemma asr_neg_r (i n : int) : to_Z n < 0 -> (i >> n)%sint63 = 0%sint63. +Proof. + intros ltn0. + apply to_Z_inj. + rewrite asr_spec, Z.pow_neg_r by assumption. + now rewrite Zdiv_0_r. +Qed. + +Lemma asr_1 (n : int) : (1 >> n)%sint63 = (n =? 0)%sint63. +Proof. + apply to_Z_inj; rewrite asr_spec. + case eqbP; [> now intros -> | intros neqn0]. + case (lebP 0 n). + - intros le0n. + apply Z.div_1_l; apply Z.pow_gt_1; [> easy |]. + rewrite to_Z_0 in *; lia. + - rewrite Z.nle_gt; intros ltn0. + now rewrite Z.pow_neg_r. +Qed. + +Notation asr := asr (only parsing). +Notation div := divs (only parsing). +Notation rem := mods (only parsing). +Notation ltb := ltsb (only parsing). +Notation leb := lesb (only parsing). +Notation compare := compares (only parsing). + +Module Export Sint63Notations. + Export Sint63NotationsInternalA. + Export Sint63NotationsInternalB. +End Sint63Notations. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 9788ad50dc..9540bc1075 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -68,10 +68,11 @@ Ltac pi := repeat f_equal ; apply proof_irrelevance. Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> `n = `m. Proof. + intros A P n m. destruct n as (x,p). destruct m as (x',p'). simpl. - split ; intros ; subst. + split ; intros H ; subst. - inversion H. reflexivity. @@ -92,7 +93,7 @@ Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B) (y : {y:A | y = x}), match_eq A B x fn = fn y. Proof. - intros. + intros A B x fn y. unfold match_eq. f_equal. destruct y. diff --git a/theories/Reals/Abstract/ConstructiveReals.v b/theories/Reals/Abstract/ConstructiveReals.v index 60fad8795a..5a599587d0 100644 --- a/theories/Reals/Abstract/ConstructiveReals.v +++ b/theories/Reals/Abstract/ConstructiveReals.v @@ -285,14 +285,14 @@ Lemma CRlt_trans : forall {R : ConstructiveReals} (x y z : CRcarrier R), Proof. intros. apply (CRlt_le_trans _ y _ H). apply CRlt_asym. exact H0. -Defined. +Qed. Lemma CRlt_trans_flip : forall {R : ConstructiveReals} (x y z : CRcarrier R), y < z -> x < y -> x < z. Proof. intros. apply (CRlt_le_trans _ y). exact H0. apply CRlt_asym. exact H. -Defined. +Qed. Lemma CReq_refl : forall {R : ConstructiveReals} (x : CRcarrier R), x == x. diff --git a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v index 53b5aca38c..6ed5845440 100644 --- a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v +++ b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v @@ -232,7 +232,7 @@ Proof. apply CRplus_lt_compat_l. apply (CRle_lt_trans _ (CR_of_Q R 0)). apply CRle_refl. apply CR_of_Q_lt. exact H. -Defined. +Qed. Lemma CRplus_neg_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q : Q), Qlt q 0 -> CRlt R (CRplus R x (CR_of_Q R q)) x. diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index 069a1292cd..9a00408de3 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -112,7 +112,7 @@ Proof. pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply H | apply H1 ]. -Defined. +Qed. Lemma Alembert_C2 : forall An:nat -> R, @@ -330,7 +330,7 @@ Proof. rewrite <- Rabs_Ropp; apply RRle_abs. rewrite double; pattern (Rabs (An n)) at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rabs_pos_lt; apply H. -Defined. +Qed. Lemma AlembertC3_step1 : forall (An:nat -> R) (x:R), @@ -374,7 +374,7 @@ Proof. [ assumption | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ]. intro; unfold Bn; apply prod_neq_R0; [ apply H0 | apply pow_nonzero; assumption ]. -Defined. +Qed. Lemma AlembertC3_step2 : forall (An:nat -> R) (x:R), x = 0 -> { l:R | Pser An x l }. @@ -405,7 +405,7 @@ Proof. cut (x <> 0). intro; apply AlembertC3_step1; assumption. red; intro; rewrite H1 in Hgt; elim (Rlt_irrefl _ Hgt). -Defined. +Qed. Lemma Alembert_C4 : forall (An:nat -> R) (k:R), diff --git a/theories/Reals/Cauchy/ConstructiveCauchyReals.v b/theories/Reals/Cauchy/ConstructiveCauchyReals.v index 8a11c155ce..4fb3846abc 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyReals.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyReals.v @@ -320,7 +320,6 @@ Proof. - contradiction. - exact Hxltz. Qed. -(* Todo: this was Defined. Why *) Lemma CReal_lt_le_trans : forall x y z : CReal, x < y -> y <= z -> x < z. @@ -330,7 +329,6 @@ Proof. - exact Hxltz. - contradiction. Qed. -(* Todo: this was Defined. Why *) Lemma CReal_le_trans : forall x y z : CReal, x <= y -> y <= z -> x <= z. @@ -347,7 +345,6 @@ Proof. apply (CReal_lt_le_trans _ y _ Hxlty). apply CRealLt_asym; exact Hyltz. Qed. -(* Todo: this was Defined. Why *) Lemma CRealEq_trans : forall x y z : CReal, CRealEq x y -> CRealEq y z -> CRealEq x z. diff --git a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v index a180e13444..bc45868244 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v @@ -733,13 +733,11 @@ Definition CReal_inv_pos (x : CReal) (Hxpos : 0 < x) : CReal := bound := CReal_inv_pos_bound x Hxpos |}. -(* ToDo: make this more obviously computing *) - Definition CReal_neg_lt_pos : forall x : CReal, x < 0 -> 0 < -x. Proof. intros x [n nmaj]. exists n. - apply (Qlt_le_trans _ _ _ nmaj). destruct x. simpl. - unfold Qminus. rewrite Qplus_0_l, Qplus_0_r. apply Qle_refl. + simpl in *. unfold CReal_opp_seq, Qminus. + abstract now rewrite Qplus_0_r, <- (Qplus_0_l (- seq x n)). Defined. Definition CReal_inv (x : CReal) (xnz : x # 0) : CReal diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v index 70d2861d17..c2b60e6478 100644 --- a/theories/Reals/Cauchy/ConstructiveRcomplete.v +++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v @@ -75,7 +75,7 @@ Proof. rewrite inject_Q_plus, (opp_inject_Q 2). ring_simplify. exact H. rewrite Qinv_plus_distr. reflexivity. -Defined. +Qed. (* ToDo: Move to ConstructiveCauchyAbs.v *) Lemma Qabs_Rabs : forall q : Q, @@ -688,21 +688,7 @@ Proof. exact (a i j H0 H1). exists l. intros p. destruct (cv p). exists x. exact c. -Defined. - -(* ToDO: Belongs into sumbool.v *) -Section connectives. - - Variables A B : Prop. - - Hypothesis H1 : {A} + {~A}. - Hypothesis H2 : {B} + {~B}. - - Definition sumbool_or_not_or : {A \/ B} + {~(A \/ B)}. - case H1; case H2; tauto. - Defined. - -End connectives. +Qed. Lemma Qnot_le_iff_lt: forall x y : Q, ~ (x <= y)%Q <-> (y < x)%Q. @@ -740,13 +726,11 @@ Proof. clear maj. right. exists n. apply H0. - clear H0 H. intro n. - apply sumbool_or_not_or. - + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq b n - seq a n)%Q). - * left; assumption. - * right; apply Qle_not_lt; assumption. - + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq d n - seq c n)%Q). - * left; assumption. - * right; apply Qle_not_lt; assumption. + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq b n - seq a n)%Q) as [H1|H1]. + + now left; left. + + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq d n - seq c n)%Q) as [H2|H2]. + * now left; right. + * now right; intros [H3|H3]; apply Qle_not_lt with (2 := H3). Qed. Definition CRealConstructive : ConstructiveReals diff --git a/theories/Reals/ClassicalDedekindReals.v b/theories/Reals/ClassicalDedekindReals.v index 500838ed26..0736b09761 100644 --- a/theories/Reals/ClassicalDedekindReals.v +++ b/theories/Reals/ClassicalDedekindReals.v @@ -233,17 +233,12 @@ Qed. (** *** Conversion from CReal to DReal *) -Definition DRealAbstr : CReal -> DReal. +Lemma DRealAbstr_aux : + forall x H, + isLowerCut (fun q : Q => + if sig_forall_dec (fun n : nat => seq x (- Z.of_nat n) <= q + 2 ^ (- Z.of_nat n)) (H q) + then true else false). Proof. - intro x. - assert (forall (q : Q) (n : nat), - {(fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n} + - {~ (fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n}). - { intros. destruct (Qlt_le_dec (q + (2^-Z.of_nat n)) (seq x (-Z.of_nat n))). - right. apply (Qlt_not_le _ _ q0). left. exact q0. } - - exists (fun q:Q => if sig_forall_dec (fun n:nat => Qle (seq x (-Z.of_nat n)) (q + (2^-Z.of_nat n))) (H q) - then true else false). repeat split. - intros. destruct (sig_forall_dec (fun n : nat => (seq x (-Z.of_nat n) <= q + (2^-Z.of_nat n))%Q) @@ -303,6 +298,20 @@ Proof. apply (Qmult_le_l _ _ 2) in q0. field_simplify in q0. apply (Qplus_le_l _ _ (-seq x (-Z.of_nat n))) in q0. ring_simplify in q0. contradiction. reflexivity. +Qed. + +Definition DRealAbstr : CReal -> DReal. +Proof. + intro x. + assert (forall (q : Q) (n : nat), + {(fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n} + + {~ (fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n}). + { intros. destruct (Qlt_le_dec (q + (2^-Z.of_nat n)) (seq x (-Z.of_nat n))). + right. apply (Qlt_not_le _ _ q0). left. exact q0. } + + exists (fun q:Q => if sig_forall_dec (fun n:nat => Qle (seq x (-Z.of_nat n)) (q + (2^-Z.of_nat n))) (H q) + then true else false). + apply DRealAbstr_aux. Defined. (** *** Conversion from DReal to CReal *) diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 6692119738..6107775003 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -170,7 +170,7 @@ Proof. reg. exists H5; symmetry ; reg; rewrite <- H3; rewrite <- H4; reflexivity. assumption. -Defined. +Qed. (**********) Lemma antiderivative_P1 : diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 7f5a859c81..2004f40f00 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -41,9 +41,13 @@ Proof. red; intro; rewrite H0 in H; elim (lt_irrefl _ H). Qed. -Lemma exist_exp0 : { l:R | exp_in 0 l }. +(* Value of [exp 0] *) +Lemma exp_0 : exp 0 = 1. Proof. - exists 1. + cut (exp_in 0 1). + cut (exp_in 0 (exp 0)). + apply uniqueness_sum. + exact (proj2_sig (exist_exp 0)). unfold exp_in; unfold infinite_sum; intros. exists 0%nat. intros; replace (sum_f_R0 (fun i:nat => / INR (fact i) * 0 ^ i) n) with 1. @@ -56,18 +60,6 @@ Proof. simpl. ring. unfold ge; apply le_O_n. -Defined. - -(* Value of [exp 0] *) -Lemma exp_0 : exp 0 = 1. -Proof. - cut (exp_in 0 (exp 0)). - cut (exp_in 0 1). - unfold exp_in; intros; eapply uniqueness_sum. - apply H0. - apply H. - exact (proj2_sig exist_exp0). - exact (proj2_sig (exist_exp 0)). Qed. (*****************************************) @@ -384,9 +376,14 @@ Proof. intros; ring. Qed. -Lemma exist_cos0 : { l:R | cos_in 0 l }. +(* Value of [cos 0] *) +Lemma cos_0 : cos 0 = 1. Proof. - exists 1. + cut (cos_in 0 1). + cut (cos_in 0 (cos 0)). + apply uniqueness_sum. + rewrite <- Rsqr_0 at 1. + exact (proj2_sig (exist_cos (Rsqr 0))). unfold cos_in; unfold infinite_sum; intros; exists 0%nat. intros. unfold R_dist. @@ -400,17 +397,4 @@ Proof. rewrite Rplus_0_r. apply Hrecn; unfold ge; apply le_O_n. simpl; ring. -Defined. - -(* Value of [cos 0] *) -Lemma cos_0 : cos 0 = 1. -Proof. - cut (cos_in 0 (cos 0)). - cut (cos_in 0 1). - unfold cos_in; intros; eapply uniqueness_sum. - apply H0. - apply H. - exact (proj2_sig exist_cos0). - assert (H := proj2_sig (exist_cos (Rsqr 0))); unfold cos; - pattern 0 at 1; replace 0 with (Rsqr 0); [ exact H | apply Rsqr_0 ]. Qed. diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 206eb606d2..422316d879 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -71,6 +71,7 @@ Section defs. (forall a l, Sorted l -> P l -> HdRel a l -> P (a :: l)) -> forall l:list A, Sorted l -> P l. Proof. + intros P ? ? l. induction l. firstorder using Sorted_inv. firstorder using Sorted_inv. Qed. @@ -78,7 +79,8 @@ Section defs. Proof. split; [induction 1 as [|a l [|]]| induction 1]; auto using Sorted, LocallySorted, HdRel. - inversion H1; subst; auto using LocallySorted. + match goal with H1 : HdRel a (_ :: _) |- _ => inversion H1 end. + subst; auto using LocallySorted. Qed. (** Strongly sorted: elements of the list are pairwise ordered *) @@ -90,7 +92,7 @@ Section defs. Lemma StronglySorted_inv : forall a l, StronglySorted (a :: l) -> StronglySorted l /\ Forall (R a) l. Proof. - intros; inversion H; auto. + intros a l H; inversion H; auto. Defined. Lemma StronglySorted_rect : @@ -99,7 +101,7 @@ Section defs. (forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) -> forall l, StronglySorted l -> P l. Proof. - induction l; firstorder using StronglySorted_inv. + intros P ? ? l; induction l; firstorder using StronglySorted_inv. Defined. Lemma StronglySorted_rec : @@ -120,7 +122,8 @@ Section defs. Lemma Sorted_extends : Transitive R -> forall a l, Sorted (a::l) -> Forall (R a) l. Proof. - intros. change match a :: l with [] => True | a :: l => Forall (R a) l end. + intros H a l H0. + change match a :: l with [] => True | a :: l => Forall (R a) l end. induction H0 as [|? ? ? ? H1]; [trivial|]. destruct H1; constructor; trivial. eapply Forall_impl; [|eassumption]. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 06b02ab211..37d30a282c 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -173,6 +173,14 @@ Proof. apply N_ascii_bounded. Qed. +Definition ltb (a b : ascii) : bool := + (N_of_ascii a <? N_of_ascii b)%N. + +Definition leb (a b : ascii) : bool := + (N_of_ascii a <=? N_of_ascii b)%N. + +Infix "<?" := ltb : char_scope. +Infix "<=?" := leb : char_scope. (** * Concrete syntax *) diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index c923b503a7..a49e21fa92 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -93,7 +93,7 @@ Module KeyDecidableType(D:DecidableType). Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. Proof. - intros; apply InA_eqA with p; auto using eqk_equiv. + intros p q m **; apply InA_eqA with p; auto using eqk_equiv. Qed. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). @@ -106,18 +106,18 @@ Module KeyDecidableType(D:DecidableType). Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. Proof. - firstorder. - exists x; auto. - induction H. - destruct y. - exists e; auto. - destruct IHInA as [e H0]. + intros k l; split; intros [y H]. + exists y; auto. + induction H as [a l eq|a l H IH]. + destruct a as [k' y']. + exists y'; auto. + destruct IH as [e H0]. exists e; auto. Qed. Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. Proof. - intros; unfold MapsTo in *; apply InA_eqA with (x,e); auto using eqke_equiv. + intros l x y e **; unfold MapsTo in *; apply InA_eqA with (x,e); auto using eqke_equiv. Qed. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. @@ -127,21 +127,21 @@ Module KeyDecidableType(D:DecidableType). Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. Proof. - inversion 1. - inversion_clear H0; eauto. + inversion 1 as [? H0]. + inversion_clear H0 as [? ? H1|]; eauto. destruct H1; simpl in *; intuition. Qed. Lemma In_inv_2 : forall k k' e e' l, InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. Proof. - inversion_clear 1; compute in H0; intuition. + inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition. Qed. Lemma In_inv_3 : forall x x' l, InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. Proof. - inversion_clear 1; compute in H0; intuition. + inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition. Qed. End Elt. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index dc7a48cd6b..7bc9f97e2b 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -65,7 +65,7 @@ Module MOT_to_OT (Import O : MiniOrderedType) <: OrderedType. Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. Proof with auto with ordered_type. - intros; elim (compare x y); intro H; [ right | left | right ]... + intros x y; elim (compare x y); intro H; [ right | left | right ]... assert (~ eq y x)... Defined. @@ -83,7 +83,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_antirefl : forall x, ~ lt x x. Proof. - intros; intro; absurd (eq x x); auto with ordered_type. + intros x; intro; absurd (eq x x); auto with ordered_type. Qed. Instance lt_strorder : StrictOrder lt. @@ -91,14 +91,14 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z. Proof with auto with ordered_type. - intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. + intros x y z H ?; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. elim (lt_not_eq H); apply eq_trans with z... elim (lt_not_eq (lt_trans Hlt H))... Qed. Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z. Proof with auto with ordered_type. - intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. + intros x y z H H0; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. elim (lt_not_eq H0); apply eq_trans with x... elim (lt_not_eq (lt_trans H0 Hlt))... Qed. @@ -111,7 +111,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Qed. Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x. - Proof. intros; destruct (compare x y); auto. Qed. + Proof. intros x y; destruct (compare x y); auto. Qed. Module TO. Definition t := t. @@ -157,7 +157,7 @@ Module OrderedTypeFacts (Import O: OrderedType). forall x y : t, eq x y -> exists H : eq x y, compare x y = EQ H. Proof. - intros; case (compare x y); intros H'; try (exfalso; order). + intros x y H; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. Qed. @@ -165,7 +165,7 @@ Module OrderedTypeFacts (Import O: OrderedType). forall x y : t, lt x y -> exists H : lt x y, compare x y = LT H. Proof. - intros; case (compare x y); intros H'; try (exfalso; order). + intros x y H; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. Qed. @@ -173,7 +173,7 @@ Module OrderedTypeFacts (Import O: OrderedType). forall x y : t, lt y x -> exists H : lt y x, compare x y = GT H. Proof. - intros; case (compare x y); intros H'; try (exfalso; order). + intros x y H; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. Qed. @@ -203,7 +203,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}. Proof. - intros; elim (compare x y); [ left | right | right ]; auto with ordered_type. + intros x y; elim (compare x y); [ left | right | right ]; auto with ordered_type. Defined. Definition eqb x y : bool := if eq_dec x y then true else false. @@ -211,7 +211,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma eqb_alt : forall x y, eqb x y = match compare x y with EQ _ => true | _ => false end. Proof. - unfold eqb; intros; destruct (eq_dec x y); elim_comp; auto. + unfold eqb; intros x y; destruct (eq_dec x y); elim_comp; auto. Qed. (* Specialization of results about lists modulo. *) @@ -327,7 +327,7 @@ Module KeyOrderedType(O:OrderedType). Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. Proof. unfold eqke, ltk; intuition; simpl in *; subst. - exact (lt_not_eq H H1). + match goal with H : lt _ _, H1 : eq _ _ |- _ => exact (lt_not_eq H H1) end. Qed. #[local] @@ -398,18 +398,18 @@ Module KeyOrderedType(O:OrderedType). Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. Proof with auto with ordered_type. - firstorder. - exists x... - induction H. - destruct y. - exists e... - destruct IHInA as [e H0]. + intros k l; split; intros [y H]. + exists y... + induction H as [a l eq|a l H IH]. + destruct a as [k' y']. + exists y'... + destruct IH as [e H0]. exists e... Qed. Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. Proof. - intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *. + intros l x y e **; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *. Qed. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. @@ -437,7 +437,7 @@ Module KeyOrderedType(O:OrderedType). Lemma Sort_Inf_NotIn : forall l k e, Sort l -> Inf (k,e) l -> ~In k l. Proof. - intros; red; intros. + intros l k e H H0; red; intros H1. destruct H1 as [e' H2]. elim (@ltk_not_eqk (k,e) (k,e')). eapply Sort_Inf_In; eauto with ordered_type. @@ -457,34 +457,34 @@ Module KeyOrderedType(O:OrderedType). Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) -> ltk e e' \/ eqk e e'. Proof. - inversion_clear 2; auto with ordered_type. + intros l; inversion_clear 2; auto with ordered_type. left; apply Sort_In_cons_1 with l; auto. Qed. Lemma Sort_In_cons_3 : forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k. Proof. - inversion_clear 1; red; intros. + inversion_clear 1 as [|? ? H0 H1]; red; intros H H2. destruct (Sort_Inf_NotIn H0 H1 (In_eq H2 H)). Qed. Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. Proof. - inversion 1. - inversion_clear H0; eauto with ordered_type. + inversion 1 as [? H0]. + inversion_clear H0 as [? ? H1|]; eauto with ordered_type. destruct H1; simpl in *; intuition. Qed. Lemma In_inv_2 : forall k k' e e' l, InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. Proof. - inversion_clear 1; compute in H0; intuition. + inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition. Qed. Lemma In_inv_3 : forall x x' l, InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. Proof. - inversion_clear 1; compute in H0; intuition. + inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition. Qed. End Elt. diff --git a/theories/dune b/theories/dune index 18e000cfe1..1cd3d8c119 100644 --- a/theories/dune +++ b/theories/dune @@ -1,6 +1,6 @@ (coq.theory (name Coq) - (package coq) + (package coq-stdlib) (synopsis "Coq's Standard Library") (flags -q) ; (mode native) @@ -8,30 +8,29 @@ ; (per_file ; (Init/*.v -> -boot)) (libraries - coq.plugins.ltac - coq.plugins.tauto + coq-core.plugins.ltac + coq-core.plugins.tauto - coq.plugins.cc - coq.plugins.firstorder + coq-core.plugins.cc + coq-core.plugins.firstorder - coq.plugins.number_string_notation - coq.plugins.int63_syntax - coq.plugins.float_syntax + coq-core.plugins.number_string_notation + coq-core.plugins.float_syntax - coq.plugins.btauto - coq.plugins.rtauto + coq-core.plugins.btauto + coq-core.plugins.rtauto - coq.plugins.ring - coq.plugins.nsatz - coq.plugins.omega + coq-core.plugins.ring + coq-core.plugins.nsatz + coq-core.plugins.omega - coq.plugins.zify - coq.plugins.micromega + coq-core.plugins.zify + coq-core.plugins.micromega - coq.plugins.funind + coq-core.plugins.funind - coq.plugins.ssreflect - coq.plugins.ssrsearch - coq.plugins.derive)) + coq-core.plugins.ssreflect + coq-core.plugins.ssrsearch + coq-core.plugins.derive)) (include_subdirs qualified) diff --git a/theories/extraction/ExtrOCamlInt63.v b/theories/extraction/ExtrOCamlInt63.v index 7f7b4af98d..1949a1a9d8 100644 --- a/theories/extraction/ExtrOCamlInt63.v +++ b/theories/extraction/ExtrOCamlInt63.v @@ -10,7 +10,7 @@ (** Extraction to OCaml of native 63-bit machine integers. *) -From Coq Require Int63 Extraction. +From Coq Require Int63 Sint63 Extraction. (** Basic data types used by some primitive operators. *) @@ -26,6 +26,7 @@ Extraction Inline Int63.int. Extract Constant Int63.lsl => "Uint63.l_sl". Extract Constant Int63.lsr => "Uint63.l_sr". +Extract Constant Sint63.asr => "Uint63.a_sr". Extract Constant Int63.land => "Uint63.l_and". Extract Constant Int63.lor => "Uint63.l_or". Extract Constant Int63.lxor => "Uint63.l_xor". @@ -36,10 +37,15 @@ Extract Constant Int63.mul => "Uint63.mul". Extract Constant Int63.mulc => "Uint63.mulc". Extract Constant Int63.div => "Uint63.div". Extract Constant Int63.mod => "Uint63.rem". +Extract Constant Sint63.div => "Uint63.divs". +Extract Constant Sint63.rem => "Uint63.rems". + Extract Constant Int63.eqb => "Uint63.equal". Extract Constant Int63.ltb => "Uint63.lt". Extract Constant Int63.leb => "Uint63.le". +Extract Constant Sint63.ltb => "Uint63.lts". +Extract Constant Sint63.leb => "Uint63.les". Extract Constant Int63.addc => "Uint63.addc". Extract Constant Int63.addcarryc => "Uint63.addcarryc". @@ -51,6 +57,7 @@ Extract Constant Int63.diveucl_21 => "Uint63.div21". Extract Constant Int63.addmuldiv => "Uint63.addmuldiv". Extract Constant Int63.compare => "Uint63.compare". +Extract Constant Sint63.compare => "Uint63.compares". Extract Constant Int63.head0 => "Uint63.head0". Extract Constant Int63.tail0 => "Uint63.tail0". |