Merge pull request #30 from inQWIRE/bugfix

Fixed compilation for QuantumLib on 8.12 through 8.16
inQWIRE · Jan 28, 2023 · 09844a6 · 09844a6
2 parents 3c4904f + b9d3608
commit 09844a6
Show file tree

Hide file tree

Showing 9 changed files with 86 additions and 65 deletions.
diff --git a/Complex.v b/Complex.v
@@ -113,29 +113,29 @@ Infix "^" := Cpow : C_scope.
 
 (** * Showing that C is a field, and a vector space over itself *)
 
-#[export] Program Instance C_is_monoid : Monoid C := 
+Global Program Instance C_is_monoid : Monoid C := 
   { Gzero := C0
   ; Gplus := Cplus
   }.
 Solve All Obligations with program_simpl; try lca.
 
-#[export] Program Instance C_is_group : Group C :=
+Global Program Instance C_is_group : Group C :=
   { Gopp := Copp }.
 Solve All Obligations with program_simpl; try lca.
 
-#[export] Program Instance C_is_comm_group : Comm_Group C.
+Global Program Instance C_is_comm_group : Comm_Group C.
 Solve All Obligations with program_simpl; lca. 
 
-#[export] Program Instance C_is_ring : Ring C :=
+Global Program Instance C_is_ring : Ring C :=
   { Gone := C1
   ; Gmult := Cmult
   }.
 Solve All Obligations with program_simpl; try lca; apply Ceq_dec. 
 
-#[export] Program Instance C_is_comm_ring : Comm_Ring C.
+Global Program Instance C_is_comm_ring : Comm_Ring C.
 Solve All Obligations with program_simpl; lca. 
 
-#[export] Program Instance C_is_field : Field C :=
+Global Program Instance C_is_field : Field C :=
   { Ginv := Cinv }.
 Next Obligation.
   assert (H := R1_neq_R0).
@@ -148,11 +148,11 @@ Next Obligation.
   apply injective_projections ; simpl ; apply H.
 Qed.
 
-#[export] Program Instance C_is_module_space : Module_Space C C :=
+Global Program Instance C_is_module_space : Module_Space C C :=
   { Vscale := Cmult }.
 Solve All Obligations with program_simpl; lca. 
 
-#[export] Program Instance C_is_vector_space : Vector_Space C C.
+Global Program Instance C_is_vector_space : Vector_Space C C.
 
 
 
@@ -1397,7 +1397,7 @@ Proof.
   lca.
 Qed.
 
-#[export] Hint Rewrite Cexp_0 Cexp_PI Cexp_PI2 Cexp_2PI Cexp_3PI2 Cexp_PI4 Cexp_PIm4
+Hint Rewrite Cexp_0 Cexp_PI Cexp_PI2 Cexp_2PI Cexp_3PI2 Cexp_PI4 Cexp_PIm4
   Cexp_1PI4 Cexp_2PI4 Cexp_3PI4 Cexp_4PI4 Cexp_5PI4 Cexp_6PI4 Cexp_7PI4 Cexp_8PI4
   Cexp_add Cexp_neg Cexp_plus_PI Cexp_minus_PI : Cexp_db.
 
@@ -1442,28 +1442,28 @@ Ltac nonzero :=
   | |- Rle _ _ => lra
   end.
 
-#[export] Hint Rewrite Cminus_unfold Cdiv_unfold Ci2 Cconj_R Cconj_opp Cconj_rad2 
+Hint Rewrite Cminus_unfold Cdiv_unfold Ci2 Cconj_R Cconj_opp Cconj_rad2 
      Cinv_sqrt2_sqrt Cplus_div2
      Cplus_0_l Cplus_0_r Cplus_opp_r Cplus_opp_l Copp_0  Copp_involutive
      Cmult_0_l Cmult_0_r Cmult_1_l Cmult_1_r : C_db.
 
-#[export] Hint Rewrite <- Copp_mult_distr_l Copp_mult_distr_r Cdouble : C_db.
-#[export] Hint Rewrite Csqrt_sqrt using Psatz.lra : C_db.
-#[export] Hint Rewrite Cinv_l Cinv_r using nonzero : C_db.
+Hint Rewrite <- Copp_mult_distr_l Copp_mult_distr_r Cdouble : C_db.
+Hint Rewrite Csqrt_sqrt using Psatz.lra : C_db.
+Hint Rewrite Cinv_l Cinv_r using nonzero : C_db.
 (* Previously in the other direction *)
-#[export] Hint Rewrite Cinv_mult_distr using nonzero : C_db.
+Hint Rewrite Cinv_mult_distr using nonzero : C_db.
 
 (* Light rewriting db *)
-#[export] Hint Rewrite Cplus_0_l Cplus_0_r Cmult_0_l Cmult_0_r Copp_0 
+Hint Rewrite Cplus_0_l Cplus_0_r Cmult_0_l Cmult_0_r Copp_0 
              Cconj_R Cmult_1_l Cmult_1_r : C_db_light.
 
 (* Distributing db *)
-#[export] Hint Rewrite Cmult_plus_distr_l Cmult_plus_distr_r Copp_plus_distr Copp_mult_distr_l 
+Hint Rewrite Cmult_plus_distr_l Cmult_plus_distr_r Copp_plus_distr Copp_mult_distr_l 
               Copp_involutive : Cdist_db.
 
-#[export] Hint Rewrite RtoC_opp RtoC_mult RtoC_minus RtoC_plus : RtoC_db.
-#[export] Hint Rewrite RtoC_inv using nonzero : RtoC_db.
-#[export] Hint Rewrite RtoC_pow : RtoC_db.
+Hint Rewrite RtoC_opp RtoC_mult RtoC_minus RtoC_plus : RtoC_db.
+Hint Rewrite RtoC_inv using nonzero : RtoC_db.
+Hint Rewrite RtoC_pow : RtoC_db.
 
 Ltac Csimpl := 
   repeat match goal with

diff --git a/FiniteGroups.v b/FiniteGroups.v
@@ -12,7 +12,7 @@ Require Import Setoid.
 
 
 
-#[export] Program Instance list_is_monoid {X} : Monoid (list X) := 
+Global Program Instance list_is_monoid {X} : Monoid (list X) := 
   { Gzero := []
   ; Gplus := @app X
   }.
@@ -721,14 +721,14 @@ Definition quatMul (q1 q2 : Quaternion) : Quaternion :=
 
 
 
-#[export] Program Instance quat_is_monoid : Monoid Quaternion := 
+Global Program Instance quat_is_monoid : Monoid Quaternion := 
   { Gzero := p_1
   ; Gplus := quatMul
   }.
 Solve All Obligations with program_simpl; destruct g; try easy; destruct h; destruct i; easy. 
 
 
-#[export] Program Instance quat_is_group : Group Quaternion :=
+Global Program Instance quat_is_group : Group Quaternion :=
   { Gopp := quatInv }.
 Solve All Obligations with program_simpl; destruct g; try easy. 
 
@@ -746,7 +746,7 @@ Qed.
 Definition quat_list : list Quaternion := [p_1; p_i; p_j; p_k; n_1; n_i; n_j; n_k].
 
 
-#[export] Program Instance quat_is_finitegroup : FiniteGroup Quaternion := 
+Global Program Instance quat_is_finitegroup : FiniteGroup Quaternion := 
   { G_list_rep := quat_list
   }.
 Next Obligation. 

diff --git a/Polar.v b/Polar.v
@@ -56,7 +56,7 @@ Proof. intros.
        assert (H0 := Rmax_Cmod (x, y)).
        apply (Rle_trans (Rabs (fst (x, y)))) in H0; try apply Rmax_l; simpl in *.
        apply (Rmult_le_compat_r (/ Cmod (x, y))) in H0.
-       rewrite Rinv_r, <- (Rabs_pos_eq (Cmod _)), <- Rabs_inv, <- Rabs_mult in H0.
+       rewrite Rinv_r, <- (Rabs_pos_eq (Cmod _)), <- Rabs_Rinv, <- Rabs_mult in H0.
        all : try (left; apply Rinv_0_lt_compat); try apply Cmod_ge_0; try apply Cmod_gt_0.
        all : try (unfold not; intros; apply H; apply Cmod_eq_0; easy).
        destruct H0.
@@ -78,7 +78,7 @@ Proof. intros.
        apply (Rle_trans (Rabs (fst (x, y)))) in H0; try apply Rmax_l; simpl in *.
        destruct H0.
        - apply (Rmult_lt_compat_r (/ Cmod (x, y))) in H0.
-         rewrite Rinv_r, <- (Rabs_pos_eq (Cmod _)), <- Rabs_inv, <- Rabs_mult in H0.
+         rewrite Rinv_r, <- (Rabs_pos_eq (Cmod _)), <- Rabs_Rinv, <- Rabs_mult in H0.
          all : try (apply Rinv_0_lt_compat; apply Cmod_gt_0).
          all : try apply Cmod_ge_0.
          all : try (unfold not; intros; apply H'; apply Cmod_eq_0; easy).
@@ -159,7 +159,8 @@ Lemma div_subtract_helper : forall (x y : R),
   (1 - (x / Cmod (x, y))²)%R = (y² * / (Cmod (x, y))²)%R.
 Proof. intros.  
        unfold Rdiv.
-       rewrite Rsqr_mult, Rsqr_inv'.
+       rewrite Rsqr_mult.
+       rewrite Rsqr_inv.
        rewrite <- (Rinv_r ((Cmod (x, y))²)).
        replace (((Cmod (x, y))² * / (Cmod (x, y))² + - (x² * / (Cmod (x, y))²))%R) with
          ( ((Cmod (x, y))² - x²) * / ((Cmod (x, y))²))%R by lra.
@@ -172,6 +173,7 @@ Proof. intros.
        unfold Rsqr in H0.
        apply Rmult_integral in H0; apply Cmod_eq_0. 
        destruct H0; easy.
+       apply Cmod_eq_0; easy.
 Qed.
 
 Lemma rect_to_polar_to_rect : forall (z : C),

diff --git a/Polynomial.v b/Polynomial.v
@@ -99,7 +99,7 @@ Fixpoint Pmult (p1 p2 : Polynomial) : Polynomial :=
 Definition Popp (p : Polynomial) : Polynomial :=
   Pmult [-C1] p.
 
-#[export] Program Instance P_is_monoid : Monoid Polynomial := 
+Global Program Instance P_is_monoid : Monoid Polynomial := 
   { Gzero := []
   ; Gplus := Pplus
   }.
@@ -1705,7 +1705,7 @@ Proof. split; intros.
          unfold Rdiv in *.
          unfold pow in *.
          apply (Rmult_le_pos a) in H1; try lra.
-         rewrite Rmult_plus_distr_l, Rinv_mult, Rmult_plus_distr_l in H1; try lra.
+         rewrite Rmult_plus_distr_l, Rinv_mult_distr, Rmult_plus_distr_l in H1; try lra.
          replace (a * (b * (- b * (/ 2 * / a))))%R 
            with (- b * b * (a * / a) * / 2)%R in H1 by lra. 
          replace (a * (a * (- b * (/ 2 * / a) * (- b * (/ 2 * / a) * 1))))%R
@@ -1722,8 +1722,17 @@ Proof. split; intros.
            unfold Rdiv; repeat rewrite Rinv_mult; try lra.
            replace ((t + b * (/ 2 * / a)) * (t + b * (/ 2 * / a)))%R 
              with (t * t + t * b * / a + (b * b * /a * /a * /4))%R by lra.
-           replace (a * c * (/ a * / a))%R with (c * / a * (a * / a))%R by lra.
-           rewrite Rinv_r, Rmult_1_r; try lra. }
+           replace (a * c * (/ a * / a))%R with (c * / a)%R; [ | shelve ].
+           R_field_simplify.
+           easy.
+           lra.
+           Unshelve.
+           rewrite (Rmult_comm a c).
+           rewrite Rmult_assoc.
+           rewrite <- (Rmult_assoc a (/ a)).
+           rewrite Rinv_r.
+           all: lra.
+         }
          rewrite <- H1.
          apply Rmult_le_pos; try lra.
          apply Rplus_le_le_0_compat.

diff --git a/README.md b/README.md
@@ -11,6 +11,11 @@ QuantumLib is a Coq library for reasoning about quantum programs. It was co-deve
 ## Compilation
 
 Tested with Coq versions 8.12 -- 8.15.
+Experimental on 8.16
+
+This project requires `opam` & `dune` to be installed.
+
+Install `dune` using `opam install dune`
 
 To compile run `make all`.
 

diff --git a/RealAux.v b/RealAux.v
@@ -24,10 +24,10 @@ Lemma Rminus_lt_0 : forall a b, a < b <-> 0 < b - a. Proof. intros. lra. Qed.
 Lemma Rminus_unfold : forall r1 r2, (r1 - r2 = r1 + -r2). Proof. reflexivity. Qed.
 Lemma Rdiv_unfold : forall r1 r2, (r1 / r2 = r1 */ r2). Proof. reflexivity. Qed.
 
-#[export] Hint Rewrite Rminus_unfold Rdiv_unfold Ropp_0 Ropp_involutive Rplus_0_l 
+Hint Rewrite Rminus_unfold Rdiv_unfold Ropp_0 Ropp_involutive Rplus_0_l 
              Rplus_0_r Rmult_0_l Rmult_0_r Rmult_1_l Rmult_1_r : R_db.
-#[export] Hint Rewrite <- Ropp_mult_distr_l Ropp_mult_distr_r : R_db.
-#[export] Hint Rewrite Rinv_l Rinv_r sqrt_sqrt using lra : R_db.
+Hint Rewrite <- Ropp_mult_distr_l Ropp_mult_distr_r : R_db.
+Hint Rewrite Rinv_l Rinv_r sqrt_sqrt using lra : R_db.
 
 Notation "√ n" := (sqrt n) (at level 20) : R_scope.
 
@@ -38,7 +38,7 @@ Proof. intros. unfold Rdiv. rewrite Rmult_assoc. reflexivity. Qed.
 
 Lemma Rmult_div : forall r1 r2 r3 r4 : R, r2 <> 0 -> r4 <> 0 -> 
   r1 / r2 * (r3 / r4) = r1 * r3 / (r2 * r4). 
-Proof. intros. unfold Rdiv. rewrite Rinv_mult; trivial. lra. Qed.
+Proof. intros. unfold Rdiv. rewrite Rinv_mult_distr; trivial. lra. Qed.
 
 Lemma Rdiv_cancel :  forall r r1 r2 : R, r1 = r2 -> r / r1 = r / r2.
 Proof. intros. rewrite H. reflexivity. Qed.
@@ -287,13 +287,17 @@ Proof. intros.
        replace (S x) with (1 + x)%nat by lia.
        rewrite Nat2Z.inj_add, Z.pow_add_r, two_val_mult; try lia.
        rewrite IHx; auto; try lia.
-       destruct x; simpl; lia.
+       try (apply (Z.pow_nonzero 2 x); lia).
+       induction x; auto.
+       replace (S x) with (1 + x)%nat by lia.
+       rewrite Nat2Z.inj_add, Z.opp_add_distr, Z.pow_add_r, two_val_mult; try lia.
 Qed.
 
 Lemma twoadic_nonzero : forall (a b : Z),
   a >= 0 -> 2^a * (2 * b + 1) <> 0.
 Proof. intros. 
-       apply Z.neq_mul_0; split; try lia.
+       apply Z.neq_mul_0; split; try lia;
+       try (apply Z.pow_nonzero; lia).
 Qed.
 
 Lemma get_two_val : forall (a b : Z),
@@ -558,7 +562,7 @@ Proof.
     apply sin_upper_bound_aux; lra.
 Qed.    
 
-#[export] Hint Rewrite sin_0 sin_PI4 sin_PI2 sin_PI cos_0 cos_PI4 cos_PI2 
+Hint Rewrite sin_0 sin_PI4 sin_PI2 sin_PI cos_0 cos_PI4 cos_PI2 
              cos_PI sin_neg cos_neg : trig_db.
 
 (** * glb support *) 
@@ -626,42 +630,42 @@ Qed.
 
 (** * Showing that R is a field, and a vector space over itself *)
 
-#[export] Program Instance R_is_monoid : Monoid R := 
+Global Program Instance R_is_monoid : Monoid R := 
   { Gzero := 0
   ; Gplus := Rplus
   }.
 Solve All Obligations with program_simpl; try lra.
 
-#[export] Program Instance R_is_group : Group R :=
+Global Program Instance R_is_group : Group R :=
   { Gopp := Ropp }.
 Solve All Obligations with program_simpl; try lra.
 
-#[export] Program Instance R_is_comm_group : Comm_Group R.
+Global Program Instance R_is_comm_group : Comm_Group R.
 Solve All Obligations with program_simpl; lra. 
 
-#[export] Program Instance R_is_ring : Ring R :=
+Global Program Instance R_is_ring : Ring R :=
   { Gone := 1
   ; Gmult := Rmult
   }.
 Solve All Obligations with program_simpl; try lra. 
 Next Obligation. try apply Req_EM_T. Qed.
 
 
-#[export] Program Instance R_is_comm_ring : Comm_Ring R.
+Global Program Instance R_is_comm_ring : Comm_Ring R.
 Solve All Obligations with program_simpl; lra. 
 
-#[export] Program Instance R_is_field : Field R :=
+Global Program Instance R_is_field : Field R :=
   { Ginv := Rinv }.
 Next Obligation. 
   rewrite Rinv_r; easy.
 Qed.
 
-#[export] Program Instance R_is_module_space : Module_Space R R :=
+Global Program Instance R_is_module_space : Module_Space R R :=
   { Vscale := Rmult }.
 Solve All Obligations with program_simpl; lra. 
 
 
-#[export] Program Instance R_is_vector_space : Vector_Space R R.  
+Global Program Instance R_is_vector_space : Vector_Space R R.