The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

Hi,

while playing with Coq I got an anomaly and problems with let-in.
I worked around them by using fst and snd. But the questions remains:

1. How to get rid of let-in's in proof?
2. What's the reason for the anomaly? Is it a bug?

Here is the simplified code:
--- begin ---
Section common.

Variable A B:Set.
Variable EqA : A->A->Prop.
Variable EqB : B->B->Prop.
Let sym_law (X:Set) (r:X->X->Prop)
:= forall (x1 x2:X),
   r x1 x2 -> r x2 x1.
Hypothesis sym_a : sym_law A EqA.
Hypothesis sym_b : sym_law B EqB.

Let T := prod A B.

Let EqT (t1 t2:T)
:= match t1, t2 with
   (a1,b1), (a2,b2) => EqA a1 a2 /\ EqB b1 b2
   end.

Section let_intro.

Lemma sym_t : sym_law T EqT.
Proof.
   unfold sym_law, EqT.
   intros x1 x2 Hx1x2.
   intros. (* Nothing introduced! Are the let-in's the reason? *)
   Abort.

End let_intro.

Section anomaly_type_of.

Lemma sym_t : sym_law T EqT.
Proof.
refine(
 fun (x1 x2:T) (H:EqT x1 x2) =>
   match x1, x2, H with
   (a1,b1), (a2,b2), (conj eq_as eq_bs) =>
      let eq_as' := (sym_a a1 a2 eq_as) in
      let eq_bs' := (sym_b b1 b2 eq_bs) in
      _
   end
   ).
   (* line 34, characters 0-212
   Anomaly: type_of: Bad recursive type. Please report. *)

End anomaly_type_of.

End common.

--- end   ---

Regards,
-- 
Stefan Karrmann

You can't fall off the floor.