Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Purge redundant misc lemmas #61

Merged
merged 3 commits into from
Aug 3, 2023
Merged

Purge redundant misc lemmas #61

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
4d7fc10
forall_cons and exists_cons are available in MathComp 2.0, so remove …
palmskog Aug 2, 2023
b875ea3
bigmax_seq_sup exists in MathComp 2.0 as bigmax_sup_seq, so remove lo…
palmskog Aug 2, 2023
abac22a
card_leq_inj is leq_card and bij_card is bij_eq_card in MathComp 2.0,…
palmskog Aug 2, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions theories/dfa.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -181,7 +181,7 @@ Section CutOff.
case H: (size x < #|rT|.+1).
+ apply/existsP. exists (Ordinal H). apply/existsP. by exists (in_tuple x).
+ have: ~ injective (fun i : 'I_(size x) => f (take i x)).
{ move/card_leq_inj. by rewrite -ltnS /= card_ord H. }
{ move/leq_card. by rewrite -ltnS /= card_ord H. }
move/injectiveP/injectivePn => [i [j]] Hij.
wlog ltn_ij : i j {Hij} / i < j => [W|] E.
{ move: Hij. rewrite neq_ltn. case/orP => l; exact: W l _. }
Expand Down Expand Up @@ -429,7 +429,7 @@ Section NonRegular.
Proof.
move => f_spec [[A E]].
pose f' (n : 'I_#|A|.+1) := delta_s A (f n).
suff: injective f' by move/card_leq_inj ; rewrite card_ord ltnn.
suff: injective f' by move/leq_card; rewrite card_ord ltnn.
move => [n1 H1] [n2 H2]. rewrite /f' /delta_s /= => H.
apply/eqP; change (n1 == n2); apply/eqP. apply: f_spec => w.
by rewrite /residual !E !inE /dfa_accept !delta_cat H.
Expand Down Expand Up @@ -482,7 +482,7 @@ Section Pumping.
Proof.
rewrite -delta_lang => H1 H2.
have/injectivePn : ~~ injectiveb (fun i : 'I_(size y) => delta (delta_s A x) (take i y)).
apply: contraL H2 => /injectiveP/card_leq_inj. by rewrite leqNgt card_ord.
apply: contraL H2 => /injectiveP/leq_card. by rewrite leqNgt card_ord.
move => [i] [j] ij fij.
wlog {ij} ij : i j fij / i < j. rewrite neq_ltn in ij. case/orP : ij => ij W; exact: W _ ij.
exists (take i y), (sub i j y), (drop j y). split => [||k].
Expand Down
2 changes: 1 addition & 1 deletion theories/minimization.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ Section Isomopism.
Qed.

Lemma dfa_iso_size : dfa_iso A B -> #|A| = #|B|.
Proof. move => [iso [H _ _ _]]. exact (bij_card H). Qed.
Proof. move => [iso [H _ _ _]]. exact (bij_eq_card H). Qed.
End Isomopism.

Lemma abstract_minimization A f :
Expand Down
29 changes: 0 additions & 29 deletions theories/misc.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,22 +56,6 @@ Lemma index_take (T : eqType) (a : T) n (s : seq T) :
a \in take n s -> index a (take n s) = index a s.
Proof. move => H. by rewrite -{2}[s](cat_take_drop n) index_cat H. Qed.

(* from mathcomp-1.13 *)
Lemma forall_cons {T : eqType} {P : T -> Prop} {a s} :
{in a::s, forall x, P x} <-> P a /\ {in s, forall x, P x}.
Proof.
split=> [A|[A B]]; last by move => x /predU1P [-> //|]; apply: B.
by split=> [|b Hb]; apply: A; rewrite !inE ?eqxx ?Hb ?orbT.
Qed.

(* from mathcomp-1.13 *)
Lemma exists_cons {T : eqType} {P : T -> Prop} {a s} :
(exists2 x, x \in a::s & P x) <-> P a \/ exists2 x, x \in s & P x.
Proof.
split=> [[x /predU1P[->|x_s] Px]|]; [by left| by right; exists x|].
by move=> [?|[x x_s ?]]; [exists a|exists x]; rewrite ?inE ?eqxx ?x_s ?orbT.
Qed.

Lemma orS (b1 b2 : bool) : b1 || b2 -> {b1} + {b2}.
Proof. by case: b1 => /= [_|H]; [left|right]. Qed.

Expand All @@ -83,10 +67,6 @@ Proof.
- rewrite inE. case/orS => [/eqP -> //|]. exact: B.
Qed.

Lemma bigmax_seq_sup (T : eqType) (s:seq T) (P : pred T) F k m :
k \in s -> P k -> m <= F k -> m <= \max_(i <- s | P i) F i.
Proof. move => A B C. by rewrite (big_rem k) //= B leq_max C. Qed.

Lemma max_mem n0 (s : seq nat) : n0 \in s -> \max_(i <- s) i \in s.
Proof.
case: s => // a s _. rewrite big_cons big_seq.
Expand Down Expand Up @@ -114,15 +94,6 @@ Lemma sub_exists (T : finType) (P1 P2 : pred T) :
subpred P1 P2 -> [exists x, P1 x] -> [exists x, P2 x].
Proof. move => H. case/existsP => x /H ?. apply/existsP. by exists x. Qed.

Lemma card_leq_inj (T T' : finType) (f : T -> T') : injective f -> #|T| <= #|T'|.
Proof. move => inj_f. by rewrite -(card_imset predT inj_f) max_card. Qed.

Lemma bij_card {X Y : finType} (f : X->Y): bijective f -> #|X| = #|Y|.
Proof.
case => g /can_inj Hf /can_inj Hg. apply/eqP.
by rewrite eqn_leq (card_leq_inj Hf) (card_leq_inj Hg).
Qed.

Lemma cardT_eq (T : finType) (p : pred T) : #|{: { x | p x}}| = #|T| -> p =1 predT.
Proof.
move=> eq_pT; have [|g g1 g2 x] := @inj_card_bij (sig p) T _ val_inj.
Expand Down
2 changes: 1 addition & 1 deletion theories/shepherdson.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -359,7 +359,7 @@ Section DFA2toAFA.
apply: (@leq_trans #|{: table'}|); last by rewrite card_prod card_ffun !card_option expnS.
pose f (x : image_type (@Tab_rc _ M)) : table' :=
let (b,_) := x in ([pick q | q \in b.1],[ffun p => [pick q | (p,q) \in b.2]]).
suff : injective f by apply: card_leq_inj.
suff : injective f by apply: leq_card.
move => [[a1 a2] Ha] [[b1 b2] Hb] [E1 /ffunP E2]. apply: val_inj => /=.
move: Ha Hb => /dec_eq /= [x Hx] /dec_eq [y Hy].
rewrite [Tab M x]surjective_pairing [Tab M y]surjective_pairing !xpair_eqE in Hx Hy.
Expand Down
6 changes: 3 additions & 3 deletions theories/wmso.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -271,7 +271,7 @@ Proof.
- rewrite I_of_glue0. case: (boolP (i < (\max_(k <- N) k).+1)) => ltn_max.
+ by rewrite (nth_map 0) ?size_iota // nth_iota.
+ rewrite nth_default ?size_map ?size_iota 1?leqNgt //.
apply: contraNF ltn_max => H. rewrite ltnS. exact: bigmax_seq_sup H _ _.
apply: contraNF ltn_max => H. rewrite ltnS. exact: bigmax_sup_seq H _ _.
- rewrite I_of_glueS /= /I_of mem_filter mem_iota /= add0n.
case: (ltnP i (size vs)) => H; first by rewrite andbT.
rewrite andbF [nth _ _ i]nth_default //.
Expand Down Expand Up @@ -420,7 +420,7 @@ Proof.
rewrite -addnS leq_add2l index_mem B andTb.
rewrite nth_cat size_tk leqNgt leq_addr /= /i.
by rewrite addnC -addnBA // subnn addn0 nth_index. }
have: i <= k by apply: bigmax_seq_sup i_in_X _ _.
have: i <= k by apply: bigmax_sup_seq i_in_X _ _.
by rewrite /i addSn -ltn_subRL subnn.
+ move/hasPn => /= B. exists [::], v; split => // u in_v.
apply/negbTE/negP => D.
Expand Down Expand Up @@ -457,7 +457,7 @@ Proof.
by rewrite (nth_map (Ordinal lt_n)) ?size_enum_ord ?nth_enum_ord.
+ apply: contraNF A => A. rewrite ltnS. rewrite /lim.
apply: bigmax_sup => //. instantiate (1 := Ordinal lt_n) => /=.
exact: bigmax_seq_sup A _ _ .
exact: bigmax_sup_seq A _ _ .
Qed.

Lemma vec_of_valP I s : satisfies I s <-> satisfies (I_of (vec_of_val I (bound s))) s.
Expand Down
Loading