Giter VIP home page Giter VIP logo

internship2019's People

Contributors

esum avatar

Watchers

avatar

internship2019's Issues

mem_big_eq

internship2019/src/seq2.v

Line 68 in 17e55db

Lemma mem_big_eq {T : eqType} :

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.

eq_in_map_eq

internship2019/src/seq2.v

Line 51 in 17e55db

Lemma eq_in_map_eq {T1 : eqType} {T2 : Type} :

ce lemme n'est pas vraiment nécessaire. Son utilisation ici :

internship2019/src/arith.v

Line 741 in 17e55db

apply eq_in_map_eq.

peut être remplacée par :

  have ->: primes m = primes n; last first.
    apply eq_in_map.
    move=> p p_in ; rewrite H //.
    rewrite mem_primes in p_in.
    move/and3P in p_in.
    by destruct p_in.

pose proof _ as _

internship2019/src/arith.v

Lines 413 to 414 in 17e55db

pose proof (coprime_dvdr p_coprime_n m_coprime_n) as m_coprime_p.
pose proof (coprime_dvdl p_coprime_m m_coprime_p) as p_coprime_p.

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

internship2019/src/arith.v

Lines 310 to 324 in 17e55db

move=> n_p_dvd_m b b_in.
rewrite eqnE eq_sym.
move/nthP in b_in.
destruct (b_in 0) as [i H H0].
rewrite size_map in H.
rewrite (nth_map 1) // in H0.
rewrite -H0 eqn0_negb.
apply/negP.
move=> H1.
apply n_p_dvd_m.
apply dvdn_exp2 with (nth 1 (index_iota 1 m) i) ; last by [].
assert (nth 1 (index_iota 1 m) i \in (index_iota 1 m)) as e_in_iota ; first by apply mem_nth.
rewrite mem_index_iota in e_in_iota.
move/andP in e_in_iota.
by destruct e_in_iota.

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).

ltn_leq_trans

internship2019/src/arith.v

Line 35 in 17e55db

Lemma ltn_leq_trans : forall x y z, ltn x y -> leq y z -> ltn x z.

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.

anti_ltn

internship2019/src/arith.v

Line 16 in 17e55db

Lemma anti_ltn : antisymmetric ltn.

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.

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 :

internship2019/src/arith.v

Lines 105 to 112 in 17e55db

Lemma lognn : forall n, logn n n = prime n.
Proof.
move=> n.
destruct (prime n)eqn:n_prime ; unfold logn ; rewrite n_prime //.
destruct n as [|n] ; first inversion n_prime.
rewrite /= edivn_def /= divnn modnn /=.
by destruct n as [|n] ; first inversion n_prime.
Qed.

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

internship2019/src/arith.v

Lines 377 to 392 in 17e55db

destruct (coprime p m)eqn:p_coprime_m.
apply/orP.
left.
apply/allP.
move=> b b_in.
move/nthP in b_in.
destruct (b_in false) as [i Hb Hb0].
rewrite size_map in Hb.
rewrite (nth_map (0, 0) false) // in Hb0.
remember (nth (0, 0) (prime_decomp m) i) as q ; destruct q as [q a].
rewrite -Hb0 eq_sym bool_eq_true.
apply coprime_dvdr with m ; last by [].
apply (mem_nth (0, 0)) in Hb.
rewrite -Heqq in Hb.
apply mem_prime_decomp in Hb.
apply dvdn_exp2 with a ; by destruct Hb.

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).

destruct _ as [_]eqn:_

internship2019/src/arith.v

Line 192 in 17e55db

destruct (prime_decomp n) as [|[p a] t]eqn:n_decomp ; first unfold primepow ; first by rewrite n_decomp.

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.

ltn_0_prod

internship2019/src/arith.v

Line 59 in 17e55db

Lemma ltn_0_prod : forall s, all (ltn 0) s -> 0 < \prod_(n <- s) n.

ce lemme n'est pas utilisé (et se prouve trivialement à partir de ltn_0_prod_f et map_id)

equiv_eqP

internship2019/src/arith.v

Line 6 in 17e55db

Lemma equiv_eqP : forall P Q x y, reflect P x -> reflect Q y

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.

Opérations sur les hypothèses nommées

internship2019/src/arith.v

Lines 59 to 71 in 17e55db

Lemma ltn_0_prod : forall s, all (ltn 0) s -> 0 < \prod_(n <- s) n.
Proof.
elim=> [|m s IHs] s_gt_0 ; rewrite BigOp.bigopE //.
rewrite /= in s_gt_0.
move/andP in s_gt_0.
destruct s_gt_0 as [m_gt_0 s_gt_0].
simpl.
rewrite {1}[0]/(0 * 0) -mulnE.
apply ltn_mul.
by [].
rewrite -BigOp.bigopE.
by apply IHs.
Qed.

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.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo 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.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.