search

esum / internship2019

0 stars 0 forks source link

style ssreflect #9

Open vblot opened 5 years ago

vblot commented 5 years ago

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 : https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L105-L112 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.