Solve Proof with Circular Symmetry in Coq

Question

I am working on a proof using structural congruence, which is defined very similar to this example:

Require Import Nat.
Require Import Omega.

Inductive expr :=
  | Const : nat -> expr
  | Add : expr -> expr -> expr.


Reserved Notation "e1 === e2" (at level 80).
Inductive expr_congruence : expr -> expr -> Prop :=
  | Commutative : forall e1 e2, Add e1 e2 === Add e2 e1
  | Associative : forall e1 e2 e3, Add (Add e1 e2) e3 === Add e1 (Add e2 e3)
  | CongruenceReflexive : forall e, e === e
  | CongruenceSymmetric : forall e1 e2, e1 === e2 -> e2 === e1
  | CongruenceTransitive :
      forall e1 e2 e3, e1 === e2 -> e2 === e3 -> e1 === e3
  where "e1 === e2" := (expr_congruence e1 e2).

I run into problems when trying to define something of the form forall e1 e2, e1 === e2 -> P e1 -> P e2: I always end up with circular logic. As an example:

Inductive is_zero : expr -> Prop :=
  | ZConst : is_zero (Const 0)
  | ZAdd : forall e1 e2, is_zero e1 -> is_zero e2 -> is_zero (Add e1 e2).

Hint Constructors is_zero expr_congruence.

Lemma is_zero_over_congruence :
  forall e1 e2,
    e1 === e2 ->
    is_zero e1 ->
    is_zero e2.
Proof.
  induction 1; eauto; intros.

  Show 3.
(**
1 subgoal
e1, e2 : expr
H : e1 === e2
IHexpr_congruence : is_zero e1 -> is_zero e2
H0 : is_zero e2
**)

The only connection between e1 and e2 here is that they are congruent. Doing inversion or induction on them eventually leads back to the same case, which provides no extra information.

What is the proper way to handle induction when using structures with symmetry defined in this way?

Answer 1

At least in this minimal example, you just need to prove something stronger:

Lemma is_zero_over_congruence :
  forall e1 e2, e1 === e2 -> is_zero e1 <-> is_zero e2.
Proof.
  induction 1.
  - split; intros HI; inversion HI; eauto.
  - split; intros HI; inversion HI; [inversion H1 | inversion H2]; eauto.
  - reflexivity.
  - symmetry. auto.
  - rewrite IHexpr_congruence1, IHexpr_congruence2. reflexivity.
Qed.

so that you have available is_zero e1 <-> is_zero e2 as an inductive hypothesis when you need to prove is_zero e2 <-> is_zero e1.