Chaining tactics issues

[Villetaneuse]

Some thoughts I will try to address shortly, but this can start a discussion.
This follows the merging of #66.

1. There is no benefit in using sum and prop in Type instead of \/ and /\ in Prop. Depending on their background, some users can be very surprised that we build functions this way. The same apply to the second part where A, B, ... could perfectly live in Prop.
   Even with a background in type theory, this is not, imho, a case where a proof is much simpler than the hand-written term:

Definition foo (x : A * (B + C + D)) : A * B + A * C + A * D :=
  let (a, bcd) := x in
  match bcd with
  | inl bc => match bc with
              | inl b => inl (inl (a, b))
              | inr c => inl (inr (a, c))
              end
  | inr d => inr (a, d)
  end.

2. Is there an agreement on using Goal instead of Lemma foo1, Lemma foo2? I don't see a strong benefit except being able to give multiple proofs without providing new names for lemmas.
3. We should emphasize that both try and repeat break the "fail fast" principle and may make some proofs very hard to maintain.
4. Some consistency in the proof scripts style could be discussed (bullets, spaces around : or ;, spaces inside brackets, ...)
5. The fact that chaining and tactics like assumption can free us from naming explicitly assumptions could be discussed here.
6. We need to add examples with [tac1 | tac2.. | tacn].
7. The word "tactical" is not used, is it a choice?

[thomas-lamiaux]

1. There is no benefit in using sum and prop in Type instead of \/ and /\ in Prop.

I don't care much but it is easy to change to Prop

2. Is there an agreement on using Goal instead of Lemma foo1, Lemma foo2? I don't see a strong benefit except being able to give multiple proofs without providing new names for lemmas.

I didn't see the point of trying to figure out names, and as I don't reuse them I thought it was easier. But feel free to add them. There is no consensus now but in my work I basically use Definition all the time.

3. We should emphasize that both try and repeat break the "fail fast" principle and may make some proofs very hard to maintain.

You can have a comment or two more but keep in mind that it is also use extensively without issues in many developments like done of ssreflect of std++ version of it. Plus there are already a lot of disclaimer around repeat.

4. Some consistency in the proof scripts style could be discussed (bullets, spaces around : or ;, spaces inside brackets, ...)

I am not sure if it matters. At the opposite, the style seems very uniform to me.

5. The fact that chaining and tactics like assumption can free us from naming explicitly assumptions could be discussed here.

I don't see how it brings much compared to using bullets and repeating the assumption

6. We need to add examples with [tac1 | tac2.. | tacn].

There was one at first, but it didn't feel natural. I removed it as I thought there was already enough examples.

7. The word "tactical" is not used, is it a choice?

I am not exactly sure what it means and I am not sure that there is a proper definition so I didn't use it.