The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Thanks Jim, I don't know enough about using this discourse system to 
troubleshoot, here it is, also to the coq-club mailing list

Cheers, 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

On 5/1/21 10:05 am, Jim Fehrle wrote:
> Ah, no.  It's still truncated.
>
> On Mon, Jan 4, 2021 at 3:03 PM Jeremy Dawson via Coq 
> <coq AT discoursemail.com <mailto:coq AT discoursemail.com>> wrote:
>
>     __
>     [jeremydaw]         jeremydaw <https://coq.discourse.group/u/jeremydaw>
>     January 4
>
>     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
>
>     ------------------------------------------------------------------------
>
>     Visit Topic
>     <https://coq.discourse.group/t/avoiding-type-error/1177/3> or reply
>     to this email to respond.
>
>     ------------------------------------------------------------------------
>
>
>             In Reply To
>
>     [jfehrle]   jfehrle <https://coq.discourse.group/u/jfehrle>
>     January 4
>
>     Did your posting get truncated?
>     ------------------------------------------------------------------------
>
>     Visit Topic
>     <https://coq.discourse.group/t/avoiding-type-error/1177/3> or reply
>     to this email to respond.
>
>     To unsubscribe from these emails, click here
>     
> <https://coq.discourse.group/email/unsubscribe/7fd52dd2c0f88303f5b787f3d388533936dca1aba6b160099e87a654b83ad616>.