diff --git a/lib/coq/int/Exponentiation.v b/lib/coq/int/Exponentiation.v index 042254cbf893243d41b83c044ad769e21dd7aae1..2f589a3e84388610781ce9794f30a9d4e49ae06a 100644 --- a/lib/coq/int/Exponentiation.v +++ b/lib/coq/int/Exponentiation.v @@ -38,9 +38,6 @@ Hypothesis Unit_def_l : forall (x:t), ((infix_as one x) = x). (* Why3 goal *) Hypothesis Unit_def_r : forall (x:t), ((infix_as x one) = x). -(* Why3 goal *) -Hypothesis Comm : forall (x:t) (y:t), ((infix_as x y) = (infix_as y x)). - (* Why3 goal *) Definition power: t -> Z -> t. intros x n. @@ -66,6 +63,7 @@ Qed. (* Why3 goal *) Lemma Power_s_alt : forall (x:t) (n:Z), (0%Z < n)%Z -> ((power x n) = (infix_as x (power x (n - 1%Z)%Z))). +Proof. intros x n h1. rewrite <- Power_s; auto with zarith. f_equal; omega. @@ -101,26 +99,47 @@ revert m Hm. apply natlike_ind. now rewrite Zmult_0_r, 2!Power_0. intros m Hm IHm. -replace (n * Zsucc m)%Z with (n * m + n)%Z by ring. +replace (n * Zsucc m)%Z with (n + n * m)%Z by ring. rewrite Power_sum by auto with zarith. rewrite IHm. -now rewrite Comm, <- Power_s. +now rewrite <- Power_s. +Qed. + +(* Why3 goal *) +Lemma Power_comm1 : forall (x:t) (y:t), ((infix_as x y) = (infix_as y x)) -> + forall (n:Z), (0%Z <= n)%Z -> ((infix_as (power x n) y) = (infix_as y + (power x n))). +Proof. +intros x y comm. +apply natlike_ind. +now rewrite Power_0, Unit_def_r, Unit_def_l. +intros n Hn IHn. +unfold Zsucc. +rewrite (Power_s _ _ Hn). +rewrite Assoc. +rewrite IHn. +rewrite <- Assoc. +rewrite <- Assoc. +now rewrite comm. Qed. (* Why3 goal *) -Lemma Power_mult2 : forall (x:t) (y:t) (n:Z), (0%Z <= n)%Z -> - ((power (infix_as x y) n) = (infix_as (power x n) (power y n))). +Lemma Power_comm2 : forall (x:t) (y:t), ((infix_as x y) = (infix_as y x)) -> + forall (n:Z), (0%Z <= n)%Z -> ((power (infix_as x y) + n) = (infix_as (power x n) (power y n))). Proof. -intros x y. +intros x y comm. apply natlike_ind. -apply sym_eq. rewrite 3!Power_0. -apply Unit_def_r. +now rewrite Unit_def_r. intros n Hn IHn. unfold Zsucc. rewrite 3!(Power_s _ _ Hn). rewrite IHn. -now rewrite Assoc, <- (Assoc y), (Comm y), 2!Assoc. +rewrite <- Assoc. +rewrite (Assoc x). +rewrite <- (Power_comm1 _ _ comm _ Hn). +now rewrite <- 2!Assoc. Qed. End Exponentiation. diff --git a/lib/coq/int/Power.v b/lib/coq/int/Power.v index 11f2185fa86642786a3fffb9fa986a41a8121545..65ef76c2f4f680da0136d9609e90f6bfbf78d87b 100644 --- a/lib/coq/int/Power.v +++ b/lib/coq/int/Power.v @@ -82,12 +82,21 @@ apply Power_mult ; auto with zarith. Qed. (* Why3 goal *) -Lemma Power_mult2 : forall (x:Z) (y:Z) (n:Z), (0%Z <= n)%Z -> - ((power (x * y)%Z n) = ((power x n) * (power y n))%Z). +Lemma Power_comm1 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z) -> + forall (n:Z), (0%Z <= n)%Z -> (((power x n) * y)%Z = (y * (power x n))%Z). Proof. -intros x y n Hn. +intros x y h1 n h2. +auto with zarith. +Qed. + +(* Why3 goal *) +Lemma Power_comm2 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z) -> + forall (n:Z), (0%Z <= n)%Z -> ((power (x * y)%Z n) = ((power x + n) * (power y n))%Z). +Proof. +intros x y h1 n h2. rewrite 3!power_is_exponentiation ; auto with zarith. -apply Power_mult2 ; auto with zarith. +apply Power_comm2 ; auto with zarith. Qed. (* Why3 goal *) diff --git a/lib/coq/map/Map.v b/lib/coq/map/Map.v index c362587c1a9a45531c0f73038cb9931440388cf3..27060930b80bcaa1e76793814ebf1acc50f9f782 100644 --- a/lib/coq/map/Map.v +++ b/lib/coq/map/Map.v @@ -14,11 +14,6 @@ Require Import BuiltIn. Require BuiltIn. -(* This file is generated by Why3's Coq-realize driver *) -(* Beware! Only edit allowed sections below *) -Require Import BuiltIn. -Require BuiltIn. - Require Import ClassicalEpsilon. Inductive _map (a b:Type) := diff --git a/lib/coq/real/PowerInt.v b/lib/coq/real/PowerInt.v index c9c9a85e6961e8c417c79941b163adbfe8bc8bd2..cbe145e75b23e5a95f51466102869a81ab2ec2a4 100644 --- a/lib/coq/real/PowerInt.v +++ b/lib/coq/real/PowerInt.v @@ -88,12 +88,21 @@ apply Power_mult ; auto with real. Qed. (* Why3 goal *) -Lemma Power_mult2 : forall (x:R) (y:R) (n:Z), (0%Z <= n)%Z -> +Lemma Power_comm1 : forall (x:R) (y:R), ((x * y)%R = (y * x)%R) -> + forall (n:Z), (0%Z <= n)%Z -> + (((Reals.Rfunctions.powerRZ x n) * y)%R = (y * (Reals.Rfunctions.powerRZ x n))%R). +intros x y h1 n h2. +apply Rmult_comm. +Qed. + +(* Why3 goal *) +Lemma Power_comm2 : forall (x:R) (y:R), ((x * y)%R = (y * x)%R) -> + forall (n:Z), (0%Z <= n)%Z -> ((Reals.Rfunctions.powerRZ (x * y)%R n) = ((Reals.Rfunctions.powerRZ x n) * (Reals.Rfunctions.powerRZ y n))%R). Proof. -intros x y n h1. +intros x y h1 n h2. rewrite 3!power_is_exponentiation by auto with zarith. -apply Power_mult2 ; auto with real. +apply Power_comm2 ; auto with real. Qed. (* Why3 goal *) diff --git a/theories/int.why b/theories/int.why index 047a4c3fdc2db46aee5c691a408d722232f8288d..724b03cc7a6446e2843d9a20a7fc137d9d56c487 100644 --- a/theories/int.why +++ b/theories/int.why @@ -226,7 +226,12 @@ theory Exponentiation lemma Power_mult : forall x:t, n m : int. 0 <= n -> 0 <= m -> power x (Int.( * ) n m) = power (power x n) m - lemma Power_mult2 : forall x y: t, n: int. 0 <= n -> + lemma Power_comm1 : forall x y: t. x * y = y * x -> + forall n:int. 0 <= n -> + power x n * y = y * power x n + + lemma Power_comm2 : forall x y: t. x * y = y * x -> + forall n:int. 0 <= n -> power (x * y) n = power x n * power y n (* TODO