avoiding type error

Hi,

I have a situation as follows:

  H : [(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p0);
       (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [B0], Var p)] = lpst
   ind2 : in_dersrec d2 d1

Did your posting get truncated?

Hi Jim,

Yes, obviously, see if this works better

I have a situation as follows:

H : [(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p0);
(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [B0], Var p)] = lpst
ind2 : in_dersrec d2 d1

(reposting for Jeremy)

Hi,

I have a situation as follows:

   H : [(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p0);
       (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [B0], Var p)] = lpst
   ind2 : in_dersrec d2 d1
   ============================
   in_dersrec d2 d1

However
exact ind2.
fails with the message

The term "ind2" has type
  "@in_dersrec (srseq (PropF V)) (@LJArules V) (@emptyT (srseq (PropF
V))) c1
     d2
     [(@fmlsext (PropF V) (Γ1 ++ @Imp V (@Var V p) B :: H2) Γ3
         [@Imp V (@Var V p0) B0], @Var V p0);
     (@fmlsext (PropF V) (Γ1 ++ @Imp V (@Var V p) B :: H2) Γ3 [B0], @Var
V p)]
     d1" while it is expected to have type
  "@in_dersrec (srseq (PropF V)) (@LJArules V) (@emptyT (srseq (PropF
V))) c1
     d2 lpst d1".

That is, the two types are equal (hypothesis H) but expressed differently

Question : where types T and T’ are equal, is (for example)
(x : T) = (x’ : T’) well-typed or not?

In this case, since type type of in_dersrec and d1 are as follows

in_dersrec
      : forall (X : Type) (rules : rlsT X) (prems : X -> Type) (concl : X),
        derrec rules prems concl ->
        forall concls : list X, dersrec rules prems concls -> Type
d1 : dersrec LJArules emptyT lpst

Now if types need to be identical rather than equal, then ind2 is
ill-typed, so should Coq allow this? If types don’t need to be identical
but somehow you have to remind Coq that they are equal, then how do you do
this?

I’ve tried
subst lpst.
rewrite H in ind2.
but both produce an error

Error: Illegal application:
The term "in_dersrec" of type ...
cannot be applied to the terms
    ...
  "d1" : "dersrec LJArules emptyT lpst"
The 7th term has type "dersrec LJArules emptyT lpst"
which should be coercible to
  "dersrec LJArules emptyT
     [(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p0);
     (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [B0], Var p)]".

Trying
destruct ind2.
inversion ind2.
elim ind2.
all produce similar errors, eg

Unable to unify "dersrec LJArules emptyT lpst" with
  "dersrec LJArules emptyT
     [(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p0);
     (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [B0], Var p)]".

Any help would be very much appreciated.

Thanks

Jeremy Dawson

Without seeing the whole development it is hard to tell, but conversion does unfold constants. Are you sure that everything is definitionnaly equivalent? Often some implicit are actually not.

I’m not sure what definitionnaly equivalent means - if it means that the equality H is obtained by defining lpst in that way - then, no, it is not. Sorry I don’t understand the sentence “Often some implicit are actually not.”

Cheers, Jeremy

The types don’t need to be identical — just definitionally/judgmentally equal: you can only reduce definitions or equalities like a := b, but not propositional equalities like a = b.

So, it’s indeed weird that ind2 typechecks, but things aren’t working. I don’t think anybody can debug this without access to the actual failing proof. We can speculate on a bunch of things that might be different (universes?), but it’s too hard to debug at a distance. OTOH, I’d be curious to see the full context at least.


Basically, Coq’s typechecker can’t use automatically equalities between types — it sounds stupid, but in short using those equalities automatically is impossible (if you want to look this up, we say that “Extensional Type Theory (ETT) has undecidable typechecking”).

Not if you only know H : T = T', you need a definitional equality between T and T' — above, do you have lpst := ... in the context?

FWIW, I had a brief look at the actual proof (if this is the same as the one @jeremydaw sent me), and I couldn’t figure it out immediately — and then I got busy with other stuff :confused: @jeremydaw , if the code can be made public, I think it would be very useful to post it somewhere on Github (thankfully the set-up was easy), and hopefully someone will beat me to figuring out what the issue is.

1 Like

The full context (possibly also with universes and whatever else enabled) might already help some? :slight_smile:

This is probably what you need: https://coq.inria.fr/distrib/current/refman/proofs/writing-proofs/rewriting.html#term-definitional-equality

Thanks very much for all the replies. Sorry for the late and brief
response, I have been travelling.

What I had sent @cpitclaudel was a tar file which is now (temporarily)
at http://users.cecs.anu.edu.au/~jeremy/tmp/type-error.tar
(I don’t think I should post it permanently somewhere public)

And the info with it is as follows:

it runs on Coq 8.11.0
(probably not on Coq 8.12, I’m told Add LoadPath causes a problem)

to compile the lot, do
make ljt/ljt_dnterm.vo
then the way I run it is cd ljt
coqtop -color no
Load ljt_dnterm.
then the lemma I can’t prove because of the problem starts at line 690,
with the commands showing what puzzles me starting from line 856

(also another thing that puzzled me at lines 882-3)

A bit more background to the error, in the light of replies (from
memory, I haven’t been able to go through it again just now), is

the equality H, which says that two things are equal (which should make
the types right) is
H : ffff (long) = lpst
It was got by
remember ffff’ as lpst.
(and this has the effect of changing the type of a term in the goal)
assert and prove ffff = ffff’
thereby deduce H

With the clues I’ve been given now I might be able to figure it out a
bit more, but obviously I’d also appreciate experts looking at it

Thanks,

Jeremy

Has this been solved already?

The problem is indeed with remember: once you have applied this tactic lpst is only provably equal to ffff (long), but the fact that it is its actual definition is lost. This makes types containing one and the other not convertible anymore. So even if you “subst” lpst, the pattern ffff (long) may re-appear later in the proof and you won’t have them convertible.

In other word: use “pose” instead and it should be ok. pose only introduce a “let” binding, so it does not lose track of convertibility.