Merge pull request #68 from clayrat/variant

change CoInductive to Variant for specs

refinements/seqmx.v

@@ -294,7 +294,7 @@ Local Instance implem_ord : forall n, (implem_of 'I_n 'I_n) :=
 
 Local Open Scope rel_scope.
 
-CoInductive Rseqmx {m1 m2} (rm : nat_R m1 m2) {n1 n2} (rn : nat_R n1 n2) :
+Variant Rseqmx {m1 m2} (rm : nat_R m1 m2) {n1 n2} (rn : nat_R n1 n2) :
   'M[R]_(m1,n1) -> hseqmx m2 n2 -> Type :=
   Rseqmx_spec (A : 'M[R]_(m1, n1)) M of
     size M = m2

theory/dvdring.v

@@ -48,7 +48,7 @@ End GUARD.
 Module DvdRing.
 
 (* Specification of division: div_spec a b == b | a *)
-CoInductive div_spec (R : ringType) (a b :R) : option R -> Type :=
+Variant div_spec (R : ringType) (a b : R) : option R -> Type :=
 | DivDvd x of a = x * b : div_spec a b (Some x)
 | DivNDvd of (forall x, a != x * b) : div_spec a b None.
 
@@ -1272,7 +1272,7 @@ End GCDDomainTheory.
 
 Module BezoutDomain.
 
-CoInductive bezout_spec (R : gcdDomainType) (a b : R) : R * R -> Type:=
+Variant bezout_spec (R : gcdDomainType) (a b : R) : R * R -> Type:=
   BezoutSpec x y of gcdr a b %= x * a + y * b : bezout_spec a b (x, y).
 
 Record mixin_of (R : gcdDomainType) : Type := Mixin {
@@ -1370,7 +1370,7 @@ Definition egcdr a b :=
         let b1 := odflt 0 (b %/? g) in
           if g == 0 then (0,1,0,1,0) else (g, u, v, a1, b1).
 
-CoInductive egcdr_spec a b : R * R * R * R * R -> Type :=
+Variant egcdr_spec a b : R * R * R * R * R -> Type :=
   EgcdrSpec g u v a1 b1 of u * a1 + v * b1 = 1
                          & g %= gcdr a b
                          & a = a1 * g
@@ -1703,7 +1703,7 @@ End PIDTheory.
 
 Module EuclideanDomain.
 
-CoInductive edivr_spec (R : ringType)
+Variant edivr_spec (R : ringType)
   (norm : R -> nat) (a b : R) : R * R -> Type :=
   EdivrSpec q r of a = q * b + r & (b != 0) ==> (norm r < norm b)
   : edivr_spec norm a b (q,r).

theory/edr.v

@@ -19,7 +19,7 @@ Local Open Scope ring_scope.
 (** Elementary divisor rings *)
 Module EDR.
 
-CoInductive smith_spec (R : dvdRingType) m n M
+Variant smith_spec (R : dvdRingType) m n M
   : 'M[R]_m * seq R * 'M[R]_n -> Type :=
     SmithSpec P d Q of P *m M *m Q = diag_mx_seq m n d
                      & sorted %|%R d
@@ -498,12 +498,12 @@ elim: i {-2}i (leqnn i)=>[i|i IHi j Hji Hj].
   rewrite leqn0=> /eqP -> Hi.
   move: (Smith_gcdr_spec Hi Hd HMd); rewrite eqd_sym.
   move/(eqd_trans (Smith_gcdr_spec Hi Hsorted HMdmt)).
-  by rewrite !big_ord1 eqd_sym. 
+  by rewrite !big_ord1 eqd_sym.
 move: (Smith_gcdr_spec Hj Hd HMd); rewrite eqd_sym.
 move/(eqd_trans (Smith_gcdr_spec Hj Hsorted HMdmt)).
 rewrite !big_ord_recr /= => H3.
 have H1: \prod_(i < j) d`_i %= \prod_(i < j) s`_i.
-  apply: eqd_big_mul=> k _. 
+  apply: eqd_big_mul=> k _.
   by rewrite (IHi k _ (ltn_trans _ Hj)) // -ltnS (leq_trans (ltn_ord k) Hji).
 have [H0|H0] := boolP (\prod_(i < j) d`_i == 0).
   have/prodf_eq0 [k _ /eqP Hk] : (\prod_(i < j) s`_i == 0).

theory/kaplansky.v

@@ -360,7 +360,7 @@ Definition egcdr3 (a b c : R) :=
   let: (g,u,v,a1,g1)    := egcdr a g' in
   (g, u, v * u1, v * v1, a1,b1 * g1,c1 * g1).
 
-CoInductive egcdr3_spec a b c : R * R * R * R * R * R * R-> Type :=
+Variant egcdr3_spec a b c : R * R * R * R * R * R * R-> Type :=
   EgcdrSpec g x y z a1 b1 c1 of x * a1 + y * b1 + z * c1 = 1
   & g %= gcdr a (gcdr b c)
   & a = a1 * g & b = b1 * g & c = c1 * g : egcdr3_spec a b c (g,x,y,z,a1,b1,c1).
@@ -481,7 +481,7 @@ Section AdequacyGdco.
 
 Variable R : gcdDomainType.
 
-CoInductive adequate_spec (a b : R) : R -> Type :=
+Variant adequate_spec (a b : R) : R -> Type :=
   | AdequateSpec0 of b = 0 : adequate_spec a b 0
   | AdequateSpec r of b != 0
                       & r %| b
@@ -490,7 +490,7 @@ CoInductive adequate_spec (a b : R) : R -> Type :=
                           ~~ coprimer d a)
                       : adequate_spec a b r.
 
-CoInductive gdco_spec (a b : R) : R -> Type :=
+Variant gdco_spec (a b : R) : R -> Type :=
   | GdcoSpec0 of b = 0 : gdco_spec a b 0
   | GdcoSpec r of b != 0
                   & r %| b

theory/smith.v

@@ -98,7 +98,7 @@ Fixpoint Smith m n : 'M[E]_(m,n) -> 'M[E]_(m) * seq E * 'M[E]_(n) :=
   | _, _ => fun M => (1%:M, [::], 1%:M)
   end.
 
-CoInductive improve_pivot_rec_spec m n P M Q :
+Variant improve_pivot_rec_spec m n P M Q :
   'M_(1 + m) * 'M_(1 + m,1 + n) * 'M[E]_(1 + n) -> Type :=
   ImprovePivotQecSpec P' M' Q' of P^-1 *m M *m Q^-1 = P'^-1 *m M' *m Q'^-1
   & (forall i j, M' 0 0 %| M' i j)
@@ -183,7 +183,7 @@ constructor=> //; first by rewrite -HblockL -Hblock invrM // mulmxA mulmxKV.
 by rewrite -HblockL unitmx_mul unitmxE (det_lblock 1 P) !det1 mulr1 unitr1.
 Qed.
 
-CoInductive improve_pivot_spec m n M :
+Variant improve_pivot_spec m n M :
   'M[E]_(1 + m) * 'M_(1 + m,1 + n) * 'M_(1 + n) -> Type :=
   ImprovePivotSpec L A R of L *m M *m R = A
   & (forall i j, A 0 0 %| A i j)

theory/smithpid.v

@@ -114,7 +114,7 @@ Fixpoint Smith {m n} : 'M[R]_(m,n) -> 'M[R]_(m) * seq R * 'M[R]_(n) :=
 Hypothesis find_pivotP : forall m n (M : 'M[R]_(1 + m,1 + n)),
   pick_spec [pred ij | M ij.1 ij.2 != 0] (find_pivot M).
 
-CoInductive improve_pivot_rec_spec m n P M Q :
+Variant improve_pivot_rec_spec m n P M Q :
   'M[R]_(1 + m) * 'M[R]_(1 + m,1 + n) * 'M[R]_(1 + n) -> Type :=
   ImprovePivotRecSpec P' A Q' of P^-1 *m M *m Q^-1 = P'^-1 *m A *m Q'^-1
   & (forall i j, A 0 0 %| A i j)
@@ -213,7 +213,7 @@ constructor=> //; first by rewrite -HblockP -Hblock invrM // mulmxA mulmxKV.
 by rewrite -HblockP unitmx_mul unitmxE (det_lblock 1 M') !det1 mulr1 unitr1.
 Qed.
 
-CoInductive improve_pivot_spec m n M :
+Variant improve_pivot_spec m n M :
   'M[R]_(1 + m) * 'M[R]_(1 + m,1 + n) * 'M[R]_(1 + n) -> Type :=
   ImprovePivotSpec P A Q of P *m M *m Q = A
   & (forall i j, A 0 0 %| A i j)

theory/stronglydiscrete.v

@@ -17,7 +17,7 @@ Local Open Scope ring_scope.
 (** Strongly discrete rings *)
 Module StronglyDiscrete.
 
-CoInductive member_spec (R : ringType) n (x : R) (I : 'cV[R]_n)
+Variant member_spec (R : ringType) n (x : R) (I : 'cV[R]_n)
   : option 'rV[R]_n -> Type :=
 | Member J of x%:M = J *m I : member_spec x I (Some J)
 | NMember of (forall J, x%:M != J *m I) : member_spec x I None.
@@ -661,7 +661,7 @@ Section IdealIntersection.
 
 Variable cap_size : forall n m, 'cV[R]_n -> 'cV[R]_m -> nat.
 
-CoInductive int_spec m n (I : 'cV[R]_m) (J : 'cV[R]_n) : 'cV[R]_(cap_size I J).+1 -> Type :=
+Variant int_spec m n (I : 'cV[R]_m) (J : 'cV[R]_n) : 'cV[R]_(cap_size I J).+1 -> Type :=
   IntSpec cap of (cap <= I)%IS
   & (cap <= J)%IS
   & (forall x, member x I -> member x J -> member x cap) : int_spec cap.