The Coq mailing list

[brandon_m_moore AT yahoo.com]

I'm trying to use setoid rewriting over impl to simplify hypotheses.
It usually works fine, but if the conclusion of the implication is
an equality or similarly defined inductive type, there are problems.

rewriting in * |- always seems to fail, by encountering a fatal error
when deciding whether the rule can be used to rewrite in a type
like Z in a hypothesis like (p : Z).

Require Import Setoid.
Require Import Program.
Require Import ZArith.

Inductive Breaks (a : Z) : Z -> Prop :=
  B : Breaks a a.

Parameter breaks : forall a b, impl (Zeq_bool a b = true) (Breaks a b).

Lemma examples p q : Zeq_bool p q = true -> True.
intro H.
(*
rewrite breaks in * |- .

Error: Too complex unification problem: cannot find a solution for both P
and a.
 *)
(*
rewrite breaks in p.

Error: Too complex unification problem: cannot find a solution for both P
and a.
*)
rewrite breaks in H. constructor. Qed.

Inductive Works (a : Z) : Z -> Prop :=
  W b : Works a b.

Parameter works : forall a b,  impl (Zeq_bool a b = true) (Works a b).

Lemma test p q : Zeq_bool p q = true -> True.
intro H. rewrite works in * |- . auto.
Qed.