Commit fad12c90 authored by François Thiré's avatar François Thiré

add a coq file because why not?

parent 6ebc8b45
(** Start to implement lambda pi modulo with pretty printing.
TODO:
- Have a better pretty printing for binders
- Have a pretty printer for application
- no substitution
- Try a localy nameless representation, but not implemented
*)
Parameter Var : Set.
Axiom var_dec : forall (x y:Var), {x = y} + {x <> y}.
Inductive sort : Set :=
| SType
| SKind.
Inductive term : Set :=
| TBound : nat -> term
| TFree : Var -> term
| TSort : sort -> term
| TPi : term -> term -> term
| TAbs : term -> term -> term
| TApp : term -> term -> term.
Notation "'#' x" := (TFree x) (at level 10).
Notation "'?' x" := (TBound x) (at level 10).
Notation "'Π' A '~' B" := (TPi A B) (at level 50).
Notation "'λ' A '~' B" := (TAbs A B) (at level 50).
Definition of_sort (s:sort) : term := TSort s.
Coercion of_sort : sort >-> term.
Definition type : term := SType.
Definition kind : term := SKind.
Inductive context : Set :=
| CEmpty : context
| CVar : Var -> term -> context -> context
| CRel : term -> term -> context -> context.
Notation "Γ ',' x ':' A" := (CVar x A Γ) (at level 40, x at level 40).
Notation "[ ]" := CEmpty (at level 80).
Notation "Γ ';' t '≡' u" := (CRel t u Γ) (at level 40).
Reserved Notation "x ':' A '∈' Γ" (at level 60).
Inductive InCtx : context -> Var -> term -> Prop :=
| Now : forall Γ x A, x : A (Γ , x : A)
| After : forall Γ A x y B, x : A Γ -> x : A (Γ, y : B)
where "x ':' A ∈ Γ" := (InCtx Γ x A).
Reserved Notation "Γ '⊢' t ':' A" (at level 45, t at level 55, A at level 55).
Reserved Notation "Γ ✓" (at level 100).
Inductive Conv (Γ: context) : term -> term -> Prop := .
Notation "Γ ⊧ t '≡' u" := (Conv Γ t u) (at level 50).
Inductive typing : context -> term -> term -> Prop :=
| TyAxiom : forall Γ x A, Γ -> x : A Γ -> Γ (# x) : A
| TyType : forall Γ, Γ type : kind
| TyPi : forall Γ A B s x, Γ A : type -> Γ, x : A B : s -> Γ Π A ~ B : s
| TyAbs : forall Γ x A B t s, Γ A : type -> Γ, x : A B : s ->
Γ, x : A t : B -> Γ λ A ~ t : Π A ~ B
| TyApp : forall Γ t u A B, Γ t : Π A ~ B -> Γ u : A -> Γ TApp t u : B
| TyConv : forall Γ t A B s, Γ t : A -> Γ B : s -> Γ A B -> Γ t : B
where "Γ '⊢' t ':' A" := (typing Γ t A)
with well_formed : context -> Prop :=
| WFEmpty : [ ]
| WFVar : forall Γ x A, Γ A : type -> Γ -> Γ , x : A
| WFRel : forall Γ A t u, Γ A : type -> Γ t : A -> Γ u : A -> Γ -> Γ ; t u
where "Γ ✓" := (well_formed Γ).
......@@ -17,8 +17,8 @@
\textbf{Variables} & \(x,y,z,\dots\) & & \\
\textbf{Sorts} & \(s\) & \(\defn\) & \(\ttype{} ~|~ \tkind\) \\
\textbf{Terms} & \(A,B,t,u\) & \(\defn\) & \(x~|~s~|~\tpi{x}{A}{B} ~|~\tabs{x}{A}{u} ~|~ \tapp{t}{u} \)\\
\textbf{Relations} & \(\mathcal{R}\) & & \\
\textbf{Context} & \(\Gamma\) & \(\defn\) & \(\emptyset~|~\Gamma, x:A~|~\Gamma, \mathcal{R}\)\\
\textbf{Relations} & \(\mathcal{R}\) &\(\defn\) & \((t,u)\) \\
\textbf{Context} & \(\Gamma\) & \(\defn\) & \([]~|~\Gamma, x:A~|~\Gamma, \mathcal{R}\)\\
\textbf{Typing Judgment} & & & \(\Gamma \vdash t : A\)\\
\textbf{Typing context well-formed} & & & \(\phantom{\Gamma} \vdash \wf{\Gamma}\) \\
\textbf{Relation well-formed} & & & \(\Gamma \vdash \wf{\mathcal{R}}\) \\
......@@ -49,21 +49,21 @@
\end{definition}
\begin{definition}
We define \(\conv_{\beta\Gamma}\) as the reflexive, symmetric, transitive closure of \(\beta\) and \(\bigcup_{\mathcal{R} \in \Gamma} \mathcal{R}\) and closed by context.
We define \(\convbg\) as the reflexive, symmetric, transitive closure of \(\beta\) and \(\bigcup_{\mathcal{R} \in \Gamma} \mathcal{R}\) and closed by context.
\end{definition}
\begin{rules}{typing}{Typing rules}
\inferrule{ }
\inferrule*{ }
{\wf{\emptyset}}
\and
\inferrule{
\inferrule*{
\wf{\Gamma}
\\
{\Gamma \vdash A : \ttype}
}
{\wf{\Gamma, x:A}}
\and
\inferrule{
\inferrule*{
\wf{\Gamma}
\\
{\mathcal{R} \in \mathfrak{R}_{Dom(\Gamma)}}
......@@ -72,30 +72,34 @@
}
{\wf{\Gamma, \mathcal{R}}}
\and
\inferrule{
TODO
\inferrule*[Right=Rel]{
\Gamma \vdash A : \ttype
\\
\Gamma \vdash t : A
\\
\Gamma \vdash u : A
}
{\Gamma \vdash \wf{\mathcal{R}}}
{\Gamma \vdash \wf{\mathcal{R} = (t,u)}}
\and
\inferrule{
\inferrule*{
\wf{\Gamma}
\\
x : A \in \Gamma
}
{\Gamma \vdash x : A}
\and
\inferrule{
\inferrule*{
}
{\Gamma \vdash \ttype : \tkind}
\and
\inferrule{
\inferrule*{
\Gamma \vdash A : \ttype
\\
\Gamma, x : A \vdash B : s
}
{\Gamma \vdash \tpi{x}{A}{B} : s}
\and
\inferrule{
\inferrule*{
\Gamma \vdash A : \ttype
\\
\Gamma, x : A \vdash B : s
......@@ -104,21 +108,38 @@
}
{\Gamma \vdash \tabs{x}{A}{t} : \tpi{x}{A}{B}}
\and
\inferrule{
\inferrule*{
\Gamma \vdash t : \tpi{x}{A}{B}
\\
\Gamma \vdash u : A
}
{\Gamma \vdash t~u : \subst{B}{x}{u}}
\and
\inferrule{
\inferrule*{
\Gamma \vdash t : A
\\
\Gamma \vdash B : s
\\
A \conv_{\beta\Gamma} B
A \convbg B
}
{\Gamma \vdash t: B}
\end{rules}
\begin{lemma}
For any context \(\Gamma\), if \(\tkind \convbg t\) then \(t = \tkind\).
\end{lemma}
\begin{proof}
By induction on the length of \(\Gamma\), we can prove that there is no \(u\) such that \(\Gamma \vdash \wf{(\tkind,u)}\) or the symmetrical case are derivable. From this, we can conclude the statement.
\todo{Peut-on le prouver sans induction ?}
\end{proof}
\begin{lemma}
For any context \(\Gamma\), if \(\ttype \convbg t\) then \(t = \ttype\).
\end{lemma}
\begin{proof}
Same proof as the precedent lemma.
\end{proof}
Notice that if we want to be pedantic, the proofs above need actually to prove a mutual judgment since the congruence relation and the typing judgements are mutually defined.
\end{document}
\newtheorem{definition}{Definition}
\newtheorem{lemma}{Lemma}
\newcommand{\lfmt}{\ensuremath{\lambda\Pi\text{-modulo theory}}}
\newcommand{\defn}{\ensuremath{:=}}
......@@ -16,6 +18,8 @@
\newcommand{\conv}{\ensuremath{\equiv}}
\newcommand{\convbg}{\ensuremath{\conv_{\beta\Gamma}}}
\newcommand{\wf}[1]{\ensuremath{{#1}~\mathbf{wf}}}
\newcommand{\subst}[3]{\ensuremath{#1[#2 \leftarrow #3]}}
......@@ -39,3 +43,7 @@
\end{figure}
}
\newcommand{\todo}[1]{}
\renewcommand{\todo}[1]{{\color{red} TODO: {#1}}}
\ No newline at end of file
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