Coq: Use equality of types for type checking a term in a definition

Question

I have a question regarding type checking definitions in Coq. I ran into a situation where I have two terms of type t1 and t2, where I know that t1 and t2 are equal (t1 = t2) from the definition. However, I cannot use those two terms together since the types are not considered equal by the type checker. I tried to isolate a minimum example modeling the situation (yeah I know that's a stupid property, but I just want it to get type checked ;) ):

Require Import Coq.Lists.List.

Lemma myLemma :
  forall t1 t2 : Type,
    forall (l1 : list t1) (l2 : list t2),
      t1 = t2 ->
        l1 = l2.

Just assume that I cannot write (l2 : list t1) directly instead, since I get it from another definition.

I tried using Program because I hoped that I could somehow defer the task to prove that the types match, but that did not help (got the same type checking errors).

---

If the example above is not sufficient for making the problem clear, here's an excerpt from my actual problem:

Definition taclet_sound_new (t : taclet) :=
  forall K st seSt, let S := (sig K) in
    [(K, st)] |= (pathC seSt) ->
      (forall K', let S' := (sig K') in
        S' = (newSig t S) ->
          exists (seSt' : (@sestatesc (newSig t S))),
            List.In seSt' (apply t S seSt) ->
              [(K', st)] |= (conv S' (pathC seSt'))).

The system complains that The term "pathC seSt'" has type "@pathCond (newSig t S)" while it is expected to have type "@pathCond S'".; however, from the premise S' = (newSig t S) I would expect that it somehow should be possible to get that definition type checked.

(Remark: conv is a trivial definition which I only added for improving Coq's output -- Definition conv (S : signature) (pc : (@pathCond S)) : list (@formulas S) := pc. -- without that, it says The term "pathC seSt'" has type "pathCond" while it is expected to have type "list formulas". which hid the actual problem.)

For completeness: The record taclet is defined as

Record taclet : Type := {
    defined (prog : P) : Prop;
    newSig (S1 : signature) : signature ;
    apply : forall (S1 : signature),
              (@sestatesc S1) -> list (@sestatesc (newSig S1)) ;
}.

So there is that newSig term in there. Therefore, the alternative definition

Definition taclet_sound_new (t : taclet) :=
  forall K st seSt, let S := (sig K) in
    [(K, st)] |= (pathC seSt) ->
      (forall K', let S' := (sig K') in
          exists (seSt' : (@sestatesc S')),
            S' = (newSig t S) ->
              List.In seSt' (apply t S seSt) ->
                [(K', st)] |= (pathC seSt')).

Also does not type check, with the similar error The term "apply t S seSt" has type "list (sestatesc P (newSig t S))" while it is expected to have type "list (sestatesc P S')". which, again, should be clear from the premise.

I would be very happy if anybody could help me out. That type checking mechanism of Coq is sometimes a little inconvenient... ;)

Thanks in advance!

---

/edit (2018-09-27): Although I gave myself an answer below that appeases the type checker, I still run into a lot of problems when trying to solve my problems around some theorems and definitions in the area of predicate logic. For instance, I totally fail to define a satisfying version of a conservativity theorem (if a formula is valid in a structure, it's also valid in all extensions) due to type checking, and even if a add a crazy constraint (the extension shares the same signature, so it's not really an extension) and add a (working) cast, I cannot prove it!

This time, I thought I give a complete example. I isolated the problem and put it into a single file "firstorder.v" as a GitHub Gist (https://gist.github.com/rindPHI/9c55346965418bd5db26bfa8404aa7fe). There are comments in the document explaining the challenges I discovered for myself. If anybody finds an answer to one or two of the "main challenges" in there, I'd be really happy to know about them (and would accept this as an answer to the question here). Thanks again! I hope that a solution to those problems not only helps me, but also others out there that are getting desperate due to dependent problems ;)

Answer 1

Thanks to the comment of Anton, I managed to resolve the issue in a way. This answer to the first question cited by Anton made me think about writing a cast function (I also tried to use the other alternative, JMeq, but it lead me nowhere -- probably I don't really understand it). I thought I'd share the solution, in case it helps somebody.

First, I wrote the following cast function and used it via two wrappers (which I won't post since they're not generally interesting:

Definition simple_cast {T1 T2 : Type} (H : T1 = T2) (x : T1) : T2 :=
  eq_rect T1 (fun T3 : Type => T3) x T2 H.

(Remark: I did not directly come up with the eq_rect term, for that I'm not enough of a pro user; however, it's possible to do the following in Coq, which I find quite interesting: Definition simple_cast {T1 T2 : Type} (H : T1 = T2) (x : T1) : T2. rewrite -> H in x. assumption. Defined. If you then Print simple_cast, you get a term that you can simplify a bit and directly post into the definition to make it more explicit. Constructing the term that way is significantly easier since you can work with simple tactics).

Next, I came up with the following definition which spared me the wrappers:

Definition cast {T : Type} {T1 T2 : T} (H : T1 = T2) (f : T -> Type) (x : f T1) :=
  eq_rect T1 (fun T3 : T => f T3) x T2 H.

Regarding the simple list example, the following code type checks:

Lemma myLemma :
  forall t1 t2 : Type,
    forall (l1 : list t1) (l2 : list t2),
      forall (H : t2 = t1),
        l1 = cast H (list) l2.

My actual code snippet also type checks:

  Definition taclet_sound_new (t : taclet) :=
    forall K st seSt, let S := (sig K) in
      [(K, st)] |= (pathC seSt) ->
        (forall K', let S' := (sig K') in
           forall (H : (newSig t S) = S'),
              exists (seSt' : (@sestatesc (newSig t S))),
                  List.In seSt' (apply t S seSt) ->
                    [(K', st)] |= (cast H (@pathCond) (pathC seSt'))).

Finally, I can cast expressions in Coq (given that there's named evidence that the cast is OK -- I can live with that)!

/edit: I now found a library for such casts: The Heq library. With that, myLemma looks like

Lemma myLemma :
  forall t1 t2 : Type,
    forall (l1 : list t1) (l2 : list t2),
      forall (H : t2 = t1),
        l1 = << list # H >> l2.

so you don't have to write your own cast function.

Unfortunately, I couldn't really eliminate the casts in proofs (regardless of whether I use my own cast or the one of Heq); it seems that you need to be a really experienced dependent types hacker to do so. Or my lemmas are wrong, which I don't think however. For those of you who really want to get into the topic, there's a chapter on equalities in Adam Chlipala's great CPDT book; in my case, I'll personally just "admit" some proofs simplifying those expressions and build upon that. At least it type checks...