I got a definition like:

```
Definition add (a b: R): R :=
match a, b with
| Some true, _ => Some true
| _, Some true => Some true
| Some false, Some false => Some false
| _, _ => None
end.
```

And a proof of its associativity:

```
Lemma addA: forall a b c:R,
add a (add b c) = add (add a b) c.
Proof.
intros a b c.
induction a.
- induction b as [b|].
+ induction c as [c|].
* induction a; induction b; induction c; now simpl.
* induction a; induction b; now simpl.
+ induction c as [c|].
* induction a; induction c; now simpl.
* induction a; now simpl.
- induction b as [b|].
+ induction c as [c|].
* induction b; induction c; now simpl.
* induction b; now simpl.
+ induction c.
* induction a; now simpl.
* now simpl.
Qed.
```

I was trying to use ssreflect to do the same thing and did:

```
Lemma addA: forall a b c:R,
add a (add b c) = add (add a b) c.
Proof.
move=> a b c; case: a.
move=> a; case: a.
case: b.
move=>a; case: a.
case: c.
move=>a; case: a.
by [].
by [].
by [].
by [].
by [].
case: b.
move=>a; case: a.
case: c.
move=>a; case: a.
by [].
by [].
by [].
case: c.
move=>a; case: a.
by [].
by [].
by [].
case: c.
move=>a; case: a.
by [].
by [].
by [].
case: b.
move=>a; case: a.
case: c.
move=>a; case: a.
by [].
by [].
by [].
case: c.
move=>a; case: a.
by [].
by [].
by [].
case: c.
move=>a; case: a.
by [].
by [].
by [].
Qed.
```

I guess it's safe to say this isn't the right way to go about this due to the repetitive patterns.

How would a better way look like?

Here's my proposal:

```
Lemma addrC (a b c : R) : add a (add b c) = add (add a b) c.
Proof. by move: a b c; do !case. Qed.
```

In general, `by []`

can be replaced with a `move=> //`

somewhere before, or by prepending `by`

to the previous tactic if it solved all goals.

for example, `case: a => //`

automatically solves whatever goals are solvable by `by []`

upon the case distinction on `a`

. If both goals are automatically solvable in that case, it would be more ideomatic to write `by case: a`

```
move=>a; case: a.
```

precisely the point of the ssreflect language is to avoid this step by just doing `case.`

, which will act on top of the stack, avoding having to pick a name. The rest is just tactic chaining which is convenient when all the alternative cases are uniform.

Also, indentation! Whenever a second goal is generated, it's typical to indent the next tactics to reflect this, and to revert to the previous indentation as soon as the new goal has been solved. If your example, the indentation would be:

```
Lemma addA: forall a b c:R,
add a (add b c) = add (add a b) c.
Proof.
move=> a b c; case: a.
move=> a; case: a.
case: b.
move=>a; case: a.
case: c.
move=>a; case: a.
by [].
by [].
by [].
by [].
by [].
case: b.
move=>a; case: a.
case: c.
move=>a; case: a.
by [].
by [].
by [].
case: c.
move=>a; case: a.
by [].
by [].
by [].
case: c.
move=>a; case: a.
by [].
by [].
by [].
case: b.
move=>a; case: a.
case: c.
move=>a; case: a.
by [].
by [].
by [].
case: c.
move=>a; case: a.
by [].
by [].
by [].
case: c.
move=>a; case: a.
by [].
by [].
by [].
Qed.
```

Last updated: Jul 25 2024 at 16:02 UTC