Stream: math-comp users

Topic: Less verbose ssreflect proof


view this post on Zulip Julin Shaji (Oct 13 2023 at 15:25):

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?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 13 2023 at 15:31):

Here's my proposal:

view this post on Zulip Emilio Jesús Gallego Arias (Oct 13 2023 at 15:31):

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.

view this post on Zulip Ana de Almeida Borges (Oct 13 2023 at 15:36):

In general, by [] can be replaced with a move=> // somewhere before, or by prepending by to the previous tactic if it solved all goals.

view this post on Zulip Ana de Almeida Borges (Oct 13 2023 at 15:37):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 13 2023 at 15:37):

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.

view this post on Zulip Ana de Almeida Borges (Oct 13 2023 at 15:42):

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