The Coq mailing list

[Hendrik Boom <hendrik AT topoi.cam.org>]

> 
>   Dear Hendrik Boom,
>  
> > I was trying to prove that typed lambda-expressions have typed
> > functions as values by induction on the proof that the expressions are 
> > typed.
> > I append the complete code later, but first present a stripped-down 
> > version
> > of what I'm having trouble   with.
> > 
> > Hypothesis ccc : exp -> exp -> exp.
> > 
> > Inductive ttt : env -> exp -> Set -> Set :=
> >   | makettt : (e : env)(f : exp)(x : exp) (t : Set) (tx : Set)
> >     (ttt e f (tx->t))
> >       ->(ttt e x tx) -> (ttt e (call f x) t)
> > .
> > 
> > Fixpoint vvv[x : exp; e : env; t : Set; en : (u : Id) (e u); p : (ttt e x 
> > t)] : t
> > :=
> >   Cases p of
> >   | (makettt e2 f2 x2 t2 tx2 q2 r2) => ((vvv f2 e2 (tx2->t2) en q2) (vvv 
> > x2 e2 t2 en r2)) 
> >   end
> > .
> > 
> > This fails because there seems to be no way of telling it that the e2
> > in the pattern (makettt e2 f2 x2 t2 tx2 q2 r2) is necessarily the
> > same as the e in the type (ttt e x t) of p.
> 
>   You can tell this making explicit in "<...>" that the result of the
> definition by cases is dependent on the argument, as follows:
> 
>    Fixpoint vvv[x:exp; e:env; t:Set; p:(ttt e x t)]:t:=
>      <[e; x; t; p:(ttt e x t)]t>
>      Cases p of
>      | (makettt e2 f2 x2 t2 tx2 q2 r2) =>
>           ((vvv f2 e2 (tx2->t2) q2) (vvv x2 e2 tx2 r2)) 
>      end
>    .
> 
>  (I remove "en" useless in this definition)
> 
> 
> > Hypothesis inteq : nat -> nat -> bool.
> > (* TODO: find out what the *real* way is to test for equality of nat.
> >    It's probably in a library somewhere; if not, code my own
> > *)
> 
>   This is beq_nat in module EqNat. You may also reason by Cases on the
> theorem eq_nat_decide in EqNat which give you in addition the proofs
> of why it is equal or not.
> 
> 
>   Best regards,
>                                                   Hugo Herbelin
> 


Thanks for your reply, but I'm sorry to say that I'm still not out
of the woods.

As far as I understand from the manual, the <> notation serves to specify
the type returned by the cases construction.  Somehow your suggestion implies
that the bound variables inside the type inside the angle brackets
are somehow accessible inside the Cases clause.  Where is this documented?
Or is this a complete misunderstanding?

Your example works -- the simplified version with the "en" removed.
Unfortunately, it is now the "en" in the real case that is giving me problems.

Following your advice. I tried 

    Fixpoint eval[x : exp; e : env; t : Set; en : (u : Id) (e u); p : 
(hasType1 e x t)] : t
    :=
      <[e; x; t; p : (hasType1 e x t)]t>
      Cases p of
        (typedId e x t zzz) => (en x)
      | (iscall e2 f2 x2 t2 tx2 q2 r2) => ((eval f2 e2 (tx2->t2) en q2) (eval 
x2 e2 t2 en r2)) 
      | (isfn e x xt body bt q) =>
        [z : xt](eval body e bt ([i : Id](if (eqId i x) then z else (en i))) 
q)
      end
    
    .

(which ignores the en), and was told:

|   Error during interpretation of command:
|   Fixpoint eval[x : exp; e : env; t : Set; en : (u : Id) (e u); p : 
(hasType1 e x
|   t)] : t
|   :=
|     <[e; x; t; p : (hasType1 e x t)]t>
|     Cases p of
|       (typedId e x t zzz) => (en x)
|     | (iscall e2 f2 x2 t2 tx2 q2 r2) => ((eval f2 e2 (tx2->t2) en q2) (eval 
x2 e2
|   t2 en r2))
|     | (isfn e x xt body bt q) =>
|           [z : xt](eval body e bt ([i : Id](if (eqId i x) then z else (en 
i))) q)
|   Error: The term (eval f2 e2 tx2->t2 en q2 (eval x2 e2 t2 en r2)) is not 
well typed.
|    The risen type error on the result of expansion was:
|     Illegal application (Type Error): in environment
|     eval : (x:exp; e:env; t:Set)((u:Id)(e u))->(hasType1 e x t)->t
|     x : exp
|     e : env
|     t : Set
|     en : (u:Id)(e u)
|     p : (hasType1 e x t)
|     e2 : env
|     f2 : exp
|     x2 : exp
|     t2 : Set
|     tx2 : Set
|     q2 : (hasType1 e2 f2 tx2->t2)
|     r2 : (hasType1 e2 x2 tx2)
|     The term eval of type
|      (x:exp; e:env; t:Set)((u:Id)(e u))->(hasType1 e x t)->t
|     cannot be applied to the terms
|      f2 : exp
|      e2 : env
|      tx2->t2 : Set
|      en : (u:Id)(e u)
|      q2 : (hasType1 e2 f2 tx2->t2)
|    
|   Coq <
|       eval : (x:exp; e:env; t:Set)((u:Id)(e u))->(hasType1 e x t)->t
|   is being applied to args
|      f2 : exp
|      e2 : env
|      tx2->t2 : Set
|      en : (u:Id)(e u)
|      q2 : (hasType1 e2 f2 tx2->t2)

 Presumably q2 is the problem arg, because it stopped there and there
 are more args in the source code.

Let's analyse:
        formal  type    actual  type
        x       exp     f2      exp
        e       env     e2      env
        t       Set     tx2->t2 Set
        ?en?    (u:Id)(e u), which is (u:Id)(e2 u) after substituting
                        en      (u:Id)(e u)
                (hasType e x t), which is (hasType e2 f2 tx2->t2) after 
substituting
                        q2      (hasType1 e2 f2 tx2->t2)


So it is presumably not recognizing that (u:Id)(e2 u) is the same as (u:Id)(e 
u).

But this does not explain why it stopped only after gobbling yet another 
argument, but not all of them.


Still, let's try to introduce en into <[...]t>

    Fixpoint eval[x : exp; e : env; t : Set; en : (u : Id) (e u); p : 
(hasType1 e x t)] : t
    :=
      <[e; x; t; en : (u : Id) (e u); p : (hasType1 e x t)]t>
      Cases p of
        (typedId e x t zzz) => (en x)
      | (iscall e2 f2 x2 t2 tx2 q2 r2) => ((eval f2 e2 (tx2->t2) en q2) (eval 
x2 e2 t2 en r2)) 
      | (isfn e x xt body bt q) =>
        [z : xt](eval body e bt ([i : Id](if (eqId i x) then z else (en i))) 
q)
      end
    
    .


I get:
 
|   Coq <
|   Coq < Fixpoint eval[x : exp; e : env; t : Set; en : (u : Id) (e u); p : 
(hasType1 e x t)] : t
|   Coq < :=
|   Coq <   <[e; x; t; en : (u : Id) (e u); p : (hasType1 e x t)]t>
|   Coq <   Cases p of
|   Coq <     (typedId e x t zzz) => (en x)
|   Coq <   | (iscall e2 f2 x2 t2 tx2 q2 r2) => ((eval f2 e2 (tx2->t2) en q2) 
(eval x2 e2 t2 en r2))
|   Coq <   | (isfn e x xt body bt q) =>
|           [z : xt](eval body e bt ([i : Id](if (eqId i x) then z else (en 
i))) q)
|     end
|    
|   .
|   Coq < Coq < Coq < Coq < Error during interpretation of command:
|   Fixpoint eval[x : exp; e : env; t : Set; en : (u : Id) (e u); p : 
(hasType1 e x t)] : t
|   :=
|     <[e; x; t; en : (u : Id) (e u); p : (hasType1 e x t)]t>
|     Cases p of
|       (typedId e x t zzz) => (en x)
|     | (iscall e2 f2 x2 t2 tx2 q2 r2) => ((eval f2 e2 (tx2->t2) en q2) (eval 
x2 e2 t2 en r2))
|     | (isfn e x xt body bt q) =>
|           [z : xt](eval body e bt ([i : Id](if (eqId i x) then z else (en 
i))) q)
|     end
|    
|   .
|   Error: Illegal generalization: in environment
|    eval : (x:exp; e:env; t:Set)((u:Id)(e u))->(hasType1 e x t)->t
|    x : exp
|    e : env
|    t : Set
|    en : (u:Id)(e u)
|    p : (hasType1 e x t)
|    e : ?7
|    x : ?8
|    t : ?9
|    Cannot generalize Id over (e u)
|    which should be typed by Set, Prop or Type.
|    
|   Coq <                                                                 

Now as far as I can tell, (e u) *is* typed by Set, so maybe
it is still confused about e.

I try explicitly typing e in the <>:

    Fixpoint eval[x : exp; e : env; t : Set; en : (u : Id) (e u); p : 
(hasType1 e x t)] : t
    :=
      <[e : env; x; t; en : (u : Id) (e u); p : (hasType1 e x t)]t>
      Cases p of
        (typedId e x t zzz) => (en x)
      | (iscall e2 f2 x2 t2 tx2 q2 r2) => ((eval f2 e2 (tx2->t2) en q2) (eval 
x2 e2 t2 en r2))
      | (isfn e x xt body bt q) =>
            [z : xt](eval body e bt ([i : Id](if (eqId i x) then z else (en 
i))) q)
      end
     
    .


Now I get:

 
|   Coq < Fixpoint eval[x : exp; e : env; t : Set; en : (u : Id) (e u); p : 
(hasType1 e x t)] : t
|   Coq < :=
|     <[e : env; x; t; en : (u : Id) (e u); p : (hasType1 e x t)]t>
|     Cases p of
|       (typedId e x t zzz) => (en x)
|     | (iscall e2 f2 x2 t2 tx2 q2 r2) => ((eval f2 e2 (tx2->t2) en q2) (eval 
x2 e2 t2 en r2))
|     | (isfn eCoq < Coq < Coq < Coq <  x xt body bt q) =>
|           [z : xt](eval body e bt ([i : Id](if (eqId i x) then z else (en 
i))) q)
|     end
|    
|   .
|    
|   Coq < Coq < Coq < Coq < Coq < Error during interpretation of command:
|   Fixpoint eval[x : exp; e : env; t : Set; en : (u : Id) (e u); p : 
(hasType1 e x t)] : t
|   :=
|     <[e : env; x; t; en : (u : Id) (e u); p : (hasType1 e x t)]t>
|     Cases p of
|       (typedId e x t zzz) => (en x)
|     | (iscall e2 f2 x2 t2 tx2 q2 r2) => ((eval f2 e2 (tx2->t2) en q2) (eval 
x2 e2 t2 en r2))
|     | (isfn e x xt body bt q) =>
|           [z : xt](eval body e bt ([i : Id](if (eqId i x) then z else (en 
i))) q)
|     end
|    
|   .
|   Error: The elimination predicate [e0:env;
|                                     x0:?12;
|                                     t:?13;
|                                     _:((u:Id)(e0 u));
|                                     _:(hasType1 e0 x0 t)]t
|    should be of arity 3 (for non dependent case)  or 4 (for dependent case).
|    
|   Coq < Coq <                                             
|   


I no longer have any idea what the error messages mean.

-- hendrik.


I append the code leading up to eht fixpoint eval:



Inductive Id : Set := makeid : nat -> Id .

Hypothesis inteq : nat -> nat -> bool.

Definition eqId : Id -> Id -> bool :=
  [i : Id][j : Id]
    Cases i of
      (makeid ian) =>
        Cases j of
          (makeid jn) => (inteq ian jn)
        end
    end.

Inductive exp : Set :=
  | id : Id -> exp
  | call : exp -> exp -> exp
  | fn : Id -> exp -> exp.

Definition env : Type := (id : Id)Set.

Inductive hasType1 : env -> exp -> Set -> Set :=
  | typedId : (e : env) (x : Id) (t : Set) (eqT Set (e x) t) -> (hasType1 e 
(id x) t)
  | iscall : (e : env)(f : exp)(x : exp) (t : Set) (tx : Set)
        (hasType1 e f (tx->t))
      ->(hasType1 e x tx) -> (hasType1 e (call f x) t)
  | isfn : (e:env)(x : Id)(xt : Set)(body : exp)(bt : Set)
        (hasType1 ([i : Id] (if (eqId i x) then xt else (e i))) body bt)
      ->(hasType1 e (fn x body) (xt->bt)).