Commit 9669a549 by MARCHE Claude

### update theory int.Exponentiation and its Coq realization

parent cfa13365
 ... ... @@ -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. ... ... @@ -109,19 +107,40 @@ now rewrite Power_1. 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_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_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.
 ... ... @@ -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 *) ... ...
 ... ... @@ -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 *) ... ...
 ... ... @@ -265,7 +265,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 ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!