The Coq mailing list

[Li-Yang Tan <lytan AT artsci.wustl.edu>]

Hello,

I am working on formalizing Peter Andrews' higher-order logic q0 in Coq. 
 I have defined the subterm relationship inductively as follows:

Inductive subtrm : forall a b, Trm a -> Trm b -> Pos -> Prop :=
  subtrm_empty : forall a A, subtrm a a A A empty
| subtrm_apply0 :
        forall a b t M N T p,
          subtrm t (Fun a b) T M p ->
          subtrm _ _ T (Apply M N) (P0 p)
| subtrm_apply1 :
        forall a b t M N T p,
          subtrm t b T N p ->
          subtrm _ a T (Apply M N) (P1 p)
| subtrm_lambda0 :
        forall a b t x M T p,
          subtrm t a T (_v x) p ->
          subtrm t (Fun b a) T (Lambda x M) (P0 p)
| subtrm_lambda1 :
        forall a b t x M T p,
          subtrm t b T M p ->
          subtrm t (Fun b a) T (Lambda x M) (P1 p).
Implicit Arguments subtrm.


I would like to prove falsity from the hypothesis that a lambda term is 
a subterm of an apply term at the empty position.  That is, I have the 
following subgoal:

s : q0_type
t : q0_type
M : Trm (Fun s t)
N : Trm t
x0 : q0_type
x1 : q0_type
x2 : Var x0
x3 : Trm x1

H7 : subterm (Lambda x2 x3) (Apply M N) empty
------------------------------------------------(1/2)
Logic.False

When I use the inversion tactic on H7, I get the following:

a : q0_type
A : Trm (Fun x1 x0)
H8 : a = Fun x1 x0
H10 : Fun x1 x0 = s
H12 : existS (fun x : q0_type => Trm x) (Fun x1 x0) A =
       existS (fun x : q0_type => Trm x) (Fun x1 x0) (Lambda x2 x3)
H13 : Fun x1 x0 = s
H14 : existS (fun x : q0_type => Trm x) (Fun x1 x0) A =
       existS (fun x : q0_type => Trm x) (Fun x1 x0) (Apply M N)
-------------------------------------------------------------------(1/2)
Logic.False

I am currently clueless as to how to proceed from here.  In particular, 
 it would be helpful if I knew what the "existS" construct means and 
how I can make use of the hypotheses invoving it.  I have looked in 
Coq'Art but cannot seem to find a answer to this question.

Any help or suggestion would be greatly appreciated.

Thanks in advance,
Li-Yang Tan