Ssreflect Users Discussion List

[Enrico Tassi <>]

On Mon, Feb 12, 2018 at 12:02:02PM -0500, Mitchell Wand wrote:
> Ahh, thank you.  That is very useful.
> 
> I am impressed that the index is so short.  That means fewer things for me
> to memorize :)
> 
> On the other hand, I find the long chains of tacticals difficult to
> understand.  For example, in
> 
> elim=> [|m IHm] [|n] //; exact: IHm.

Sure, I suggest you try

  elim.
  elim=> [|m IHm].
  elim=> [|m IHm] [|n].
  elim=> [|m IHm] [|n] //.

It takes time and effort, I know, but the pattern above gets readable
after a while.

For example, I've no clue where the line comes from, but I can tell you
that there is an induction going on, with 2 branches (I guess on a
natural number, since m is a name for numbers) and in the second case,
then one for the successor, after naming the induction hypothesis the
goal is something like "forall k : nat, ..." and we reason by cases on
that k (in the case it is not zero, it is "S n").  Now I guess 2 out of
three goals are trivial, solved by //, and the last one (probably the
third one) matches the induction hypothesis.

Hope it helps,
-- 
Enrico Tassi