The Coq mailing list

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

OK.  Here's my first coq coding problem.

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.

This is, however, plain to me from the type of the constructor makettt.

The use of e here reminds me of the inductive definition of equality.


How can I get around this?

-- hendrik

----------------------------

In case you're interested, here's the complete code I'm working with:


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

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
*)

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.

(* env needs an augmentation operation.
   So do element of (u : Id) (e u) for e in env.

   Actually, we want Prop instead of Set to be the value of hasType1,
   but they refuse to let us access the proof of a Prop when definint eval, 
later.
*)

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)).

(* Following doesn't work yet. *)

Fixpoint eval[x : exp; e : env; t : Set; 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

.

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 e (tx2->t2) en q2) (vvv x2 e 
t2 en r2)) 
  end
.