remove the attic/ directory

1 files changed, 0 insertions, 197 deletions

diff --git a/mathcomp/attic/forms.v b/mathcomp/attic/forms.v
deleted file mode 100644
index 7098af9..0000000
--- a/mathcomp/attic/forms.v
+++ /dev/null
@@ -1,197 +0,0 @@
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
-(* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype bigop.
-From mathcomp
-Require Import finfun tuple ssralg matrix zmodp vector.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-Local Open Scope ring_scope.
-
-Import GRing.Theory.
-
-Section RingLmodule.
-
-Variable (R : fieldType).
-
-Definition r2rv x: 'rV[R^o]_1 := \row_(i < 1) x .
-
-Lemma r2rv_morph_p : linear r2rv.
-Proof. by move=> k x y; apply/matrixP=> [] [[|i] Hi] j; rewrite !mxE. Qed.
-
-Canonical Structure r2rv_morph := Linear r2rv_morph_p.
-
-Definition rv2r (A: 'rV[R]_1): R^o := A 0 0.
-
-Lemma r2rv_bij : bijective r2rv.
-Proof.
-exists rv2r; first by move=> x; rewrite /r2rv /rv2r /= mxE.
-by move=> x; apply/matrixP=> i j; rewrite [i]ord1 [j]ord1 /r2rv /rv2r !mxE /=.
-Qed.
-
-Canonical Structure  RVMixin := Eval hnf in VectMixin r2rv_morph_p r2rv_bij.
-Canonical Structure RVVectType :=  VectType R RVMixin.
-
-Lemma dimR : vdim RVVectType = 1%nat.
-Proof. by rewrite /vdim /=. Qed.
-
-End RingLmodule.
-
-(* BiLinear & Sesquilinear & Quadratic Forms over a vectType *)
-Section LinearForm.
-
-Variable (F : fieldType) (V : vectType  F).
-
-Section SesquiLinearFormDef.
-
-Structure fautomorphism:= FautoMorph {fval :> F -> F;
-                                      _ : rmorphism  fval;
-                                      _ : bijective fval}.
-Variable theta: fautomorphism.
-
-Lemma fval_rmorph : rmorphism theta.
-Proof. by case: theta. Qed.
-
-Canonical Structure fautomorh_additive := Additive fval_rmorph.
-Canonical Structure fautomorph_rmorphism := RMorphism  fval_rmorph.
-
-Local Notation vvf:= (V -> V -> F).
-
-Structure sesquilinear_form  := 
-              SesqlinearForm {formv :> vvf;
- 	         _ : forall x, {morph formv x : y z / y + z};
- 	         _ : forall x, {morph formv ^~  x : y z / y + z};
- 	         _ : forall a x y,  formv  (a *: x) y = a * formv x y;
- 		 _ : forall a x y , formv x (a *: y) = (theta a) * (formv x y)}.
-
-Variable f : sesquilinear_form.
-
-Lemma bilin1 :  forall x, {morph f x : y z / y + z}. Proof. by case f. Qed.
-Lemma bilin2 :  forall x, {morph f ^~  x : y z / y + z}. Proof. by case f. Qed.
-Lemma bilina1 :  forall a x y, f (a *: x) y = a * f x y. Proof. by case f. Qed.
-Lemma bilina2 : forall a x y, f x (a *: y) = (theta  a) * (f x y).
-Proof. by case f. Qed.
-
-End SesquiLinearFormDef.
-
-Section SesquiLinearFormTheory.
-
-Variable theta: fautomorphism.
-Local Notation sqlf := (sesquilinear_form theta).
-
-Definition symmetric (f : sqlf):= (forall a,  (theta  a = a)) /\  
-                                  forall x y, (f x y = f y x).
-Definition skewsymmetric (f : sqlf) := (forall a , theta a = a) /\ 
-                                      forall x y, f x y = -(f y x).
-
-Definition hermitian_sym  (f : sqlf) := (forall x y, f x y = (theta (f y x))).
-
-Inductive symmetricf (f : sqlf): Prop :=
-  Symmetric : symmetric f -> symmetricf f
-| Skewsymmetric: skewsymmetric f -> symmetricf f
-| Hermitian_sym : hermitian_sym f -> symmetricf f .
-
-Lemma fsym_f0: forall  (f: sqlf) x y, (symmetricf f) ->  
-                                        (f x y = 0  <-> f y x = 0).
-Proof.
-move=> f x y; case; first by  move=> [Htheta Hf]; split; rewrite Hf.
-  by move=> [Htheta Hf]; split; rewrite Hf; move/eqP; rewrite oppr_eq0; move/eqP->.
-move=> Htheta; split; first by rewrite (Htheta y x) => ->; rewrite rmorph0.
-by rewrite (Htheta x y) => ->; rewrite rmorph0.
-Qed.
-
-End SesquiLinearFormTheory.
-
-Variable theta: fautomorphism.
-Variable f: (sesquilinear_form theta).
-Hypothesis fsym: symmetricf f.
-
-Section orthogonal.
-
-Definition orthogonal x y := f x y = 0.
-
-Lemma ortho_sym: forall x y, orthogonal x y <-> orthogonal y x.
-Proof. by move=> x y; apply: fsym_f0. Qed.
-
-Theorem Pythagore: forall u v, orthogonal u v -> f (u+v) (u+v)  = f u u  + f v v.
-Proof.
-move=> u v Huv; case: (ortho_sym  u v ) => Hvu _.
-by rewrite !bilin1 !bilin2 Huv (Hvu Huv) add0r addr0.
-Qed.
-
-Lemma orthoD : forall u v w , orthogonal u v -> orthogonal u w -> orthogonal u (v + w).
-Proof.
-by move=> u v w Huv Huw; rewrite /orthogonal bilin1 Huv Huw add0r.
-Qed.
-
-Lemma orthoZ: forall u v a, orthogonal u v ->  orthogonal (a *: u) v.
-Proof. by move=> u v a Huv; rewrite /orthogonal bilina1 Huv mulr0. Qed.
-
-Variable x:V.
-
-Definition alpha : V-> (RVVectType F) := fun y => f y x.
-
-Definition alpha_lfun := (lfun_of_fun alpha).
-
-Definition  xbar := lker alpha_lfun .
-
-Lemma alpha_lin: linear alpha.
-Proof. by move=> a b c; rewrite /alpha bilin2 bilina1. Qed.
-
-
-
-Lemma xbarP:  forall e1, reflect (orthogonal e1 x ) (e1 \in xbar).
-move=> e1; rewrite memv_ker  lfun_of_funK //=.
-  by apply: (iffP eqP).
-by apply alpha_lin.
-Qed.
-
-
-Lemma dim_xbar :forall vs,(\dim vs ) -  1 <= \dim (vs :&: xbar).
-Proof.
-move=> vs; rewrite -(addKn 1 (\dim (vs :&: xbar))) addnC leq_sub2r //.
-have H :\dim  (alpha_lfun @: vs )<= 1 by rewrite -(dimR F) -dimvf dimvS // subvf.
-by rewrite -(limg_ker_dim alpha_lfun vs)(leq_add (leqnn (\dim(vs :&: xbar)))).
-Qed.
-
-(* to be improved*)
-Lemma xbar_eqvs: forall vs,  (forall v , v \in vs -> orthogonal v x )-> \dim (vs :&: xbar)= (\dim vs ).
-move=> vs  Hvs.
-rewrite -(limg_ker_dim alpha_lfun vs).
-suff-> : \dim (alpha_lfun @: vs) = 0%nat by rewrite addn0.
-apply/eqP; rewrite dimv_eq0; apply/vspaceP => w.
-rewrite memv0; apply/memv_imgP.
-case e: (w==0).
-  exists 0; split; first by rewrite mem0v.
-  apply sym_eq; rewrite (eqP e).
-  rewrite (lfun_of_funK alpha_lin 0).
-  rewrite /alpha_lfun /alpha /=.
-  by move: (bilina1 f 0 x x); rewrite scale0r mul0r.
-move/eqP:e =>H2; case=> x0 [Hx0 Hw].
-apply H2; rewrite Hw; move: (Hvs x0 Hx0).
-rewrite /orthogonal.
-by rewrite (lfun_of_funK alpha_lin x0).
-Qed.
-
-
-End orthogonal.
-
-Definition quadraticf (Q: V -> F) := 
-     (forall x a, Q (a *: x) = a ^+ 2 * (Q x))%R *
-     (forall x y, Q (x + y) = Q x + Q y + f x y)%R : Prop.
-Variable Q : V -> F.
-Hypothesis quadQ :  quadraticf Q.
-Import GRing.Theory.
-
-
-Lemma f2Q:  forall x, Q x + Q x = f x x.
-Proof.
-move=> x; apply: (@addrI _ (Q x + Q x)).
-rewrite !addrA  -quadQ -[x + x](scaler_nat 2) quadQ.
-by rewrite -mulrA !mulr_natl -addrA.
-Qed.
-
-End LinearForm.