properties.v 2.2 KB
Newer Older
Gaspard Ferey's avatar
Gaspard Ferey committed
1 2

Require Import LPTerm.
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
3
Require Import WF.
Gaspard Ferey's avatar
Gaspard Ferey committed
4 5 6
Require Import conversion.


Gaspard Ferey's avatar
Gaspard Ferey committed
7 8 9
Theorem kind_not_typable2 : forall Γ T t, Γ  t : T -> ~ (t = kind).
Proof. intros. induction H; try easy. Qed.

Gaspard Ferey's avatar
Gaspard Ferey committed
10
Theorem kind_not_typable : forall Γ T, Γ  kind : T -> False.
Gaspard Ferey's avatar
Gaspard Ferey committed
11
Proof. intros. pose proof (kind_not_typable2 _ _ _ H). easy. Qed.
Gaspard Ferey's avatar
Gaspard Ferey committed
12

Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
13
Lemma not_var_kind_gamma : forall Γ x, Γ  -> ~ (x : kind  Γ).
Gaspard Ferey's avatar
Gaspard Ferey committed
14
Proof.
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
15 16 17 18 19 20 21 22 23
  intros. intro.
  remember (kind) as K.
  induction H0.
  - remember (Γ, x : A) as Γ'.
    destruct H; inversion HeqΓ'.
    + subst. apply (kind_not_typable _ _ H0).
    + subst. apply (kind_not_typable _ _ H0).
  - apply IHInCtx. eapply vardecl_WF. apply H. easy.
   -apply IHInCtx. eapply ruldecl_WF. apply H. easy.
Gaspard Ferey's avatar
Gaspard Ferey committed
24 25 26
Qed.

Lemma not_rel_kind_gamma_left : forall Γ t, Γ, kind  t  -> False.
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
27
Proof. intros; inversion H ; subst ; eapply kind_not_typable ; eassumption. Qed.
Gaspard Ferey's avatar
Gaspard Ferey committed
28 29

Lemma not_rel_kind_gamma_right : forall Γ t, Γ, t  kind  -> False.
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
30
Proof. intros; inversion H ; subst ; eapply kind_not_typable ; eassumption. Qed.
Gaspard Ferey's avatar
Gaspard Ferey committed
31 32 33

Lemma rel_kind_in_left : forall Γ t, Γ  -> kind  t  Γ -> False.
Proof.
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
34 35 36 37 38 39
  intros.
  remember (kind) as K.
  induction H0; subst.
  - eapply not_rel_kind_gamma_left. apply H.
  - apply IHInRelCtx. eapply vardecl_WF. apply H. easy.
  - apply IHInRelCtx. eapply ruldecl_WF. apply H. easy.
Gaspard Ferey's avatar
Gaspard Ferey committed
40 41 42 43
Qed.

Lemma rel_kind_in_right : forall Γ t, Γ  -> t  kind  Γ -> False.
Proof.
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
44 45 46 47 48 49
  intros.
  remember (kind) as K.
  induction H0; subst.
  - eapply not_rel_kind_gamma_right. apply H.
  - apply IHInRelCtx. eapply vardecl_WF. apply H. easy.
  - apply IHInRelCtx. eapply ruldecl_WF. apply H. easy.
Gaspard Ferey's avatar
Gaspard Ferey committed
50 51
Qed.

Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
52
Theorem conv_kind_not_typable : forall Γ t T, Γ  t : T -> ~ (Γ  t  T).
Gaspard Ferey's avatar
Gaspard Ferey committed
53
Proof.
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
54 55 56 57
  intros. intro.
  induction H0.
  
  Qed.
Gaspard Ferey's avatar
Gaspard Ferey committed
58 59 60



Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
61
Lemma kind_conv : forall Γ t T, Γ  t : T -> Γ  type  t -> type = t.
Gaspard Ferey's avatar
Gaspard Ferey committed
62 63
Proof.
  intros.
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
64 65
  remember kind as K.
  induction H.
Gaspard Ferey's avatar
Gaspard Ferey committed
66
  - easy.
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
67 68
  - subst; try easy.
  
Gaspard Ferey's avatar
Gaspard Ferey committed
69 70 71 72 73 74 75 76 77 78 79 80 81 82

Lemma type_kind : forall Γ A, Γ  type : A -> A = kind.
Proof.
  intros.
  remember type as x.
  induction H ; try inversion Heqx.
  - easy.
  - apply IHtyping1 in H2.
    pose proof (inversion_typing Γ t A H).
    subst.
    pose proof (inverse_kind Γ B H3 kind H1).
    now apply H2.
Qed.