The Coq mailing list

[Koper <Koper AT acn.waw.pl>]

I've just finished the formalization of the proof of well-foundedness 

of the higher-order recursive path ordering in Coq 8. Both the 

definition of the order and the proof of its well-foundedness are due 

to Jouannaud and Rubio and were presented in "The Higher-Order 

Recursive Path Ordering" in "Proceedings of the 14th annual IEEE 

Symposium on Logic in Computer Science (LICS'99)". I just miss one 

result concerning terms which I really cannot accomplish by myself and 

thus I'm asking for help for which I will be very grateful! 

I work with terms of simply typed lambda-calculus. I have an 

arbitrary set of base types and then simple types are build in an 

usual 

fashion. Also an arbitrary set of function symbols with types attached 

to them is present. I use de Bruijn indices so environment is simply a 

list of simple types. Then comes the definition of preterms (also 

called raw terms or pseudo terms in literature ), derivations and 

finally terms. I hope the attached Coq listing (which I tried to make 

as short as possible by aggregating only the definitions crucial for 

the problem; in the real development they are scattered across 

different modules) is self-explanatory. 

The problem, which I cannot overcome, is to show that derivations 

are 

unique; that is if we have terms that equal on environment, preterm 

and 

type components then they are equal (deriv_uniq). I guess the problem 

has to do with Coq's equality on dependent types which I don't know 

much about. From this it's easy (and I've done it) to conclude that 

typing is unique that is two terms with equal environments and 

preterms 

have equal types (typing_uniq). Finally the fact that two terms with 

equal environment and preterms are equal follows trivially (term_eq). 

Any comments, suggestions etc. welcome! 

Kind regards, 

Adam Koprowski 

 

----- 

Require Import List. 

Set Implicit Arguments. 

 

(* Base types; denoted as a, b, c, ... *) 

Parameter Stepper: Set. 

Implicit Types a b c : BaseType. 

(* Decidable equality on base types *) 

Parameter eq_BaseType_dec: forall a b, {a=b} + {a<>b}. 

(* Simple types: either basic types or arrow types A->B with A and B 

simple types. 

We denote them as A, B, C, ... *) 

Inductive SimpleType : Set := 

| BasicType(T: BaseType) 

| ArrowType(A B : SimpleType). 

Notation "x --> y" := (ArrowType x y) (at level 55, right 

associativity) : type_scope. 

Notation "# x " := (BasicType x) (at level 0) : type_scope. 

Implicit Types A B C : SimpleType. 

 

(* Function symbols, denoted as f, g, h, ... *) 

Parameter FunctionSymbol: Set. 

Implicit Types f g h : FunctionSymbol. 

(* Decidable qquality on function symbols *) 

Parameter eq_FunctionSymbol_dec: forall (f g: FunctionSymbol), {f=g} + 

{f<>g}. 

(* Types for function symbols *) 

Parameter f_type: FunctionSymbol -> SimpleType. 

 

(* We are using de Bruijn indices for bindings so environments are 

simply 

lists of simple types. *) 

Definition Env := list (option SimpleType). 

Definition EmptyEnv : Env := nil. 

Implicit Type x y : nat. 

Implicit Type E : Env. 

 

(* VarD E x A (denoted as: "E |= x := A") indicates that in 

environment 

E variable x has type A *) 

Definition VarD  E x A := nth_error E x = Some (Some A). 

Notation "E |= x := A" := (VarD E x A) (at level 60). 

(* VarUD E x (denoted as: "E |= x :!") indicates that in environment 

E variable x is undeclared *) 

Definition VarUD E x := nth_error E x = None / nth_error E x = Some 

None. 

Notation "E |= x :!" := (VarUD E x) (at level 60). 

 

(* 'decl A E' returns environment E with new declaration for A *) 

Definition decl A E := Some A::E. 

(* 'declDummy E' returns environment E with new dummy variable *) 

Definition declDummy E := None::E. 

 

(* Preterm represents the set of preterms *) 

Inductive Preterm : Set := 

| Var(x: nat) 

| Fun(f: FunctionSymbol) 

| Abs(A: SimpleType)(M: Preterm) 

| App(M N: Preterm). 

 

(* Some notation for preterms *) 

Implicit Type Pt : Preterm. 

Notation "^ f" := (Fun f) (at level 20). 

Notation "% x" := (Var x) (at level 20). 

Infix "@@" := App (at level 25, left associativity). 

Notation "s [ x ]" := (s @@ x) (at level 30). 

Notation "s [ x , y ]" := (s @@ x @@ y) (at level 30). 

Notation " A => M" := (Abs A M) (at level 35). 

 

(* Typing E Pt A represent the derivation showing that preterm Pt 

in environment E has type A *) 

Reserved Notation "E |- Pt := A" (at level 60). 

Inductive Typing : Env -> Preterm -> SimpleType -> Set := 

| TVar: forall E x A, 

(E |= x := A) -> 

(E |- %x := A) 

| TFun: forall E f, 

(E |- ^f := f_type f) 

| TAbs: forall E A B Pt, 

(decl A E |- Pt := B) -> 

(E |- A => Pt := A --> B) 

| TApp: forall E A B Pt0 Pt1, 

(E |- Pt0 := A --> B) -> 

(E |- Pt1 := A) -> 

(E |- Pt0 @@ Pt1 := B) 

where "E |- Pt := A" := (Typing E Pt A). 

 

(* Term consist of environment, preterm and type and derivation 

showing that this triple is well-formed *) 

Record Term : Set := buildT { 

env: Env; 

term: Preterm; 

type: SimpleType; 

typing: Typing env term type 

}. 

Implicit Types M N : Term. 

 

Theorem deriv_uniq: forall M N, 

env M = env N -> 

term M = term N -> 

type M = type N -> 

M = N. 

Proof. 

(* ??? *) 

Qed. 

 

Lemma typing_uniq: forall M N, 

env M = env N -> 

term M = term N -> 

type M = type N. 

Proof. 

(* easy *) 

Qed. 

 

Lemma term_eq: forall M N, 

env M = env N -> 

term M = term N -> 

M = N. 

Proof. 

(* easy with two above *) 

Qed.