The Coq mailing list

[Kazuhiko Sakaguchi <pi8027 AT gmail.com>]

Dear Coq users,

I found out a new proof technique about congruence tactic.

According to the Coq reference manual, congruence tactic can't solve equations
which need unfolding definitions.  But if hypothesis contains definitions as
quantified equations, congruence tactic can unfold definitions.
For example, commutativity and associativity of addition and multiplication of
natural numbers are proved by induction and congruence:

==========
Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

Lemma add0n n : 0 + n = n. Proof. reflexivity. Qed.
Lemma addSn n m : n.+1 + m = (n + m).+1. Proof. reflexivity. Qed.
Lemma addn0 n : n + 0 = n. Proof. elim: n; move: add0n addSn; congruence. Qed.
Lemma addnS n m : n + m.+1 = (n + m).+1.
  Proof. elim: n; move: add0n addSn; congruence. Qed.
Lemma addnC n m : n + m = m + n.
  Proof. elim: n; move: add0n addSn addn0 addnS; congruence. Qed.
Lemma addnA a b c : a + b + c = a + (b + c).
  Proof. elim: a; move: add0n addSn; congruence. Qed.
Lemma mul0n n : 0 * n = 0. Proof. reflexivity. Qed.
Lemma mulSn n m : n.+1 * m = m + n * m. Proof. reflexivity. Qed.
Lemma muln0 n : n * 0 = 0.
  Proof. elim n; move: add0n mul0n mulSn; congruence. Qed.
Lemma mulnS n m : n * m.+1 = n + n * m.
  Proof. elim: n; move: add0n addSn addnC addnA mul0n mulSn; congruence. Qed.
Lemma mulnC n m : n * m = m * n.
  Proof. elim: n; move: mul0n mulSn muln0 mulnS; congruence. Qed.
Lemma mulnDl a b c : (a + b) * c = a * c + b * c.
  Proof. elim: a; move: add0n addSn addnA mul0n mulSn; congruence. Qed.
Lemma mulnA a b c : a * b * c = a * (b * c).
  Proof. elim: a; move: mul0n mulSn mulnDl; congruence. Qed.
==========

This method may be incomplete, but practically useful. And I wish "congruence
with e_1, ..., e_n" tactic which means "congruence after adding e_1, ..., e_n 
to
hypothesis" is implemented in a future version of Coq.

Best regards,

Kazuhiko