diff options
| author | Enrico Tassi | 2015-03-09 11:07:53 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-03-09 11:24:38 +0100 |
| commit | fc84c27eac260dffd8f2fb1cb56d599f1e3486d9 (patch) | |
| tree | c16205f1637c80833a4c4598993c29fa0fd8c373 /mathcomp/attic | |
Initial commit
Diffstat (limited to 'mathcomp/attic')
| -rw-r--r-- | mathcomp/attic/algnum_basic.v | 535 | ||||
| -rw-r--r-- | mathcomp/attic/all.v | 9 | ||||
| -rw-r--r-- | mathcomp/attic/amodule.v | 417 | ||||
| -rw-r--r-- | mathcomp/attic/fib.v | 340 | ||||
| -rw-r--r-- | mathcomp/attic/forms.v | 193 | ||||
| -rw-r--r-- | mathcomp/attic/galgebra.v | 227 | ||||
| -rw-r--r-- | mathcomp/attic/multinom.v | 438 | ||||
| -rw-r--r-- | mathcomp/attic/mxtens.v | 312 | ||||
| -rw-r--r-- | mathcomp/attic/quote.v | 365 | ||||
| -rw-r--r-- | mathcomp/attic/tutorial.v | 296 |
10 files changed, 3132 insertions, 0 deletions
diff --git a/mathcomp/attic/algnum_basic.v b/mathcomp/attic/algnum_basic.v new file mode 100644 index 0000000..a302e7a --- /dev/null +++ b/mathcomp/attic/algnum_basic.v @@ -0,0 +1,535 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple div. +Require Import bigop prime finset fingroup ssralg finalg zmodp abelian. +Require Import matrix vector falgebra finfield action poly ssrint cyclotomic. +Require Import fieldext mxalgebra mxpoly. + +(************************************************************************************************) +(* Basic algebraic number theory concepts from Milne, J.S.: Algebraic Number Theory. *) +(* We work in the setting of an extension field L0 : fieldextType F. At this point, *) +(* an integral domain is represented as a collective predicate on L0 closed under *) +(* subring operations. A module over the integral domain A is represented as a *) +(* Prop-valued predicate closed under the operations (0, x + y, x - y, x * y). It *) +(* is not a-priori made a collective predicate since we first need to establish the *) +(* Basis Lemma in order to show decidability. *) +(* *) +(* integral A l <-> l is integral over the domain A, i.e., it satisfies a polynomial *) +(* over A. This is currently a Prop-valued predicate since we *) +(* quantify over all polynomials over A. An alternative definition *) +(* would be to say that the minimal polynomial of l over the field *) +(* of fractions of A is itself a polynomial over A. The latter is *) +(* a decidable property and the equivalence of the two definitions *) +(* is provided by Prop. 2.11 in Milne. *) +(* int_closed A <-> A is integrally closed. *) +(* int_closure A L == The integral closure of A in L. This is currently a Prop-valued *) +(* predicate. *) +(* is_frac_field A K <-> K is the field of fractions of A. The condition of every k \in K *) +(* arising as a quotient a / b for a,b \in K is skolemized. This is *) +(* not strictly necessary since L0 has a canonical choiceType *) +(* structure but it facilitates some of the later proofs. *) +(* frac_field_alg_int A == Every element l arises as a quotient b / a, where a is in A and b *) +(* is integral over A. The statement of the theorem is skolemized, *) +(* which is not strictly necessary. *) +(* int_clos_incl A == Every element of A is integral over A. *) +(* int_subring_closed A == The integral closure of A is closed under the subring operations *) +(* (a - b, a * b). The proof of this lemma uses an equivalent *) +(* characterization of integrality, cf. Prop. 2.4 in Milne, which is *) +(* captured by the Lemmas intPl and intPr. The former states that *) +(* if there exists a nonzero finitely-generated A-module closed under *) +(* multiplication by l, then l is integral over A. The latter states *) +(* that if l is integral over A, then the A-algebra generated by l is *) +(* closed under multiplication by l. Note: These lemmas probably need *) +(* better names. *) +(* int_zmod_closed A == The integral closure of A is closed under subtraction. *) +(* int_mulr_closed A == The integral closure of A is closed under multiplication. *) +(* tr L l k == The trace of l * k on L; the result is in the field of scalars F. *) +(* The function tr is scalar in its first argument. *) +(* tr_sym == The trace function is commutative. *) +(* ndeg Q V <-> The binary function Q : vT -> vT -> rT is nondegenerate on the *) +(* subspace V. *) +(* dual_basis U X == The dual basis of U for X, with respect to the trace bilinear form. *) +(* trK K L == The trace function on L viewed as a subfield over K. *) +(* trK_int A K L == If k and l are integral over A then their trace is in A, provided *) +(* A is an integrally closed domain, K is its field of fractions, and *) +(* L extends K. *) +(* module A M <-> M is an A-module. *) +(* span_mod A X == The A-module generated by X. *) +(* submod A M N <-> M is a submodule of N over A. *) +(* basis_of_mod A M X <-> X is the basis of the A-module M. *) +(* ideal A N <-> N is an A-ideal. *) +(* PID A <-> Every ideal in A is principal. *) +(* int_mod_closed A L == The integral closure of A in L is an A-module. *) +(* basis_lemma I Ifr K == The integral closure of I in K is a free module, provided I is an *) +(* integrally-closed principal ideal domain contained in K, Ifr is the *) +(* field of fractions of I, and the trace function trK Ifr K is *) +(* nondegenerate on K. *) +(************************************************************************************************) + +Import GRing.Theory. +Import DefaultKeying GRing.DefaultPred. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope ring_scope. + +Section Integral. + +Variable (F : fieldType) (L0 : fieldExtType F) (A : pred L0) (K L : {subfield L0}). + +Hypothesis Asubr : subring_closed A. + +Definition integral l := exists p, [/\ p \is monic, p \is a polyOver A & root p l]. +Definition int_closed := {in A, forall a b, integral (a / b) -> (a / b) \in A}. +Definition int_closure l := l \in L /\ integral l. +Definition is_frac_field := {subset A <= K} /\ exists f, forall k, f k != 0 /\ + (k \in K -> f k \in A /\ f k * k \in A). + +Hypothesis AfracK : is_frac_field. + +Lemma frac_field_alg_int : exists f, forall l, [/\ f l != 0, f l \in A & integral (f l * l)]. +Proof. +have [Aid _ Amcl] := Asubr; have Amulr : mulr_closed A := Asubr. +have [AsubK [f /all_and2-[fH0 /(_ _)/all_and2-/all_and2-[fHa fHk]]]] := AfracK. +pose g := fun l => let p := minPoly K l in \prod_(i < size p) f p`_i; exists g => l. +pose p := minPoly K l; pose n := (size p).-1. +pose s := mkseq (fun i => p`_i * (g l) ^+ (n - i)%N) (size p). +have kI (i : 'I_(size p)) : p`_i \in K by apply/all_nthP => //; apply/minPolyOver. +have glA : g l \in A by rewrite/g; elim/big_ind: _ => // i _; apply/fHa. +have pmon: p`_n = 1 by have /monicP := monic_minPoly K l. +have an1: nth 0 s n = 1 by rewrite /n nth_mkseq ?pmon ?mul1r ?subnn ?size_minPoly. +have eqPs: (Poly s) = s :> seq L0. + by rewrite (PolyK (c := 0)) // -nth_last size_mkseq an1 oner_neq0. +have ilen i : i < size p -> i <= n by move => iB; rewrite /n -ltnS prednK // size_minPoly. +split => //; first by apply/prodf_neq0 => i _. +exists (Poly s); split; last first; last by rewrite monicE lead_coefE eqPs // size_mkseq an1. + rewrite /root -(mulr0 ((g l) ^+ n)); have <- := minPolyxx K l. + rewrite !horner_coef eqPs size_mkseq big_distrr; apply/eqP/eq_bigr => i _. + rewrite nth_mkseq // exprMn //=; rewrite !mulrA; congr (_ * _); rewrite -mulrA mulrC. + by congr (_ * _); rewrite -exprD subnK ?ilen. +apply/(all_nthP 0) => i; rewrite eqPs size_mkseq => iB; rewrite nth_mkseq //. + have := ilen _ iB; rewrite leq_eqVlt => /orP. + case; first by move /eqP ->; rewrite subnn pmon mulr1. + rewrite -subn_gt0 => {pmon ilen eqPs an1} /prednK <-; rewrite exprS mulrA /= Amcl ?rpredX //. + rewrite /g (bigD1 (Ordinal iB)) //= mulrA; apply/Amcl. + by rewrite mulrC; apply/fHk/(kI (Ordinal iB)). + by rewrite rpred_prod => // j _; apply/fHa. +Qed. + +Lemma int_clos_incl a : a \in A -> integral a. +Proof. +move=> ainA; exists ('X - a%:P); rewrite monicXsubC root_XsubC. +rewrite polyOverXsubC => //; by exact Asubr. +Qed. + +Lemma intPl (I : eqType) G (r : seq I) l : has (fun x => G x != 0) r -> + (forall e, e \in r -> {f | \sum_(e' <- r) f e' * G e' = l * G e & forall e', f e' \in A}) -> + integral l. +Proof. +have Aaddr : addr_closed A := Asubr; have Amulr : mulr_closed A := Asubr. +have Aoppr : oppr_closed A := Asubr; have [Aid _ _] := Asubr. +move => rn gen; pose s := in_tuple r; pose g j := gen (tnth s j) (mem_tnth j s). +pose f j := sval (g j); pose fH j := svalP (g j). +pose M := \matrix_(i, j < size r) f j (tnth s i). +exists (char_poly M); rewrite char_poly_monic; split => //. + apply/rpred_sum => p _; apply/rpredM; first by apply/rpredX; rewrite rpredN polyOverC. + apply/rpred_prod => i _; rewrite !mxE /= rpredB ?rpredMn ?polyOverX ?polyOverC ?/f //. + by have [_ fH2] := fH (perm.PermDef.fun_of_perm p i). +rewrite -eigenvalue_root_char; apply/eigenvalueP; move: rn => /hasP[x] /(nthP x)[k kB <- xn]. +exists (\row_(i < size r) G (tnth s i)); last first. + move: xn; apply/contra => /eqP/matrixP-v0; have := v0 0 (Ordinal kB). + by rewrite !mxE (tnth_nth x) => <-. +rewrite -rowP => j; rewrite !mxE; have [fH1 _] := fH j; rewrite -fH1 (big_nth x) big_mkord. +by apply/eq_bigr => /= i _; rewrite /M !mxE (tnth_nth x) mulrC. +Qed. + +Lemma intPr l : integral l -> exists r : seq L0, + [/\ r != nil, all A r & \sum_(i < size r) r`_i * l ^+ i = l ^+ (size r)]. +Proof. +move => [p [pm pA pr]]; pose n := size p; pose r := take n.-1 (- p). +have ps : n > 1. + rewrite ltnNge; apply/negP => /size1_polyC pc; rewrite pc in pr pm => {pc}. + move: pr => /rootP; rewrite hornerC => pc0. + by move: pm; rewrite monicE lead_coefC pc0 eq_sym oner_eq0. +have rs : size r = n.-1 by rewrite /r size_takel // size_opp leq_pred. +exists r; split. + apply/eqP => /nilP; rewrite /nilp /r size_takel; last by rewrite size_opp leq_pred. + by rewrite -subn1 subn_eq0 leqNgt ps. + have : - p \is a polyOver A by rewrite rpredN //; exact Asubr. + by move => /allP-popA; apply/allP => x /mem_take /popA. +move: pr => /rootP; rewrite horner_coef -(prednK (n := size p)); last by rewrite ltnW. +rewrite big_ord_recr /= rs; have := monicP pm; rewrite /lead_coef => ->; rewrite mul1r => /eqP. +rewrite addrC addr_eq0 -sumrN => /eqP => ->; apply/eq_bigr => i _; rewrite /r nth_take //. +by rewrite coefN mulNr. +Qed. + +Lemma int_subring_closed a b : integral a -> integral b -> + integral (a - b) /\ integral (a * b). +Proof. +have [A0 _ ] := (Asubr : zmod_closed A); have [A1 Asubr2 Amulr2] := Asubr. +move => /intPr[ra [/negbTE-ran raA raS]] /intPr[rb [/negbTE-rbn rbA rbS]]. +pose n := size ra; pose m := size rb; pose r := Finite.enum [finType of 'I_n * 'I_m]. +pose G (z : 'I_n * 'I_m) := let (k, l) := z in a ^ k * b ^l. +have [nz mz] : 0 < n /\ 0 < m. + by rewrite !lt0n; split; apply/negP; move => /nilP/eqP; rewrite ?ran ?rbn. +have rnn : has (fun x => G x != 0) r. + apply/hasP; exists (Ordinal nz, Ordinal mz); first by rewrite /r -enumT mem_enum. + by rewrite /G mulr1 oner_neq0. +pose h s i : 'I_(size s) -> L0 := fun k => if (i != size s) then (i == k)%:R else s`_k. +pose f i j (z : 'I_n * 'I_m) : L0 := let (k, l) := z in h ra i k * h rb j l. +have fA i j : forall z, f i j z \in A. + have hA s k l : all A s -> h s k l \in A. + move => /allP-sa; rewrite /h; case (eqVneq k (size s)) => [/eqP ->|->]. + by apply/sa/mem_nth. + by case (eqVneq k l) => [/eqP ->|/negbTE ->]. + by move => [k l]; rewrite /f; apply/Amulr2; apply/hA. +have fS i j : (i <= n) -> (j <= m) -> \sum_(z <- r) f i j z * G z = a ^ i * b ^ j. + have hS s k c : (k <= size s) -> \sum_(l < size s) s`_l * c ^ l = c ^ (size s) -> + \sum_(l < size s) h s k l * c ^ l = c ^ k. + move => kB sS; rewrite /h; case (eqVneq k (size s)) => [->|kn {sS}]; first by rewrite eqxx. + rewrite kn; rewrite leq_eqVlt (negbTE kn) /= in kB => {kn}. + rewrite (bigD1 (Ordinal kB)) //= eqxx mul1r /= -[RHS]addr0; congr (_ + _). + by apply/big1 => l; rewrite eq_sym => kl; have : k != l := kl => /negbTE ->; rewrite mul0r. + move => iB jB; rewrite -(hS ra i a) // -(hS rb j b) // mulr_suml. + rewrite (eq_bigr (fun k => \sum_(l < m) (h ra i k * a ^ k) * (h rb j l * b ^ l))). + rewrite pair_bigA; apply eq_bigr => [[k l] _]; rewrite !mulrA; congr (_ * _). + by rewrite -!mulrA [in h rb j l * a ^ k] mulrC. + by move => k _; rewrite mulr_sumr. +pose fB i j z := f i.+1 j z - f i j.+1 z; pose fM i j z := f i.+1 j.+1 z. +have fBA i j z : fB i j z \in A by rewrite /fB Asubr2. +have fBM i j z : fM i j z \in A by rewrite /fM. +split; apply/(@intPl _ G r) => //= [[i j] _]; [exists (fB i j) | exists (fM i j)] => //. + rewrite /fB [in RHS]/G mulrBl mulrA -exprS [in b * (a ^ i * b ^ j)] mulrC -mulrA -exprSr. + rewrite -(fS _ _ (ltnW (ltn_ord i))) // -(fS _ _ _ (ltnW (ltn_ord j))) //. + by rewrite -sumrB; apply/eq_bigr => [[k l] _]; apply/mulrBl. +by rewrite /fM [in RHS]/G mulrA [in (a * b) * a ^ i] mulrC mulrA -exprSr -mulrA -exprS -!fS. +Qed. + +Lemma int_zmod_closed a b : integral a -> integral b -> integral (a - b). +Proof. by move => aI bI; have [Azmod] := int_subring_closed aI bI. Qed. + +Lemma int_mulr_closed a b : integral a -> integral b -> integral (a * b). +Proof. by move => aI bI; have [_] := int_subring_closed aI bI. Qed. + +End Integral. + +Section Trace. + +Variable (F : fieldType) (L0 : fieldExtType F) (A : pred L0) (L : {subfield L0}). + +Implicit Types k l : L0. + +Definition tr : L0 -> L0 -> F := fun l k => + let X := vbasis L in + let M := \matrix_(i, j) coord X i (l * k * X`_j) + in \tr M. + +Fact tr_is_scalar l : scalar (tr l). +Proof. +move => c a b; rewrite /tr -!linearP /=; congr (\tr _); apply/matrixP => i j; rewrite !mxE. +by rewrite mulrDr mulrDl linearD /= -scalerAr -scalerAl linearZ. +Qed. + +Canonical tr_additive l := Additive (@tr_is_scalar l). +Canonical tr_linear l := AddLinear (@tr_is_scalar l). + +Lemma tr_sym : commutative tr. +Proof. by move => a b; rewrite /tr mulrC. Qed. + +Hypothesis Asubr : subring_closed A. +Hypothesis Aint : int_closed A. +Hypothesis Afrac : is_frac_field A 1%AS. + +Lemma tr_int k l : integral A k -> integral A l -> (tr k l)%:A \in A. +Proof. admit. Qed. + +Section NDeg. + +Variable (vT : vectType F) (rT : ringType) (Q : vT -> vT -> rT) (V : {vspace vT}). + +Definition ndeg := forall (l : vT), l != 0 -> l \in V -> exists (k : vT), k \in V /\ Q l k != 0. + +End NDeg. + +Variable (U : {vspace L0}). +Let m := \dim U. +Variable (X : m.-tuple L0). + +Lemma dual_basis_def : + {Y : m.-tuple L0 | ndeg tr U -> basis_of U X -> basis_of U Y /\ + forall (i : 'I_m), tr X`_i Y`_i = 1 /\ + forall (j : 'I_m), j != i -> tr X`_i Y`_j = 0}. +Proof. +pose Uv := subvs_vectType U; pose Fv := subvs_FalgType (1%AS : {aspace L0}); +pose HomV := [vectType _ of 'Hom(Uv, Fv)]. +pose tr_sub : Uv -> Uv -> Fv := fun u v => (tr (vsval u) (vsval v))%:A. +have HomVdim : \dim {:HomV} = m by rewrite dimvf /Vector.dim /= /Vector.dim /= dimv1 muln1. +have [f fH] : {f : 'Hom(Uv, HomV) | forall u, f u =1 tr_sub u}. + have lf1 u : linear (tr_sub u) by move => c x y; rewrite /tr_sub linearP scalerDl scalerA. + have lf2 : linear (fun u => linfun (Linear (lf1 u))). + move => c x y; rewrite -lfunP => v; rewrite add_lfunE scale_lfunE !lfunE /= /tr_sub. + by rewrite tr_sym linearP scalerDl scalerA /=; congr (_ + _); rewrite tr_sym. + by exists (linfun (Linear lf2)) => u v; rewrite !lfunE. +have [Xdual XdualH] : {Xdual : m.-tuple HomV | + forall (i : 'I_m) u, Xdual`_i u = (coord X i (vsval u))%:A}. + have lg (i : 'I_m) : linear (fun u : Uv => (coord X i (vsval u))%:A : Fv). + by move => c x y; rewrite linearP /= scalerDl scalerA. + exists (mktuple (fun i => linfun (Linear (lg i)))) => i u. + by rewrite -tnth_nth tnth_mktuple !lfunE. +have [finv finvH] : {finv : 'Hom(HomV, L0) | finv =1 vsval \o (f^-1)%VF}. + by exists (linfun vsval \o f^-1)%VF => u; rewrite comp_lfunE lfunE. +pose Y := map_tuple finv Xdual; exists Y => Und Xb. +have Ydef (i : 'I_m) : Y`_i = finv Xdual`_i by rewrite -!tnth_nth tnth_map. +have XiU (i : 'I_m) : X`_i \in U by apply/(basis_mem Xb)/mem_nth; rewrite size_tuple. +have Xii (i : 'I_m) : coord X i X`_i = 1%:R. + by rewrite coord_free ?eqxx //; exact (basis_free Xb). +have Xij (i j : 'I_m) : j != i -> coord X i X`_j = 0%:R. + by rewrite coord_free; [move => /negbTE -> | exact (basis_free Xb)]. +have Xdualb : basis_of fullv Xdual. + suffices Xdualf : free Xdual. + rewrite /basis_of Xdualf andbC /= -dimv_leqif_eq ?subvf // eq_sym HomVdim. + by move: Xdualf; rewrite /free => /eqP => ->; rewrite size_tuple. + apply/freeP => k sX i. + suffices: (\sum_(i < m) k i *: Xdual`_i) (vsproj U X`_i) = (k i)%:A. + by rewrite sX zero_lfunE => /esym /eqP; rewrite scaler_eq0 oner_eq0 orbF => /eqP. + rewrite sum_lfunE (bigD1 i) //= scale_lfunE XdualH vsprojK // Xii. + rewrite scaler_nat -[RHS]addr0; congr (_ + _); apply/big1 => j; rewrite eq_sym => ineqj. + by rewrite scale_lfunE XdualH vsprojK ?Xij // scaler_nat scaler0. +have finj : (lker f = 0)%VS. + apply/eqP; rewrite -subv0; apply/subvP=> u; rewrite memv_ker memv0 => /eqP-f0. + apply/contraT => un0; have {un0} [k [kiU /negP[]]] := Und (vsval u) un0 (subvsP u). + have /eqP := fH u (vsproj U k). + by rewrite /tr_sub vsprojK // f0 zero_lfunE eq_sym scaler_eq0 oner_eq0 orbF. +have flimg : limg f = fullv. + apply/eqP; rewrite -dimv_leqif_eq ?subvf // limg_dim_eq; last by rewrite finj capv0. + by rewrite HomVdim dimvf /Vector.dim. +have finvK : cancel finv (f \o vsproj U). + by move => u; rewrite finvH /= vsvalK; apply/limg_lfunVK; rewrite flimg memvf. +have finv_inj : (lker finv = 0)%VS by apply/eqP/lker0P/(can_inj finvK). +have finv_limg : limg finv = U. + apply/eqP; rewrite -dimv_leqif_eq; first by rewrite limg_dim_eq ?HomVdim ?finv_inj ?capv0. + by apply/subvP => u /memv_imgP [h _] ->; rewrite finvH subvsP. +have Xt (i j : 'I_m) : (f \o vsproj U) Y`_j (vsproj U X`_i) = (tr Y`_j X`_i)%:A. + by rewrite fH /tr_sub !vsprojK // Ydef finvH subvsP. +have Xd (i j : 'I_m) : (f \o vsproj U) Y`_j (vsproj U X`_i) = Xdual`_j (vsproj U X`_i). + by rewrite Ydef finvK. +have Ainj := fmorph_inj [rmorphism of in_alg Fv]. +split => [| i]; first by rewrite -{1}finv_limg limg_basis_of // capfv finv_inj. +split => [| j]; first by have := Xt i i; rewrite tr_sym Xd XdualH vsprojK // Xii => /Ainj. +by rewrite eq_sym => inj; have := Xt i j; rewrite tr_sym Xd XdualH vsprojK // Xij // => /Ainj. +Qed. + +Definition dual_basis : m.-tuple L0 := sval dual_basis_def. + +Hypothesis Und : ndeg tr U. +Hypothesis Xb : basis_of U X. + +Lemma dualb_basis : basis_of U dual_basis. +Proof. have [Yb _] := svalP dual_basis_def Und Xb; exact Yb. Qed. + +Lemma dualb_orth : + forall (i : 'I_m), tr X`_i dual_basis`_i = 1 /\ + forall (j : 'I_m), j != i -> tr X`_i dual_basis`_j = 0. +Proof. by have [_] := svalP dual_basis_def Und Xb. Qed. + +End Trace. + +Section TraceFieldOver. + +Variable (F : fieldType) (L0 : fieldExtType F) (A : pred L0) (K L : {subfield L0}). + +Implicit Types k l : L0. + +Let K' := subvs_fieldType K. +Let L0' := fieldOver_fieldExtType K. + +Definition trK : L0 -> L0 -> K' := tr (aspaceOver K L). + +Lemma trK_ndeg (U : {aspace L0}) : (K <= U)%VS -> + (ndeg trK U <-> ndeg (tr (aspaceOver K L)) (aspaceOver K U)). +Proof. +move => UsubL; have UU' : aspaceOver K U =i U := mem_aspaceOver UsubL. +split => [ndK l lnz | nd l lnz]. + by rewrite UU' => liU; have [k] := ndK l lnz liU; exists k; rewrite UU'. +by rewrite -UU' => liU'; have [k] := nd l lnz liU'; exists k; rewrite -UU'. +Qed. + +Hypothesis Asubr : subring_closed A. +Hypothesis Aint : int_closed A. +Hypothesis Afrac : is_frac_field A K. +Hypothesis AsubL : {subset A <= L}. + +Lemma trK_int k l : integral A k -> integral A l -> ((trK k l)%:A : L0') \in A. +Proof. admit. Qed. + +End TraceFieldOver. + +Section BasisLemma. + +Section Modules. + +Variable (F : fieldType) (L0 : fieldExtType F) (A : pred L0). + +Implicit Types M N : L0 -> Prop. + +Definition module M := M 0 /\ forall a k l, a \in A -> M k -> M l -> M (a * k - l). +Definition span_mod X m := exists2 r : (size X).-tuple L0, + all A r & m = \sum_(i < size X) r`_i * X`_i. +Definition submod M N := forall m, M m -> N m. +Definition basis_of_mod M X := free X /\ submod M (span_mod X) /\ forall m, m \in X -> M m. +Definition ideal N := submod N A /\ module N. +Definition PID := forall (N : L0 -> Prop), ideal N -> + exists2 a, N a & forall v, N v -> exists2 d, d \in A & d * a = v. + +Variable L : {subfield L0}. + +Hypothesis Asubr : subring_closed A. +Hypothesis AsubL : {subset A <= L}. + +Lemma int_mod_closed : module (int_closure A L). +Proof. +have [A0 _] : zmod_closed A := Asubr; split. + by rewrite /int_closure mem0v; split => //; apply/int_clos_incl. +move => a k l aA [kI kL] [lI lL]; split; first by rewrite rpredB ?rpredM //; apply/AsubL. +by apply/int_zmod_closed => //; apply/int_mulr_closed => //; apply/int_clos_incl. +Qed. + +End Modules. + +Variable (F0 : fieldType) (E : fieldExtType F0) (I : pred E) (Ifr K : {subfield E}). + +Hypothesis Isubr : subring_closed I. +Hypothesis Iint : int_closed I. +Hypothesis Ipid : PID I. +Hypothesis Ifrac : is_frac_field I Ifr. +Hypothesis IsubK : {subset I <= K}. +Hypothesis Knd : ndeg (trK Ifr K) K. + +Lemma basis_lemma : exists X : (\dim_Ifr K).-tuple E, basis_of_mod I (int_closure I K) X. +Proof. +suffices FisK (F : fieldType) (L0 : fieldExtType F) (A : pred L0) (L : {subfield L0}) : + subring_closed A -> int_closed A -> PID A -> is_frac_field A 1 -> ndeg (tr L) L -> + exists2 X, size X == \dim L & basis_of_mod A (int_closure A L) X. + have [Isub [f /all_and2[fH0 fHk]]] := Ifrac; pose F := subvs_fieldType Ifr; + pose L0 := fieldOver_fieldExtType Ifr; pose L := aspaceOver Ifr K. + have Ifrsub : (Ifr <= K)%VS. + apply/subvP=> x /fHk-[fHx fHxx]; rewrite -(mulKf (fH0 x) x). + by apply/memvM; rewrite ?memvV; apply/IsubK. + have LK : L =i K := mem_aspaceOver Ifrsub; have Lnd : ndeg (tr L) L by rewrite -trK_ndeg. + have Ifrac1 : is_frac_field (I : pred L0) 1. + split; first by move => a; rewrite /= trivial_fieldOver; apply/Isub. + by exists f => k; split => //; rewrite trivial_fieldOver => /fHk. + have [X Xsize [Xf [Xs Xi]]] := FisK _ L0 _ _ Isubr Iint Ipid Ifrac1 Lnd. + rewrite -dim_aspaceOver => //; have /eqP <- := Xsize; exists (in_tuple X); split; last first. + split => m; last by move => /Xi; rewrite /int_closure LK. + by rewrite /int_closure -LK; move => /Xs. + move: Xf; rewrite -{1}(in_tupleE X); move => /freeP-XfL0; apply/freeP => k. + have [k' kk'] : exists k' : 'I_(size X) -> F, forall i, (k i)%:A = vsval (k' i). + by exists (fun i => vsproj Ifr (k i)%:A) => i; rewrite vsprojK ?rpredZ ?mem1v. + pose Ainj := fmorph_inj [rmorphism of in_alg E]. + move => kS i; apply/Ainj => {Ainj} /=; rewrite scale0r kk'; apply/eqP. + rewrite raddf_eq0; last by apply/subvs_inj. + by apply/eqP/XfL0; rewrite -{3}kS => {i}; apply/eq_bigr => i _; rewrite -[RHS]mulr_algl kk'. +move => Asubr Aint Apid Afrac1 Lnd; pose n := \dim L; have Amulr : mulr_closed A := Asubr. +have [A0 _] : zmod_closed A := Asubr; have [Asub1 _] := Afrac1. +have AsubL : {subset A <= L} by move => a /Asub1; exact (subvP (sub1v L) a). +have [b1 [b1B b1H]] : exists (b1 : n.-tuple L0), [/\ basis_of L b1 & + forall i : 'I_n, integral A b1`_i]. + pose b0 := vbasis L; have [f /all_and3-[fH0 fHa fHi]] := frac_field_alg_int Asubr Afrac1. + pose d := \prod_(i < n) f b0`_i; pose b1 := map_tuple (amulr d) b0. + exists b1; split; last first => [i|]. + rewrite (nth_map 0) /d; last by rewrite size_tuple. + rewrite lfunE /= (bigD1 i) //= mulrA; apply/int_mulr_closed => //; first by rewrite mulrC. + by apply/int_clos_incl => //; rewrite rpred_prod. + have dun : d \is a GRing.unit by rewrite unitfE /d; apply/prodf_neq0 => i _. + have lim : (amulr d @: L = L)%VS. + have dinA : d \in A by rewrite rpred_prod. + rewrite limg_amulr; apply/eqP; rewrite -dimv_leqif_eq; first by rewrite dim_cosetv_unit. + by apply/prodv_sub => //; apply/AsubL. + rewrite -lim limg_basis_of //; last by apply/vbasisP. + by have /eqP -> := lker0_amulr dun; rewrite capv0. +have [b2 [/andP[/eqP-b2s b2f] b2H]] : exists (b2 : n.-tuple L0), [/\ basis_of L b2 & + forall b, b \in L -> integral A b -> forall i, (coord b2 i b)%:A \in A]. + pose b2 := dual_basis L b1; have b2B := dualb_basis Lnd b1B; exists b2; rewrite b2B. + split => // b biL bint i; suffices <-: tr L b1`_i b = coord b2 i b by rewrite tr_int. + have -> : tr L b1`_i b = \sum_(j < n) coord b2 j b * tr L b1`_i b2`_j. + by rewrite {1}(coord_basis b2B biL) linear_sum; apply/eq_bigr => j _; rewrite linearZ. + rewrite (bigD1 i); have [oi oj //] := dualb_orth Lnd b1B i; rewrite /= oi mulr1 -[RHS]addr0. + by congr (_ + _); apply/big1 => j jneqi; rewrite (oj j jneqi) mulr0. +have Mbasis k (X : k.-tuple L0) M : free X -> module A M -> submod M (span_mod A X) -> + exists B, basis_of_mod A M B. + move: k X M; elim => [X M _ _ Ms | k IH X M Xf [M0 Mm] Ms]. + by exists [::]; rewrite /basis_of_mod nil_free; move: Ms; rewrite tuple0. + pose X1 := [tuple of behead X]; pose v := thead X. + pose M1 := fun m => M m /\ coord X ord0 m = 0. + pose M2 := fun (a : L0) => exists2 m, M m & (coord X ord0 m)%:A = a. + have scr r m : r \in A -> exists c, r * m = c *: m. + by move => /Asub1/vlineP[c ->]; exists c; rewrite mulr_algl. + have span_coord m : M m -> exists r : (k.+1).-tuple L0, + [/\ all A r, m = \sum_(i < k.+1) r`_i * X`_i & forall i, (coord X i m)%:A = r`_i]. + have seqF (s : seq L0) : all A s -> exists s', s = [seq c%:A | c <- s']. + elim: s => [_| a l IHl /= /andP[/Asub1/vlineP[c ->]]]; first by exists [::]. + by move => /IHl[s' ->]; exists (c :: s'). + move => mM; have := Ms m mM; rewrite /span_mod !size_tuple; move => [r rA rS]. + exists r; split => //; have [rF rFr] := seqF r rA => {seqF}; rewrite rFr in rA. + have rFs : size rF = k.+1 by rewrite -(size_tuple r) rFr size_map. + have -> : m = \sum_(i < k.+1) rF`_i *: X`_i. + by rewrite rS; apply/eq_bigr => i _; rewrite rFr (nth_map 0) ?rFs // mulr_algl. + by move => i; rewrite coord_sum_free // rFr (nth_map 0) ?rFs. + have [B1 [B1f [B1s B1A]]] : exists B1, basis_of_mod A M1 B1. + have X1f : free X1 by move: Xf; rewrite (tuple_eta X) free_cons => /andP[_]. + apply/(IH X1) => //. + rewrite /module /M1 linear0; split => // a x y aA [xM xfc0] [yM yfc0]. + have := Mm a x y aA xM yM; move: aA => /Asub1/vlineP[r] ->; rewrite mulr_algl => msc. + by rewrite /M1 linearB linearZ /= xfc0 yfc0 subr0 mulr0. + move => m [mM mfc0]; have := span_coord m mM; move => [r [rA rS rC]]. + move: mfc0 (rC 0) ->; rewrite scale0r; move => r0; rewrite /span_mod size_tuple. + exists [tuple of behead r]; first by apply/allP => a /mem_behead/(allP rA). + by rewrite rS big_ord_recl -r0 mul0r add0r; apply/eq_bigr => i _; rewrite !nth_behead. + have [a [w wM wC] aG] : exists2 a, M2 a & forall v, M2 v -> exists2 d, d \in A & d * a = v. + apply/Apid; split. + move => c [m mM <-]; have := span_coord m mM; move => [r [/all_nthP-rA _ rC]]. + by move: rC ->; apply/rA; rewrite size_tuple. + split; first by exists 0 => //; rewrite linear0 scale0r. + move => c x y cA [mx mxM mxC] [my myM myC]; have := Mm c mx my cA mxM myM. + move: cA => /Asub1/vlineP[r] ->; rewrite !mulr_algl => mC. + by exists (r *: mx - my) => //; rewrite linearB linearZ /= scalerBl -scalerA mxC myC. + pose Ainj := fmorph_inj [rmorphism of in_alg L0]. + have mcM1 m : M m -> exists2 d, d \in A & d * a = (coord X 0 m)%:A. + by move => mM; apply/aG; exists m. + case: (eqVneq a 0) => [| an0]. + exists B1; split => //; split => [m mM |]; last by move => m /B1A[mM]. + apply/B1s; split => //; apply/Ainj => /=; have [d _ <-] := mcM1 m mM. + by rewrite a0 mulr0 scale0r. + exists (w :: B1); split. + rewrite free_cons B1f andbT; move: an0; apply/contra; move: wC <-. + rewrite -(in_tupleE B1); move => /coord_span ->; apply/eqP. + rewrite linear_sum big1 ?scale0r => //= i _; rewrite linearZ /=. + by have [_] := B1A B1`_i (mem_nth 0 (ltn_ord _)) => ->; rewrite mulr0. + split => [m mM | m]; last by rewrite in_cons; move => /orP; case => [/eqP ->|/B1A[mM]]. + have [d dA dam] := mcM1 m mM; have mdwM1 : M1 (m - d * w). + split; [have Mdwm := Mm d w m dA wM mM; have := Mm _ _ _ A0 Mdwm Mdwm |]. + by rewrite mul0r sub0r opprB. + move: dA dam => /Asub1/vlineP[r] -> {d}; rewrite !mulr_algl linearB linearZ /= => rac. + by apply/Ainj => /=; rewrite scalerBl -scalerA wC rac subrr scale0r. + have [r rA rS] := B1s _ mdwM1; exists [tuple of d :: r]; first by rewrite /= rA andbT. + by move: rS => /eqP; rewrite subr_eq addrC => /eqP ->; rewrite /= big_ord_recl. +have [X Xb] : exists X, basis_of_mod A (int_closure A L) X. + apply/(Mbasis _ b2 _ b2f) => [| m [mL mI]]; first by apply/int_mod_closed. + pose r : n.-tuple L0 := [tuple (coord b2 i m)%:A | i < n]; rewrite /span_mod size_tuple. + exists r; have rci (i : 'I_n) : r`_i = (coord b2 i m)%:A by rewrite -tnth_nth tnth_mktuple. + apply/(all_nthP 0) => i; rewrite size_tuple; move => iB. + by have -> := rci (Ordinal iB); apply/b2H. + move: mL; rewrite -b2s; move => /coord_span ->; apply/eq_bigr => i _. + by rewrite rci mulr_algl. +exists X => //; move: Xb => [/eqP-Xf [Xs Xg]]; rewrite -Xf eqn_leq; apply/andP; split. + by apply/dimvS/span_subvP => m /Xg[mL _]. +have /andP[/eqP-b1s _] := b1B; rewrite -b1s; apply/dimvS/span_subvP => b /tnthP-[i ->] {b}. +rewrite (tnth_nth 0); have [r /all_tnthP-rA ->] : span_mod A X b1`_i. + by apply/Xs; rewrite /int_closure (basis_mem b1B) ?mem_nth ?size_tuple => //. +apply/rpred_sum => j _; have := rA j; rewrite (tnth_nth 0); move => /Asub1/vlineP[c ->]. +by rewrite mulr_algl; apply/rpredZ/memv_span/mem_nth. +Qed. + +End BasisLemma.
\ No newline at end of file diff --git a/mathcomp/attic/all.v b/mathcomp/attic/all.v new file mode 100644 index 0000000..41badbb --- /dev/null +++ b/mathcomp/attic/all.v @@ -0,0 +1,9 @@ +Require Export algnum_basic. +Require Export amodule. +Require Export fib. +Require Export forms. +Require Export galgebra. +Require Export multinom. +Require Export mxtens. +Require Export quote. +Require Export tutorial. diff --git a/mathcomp/attic/amodule.v b/mathcomp/attic/amodule.v new file mode 100644 index 0000000..f23ed60 --- /dev/null +++ b/mathcomp/attic/amodule.v @@ -0,0 +1,417 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrbool ssrfun eqtype fintype finfun finset ssralg. +Require Import bigop seq tuple choice ssrnat prime ssralg fingroup pgroup. +Require Import zmodp matrix vector falgebra galgebra. + +(*****************************************************************************) +(* * Module over an algebra *) +(* amoduleType A == type for finite dimension module structure. *) +(* *) +(* v :* x == right product of the module *) +(* (M :* A)%VS == the smallest vector space that contains *) +(* {v :* x | v \in M & x \in A} *) +(* (modv M A) == M is a module for A *) +(* (modf f M A) == f is a module homomorphism on M for A *) +(*****************************************************************************) +(*****************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Open Local Scope ring_scope. + +Delimit Scope amodule_scope with aMS. + +Import GRing.Theory. + +Module AModuleType. +Section ClassDef. + +Variable R : ringType. +Variable V: vectType R. +Variable A: FalgType R. + +Structure mixin_of (V : vectType R) : Type := Mixin { + action: A -> 'End(V); + action_morph: forall x a b, action (a * b) x = action b (action a x); + action_linear: forall x , linear (action^~ x); + action1: forall x , action 1 x = x +}. + +Structure class_of (V : Type) : Type := Class { + base : Vector.class_of R V; + mixin : mixin_of (Vector.Pack _ base V) +}. +Local Coercion base : class_of >-> Vector.class_of. + +Implicit Type phA : phant A. + +Structure type phA : Type := Pack {sort : Type; _ : class_of sort; _ : Type}. +Local Coercion sort : type >-> Sortclass. + +Definition class phA (cT : type phA):= + let: Pack _ c _ := cT return class_of cT in c. +Definition clone phA T cT c of phant_id (@class phA cT) c := @Pack phA T c T. + +Definition pack phA V V0 (m0 : mixin_of (@Vector.Pack R _ V V0 V)) := + fun bT b & phant_id (@Vector.class _ (Phant R) bT) b => + fun m & phant_id m0 m => Pack phA (@Class V b m) V. + +Definition eqType phA cT := Equality.Pack (@class phA cT) cT. +Definition choiceType phA cT := choice.Choice.Pack (@class phA cT) cT. +Definition zmodType phA cT := GRing.Zmodule.Pack (@class phA cT) cT. +Definition lmodType phA cT := GRing.Lmodule.Pack (Phant R) (@class phA cT) cT. +Definition vectType phA cT := Vector.Pack (Phant R) (@class phA cT) cT. + +End ClassDef. + +Module Exports. +Coercion base : class_of >-> Vector.class_of. +Coercion mixin : class_of >-> mixin_of. +Coercion sort : type >-> Sortclass. + +Coercion eqType : type >-> Equality.type. +Canonical Structure eqType. +Coercion choiceType : type >-> Choice.type. +Canonical Structure choiceType. +Coercion zmodType : type >-> GRing.Zmodule.type. +Canonical Structure zmodType. +Coercion lmodType : type>-> GRing.Lmodule.type. +Canonical Structure lmodType. +Coercion vectType : type >-> Vector.type. +Canonical Structure vectType. + +Notation amoduleType A := (@type _ _ (Phant A)). +Notation AModuleType A m := (@pack _ _ (Phant A) _ _ m _ _ id _ id). +Notation AModuleMixin := Mixin. + +Bind Scope ring_scope with sort. +End Exports. + +End AModuleType. +Import AModuleType.Exports. + +Section AModuleDef. +Variables (F : fieldType) (A: FalgType F) (M: amoduleType A). + +Definition rmorph (a: A) := AModuleType.action (AModuleType.class M) a. +Definition rmul (a: M) (b: A) : M := rmorph b a. +Notation "a :* b" := (rmul a b): ring_scope. + +Implicit Types x y: A. +Implicit Types v w: M. +Implicit Types c: F. + +Lemma rmulD x: {morph (rmul^~ x): v1 v2 / v1 + v2}. +Proof. move=> *; exact: linearD. Qed. + +Lemma rmul_linear_proof : forall v, linear (rmul v). +Proof. by rewrite /rmul /rmorph; case: M => s [] b []. Qed. +Canonical Structure rmul_linear v := GRing.Linear (rmul_linear_proof v). + +Lemma rmulA v x y: v :* (x * y) = (v :* x) :* y. +Proof. exact: AModuleType.action_morph. Qed. + +Lemma rmulZ : forall c v x, (c *: v) :* x = c *: (v :* x). +Proof. move=> c v x; exact: linearZZ. Qed. + +Lemma rmul0 : left_zero 0 rmul. +Proof. move=> x; exact: linear0. Qed. + +Lemma rmul1 : forall v , v :* 1 = v. +Proof. by rewrite /rmul /rmorph; case: M => s [] b []. Qed. + +Lemma rmul_sum : forall I r P (f : I -> M) x, + \sum_(i <- r | P i) f i :* x = (\sum_(i <- r | P i) f i) :* x. +Proof. +by move=> I r P f x; rewrite -linear_sum. +Qed. + +Implicit Types vs: {vspace M}. +Implicit Types ws: {vspace A}. + +Lemma size_eprodv : forall vs ws, + size (allpairs rmul (vbasis vs) (vbasis ws)) == (\dim vs * \dim ws)%N. +Proof. by move=> *; rewrite size_allpairs !size_tuple. Qed. + +Definition eprodv vs ws := span (Tuple (size_eprodv vs ws)). +Local Notation "A :* B" := (eprodv A B) : vspace_scope. + +Lemma memv_eprod vs ws a b : a \in vs -> b \in ws -> a :* b \in (vs :* ws)%VS. +Proof. +move=> Ha Hb. +rewrite (coord_vbasis Ha) (coord_vbasis Hb). +rewrite linear_sum /=; apply: memv_suml => j _. +rewrite -rmul_sum; apply: memv_suml => i _ /=. +rewrite linearZ memvZ //= rmulZ memvZ //=. +apply: memv_span; apply/allpairsP; exists ((vbasis vs)`_i, (vbasis ws)`_j)=> //. +by rewrite !mem_nth //= size_tuple. +Qed. + +Lemma eprodvP : forall vs1 ws vs2, + reflect (forall a b, a \in vs1 -> b \in ws -> a :* b \in vs2) + (vs1 :* ws <= vs2)%VS. +Proof. +move=> vs1 ws vs2; apply: (iffP idP). + move=> Hs a b Ha Hb. + by apply: subv_trans Hs; exact: memv_eprod. +move=> Ha; apply/subvP=> v. +move/coord_span->; apply: memv_suml=> i _ /=. +apply: memvZ. +set u := allpairs _ _ _. +have: i < size u by rewrite (eqP (size_eprodv _ _)). +move/(mem_nth 0); case/allpairsP=> [[x1 x2] [I1 I2 ->]]. +by apply Ha; apply: vbasis_mem. +Qed. + +Lemma eprod0v: left_zero 0%VS eprodv. +Proof. +move=> vs; apply subv_anti; rewrite sub0v andbT. +apply/eprodvP=> a b; case/vlineP=> k1 -> Hb. +by rewrite scaler0 rmul0 mem0v. +Qed. + +Lemma eprodv0 : forall vs, (vs :* 0 = 0)%VS. +Proof. +move=> vs; apply subv_anti; rewrite sub0v andbT. +apply/eprodvP=> a b Ha; case/vlineP=> k1 ->. +by rewrite scaler0 linear0 mem0v. +Qed. + +Lemma eprodv1 : forall vs, (vs :* 1 = vs)%VS. +Proof. +case: (vbasis1 A) => k Hk He /=. +move=> vs; apply subv_anti; apply/andP; split. + apply/eprodvP=> a b Ha; case/vlineP=> k1 ->. + by rewrite linearZ /= rmul1 memvZ. +apply/subvP=> v Hv. +rewrite (coord_vbasis Hv); apply: memv_suml=> [] [i Hi] _ /=. +apply: memvZ. +rewrite -[_`_i]rmul1; apply: memv_eprod; last by apply: memv_line. +by apply: vbasis_mem; apply: mem_nth; rewrite size_tuple. +Qed. + +Lemma eprodvSl ws vs1 vs2 : (vs1 <= vs2 -> vs1 :* ws <= vs2 :* ws)%VS. +Proof. +move=> Hvs; apply/eprodvP=> a b Ha Hb; apply: memv_eprod=> //. +by apply: subv_trans Hvs. +Qed. + +Lemma eprodvSr vs ws1 ws2 : (ws1 <= ws2 -> vs :* ws1 <= vs :* ws2)%VS. +Proof. +move=> Hvs; apply/eprodvP=> a b Ha Hb; apply: memv_eprod=> //. +by apply: subv_trans Hvs. +Qed. + +Lemma eprodv_addl: left_distributive eprodv addv. +Proof. +move=> vs1 vs2 ws; apply subv_anti; apply/andP; split. + apply/eprodvP=> a b;case/memv_addP=> v1 Hv1 [v2 Hv2 ->] Hb. + by rewrite rmulD; apply: memv_add; apply: memv_eprod. +apply/subvP=> v; case/memv_addP=> v1 Hv1 [v2 Hv2 ->]. +apply: memvD. + move: v1 Hv1; apply/subvP; apply: eprodvSl; exact: addvSl. +move: v2 Hv2; apply/subvP; apply: eprodvSl; exact: addvSr. +Qed. + +Lemma eprodv_sumr vs ws1 ws2 : (vs :* (ws1 + ws2) = vs :* ws1 + vs :* ws2)%VS. +Proof. +apply subv_anti; apply/andP; split. + apply/eprodvP=> a b Ha;case/memv_addP=> v1 Hv1 [v2 Hv2 ->]. + by rewrite linearD; apply: memv_add; apply: memv_eprod. +apply/subvP=> v; case/memv_addP=> v1 Hv1 [v2 Hv2 ->]. +apply: memvD. + move: v1 Hv1; apply/subvP; apply: eprodvSr; exact: addvSl. +move: v2 Hv2; apply/subvP; apply: eprodvSr; exact: addvSr. +Qed. + +Definition modv (vs: {vspace M}) (al: {aspace A}) := + (vs :* al <= vs)%VS. + +Lemma mod0v : forall al, modv 0 al. +Proof. by move=> al; rewrite /modv eprod0v subvv. Qed. + +Lemma modv1 : forall vs, modv vs (aspace1 A). +Proof. by move=> vs; rewrite /modv eprodv1 subvv. Qed. + +Lemma modfv : forall al, modv fullv al. +Proof. by move=> al; exact: subvf. Qed. + +Lemma memv_mod_mul : forall ms al m a, + modv ms al -> m \in ms -> a \in al -> m :* a \in ms. +Proof. +move=> ms al m a Hmo Hm Ha; apply: subv_trans Hmo. +by apply: memv_eprod. +Qed. + +Lemma modvD : forall ms1 ms2 al , + modv ms1 al -> modv ms2 al -> modv (ms1 + ms2) al. +Proof. +move=> ms1 ms2 al Hm1 Hm2; rewrite /modv eprodv_addl. +apply: (subv_trans (addvS Hm1 (subvv _))). +exact: (addvS (subvv _) Hm2). +Qed. + +Lemma modv_cap : forall ms1 ms2 al , + modv ms1 al -> modv ms2 al -> modv (ms1:&: ms2) al. +Proof. +move=> ms1 ms2 al Hm1 Hm2. +by rewrite /modv subv_cap; apply/andP; split; + [apply: subv_trans Hm1 | apply: subv_trans Hm2]; + apply: eprodvSl; rewrite (capvSr,capvSl). +Qed. + +Definition irreducible ms al := + [/\ modv ms al, ms != 0%VS & + forall ms1, modv ms1 al -> (ms1 <= ms)%VS -> ms != 0%VS -> ms1 = ms]. + +Definition completely_reducible ms al := + forall ms1, modv ms1 al -> (ms1 <= ms)%VS -> + exists ms2, + [/\ modv ms2 al, (ms1 :&: ms2 = 0)%VS & (ms1 + ms2)%VS = ms]. + +Lemma completely_reducible0 : forall al, completely_reducible 0 al. +Proof. +move=> al ms1 Hms1; rewrite subv0; move/eqP->. +by exists 0%VS; split; [exact: mod0v | exact: cap0v | exact: add0v]. +Qed. + +End AModuleDef. + +Notation "a :* b" := (rmul a b): ring_scope. +Notation "A :* B" := (eprodv A B) : vspace_scope. + +Section HomMorphism. + +Variable (K: fieldType) (A: FalgType K) (M1 M2: amoduleType A). + +Implicit Types ms : {vspace M1}. +Implicit Types f : 'Hom(M1, M2). +Implicit Types al : {aspace A}. + +Definition modf f ms al := + all (fun p => f (p.1 :* p.2) == f p.1 :* p.2) + (allpairs (fun x y => (x,y)) (vbasis ms) (vbasis al)). + +Lemma modfP : forall f ms al, + reflect (forall x v, v \in ms -> x \in al -> f (v :* x) = f v :* x) + (modf f ms al). +Proof. +move=> f ms al; apply: (iffP idP)=> H; last first. + apply/allP=> [] [v x]; case/allpairsP=> [[x1 x2] [I1 I2 ->]]. + by apply/eqP; apply: H; apply: vbasis_mem. +move=> x v Hv Hx; rewrite (coord_vbasis Hv) (coord_vbasis Hx). +rewrite !linear_sum; apply: eq_big=> //= i _. +rewrite !linearZ /=; congr (_ *: _). +rewrite -!rmul_sum linear_sum; apply: eq_big=> //= j _. +rewrite rmulZ !linearZ /= rmulZ; congr (_ *: _). +set x1 := _`_ _; set y1 := _ `_ _. +case: f H => f /=; move/allP; move/(_ (x1,y1))=> HH. +apply/eqP; apply: HH; apply/allpairsP; exists (x1, y1). +by rewrite !mem_nth //= size_tuple. +Qed. + +Lemma modf_zero : forall ms al, modf 0 ms al. +Proof. by move=> ms al; apply/allP=> i _; rewrite !lfunE rmul0. Qed. + +Lemma modf_add : forall f1 f2 ms al, + modf f1 ms al -> modf f2 ms al -> modf (f1 + f2) ms al. +Proof. +move=> f1 f2 ms al Hm1 Hm2; apply/allP=> [] [v x]. +case/allpairsP=> [[x1 x2] [I1 I2 ->]]; rewrite !lfunE rmulD /=. +move/modfP: Hm1->; try apply: vbasis_mem=>//. +by move/modfP: Hm2->; try apply: vbasis_mem. +Qed. + +Lemma modf_scale : forall k f ms al, modf f ms al -> modf (k *: f) ms al. +Proof. +move=> k f ms al Hm; apply/allP=> [] [v x]. +case/allpairsP=> [[x1 x2] [I1 I2 ->]]; rewrite !lfunE rmulZ /=. +by move/modfP: Hm->; try apply: vbasis_mem. +Qed. + +Lemma modv_ker : forall f ms al, + modv ms al -> modf f ms al -> modv (ms :&: lker f) al. +Proof. +move=> f ms al Hmd Hmf; apply/eprodvP=> x v. +rewrite memv_cap !memv_ker. +case/andP=> Hx Hf Hv. +rewrite memv_cap (memv_mod_mul Hmd) // memv_ker. +by move/modfP: Hmf=> ->; rewrite // (eqP Hf) rmul0 eqxx. +Qed. + +Lemma modv_img : forall f ms al, + modv ms al -> modf f ms al -> modv (f @: ms) al. +Proof. +move=> f ms al Hmv Hmf; apply/eprodvP=> v x. +case/memv_imgP=> u Hu -> Hx. +move/modfP: Hmf<-=> //. +apply: memv_img. +by apply: (memv_mod_mul Hmv). +Qed. + +End HomMorphism. + +Section ModuleRepresentation. + +Variable (F: fieldType) (gT: finGroupType) + (G: {group gT}) (M: amoduleType (galg F gT)). +Hypothesis CG: ([char F]^'.-group G)%g. +Implicit Types ms : {vspace M}. + +Let FG := gaspace F G. +Local Notation " g %:FG " := (injG _ g). + +Lemma Maschke : forall ms, modv ms FG -> completely_reducible ms FG. +Proof. +move=> ms Hmv ms1 Hms1 Hsub; rewrite /completely_reducible. +pose act g : 'End(M) := rmorph M (g%:FG). +have actE: forall g v, act g v = v :* g%:FG by done. +pose f: 'End(M) := #|G|%:R^-1 *: + \sum_(i in G) (act (i^-1)%g \o projv ms1 \o act i)%VF. +have Cf: forall v x, x \in FG -> f (v :* x) = f v :* x. + move=> v x; case/memv_sumP=> g_ Hg_ ->. + rewrite !linear_sum; apply: eq_big => //= i Hi. + move: (Hg_ _ Hi); case/vlineP=> k ->. + rewrite !linearZ /=; congr (_ *: _). + rewrite /f /= !lfunE /= !sum_lfunE rmulZ /=; congr (_ *: _). + rewrite -rmul_sum (reindex (fun g => (i^-1 * g)%g)); last first. + by exists (fun g => (i * g)%g)=> h; rewrite mulgA (mulVg, mulgV) mul1g. + apply: eq_big=> g; first by rewrite groupMl // groupV. + rewrite !lfunE /= !lfunE /= !actE -rmulA=> Hig. + have Hg: g \in G by rewrite -[g]mul1g -[1%g](mulgV i) -mulgA groupM. + by rewrite -injGM // mulgA mulgV mul1g invMg invgK !injGM + ?groupV // rmulA. +have Himf: forall v, v \in ms1 -> f v = v. + move=> v Hv. + rewrite /f !lfunE /= sum_lfunE (eq_bigr (fun x => v)); last move=> i Hi. + by rewrite sumr_const -scaler_nat scalerA mulVf // ?scale1r // -?charf'_nat. + rewrite !lfunE /= !lfunE /= projv_id !actE; last first. + by rewrite (memv_mod_mul Hms1) //= /gvspace (bigD1 i) // memvE addvSl. + by rewrite -rmulA -injGM // ?groupV // mulgV rmul1. +have If: limg f = ms1. + apply: subv_anti; apply/andP; split; last first. + by apply/subvP=> v Hv; rewrite -(Himf _ Hv) memv_img // memvf. + apply/subvP=> i; case/memv_imgP=> x _ ->. + rewrite !lfunE memvZ //= sum_lfunE memv_suml=> // j Hj. + rewrite lfunE /= lfunE (memv_mod_mul Hms1) //; first by exact: memv_proj. + by rewrite memvE /= /gvspace (bigD1 (j^-1)%g) ?addvSl // groupV. +exists (ms :&: lker f)%VS; split. + - apply: modv_ker=> //; apply/modfP=> *; exact: Cf. + apply/eqP; rewrite -subv0; apply/subvP=> v; rewrite memv0. + rewrite !memv_cap; case/andP=> Hv1; case/andP=> Hv2 Hv3. + by move: Hv3; rewrite memv_ker Himf. +apply: subv_anti; rewrite subv_add Hsub capvSl. +apply/subvP=> v Hv. +have->: v = f v + (v - f v) by rewrite addrC -addrA addNr addr0. +apply: memv_add; first by rewrite -If memv_img // memvf. +rewrite memv_cap; apply/andP; split. + apply: memvB=> //; apply: subv_trans Hsub. + by rewrite -If; apply: memv_img; exact: memvf. +rewrite memv_ker linearB /= (Himf (f v)) ?subrr // /in_mem /= -If. +by apply: memv_img; exact: memvf. +Qed. + +End ModuleRepresentation. + +Export AModuleType.Exports. diff --git a/mathcomp/attic/fib.v b/mathcomp/attic/fib.v new file mode 100644 index 0000000..e002a72 --- /dev/null +++ b/mathcomp/attic/fib.v @@ -0,0 +1,340 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype. +Require Import bigop div prime finfun tuple ssralg zmodp matrix binomial. + +(*****************************************************************************) +(* This files contains the definitions of: *) +(* fib n == n.+1 th fibonacci number *) +(* *) +(* lucas n == n.+1 lucas number *) +(* *) +(* and some of their standard properties *) +(*****************************************************************************) + +Fixpoint fib_rec (n : nat) {struct n} : nat := + if n is n1.+1 then + if n1 is n2.+1 then fib_rec n1 + fib_rec n2 + else 1 + else 0. + +Definition fib := nosimpl fib_rec. + +Lemma fibE : fib = fib_rec. +Proof. by []. Qed. + +Lemma fib0 : fib 0 = 0. +Proof. by []. Qed. + +Lemma fib1 : fib 1 = 1. +Proof. by []. Qed. + +Lemma fibSS : forall n, fib n.+2 = fib n.+1 + fib n. +Proof. by []. Qed. + +Fixpoint lin_fib_rec (a b n : nat) {struct n} : nat := + if n is n1.+1 then + if n1 is n2.+1 + then lin_fib_rec b (b + a) n1 + else b + else a. + +Definition lin_fib := nosimpl lin_fib_rec. + +Lemma lin_fibE : lin_fib = lin_fib_rec. +Proof. by []. Qed. + +Lemma lin_fib0 : forall a b, lin_fib a b 0 = a. +Proof. by []. Qed. + +Lemma lin_fib1 : forall a b, lin_fib a b 1 = b. +Proof. by []. Qed. + +Lemma lin_fibSS : forall a b n, lin_fib a b n.+2 = lin_fib b (b + a) n.+1. +Proof. by []. Qed. + +Lemma lin_fib_alt : forall n a b, + lin_fib a b n.+2 = lin_fib a b n.+1 + lin_fib a b n. +Proof. +case=>//; elim => [//|n IHn] a b. +by rewrite lin_fibSS (IHn b (b + a)) lin_fibE. +Qed. + +Lemma fib_is_linear : fib =1 lin_fib 0 1. +Proof. +move=>n; elim: n {-2}n (leqnn n)=> [n|n IHn]. + by rewrite leqn0; move/eqP=>->. +case=>//; case=>// n0; rewrite ltnS=> ltn0n; rewrite fibSS lin_fib_alt. +by rewrite (IHn _ ltn0n) (IHn _ (ltnW ltn0n)). +Qed. + +Lemma fib_add : forall m n, + m != 0 -> fib (m + n) = fib m.-1 * fib n + fib m * fib n.+1. +Proof. +move=> m; elim: m {-2}m (leqnn m)=> [[] // _ |m IH]. +move=> m1; rewrite leq_eqVlt; case/orP=> [|Hm]; last first. + by apply: IH; rewrite -ltnS. +move/eqP->; case: m IH=> [|[|m]] IH n _. +- by case: n=> [|n] //; rewrite fibSS mul1n. +- by rewrite add2n fibSS addnC !mul1n. +rewrite 2!addSn fibSS -addSn !IH // addnA [fib _ * _ + _ + _]addnAC. +by rewrite -addnA -!mulnDl -!fibSS. +Qed. + +Theorem dvdn_fib: forall m n, m %| n -> fib m %| fib n. +Proof. +move=> m n; case/dvdnP=> n1 ->. +elim: {n}n1 m=> [|m IH] // [|n]; first by rewrite muln0. +by rewrite mulSn fib_add // dvdn_add //; [apply dvdn_mull | apply dvdn_mulr]. +Qed. + +Lemma fib_gt0 : forall m, 0 < m -> 0 < fib m. +Proof. +by elim=> [|[|m] IH _] //; rewrite fibSS addn_gt0 IH. +Qed. + +Lemma fib_smonotone : forall m n, 1 < m < n -> fib m < fib n. +Proof. +move=> m n; elim: n=> [|[|n] IH]; first by rewrite andbF. + by rewrite ltnNge leq_eqVlt orbC andbC; case: leq. +rewrite fibSS andbC; case/andP; rewrite leq_eqVlt; case/orP. + by rewrite eqSS; move/eqP=> -> H1m; rewrite -addn1 leq_add // fib_gt0. +by move=> H1m H2m; apply: ltn_addr; apply: IH; rewrite // H2m. +Qed. + +Lemma fib_monotone : forall m n, m <= n -> fib m <= fib n. +Proof. +move=> m n; elim: n=> [|[|n] IH]; first by case: m. + by case: m{IH}=> [|[]]. +rewrite fibSS leq_eqVlt; case/orP=>[|Hm]; first by move/eqP->. +by apply: (leq_trans (IH _)) => //; exact: leq_addr. +Qed. + +Lemma fib_eq1 : forall n, (fib n == 1) = ((n == 1) || (n == 2)). +Proof. +case=> [|[|[|n]]] //; case: eqP=> // Hm; have: 1 < 2 < n.+3 by []. +by move/fib_smonotone; rewrite Hm. +Qed. + +Lemma fib_eq : forall m n, + (fib m == fib n) = [|| m == n, (m == 1) && (n == 2) | (m == 2) && (n == 1)]. +Proof. +move=> m n; wlog: m n/ m <= n=> [HH|]. + case/orP: (leq_total m n)=> Hm; first by exact: HH. + by rewrite eq_sym HH // eq_sym ![(_ == 1) && _]andbC [(_ && _) || _] orbC. +rewrite leq_eqVlt; case/orP=>[|]; first by move/eqP->; rewrite !eqxx. +case: m=> [|[|m]] Hm. +- by move: (fib_gt0 _ Hm); rewrite orbF [0 == _]eq_sym !eqn0Ngt Hm; + case: (fib n). +- by rewrite eq_sym fib_eq1 orbF [1==_]eq_sym; case: eqP. +have: 1 < m.+2 < n by []. +move/fib_smonotone; rewrite ltn_neqAle; case/andP; move/negPf=> -> _. +case: n Hm=> [|[|n]] //;rewrite ltn_neqAle; case/andP; move/negPf=> ->. +by rewrite andbF. +Qed. + +Lemma fib_prime : forall p, p != 4 -> prime (fib p) -> prime p. +Proof. +move=> p Dp4 Pp. +apply/primeP; split; first by case: (p) Pp => [|[]]. +move=> d; case/dvdnP=> k Hp. +have F: forall u, (fib u == 1) = ((u == 1) || (u == 2)). + case=> [|[|[|n]]] //; case: eqP=> // Hm; have: 1 < 2 < n.+3 by []. + by move/fib_smonotone; rewrite Hm. +case/primeP: (Pp); rewrite Hp => _ Hf. +case/orP: (Hf _ (dvdn_fib _ _ (dvdn_mulr d (dvdnn k)))). + rewrite fib_eq1; case/orP; first by move/eqP->; rewrite mul1n eqxx orbT. + move/eqP=> Hk. + case/orP: (Hf _ (dvdn_fib _ _ (dvdn_mull k (dvdnn d)))). + rewrite fib_eq1; case/orP; first by move->. + by move/eqP=>Hd; case/negP: Dp4; rewrite Hp Hd Hk. + rewrite fib_eq; case/or3P; first by move/eqP<-; rewrite eqxx orbT. + by case/andP=>->. + by rewrite Hk; case: (d)=> [|[|[|]]]. +rewrite fib_eq; case/or3P; last by case/andP;move/eqP->; case: (d)=> [|[|]]. + rewrite -{1}[k]muln1; rewrite eqn_mul2l; case/orP; move/eqP=> HH. + by move: Pp; rewrite Hp HH. + by rewrite -HH eqxx. +by case/andP; move/eqP->; rewrite mul1n eqxx orbT. +Qed. + +Lemma fib_sub : forall m n, n <= m -> + fib (m - n) = if odd n then fib m.+1 * fib n - fib m * fib n.+1 + else fib m * fib n.+1 - fib m.+1 * fib n. +Proof. +elim=> [|m IH]; first by case=> /=. +case=> [|n Hn]; first by rewrite muln0 muln1 !subn0. +by rewrite -{2}[n.+1]add1n odd_add (addTb (odd n)) subSS IH //; case: odd; + rewrite !fibSS !mulnDr !mulnDl !subnDA !addKn. +Qed. + +Lemma gcdn_fib: forall m n, gcdn (fib m) (fib n) = fib (gcdn m n). +Proof. +move=> m n; apply: gcdn_def. +- by apply: dvdn_fib; exact: dvdn_gcdl. +- by apply: dvdn_fib; exact: dvdn_gcdr. +move=> d' Hdm Hdn. +case: m Hdm=> [|m Hdm]; first by rewrite gcdnE eqxx. +have F: 0 < m.+1 by []. +case: (egcdnP n F)=> km kn Hg Hl. +have->: gcdn m.+1 n = km * m.+1 - kn * n by rewrite Hg addKn. +rewrite fib_sub; last by rewrite Hg leq_addr. +by case: odd; apply: dvdn_sub; + try (by apply: (dvdn_trans Hdn); apply: dvdn_mull; + apply: dvdn_fib; apply: dvdn_mull); + apply: (dvdn_trans Hdm); apply: dvdn_mulr; + apply: dvdn_fib; apply: dvdn_mull. +Qed. + +Lemma coprimeSn_fib: forall n, coprime (fib n.+1) (fib n). +Proof. +by move=> n; move: (coprimeSn n); rewrite /coprime gcdn_fib; move/eqP->. +Qed. + +Fixpoint lucas_rec (n : nat) {struct n} : nat := + if n is n1.+1 then + if n1 is n2.+1 then lucas_rec n1 + lucas_rec n2 + else 1 + else 2. + +Definition lucas := nosimpl lucas_rec. + +Lemma lucasE : lucas = lucas_rec. +Proof. by []. Qed. + +Lemma lucas0 : lucas 0 = 2. +Proof. by []. Qed. + +Lemma lucas1 : lucas 1 = 1. +Proof. by []. Qed. + +Lemma lucasSS : forall n, lucas n.+2 = lucas n.+1 + lucas n. +Proof. by []. Qed. + +Lemma lucas_is_linear : lucas =1 lin_fib 2 1. +Proof. +move=>n; elim: n {-2}n (leqnn n)=> [n|n IHn]. + by rewrite leqn0; move/eqP=>->. +case=>//; case=>// n0; rewrite ltnS=> ltn0n; rewrite lucasSS lin_fib_alt. +by rewrite (IHn _ ltn0n) (IHn _ (ltnW ltn0n)). +Qed. + +Lemma lucas_fib: forall n, n != 0 -> lucas n = fib n.+1 + fib n.-1. +Proof. +move=> n; elim: n {-2}n (leqnn n)=> [[] // _ |n IH]. +move=> n1; rewrite leq_eqVlt; case/orP=> [|Hn1]; last first. + by apply: IH; rewrite -ltnS. +move/eqP->; case: n IH=> [|[|n] IH _] //. +by rewrite lucasSS !IH // addnCA -addnA -fibSS addnC. +Qed. + +Lemma lucas_gt0 : forall m, 0 < lucas m. +Proof. +by elim=> [|[|m] IH] //; rewrite lucasSS addn_gt0 IH. +Qed. + +Lemma double_lucas: forall n, 3 <= n -> (lucas n).*2 = fib (n.+3) + fib (n-3). +Proof. +case=> [|[|[|n]]] // _; rewrite !subSS subn0. +apply/eqP; rewrite -(eqn_add2l (lucas n.+4)) {2}lucasSS addnC -addnn. +rewrite -2![lucas _ + _ + _]addnA eqn_add2l addnC -lucasSS. +rewrite !lucas_fib // [_ + (_ + _)]addnC -[fib _ + _ + _]addnA eqn_add2l. +by rewrite [_ + (_ + _)]addnC -addnA -fibSS. +Qed. + +Lemma fib_double_lucas : forall n, fib (n.*2) = fib n * lucas n. +Proof. +case=> [|n]; rewrite // -addnn fib_add // lucas_fib // mulnDr addnC. +by apply/eqP; rewrite eqn_add2l mulnC. +Qed. + +Lemma fib_doubleS: forall n, fib (n.*2.+1) = fib n.+1 ^ 2 + fib n ^ 2. +Proof. +by move=> n; rewrite -addnn -addSn fib_add // addnC. +Qed. + +Lemma fib_square: forall n, (fib n)^2 = if odd n then (fib n.+1 * fib n.-1).+1 + else (fib n.+1 * fib n.-1).-1. +Proof. +case=> [|n] //; move: (fib_sub (n.+1) n (leqnSn _)). +rewrite subSn // subnn fib1 -{8}[n.+1]add1n odd_add addTb. +case: odd=> H1; last first. + by rewrite -[(_ * _).+1]addn1 {2}H1 addnC subnK // ltnW // -subn_gt0 -H1. +by apply/eqP; rewrite -subn1 {2}H1 subKn // ltnW // -subn_gt0 -H1. +Qed. + +Lemma fib_sum : forall n, \sum_(i < n) fib i = (fib n.+1).-1. +Proof. +elim=> [|n IH]; first by rewrite big_ord0. +by rewrite big_ord_recr /= IH fibSS; case: fib (fib_gt0 _ (ltn0Sn n)). +Qed. + +Lemma fib_sum_even : forall n, \sum_(i < n) fib i.*2 = (fib n.*2.-1).-1. +Proof. +elim=> [|n IH]; first by rewrite big_ord0. +rewrite big_ord_recr IH; case: (n)=> [|n1] //. +rewrite (fibSS (n1.*2.+1)) addnC -[(n1.+1).*2.-1]/n1.*2.+1. +by case: fib (fib_gt0 _ (ltn0Sn ((n1.*2)))). +Qed. + +Lemma fib_sum_odd: forall n, \sum_(i < n) fib i.*2.+1 = fib n.*2. +Proof. +elim=> [|n IH]; first by rewrite big_ord0. +by rewrite big_ord_recr IH /= addnC -fibSS. +Qed. + +Lemma fib_sum_square: forall n, \sum_(i < n) (fib i)^2 = fib n * fib n.-1. +Proof. +elim=> [|n IH]; first by rewrite big_ord0. +rewrite big_ord_recr /= IH. +by rewrite -mulnDr addnC; case: (n)=> // n1; rewrite -fibSS mulnC. +Qed. + +Lemma bin_sum_diag: forall n, \sum_(i < n) 'C(n.-1-i,i) = fib n. +Proof. +move=> n; elim: n {-2}n (leqnn n)=> [[] // _ |n IH]; first by rewrite big_ord0. +move=> n1; rewrite leq_eqVlt; case/orP=> [|Hn]; last first. + by apply: IH; rewrite -ltnS. +move/eqP->; case: n IH=> [|[|n]] IH. +- by rewrite big_ord_recr big_ord0. +- by rewrite !big_ord_recr big_ord0. +rewrite fibSS -!IH // big_ord_recl bin0 big_ord_recr /= subnn bin0n addn0. +set ss := \sum_(i < _) _. +rewrite big_ord_recl bin0 -addnA -big_split; congr (_ + _). +by apply eq_bigr=> i _ /=; rewrite -binS subSn //; case: i. +Qed. + + +(* The matrix *) + +Section Matrix. + +Open Local Scope ring_scope. +Import GRing.Theory. + +Variable R: ringType. + +(* Equivalence ^ n.+1 *) +(* fib n.+2 fib n.+1 1 1 *) +(* = *) +(* fib n.+1 fib n 1 0 *) + +Definition seq2matrix m n (l: seq (seq R)) := + \matrix_(i<m,j<n) nth 1 (nth [::] l i) j. + +Local Notation "''M{' l } " := (seq2matrix _ _ l). + +Lemma matrix_fib : forall n, + 'M{[:: [::(fib n.+2)%:R; (fib n.+1)%:R]; + [::(fib n.+1)%:R; (fib n)%:R]]} = + ('M{[:: [:: 1; 1]; + [:: 1; 0]]})^+n.+1 :> 'M[R]_(2,2). +Proof. +elim=> [|n IH]. + by apply/matrixP=> [[[|[|]] // _] [[|[|]] // _]]; rewrite !mxE. +rewrite exprS -IH; apply/matrixP=> i j. +by rewrite !mxE !big_ord_recl big_ord0 !mxE; + case: i=> [[|[|]]] //= _; case: j=> [[|[|]]] //= _; + rewrite !mul1r ?mul0r !addr0 // fibSS natrD. +Qed. + +End Matrix. diff --git a/mathcomp/attic/forms.v b/mathcomp/attic/forms.v new file mode 100644 index 0000000..1c88af5 --- /dev/null +++ b/mathcomp/attic/forms.v @@ -0,0 +1,193 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype bigop. +Require Import finfun tuple ssralg matrix zmodp vector. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Open Local 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. diff --git a/mathcomp/attic/galgebra.v b/mathcomp/attic/galgebra.v new file mode 100644 index 0000000..411fb6a --- /dev/null +++ b/mathcomp/attic/galgebra.v @@ -0,0 +1,227 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun. +Require Import bigop finset ssralg fingroup zmodp matrix vector falgebra. + +(*****************************************************************************) +(* * Finite Group as an algebra *) +(* (galg F gT) == the algebra generated by gT on F *) +(*****************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Reserved Notation "g %:FG" + (at level 2, left associativity, format "g %:FG"). + +Open Local Scope ring_scope. +Import GRing.Theory. + +Section GroupAlgebraDef. +Variables (F : fieldType) (gT : finGroupType). + +Inductive galg : predArgType := GAlg of {ffun gT -> F}. + +Definition galg_val A := let: GAlg f := A in f. + +Canonical galg_subType := Eval hnf in [newType for galg_val]. +Definition galg_eqMixin := Eval hnf in [eqMixin of galg by <:]. +Canonical galg_eqType := Eval hnf in EqType galg galg_eqMixin. +Definition galg_choiceMixin := [choiceMixin of galg by <:]. +Canonical galg_choiceType := Eval hnf in ChoiceType galg galg_choiceMixin. + +Definition fun_of_galg A (i : gT) := galg_val A i. + +Coercion fun_of_galg : galg >-> Funclass. + +Lemma galgE : forall f, GAlg (finfun f) =1 f. +Proof. by move=> f i; rewrite /fun_of_galg ffunE. Qed. + +Definition injG (g : gT) := GAlg ([ffun k => (k == g)%:R]). +Notation Local "g %:FG" := (injG g). + +Implicit Types v: galg. + +Definition g0 := GAlg 0. +Definition g1 := 1%g %:FG. +Definition opprg v := GAlg (-galg_val v). +Definition addrg v1 v2 := GAlg (galg_val v1 + galg_val v2). +Definition mulvg a v := GAlg ([ffun k => a * galg_val v k]). +Definition mulrg v1 v2 := + GAlg ([ffun g => \sum_(k : gT) (v1 k) * (v2 ((k^-1) * g)%g)]). + +Lemma addrgA : associative addrg. +Proof. +by move=> *; apply: val_inj; apply/ffunP=> ?; rewrite !ffunE addrA. +Qed. +Lemma addrgC : commutative addrg. +Proof. +by move=> *; apply: val_inj; apply/ffunP=> ?; rewrite !ffunE addrC. +Qed. +Lemma addr0g : left_id g0 addrg. +Proof. +by move=> *; apply: val_inj; apply/ffunP=> ?; rewrite !ffunE add0r. +Qed. +Lemma addrNg : left_inverse g0 opprg addrg. +Proof. +by move=> *; apply: val_inj; apply/ffunP=> ?; rewrite !ffunE addNr. +Qed. + +(* abelian group structure *) +Definition gAlgZmodMixin := ZmodMixin addrgA addrgC addr0g addrNg. +Canonical Structure gAlgZmodType := + Eval hnf in ZmodType galg gAlgZmodMixin. + +Lemma GAlg_morph : {morph GAlg: x y / x + y}. +Proof. by move=> f1 f2; apply/eqP. Qed. + +Lemma mulvgA : forall a b v, mulvg a (mulvg b v) = mulvg (a * b) v. +Proof. +by move=> *; apply: val_inj; apply/ffunP=> g; rewrite !ffunE mulrA. +Qed. + +Lemma mulvg1 : forall v, mulvg 1 v = v. +Proof. by move=> v; apply: val_inj; apply/ffunP=> g; rewrite ffunE mul1r. Qed. + +Lemma mulvg_addr : forall a u v, mulvg a (u + v) = (mulvg a u) + (mulvg a v). +Proof. +by move=> *; apply: val_inj; apply/ffunP=> g; rewrite !ffunE mulrDr. +Qed. + +Lemma mulvg_addl : forall u a b, mulvg (a + b) u = (mulvg a u) + (mulvg b u). +Proof. +by move=> *; apply: val_inj; apply/ffunP=> g; rewrite !ffunE mulrDl. +Qed. + +Definition gAlgLmodMixin := LmodMixin mulvgA mulvg1 mulvg_addr mulvg_addl. +Canonical gAlgLmodType := Eval hnf in LmodType F galg gAlgLmodMixin. + +Lemma sum_fgE : forall I r (P : pred I) (E : I -> galg) i, + (\sum_(k <- r | P k) E k) i = \sum_(k <- r | P k) E k i. +Proof. +move=> I r P E i. +by apply: (big_morph (fun A : galg => A i)) => [A B|]; rewrite galgE. +Qed. + +Lemma mulrgA : associative mulrg. +Proof. +move=> x y z; apply: val_inj; apply/ffunP=> g; rewrite !ffunE; symmetry. +rewrite (eq_bigr (fun k => \sum_i x i * (y (i^-1 * k)%g * z (k^-1 * g)%g))) + => [| *]; last by rewrite galgE big_distrl; apply: eq_bigr => *; rewrite mulrA. +rewrite exchange_big /=. +transitivity (\sum_j x j * \sum_i y (j^-1 * i)%g * z (i^-1 * g)%g). + by apply: eq_bigr => i _; rewrite big_distrr /=. +apply: eq_bigr => i _; rewrite galgE (reindex (fun j => (i * j)%g)); last first. + by exists [eta mulg i^-1] => /= j _; rewrite mulgA 1?mulgV 1?mulVg mul1g. +by congr (_ * _); apply: eq_bigr => *; rewrite mulgA mulVg mul1g invMg mulgA. +Qed. + +Lemma mulr1g : left_id g1 mulrg. +Proof. +move=> x; apply: val_inj; apply/ffunP=> g. +rewrite ffunE (bigD1 1%g) //= galgE eqxx invg1. +by rewrite mul1g mul1r big1 1?addr0 // => i Hi; rewrite galgE (negbTE Hi) mul0r. +Qed. + +Lemma mulrg1 : right_id g1 mulrg. +Proof. +move=> x; apply: val_inj; apply/ffunP=> g. +rewrite ffunE (bigD1 g) //= galgE mulVg eqxx mulr1. +by rewrite big1 1?addr0 // => i Hi; rewrite galgE -eq_mulVg1 (negbTE Hi) mulr0. +Qed. + +Lemma mulrg_addl : left_distributive mulrg addrg. +Proof. +move=> x y z; apply: val_inj; apply/ffunP=> g; rewrite !ffunE -big_split /=. +by apply: eq_bigr => i _; rewrite galgE mulrDl. +Qed. + +Lemma mulrg_addr : right_distributive mulrg addrg. +Proof. +move=> x y z; apply: val_inj; apply/ffunP=> g; rewrite !ffunE -big_split /=. +by apply: eq_bigr => i _; rewrite galgE mulrDr. +Qed. + +Lemma nong0g1 : g1 != 0 :> galg. +Proof. +apply/eqP; case. +move/ffunP; move/(_ 1%g); rewrite !ffunE eqxx. +by move/eqP; rewrite oner_eq0. +Qed. + +Definition gAlgRingMixin := + RingMixin mulrgA mulr1g mulrg1 mulrg_addl mulrg_addr nong0g1. +Canonical gAlgRingType := Eval hnf in RingType galg gAlgRingMixin. + +Implicit Types x y : galg. + +Lemma mulg_mulvl : forall a x y, a *: (x * y) = (a *: x) * y. +Proof. +move=> a x y; apply: val_inj; apply/ffunP=> g. +rewrite !ffunE big_distrr /=. +by apply: eq_bigr => i _; rewrite mulrA galgE. +Qed. + +Lemma mulg_mulvr : forall a x y, a *: (x * y) = x * (a *: y). +Proof. +move=> a x y; apply: val_inj; apply/ffunP=> g. +rewrite !ffunE big_distrr /=. +by apply: eq_bigr => i _; rewrite galgE mulrCA. +Qed. + +Canonical gAlgLalgType := Eval hnf in LalgType F galg mulg_mulvl. +Canonical gAlgAlgType := Eval hnf in AlgType F galg mulg_mulvr. + +Lemma injGM : forall g h, (g * h)%g %:FG = (g %:FG) * (h %:FG). +Proof. +move=> g h; apply: val_inj; apply/ffunP=> k. +rewrite !ffunE (bigD1 g) //= !galgE eqxx mul1r. +rewrite big1 1?addr0 => [| i Hi]; last by rewrite !galgE (negbTE Hi) mul0r. +by rewrite -(inj_eq (mulgI (g^-1)%g)) mulgA mulVg mul1g. +Qed. + +Fact gAlg_iso_vect : Vector.axiom #|gT| galg. +Proof. +exists (fun x => \row_(i < #|gT|) x (enum_val i)) => [k x y | ]. + by apply/rowP=> i; rewrite !mxE !galgE !ffunE. +exists (fun x : 'rV[F]_#|gT| => GAlg ([ffun k => (x 0 (enum_rank k))])) => x. + by apply: val_inj; apply/ffunP=> i; rewrite ffunE mxE enum_rankK. +by apply/rowP=> i; rewrite // !mxE galgE enum_valK. +Qed. + +Definition galg_vectMixin := VectMixin gAlg_iso_vect. +Canonical galg_vectType := VectType F galg galg_vectMixin. + +Canonical galg_unitRingType := FalgUnitRingType galg. +Canonical galg_unitAlgFType := [unitAlgType F of galg]. +Canonical gAlgAlgFType := [FalgType F of galg]. + + +Variable G : {group gT}. + +Definition gvspace: {vspace galg} := (\sum_(g in G) <[g%:FG]>)%VS. + +Fact gspace_subproof : has_algid gvspace && (gvspace * gvspace <= gvspace)%VS. +Proof. +apply/andP; split. + apply: has_algid1. + rewrite /gvspace (bigD1 (1)%g) //=. + apply: subv_trans (addvSl _ _). + by apply/vlineP; exists 1; rewrite scale1r. +apply/prodvP=> u v Hu Hv. +case/memv_sumP: Hu => u_ Hu ->; rewrite big_distrl /=. +apply: memv_suml=> i Hi. +case/memv_sumP: Hv => v_ Hv ->; rewrite big_distrr /=. +apply: memv_suml=> j Hj. +rewrite /gvspace (bigD1 (i*j)%g) /=; last by exact: groupM. +apply: subv_trans (addvSl _ _). +case/vlineP: (Hu _ Hi)=> k ->; case/vlineP: (Hv _ Hj)=> l ->. +apply/vlineP; exists (k * l). +by rewrite -scalerAl -scalerAr scalerA injGM. +Qed. + +Definition gaspace : {aspace galg} := ASpace gspace_subproof. + +End GroupAlgebraDef. + +Notation " g %:FG " := (injG _ g). diff --git a/mathcomp/attic/multinom.v b/mathcomp/attic/multinom.v new file mode 100644 index 0000000..b203381 --- /dev/null +++ b/mathcomp/attic/multinom.v @@ -0,0 +1,438 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype. +Require Import tuple finfun bigop ssralg poly generic_quotient bigenough. + +(* We build the ring of multinomials with an arbitrary (countable) *) +(* number of indeterminates. We show it is a ring when the base field *) +(* is a ring, and a commutative ring when the base field is commutative *) + +(* TODO: + - when the base field is an integral domain, so are multinomials (WIP) + - replace the countable type of indeterminates by an arbitrary choice type + - do the theory of symmetric polynomials +*) + + + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope ring_scope. +Local Open Scope quotient_scope. + +Import GRing.Theory BigEnough. + +Module Multinomial. + +Section Multinomial. + +Variable X : countType. + +Section MultinomialRing. + +Variable R : ringType. + +(* Definining the free algebra of multinomial terms *) +Inductive multi_term := +| Coef of R +| Var of X +| Oper of bool & multi_term & multi_term. + +Notation Sum := (Oper false). +Notation Prod := (Oper true). + +(* Encoding to a tree structure in order to recover equality and choice *) +Fixpoint to_tree m : GenTree.tree (X + R) := +match m with +| Coef x => GenTree.Node 0 [:: GenTree.Leaf (inr _ x)] +| Var x => GenTree.Node 0 [:: GenTree.Leaf (inl _ x)] +| Oper b m1 m2 => GenTree.Node (b.+1) [:: to_tree m1; to_tree m2] +end. + +Fixpoint from_tree t := +match t with +| GenTree.Node 0 [:: GenTree.Leaf (inr x)] => Some (Coef x) +| GenTree.Node 0 [:: GenTree.Leaf (inl x)] => Some (Var x) +| GenTree.Node n.+1 [:: t1; t2] => + if (from_tree t1, from_tree t2) is (Some m1, Some m2) + then Some (Oper (n == 1)%N m1 m2) else None +| _ => None +end. + +Lemma to_treeK : pcancel to_tree from_tree. +Proof. by elim=> //=; case=> ? -> ? ->. Qed. + +Definition multi_term_eqMixin := PcanEqMixin to_treeK. +Canonical multi_term_eqType := EqType multi_term multi_term_eqMixin. +Definition multi_term_choiceMixin := PcanChoiceMixin to_treeK. +Canonical multi_term_choiceType := ChoiceType multi_term multi_term_choiceMixin. + +(* counting the variables, in order to know how to interpret multi_term *) +Fixpoint nbvar_term t := + match t with + | Coef _ => 0%N + | Var x => (pickle x).+1 + | Sum u v => maxn (nbvar_term u) (nbvar_term v) + | Prod u v => maxn (nbvar_term u) (nbvar_term v) + end. + +(* Iterated polynomials over a ring *) +Fixpoint multi n := if n is n.+1 then [ringType of {poly multi n}] else R. + +Fixpoint inject n m (p : multi n) {struct m} : multi (m + n) := + if m is m'.+1 return multi (m + n) then (inject m' p)%:P else p. + +Lemma inject_inj : forall i m, injective (@inject i m). +Proof. by move=> i; elim=> //= m IHm p q; move/polyC_inj; move/IHm. Qed. + +Lemma inject0 : forall i m, @inject i m 0 = 0. +Proof. by move=> i; elim=> //= m ->. Qed. + +Lemma inject_eq0 : forall i m p, (@inject i m p == 0) = (p == 0). +Proof. by move=> i m p; rewrite -(inj_eq (@inject_inj i m)) inject0. Qed. + +Lemma size_inject : forall i m p, size (@inject i m.+1 p) = (p != 0 : nat). +Proof. by move=> i m p; rewrite size_polyC inject_eq0. Qed. + +Definition cast_multi i m n Emn : multi i -> multi n := + let: erefl in _ = n' := Emn return _ -> multi n' in inject m. + +Definition multi_var n (i : 'I_n) := cast_multi (subnK (valP i)) 'X. + +Notation "'X_ i" := (multi_var i). + +Lemma inject_is_rmorphism : forall m n, rmorphism (@inject n m). +Proof. +elim=> // m ihm n /=; have ->: inject m = RMorphism (ihm n) by []. +by rewrite -/(_ \o _); apply: rmorphismP. +Qed. +Canonical inject_rmorphism m n := RMorphism (inject_is_rmorphism m n). +Canonical inject_additive m n := Additive (inject_is_rmorphism m n). + +Lemma cast_multi_is_rmorphism i m n Enm : rmorphism (@cast_multi i m n Enm). +Proof. by case: n / Enm; apply: rmorphismP. Qed. +Canonical cast_multi_rmorphism i m n e := + RMorphism (@cast_multi_is_rmorphism i m n e). +Canonical cast_multi_additive i m n e := + Additive (@cast_multi_is_rmorphism i m n e). + +Definition multiC n : R -> multi n := cast_multi (addn0 n). +Lemma multiC_is_rmorphism n : rmorphism (multiC n). +Proof. by rewrite /multiC -[R]/(multi 0); apply: rmorphismP. Qed. +Canonical multiC_rmorphism n := RMorphism (multiC_is_rmorphism n). +Canonical multiC_additive n := Additive (multiC_is_rmorphism n). + +Lemma cast_multi_inj n i i' n' (m1 m2 : multi n) + (p1: (i + n)%N=n') (p2: (i' + n)%N=n') : + cast_multi p1 m1 == cast_multi p2 m2 = (m1 == m2). +Proof. +have := p2; rewrite -{1}[n']p1; move/eqP; rewrite eqn_add2r. +move=> /eqP /= Eii; move:p2; rewrite Eii=> p2 {Eii}. +have <-: p1 = p2; first exact: nat_irrelevance. +apply/idP/idP; last by move/eqP->. +move => Hm {p2}. +have : inject i m1 = inject i m2; last first. + by move/eqP; rewrite (inj_eq (@inject_inj _ _)). +move: Hm; move:(p1); rewrite -p1 => p2. +rewrite (_ : p2 = erefl (i+n)%N); last exact: nat_irrelevance. +by move/eqP. +Qed. + +Lemma Emj_Enk i j k m n : + forall (Emj : (m + i)%N = j) (Enk : (n + j)%N = k), (n + m + i)%N = k. +Proof. by move<-; rewrite addnA. Qed. + +Lemma cast_multi_id n (e : (0 + n)%N = n) m : cast_multi e m = m. +Proof. by rewrite (_ : e = erefl _) //; apply: nat_irrelevance. Qed. + +Lemma cast_multiS n i n' (m : multi n) + (p: (i + n)%N = n') (pS: ((i.+1) + n)%N = n'.+1) : + (cast_multi pS m) = (cast_multi p m)%:P. +Proof. by case: _ / p in pS *; rewrite [pS](nat_irrelevance _ (erefl _)). Qed. + +Lemma injectnm_cast_multi i m n p : + inject (n + m)%N p = + ((@cast_multi (m + i)%N n ((n + m) + i)%N (addnA _ _ _)) \o (inject m)) p. +Proof. +elim: n => [|n /= -> /=]. + by rewrite [addnA 0%N m i](nat_irrelevance _ (erefl _)). +by rewrite cast_multiS; congr (cast_multi _ _)%:P; apply: nat_irrelevance. +Qed. + +Lemma cast_multi_add i j k m n Emj Enk p : + @cast_multi j n k Enk (@cast_multi i m j Emj p) = + @cast_multi i (n + m)%N k (Emj_Enk Emj Enk) p. +Proof. +move: (Emj) (Enk) (Emj_Enk Emj Enk); rewrite -Enk -Emj. +change (addn_rec n (addn_rec m i)) with (n+m+i)%N. +rewrite {-1}[(n+(m+i))%N]addnA=> Emj0 Enk0 Enmi. +have ->: (Emj0 = erefl (m+i)%N); first exact: nat_irrelevance. +have ->: (Enmi = erefl (n+m+i)%N); first exact: nat_irrelevance. +rewrite /= injectnm_cast_multi /=. +by apply/eqP; rewrite cast_multi_inj. +Qed. + +(* Interpretation of a multi_term in iterated polynomials, + for a given number of variables n *) +Fixpoint interp n m : multi n := + match m with + | Coef x => multiC n x + | Var x => let i := pickle x in + (if i < n as b return (i < n) = b -> multi n + then fun iltn => cast_multi (subnK iltn) 'X_(Ordinal (leqnn i.+1)) + else fun _ => 0) (refl_equal (i < n)) + | Sum p q => interp n p + interp n q + | Prod p q => interp n p * interp n q +end. + +Lemma interp_cast_multi n n' m (nltn' : n <= n') : + nbvar_term m <= n -> interp n' m = cast_multi (subnK nltn') (interp n m). +Proof. +move=> dmltn; have dmltn' := (leq_trans dmltn nltn'). +elim: m nltn' dmltn dmltn'. ++ move=> a /= nltn' dmltn dmltn'. + apply/eqP; rewrite /multiC. + by rewrite cast_multi_add /= cast_multi_inj. ++ move=> N /= nltn' dmltn dmltn'. + move: (refl_equal (_ N < n')) (refl_equal (_ N < n)). + rewrite {2 3}[_ N < n]dmltn {2 3}[_ N < n']dmltn' => Nn' Nn. + by apply/eqP; rewrite cast_multi_add cast_multi_inj. +move=> [] m1 Hm1 m2 Hm2 nltn' /=; +rewrite !geq_max => /andP [dm1n dm1n'] /andP [dm2n dm2n']; +by rewrite (Hm1 nltn') // (Hm2 nltn') // (rmorphM, rmorphD). +Qed. + +(* identification of to multi_terms modulo equality of iterated polynomials *) +Definition equivm m1 m2 := let n := maxn (nbvar_term m1) (nbvar_term m2) in + interp n m1 == interp n m2. + +(* it works even for a bigger n *) +Lemma interp_gtn n m1 m2 : maxn (nbvar_term m1) (nbvar_term m2) <= n -> + equivm m1 m2 = (interp n m1 == interp n m2). +Proof. +move=> hn; rewrite !(interp_cast_multi hn) ?leq_max ?leqnn ?orbT //. +by rewrite cast_multi_inj. +Qed. + +Lemma equivm_refl : reflexive equivm. Proof. by move=> x; rewrite /equivm. Qed. + +Lemma equivm_sym : symmetric equivm. +Proof. by move=> x y; rewrite /equivm eq_sym maxnC. Qed. + +Lemma equivm_trans : transitive equivm. +Proof. +move=> x y z; pose_big_enough n. + by rewrite !(@interp_gtn n) => // /eqP-> /eqP->. +by close. +Qed. + +(* equivm is an equivalence *) +Canonical equivm_equivRel := EquivRel equivm + equivm_refl equivm_sym equivm_trans. + +(* we quotient by the equivalence *) +Definition multinom := {eq_quot equivm}. +Definition multinom_of of phant X & phant R := multinom. + +Local Notation "{ 'multinom' R }" := (multinom_of (Phant X) (Phant R)) + (at level 0, format "{ 'multinom' R }"). +(* We recover a lot of structure *) +Canonical multinom_quotType := [quotType of multinom]. +Canonical multinom_eqType := [eqType of multinom]. +Canonical multinom_eqQuotType := [eqQuotType equivm of multinom]. +Canonical multinom_choiceType := [choiceType of multinom]. +Canonical multinom_of_quotType := [quotType of {multinom R}]. +Canonical multinom_of_eqType := [eqType of {multinom R}]. +Canonical multinom_of_eqQuotType := [eqQuotType equivm of {multinom R}]. +Canonical multinom_of_choiceType := [choiceType of {multinom R}]. + +Lemma eqm_interp n m1 m2 : maxn (nbvar_term m1) (nbvar_term m2) <= n -> + (interp n m1 == interp n m2) = (m1 == m2 %[mod {multinom R}]). +Proof. by move=> hn; rewrite eqmodE /= -interp_gtn. Qed. + +Definition cstm := lift_embed {multinom R} Coef. +Notation "c %:M" := (cstm c) (at level 2, format "c %:M"). +Canonical pi_cstm_morph := PiEmbed cstm. + +Definition varm := lift_embed {multinom R} Var. +Notation "n %:X" := (varm n) (at level 2, format "n %:X"). +Canonical pi_varm_morph := PiEmbed varm. + +(* addition is defined by lifting Sum *) +Definition addm := lift_op2 {multinom R} Sum. +Lemma pi_addm : {morph \pi : x y / Sum x y >-> addm x y}. +Proof. +move=> x y /=; unlock addm; apply/eqmodP => /=. +pose_big_enough n. + rewrite (@interp_gtn n) //=; apply/eqP; congr (_ + _); + by apply/eqP; rewrite eqm_interp // reprK. +by close. +Qed. +Canonical pi_addm_morph := PiMorph2 pi_addm. + +Definition Opp := Prod (Coef (-1)). +Definition oppm := lift_op1 {multinom R} Opp. +Lemma pi_oppm : {morph \pi : x / Opp x >-> oppm x}. +Proof. +move=> x; unlock oppm; apply/eqmodP => /=. +rewrite /equivm /= !max0n; apply/eqP; congr (_ * _). +by apply/eqP; rewrite eqm_interp ?reprK. +Qed. +Canonical pi_oppm_morph := PiMorph1 pi_oppm. + +(* addition is defined by lifting Prod *) +Definition mulm := lift_op2 {multinom R} Prod. +Lemma pi_mulm : {morph \pi : x y / Prod x y >-> mulm x y}. +Proof. +move=> x y; unlock mulm; apply/eqP; set x' := repr _; set y' := repr _. +rewrite -(@eqm_interp (nbvar_term (Sum (Sum x y) (Sum x' y')))) /=. + apply/eqP; congr (_ * _); apply/eqP; + by rewrite eqm_interp ?reprK // !(geq_max, leq_max, leqnn, orbT). +by rewrite maxnC. +Qed. +Canonical pi_mulm_morph := PiMorph2 pi_mulm. + +(* Ring properties are obtained from iterated polynomials *) +Lemma addmA : associative addm. +Proof. +elim/quotW=> x; elim/quotW=> y; elim/quotW=> z; apply/eqP. +by rewrite !piE /equivm /= addrA. +Qed. + +Lemma addmC : commutative addm. +Proof. +by elim/quotW=> x; elim/quotW=> y; apply/eqP; rewrite !piE /equivm /= addrC. +Qed. + +Lemma add0m : left_id 0%:M addm. +Proof. by elim/quotW=> x; apply/eqP; rewrite piE /equivm /= rmorph0 add0r. Qed. + +Lemma addmN : left_inverse 0%:M oppm addm. +Proof. +elim/quotW=> x; apply/eqP; rewrite piE /equivm /=. +by rewrite !rmorph0 rmorphN rmorph1 mulN1r addNr. +Qed. + +Definition multinom_zmodMixin := ZmodMixin addmA addmC add0m addmN. +Canonical multinom_zmodType := ZmodType multinom multinom_zmodMixin. +Canonical multinom_of_zmodType := ZmodType {multinom R} multinom_zmodMixin. + +Lemma mulmA : associative mulm. +Proof. +elim/quotW=> x; elim/quotW=> y; elim/quotW=> z; apply/eqP. +by rewrite piE /equivm /= mulrA. +Qed. + +Lemma mul1m : left_id 1%:M mulm. +Proof. by elim/quotW=> x; apply/eqP; rewrite piE /equivm /= rmorph1 mul1r. Qed. + +Lemma mulm1 : right_id 1%:M mulm. +Proof. +elim/quotW=> x; rewrite !piE /=; apply/eqmodP; rewrite /= /equivm /=. +by rewrite rmorph1 mulr1. +Qed. + +Lemma mulm_addl : left_distributive mulm addm. +Proof. +elim/quotW=> x; elim/quotW=> y; elim/quotW=> z; apply/eqP. +by rewrite !piE /equivm /= mulrDl. +Qed. + +Lemma mulm_addr : right_distributive mulm addm. +Proof. +elim/quotW=> x; elim/quotW=> y; elim/quotW=> z; apply/eqP. +by rewrite !piE /equivm /= mulrDr. +Qed. + +Lemma nonzero1m : 1%:M != 0%:M. +Proof. by rewrite piE /equivm /= rmorph1 rmorph0 oner_neq0. Qed. + +Definition multinom_ringMixin := RingMixin mulmA mul1m mulm1 mulm_addl mulm_addr nonzero1m. +Canonical multinom_ringType := RingType multinom multinom_ringMixin. +Canonical multinom_of_ringType := RingType {multinom R} multinom_ringMixin. + +End MultinomialRing. + +Notation "{ 'multinom' R }" := (@multinom_of _ (Phant X) (Phant R)) + (at level 0, format "{ 'multinom' R }"). + +Notation "c %:M" := (cstm c) (at level 2, format "c %:M"). +Notation "n %:X" := (varm n) (at level 2, format "n %:X"). + +Section MultinomialComRing. + +Variable R : comRingType. + +Lemma mul_multiC n : commutative (@GRing.mul (multi R n)). +Proof. +suff [M IH_CR] : {CR : comRingType | [ringType of CR] = multi R n}. + by case: _ / IH_CR => x y; rewrite mulrC. +elim: n => [|n [CR IH_CR]] //=; first by exists R. +by exists [comRingType of {poly CR}]; rewrite -IH_CR. +Qed. + +Lemma mulmC : commutative (@mulm R). +Proof. +elim/quotW=> x; elim/quotW=> y; apply/eqP. +by rewrite piE /equivm /= mul_multiC. +Qed. + +(* if R is commutative, so is {multinom R} *) +Canonical multinom_comRing := Eval hnf in ComRingType (@multinom R) mulmC. +Canonical multinom_of_comRing := Eval hnf in ComRingType {multinom R} mulmC. + +End MultinomialComRing. + +Section MultinomialIdomain. + +Variable R : idomainType. + +(* if R is an integral domain, {multinom R} should also be one, + but the developpment is unfinished *) +Lemma multi_unitClass n : GRing.UnitRing.class_of (multi R n). +Proof. +suff [D IH_D] : {D : idomainType | [ringType of D] = multi R n}. + by case: _ / IH_D; case: D => [sort [[[rc /= _ um _ _]]]]; exists rc. +elim: n => [|n [D IH_D]] //=; first by exists R. +by exists [idomainType of {poly D}]; case: _ / IH_D. +Qed. + +Canonical multi_unitRing n := GRing.UnitRing.Pack + (multi_unitClass n) (multi R n). + +(* Definition Unit (m : multi_term R) := *) +(* let n := nbvar_term m in interp n m \in GRing.unit. *) +(* Definition unitm := lift_fun1 {multinom R} Unit. *) +(* Lemma pi_unitm : {mono \pi : x / Unit x >-> unitm x}. *) +(* Proof. *) +(* move=> x; unlock unitm; rewrite /Unit /=. *) +(* Admitted. *) +(* Canonical pi_unitm_morph := PiMono1 pi_unitm. *) + +Lemma multi_idomain n : GRing.IntegralDomain.axiom (multi R n). +Proof. +suff [D IH_D] : {D : idomainType | [ringType of D] = multi R n}. + by case: _ / IH_D => x y /eqP; rewrite mulf_eq0. +elim: n => [|n [D IH_D]] //=; first by exists R. +by exists [idomainType of {poly D}]; rewrite -IH_D. +Qed. + +Lemma multinom_idomain : GRing.IntegralDomain.axiom [ringType of multinom R]. +Proof. +elim/quotW=> x; elim/quotW=> y /eqP; rewrite -[_ * _]pi_mulm !piE. +pose_big_enough n. + by rewrite !(@interp_gtn _ n) //= !rmorph0 => /eqP /multi_idomain. +by close. +Qed. + +(* Work in progress *) + +End MultinomialIdomain. + +End Multinomial. +End Multinomial. + + + + diff --git a/mathcomp/attic/mxtens.v b/mathcomp/attic/mxtens.v new file mode 100644 index 0000000..c52039f --- /dev/null +++ b/mathcomp/attic/mxtens.v @@ -0,0 +1,312 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype. +Require Import bigop ssralg matrix zmodp div. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import GRing.Theory. +Local Open Scope nat_scope. +Local Open Scope ring_scope. + +Section ExtraBigOp. + +Lemma sumr_add : forall (R : ringType) m n (F : 'I_(m + n) -> R), + \sum_(i < m + n) F i = \sum_(i < m) F (lshift _ i) + + \sum_(i < n) F (rshift _ i). +Proof. +move=> R; elim=> [|m ihm] n F. + rewrite !big_ord0 add0r; apply: congr_big=> // [[i hi]] _. + by rewrite /rshift /=; congr F; apply: val_inj. +rewrite !big_ord_recl ihm -addrA. +congr (_ + _); first by congr F; apply: val_inj. +congr (_ + _); by apply: congr_big=> // i _ /=; congr F; apply: val_inj. +Qed. + +Lemma mxtens_index_proof m n (ij : 'I_m * 'I_n) : ij.1 * n + ij.2 < m * n. +Proof. +case: m ij=> [[[] //]|] m ij; rewrite mulSn addnC -addSn leq_add //. +by rewrite leq_mul2r; case: n ij=> // n ij; rewrite leq_ord orbT. +Qed. + +Definition mxtens_index m n ij := Ordinal (@mxtens_index_proof m n ij). + +Lemma mxtens_index_proof1 m n (k : 'I_(m * n)) : k %/ n < m. +Proof. by move: m n k=> [_ [] //|m] [|n] k; rewrite ?divn0 // ltn_divLR. Qed. +Lemma mxtens_index_proof2 m n (k : 'I_(m * n)) : k %% n < n. +Proof. by rewrite ltn_mod; case: n k=> //; rewrite muln0=> [] []. Qed. + +Definition mxtens_unindex m n k := + (Ordinal (@mxtens_index_proof1 m n k), Ordinal (@mxtens_index_proof2 m n k)). + +Implicit Arguments mxtens_index [[m] [n]]. +Implicit Arguments mxtens_unindex [[m] [n]]. + +Lemma mxtens_indexK m n : cancel (@mxtens_index m n) (@mxtens_unindex m n). +Proof. +case: m=> [[[] //]|m]; case: n=> [[_ [] //]|n]. +move=> [i j]; congr (_, _); apply: val_inj=> /=. + by rewrite divnMDl // divn_small. +by rewrite modnMDl // modn_small. +Qed. + +Lemma mxtens_unindexK m n : cancel (@mxtens_unindex m n) (@mxtens_index m n). +Proof. +case: m=> [[[] //]|m]. case: n=> [|n] k. + by suff: False by []; move: k; rewrite muln0=> [] []. +by apply: val_inj=> /=; rewrite -divn_eq. +Qed. + +CoInductive is_mxtens_index (m n : nat) : 'I_(m * n) -> Type := + IsMxtensIndex : forall (i : 'I_m) (j : 'I_n), + is_mxtens_index (mxtens_index (i, j)). + +Lemma mxtens_indexP (m n : nat) (k : 'I_(m * n)) : is_mxtens_index k. +Proof. by rewrite -[k]mxtens_unindexK; constructor. Qed. + +Lemma mulr_sum (R : ringType) m n (Fm : 'I_m -> R) (Fn : 'I_n -> R) : + (\sum_(i < m) Fm i) * (\sum_(i < n) Fn i) + = \sum_(i < m * n) ((Fm (mxtens_unindex i).1) * (Fn (mxtens_unindex i).2)). +Proof. +rewrite mulr_suml; transitivity (\sum_i (\sum_(j < n) Fm i * Fn j)). + by apply: eq_big=> //= i _; rewrite -mulr_sumr. +rewrite pair_big; apply: reindex=> //=. +by exists mxtens_index=> i; rewrite (mxtens_indexK, mxtens_unindexK). +Qed. + +End ExtraBigOp. + +Section ExtraMx. + +Lemma castmx_mul (R : ringType) + (m m' n p p': nat) (em : m = m') (ep : p = p') + (M : 'M[R]_(m, n)) (N : 'M[R]_(n, p)) : + castmx (em, ep) (M *m N) = castmx (em, erefl _) M *m castmx (erefl _, ep) N. +Proof. by case: m' / em; case: p' / ep. Qed. + +Lemma mulmx_cast (R : ringType) + (m n n' p p' : nat) (en : n' = n) (ep : p' = p) + (M : 'M[R]_(m, n)) (N : 'M[R]_(n', p')) : + M *m (castmx (en, ep) N) = + (castmx (erefl _, (esym en)) M) *m (castmx (erefl _, ep) N). +Proof. by case: n / en in M *; case: p / ep in N *. Qed. + +Lemma castmx_row (R : Type) (m m' n1 n2 n1' n2' : nat) + (eq_n1 : n1 = n1') (eq_n2 : n2 = n2') (eq_n12 : (n1 + n2 = n1' + n2')%N) + (eq_m : m = m') (A1 : 'M[R]_(m, n1)) (A2 : 'M_(m, n2)) : + castmx (eq_m, eq_n12) (row_mx A1 A2) = + row_mx (castmx (eq_m, eq_n1) A1) (castmx (eq_m, eq_n2) A2). +Proof. +case: _ / eq_n1 in eq_n12 *; case: _ / eq_n2 in eq_n12 *. +by case: _ / eq_m; rewrite castmx_id. +Qed. + +Lemma castmx_col (R : Type) (m m' n1 n2 n1' n2' : nat) + (eq_n1 : n1 = n1') (eq_n2 : n2 = n2') (eq_n12 : (n1 + n2 = n1' + n2')%N) + (eq_m : m = m') (A1 : 'M[R]_(n1, m)) (A2 : 'M_(n2, m)) : + castmx (eq_n12, eq_m) (col_mx A1 A2) = + col_mx (castmx (eq_n1, eq_m) A1) (castmx (eq_n2, eq_m) A2). +Proof. +case: _ / eq_n1 in eq_n12 *; case: _ / eq_n2 in eq_n12 *. +by case: _ / eq_m; rewrite castmx_id. +Qed. + +Lemma castmx_block (R : Type) (m1 m1' m2 m2' n1 n2 n1' n2' : nat) + (eq_m1 : m1 = m1') (eq_n1 : n1 = n1') (eq_m2 : m2 = m2') (eq_n2 : n2 = n2') + (eq_m12 : (m1 + m2 = m1' + m2')%N) (eq_n12 : (n1 + n2 = n1' + n2')%N) + (ul : 'M[R]_(m1, n1)) (ur : 'M[R]_(m1, n2)) + (dl : 'M[R]_(m2, n1)) (dr : 'M[R]_(m2, n2)) : + castmx (eq_m12, eq_n12) (block_mx ul ur dl dr) = + block_mx (castmx (eq_m1, eq_n1) ul) (castmx (eq_m1, eq_n2) ur) + (castmx (eq_m2, eq_n1) dl) (castmx (eq_m2, eq_n2) dr). +Proof. +case: _ / eq_m1 in eq_m12 *; case: _ / eq_m2 in eq_m12 *. +case: _ / eq_n1 in eq_n12 *; case: _ / eq_n2 in eq_n12 *. +by rewrite !castmx_id. +Qed. + +End ExtraMx. + +Section MxTens. + +Variable R : ringType. + +Definition tensmx {m n p q : nat} + (A : 'M_(m, n)) (B : 'M_(p, q)) : 'M[R]_(_,_) := nosimpl + (\matrix_(i, j) (A (mxtens_unindex i).1 (mxtens_unindex j).1 + * B (mxtens_unindex i).2 (mxtens_unindex j).2)). + +Notation "A *t B" := (tensmx A B) + (at level 40, left associativity, format "A *t B"). + +Lemma tensmxE {m n p q} (A : 'M_(m, n)) (B : 'M_(p, q)) i j k l : + (A *t B) (mxtens_index (i, j)) (mxtens_index (k, l)) = A i k * B j l. +Proof. by rewrite !mxE !mxtens_indexK. Qed. + +Lemma tens0mx {m n p q} (M : 'M[R]_(p,q)) : (0 : 'M_(m,n)) *t M = 0. +Proof. by apply/matrixP=> i j; rewrite !mxE mul0r. Qed. + +Lemma tensmx0 {m n p q} (M : 'M[R]_(m,n)) : M *t (0 : 'M_(p,q)) = 0. +Proof. by apply/matrixP=> i j; rewrite !mxE mulr0. Qed. + +Lemma tens_scalar_mx (m n : nat) (c : R) (M : 'M_(m,n)): + c%:M *t M = castmx (esym (mul1n _), esym (mul1n _)) (c *: M). +Proof. +apply/matrixP=> i j. +case: (mxtens_indexP i)=> i0 i1; case: (mxtens_indexP j)=> j0 j1. +rewrite tensmxE [i0]ord1 [j0]ord1 !castmxE !mxE /= mulr1n. +by congr (_ * M _ _); apply: val_inj. +Qed. + +Lemma tens_scalar1mx (m n : nat) (M : 'M_(m,n)) : + 1 *t M = castmx (esym (mul1n _), esym (mul1n _)) M. +Proof. by rewrite tens_scalar_mx scale1r. Qed. + +Lemma tens_scalarN1mx (m n : nat) (M : 'M_(m,n)) : + (-1) *t M = castmx (esym (mul1n _), esym (mul1n _)) (-M). +Proof. by rewrite [-1]mx11_scalar /= tens_scalar_mx !mxE scaleNr scale1r. Qed. + +Lemma trmx_tens {m n p q} (M :'M[R]_(m,n)) (N : 'M[R]_(p,q)) : + (M *t N)^T = M^T *t N^T. +Proof. by apply/matrixP=> i j; rewrite !mxE. Qed. + +Lemma tens_col_mx {m n p q} (r : 'rV[R]_n) + (M :'M[R]_(m, n)) (N : 'M[R]_(p, q)) : + (col_mx r M) *t N = + castmx (esym (mulnDl _ _ _), erefl _) (col_mx (r *t N) (M *t N)). +Proof. +apply/matrixP=> i j. +case: (mxtens_indexP i)=> i0 i1; case: (mxtens_indexP j)=> j0 j1. +rewrite !tensmxE castmxE /= cast_ord_id esymK !mxE /=. +case: splitP=> i0' /= hi0'; case: splitP=> k /= hk. ++ case: (mxtens_indexP k) hk=> k0 k1 /=; rewrite tensmxE. + move=> /(f_equal (edivn^~ p)); rewrite !edivn_eq // => [] [h0 h1]. + by congr (r _ _ * N _ _); apply:val_inj; rewrite /= -?h0 ?h1. ++ move: hk (ltn_ord i1); rewrite hi0'. + by rewrite [i0']ord1 mul0n mul1n add0n ltnNge=> ->; rewrite leq_addr. ++ move: (ltn_ord k); rewrite -hk hi0' ltnNge {1}mul1n. + by rewrite mulnDl {1}mul1n -addnA leq_addr. +case: (mxtens_indexP k) hk=> k0 k1 /=; rewrite tensmxE. +rewrite hi0' mulnDl -addnA=> /addnI. + move=> /(f_equal (edivn^~ p)); rewrite !edivn_eq // => [] [h0 h1]. +by congr (M _ _ * N _ _); apply:val_inj; rewrite /= -?h0 ?h1. +Qed. + +Lemma tens_row_mx {m n p q} (r : 'cV[R]_m) (M :'M[R]_(m,n)) (N : 'M[R]_(p,q)) : + (row_mx r M) *t N = + castmx (erefl _, esym (mulnDl _ _ _)) (row_mx (r *t N) (M *t N)). +Proof. +rewrite -[_ *t _]trmxK trmx_tens tr_row_mx tens_col_mx. +apply/eqP; rewrite -(can2_eq (castmxKV _ _) (castmxK _ _)); apply/eqP. +by rewrite trmx_cast castmx_comp castmx_id tr_col_mx -!trmx_tens !trmxK. +Qed. + +Lemma tens_block_mx {m n p q} + (ul : 'M[R]_1) (ur : 'rV[R]_n) (dl : 'cV[R]_m) + (M :'M[R]_(m,n)) (N : 'M[R]_(p,q)) : + (block_mx ul ur dl M) *t N = + castmx (esym (mulnDl _ _ _), esym (mulnDl _ _ _)) + (block_mx (ul *t N) (ur *t N) (dl *t N) (M *t N)). +Proof. +rewrite !block_mxEv tens_col_mx !tens_row_mx -!cast_col_mx castmx_comp. +by congr (castmx (_,_)); apply nat_irrelevance. +Qed. + + +Fixpoint ntensmx_rec {m n} (A : 'M_(m,n)) k : 'M_(m ^ k.+1,n ^ k.+1) := + if k is k'.+1 then (A *t (ntensmx_rec A k')) else A. + +Definition ntensmx {m n} (A : 'M_(m, n)) k := nosimpl + (if k is k'.+1 return 'M[R]_(m ^ k,n ^ k) then ntensmx_rec A k' else 1). + +Notation "A ^t k" := (ntensmx A k) + (at level 39, left associativity, format "A ^t k"). + +Lemma ntensmx0 : forall {m n} (A : 'M_(m,n)) , A ^t 0 = 1. +Proof. by []. Qed. + +Lemma ntensmx1 : forall {m n} (A : 'M_(m,n)) , A ^t 1 = A. +Proof. by []. Qed. + +Lemma ntensmx2 : forall {m n} (A : 'M_(m,n)) , A ^t 2 = A *t A. +Proof. by []. Qed. + +Lemma ntensmxSS : forall {m n} (A : 'M_(m,n)) k, A ^t k.+2 = A *t A ^t k.+1. +Proof. by []. Qed. + +Definition ntensmxS := (@ntensmx1, @ntensmx2, @ntensmxSS). + +End MxTens. + +Notation "A *t B" := (tensmx A B) + (at level 40, left associativity, format "A *t B"). + +Notation "A ^t k" := (ntensmx A k) + (at level 39, left associativity, format "A ^t k"). + +Section MapMx. +Variables (aR rR : ringType). +Hypothesis f : {rmorphism aR -> rR}. +Local Notation "A ^f" := (map_mx f A) : ring_scope. + +Variables m n p q: nat. +Implicit Type A : 'M[aR]_(m, n). +Implicit Type B : 'M[aR]_(p, q). + +Lemma map_mxT A B : (A *t B)^f = A^f *t B^f :> 'M_(m*p, n*q). +Proof. by apply/matrixP=> i j; rewrite !mxE /= rmorphM. Qed. + +End MapMx. + +Section Misc. + +Lemma tensmx_mul (R : comRingType) m n p q r s + (A : 'M[R]_(m,n)) (B : 'M[R]_(p,q)) (C : 'M[R]_(n, r)) (D : 'M[R]_(q, s)) : + (A *t B) *m (C *t D) = (A *m C) *t (B *m D). +Proof. +apply/matrixP=> /= i j. +case (mxtens_indexP i)=> [im ip] {i}; case (mxtens_indexP j)=> [jr js] {j}. +rewrite !mxE !mxtens_indexK mulr_sum; apply: congr_big=> // k _. +by rewrite !mxE !mxtens_indexK mulrCA !mulrA [C _ _ * A _ _]mulrC. +Qed. + +(* Todo : move to div ? *) +Lemma eq_addl_mul q q' m m' d : m < d -> m' < d -> + (q * d + m == q' * d + m')%N = ((q, m) == (q', m')). +Proof. +move=> lt_md lt_m'd; apply/eqP/eqP; last by move=> [-> ->]. +by move=> /(f_equal (edivn^~ d)); rewrite !edivn_eq. +Qed. + +Lemma tensmx_unit (R : fieldType) m n (A : 'M[R]_m%N) (B : 'M[R]_n%N) : + m != 0%N -> n != 0%N -> A \in unitmx -> B \in unitmx -> (A *t B) \in unitmx. +Proof. +move: m n A B => [|m] [|n] // A B _ _ uA uB. +suff : (A^-1 *t B^-1) *m (A *t B) = 1 by case/mulmx1_unit. +rewrite tensmx_mul !mulVmx //; apply/matrixP=> /= i j. +rewrite !mxE /=; symmetry; rewrite -natrM -!val_eqE /=. +rewrite {1}(divn_eq i n.+1) {1}(divn_eq j n.+1). +by rewrite eq_addl_mul ?ltn_mod // xpair_eqE mulnb. +Qed. + + +Lemma tens_mx_scalar : forall (R : comRingType) + (m n : nat) (c : R) (M : 'M[R]_(m,n)), + M *t c%:M = castmx (esym (muln1 _), esym (muln1 _)) (c *: M). +Proof. +move=> R0 m n c M; apply/matrixP=> i j. +case: (mxtens_indexP i)=> i0 i1; case: (mxtens_indexP j)=> j0 j1. +rewrite tensmxE [i1]ord1 [j1]ord1 !castmxE !mxE /= mulr1n mulrC. +by congr (_ * M _ _); apply: val_inj=> /=; rewrite muln1 addn0. +Qed. + +Lemma tensmx_decr : forall (R : comRingType) m n (M :'M[R]_m) (N : 'M[R]_n), + M *t N = (M *t 1%:M) *m (1%:M *t N). +Proof. by move=> R0 m n M N; rewrite tensmx_mul mul1mx mulmx1. Qed. + +Lemma tensmx_decl : forall (R : comRingType) m n (M :'M[R]_m) (N : 'M[R]_n), + M *t N = (1%:M *t N) *m (M *t 1%:M). +Proof. by move=> R0 m n M N; rewrite tensmx_mul mul1mx mulmx1. Qed. + +End Misc. diff --git a/mathcomp/attic/quote.v b/mathcomp/attic/quote.v new file mode 100644 index 0000000..bde7fac --- /dev/null +++ b/mathcomp/attic/quote.v @@ -0,0 +1,365 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Structure tProp := TProp {tProp_statement :> Prop; _ : tProp_statement}. +Lemma claim : forall tP : tProp, tP. Proof. by case. Qed. +Hint Resolve claim. + +Canonical Structure True_tProp := TProp Logic.I. +Canonical Structure eq_tProp T (x : T) := TProp (erefl x). +Canonical Structure true_tProp := @TProp true (erefl _). +Canonical Structure and_tProp (P Q : tProp) := + TProp (conj (claim P) (claim Q)). + +Structure postProp (P : Prop) := PostProp {postProp_statement :> tProp; _ : P}. +Canonical Structure tProp_postProp P claimP pP := + PostProp (@TProp P claimP) (claim pP). + +Delimit Scope n_ary_op_scope with QOP. +Delimit Scope quote_scope with QT. + +Fixpoint n_ary n T := if n is n'.+1 then T -> n_ary n' T else T. +Notation "n .-ary" := (n_ary n) (at level 2, format "n .-ary") : type_scope. + +Module Quotation. + +CoInductive n_ary_op T := NaryOp n of n.-ary T. +Notation "f / n" := (@NaryOp _ n f) : n_ary_op_scope. +Definition bind_op T R (op : n_ary_op T) ifun : R := + let: NaryOp n f := op in ifun n f. +Definition arity T op := @bind_op T nat op (fun n _ => n). + +Structure type := Pack {sort :> Type; sym; _ : sym -> n_ary_op sort}. +Notation QuoteType sf := (Pack sf%QOP). +Definition symop T := let: Pack _ _ ops := T return sym T -> n_ary_op T in ops. + +Inductive term S := Var of nat | App of S & seq (term S). + +Lemma term_ind' : forall S (P : term S -> Type), + (forall i, P (Var S i)) -> + (forall s a, foldr prod True (map P a) -> P (App s a)) -> + (forall t, P t). +Proof. +move=> S P P_V P_A; pose fix sz (t : term S) := + if t is App _ a then (foldr maxn 0 (map sz a)).+1 else 0. +move=> t; elim: {t}(sz t) {-2}t (leqnn (sz t)) => [|n IHn] [i | s a] //=. +rewrite ltnS => sz_a; apply: P_A; elim: a sz_a => //= t a IHa. +by rewrite geq_max; case/andP; move/IHn=> Pt; move/IHa. +Qed. + +Bind Scope quote_scope with term. +Notation "''K_' i" := (Var _ i) + (at level 8, i at level 2, format "''K_' i") : quote_scope. +Notation "''[' s x1 .. xn ]" := (App s (x1%QT :: .. [:: xn%QT] ..)) + (at level 0, s at level 2, x1, xn at level 8, + format "''[' '[hv' s x1 .. xn ']' ]") : quote_scope. +Notation "''[' s ]" := (App s [::]) + (at level 0, s at level 2, format "''[' s ]") : quote_scope. + +Section OneType. + +Variable T : type. +Implicit Type P : Prop. +Implicit Type tP : tProp. + +Definition Env := @id (seq T). + +Fixpoint lookup i e : option T := + if i is i'.+1 then lookup i' (behead e) else ohead e. + +Definition interp_app (iarg : term (sym T) -> option T) := + fix loop a n {struct a} : n.-ary T -> option T := + if n is n'.+1 return n.-ary T -> option T + then fun f => if a is t :: a' then obind (loop a' n' \o f) (iarg t) else None + else fun x => if a is [::] then Some x else None. + +Fixpoint interp e t := match t with + | Var i => lookup i e + | App s a => bind_op (symop s) (interp_app (interp e) a) + end. + +Fixpoint wf (t : term (sym T)) := + match t with + | App s a => let: NaryOp n _ := symop s in (n == size a) && all wf a + | Var _ => true + end. + +Fixpoint eval x0 e t := + match t with + | Var i => nth x0 e i + | App s a => + odflt x0 (bind_op (symop s) (interp_app (fun x => Some (eval x0 e x)) a)) + end. + +Lemma interp_wf_eval : forall y0 e t y, + interp e t = Some y -> wf t /\ eval y0 e t = y. +Proof. +move=> y0 e t; elim/term_ind': t => [i|s a IHa] y /=. + by elim: i e => [|i IHi] [|z e] //=; [case | elim: i {IHi} | exact: IHi]. +case: symop => /= n x1. +elim: n x1 a IHa => [|n IHn] x1 [|f a] //=; first by move=> _ []. +case: (interp e f) => //= x []; case/(_ x)=> // -> ->; exact: IHn. +Qed. + +Definition var_val := @id T. +Definition op_val := var_val. + +Structure form e t P := Form {fval; _ : P -> interp e t = Some fval}. +Lemma formP : forall e t tP f, interp e t = Some (@fval e t tP f). +Proof. by move=> e t tP [x <-]. Qed. + +Structure store i x P := Store {stval; _ : P -> lookup i stval = Some x}. +Canonical Structure head_store x e := + @Store 0 x True (Env (x :: Env e)) (fun _ => erefl _). +Lemma tail_store_subproof : forall i x y e tP s, + e = @stval i x tP s -> lookup i.+1 (y :: e) = Some x. +Proof. by move=> i x y _ tP [e /= <- //] ->. Qed. +Canonical Structure tail_store i x y e tP s := + Store (@tail_store_subproof i x y e tP s). + +Lemma var_form_subproof : forall i x P (s : store i x P), + P -> interp (stval s) 'K_i = Some (var_val x). +Proof. by move=> i x P []. Qed. +Canonical Structure var_form i x P s := Form (@var_form_subproof i x P s). + +Lemma op_form_subproof : forall e t tP (f : form e t tP) x, + x = @fval e t tP f -> interp e t = Some (op_val x). +Proof. by move=> e t tP f _ ->; exact: formP. Qed. + +Canonical Structure op_form e t tP f x := + Form (@op_form_subproof e t tP f x). + +Section OpForm. + +Variables (s : sym T) (e : seq T). + +Fixpoint OpForm_type a xa fa n := + if n is n'.+1 then + forall x t tP f, OpForm_type (t :: a) (x :: xa) (@fval e t tP f :: fa) n' + else form e (App s (rev a)) (map op_val (rev xa) = rev fa). + +Definition OpForm_rechyp a (xa fa : seq T) n (x : n.-ary T) := + forall a', map op_val (rev xa) = rev fa -> + interp e (App s (catrev a' a)) = interp_app (interp e) a' x. + +Definition OpForm_rectype a xa fa n (x : n.-ary T) := + OpForm_rechyp a xa fa x -> OpForm_type a xa fa n. + +Definition OpForm_basetype P x a := + (P -> interp e (App s a) = Some x) -> form e (App s a) P. + +Lemma OpForm_recproof : forall a xa fa n (x1 : n.+1.-ary T), + forall x t tP f, OpForm_rechyp a xa fa x1 -> + OpForm_rechyp (t :: a) (x :: xa) (@fval e t tP f :: fa) (x1 x). +Proof. +move=> a xa fa n x1 x t tP f IHx a'; move/(_ (t :: a')): IHx => /=. +rewrite !map_id (formP f) /= => IHx; case/(can_inj (@revK _)) => -> eq_xa. +by rewrite {}IHx ?eq_xa. +Qed. + +Fixpoint OpForm_rec a xa fa n : forall x, @OpForm_rectype a xa fa n x := + if n is _.+1 return forall x, @OpForm_rectype a xa fa n x then + fun _ IHx _ _ _ _ => OpForm_rec (OpForm_recproof IHx) else + fun x IHx => + (if rev a is (t :: a') as rev_a return OpForm_basetype _ _ rev_a then + fun IHx => Form IHx else fun IHx => Form IHx) (IHx [::]). + +Lemma OpForm_subproof : bind_op (symop s) (OpForm_rechyp [::] [::] [::]). +Proof. by case def_s: (symop s) => [n x] a _; rewrite /= def_s. Qed. + +Definition OpForm := + (let: (op/n)%QOP as op_n := symop s + return (bind_op op_n _ : Prop) -> @OpForm_type _ _ _ (arity op_n) in + @OpForm_rec _ _ _ n op) + OpForm_subproof. + +End OpForm. + +Section GenSimp. + +Variable simp : seq T -> term (sym T) -> option T. + +Definition simp_axiom := forall e t x y, + interp e t = Some x -> simp e t = Some y -> x = y. + +Hypothesis simpP : simp_axiom. + +Structure closed := Closed {closed_val :> seq T}. +Canonical Structure head_closed := Closed (Env [::]). +Canonical Structure tail_closed x (ce : closed) := Closed (x :: ce). +Inductive close : seq T -> Prop := Close (ce : closed) : close ce. +Canonical Structure close_tProp ce := TProp (Close ce). + +Lemma simp_form : forall e t y ptP, + forall f : form (Env e) t + (@postProp_statement (close (Env e) /\ simp e t = Some y) ptP), + fval f = y. +Proof. +move=> e t y [tP [_ def_y]] [x /= def_x]; apply: simpP def_y; exact: def_x. +Qed. + +End GenSimp. + +Definition Econs := Cons. +Definition Etag of nat := @idfun. +Definition Enil := Nil. + +Fixpoint simp_env {T'} e i := + if e is x :: e' then omap (Econs (Etag i x)) (simp_env e' i.+1) + else Some (Enil T'). + +Notation "' 'K_' i := x" := (Etag i x) + (at level 200, format "' 'K_' i := x") : quote_tag_scope. +Arguments Scope Econs [type_scope quote_tag_scope _]. + +Notation "[ 'env' d1 ; .. ; d_n ]" := (Econs d1 .. (Econs d_n (Enil _)) ..) + (at level 0, format "[ 'env' '[' d1 ; '/' .. ; '/' d_n ] ']'") + : quote_scope. + +Notation "[ 'env' ]" := (Enil _) + (at level 0, format "[ 'env' ]") : quote_scope. + +Lemma unquote_default : false -> T. Proof. by []. Qed. +Definition unquote e t := + if interp e t is Some x as ox return ox -> T then fun _ => x else + unquote_default. + +Arguments Scope unquote [quote_scope quote_scope _]. + +Lemma end_unquote : true. Proof. by []. Qed. +Definition simp_quote e t := + obind (fun e' => + (if interp e' t as b return (b -> _) -> _ then + fun wf_t' => Some (unquote (wf_t' end_unquote)) + else fun _ => None) id) + (simp_env e 0). + +Lemma simp_quoteP : simp_axiom simp_quote. +Proof. +rewrite /simp_quote => e t x y def_x. +suff ->: simp_env e 0 = Some e by rewrite /unquote /= def_x; case. +by elim: e {def_x} 0 => //= z e IHe i; rewrite IHe. +Qed. + +Definition quote := simp_form simp_quoteP. + +End OneType. + +End Quotation. + +Canonical Structure Quotation.head_store. +Canonical Structure Quotation.tail_store. +Canonical Structure Quotation.var_form. +Canonical Structure Quotation.op_form. +Canonical Structure Quotation.head_closed. +Canonical Structure Quotation.tail_closed. +Canonical Structure Quotation.close_tProp. + +Notation QuoteType sf := (Quotation.Pack sf%QOP). +Notation "f / n" := (@Quotation.NaryOp _ n f) : n_ary_op_scope. + +Notation OpForm := Quotation.OpForm. + +Notation "''K_' i" := (Quotation.Var _ i) + (at level 8, i at level 2, format "''K_' i") : quote_scope. +Notation "''[' s x1 .. xn ]" := + (Quotation.App s (x1%QT :: .. [:: xn%QT] ..)) + (at level 0, s at level 2, x1, xn at level 8, + format "''[' s '[hv' x1 '/' .. '/' xn ']' ]") : quote_scope. +Notation "''[' s ]" := (Quotation.App s [::]) + (at level 0, s at level 2, format "''[' s ]") : quote_scope. +Notation "' 'K_' i := x" := (Quotation.Etag i x) + (at level 200, format "' 'K_' i := x") : quote_tag_scope. +Arguments Scope Quotation.Econs [type_scope quote_tag_scope _]. +Notation "[ 'env' d1 ; .. ; d_n ]" := + (Quotation.Econs d1 .. (Quotation.Econs d_n (Quotation.Enil _)) ..) + (at level 0, format "[ 'env' '[' d1 ; '/' .. ; '/' d_n ] ']'") + : quote_scope. +Notation "[ 'env' ]" := (Quotation.Enil _) + (at level 0, format "[ 'env' ]") : quote_scope. + +Arguments Scope Quotation.unquote [_ quote_scope quote_scope _]. +Notation unquote e t := (@Quotation.unquote _ e t%QT _). + +CoInductive bool_sym := bTrue | bAnd. +Canonical Structure bool_quoteType := + QuoteType (fun s => match s with bTrue => true/0 | bAnd => andb/2 end). +Canonical Structure and_form := Eval hnf in OpForm bAnd. +Canonical Structure true_form := Eval hnf in OpForm bTrue. + +Lemma try_bquote : forall b1 b2 b3, + false && b1 && (b2 && true && b3) && (b2 && b1 && b2) = false && b2. +Proof. +move=> b1 b2 b3. +Time rewrite Quotation.quote. +Time rewrite !Quotation.quote. +by []. +Qed. + +Fixpoint bstore s bt := match bt with +| 'K_i => set_nth false s i true +| '[bAnd t1 t2] => bstore (bstore s t1) t2 +| _ => s +end%QT. + +Fixpoint bread ot i s := match s with +| [::] => odflt '[bTrue] ot +| true :: s' => bread (Some (oapp (fun t => '[bAnd t 'K_i]) 'K_i ot)) i.+1 s' +| false :: s' => bread ot i.+1 s' +end%QT. + +Fixpoint bnormed t i := match t with +| '[bAnd t' 'K_j] => bnormed t' 1 +| 'K_j => i > 0 +| '[bTrue] => i == 0 +| _ => false +end%QT. + +Definition bsimp_fn e t := + if bnormed t 0 then None else + Quotation.interp e (bread None 0 (bstore [::] t)). + +Lemma bsimpP : Quotation.simp_axiom bsimp_fn. +Proof. +pose oand ob1 ob2 := obind (fun b1 => omap (andb b1) ob2) ob1. +have [oaC oaA oaI]: [/\ commutative oand, associative oand & idempotent oand]. + by split; do 6?case=> //. +have oa1: left_id (Some true) oand by case=> [[]|]. +rewrite /bsimp_fn => e t b b'; case: bnormed => //=. +set ie := Quotation.interp e; set s := [::] => def_b. +pose ir j s := ie (bread None j s). +suff{b'} storeP: ir 0 (bstore s t) = oand (ir 0 s) (Some b). + by rewrite [ie _]storeP => [[]]. +elim/Quotation.term_ind': t s => [i | op a IHa] /= s in b def_b *; last first. + case: op def_b; first by case: a {IHa} => //= <-; rewrite oaC oa1. + case: a IHa => //= t1; rewrite /ie /= -/ie; case: (ie _) => //= b1 [] //= t2. + case: (ie t2) => //= b2 [] //= [IHb1 [IHb2 _]] [<-]. + by rewrite (IHb2 _ b2) // (IHb1 _ b1) // -oaA. +have irT: forall s' j, ir j (true :: s') = oand (ie 'K_j)%QT (ir j.+1 s'). + rewrite /ir /= => s' j; move: s' j ('K_j)%QT. + by elim=> [|[|] s' IHs] j u; first 1 [rewrite oaC oa1] || rewrite !IHs -?oaA. +rewrite -{}def_b -{2}[i]addn0; elim: i 0 s => [|i IHi] j. + case=> [|bj s]; first by rewrite oa1. + by case: bj; rewrite !irT oaC // -oaA oaI. +rewrite addSnnS; case=> [|[|] s]; last exact: IHi. + by rewrite /= -set_nth_nil [ir _ _]IHi. +by rewrite !irT IHi oaA. +Qed. + +Definition bsimp := Quotation.simp_form bsimpP. + +Lemma try_bsimp : forall b1 b2 b3, + true && b1 && (b2 && b3) && (b2 && b1 && b2) = b1 && b2 && true && b3. +Proof. +move=> b1 b2 b3. +Time rewrite bsimp. +Time rewrite !bsimp. +by []. +Qed. +Print try_bsimp. + + diff --git a/mathcomp/attic/tutorial.v b/mathcomp/attic/tutorial.v new file mode 100644 index 0000000..3326c90 --- /dev/null +++ b/mathcomp/attic/tutorial.v @@ -0,0 +1,296 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. + + +Section HilbertSaxiom. + +Variables A B C : Prop. + +Lemma HilbertS : (A -> B -> C) -> (A -> B) -> A -> C. +Proof. +move=> hAiBiC hAiB hA. +move: hAiBiC. +apply. + by []. +by apply: hAiB. +Qed. + +Hypotheses (hAiBiC : A -> B -> C) (hAiB : A -> B) (hA : A). + +Lemma HilbertS2 : C. +Proof. +apply: hAiBiC; first by apply: hA. +exact: hAiB. +Qed. + +Check (hAiB hA). + +Lemma HilbertS3 : C. +Proof. by apply: hAiBiC; last exact: hAiB. Qed. + +Lemma HilbertS4 : C. +Proof. exact: (hAiBiC _ (hAiB _)). Qed. + +Lemma HilbertS5 : C. +Proof. exact: hAiBiC (hAiB _). Qed. + +Lemma HilbertS6 : C. +Proof. exact HilbertS5. Qed. + +End HilbertSaxiom. + + + +Section Symmetric_Conjunction_Disjunction. + +Print bool. + +Lemma andb_sym : forall A B : bool, A && B -> B && A. +Proof. +case. + by case. +by []. +Qed. + +Lemma andb_sym2 : forall A B : bool, A && B -> B && A. +Proof. by case; case. Qed. + +Lemma andb_sym3 : forall A B : bool, A && B -> B && A. +Proof. by do 2! case. Qed. + +Variables (C D : Prop) (hC : C) (hD : D). +Check (and C D). +Print and. +Check conj. +Check (conj hC hD). + +Lemma and_sym : forall A B : Prop, A /\ B -> B /\ A. +Proof. by move=> A1 B []. Qed. + +Print or. + +Check or_introl. + +Lemma or_sym : forall A B : Prop, A \/ B -> B \/ A. +Proof. by move=> A B [hA | hB]; [apply: or_intror | apply: or_introl]. Qed. + +Lemma or_sym2 : forall A B : bool, A \/ B -> B \/ A. +Proof. by move=> [] [] AorB; apply/orP; move/orP : AorB. Qed. + +End Symmetric_Conjunction_Disjunction. + + + +Section R_sym_trans. + +Variables (D : Type) (R : D -> D -> Prop). + +Hypothesis R_sym : forall x y, R x y -> R y x. + +Hypothesis R_trans : forall x y z, R x y -> R y z -> R x z. + +Lemma refl_if : forall x : D, (exists y, R x y) -> R x x. +Proof. +move=> x [y Rxy]. +exact: R_trans (R_sym _ y _). +Qed. + +End R_sym_trans. + + + +Section Smullyan_drinker. + +Variables (D : Type) (P : D -> Prop). +Hypotheses (d : D) (EM : forall A, A \/ ~A). + +Lemma drinker : exists x, P x -> forall y, P y. +Proof. +(* case: (EM (exists y, ~P y)) => [[y notPy]| nonotPy] *) +have [[y notPy]| nonotPy] := EM (exists y, ~P y); first by exists y. +exists d => _ y; case: (EM (P y)) => // notPy. +by case: nonotPy; exists y. +Qed. + +End Smullyan_drinker. + + + +Section Equality. + +Variable f : nat -> nat. +Hypothesis f00 : f 0 = 0. + +Lemma fkk : forall k, k = 0 -> f k = k. +Proof. by move=> k k0; rewrite k0. Qed. + +Lemma fkk2 : forall k, k = 0 -> f k = k. +Proof. by move=> k ->. Qed. + +Variable f10 : f 1 = f 0. + +Lemma ff10 : f (f 1) = 0. +Proof. by rewrite f10 f00. Qed. + +Variables (D : eqType) (x y : D). + +Lemma eq_prop_bool : x = y -> x == y. +Proof. by move/eqP. Qed. + +Lemma eq_bool_prop : x == y -> x = y. +Proof. by move/eqP. Qed. + +End Equality. + + + +Section Using_Definition. + +Variable U : Type. + +Definition set := U -> Prop. + +Definition subset (A B : set) := forall x, A x -> B x. + +Definition transitive (T : Type) (R : T -> T -> Prop) := + forall x y z, R x y -> R y z -> R x z. + +Lemma subset_trans : transitive set subset. +Proof. +rewrite /transitive /subset => x y z subxy subyz t xt. +by apply: subyz; apply: subxy. +Qed. + +Lemma subset_trans2 : transitive set subset. +Proof. +move=> x y z subxy subyz t. +by move/subxy; move/subyz. +Qed. + +End Using_Definition. + + +Section Basic_ssrnat. + + +Lemma three : S (S (S O)) = 3 /\ 3 = 0.+1.+1.+1. +Proof. by []. Qed. + +Lemma concrete_plus : plus 16 64 = 80. +Proof. (*simpl.*) by []. Qed. + +Lemma concrete_addn : 16 + 64 = 80. +Proof. (*simpl.*) by []. Qed. + +Lemma concrete_le : le 1 3. +Proof. by apply: (Le.le_trans _ 2); apply: Le.le_n_Sn. Qed. + +Lemma concrete_big_le : le 16 64. +Proof. by auto 47 with arith. Qed. + +Lemma concrete_big_leq : 0 <= 51. +Proof. by []. Qed. + +Lemma semi_concrete_leq : forall n m, n <= m -> 51 + n <= 51 + m. +Proof. by []. Qed. + +Lemma concrete_arith : (50 < 100) && (3 + 4 < 3 * 4 <= 17 - 2). +Proof. by []. Qed. + +Lemma plus_com : forall m1 n1, n1 + m1 = m1 + n1. +Proof. +by elim=> [| n IHn m]; [elim | rewrite -[n.+1 + m]/(n + m).+1 -IHn; elim: m]. +Qed. + +End Basic_ssrnat. + + +Section Euclidean_division. + + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Definition edivn_rec d := fix loop (m q : nat) {struct m} := + if m - d is m'.+1 then loop m' q.+1 else (q, m). + +Definition edivn m d := if d is d'.+1 then edivn_rec d' m 0 else (0, m). + +CoInductive edivn_spec (m d : nat) : nat * nat -> Type := + EdivnSpec q r of m = q * d + r & (d > 0) ==> (r < d) : edivn_spec m d (q, r). + +Lemma edivnP : forall m d, edivn_spec m d (edivn m d). +Proof. +move=> m [|d] //=; rewrite -{1}[m]/(0 * d.+1 + m). +elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=; rewrite ltnS => le_mn. +rewrite subn_if_gt; case: ltnP => // le_dm. +rewrite -{1}(subnKC le_dm) -addSn addnA -mulSnr; apply: IHn. +apply: leq_trans le_mn; exact: leq_subr. +Qed. + +Lemma edivn_eq : forall d q r, r < d -> edivn (q * d + r) d = (q, r). +Proof. +move=> d q r lt_rd; have d_gt0: 0 < d by exact: leq_trans lt_rd. +case: edivnP lt_rd => q' r'; rewrite d_gt0 /=. +wlog: q q' r r' / q <= q' by case (ltnP q q'); last symmetry; eauto. +rewrite leq_eqVlt; case: eqP => [-> _|_] /=; first by move/addnI->. +rewrite -(leq_pmul2r d_gt0); move/leq_add=> Hqr Eqr _; move/Hqr {Hqr}. +by rewrite addnS ltnNge mulSn -addnA Eqr addnCA addnA leq_addr. +Qed. + +CoInductive edivn_spec_right : nat -> nat -> nat * nat -> Type := + EdivnSpec_right m d q r of m = q * d + r & (d > 0) ==> (r < d) : + edivn_spec_right m d (q, r). + +CoInductive edivn_spec_left (m d : nat)(qr : nat * nat) : Type := +EdivnSpec_left of m = (fst qr) * d + (snd qr) & (d > 0) ==> (snd qr < d) : + edivn_spec_left m d qr. + + +Lemma edivnP_left : forall m d, edivn_spec_left m d (edivn m d). +Proof. +move=> m [|d] //=; rewrite -{1}[m]/(0 * d.+1 + m). +elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=; rewrite ltnS => le_mn. +rewrite subn_if_gt; case: ltnP => // le_dm. +rewrite -{1}(subnKC le_dm) -addSn addnA -mulSnr; apply: IHn. +apply: leq_trans le_mn; exact: leq_subr. +Qed. + +Lemma edivnP_right : forall m d, edivn_spec_right m d (edivn m d). +Proof. +move=> m [|d] //=; rewrite -{1}[m]/(0 * d.+1 + m). +elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=; rewrite ltnS => le_mn. +rewrite subn_if_gt; case: ltnP => // le_dm. +rewrite -{1}(subnKC le_dm) -addSn addnA -mulSnr; apply: IHn. +apply: leq_trans le_mn; exact: leq_subr. +Qed. + +Lemma edivn_eq_right : forall d q r, r < d -> edivn (q * d + r) d = (q, r). +Proof. +move=> d q r lt_rd; have d_gt0: 0 < d by exact: leq_trans lt_rd. +set m := q * d + r; have: m = q * d + r by []. +set d' := d; have: d' = d by []. +case: (edivnP_right m d') => {m d'} m d' q' r' -> lt_r'd' d'd q'd'r'. +move: q'd'r' lt_r'd' lt_rd; rewrite d'd d_gt0 {d'd m} /=. +wlog: q q' r r' / q <= q' by case (ltnP q q'); last symmetry; eauto. +rewrite leq_eqVlt; case: eqP => [-> _|_] /=; first by move/addnI->. +rewrite -(leq_pmul2r d_gt0); move/leq_add=> Hqr Eqr _; move/Hqr {Hqr}. +by rewrite addnS ltnNge mulSn -addnA -Eqr addnCA addnA leq_addr. +Qed. + + +Lemma edivn_eq_left : forall d q r, r < d -> edivn (q * d + r) d = (q, r). +Proof. +move=> d q r lt_rd; have d_gt0: 0 < d by exact: leq_trans lt_rd. +case: (edivnP_left (q * d + r) d) lt_rd; rewrite d_gt0 /=. +set q':= (edivn (q * d + r) d).1; set r':= (edivn (q * d + r) d).2. +rewrite (surjective_pairing (edivn (q * d + r) d)) -/q' -/r'. +wlog: q r q' r' / q <= q' by case (ltnP q q'); last symmetry; eauto. +rewrite leq_eqVlt; case: eqP => [-> _|_] /=; first by move/addnI->. +rewrite -(leq_pmul2r d_gt0); move/leq_add=> Hqr Eqr _; move/Hqr {Hqr}. +by rewrite addnS ltnNge mulSn -addnA Eqr addnCA addnA leq_addr. +Qed. + + +End Euclidean_division.
\ No newline at end of file |