diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 52f4ada8..32f4c8c3 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -15,6 +15,7 @@ jobs: strategy: matrix: image: + - 'mathcomp/mathcomp:1.18.0-coq-8.18' - 'mathcomp/mathcomp:1.17.0-coq-8.17' - 'mathcomp/mathcomp:1.15.0-coq-8.16' - 'mathcomp/mathcomp:1.14.0-coq-8.15' diff --git a/coq-addition-chains.opam b/coq-addition-chains.opam index 4b02fc2d..b94853ba 100644 --- a/coq-addition-chains.opam +++ b/coq-addition-chains.opam @@ -18,8 +18,8 @@ build: ["dune" "build" "-p" name "-j" jobs] depends: [ "dune" {>= "2.5"} "coq" {>= "8.14"} - "coq-paramcoq" {(>= "1.1.3" & < "1.2~") | (= "dev")} - "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.18"} + "coq-paramcoq" {>= "1.1.3"} + "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.19"} "coq-mathcomp-algebra" ] diff --git a/coq-gaia-hydras.opam b/coq-gaia-hydras.opam index e4b5c505..14cee304 100644 --- a/coq-gaia-hydras.opam +++ b/coq-gaia-hydras.opam @@ -18,9 +18,9 @@ depends: [ "dune" {>= "2.5"} "coq" {>= "8.14"} "coq-hydra-battles" {= version} - "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.18"} + "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.19"} "coq-mathcomp-zify" {< "2"} - "coq-gaia-schutte" {>= "1.14" & < "1.18~"} + "coq-gaia-schutte" {>= "1.14" & < "1.18"} ] tags: [ diff --git a/coq-goedel.opam b/coq-goedel.opam index 5a216e54..40d929b8 100644 --- a/coq-goedel.opam +++ b/coq-goedel.opam @@ -18,7 +18,7 @@ depends: [ "dune" {>= "2.5"} "coq" {>= "8.14"} "coq-hydra-battles" {= version} - "coq-coqprime" {= "dev"} + "coq-coqprime" {>= "1.3.0"} ] tags: [ diff --git a/coq-hydra-battles.opam b/coq-hydra-battles.opam index 10d631a5..07b7dd64 100644 --- a/coq-hydra-battles.opam +++ b/coq-hydra-battles.opam @@ -19,7 +19,7 @@ build: ["dune" "build" "-p" name "-j" jobs] depends: [ "dune" {>= "2.5"} "coq" {>= "8.14"} - "coq-equations" {(>= "1.2" & < "1.4~") | (= "dev")} + "coq-equations" {>= "1.2"} "coq-zorns-lemma" {>= "10.2.0"} "coq-libhyps" ] diff --git a/meta.yml b/meta.yml index 51ff87e0..52aa7b08 100644 --- a/meta.yml +++ b/meta.yml @@ -120,6 +120,8 @@ supported_coq_versions: opam: '{>= "8.14"}' tested_coq_opam_versions: +- version: '1.18.0-coq-8.18' + repo: 'mathcomp/mathcomp' - version: '1.17.0-coq-8.17' repo: 'mathcomp/mathcomp' - version: '1.15.0-coq-8.16' @@ -132,28 +134,28 @@ tested_coq_opam_versions: dependencies: - opam: name: coq-equations - version: '{(>= "1.2" & < "1.4~") | (= "dev")}' + version: '{>= "1.2"}' description: |- [Equations](https://github.com/mattam82/Coq-Equations) 1.2 or later - opam: name: coq-paramcoq - version: '{(>= "1.1.3" & < "1.2~") | (= "dev")}' + version: '{>= "1.1.3"}' description: |- [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later - opam: name: coq-mathcomp-ssreflect - version: '{(>= "1.13.0" & < "1.18~")}' + version: '{>= "1.13.0" & < "1.19"}' description: |- - [MathComp SSReflect](https://github.com/math-comp/math-comp) 1.13 or later + [MathComp SSReflect](https://github.com/math-comp/math-comp) 1.13 to 1.18 - opam: name: coq-mathcomp-algebra description: |- [MathComp Algebra](https://github.com/math-comp/math-comp) - opam: name: coq-gaia-schutte - version: '{(>= "1.14" & < "1.18~") | (= "dev")}' + version: '{>= "1.14" & < "1.18"}' description: |- - [Gaia's Schütte ordinals](https://github.com/coq-community/gaia) 1.14 or later + [Gaia's Schütte ordinals](https://github.com/coq-community/gaia) 1.14 to 1.17 - opam: name: coq-mathcomp-zify version: '{< "2~"}' @@ -165,7 +167,7 @@ dependencies: [LibHyps](https://github.com/Matafou/LibHyps) - opam: name: coq-coqprime - version: '{= "dev"}' + version: '{>= "1.3.0"}' description: |- [CoqPrime](https://github.com/thery/coqprime) - opam: diff --git a/theories/additions/AM.v b/theories/additions/AM.v index 52ef9818..e5436c7a 100644 --- a/theories/additions/AM.v +++ b/theories/additions/AM.v @@ -552,9 +552,9 @@ Function chain_gen (s:signature) {measure signature_measure} | (q, 0%N) => (chain_gen (gen_F (gamma i))) ++ (chain_gen (gen_F (N2pos q))) - | (q,r) => KFF (chain_gen - (gen_K (N2pos r) - (gamma i - N2pos r))) + | (q,_r) => KFF (chain_gen + (gen_K (N2pos _r) + (gamma i - N2pos _r))) (chain_gen (gen_F (N2pos q))) end @@ -565,8 +565,8 @@ Function chain_gen (s:signature) {measure signature_measure} match N.pos_div_eucl (p + d) (Npos p) with | (q, 0%N) => FFK (chain_gen (gen_F p)) (chain_gen (gen_F (N2pos q))) - | (q,r) => KFK (chain_gen (gen_K (N2pos r) - (p - N2pos r))) + | (q, _r) => KFK (chain_gen (gen_K (N2pos _r) + (p - N2pos _r))) (chain_gen (gen_F (N2pos q))) end end. @@ -601,20 +601,20 @@ Proof. + apply IHc. + apply IHc0. - cbn; pattern i at 1; - replace i with (gamma i * (N2pos q) + N2pos r). + replace i with (gamma i * (N2pos q) + N2pos _r). + cbn in *. * apply KFF_correct;auto. replace (gamma i) with - (N2pos r + (gamma i - N2pos r)) at 1. + (N2pos _r + (gamma i - N2pos _r)) at 1. -- apply IHc. -- rewrite Pplus_minus;auto with chains. apply Pos.lt_gt; rewrite N2pos_lt_switch2. generalize (N.pos_div_eucl_remainder i (N.pos (gamma i) )); rewrite e3; simpl;auto with chains. - destruct r; [ contradiction | auto with chains]. + destruct _r; [ contradiction | auto with chains]. + apply N_pos_div_eucl_rest; auto with chains. - destruct r;try contradiction; auto with chains. + destruct _r;try contradiction; auto with chains. apply (div_gamma_pos _ _ _ e3); auto with chains. apply pos_gt_3;auto with chains. destruct (exact_log2 i); [contradiction | reflexivity]. @@ -630,15 +630,15 @@ Proof. N2pos_destruct q q. injection H4;auto with chains. rewrite Pos.mul_comm; auto with chains. - - cbn; red; replace (p+d) with (p * N2pos q + N2pos r). + - cbn; red; replace (p+d) with (p * N2pos q + N2pos _r). + apply KFK_correct;auto with chains. - cbn in *; replace (N2pos r + (p - N2pos r))%positive with p in IHc. + cbn in *; replace (N2pos _r + (p - N2pos _r))%positive with p in IHc. apply IHc. rewrite Pplus_minus; auto. generalize (N.pos_div_eucl_remainder (p + d) (N.pos p)); rewrite e1; cbn; intro H3. apply Pos.lt_gt; rewrite N2pos_lt_switch2;auto with chains. - destruct r; [contradiction | auto with chains]. + destruct _r; [contradiction | auto with chains]. + generalize (N.pos_div_eucl_spec (p + d) (N.pos p)). rewrite e1; intros H3. @@ -647,7 +647,7 @@ Proof. destruct 1;auto with chains. rewrite pos2N_inj_add; apply N.le_add_r. } - { intros p0 Hp0;subst q; cbn; destruct r; [ contradiction | ]. + { intros p0 Hp0;subst q; cbn; destruct _r; [ contradiction | ]. simpl; simpl in H3; injection H3. rewrite Pos.mul_comm; auto with chains. } @@ -702,3 +702,4 @@ Time Compute chain_apply F197887 NPlus 1%N. Time Compute chain_apply F197887 NPlus 1%N. + diff --git a/theories/additions/Demo_power.v b/theories/additions/Demo_power.v index f626ab98..b196be7b 100644 --- a/theories/additions/Demo_power.v +++ b/theories/additions/Demo_power.v @@ -4,11 +4,11 @@ Open Scope M_scope. Compute 22%Z ^ 20. -Import Int31. +Import Uint63. +Search (Z -> int). +Coercion of_Z : Z >-> int. -Coercion phi_inv : Z >-> int31. - -Compute 22%int31 ^ 20. +Compute 22%int63 ^ 50. (* end snippet DemoPower *) diff --git a/theories/additions/Dichotomy.v b/theories/additions/Dichotomy.v index 42d74a58..9b40a7ca 100644 --- a/theories/additions/Dichotomy.v +++ b/theories/additions/Dichotomy.v @@ -171,7 +171,7 @@ Proof. intros p H; unfold dicho; generalize (dicho_aux_lt p H). intro H0; assert (2 <= N.pos p / (N.pos (dicho_aux p)) )%N. - replace 2%N with (2%N * Npos (dicho_aux p) / Npos (dicho_aux p))%N. - + apply (* N.Div0.div_le_mono. *) N.div_le_mono; try discriminate. + + apply N.div_le_mono; try discriminate. * replace 2%N with (Npos 2%positive); cbn;auto. + rewrite N.div_mul; [auto | discriminate]. - case_eq (N.pos p / N.pos (dicho_aux p))%N. diff --git a/theories/additions/Euclidean_Chains.v b/theories/additions/Euclidean_Chains.v index a28ff77b..53054dc3 100644 --- a/theories/additions/Euclidean_Chains.v +++ b/theories/additions/Euclidean_Chains.v @@ -162,6 +162,7 @@ Compute the_exponent (F2C F9). + (** A first attempt to define Fchain correctness *) (* begin snippet BadDefa *) @@ -1369,9 +1370,9 @@ Function chain_gen (s:signature) {measure signature_measure} | (q, 0%N) => Fcompose (chain_gen (gen_F (gamma i))) (chain_gen (gen_F (N2pos q))) - | (q,r) => KFF (chain_gen - (gen_K (N2pos r) - (gamma i - N2pos r))) + | (q,_r) => KFF (chain_gen + (gen_K (N2pos _r) + (gamma i - N2pos _r))) (chain_gen (gen_F (N2pos q))) end end | gen_K p d => @@ -1380,8 +1381,8 @@ Function chain_gen (s:signature) {measure signature_measure} match N.pos_div_eucl (p + d) (Npos p) with | (q, 0%N) => FFK (chain_gen (gen_F p)) (chain_gen (gen_F (N2pos q))) - | (q,r) => KFK (chain_gen (gen_K (N2pos r) - (p - N2pos r))) + | (q, _r) => KFK (chain_gen (gen_K (N2pos _r) + (p - N2pos _r))) (chain_gen (gen_F (N2pos q))) end end. @@ -1426,23 +1427,23 @@ Proof. - pattern i at 1; - replace i with (gamma i * (N2pos q) + N2pos r). + replace i with (gamma i * (N2pos q) + N2pos _r). + destruct IHc, IHc0;split. * apply KFF_correct;auto. simpl; simpl in H. replace (gamma i) with - (N2pos r + (gamma i - N2pos r)) at 1. + (N2pos _r + (gamma i - N2pos _r)) at 1. apply H. rewrite Pplus_minus;auto with chains. apply Pos.lt_gt; rewrite N2pos_lt_switch2. generalize (N.pos_div_eucl_remainder i (N.pos (gamma i) )); rewrite e3; simpl;auto with chains. - destruct r; [ contradiction | auto with chains]. + destruct _r; [ contradiction | auto with chains]. * apply KFF_proper;auto with chains. + apply N_pos_div_eucl_rest; auto with chains. - destruct r;try contradiction; auto with chains. + destruct _r;try contradiction; auto with chains. apply (div_gamma_pos _ _ _ e3); auto with chains. apply pos_gt_3;auto with chains. destruct (exact_log2 i); [contradiction | reflexivity]. @@ -1468,15 +1469,15 @@ Proof. + apply FFK_proper;auto with chains. - destruct IHc, IHc0; split. - + red; replace (p+d) with (p * N2pos q + N2pos r). + + red; replace (p+d) with (p * N2pos q + N2pos _r). * apply KFK_correct;auto with chains. - red in H; replace (N2pos r + (p - N2pos r))%positive with p in H. + red in H; replace (N2pos _r + (p - N2pos _r))%positive with p in H. apply H. rewrite Pplus_minus; auto. generalize (N.pos_div_eucl_remainder (p + d) (N.pos p)); rewrite e1; cbn; intro H3. apply Pos.lt_gt; rewrite N2pos_lt_switch2;auto with chains. - destruct r; [contradiction | auto with chains]. + destruct _r; [contradiction | auto with chains]. * generalize (N.pos_div_eucl_spec (p + d) (N.pos p)); rewrite e1; intros H3; clear H H0 H1 H2. @@ -1486,7 +1487,7 @@ Proof. rewrite pos2N_inj_add; apply N.le_add_r. } { - intros p0 Hp0;subst q; cbn; destruct r; [ contradiction | ]. + intros p0 Hp0;subst q; cbn; destruct _r; [ contradiction | ]. simpl; simpl in H3; injection H3. rewrite Pos.mul_comm; auto with chains. } @@ -1508,23 +1509,26 @@ Arguments make_chain gamma {_} _ _ _ . Compute the_exponent (make_chain dicho 87). (* end snippet C87Dicho *) -(** cf Coq workshop 2014 by Jason Grosss *) -Module Examples. +Require Import Int63.Uint63. +Require Import Monoid_instances. -Import Int31. +Check cpower (make_chain dicho) 10. +Module Examples. Compute cpower (make_chain dicho) 10 12. Compute cpower (make_chain dicho) 87 12. +Search (int -> Z). +Search (positive -> int). + -Definition fast_int31_power (x :positive)(n:N) : Z := - Int31.phi (cpower (make_chain dicho) n (snd (positive_to_int31 x))). +Definition fast_int63_power (x :positive)(n:N) : Z := + to_Z (cpower (make_chain dicho) n (of_pos x)). Definition slow_int31_power (x :positive)(n:N) : Z := - Int31.phi (power (snd (positive_to_int31 x)) (N.to_nat n) ). + to_Z (power (of_pos x) (N.to_nat n) ). Definition binary_int31_power (x :positive)(n:N) : Z := -Int31.phi (N_bpow (snd (positive_to_int31 x)) n ). - + to_Z (N_bpow (of_pos x) n). (** long computations ... *) @@ -1537,7 +1541,7 @@ Arguments big_chain _%type_scope. Remark RM : (1 < 56789)%N. Proof. reflexivity. Qed. -Definition M := Nmod_Monoid _ RM. +Definition M := Nmod_Monoid 56789%N RM. Definition exp56789 x := chain_apply big_chain (M:=M) x. @@ -1550,12 +1554,6 @@ Eval cbv iota match delta [big_chain chain_apply computation_eval ] zeta beta Definition C87' := ltac:( compute_chain C87 ). -Time Compute Int31.phi - (chain_apply big_chain (snd (positive_to_int31 67777))) . - - -Compute Int31.phi (chain_apply big_chain (snd (positive_to_int31 67777))) . - Compute chain_length big_chain. Goal parametric (make_chain dicho 45319). diff --git a/theories/additions/Monoid_instances.v b/theories/additions/Monoid_instances.v index faca16b2..5478716c 100644 --- a/theories/additions/Monoid_instances.v +++ b/theories/additions/Monoid_instances.v @@ -10,7 +10,7 @@ Require Import RelationClasses Morphisms. Require Import ZArith PArith. Require Import Arith. Require Import NArith. -Require Import Ring31. +Require Import Ring63. Open Scope Z_scope. @@ -100,25 +100,25 @@ Proof. Qed. -Import Int31. -Open Scope int31_scope. +Import Uint63. +Open Scope int63_scope. -(** *** Multiplicative monoid on 31-bits integers +(** *** Multiplicative monoid on 63-bits integers Cyclic numeric types are good candidates for testing exponentiations with big exponents, since the size of data is bounded. -The type [int31] is defined in Standard Library in Module -[Coq.Numbers.Cyclic.Int31.Int31]. +The type [int63] is defined in Standard Library in Module +[Coq.Numbers.Cyclic.Int63.Uint63]. *) (* begin snippet int31:: no-out *) -#[ global ] Instance int31_mult_op : Mult_op int31 := mul31. +#[ global ] Instance int63_mult_op : Mult_op int := mul. -#[ global ] Instance Int31mult : Monoid int31_mult_op 1. +#[ global ] Instance Int63mult : Monoid int63_mult_op 1. Proof. - split;unfold int31_mult_op, mult_op; intros; ring. + split;unfold int63_mult_op, mult_op; intros; ring. Qed. (* end snippet int31 *) @@ -127,25 +127,25 @@ Qed. (* begin snippet BadFact *) Module Bad. - Fixpoint int31_from_nat (n:nat) := + Fixpoint int63_from_nat (n:nat) :int := match n with | O => 1 - | S p => 1 + int31_from_nat p + | S p => 1 + int63_from_nat p end. - Coercion int31_from_nat : nat >-> int31. + Coercion int63_from_nat : nat >-> int. - Fixpoint fact (n:nat) := match n with + Fixpoint fact (n:nat) : int := match n with O => 1 | S p => n * fact p end. - Compute fact 40. + Compute fact 160. End Bad. (* end snippet BadFact *) -Close Scope int31_scope. +Close Scope int63_scope. (** *** Monoid of 2x2 matrices @@ -261,12 +261,13 @@ Section Nmodulo. (* end snippet Nmoduloc *) Proof. unfold mod_equiv, mod_op, mult_mod, mod_eq. - intros x y Hxy z t Hzt. + intros x y Hxy z t Hzt. rewrite N.mod_mod. repeat rewrite N.mod_mod; auto with chains. rewrite (N.mul_mod x z);auto with chains. rewrite (N.mul_mod y t);auto with chains. rewrite Hxy, Hzt; reflexivity. - Qed. + intros ?; subst. inversion m_gt_1. +Qed. (* begin snippet Nmodulod:: no-out *) #[local] Open Scope M_scope. diff --git a/theories/goedel/PRrepresentable.v b/theories/goedel/PRrepresentable.v index b174758d..e7c6e27c 100644 --- a/theories/goedel/PRrepresentable.v +++ b/theories/goedel/PRrepresentable.v @@ -1545,7 +1545,7 @@ Proof. ** elim closedNN with v. exists x0; auto. ** destruct H6. destruct H5 as [H5 | H5]; try congruence. fold (freeVarT (n2t a)) in H5. simpl in H5. - rewrite <- app_nil_end in H5. elim (closedNatToTerm _ _ H5). + rewrite app_nil_r in H5. elim (closedNatToTerm _ _ H5). ** apply impE with (LT (var x) (n2t a)). --- apply sysWeaken. apply boundedLT. intros n H5. rewrite (subFormulaNot LNN). diff --git a/theories/goedel/rosserPA.v b/theories/goedel/rosserPA.v index b71b44d8..1750a34a 100644 --- a/theories/goedel/rosserPA.v +++ b/theories/goedel/rosserPA.v @@ -425,7 +425,7 @@ Proof. exists x0; intros g H1; apply extendsPA. fold mem; auto. + exists (LNN2LNT_formula x :: nil); split. - * simpl; repeat rewrite <- app_nil_end. + * simpl; repeat rewrite app_nil_r. apply (LNN2LNT_freeVarF1 x). * exists (AXM _ (LNN2LNT_formula x)). intros g H1; induction H1 as [H1| H1]. diff --git a/theories/ordinals/Ackermann/LNN.v b/theories/ordinals/Ackermann/LNN.v index 51376989..372e8301 100644 --- a/theories/ordinals/Ackermann/LNN.v +++ b/theories/ordinals/Ackermann/LNN.v @@ -114,16 +114,16 @@ Section Free_Variables. Lemma freeVarPlus (x y : Term) : freeVarT (Plus x y) = freeVarT x ++ freeVarT y. -Proof. now rewrite (app_nil_end (freeVarT y)). Qed. +Proof. now rewrite <- (app_nil_r (freeVarT y)). Qed. Lemma freeVarTimes (x y : Term): freeVarT (Times x y) = freeVarT x ++ freeVarT y. -Proof. now rewrite (app_nil_end (freeVarT y)). Qed. +Proof. now rewrite <- (app_nil_r (freeVarT y)). Qed. Lemma freeVarSucc (x : Term): freeVarT (Succ x) = freeVarT x. Proof. - now rewrite (app_nil_end (freeVarT x)). + now rewrite <- (app_nil_r (freeVarT x)). Qed. Lemma freeVarZero : freeVarT Zero = nil. @@ -132,7 +132,7 @@ Proof. reflexivity. Qed. Lemma freeVarLT (x y : Term) : freeVarF (LT x y) = freeVarT x ++ freeVarT y. Proof. - now rewrite (app_nil_end (freeVarT y)). + now rewrite <- (app_nil_r (freeVarT y)). Qed. End Free_Variables. diff --git a/theories/ordinals/Ackermann/LNN2LNT.v b/theories/ordinals/Ackermann/LNN2LNT.v index d41d9ace..96f832ae 100644 --- a/theories/ordinals/Ackermann/LNN2LNT.v +++ b/theories/ordinals/Ackermann/LNN2LNT.v @@ -237,7 +237,7 @@ Proof. rewrite <- (nilTerms _ b0). unfold freeVarTs in |- *. fold (@freeVarT LNN) in |- *. - rewrite <- app_nil_end. + rewrite app_nil_r. split. + intros H; decompose record (freeVarSubAllFormula1 _ _ _ _ H) /r. intros H x [H0| H0] H2. @@ -617,7 +617,7 @@ Proof. + exists x; destruct H0 as [H0 H1]. split. * apply H0. - * intros v H2; simpl; rewrite <- app_nil_end. + * intros v H2; simpl; rewrite app_nil_r. apply H1, H2. - assert (H0: forall g : fol.Formula LNN, In g Axm2 -> mem (fol.Formula LNN) U g). diff --git a/theories/ordinals/Ackermann/LNT.v b/theories/ordinals/Ackermann/LNT.v index 41a637c5..982c8ff7 100644 --- a/theories/ordinals/Ackermann/LNT.v +++ b/theories/ordinals/Ackermann/LNT.v @@ -110,19 +110,19 @@ Section Free_Variables. Lemma freeVarPlus (x y: Term) : freeVarT (Plus x y) = freeVarT x ++ freeVarT y. Proof. - now rewrite (app_nil_end (freeVarT y)). + now rewrite <- (app_nil_r (freeVarT y)). Qed. Lemma freeVarTimes (x y : Term) : freeVarT (Times x y) = freeVarT x ++ freeVarT y. Proof. - now rewrite (app_nil_end (freeVarT y)). + now rewrite <- (app_nil_r (freeVarT y)). Qed. Lemma freeVarSucc (x : Term): freeVarT (S_ x)%nt = freeVarT x. Proof. - now rewrite (app_nil_end (freeVarT x)). + now rewrite <- (app_nil_r (freeVarT x)). Qed. Lemma freeVarZero : freeVarT Zero = nil. diff --git a/theories/ordinals/Ackermann/codeSubFormula.v b/theories/ordinals/Ackermann/codeSubFormula.v index e4492b60..ed525058 100644 --- a/theories/ordinals/Ackermann/codeSubFormula.v +++ b/theories/ordinals/Ackermann/codeSubFormula.v @@ -4817,7 +4817,7 @@ Proof. apply Nat.le_max_l. simpl; apply maxLemma. apply le_n. - rewrite ass_app. + rewrite app_assoc. apply maxLemma2. ++ apply Nat.le_trans with (evalStrongRec 1 A (codeFormula f1) diff --git a/theories/ordinals/Epsilon0/T1.v b/theories/ordinals/Epsilon0/T1.v index 263b4597..c9872957 100644 --- a/theories/ordinals/Epsilon0/T1.v +++ b/theories/ordinals/Epsilon0/T1.v @@ -99,7 +99,7 @@ Fixpoint T1is_succ alpha := match alpha with | zero => false | cons zero _ _ => true - | cons alpha n beta => T1is_succ beta + | cons _alpha _n beta => T1is_succ beta end. diff --git a/theories/ordinals/MoreAck/LNN_Examples.v b/theories/ordinals/MoreAck/LNN_Examples.v index 8d0f0cc7..d8bdf2ce 100644 --- a/theories/ordinals/MoreAck/LNN_Examples.v +++ b/theories/ordinals/MoreAck/LNN_Examples.v @@ -114,9 +114,9 @@ Compute List.nodup Nat.eq_dec (freeVarF f3). Compute close _ f3. -Compute freeVarFormula f3. +Compute freeVarF f3. -Compute freeVarFormula (close _ f4). +Compute freeVarF (close _ f4). Compute substF f4 0 (natToTerm 0). (* end snippet freeVarExamples *) diff --git a/theories/ordinals/OrdinalNotations/ON_Omega2.v b/theories/ordinals/OrdinalNotations/ON_Omega2.v index 05f0b8fc..087798e5 100644 --- a/theories/ordinals/OrdinalNotations/ON_Omega2.v +++ b/theories/ordinals/OrdinalNotations/ON_Omega2.v @@ -371,7 +371,7 @@ Definition plus (alpha beta : t) : t := | (0, b), (0, b') => (0, b + b') | (0,0), y => y | x, (0,0) => x - | (0, b), (S n', b') => (S n', b') + | (0, _b), (S n', b') => (S n', b') | (S n, b), (S n', b') => (S n + S n', b') | (S n, b), (0, b') => (S n, b + b') end. diff --git a/theories/ordinals/rpo/dickson.v b/theories/ordinals/rpo/dickson.v index cb6bb211..73ba9949 100644 --- a/theories/ordinals/rpo/dickson.v +++ b/theories/ordinals/rpo/dickson.v @@ -87,7 +87,7 @@ intros R l1 l2 l H; destruct H as [l1 l2 l12 la a H P1 P2]. apply (@rmv_case R (l++l1) (l++l2) (l++l12) la a); trivial. apply list_permut_trans with (l ++ la ++ l12). apply context_list_permut_app1; trivial. -do 2 rewrite <- app_ass; apply context_list_permut_app2; trivial. +do 2 rewrite app_assoc; apply context_list_permut_app2; trivial. apply list_permut_app_app. apply list_permut_trans with (l ++ a :: l12). apply context_list_permut_app1; trivial. @@ -111,7 +111,7 @@ Lemma context_multiset_extension_step_app2 : Proof. intros R l1 l2 l H; destruct H as [l1 l2 l12 la a H P1 P2]. apply (@rmv_case R (l1++l) (l2++l) (l12++l) la a); trivial. -rewrite <- app_ass; apply context_list_permut_app2; trivial. +rewrite app_assoc; apply context_list_permut_app2; trivial. rewrite app_comm_cons; apply context_list_permut_app2; trivial. Qed. @@ -231,10 +231,10 @@ generalize (split_list_app_cons eq_elt_dec _ _ a_in_q'); destruct (split_list eq_elt_dec q' a) as [q1' q2']; intro; subst. exists (la ++ q1' ++ q2'); exists r'; exists qr; split. refine (list_permut_trans Pp _). -do 2 rewrite app_ass; apply context_list_permut_app1. +do 2 rewrite <- app_assoc; apply context_list_permut_app1. apply list_permut_remove_hd with a. refine (list_permut_trans (list_permut_sym Pq) _). -rewrite app_comm_cons; rewrite <- app_ass; trivial. +rewrite app_comm_cons; rewrite app_assoc; trivial. split; trivial. split; trivial. intros b b_in_la_q1'_q2'; @@ -250,14 +250,14 @@ generalize (split_list_app_cons eq_elt_dec _ _ a_in_qr); destruct (split_list eq_elt_dec qr a) as [qr1 qr2]; intro; subst. exists (la ++ q'); exists (a :: r'); exists (qr1 ++ qr2); split. refine (list_permut_trans Pp _). -rewrite app_ass; apply context_list_permut_app1. -rewrite <- app_ass; apply list_permut_remove_hd with a. +rewrite <- app_assoc; apply context_list_permut_app1. +rewrite app_assoc; apply list_permut_remove_hd with a. refine (list_permut_trans (list_permut_sym Pq) _). -rewrite app_ass; trivial. +rewrite <- app_assoc; trivial. split. -refine (list_permut_trans Pr _); rewrite <- app_ass; +refine (list_permut_trans Pr _); rewrite app_assoc; apply list_permut_sym; simpl; apply list_permut_add_cons_inside; -rewrite ass_app; apply list_permut_refl. +rewrite app_assoc; apply list_permut_refl. split. discriminate. intros b b_in_la_q'; diff --git a/theories/ordinals/rpo/list_permut.v b/theories/ordinals/rpo/list_permut.v index a639af10..b002e789 100644 --- a/theories/ordinals/rpo/list_permut.v +++ b/theories/ordinals/rpo/list_permut.v @@ -379,9 +379,9 @@ intros l2 l3 l4 P; rewrite <- app_comm_cons in P; elim (in_app_or l3 l4 a (cons_permut_in P)); intro In_a; generalize (split_list_app_cons eq_elt_dec a _ In_a). destruct (split_list eq_elt_dec l3 a); intro; subst l3; -rewrite app_ass in P; rewrite <- app_comm_cons in P; +rewrite <- app_assoc in P; rewrite <- app_comm_cons in P; generalize (list_permut_remove_hd _ _ P); clear P; -intro P; rewrite <- app_ass in P; +intro P; rewrite app_assoc in P; elim (IHl1 l2 (l ++ l0) l4 P); clear IHl1 P; intros u1 H; elim H; clear H; intros u2 H; elim H; clear H; @@ -397,9 +397,9 @@ apply list_permut_sym; apply list_permut_add_cons_inside; apply list_permut_sym; trivial. destruct (split_list eq_elt_dec l4 a); intro; subst l4; -rewrite <- app_ass in P; +rewrite app_assoc in P; generalize (list_permut_remove_hd _ _ P); clear P; -intro P; rewrite app_ass in P; +intro P; rewrite <- app_assoc in P; elim (IHl1 l2 l3 (l ++ l0) P); clear IHl1 P; intros u1 H; elim H; clear H; intros u2 H; elim H; clear H; diff --git a/theories/ordinals/rpo/rpo.v b/theories/ordinals/rpo/rpo.v index 8edb43e5..2612154f 100644 --- a/theories/ordinals/rpo/rpo.v +++ b/theories/ordinals/rpo/rpo.v @@ -472,11 +472,11 @@ intros lsg H'; elim H'; clear H'; intros P1 H'; elim H'; clear H'; intros P2 H'; elim H'; clear H'; intros P3 P4; apply (List_mul a (lg ++ lcg) (ls0 ++ lsc) lcc). -rewrite <- ass_app; apply list_permut_trans with (ls0 ++ lc0); trivial; +rewrite <- app_assoc; apply list_permut_trans with (ls0 ++ lc0); trivial; apply context_list_permut_app1; trivial. apply list_permut_trans with (lcc ++ lsc); trivial; apply list_permut_app_app. apply list_permut_trans with (a :: lg ++ lc); trivial; -apply context_list_permut_cons; rewrite <- ass_app; +apply context_list_permut_cons; rewrite <- app_assoc; apply context_list_permut_app1; apply list_permut_trans with (lcc ++ lcg); trivial; apply list_permut_app_app. intros b In_b; elim (in_app_or _ _ _ In_b); clear In_b; intro In_b. @@ -565,11 +565,11 @@ intros lsg H'; elim H'; clear H'; intros P1 H'; elim H'; clear H'; intros P2 H'; elim H'; clear H'; intros P3 P4; apply (List_mul a (lg ++ lcg) (ls0 ++ lsc) lcc). -rewrite <- ass_app; apply list_permut_trans with (ls0 ++ lc0); trivial; +rewrite <- app_assoc; apply list_permut_trans with (ls0 ++ lc0); trivial; apply context_list_permut_app1; trivial; apply list_permut_trans with (lcc ++ lsc); trivial; apply list_permut_app_app. apply list_permut_trans with (a :: lg ++ lc); trivial; -apply context_list_permut_cons; rewrite <- ass_app; +apply context_list_permut_cons; rewrite <- app_assoc; apply context_list_permut_app1; apply list_permut_trans with (lcc ++ lcg); trivial; apply list_permut_app_app. intros b In_b; elim (in_app_or _ _ _ In_b); clear In_b; intro In_b. @@ -840,7 +840,7 @@ intros ls1 H; elim H; clear H; intros ls2 H; apply t_trans with (a0 :: ls2 ++ lc). apply t_step; apply (List_mul_rest_step a0 ls1 (ls2 ++ lc)). apply list_permut_trans with (map tt (ls ++ lc)); trivial. -rewrite <- app_ass; do 2 rewrite map_app; apply context_list_permut_app2; intuition. +rewrite app_assoc; do 2 rewrite map_app; apply context_list_permut_app2; intuition. apply list_permut_refl. intuition. apply (IHlg (a0 :: ls2 ++ lc) l a ls2 (a0 :: lc)). @@ -887,16 +887,16 @@ apply list_permut_trans with ((map tt ls) ++ tt1 :: (map tt lc)). apply list_permut_add_cons_inside; rewrite map_app; apply list_permut_refl. apply list_permut_trans with (map tt ls ++ (tt0 :: l ++ tt1 :: l0)). apply context_list_permut_app1; apply list_permut_sym; rewrite <- H2; trivial. -rewrite app_comm_cons; rewrite <- app_ass; apply list_permut_sym; +rewrite app_comm_cons; rewrite app_assoc; apply list_permut_sym; apply list_permut_add_cons_inside; -rewrite app_ass; rewrite <- app_comm_cons; simpl; +rewrite <- app_assoc; rewrite <- app_comm_cons; simpl; apply list_permut_add_cons_inside; do 2 rewrite map_app; do 2 rewrite projection_list_of_SN_terms; -do 2 rewrite <- app_ass; apply context_list_permut_app2; +do 2 rewrite app_assoc; apply context_list_permut_app2; apply list_permut_app_app. apply (List_mul_rest_step (mk_sn tt1 sn1) ls (build_list_of_SN_terms l H3 ++ build_list_of_SN_terms l0 H4)); intuition. -do 2 rewrite ass_app; do 4 rewrite map_app; +do 2 rewrite app_assoc; do 4 rewrite map_app; apply context_list_permut_app2; apply list_permut_app_app. rewrite H2; simpl; rewrite map_app; do 2 rewrite projection_list_of_SN_terms; apply list_permut_sym; apply list_permut_add_cons_inside;