Library Int_typ


Require
Import
Eqdep_dec
.
Require
Omega
.
Require
Export
Class
.

  
Inductive
Int_K
 :
Type
:=
    |
iK
 :
forall
s
,
Can
s
->
Int_K
    |
iT
 :
Int_K
.

  
Definition
intP
 :=
nat
 ->
Int_K
.

  
Definition
nil_intP
 :
intP
 :=
fun
_
=>
iT
.

  
Definition
class_of_ik
ik
:=
    
match
ik
with

    |
iK
s
_
=>
Knd
s

    |
iT
 =>
Typ
PROP

    
end
.

  
Definition
def_ik
cl
:=
    
match
cl
with

      
Knd
s
=>
iK
s
(
default_can
s
)
    |
_
=>
iT

    
end
.

  
Definition
cls_of_int
 (
ip
:
intP
) :
cls
 :=
fun
i
=>
class_of_ik
 (
ip
i
).

  
Inductive
ik_eq_can
 :
Int_K
 ->
Int_K
 ->
Prop
:=
    |
eqic_K
 :
        
forall
s
(
X
Y
:
Can
s
),
eq_can
_
X
Y
->
ik_eq_can
 (
iK
s
X
) (
iK
s
Y
)
    |
eqic_T
 :
ik_eq_can
iT
iT
.

  
Hint
Constructors
ik_eq_can
:
coc
.

  
Lemma
ik_eq_can_sym
 :
forall
i1
i2
,
ik_eq_can
i1
i2
->
ik_eq_can
i2
i1
.
Proof
.
destruct
1;
constructor
;
apply
eq_can_sym
;
trivial
.
Qed
.

  
Definition
int_eq_can
 (
ip1
ip2
:
intP
) :
Prop
:=
    
forall
i
,
ik_eq_can
 (
ip1
i
) (
ip2
i
).

  
Hint
Unfold
int_eq_can
 :
coc
.

  
Lemma
int_eq_can_right
 :
    
forall
ip1
ip2
,
int_eq_can
ip1
ip2
->
int_eq_can
ip2
ip2
.
Proof
.
unfold
int_eq_can
;
intros
.
generalize
(
H
i
);
intro
.
destruct
H0
;
trivial
with
coc
.
constructor
.
prolog
[
eq_can_right
] 2.
Qed
.

  
Lemma
tail_int_eq_can
 :
forall
i1
i2
ip1
ip2
,
     
int_eq_can
 (
cons_map
i1
ip1
) (
cons_map
i2
ip2
) ->
     
int_eq_can
ip1
ip2
.
Proof
.
unfold
int_eq_can
;
intros
;
exact
(
H
(
S
i
)).
Qed
.

  
Lemma
cons_int_eq_can
 :
forall
i1
i2
ip1
ip2
,
     
ik_eq_can
i1
i2
->
     
int_eq_can
ip1
ip2
->
     
int_eq_can
 (
cons_map
i1
ip1
) (
cons_map
i2
ip2
).
Proof
.
unfold
int_eq_can
.
destruct
i
;
simpl
;
auto
with
coc
.
Qed
.

  
Lemma
del_int_eq_can
 :
forall
ip1
ip2
n
k
,
    
int_eq_can
ip1
ip2
->
int_eq_can
 (
del_map
n
k
ip1
) (
del_map
n
k
ip2
).
Proof
.
red
;
intros
.
unfold
del_map
.
case
(
le_gt_dec
k
i
);
auto
with
coc
.
Qed
.

  
Lemma
ins_int_eq_can
 :
forall
i1
i2
ip1
ip2
k
,
    
int_eq_can
ip1
ip2
->
    
ik_eq_can
i1
i2
->
    
int_eq_can
 (
ins_map
k
i1
ip1
) (
ins_map
k
i2
ip2
).
Proof
.
red
;
intros
.
unfold
ins_map
.
case
(
lt_eq_lt_dec
k
i
);
auto
with
coc
.
destruct
s
;
auto
with
coc
.
Qed
.

  
Lemma
ins_int_eq_can_inv
 :
forall
k
i1
i2
ip1
ip2
,
     
int_eq_can
 (
ins_map
k
i1
ip1
) (
ins_map
k
i2
ip2
) ->
     
int_eq_can
ip1
ip2
.
Proof
.
red
;
intros
.
generalize
(
H
i
) (
H
(
S
i
)).
unfold
ins_map
.
generalize
(
lt_eq_lt_dec
k
i
);
intros
[[
cmp
|cmp]|cmp];
auto
.
generalize
(
lt_eq_lt_dec
k
(
S
i
));
intros
[[
cmp2
|cmp2]|cmp2];
 
try
(
apply
False_ind
;
omega
);
auto
.
generalize
(
lt_eq_lt_dec
k
(
S
i
));
intros
[[
cmp2
|cmp2]|cmp2];
 
try
(
apply
False_ind
;
omega
);
auto
.
Qed
.

Lemma
int_eq_can_cons_del
:
forall
i
i'
ip
ip'
n
k
,
 
ik_eq_can
i
i'
->
 
int_eq_can
ip
(
del_map
n
k
ip'
) ->
 
int_eq_can
 (
cons_map
i
ip
) (
del_map
n
(
S
k
) (
cons_map
i'
ip'
)).
Proof
.
red
in
|- *;
intros
.
 
rewrite
del_cons_map
.
generalize
i0
.
apply
cons_int_eq_can
;
trivial
.
Qed
.

Lemma
int_eq_can_cons_ins
:
forall
i
i'
j
ip
ip'
k
,
 
ik_eq_can
i
i'
->
 
int_eq_can
ip
(
ins_map
k
j
ip'
) ->
 
int_eq_can
 (
cons_map
i
ip
) (
ins_map
 (
S
k
)
j
(
cons_map
i'
ip'
)).
Proof
.
red
in
|- *;
intros
.
 
rewrite
ins_cons_map
.
generalize
i0
.
apply
cons_int_eq_can
;
trivial
.
Qed
.

  
Lemma
int_eq_can_class
 :
    
forall
ip
ip'
,
    
int_eq_can
ip
ip'
->
    
eq_map
 (
cls_of_int
ip
) (
cls_of_int
ip'
).
Proof
.
red
;
unfold
int_eq_can
,
cls_of_int
in
|- *;
intros
.
elim
H
with
i
;
reflexivity
.
Qed
.

  
Lemma
int_eq_can_cons_class
 :
    
forall
i
ip
ip'
,
    
eq_map
 (
cons_map
 (
class_of_ik
i
) (
cls_of_int
ip
))
ip'
->
    
eq_map
 (
cls_of_int
 (
cons_map
i
ip
))
ip'
.
Proof
.
intros
;
apply
trans_eq_map
with
(2:=H).
red
;
unfold
cls_of_int
in
|- *;
destruct
i0
;
simpl
in
|- *;
auto
with
coc
.
Qed
.

  
Hint
Resolve

    
cons_int_eq_can
ins_int_eq_can
del_int_eq_can

    
int_eq_can_cons_del
int_eq_can_cons_ins

    
int_eq_can_class
int_eq_can_cons_class
 :
coc
.

  
Inductive
can_interp
 :
Int_K
 ->
Prop
:=
    |
ca_K
 :
forall
s
C
,
is_can
_
C
->
can_interp
 (
iK
s
C
)
    |
ca_T
 :
can_interp
iT
.

  
Hint
Resolve
ca_K
ca_T
:
coc
.

  
Lemma
def_ik_can
 :
forall
cl
,
can_interp
 (
def_ik
cl
).
Proof
.
unfold
def_ik
in
|- *;
destruct
cl
;
auto
with
coc
.
Qed
.

  
Hint
Resolve
def_ik_can
 :
coc
.

  
Definition
can_adapt
 (
ip
:
intP
) :
Prop
:=
forall
i
,
can_interp
 (
ip
i
).

  
Hint
Unfold
can_adapt
:
coc
.

  
Lemma
cons_can_adapt
 :
    
forall
i
ip
,
can_interp
i
->
can_adapt
ip
->
can_adapt
 (
cons_map
i
ip
).
Proof
.
unfold
can_adapt
.
destruct
i0
;
simpl
;
auto
with
coc
.
Qed
.


  
Lemma
adapt_int_eq_can
 :
forall
ip
,
can_adapt
ip
->
int_eq_can
ip
ip
.
Proof
.
unfold
can_adapt
,
int_eq_can
.
intros
.
elim
(
H
i
);
auto
10
with
coc
.
Qed
.

  
Hint
Resolve
cons_can_adapt
adapt_int_eq_can
:
coc
.

  
Definition
coerce_CR
 (
s
:
skel
) (
i
:
Int_K
) :
Can
s
:=
    
match
i
with

    |
iK
si
Ci
=>
        
match
EQ_skel
si
s
with

        |
left
y
=>
            
match
y
in
(
_
=s)
return
(
Can
s
)
with

            |
refl_equal
 =>
Ci

            
end

        |
right
_
=>
default_can
s

        
end

    |
_
=>
default_can
s

    
end
.

  
Lemma
coerce_refl
 :
forall
s
C
,
coerce_CR
s
(
iK
s
C
) =
C
.
Proof
.
intros
.
unfold
coerce_CR
.
elim
(
EQ_skel
s
s
);
intros
.
elim
a
using
K_dec
;
trivial
.
intros
.
elim
(
EQ_skel
x
y
);
auto
.
elim
b
;
trivial
.
Qed
.

  
Lemma
eq_can_coerce
:
   
forall
s
i1
i2
,
   
ik_eq_can
i1
i2
->
eq_can
_
(
coerce_CR
s
i1
) (
coerce_CR
s
i2
).
Proof
.
destruct
1;
simpl
;
auto
with
coc
.
elim
(
EQ_skel
s0
s
);
simpl
;
auto
with
coc
.
intro
a
;
case
a
;
trivial
.
Qed
.
  
Hint
Resolve
eq_can_coerce
 :
coc
.

  
Lemma
is_can_coerce
:
forall
i
s
,
can_interp
i
->
is_can
s
(
coerce_CR
s
i
).
destruct
1;
simpl
;
intros
;
auto
with
coc
.
elim
(
EQ_skel
s0
s
);
auto
with
coc
.
intro
a
;
case
a
;
auto
with
coc
.
Qed
.
  
Hint
Resolve
is_can_coerce
 :
coc
.

  
Lemma
ik_proj_right
 :
forall
s
X
Y
,
    
existT
 (
fun
s
=>
Can
s
)
s
X
=
existT
 (
fun
s
=>
Can
s
)
s
Y
->
X
=Y.
Proof
.
intros
.
set
(
ex2ik
:=
fun
(
e
:sigT(fun
s
=>
Can
s
)) =>
       
let
(
s'
,C) :=
e
in
coerce_CR
s
(
iK
s'
C
)).
rewrite
<- (
coerce_refl
s
X
);
rewrite
<- (
coerce_refl
s
Y
).
change

 (
ex2ik
(
existT
 (
fun
s
=>
Can
s
)
s
X
) =ex2
ik
(
existT
 (
fun
s
=>
Can
s
)
s
Y
)).
rewrite
H
;
trivial
.
Qed
.

  
Lemma
ik_eq_can_trans
 :
forall
i1
i2
i3
,
    
ik_eq_can
i1
i2
->
ik_eq_can
i2
i3
->
ik_eq_can
i1
i3
.
destruct
1;
intros
.
inversion
H0
.
constructor
.
apply
eq_can_trans
with
Y
;
trivial
.
rewrite
<-
ik_proj_right
with
(1:=H3);
trivial
.
trivial
.
Qed
.



 
Definition
ik_app
i1
i2
:=
    
match
i1
,
i2
with

      
iK
s
F
,
iK
_
_
=>
        
match
s
return
Can
s
->
Int_K
with

          
PROD
s1
s2
=>
fun
F
=>
iK
s2
(
F
(
coerce_CR
s1
i2
))
        |
_
=>
fun
_
=>
i1

       
end
F

    |
_
,
_
=>
i1

    
end
.

  
Lemma
ik_app_ext
:
    
forall
U1
U2
V1
V2
,
    
ik_eq_can
U1
U2
->
    
ik_eq_can
V1
V2
->
    
ik_eq_can
 (
ik_app
U1
V1
) (
ik_app
U2
V2
).
Proof
.
intros
.
unfold
ik_app
in
|- *.
elim
H
;
intros
;
auto
with
coc
.
elim
H0
;
intros
;
auto
with
coc
.
destruct
s
;
intros
;
auto
with
coc
.
simpl
in
H1
;
auto
with
coc
.
Qed
.

  
Lemma
ik_app_can
:
    
forall
U
V
,
can_interp
U
->
can_interp
V
->
can_interp
 (
ik_app
U
V
).
Proof
.
destruct
1;
simpl
in
|- *;
auto
with
coc
.
destruct
1;
auto
with
coc
.
destruct
s
;
auto
with
coc
.
simpl
in
H
.
destruct
H
;
auto
with
coc
.
Qed
.


  
Definition
ik_lam
cl1
cl2
F
:=
    
match
cl2
,
cl1
with

    |
Typ
s2
,
Knd
s1
=>
       
iK
 (
PROD
s1
s2
) (
fun
C
=>
coerce_CR
s2
(
F
(
iK
_
C
)))
    |
Typ
_
,
Typ
PROP
 =>
F
iT

    |
_
,
_
=>
iT

    
end
.

  
Definition
ik_eq_fun
cl
F1
F2
:=
    
forall
i1
i2
,
    
ik_eq_can
i1
i2
->
class_of_ik
i1
=
cl
->
ik_eq_can
 (
F1
i1
) (
F2
i2
).

  
Hint
Unfold
ik_eq_fun
 :
coc
.

  
Lemma
ik_lam_ext
:
    
forall
clA1
clA2
clM1
clM2
F1
F2
,
    
clA1
=
clA2
->
    (
clA1
=
clA2
->
clM1
=
clM2
) ->
    
ik_eq_fun
clA1
F1
F2
->
    
ik_eq_can
 (
ik_lam
clA1
clM1
F1
) (
ik_lam
clA2
clM2
F2
).
Proof
.
unfold
ik_lam
,
ik_eq_fun
;
fold
Can
.
intros
.
elim
H
;
elim
H0
;
trivial
.
destruct
clM1
;
auto
with
coc
.
destruct
clA1
;
eauto
10
with
coc
.
destruct
s0
;
auto
10
with
coc
.
Qed
.

  
Lemma
ik_lam_can
:
    
forall
cl1
cl2
F
,
    (
forall
X
,
can_interp
X
->
can_interp
 (
F
X
)) ->
    
ik_eq_fun
cl1
F
F
->
    
can_interp
 (
ik_lam
cl1
cl2
F
).
Proof
.
unfold
ik_lam
,
ik_eq_fun
;
fold
Can
.
destruct
cl2
;
auto
with
coc
.
destruct
cl1
;
auto
with
coc
.
 
destruct
s0
;
auto
with
coc
.
 
constructor
;
split
;
auto
with
coc
.
Qed
.


  
Definition
ik_pi
cl
i
F
:=
    
let
X
:=
coerce_CR
PROP
i
in

    
match
cl
with

      
Knd
s
=>
iK
PROP
 (
Pi
s
X
(
fun
C
=>
coerce_CR
PROP
 (
F
(
iK
_
C
))))
    |
_
=>
iK
PROP
 (
Pi
PROP
X
(
fun
_
=>
coerce_CR
PROP
 (
F
iT
)))
    
end
.

  
Lemma
ik_pi_ext
:
    
forall
cl1
cl2
A1
A2
B1
B2
,
    
cl1
=
cl2
->
    
ik_eq_can
A1
A2
->
    ((
forall
s
,
cl1
<>
Knd
s
) ->
ik_eq_can
 (
B1
iT
) (
B2
iT
)) ->
    (
forall
s
X
Y
,
     
cl1
=
Knd
s
->
     
eq_can
s
X
Y
->
     
ik_eq_can
 (
B1
(
iK
_
X
)) (
B2
(
iK
_
Y
))) ->
    
ik_eq_can
 (
ik_pi
cl1
A1
B1
) (
ik_pi
cl2
A2
B2
).
Proof
.
intros
.
subst
cl2
.
unfold
ik_pi
in
|- *;
fold
Can
in
|- *.
destruct
cl1
;
constructor
;
apply
eq_can_Pi
;
eauto
with
coc
.
 
apply
eq_can_prod
;
intros
;
apply
eq_can_coerce
;
apply
H1
;
intros
;
   
discriminate
.
 
apply
eq_can_prod
;
intros
;
apply
eq_can_coerce
;
apply
H1
;
intros
;
   
discriminate
.
Qed
.

  
Lemma
ik_pi_can
:
    
forall
cl
X
F
,
    
can_interp
X
->
    (
forall
i
,
can_interp
i
->
can_interp
 (
F
i
)) ->
    
can_interp
 (
ik_pi
cl
X
F
).
Proof
.
unfold
ik_pi
in
|- *;
fold
Can
in
|- *.
destruct
cl
;
intros
;
constructor
;
simpl
in
|- *;
apply
is_can_Pi
;
 
auto
10
with
coc
.
Qed
.


  
Lemma
ik_beta_redex
 :
    
forall
cl1
cl2
F
i
,
    
typ_cls
cl2
(
class_of_ik
 (
F
i
)) ->
    
class_of_ik
i
=
cl1
->
    
ik_app
 (
ik_lam
cl1
cl2
F
)
i
=
F
i
.
Proof
.
intros
cl1
cl2
F
i
H
.
inversion
H
.
 
simpl
in
|- *;
intros
;
destruct
(
F
i
);
try
discriminate
;
reflexivity
.
 
unfold
ik_lam
in
|- *;
fold
Can
in
|- *.
   
destruct
i
;
simpl
in
|- *;
destruct
1;
unfold
ik_app
in
|- *.
   
rewrite
coerce_refl
.
    
destruct
(
F
(
iK
s0
c
));
intros
;
try
discriminate
.
     
injection
H2
;
intro
;
subst
s1
.
     
rewrite
coerce_refl
;
reflexivity
.
  
case
(
F
iT
);
reflexivity
.
Qed
.

  
Lemma
ik_pi_elim
 :
    
forall
cl
X
F
i
t
u
,
    
coerce_CR
PROP
 (
ik_pi
cl
X
F
)
t
->
    
coerce_CR
PROP
X
u
->
    
can_interp
i
->
    
class_of_ik
i
=
cl
->
    
coerce_CR
PROP
 (
F
i
) (
App
t
u
).
Proof
.
unfold
ik_pi
in
|- *;
fold
Can
in
|- *.
intros
cl
X
F
i
t
u
.
destruct
cl
;
repeat
rewrite
coerce_refl
;
simpl
in
|- *;
intros
;
red
in
H
.
 
destruct
i
;
try
discriminate
H2
.
 
destruct
i
;
try
discriminate
H2
.
    
eauto
with
coc
.
 
generalize
H2
;
clear
H2
.
   
destruct
H1
;
simpl
in
|- *;
intro
;
try
discriminate
.
    
injection
H2
;
intro
;
subst
s
.
    
eauto
with
coc
.
Qed
.

  
Lemma
ik_pi_intro
 :
    
forall
cl
X
F
A
t
,
    
can_interp
X
->
    (
forall
i
,
can_interp
i
->
can_interp
 (
F
i
)) ->
    
ik_eq_fun
cl
F
F
->
    (
forall
u
i
,
     
can_interp
i
->
     
class_of_ik
i
=
cl
->
     
coerce_CR
PROP
X
u
->
     
coerce_CR
PROP
 (
F
i
) (
subst
u
t
)) ->
    
sn
A
->
    
match
cl
with
Knd
_
=>
True
 |
Typ
PROP
 =>
True
 |
_
=>
False
end
->
    
coerce_CR
PROP
 (
ik_pi
cl
X
F
) (
Abs
A
t
).
Proof
.
intros
.
unfold
ik_pi
in
|- *;
fold
Can
in
|- *.
destruct
cl
as
[| [|
s1
s2
]|
s
];
destruct
H4
;
try
rewrite
coerce_refl
;
 
apply
Abs_sound
;
intros
;
auto
10
with
coc
.
 
split
;
simpl
in
|- *;
intros
;
auto
with
coc
.
 
split
;
simpl
in
|- *;
intros
;
auto
with
coc
.
   
fold
(
eq_can
PROP
)
in
|- *;
auto
with
coc
.
Qed
.

  
Fixpoint
int_typ
 (
T
:
term
) (
ip
:
intP
) {
struct
T
} :
Int_K
 :=
    
match
T
with

    |
Srt
_
=>
iK
_
(
default_can
PROP
)
    |
Ref
n
=>
ip
n

    |
Abs
A
t
=>
        
let
clA
:=
cl_term
A
(
cls_of_int
ip
)
in

        
let
clt
:=
cl_term
t
(
cons_map
clA
(
cls_of_int
ip
))
in

        
ik_lam
clA
clt
(
fun
i
=>
int_typ
t
(
cons_map
i
ip
))
    |
App
u
v
=>
        
ik_app
 (
int_typ
u
ip
) (
int_typ
v
ip
)
    |
Prod
A
B
=>
        
let
clA
:=
cl_term
A
(
cls_of_int
ip
)
in

        
ik_pi
clA
(
int_typ
A
ip
) (
fun
i
=>
int_typ
B
(
cons_map
i
ip
))
   
end
.


  
Fixpoint
proj_fw
 (
T
:term) (
ip
:
cls
) {
struct
T
} :
term
 :=
    
match
T
with

    |
Abs
A
t
=>
       
let
clA
:=
cl_term
A
ip
in

        
match
cl_term
t
(
cons_map
clA
ip
),
clA
with

        |
Typ
_
,
Typ
_
=>
proj_fw
t
(
cons_map
clA
ip
)
        |
_
,
_
=>
Abs
 (
proj_fw
A
ip
) (
proj_fw
t
(
cons_map
clA
ip
))
        
end

    |
App
u
v
=>
        
match
cl_term
u
ip
,
cl_term
v
ip
with

        |
Typ
_
,
Trm
 =>
proj_fw
u
ip

        |
_
,
_
=>
App
 (
proj_fw
u
ip
) (
proj_fw
v
ip
)
        
end

    |
Prod
A
B
=>
        
let
clA
:=
cl_term
A
ip
in

        
match
cl_term
B
(
cons_map
clA
ip
),
clA
with

          
Knd
_
,
Typ
_
=>
proj_fw
B
(
cons_map
clA
ip
)
        |
_
,
_
=>
Prod
 (
proj_fw
A
ip
) (
proj_fw
B
(
cons_map
clA
ip
))
        
end

    |
_
=>
T

    
end
.