Library Consistency


Require
 Import
 Termes.

Require
 Import
 Types
.

Require
 Import
 Conv.

Require
 Import
 Conv_Dec.

Require
 Import
 Strong_Norm.




Require
 Import
 Omega.




Fixpoint
 applist (l
 : list term) : term -> term :=

  fun
 t
 =>

  match
 l
 with


  | nil => t


  | arg
 :: args
 => App (applist args
 t
) arg


  end
.




Lemma
 applist_assoc :

 forall
 t
 e
 e'
, applist (e
 ++ e'
) t
 = applist e
 (applist e'
 t
).

simple
 induction
 e
; simpl
 in
 |- *; intros
; auto
.

rewrite
 H
; trivial
.

Qed
.




Lemma
 inv_typ_applist_head :

 forall
 e
 t
 l
 T
, typ e
 (applist l
 t
) T
 -> exists
 U
, typ e
 t
 U
.

Proof
.

simple
 induction
 l
; simpl
 in
 |- *; intros
.

split
 with
 T
; trivial
.




apply
 inv_typ_app with
 (1 := H0
); intros
.

eauto
.

Qed
.




Definition
 is_atom (e
 : env
) t
 :=

  exists2
 n
, n
 < length e
 & (exists
 l
, t
 = applist l
 (Ref n
)).




Lemma
 sort_not_atom : forall
 e
 s
, ~ is_atom e
 (Srt s
).

intros
 e
 s
 (n
, lt_n
, ([| t
 l
], eq_atom
)); discriminate
 eq_atom
.

Qed
.




Lemma
 prod_not_atom : forall
 e
 T
 M
, ~ is_atom e
 (Prod T
 M
).

intros
 e
 T
 M
 (n
, lt_n
, ([| t
 l
], eq_atom
)); discriminate
 eq_atom
.

Qed
.




Lemma
 is_atom_app : forall
 e
 a
 b
, is_atom e
 a
 -> is_atom e
 (App a
 b
).

intros
 e
 a
 b
 (n
, lt_n
, (l
, eq_atom
)).

rewrite
 eq_atom
.

exists
 n
; trivial
.

exists
 (b
 :: l
); trivial
.

Qed
.




Lemma
 atom_reduction : forall
 e
 t
 u
, red t
 u
 -> is_atom e
 t
 -> is_atom e
 u
.

simple
 induction
 1; intros
; trivial
.

generalize
 (H1
 H3
); clear
 H1
 H3
.

intros
 (n
, lt_n
, (l
, eq_atom
)).

rewrite
 eq_atom
 in
 H2
.

exists
 n
; trivial
.

generalize
 N
 H2
; clear
 N
 H2
 eq_atom
 H0
.

elim
 l
; simpl
 in
 |- *; intros
.

 inversion
 H2
.




 inversion
 H2
.

  apply
 False_ind.

  generalize
 H3
.

  case
 l0
; simpl
 in
 |- *; discriminate
.




  elim
 H0
 with
 (1 := H5
); intros
.

  rewrite
 H6
.

  exists
 (a
 :: x
); reflexivity
.




  exists
 (N2
 :: l0
); reflexivity
.

Qed
.




Lemma
 conv_sort_atom : forall
 (s
 : sort) e
 u
, is_atom e
 u
 -> ~ conv (Srt s
) u
.

Proof
.

red
 in
 |- *; intros
.

elim
 church_rosser with
 (1 := H0
); intros
.

rewrite
 <- red_normal with
 (1 := H1
) in
 H2
.

specialize
 atom_reduction with
 (1 := H2
) (2 := H
).

apply
 sort_not_atom.




red
 in
 |- *; red
 in
 |- *; intros
.

inversion
 H3
.

Qed
.




  Lemma
 conv_prod_atom : forall
 a
 b
 e
 u
, is_atom e
 u
 -> ~ conv (Prod a
 b
) u
.

red
 in
 |- *; intros
.

elim
 church_rosser with
 (1 := H0
); intros
.

apply
 red_prod_prod with
 (1 := H1
); intros
.

rewrite
 H3
 in
 H2
.

specialize
 atom_reduction with
 (1 := H2
) (2 := H
).

apply
 prod_not_atom.

Qed
.




Lemma
 prod_inhabitants :

 forall
 e
 t
 u
,

 typ e
 t
 u
 ->

 forall
 a
 b
,

 conv u
 (Prod a
 b
) ->

 normal t
 -> is_atom e
 t
 \/ (exists
 a'
, (exists
 m
, t
 = Abs a'
 m
)).

Proof
.

simple
 induction
 1; intros
; eauto
.

elim
 conv_sort_prod with
 (1 := H1
).




left
.

exists
 v
.

inversion_clear
 H1
.

elim
 H5
; intros
; simpl
 in
 |- *; auto
 with
 arith
.




exists
 (nil (A
:=term)); simpl
 in
 |- *; auto
.




left
.

apply
 is_atom_app.

elim
 H3
 with
 V
 Ur
; intros
; auto
 with
 coc
.

inversion_clear
 H6
.

inversion_clear
 H7
.

rewrite
 H6
 in
 H5
.

elim
 H5
 with
 (subst v
 x0
); auto
 with
 coc
.




red
 in
 |- *; red
 in
 |- *; intros
.

elim
 H5
 with
 (App u1
 v
); auto
 with
 coc
.




elim
 conv_sort_prod with
 (1 := H4
).




apply
 H1
 with
 a
 b
; auto
.

apply
 trans_conv_conv with
 V
; auto
.

Qed
.




Definition
 hnf_proofs (e
 : env
) (t
 : term) : Prop
 :=

  match
 t
 with


  | App _
 _
 => is_atom e
 t


  | _
 => True

  end
.




Lemma
 hnf_proofs_sound :

 forall
 e
 t
 T
, typ e
 t
 T
 -> normal t
 -> hnf_proofs e
 t
.

simple
 induction
 1; simpl
 in
 |- *; intros
; auto
.

apply
 is_atom_app.

elim
 prod_inhabitants with
 (1 := H2
) (a
 := V
) (b
 := Ur
); intros
;

 auto
 with
 coc
.

inversion_clear
 H5
.

inversion_clear
 H6
.

rewrite
 H5
 in
 H4
.

elim
 H4
 with
 (subst v
 x0
); auto
 with
 coc
.




red
 in
 |- *; red
 in
 |- *; intros
.

elim
 H4
 with
 (App u0
 v
); auto
 with
 coc
.

Qed
.




Lemma
 atom_inhabitants :

 forall
 e
 t
 u
 u'
,

 typ e
 t
 u
 -> conv u
 u'
 -> is_atom e
 u'
 -> hnf_proofs e
 t
 -> is_atom e
 t
.

simple
 induction
 1; simpl
 in
 |- *; intros
; auto
.

elim
 conv_sort_atom with
 (1 := H2
) (2 := H1
).




split
 with
 v
.

inversion_clear
 H1
.

elim
 H6
; simpl
 in
 |- *; auto
 with
 arith
.




split
 with
 (nil (A
:=term)); auto
.




elim
 conv_prod_atom with
 (1 := H7
) (2 := H6
).




elim
 conv_sort_atom with
 (1 := H5
) (2 := H4
).




apply
 H1
; auto
.

apply
 trans_conv_conv with
 V
; auto
 with
 coc
.

Qed
.




Definition
 absurd_prop := Prod (Srt prop) (Ref 0).




Lemma
 coc_consistency_nf : forall
 t
, normal t
 -> ~ typ nil t
 absurd_prop.

Proof
.

unfold
 absurd_prop
 in
 |- *.

red
 in
 |- *; intros
.

elim
 prod_inhabitants with
 (1 := H0
) (a
 := Srt prop) (b
 := Ref 0) (3 := H
);

 auto
 with
 coc
.

intros
.

inversion_clear
 H1
.

inversion
 H2
.




intros
 (ty
, (M
, eq_abs
)).

rewrite
 eq_abs
 in
 H0
.

apply
 inv_typ_abs with
 (1 := H0
); intros
.

specialize
 inv_conv_prod_l with
 (1 := H4
); intro
 conv_ty
.

specialize
 inv_conv_prod_r with
 (1 := H4
); intro
 conv_P
.

clear
 H0
 H4
 H3
 H1
.

assert
 (M_atom
: is_atom (ty
 :: nil) M
).

  apply
 atom_inhabitants with
 (1 := H2
) (2 := conv_P
).

  split
 with
 0; simpl
 in
 |- *; auto
 with
 arith
; split
 with
 (nil (A
:=term));

   trivial
.




  apply
 hnf_proofs_sound with
 (1 := H2
).

  rewrite
 eq_abs
 in
 H
.

  red
 in
 |- *; red
 in
 |- *; intros
.

  elim
 H
 with
 (Abs ty
 u
); auto
 with
 coc
.




destruct
 M_atom
 as
 (n
, lt_n
, (l
, eq_atom
)).

simpl
 in
 lt_n
.

generalize
 eq_atom
; clear
 eq_atom
.

replace
 n
 with
 0; try
 omega
.

rewrite
 <- (rev_involutive l
).

case
 (rev l
); simpl
 in
 |- *; intros
; rewrite
 eq_atom
 in
 H2
.

apply
 inv_typ_ref with
 (1 := H2
).

intros
 U
 itm_U
.

inversion_clear
 itm_U
.

intro
 conv_T
.

cut
 (Ref 0 = Srt prop); try
 discriminate
.

apply
 nf_uniqueness.

apply
 trans_conv_conv with
 T
; auto
 with
 coc
.

apply
 trans_conv_conv with
 (lift 1 ty
); auto
 with
 coc
.

change
 (conv (lift_rec 1 ty
 0) (lift_rec 1 (Srt prop) 0)) in
 |- *.

apply
 conv_conv_lift; auto
 with
 coc
.




red
 in
 |- *; red
 in
 |- *; intros
 r
 red_n
; inversion
 red_n
.




red
 in
 |- *; red
 in
 |- *; intros
 r
 red_n
; inversion
 red_n
.




rewrite
 applist_assoc in
 H2
.

simpl
 in
 H2
.

elim
 inv_typ_applist_head with
 (1 := H2
); intros
.

clear
 H2
 eq_atom
.

apply
 inv_typ_app with
 (1 := H0
); intros
.

apply
 inv_typ_ref with
 (1 := H1
); intros
.

apply
 conv_sort_prod with
 prop V
 Ur
.

apply
 trans_conv_conv with
 (lift 1 U
); auto
 with
 coc
.

apply
 sym_conv.

change
 (conv (lift_rec 1 U
 0) (lift_rec 1 (Srt prop) 0)) in
 |- *.

inversion_clear
 H4
.

apply
 conv_conv_lift; auto
 with
 coc
.

Qed
.




Theorem
 coc_consistency : forall
 t
, ~ typ nil t
 absurd_prop.

Proof
.

red
 in
 |- *; intros
.

elim
 compute_nf with
 t
; intros
.

specialize
 subject_reduction with
 (1 := p
) (2 := H
).

apply
 coc_consistency_nf; trivial
.




apply
 strong_norm with
 (1 := H
).

Qed
.