From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/omega/PreOmega.v | 204 +++++++++++++++++++++++------------------------ 1 file changed, 102 insertions(+), 102 deletions(-) (limited to 'plugins/omega/PreOmega.v') diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 47e22a97f..a5a085a99 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -5,16 +5,16 @@ Open Local Scope Z_scope. (** * zify: the Z-ification tactic *) -(* This tactic searches for nat and N and positive elements in the goal and - translates everything into Z. It is meant as a pre-processor for +(* This tactic searches for nat and N and positive elements in the goal and + translates everything into Z. It is meant as a pre-processor for (r)omega; for instance a positivity hypothesis is added whenever - a multiplication is encountered - an atom is encountered (that is a variable or an unknown construct) Recognized relations (can be handled as deeply as allowed by setoid rewrite): - { eq, le, lt, ge, gt } on { Z, positive, N, nat } - - Recognized operations: + + Recognized operations: - on Z: Zmin, Zmax, Zabs, Zsgn are translated in term of <= < = - on nat: + * - S O pred min max nat_of_P nat_of_N Zabs_nat - on positive: Zneg Zpos xI xO xH + * - Psucc Ppred Pmin Pmax P_of_succ_nat @@ -26,31 +26,31 @@ Open Local Scope Z_scope. (** I) translation of Zmax, Zmin, Zabs, Zsgn into recognized equations *) -Ltac zify_unop_core t thm a := +Ltac zify_unop_core t thm a := (* Let's introduce the specification theorem for t *) - let H:= fresh "H" in assert (H:=thm a); + let H:= fresh "H" in assert (H:=thm a); (* Then we replace (t a) everywhere with a fresh variable *) let z := fresh "z" in set (z:=t a) in *; clearbody z. -Ltac zify_unop_var_or_term t thm a := +Ltac zify_unop_var_or_term t thm a := (* If a is a variable, no need for aliasing *) - let za := fresh "z" in + let za := fresh "z" in (rename a into za; rename za into a; zify_unop_core t thm a) || (* Otherwise, a is a complex term: we alias it. *) (remember a as za; zify_unop_core t thm za). -Ltac zify_unop t thm a := +Ltac zify_unop t thm a := (* if a is a scalar, we can simply reduce the unop *) - let isz := isZcst a in - match isz with + let isz := isZcst a in + match isz with | true => simpl (t a) in * | _ => zify_unop_var_or_term t thm a end. -Ltac zify_unop_nored t thm a := +Ltac zify_unop_nored t thm a := (* in this version, we don't try to reduce the unop (that can be (Zplus x)) *) - let isz := isZcst a in - match isz with + let isz := isZcst a in + match isz with | true => zify_unop_core t thm a | _ => zify_unop_var_or_term t thm a end. @@ -58,20 +58,20 @@ Ltac zify_unop_nored t thm a := Ltac zify_binop t thm a b:= (* works as zify_unop, except that we should be careful when dealing with b, since it can be equal to a *) - let isza := isZcst a in - match isza with + let isza := isZcst a in + match isza with | true => zify_unop (t a) (thm a) b - | _ => - let za := fresh "z" in + | _ => + let za := fresh "z" in (rename a into za; rename za into a; zify_unop_nored (t a) (thm a) b) || - (remember a as za; match goal with + (remember a as za; match goal with | H : za = b |- _ => zify_unop_nored (t za) (thm za) za | _ => zify_unop_nored (t za) (thm za) b end) end. -Ltac zify_op_1 := - match goal with +Ltac zify_op_1 := + match goal with | |- context [ Zmax ?a ?b ] => zify_binop Zmax Zmax_spec a b | H : context [ Zmax ?a ?b ] |- _ => zify_binop Zmax Zmax_spec a b | |- context [ Zmin ?a ?b ] => zify_binop Zmin Zmin_spec a b @@ -93,13 +93,13 @@ Ltac zify_op := repeat zify_op_1. Definition Z_of_nat' := Z_of_nat. -Ltac hide_Z_of_nat t := - let z := fresh "z" in set (z:=Z_of_nat t) in *; - change Z_of_nat with Z_of_nat' in z; +Ltac hide_Z_of_nat t := + let z := fresh "z" in set (z:=Z_of_nat t) in *; + change Z_of_nat with Z_of_nat' in z; unfold z in *; clear z. -Ltac zify_nat_rel := - match goal with +Ltac zify_nat_rel := + match goal with (* I: equalities *) | H : (@eq nat ?a ?b) |- _ => generalize (inj_eq _ _ H); clear H; intro H | |- (@eq nat ?a ?b) => apply (inj_eq_rev a b) @@ -127,8 +127,8 @@ Ltac zify_nat_rel := | |- context [ ge ?a ?b ] => rewrite (inj_ge_iff a b) end. -Ltac zify_nat_op := - match goal with +Ltac zify_nat_op := + match goal with (* misc type conversions: positive/N/Z to nat *) | H : context [ Z_of_nat (nat_of_P ?a) ] |- _ => rewrite <- (Zpos_eq_Z_of_nat_o_nat_of_P a) in H | |- context [ Z_of_nat (nat_of_P ?a) ] => rewrite <- (Zpos_eq_Z_of_nat_o_nat_of_P a) @@ -158,11 +158,11 @@ Ltac zify_nat_op := | |- context [ Z_of_nat (pred ?a) ] => rewrite (pred_of_minus a) (* mult -> Zmult and a positivity hypothesis *) - | H : context [ Z_of_nat (mult ?a ?b) ] |- _ => - let H:= fresh "H" in + | H : context [ Z_of_nat (mult ?a ?b) ] |- _ => + let H:= fresh "H" in assert (H:=Zle_0_nat (mult a b)); rewrite (inj_mult a b) in * - | |- context [ Z_of_nat (mult ?a ?b) ] => - let H:= fresh "H" in + | |- context [ Z_of_nat (mult ?a ?b) ] => + let H:= fresh "H" in assert (H:=Zle_0_nat (mult a b)); rewrite (inj_mult a b) in * (* O -> Z0 *) @@ -170,29 +170,29 @@ Ltac zify_nat_op := | |- context [ Z_of_nat O ] => simpl (Z_of_nat O) (* S -> number or Zsucc *) - | H : context [ Z_of_nat (S ?a) ] |- _ => - let isnat := isnatcst a in - match isnat with + | H : context [ Z_of_nat (S ?a) ] |- _ => + let isnat := isnatcst a in + match isnat with | true => simpl (Z_of_nat (S a)) in H | _ => rewrite (inj_S a) in H end - | |- context [ Z_of_nat (S ?a) ] => - let isnat := isnatcst a in - match isnat with + | |- context [ Z_of_nat (S ?a) ] => + let isnat := isnatcst a in + match isnat with | true => simpl (Z_of_nat (S a)) | _ => rewrite (inj_S a) end - (* atoms of type nat : we add a positivity condition (if not already there) *) - | H : context [ Z_of_nat ?a ] |- _ => - match goal with + (* atoms of type nat : we add a positivity condition (if not already there) *) + | H : context [ Z_of_nat ?a ] |- _ => + match goal with | H' : 0 <= Z_of_nat a |- _ => hide_Z_of_nat a | H' : 0 <= Z_of_nat' a |- _ => fail | _ => let H:= fresh "H" in assert (H:=Zle_0_nat a); hide_Z_of_nat a end - | |- context [ Z_of_nat ?a ] => - match goal with + | |- context [ Z_of_nat ?a ] => + match goal with | H' : 0 <= Z_of_nat a |- _ => hide_Z_of_nat a | H' : 0 <= Z_of_nat' a |- _ => fail | _ => let H:= fresh "H" in @@ -205,18 +205,18 @@ Ltac zify_nat := repeat zify_nat_rel; repeat zify_nat_op; unfold Z_of_nat' in *. -(* III) conversion from positive to Z *) +(* III) conversion from positive to Z *) Definition Zpos' := Zpos. Definition Zneg' := Zneg. -Ltac hide_Zpos t := - let z := fresh "z" in set (z:=Zpos t) in *; - change Zpos with Zpos' in z; +Ltac hide_Zpos t := + let z := fresh "z" in set (z:=Zpos t) in *; + change Zpos with Zpos' in z; unfold z in *; clear z. -Ltac zify_positive_rel := - match goal with +Ltac zify_positive_rel := + match goal with (* I: equalities *) | H : (@eq positive ?a ?b) |- _ => generalize (Zpos_eq _ _ H); clear H; intro H | |- (@eq positive ?a ?b) => apply (Zpos_eq_rev a b) @@ -236,18 +236,18 @@ Ltac zify_positive_rel := | |- context [ (?a>=?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b) end. -Ltac zify_positive_op := - match goal with +Ltac zify_positive_op := + match goal with (* Zneg -> -Zpos (except for numbers) *) - | H : context [ Zneg ?a ] |- _ => - let isp := isPcst a in - match isp with + | H : context [ Zneg ?a ] |- _ => + let isp := isPcst a in + match isp with | true => change (Zneg a) with (Zneg' a) in H | _ => change (Zneg a) with (- Zpos a) in H end - | |- context [ Zneg ?a ] => - let isp := isPcst a in - match isp with + | |- context [ Zneg ?a ] => + let isp := isPcst a in + match isp with | true => change (Zneg a) with (Zneg' a) | _ => change (Zneg a) with (- Zpos a) end @@ -272,45 +272,45 @@ Ltac zify_positive_op := | H : context [ Zpos (Pminus ?a ?b) ] |- _ => rewrite (Zpos_minus a b) in H | |- context [ Zpos (Pminus ?a ?b) ] => rewrite (Zpos_minus a b) - (* Psucc -> Zsucc *) + (* Psucc -> Zsucc *) | H : context [ Zpos (Psucc ?a) ] |- _ => rewrite (Zpos_succ_morphism a) in H | |- context [ Zpos (Psucc ?a) ] => rewrite (Zpos_succ_morphism a) (* Ppred -> Pminus ... -1 -> Zmax 1 (Zminus ... - 1) *) | H : context [ Zpos (Ppred ?a) ] |- _ => rewrite (Ppred_minus a) in H | |- context [ Zpos (Ppred ?a) ] => rewrite (Ppred_minus a) - + (* Pmult -> Zmult and a positivity hypothesis *) - | H : context [ Zpos (Pmult ?a ?b) ] |- _ => - let H:= fresh "H" in + | H : context [ Zpos (Pmult ?a ?b) ] |- _ => + let H:= fresh "H" in assert (H:=Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in * - | |- context [ Zpos (Pmult ?a ?b) ] => - let H:= fresh "H" in + | |- context [ Zpos (Pmult ?a ?b) ] => + let H:= fresh "H" in assert (H:=Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in * (* xO *) - | H : context [ Zpos (xO ?a) ] |- _ => - let isp := isPcst a in - match isp with + | H : context [ Zpos (xO ?a) ] |- _ => + let isp := isPcst a in + match isp with | true => change (Zpos (xO a)) with (Zpos' (xO a)) in H | _ => rewrite (Zpos_xO a) in H end - | |- context [ Zpos (xO ?a) ] => - let isp := isPcst a in - match isp with + | |- context [ Zpos (xO ?a) ] => + let isp := isPcst a in + match isp with | true => change (Zpos (xO a)) with (Zpos' (xO a)) | _ => rewrite (Zpos_xO a) end - (* xI *) - | H : context [ Zpos (xI ?a) ] |- _ => - let isp := isPcst a in - match isp with + (* xI *) + | H : context [ Zpos (xI ?a) ] |- _ => + let isp := isPcst a in + match isp with | true => change (Zpos (xI a)) with (Zpos' (xI a)) in H | _ => rewrite (Zpos_xI a) in H end - | |- context [ Zpos (xI ?a) ] => - let isp := isPcst a in - match isp with + | |- context [ Zpos (xI ?a) ] => + let isp := isPcst a in + match isp with | true => change (Zpos (xI a)) with (Zpos' (xI a)) | _ => rewrite (Zpos_xI a) end @@ -320,38 +320,38 @@ Ltac zify_positive_op := | |- context [ Zpos xH ] => hide_Zpos xH (* atoms of type positive : we add a positivity condition (if not already there) *) - | H : context [ Zpos ?a ] |- _ => - match goal with + | H : context [ Zpos ?a ] |- _ => + match goal with | H' : Zpos a > 0 |- _ => hide_Zpos a | H' : Zpos' a > 0 |- _ => fail | _ => let H:= fresh "H" in assert (H:=Zgt_pos_0 a); hide_Zpos a end - | |- context [ Zpos ?a ] => - match goal with + | |- context [ Zpos ?a ] => + match goal with | H' : Zpos a > 0 |- _ => hide_Zpos a | H' : Zpos' a > 0 |- _ => fail | _ => let H:= fresh "H" in assert (H:=Zgt_pos_0 a); hide_Zpos a end end. -Ltac zify_positive := +Ltac zify_positive := repeat zify_positive_rel; repeat zify_positive_op; unfold Zpos',Zneg' in *. -(* IV) conversion from N to Z *) +(* IV) conversion from N to Z *) Definition Z_of_N' := Z_of_N. -Ltac hide_Z_of_N t := - let z := fresh "z" in set (z:=Z_of_N t) in *; - change Z_of_N with Z_of_N' in z; +Ltac hide_Z_of_N t := + let z := fresh "z" in set (z:=Z_of_N t) in *; + change Z_of_N with Z_of_N' in z; unfold z in *; clear z. -Ltac zify_N_rel := - match goal with +Ltac zify_N_rel := + match goal with (* I: equalities *) | H : (@eq N ?a ?b) |- _ => generalize (Z_of_N_eq _ _ H); clear H; intro H | |- (@eq N ?a ?b) => apply (Z_of_N_eq_rev a b) @@ -378,9 +378,9 @@ Ltac zify_N_rel := | H : context [ (?a>=?b)%N ] |- _ => rewrite (Z_of_N_ge_iff a b) in H | |- context [ (?a>=?b)%N ] => rewrite (Z_of_N_ge_iff a b) end. - -Ltac zify_N_op := - match goal with + +Ltac zify_N_op := + match goal with (* misc type conversions: nat to positive *) | H : context [ Z_of_N (N_of_nat ?a) ] |- _ => rewrite (Z_of_N_of_nat a) in H | |- context [ Z_of_N (N_of_nat ?a) ] => rewrite (Z_of_N_of_nat a) @@ -407,27 +407,27 @@ Ltac zify_N_op := | H : context [ Z_of_N (Nminus ?a ?b) ] |- _ => rewrite (Z_of_N_minus a b) in H | |- context [ Z_of_N (Nminus ?a ?b) ] => rewrite (Z_of_N_minus a b) - (* Nsucc -> Zsucc *) + (* Nsucc -> Zsucc *) | H : context [ Z_of_N (Nsucc ?a) ] |- _ => rewrite (Z_of_N_succ a) in H | |- context [ Z_of_N (Nsucc ?a) ] => rewrite (Z_of_N_succ a) - + (* Nmult -> Zmult and a positivity hypothesis *) - | H : context [ Z_of_N (Nmult ?a ?b) ] |- _ => - let H:= fresh "H" in + | H : context [ Z_of_N (Nmult ?a ?b) ] |- _ => + let H:= fresh "H" in assert (H:=Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in * - | |- context [ Z_of_N (Nmult ?a ?b) ] => - let H:= fresh "H" in + | |- context [ Z_of_N (Nmult ?a ?b) ] => + let H:= fresh "H" in assert (H:=Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in * - (* atoms of type N : we add a positivity condition (if not already there) *) - | H : context [ Z_of_N ?a ] |- _ => - match goal with + (* atoms of type N : we add a positivity condition (if not already there) *) + | H : context [ Z_of_N ?a ] |- _ => + match goal with | H' : 0 <= Z_of_N a |- _ => hide_Z_of_N a | H' : 0 <= Z_of_N' a |- _ => fail | _ => let H:= fresh "H" in assert (H:=Z_of_N_le_0 a); hide_Z_of_N a end - | |- context [ Z_of_N ?a ] => - match goal with + | |- context [ Z_of_N ?a ] => + match goal with | H' : 0 <= Z_of_N a |- _ => hide_Z_of_N a | H' : 0 <= Z_of_N' a |- _ => fail | _ => let H:= fresh "H" in assert (H:=Z_of_N_le_0 a); hide_Z_of_N a @@ -440,6 +440,6 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. (** The complete Z-ification tactic *) -Ltac zify := +Ltac zify := repeat progress (zify_nat; zify_positive; zify_N); zify_op. -- cgit v1.2.3