The Coq mailing list

[Andrew Kennedy <akenn AT microsoft.com>]

Hello

 

I’ve encountered a problem with setoid rewriting where the search for the relation doesn’t succeed “up to” some simple reductions. I’m not sure if this is expected behaviour, but it’s certainly a bit frustrating. Here’s my example, boiled down to something small.

 

Inductive Tm (env: nat) : nat -> Type :=

  C : forall t, Tm env t.

 

Definition globEnv := 5.

 

Definition tmEq (env: nat) (t: nat) (M1 M2: Tm (env + globEnv) t) :=

  match M1, M2 with C _, C _ => True end.

 

Global Instance ctxtEq_Reflexive (env t: nat) :

  @Reflexive (@Tm _ _) (@tmEq env t).

Proof. intros x. destruct x. simpl. auto. Qed.

 

(* This works fine *)

Lemma REFLTEST (t: nat) (M: Tm (0+globEnv) t) : (@tmEq 0 t M M).

Proof. setoid_reflexivity. Qed.

 

(* This fails with

Error: Tactic failure: The relation tmEq is not a declared reflexive relation.

Maybe you need to require the Setoid library.

*)

Lemma REFLTEST2 (t: nat) (M: Tm globEnv t) : (@tmEq 0 t M M).

Proof. setoid_reflexivity. Qed.

 

 

In essence, I have a “strongly-typed syntax”, with terms parameterized on an environment and a type, here, for simplicity, just nats. Then I define a relation “tmEq”, add an instance of Reflexive, and attempt to prove a trivial equivalence using setoid_reflexivity. But note the nat-computation inside the definition of tmEq. I would expect both REFLTEST and REFLTEST2 to succeed, as they differ only by a simple reduction, but REFLTEST2 fails.

 

Any ideas or pointers for help would be much appreciated. Although I have a workaround (the first lemma), I spent a long time tracking it down and I suspect the same thing might happen again in another context. I’m using Coq 8.3.

 

Cheers

Andrew.