coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] problem refine tactic with fix construction ---> bug in coq?

From: "Chris Dams" <chris.dams.nl AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] problem refine tactic with fix construction ---> bug in coq?
Date: Tue, 20 Jan 2009 18:30:34 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:mime-version:content-type :content-transfer-encoding:content-disposition; b=OoqbTWRD/nFYir+QExngIu6LKvAynxn2EATItYfTmxrW7Pjl6IrqfyVY9rffzOL5/T Rgf8svrHM3EH2+Al76ObMXJNh/SACgO8U0KcVUlUR1VNMLuO4BsZzKx2wL0N4m99xGcY tMZi7a8yQqUpXKzfgsXnKwFI5/KJ8xpzbCXe8=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear all,

I use coqide from coq 8.1pl1. In coqide I start the following proof

Inductive test1: Set
   := a: test1 | S1: test2 -> test1
with test2: Set
   := b: test2 | S2: test1 -> test2.

Definition test: test1 -> nat.
refine
   (fix g (t1: test1): nat := _
    with f (t2: test2): nat := _
    for g).

The result of this is

2 subgoals
g : test1 -> nat
f : test2 -> nat
t1 : test1
______________________________________(1/2)
nat

______________________________________(2/2)
nat

This is as I expected, but if I change the order of the two branches
of the fix construction as in

Definition test: test1 -> nat.
refine
   (fix f (t2: test2): nat := _
    with g (t1: test1): nat := _
    for g).

I get

2 subgoals
f : test1 -> nat
g : test1 -> nat
t2 : test1
______________________________________(1/2)
nat

______________________________________(2/2)
nat

Note that the type of f is not the same as given in the refine tactic.
Is this a bug in coq?

All the best,
Chris

[Coq-Club] problem refine tactic with fix construction ---> bug in coq?, Chris Dams