Open vblot opened 5 years ago
https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L59-L71 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 :
apply _ in _
move/_ in _
rewrite _ in _
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.
https://github.com/esum/internship2019/blob/17e55dbe0e3ad5da653a4b8086714a4b61c4177a/src/arith.v#L59-L71 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 :