Commit c340e2a1 authored by Gaspard Ferey's avatar Gaspard Ferey

Added second implementation. Added makefiles.

parent 2fc865ff
This diff is collapsed.
# This configuration file was generated by running:
# coq_makefile -f Make -o CoqMakefile
###############################################################################
# #
# Project files. #
# #
###############################################################################
COQMF_VFILES = LPTerm.v STT.v WF.v conversion.v properties.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
COQMF_MLPACKFILES =
COQMF_MLLIBFILES =
###############################################################################
# #
# Path directives (-I, -R, -Q). #
# #
###############################################################################
COQMF_OCAMLLIBS = -I .
COQMF_SRC_SUBDIRS = .
COQMF_COQLIBS = -I . -R . Top
COQMF_COQLIBS_NOML = -R . Top
###############################################################################
# #
# Coq configuration. #
# #
###############################################################################
COQMF_LOCAL=0
COQMF_COQLIB=/home/gferey/.opam/4.04.2/lib/coq/
COQMF_DOCDIR=/home/gferey/.opam/4.04.2/doc/
COQMF_OCAMLFIND=/home/gferey/.opam/4.04.2/bin/ocamlfind
COQMF_CAMLP4=camlp5
COQMF_CAMLP4O=/home/gferey/.opam/4.04.2/bin/camlp5o
COQMF_CAMLP4BIN=/home/gferey/.opam/4.04.2/bin/
COQMF_CAMLP4LIB=/home/gferey/.opam/4.04.2/lib/camlp5
COQMF_CAMLP4OPTIONS=-loc loc
COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50 -safe-string
COQMF_HASNATDYNLINK=true
COQMF_COQ_SRC_SUBDIRS=config dev lib kernel library engine pretyping interp parsing proofs tactics toplevel printing intf grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml
COQMF_WINDRIVE=/home/gferey/.opam/4.04.2/lib/coq
###############################################################################
# #
# Extra variables. #
# #
###############################################################################
COQMF_OTHERFLAGS =
COQMF_INSTALLCOQDOCROOT = Top
This diff is collapsed.
LPTerm.vo LPTerm.glob LPTerm.v.beautified: LPTerm.v
LPTerm.vio: LPTerm.v
LPTerm.v
STT.v
WF.v
conversion.v
properties.v
.PHONY: all clean
all: CoqMakefile
make -f CoqMakefile - all
clean: CoqMakefile
make -f CoqMakefile - clean
CoqMakefile: Make
coq_makefile -f Make -o CoqMakefile
STT.vo STT.glob STT.v.beautified: STT.v ./LPTerm.vo
STT.vio: STT.v ./LPTerm.vio
WF.vo WF.glob WF.v.beautified: WF.v ./LPTerm.vo
WF.vio: WF.v ./LPTerm.vio
conversion.vo conversion.glob conversion.v.beautified: conversion.v ./LPTerm.vo ./WF.vo
conversion.vio: conversion.v ./LPTerm.vio ./WF.vio
properties.vo properties.glob properties.v.beautified: properties.v ./LPTerm.vo ./WF.vo ./conversion.vo
properties.vio: properties.v ./LPTerm.vio ./WF.vio ./conversion.vio
This diff is collapsed.
# This configuration file was generated by running:
# coq_makefile -f Make -o CoqMakefile
###############################################################################
# #
# Project files. #
# #
###############################################################################
COQMF_VFILES = LPTerm.v STT.v WF.v conversion.v properties.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
COQMF_MLPACKFILES =
COQMF_MLLIBFILES =
###############################################################################
# #
# Path directives (-I, -R, -Q). #
# #
###############################################################################
COQMF_OCAMLLIBS = -I .
COQMF_SRC_SUBDIRS = .
COQMF_COQLIBS = -I . -R . Top
COQMF_COQLIBS_NOML = -R . Top
###############################################################################
# #
# Coq configuration. #
# #
###############################################################################
COQMF_LOCAL=0
COQMF_COQLIB=/home/gferey/.opam/4.04.2/lib/coq/
COQMF_DOCDIR=/home/gferey/.opam/4.04.2/doc/
COQMF_OCAMLFIND=/home/gferey/.opam/4.04.2/bin/ocamlfind
COQMF_CAMLP4=camlp5
COQMF_CAMLP4O=/home/gferey/.opam/4.04.2/bin/camlp5o
COQMF_CAMLP4BIN=/home/gferey/.opam/4.04.2/bin/
COQMF_CAMLP4LIB=/home/gferey/.opam/4.04.2/lib/camlp5
COQMF_CAMLP4OPTIONS=-loc loc
COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50 -safe-string
COQMF_HASNATDYNLINK=true
COQMF_COQ_SRC_SUBDIRS=config dev lib kernel library engine pretyping interp parsing proofs tactics toplevel printing intf grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml
COQMF_WINDRIVE=/home/gferey/.opam/4.04.2/lib/coq
###############################################################################
# #
# Extra variables. #
# #
###############################################################################
COQMF_OTHERFLAGS =
COQMF_INSTALLCOQDOCROOT = Top
LPTerm.v
STT.v
WF.v
conversion.v
properties.v
.PHONY: all clean
all: CoqMakefile
make -f CoqMakefile - all
clean: CoqMakefile
make -f CoqMakefile - clean
CoqMakefile: Make
coq_makefile -f Make -o CoqMakefile
Require Import List.
Require Import LPTerm.
Parameter OtherVars : Set.
Axiom o_var_dec : forall (x y:OtherVars), {x = y} + {x <> y}.
Axiom o_var_inf : forall (l : list OtherVars), exists x, ~ (In x l).
Inductive Var :=
| Ctype | Cι| Co | Carrow | Cη | Cimpl | Cfa | Cε
| V_a | V_b | V_c | V_x | V_y | V_z | V_F | V_G | V_X | V_Y | V_Z | V_f | V_g
| V_other : OtherVars -> Var.
Theorem var_dec : forall (x y:Var), {x = y} + {x <> y}.
Proof.
intros. induction x ; induction y; try (apply left; easy); try (apply right; easy).
destruct (o_var_dec o o0).
- left. rewrite e. easy.
- right. intro. apply n.
Qed.
Axiom var_inf : forall l, exists x:Var, ~ (In x l).
Parameter type : Var.
Parameter ι : Var.
Parameter o : Var.
Parameter arrow : Var.
Parameter η : Var.
Parameter impl : Var.
Parameter fa : Var.
Parameter ε : Var.
Parameter a b c x y z F G X Y Z f g : Var.
Theorem util_var_decl c x A : c -> (c -> c, x : A ) -> c, x : A .
Proof. exact (fun x f => f x). Qed.
Theorem util_rul_decl c t u : c -> (c -> c, t u ) -> c, t u .
Proof. exact (fun x f => f x). Qed.
Definition STT := []
, type : TType
, ι : # type
, o : # type
, arrow : # type ~> # type ~> # type
, η : # type ~> TType
, ε : # η @ # o ~> # η @ # o
, impl : # η @ # o ~> # η @ # o ~> # η @ # o
, fa : a ; # type ~> (# η @ # a ~> # η @ # o) ~> (# η @ # o)
,
x ; # type => y ; # type => # η @ (# arrow @ # x @ # y)
x ; # type => y ; # type => (# η @ # x ~> # η @ # y)
,
x ; # type => y ; # type => # ε @ (# impl @ # x @ # y)
x ; # type => y ; # type => (# ε @ # x ~> #ε @ # y)
,
a ; # type => f ; # type => # ε @ (#fa @ #a @ #f)
a ; # type => f ; # type => z ; (#η @ #a) => # ε @ (#f @ #x)
.
Theorem STT_WF : STT .
Proof.
try repeat apply util_rul_decl || apply util_var_decl.
constructor.
- intro. apply WFVarK. intro. inversion H0. inversion H1. constructor. constructor.
- intro. constructor. intro. inversion H0. inversion H1. subst. apply TyAxiom. easy. repeat constructor.
- intro. constructor. apply TyAxiom. easy. repeat constructor.
- intro. constructor. apply TyPi. constructor.
+ easy.
+ repeat constructor.
+ intros. apply TyPi.
* constructor. apply util_var_decl.
-- easy.
-- intro. apply WFVarT. apply TyAxiom. easy. repeat constructor.
-- repeat constructor.
* intros. apply TyAxiom. apply util_var_decl. apply util_var_decl. easy. intros. constructor. apply TyAxiom. easy. repeat constructor. intros. constructor. apply TyAxiom. easy. repeat constructor. repeat constructor.
- intro. apply WFVarK. constructor.
+ constructor. easy. repeat constructor.
+ intros.
constructor. constructor. constructor. easy. repeat constructor.
- intros. apply WFVarT. constructor.
+ apply
Qed.
This diff is collapsed.
Require Import LPTerm.
Require Import WF.
Lemma inversion_rel : forall Γ t u, Γ -> t u Γ -> exists s A Δ, Δ t : A /\ Δ u : A /\ Δ A : s.
Proof.
intros.
induction Γ.
- inversion H0.
- inversion H.
subst. inversion H0 ; subst. apply IHΓ.
+ eapply vardecl_WF. apply H.
+ easy.
+ eapply IHΓ. eapply vardecl_WF . apply H. inversion H0. subst. easy.
- inversion H0; subst.
inversion H ; subst.
+ exists s,A,Γ.
split. apply H5.
split. apply H6. apply H4.
+ apply IHΓ. eapply ruldecl_WF. apply H. easy.
Qed.
Require Import LPTerm.
Require Import WF.
Require Import conversion.
Theorem kind_not_typable2 : forall Γ T t, Γ t : T -> ~ (t = kind).
Proof. intros. induction H; try easy. Qed.
Theorem kind_not_typable : forall Γ T, Γ kind : T -> False.
Proof. intros. pose proof (kind_not_typable2 _ _ _ H). easy. Qed.
Lemma not_var_kind_gamma : forall Γ x, Γ -> ~ (x : kind Γ).
Proof.
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.
Qed.
Lemma not_rel_kind_gamma_left : forall Γ t, Γ, kind t -> False.
Proof. intros; inversion H ; subst ; eapply kind_not_typable ; eassumption. Qed.
Lemma not_rel_kind_gamma_right : forall Γ t, Γ, t kind -> False.
Proof. intros; inversion H ; subst ; eapply kind_not_typable ; eassumption. Qed.
Lemma rel_kind_in_left : forall Γ t, Γ -> kind t Γ -> False.
Proof.
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.
Qed.
Lemma rel_kind_in_right : forall Γ t, Γ -> t kind Γ -> False.
Proof.
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.
Qed.
Reserved Notation "t '▷' u" (at level 40, u at level 25).
Inductive R_Subterm : term -> term -> Prop :=
| HSubRefl : forall x , x x
| HSubPi1 : forall x A B, A x -> (Π A ~ B) x
| HSubPi2 : forall x A B, B x -> (Π A ~ B) x
| HSubAbs1 : forall x A t, A x -> (λ A ~ t) x
| HSubAbs2 : forall x A t, t x -> (λ A ~ t) x
| HSubApp1 : forall x t u, t x -> (t @ u) x
| HSubApp2 : forall x t u, u x -> (t @ u) x
where "t '▷' u" := (R_Subterm t u).
Definition BV_closed (t:term) : Prop := forall k, ~ (t ? k).
Definition FV_closed (t:term) : Prop := forall v, ~ (t # v).
Theorem __ : forall t, BV_closed t -> forall k u, BV_closed (t[k <- u]).
Proof.
intro. intro.
induction t; intros; simpl; try easy.
- contradiction (H n). econstructor.
-
Theorem __ : forall t u, closed t -> u t -> forall k v, u[k <- v] t.
Proof.
do 4 intro.
induction H0; intros.
-
Theorem conv_kind_not_typable : forall Γ t, Γ t →β kind -> forall T, ~ (Γ t : T).
Theorem conv_kind_not_typable : forall Γ t, Γ t →β kind -> forall T, ~ (Γ t : T).
Proof.
do 3 intro. remember kind as K.
destruct H.
destruct t.
- intros. intro.
remember ((λ A ~ TKind) @ u) as t.
destruct H; try inversion Heqt.
+ subst. inversion H.
* subst. destruct (var_inf L). pose proof (H8 x H1). eapply kind_not_typable. apply H2.
* subst.
+
Theorem conv_kind_not_typable : forall Γ t, Γ t kind -> forall T, ~ (Γ t : T).
Proof.
do 3 intro.
remember kind as K.
induction H.
- intros. subst. intro. eapply kind_not_typable. apply H.
- subst. induction H.
+ apply IHRSTClosure. easy.
Qed.
Lemma kind_conv : forall Γ t T, Γ t : T -> Γ type t -> type = t.
Proof.
intros.
remember kind as K.
induction H.
- easy.
- subst; try easy.
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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment