The Coq mailing list

[Florian Lorenzen <florian.lorenzen AT tu-berlin.de>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Dear all,

I have a very strange problem with the destruct tactic in Coq 8.3pl2.

I have the following proof context (I disabled printing of notations):

  Γ : ctx
  t0 : Tm
  e1 : Emscp
  H : Genrscp Γ (Emscp_cons t0 e1) Ty_nat
  t' : Tm
  H0 : Evr (Tm_scp (Emscp_cons t0 e1)) t'
  e10 : Emscp
  t : gdscp
  t1 : td
  Heqo : eq (tdof t0 empty) (Some t1)
  H2 : eq
       match
         gdscpof (open_scp O (cons (Tm_fvar (freshvar S.empty)) nil) e1)
           (cons (pair (freshvar S.empty) Ty_nat) empty)
       with
       | Some der2 =>
           Some
             (gdscp_cons t1 (freshvar S.empty) S.empty der2 empty
                (Emscp_cons t0 e1) Ty_nat)
       | None => None
       end (Some t)
  H1 : eq e10 (Emscp_cons t0 e1)
  H3 : eq (trans_scp t) t'
  ============================
   Typr Γ (trans_scp t) Ty_nat

Now, I'd like to perform a case analysis on the scrutinee in the match
expression but

destruct
  (gdscpof (open_scp O (cons (Tm_fvar (freshvar S.empty)) nil) e1)
    (cons (pair (freshvar S.empty) Ty_nat) empty)) in H2.

just brings an additional hypothesis

  ...
  g : gdscp
  ============================
   Typr Γ (trans_scp t) Ty_nat

with noting else changed. Looks like destruct does not find the
intended term.

I could track down the problem to the following error message:
When I issue the command in the context above

set (F:=(pair (freshvar S.empty) Ty_nat)) in H2.

Coq returns:

Error: The term "pair (freshvar S.empty) Ty_nat" does not occur in H2.

This is absolutely puzzling to me, since I can clearly see this term.
I am able to replace other term like "Tm_fvar (freshvar S.empty)" in
the matched expression but not the pair-term.

I have no clue what I am missing here. If additional information is
required to track down the problem, I'll be happy to provide it.

Any help is very much appreciated, thanks in advance,

best regards,

Florian

- -- 
Florian Lorenzen

Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik
Übersetzerbau und Programmiersprachen

Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin

Tel.:   +49 (30) 314-24618
E-Mail: 
florian.lorenzen AT tu-berlin.de
WWW:    http://www.user.tu-berlin.de/florenz/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAk9L/4IACgkQvjzICpVvX7ZtFQCdEUyEdFlyY57KiUuB6IWbgyaj
a2QAniwVGDbBor5sswVRoy+7l0yvq0ek
=0POl
-----END PGP SIGNATURE-----