3
$\begingroup$

How do you prove commutativity and associativity of addition idiomatically using SSReflect?


I am trying to learn SSReflect so I have another tool in my belt for structuring a Coq proof.

I have seen lines in SSReflect tactic scripts that look like magic.

For example, this answer from Stack Overflow has the following proof:

From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
From Coq Require Import Nat Arith Lia.

Lemma L1: forall A B C, A -> (A -> B /\ C) -> C.
Proof.
by move=> A B C /[swap] /[apply] - [].
Qed.

I have tried stepping through the proof and I do not understand how it's working on a deep level. My hunch is that it's treating a goal of the form X -> Y -> Z -> W like a little sequent $X, Y, Z \vdash W$ and /[swap] and /[apply] are flipping pseudohypotheses around in the goal.

That seems kind of nice. I know there's more to the SSReflect story than just splitting the hypotheses into two groups at a UI level as a form of housekeeping, but that's what I've been able to glean so far from reading random examples.

Anyway, I tried to prove the Hello World theorems (commutativity and associativity of natural number addition) using SSReflect, but totally hit a wall.

I can prove them, but I'm basically just using move=> whatever as intros and by [] as easy or some other finishing tactic.

How do you prove the Hello World theorems idiomatically using SSReflect?

From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
From Coq Require Import Nat Arith Lia.


Lemma add_comm : forall a b, a + b = b + a.
Proof.
  move=> a b.
  induction a.
  { by []. }
  { simpl. rewrite IHa. by []. }
Qed.

Lemma add_assoc : forall a b c, (a + b) + c = a + (b + c).
Proof.
  move=> a b c.
  induction a.
  { by []. }
  { simpl. rewrite IHa. by []. }
Qed.
```
$\endgroup$

1 Answer 1

3
$\begingroup$

To understand ssreflect operations, step through them one operation at a time. In your first example, try the following sequence of partial proofs:

  1. move=> A B C.
  2. move=> A B C /[swap].
  3. move=> A B C /[swap] /[apply].
  4. move=> A B C /[swap] /[apply] - [].
  5. move=> A B C /[swap] /[apply] - [] //.

For your second example, I think an idiomatic ssreflect proof would be

Lemma add_comm : forall a b, a + b = b + a.
Proof.
  elim => ? //= /[swap] ? -> //.
Qed.

elim is the ssreflect way to do induction. The -> tactical performs an inline rewrite. The (roughly) equivalent non-ssreflect proof is

Lemma add_comm : forall a b, a + b = b + a.
Proof.
  induction a as [ | a IHa]; intro b; simpl; now rewrite -> ? IHa.
Qed.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.