internship2019's People
internship2019's Issues
Opérations sur les hypothèses nommées
Lines 59 to 71 in 17e55db
en ssreflect on essaie le plus souvent de faire les opérations sur le but directement plutôt que d'introduire une hypothèse avec un nom et effectuer des
apply _ in _
, move/_ in _
rewrite _ in _
. Pour le lemme ci-dessus cela donne par exemple :
Lemma ltn_0_prod_f {T : Type} :
forall s (f : T -> nat), all (ltn 0) [seq f x | x <- s]
-> 0 < \prod_(n <- s) f n.
Proof.
elim=> [|m s IHs] f ; rewrite BigOp.bigopE // /=.
move/andP=> [m_gt_0 s_gt_0].
simpl.
rewrite {1}[0]/(0 * 0) -mulnE.
apply ltn_mul=> //.
rewrite -BigOp.bigopE.
by apply IHs.
Qed.
mem_cons
Line 224 in 17e55db
Ce lemme devrait plutôt être dans seq2
ltn_leq_trans
Line 35 in 17e55db
Ce lemme est en fait une instance de leq_trans car
m<n
est codé par m.+1<=n
. Du coup tu peux remplacer partout ltn_leq_trans par leq_trans et supprimer ce lemme.equiv_eqP
Line 6 in 17e55db
ce lemme peut être évité : si le but est
b=b'
alors
apply/eqP/equiv_eqP ; first apply idP ; first apply idP; split.
peut être remplacé par :
apply/idP/idP.
pose proof _ as _
Lines 413 to 414 in 17e55db
en ssreflect on écrit plutôt :
move: (coprime_dvdr p_coprime_n m_coprime_n)=> m_coprime_p.
move: (coprime_dvdl p_coprime_m m_coprime_p)=> p_coprime_p.
ou encore simplement :
move: (coprime_dvdr p_coprime_n m_coprime_n).
move: (coprime_dvdl p_coprime_m m_coprime_p).
pour garder les assertions dans le but (c.f. issue #11)
nth
Lines 310 to 324 in 17e55db
ici et à plusieurs autres endroits tu passes par
nth
, ce qui n'est pas nécessaire. Par exemple le morceau de preuve ci-dessus peut être remplacé par :
move=> n_p_dvd_m b.
rewrite eqnE eq_sym.
move/mapP=> [n].
rewrite mem_index_iota=> /andP [] n_gt_0 _ ->.
rewrite eqb0.
apply/negP=> n_p_n_dvd_m.
apply: n_p_dvd_m.
by apply (dvdn_exp2 _ _ n).
anti_ltn
Line 16 in 17e55db
Même si c'est formellement vrai, c'est très troublant de lire que < est antisymmétrique. Il me semble que tu utilises ce lemme uniquement avec sorted_primes. Il serait plus naturel de montrer :
sorted_primes_leq : forall n : nat, sorted (T:=nat_eqType) leq (primes n)
ou encore :
sorted_leq_ltn : forall s, sorted ltn s -> sorted leq s
qui se prouve facilement avec ltn_sorted_uniq_leq.
mem_head_or_behead
Line 4 in 17e55db
ce lemme est dans ssreflect.seq et s'appelle in_cons
mem_big_eq
Line 68 in 17e55db
ce lemme peut être prouvé par :
by move=> x s; rewrite big_has has_pred1.
du coup ce n'est peut-être pas la peine de le prouver séparément.
ltn_0_prod
Line 59 in 17e55db
ce lemme n'est pas utilisé (et se prouve trivialement à partir de ltn_0_prod_f et map_id)
eq_map_eq
assert _ as _
style ssreflect
Dans le style ssreflect on n'utilise pas destruct
, mais case
.
D'autre part on n'utilise pas non plus fold
ou unfold
, mais plutôt rewrite -/cste
et rewrite /cste
Par exemple :
Lines 105 to 112 in 17e55db
s'écrit plutôt :
Lemma lognn : forall n, logn n n = prime n.
Proof.
move=> n.
case n_prime: (prime n) ; rewrite /logn n_prime //.
case: n n_prime=> [|n] n_prime ; first inversion n_prime.
rewrite /= edivn_def /= divnn modnn /=.
by case: n n_prime=> [|n] n_prime ; first inversion n_prime.
Qed.
factorisation de preuves
Lines 377 to 392 in 17e55db
ce morceau de preuve est répété deux fois d'affilée. Il serait mieux de prouver par exemple le lemme :
forall p m, coprime p m -> all (coprime p) (primes m).
eq_in_map_eq
destruct _ as [_]eqn:_
Line 192 in 17e55db
destruct
n'est pas utilisé en ssreflect. L'équivalent de la ligne ci-dessus est :
case n_decomp: (prime_decomp n)=> [|[p a] t] ; first by rewrite /primepow n_decomp.
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.