Opérations sur les hypothèses nommées

[vblot]

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.