diff options
| author | Enrico Tassi | 2018-04-20 14:17:38 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-20 14:17:38 +0200 |
| commit | dcc7917ac5d66472f751ebbd31b7b63db5465303 (patch) | |
| tree | 22228fc984fdf119291e0e4601a6c3e028107408 /mathcomp | |
| parent | e418a8b26b66ce88e22cff5978823e25aab03d94 (diff) | |
remove the attic/ directory
Diffstat (limited to 'mathcomp')
| l--------- | mathcomp/attic/AUTHORS | 1 | ||||
| l--------- | mathcomp/attic/CeCILL-B | 1 | ||||
| l--------- | mathcomp/attic/INSTALL | 1 | ||||
| -rw-r--r-- | mathcomp/attic/Makefile | 22 | ||||
| l--------- | mathcomp/attic/README | 1 | ||||
| -rw-r--r-- | mathcomp/attic/algnum_basic.v | 541 | ||||
| -rw-r--r-- | mathcomp/attic/amodule.v | 422 | ||||
| -rw-r--r-- | mathcomp/attic/fib.v | 344 | ||||
| -rw-r--r-- | mathcomp/attic/forms.v | 197 | ||||
| -rw-r--r-- | mathcomp/attic/galgebra.v | 231 | ||||
| -rw-r--r-- | mathcomp/attic/multinom.v | 442 | ||||
| -rw-r--r-- | mathcomp/attic/quote.v | 368 | ||||
| -rw-r--r-- | mathcomp/attic/tutorial.v | 299 |
13 files changed, 0 insertions, 2870 deletions
diff --git a/mathcomp/attic/AUTHORS b/mathcomp/attic/AUTHORS deleted file mode 120000 index b55a98d..0000000 --- a/mathcomp/attic/AUTHORS +++ /dev/null @@ -1 +0,0 @@ -../../etc/AUTHORS
\ No newline at end of file diff --git a/mathcomp/attic/CeCILL-B b/mathcomp/attic/CeCILL-B deleted file mode 120000 index 83e22fd..0000000 --- a/mathcomp/attic/CeCILL-B +++ /dev/null @@ -1 +0,0 @@ -../../etc/CeCILL-B
\ No newline at end of file diff --git a/mathcomp/attic/INSTALL b/mathcomp/attic/INSTALL deleted file mode 120000 index 573e04d..0000000 --- a/mathcomp/attic/INSTALL +++ /dev/null @@ -1 +0,0 @@ -../../etc/INSTALL.md
\ No newline at end of file diff --git a/mathcomp/attic/Makefile b/mathcomp/attic/Makefile deleted file mode 100644 index a58be7b..0000000 --- a/mathcomp/attic/Makefile +++ /dev/null @@ -1,22 +0,0 @@ -H=@ - -ifeq "$(COQBIN)" "" -COQBIN=$(dir $(shell which coqtop))/ -endif - -OLD_MAKEFLAGS:=$(MAKEFLAGS) -MAKEFLAGS+=-B - -.DEFAULT_GOAL := all - -%: - $(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq - $(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \ - -f Makefile.coq $* - -.PHONY: clean -clean: - $(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \ - -f Makefile.coq clean - $(H)rm -f Makefile.coq - diff --git a/mathcomp/attic/README b/mathcomp/attic/README deleted file mode 120000 index e4e30e8..0000000 --- a/mathcomp/attic/README +++ /dev/null @@ -1 +0,0 @@ -../../etc/README
\ No newline at end of file diff --git a/mathcomp/attic/algnum_basic.v b/mathcomp/attic/algnum_basic.v deleted file mode 100644 index d908b09..0000000 --- a/mathcomp/attic/algnum_basic.v +++ /dev/null @@ -1,541 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype tuple div. -From mathcomp -Require Import bigop prime finset fingroup ssralg finalg zmodp abelian. -From mathcomp -Require Import matrix vector falgebra finfield action poly ssrint cyclotomic. -From mathcomp -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 apply: 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 //; apply: 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 => /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. Admitted. - -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 //; apply (basis_free Xb). -have Xij (i j : 'I_m) : j != i -> coord X i X`_j = 0%:R. - by rewrite coord_free; [move=> /negbTE -> | apply (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. by have [Yb _] := svalP dual_basis_def Und Xb; apply 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. Admitted. - -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 => /Xs. - move: Xf; rewrite -{1}(in_tupleE X) => /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; apply (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 => -[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 => -[r [rA rS rC]]. - move: mfc0 (rC 0) ->; rewrite scale0r => 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 => -[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) => /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 => /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 => iB. - by have -> := rci (Ordinal iB); apply/b2H. - move: mL; rewrite -b2s => /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) => /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/amodule.v b/mathcomp/attic/amodule.v deleted file mode 100644 index 0a5b655..0000000 --- a/mathcomp/attic/amodule.v +++ /dev/null @@ -1,422 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype fintype finfun finset ssralg. -From mathcomp -Require Import bigop seq tuple choice ssrnat prime ssralg fingroup pgroup. -From mathcomp -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. -Local Open 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. by move=> *; apply: 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. by move=> c v x; apply: linearZZ. Qed. - -Lemma rmul0 : left_zero 0 rmul. -Proof. by move=> x; apply: 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; apply: 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. - by move: v1 Hv1; apply/subvP; apply: eprodvSl; apply: addvSl. -by move: v2 Hv2; apply/subvP; apply: eprodvSl; apply: 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. - by move: v1 Hv1; apply/subvP; apply: eprodvSr; apply: addvSl. -by move: v2 Hv2; apply/subvP; apply: eprodvSr; apply: 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; apply: 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; [apply: mod0v | apply: cap0v | apply: 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 apply: memv_proj. - by rewrite memvE /= /gvspace (bigD1 (j^-1)%g) ?addvSl // groupV. -exists (ms :&: lker f)%VS; split. - - by apply: modv_ker=> //; apply/modfP=> *; apply: 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; apply: memvf. -rewrite memv_ker linearB /= (Himf (f v)) ?subrr // /in_mem /= -If. -by apply: memv_img; apply: memvf. -Qed. - -End ModuleRepresentation. - -Export AModuleType.Exports. diff --git a/mathcomp/attic/fib.v b/mathcomp/attic/fib.v deleted file mode 100644 index a75a226..0000000 --- a/mathcomp/attic/fib.v +++ /dev/null @@ -1,344 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. -From mathcomp -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 _)) => //; apply: 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 apply: 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; apply: dvdn_gcdl. -- by apply: dvdn_fib; apply: 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. - -Local Open 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 deleted file mode 100644 index 7098af9..0000000 --- a/mathcomp/attic/forms.v +++ /dev/null @@ -1,197 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype bigop. -From mathcomp -Require Import finfun tuple ssralg matrix zmodp vector. - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. -Local Open Scope ring_scope. - -Import GRing.Theory. - -Section RingLmodule. - -Variable (R : fieldType). - -Definition r2rv x: 'rV[R^o]_1 := \row_(i < 1) x . - -Lemma r2rv_morph_p : linear r2rv. -Proof. by move=> k x y; apply/matrixP=> [] [[|i] Hi] j; rewrite !mxE. Qed. - -Canonical Structure r2rv_morph := Linear r2rv_morph_p. - -Definition rv2r (A: 'rV[R]_1): R^o := A 0 0. - -Lemma r2rv_bij : bijective r2rv. -Proof. -exists rv2r; first by move=> x; rewrite /r2rv /rv2r /= mxE. -by move=> x; apply/matrixP=> i j; rewrite [i]ord1 [j]ord1 /r2rv /rv2r !mxE /=. -Qed. - -Canonical Structure RVMixin := Eval hnf in VectMixin r2rv_morph_p r2rv_bij. -Canonical Structure RVVectType := VectType R RVMixin. - -Lemma dimR : vdim RVVectType = 1%nat. -Proof. by rewrite /vdim /=. Qed. - -End RingLmodule. - -(* BiLinear & Sesquilinear & Quadratic Forms over a vectType *) -Section LinearForm. - -Variable (F : fieldType) (V : vectType F). - -Section SesquiLinearFormDef. - -Structure fautomorphism:= FautoMorph {fval :> F -> F; - _ : rmorphism fval; - _ : bijective fval}. -Variable theta: fautomorphism. - -Lemma fval_rmorph : rmorphism theta. -Proof. by case: theta. Qed. - -Canonical Structure fautomorh_additive := Additive fval_rmorph. -Canonical Structure fautomorph_rmorphism := RMorphism fval_rmorph. - -Local Notation vvf:= (V -> V -> F). - -Structure sesquilinear_form := - SesqlinearForm {formv :> vvf; - _ : forall x, {morph formv x : y z / y + z}; - _ : forall x, {morph formv ^~ x : y z / y + z}; - _ : forall a x y, formv (a *: x) y = a * formv x y; - _ : forall a x y , formv x (a *: y) = (theta a) * (formv x y)}. - -Variable f : sesquilinear_form. - -Lemma bilin1 : forall x, {morph f x : y z / y + z}. Proof. by case f. Qed. -Lemma bilin2 : forall x, {morph f ^~ x : y z / y + z}. Proof. by case f. Qed. -Lemma bilina1 : forall a x y, f (a *: x) y = a * f x y. Proof. by case f. Qed. -Lemma bilina2 : forall a x y, f x (a *: y) = (theta a) * (f x y). -Proof. by case f. Qed. - -End SesquiLinearFormDef. - -Section SesquiLinearFormTheory. - -Variable theta: fautomorphism. -Local Notation sqlf := (sesquilinear_form theta). - -Definition symmetric (f : sqlf):= (forall a, (theta a = a)) /\ - forall x y, (f x y = f y x). -Definition skewsymmetric (f : sqlf) := (forall a , theta a = a) /\ - forall x y, f x y = -(f y x). - -Definition hermitian_sym (f : sqlf) := (forall x y, f x y = (theta (f y x))). - -Inductive symmetricf (f : sqlf): Prop := - Symmetric : symmetric f -> symmetricf f -| Skewsymmetric: skewsymmetric f -> symmetricf f -| Hermitian_sym : hermitian_sym f -> symmetricf f . - -Lemma fsym_f0: forall (f: sqlf) x y, (symmetricf f) -> - (f x y = 0 <-> f y x = 0). -Proof. -move=> f x y; case; first by move=> [Htheta Hf]; split; rewrite Hf. - by move=> [Htheta Hf]; split; rewrite Hf; move/eqP; rewrite oppr_eq0; move/eqP->. -move=> Htheta; split; first by rewrite (Htheta y x) => ->; rewrite rmorph0. -by rewrite (Htheta x y) => ->; rewrite rmorph0. -Qed. - -End SesquiLinearFormTheory. - -Variable theta: fautomorphism. -Variable f: (sesquilinear_form theta). -Hypothesis fsym: symmetricf f. - -Section orthogonal. - -Definition orthogonal x y := f x y = 0. - -Lemma ortho_sym: forall x y, orthogonal x y <-> orthogonal y x. -Proof. by move=> x y; apply: fsym_f0. Qed. - -Theorem Pythagore: forall u v, orthogonal u v -> f (u+v) (u+v) = f u u + f v v. -Proof. -move=> u v Huv; case: (ortho_sym u v ) => Hvu _. -by rewrite !bilin1 !bilin2 Huv (Hvu Huv) add0r addr0. -Qed. - -Lemma orthoD : forall u v w , orthogonal u v -> orthogonal u w -> orthogonal u (v + w). -Proof. -by move=> u v w Huv Huw; rewrite /orthogonal bilin1 Huv Huw add0r. -Qed. - -Lemma orthoZ: forall u v a, orthogonal u v -> orthogonal (a *: u) v. -Proof. by move=> u v a Huv; rewrite /orthogonal bilina1 Huv mulr0. Qed. - -Variable x:V. - -Definition alpha : V-> (RVVectType F) := fun y => f y x. - -Definition alpha_lfun := (lfun_of_fun alpha). - -Definition xbar := lker alpha_lfun . - -Lemma alpha_lin: linear alpha. -Proof. by move=> a b c; rewrite /alpha bilin2 bilina1. Qed. - - - -Lemma xbarP: forall e1, reflect (orthogonal e1 x ) (e1 \in xbar). -move=> e1; rewrite memv_ker lfun_of_funK //=. - by apply: (iffP eqP). -by apply alpha_lin. -Qed. - - -Lemma dim_xbar :forall vs,(\dim vs ) - 1 <= \dim (vs :&: xbar). -Proof. -move=> vs; rewrite -(addKn 1 (\dim (vs :&: xbar))) addnC leq_sub2r //. -have H :\dim (alpha_lfun @: vs )<= 1 by rewrite -(dimR F) -dimvf dimvS // subvf. -by rewrite -(limg_ker_dim alpha_lfun vs)(leq_add (leqnn (\dim(vs :&: xbar)))). -Qed. - -(* to be improved*) -Lemma xbar_eqvs: forall vs, (forall v , v \in vs -> orthogonal v x )-> \dim (vs :&: xbar)= (\dim vs ). -move=> vs Hvs. -rewrite -(limg_ker_dim alpha_lfun vs). -suff-> : \dim (alpha_lfun @: vs) = 0%nat by rewrite addn0. -apply/eqP; rewrite dimv_eq0; apply/vspaceP => w. -rewrite memv0; apply/memv_imgP. -case e: (w==0). - exists 0; split; first by rewrite mem0v. - apply sym_eq; rewrite (eqP e). - rewrite (lfun_of_funK alpha_lin 0). - rewrite /alpha_lfun /alpha /=. - by move: (bilina1 f 0 x x); rewrite scale0r mul0r. -move/eqP:e =>H2; case=> x0 [Hx0 Hw]. -apply H2; rewrite Hw; move: (Hvs x0 Hx0). -rewrite /orthogonal. -by rewrite (lfun_of_funK alpha_lin x0). -Qed. - - -End orthogonal. - -Definition quadraticf (Q: V -> F) := - (forall x a, Q (a *: x) = a ^+ 2 * (Q x))%R * - (forall x y, Q (x + y) = Q x + Q y + f x y)%R : Prop. -Variable Q : V -> F. -Hypothesis quadQ : quadraticf Q. -Import GRing.Theory. - - -Lemma f2Q: forall x, Q x + Q x = f x x. -Proof. -move=> x; apply: (@addrI _ (Q x + Q x)). -rewrite !addrA -quadQ -[x + x](scaler_nat 2) quadQ. -by rewrite -mulrA !mulr_natl -addrA. -Qed. - -End LinearForm. diff --git a/mathcomp/attic/galgebra.v b/mathcomp/attic/galgebra.v deleted file mode 100644 index 16bbe1e..0000000 --- a/mathcomp/attic/galgebra.v +++ /dev/null @@ -1,231 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq choice fintype finfun. -From mathcomp -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"). - -Local Open 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]). -Local Notation "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 apply: 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 deleted file mode 100644 index 96a8071..0000000 --- a/mathcomp/attic/multinom.v +++ /dev/null @@ -1,442 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. -From mathcomp -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/quote.v b/mathcomp/attic/quote.v deleted file mode 100644 index cdf73bc..0000000 --- a/mathcomp/attic/quote.v +++ /dev/null @@ -1,368 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat seq. - -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} | apply: IHi]. -case: symop => /= n x1. -elim: n x1 a IHa => [|n IHn] x1 [|f a] //=; first by move=> _ []. -by case: (interp e f) => //= x []; case/(_ x)=> // -> ->; apply: 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 _ ->; apply: 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. -by move=> e t y [tP [_ def_y]] [x /= def_x]; apply: simpP def_y; apply: 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. - - - diff --git a/mathcomp/attic/tutorial.v b/mathcomp/attic/tutorial.v deleted file mode 100644 index b2025a7..0000000 --- a/mathcomp/attic/tutorial.v +++ /dev/null @@ -1,299 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat seq. - - -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 apply: 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. -by apply: leq_trans le_mn; apply: 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 apply: 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. -by apply: leq_trans le_mn; apply: 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. -by apply: leq_trans le_mn; apply: 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 apply: 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 apply: 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 |