Commit 54333a96 authored by Valentin Blot's avatar Valentin Blot
Browse files

Comments in the Coq file.

parent 11c2509a
......@@ -4,16 +4,23 @@ Require Import Arith.
Require Import List.
Import ListNotations.
Import EqNotations.
(* Types of System F.
We use de Bruijn indices,
so variables are in nat. *)
Inductive type : Type :=
| TVar : nat -> type
| TArrow : type -> type -> type
| TForall : type -> type.
(* "type_lift n T" increments every free
variable of T with index m >= n. *)
Fixpoint type_lift (n : nat) (T : type) : type :=
match T with
| TVar m => if m <? n then TVar m else TVar (S m)
| TArrow T U => TArrow (type_lift n T) (type_lift n U)
| TForall T => TForall (type_lift (S n) T)
end.
(* "type_subst n T U" is T[U/n]. All free
variables of T with index > n are decremented. *)
Fixpoint type_subst (n : nat) (T : type) (U : type) : type :=
match T with
| TVar m =>
......@@ -26,14 +33,20 @@ Fixpoint type_subst (n : nat) (T : type) (U : type) : type :=
| TForall T => TForall (type_subst (S n) T (type_lift 0 U))
end.
(* Curch-style terms of System F.
de Bruijn indices again. *)
Inductive fterm : Type :=
| FVar : nat -> fterm
| FAbs : type -> fterm -> fterm
| FApp : fterm -> fterm -> fterm
| FTAbs : fterm -> fterm
| FTApp : fterm -> type -> fterm.
(* ΛX.λx:X.x *)
Definition term1 : fterm := FTAbs (FAbs (TVar 0) (FVar 0)).
(* λx:X(XX).x(X(XX))x *)
Definition term2 : fterm := FAbs (TForall (TArrow (TVar 0) (TVar 0))) (FApp (FTApp (FVar 0) (TForall (TArrow (TVar 0) (TVar 0)))) (FVar 0)).
(* "type_get context t" is the type
of t in context context. *)
Fixpoint type_get (context : list type) (t : fterm) : type :=
match t with
| FVar n => nth n context (TVar 0)
......@@ -50,6 +63,8 @@ Fixpoint type_get (context : list type) (t : fterm) : type :=
| _ => TVar 0
end
end.
(* "type_correct context t" holds if
t is typable in context context. *)
Fixpoint type_correct (context : list type) (t : fterm) : Prop :=
match t with
| FVar n => n < length context
......@@ -59,10 +74,14 @@ Fixpoint type_correct (context : list type) (t : fterm) : Prop :=
| FTApp t T => type_correct context t /\ exists T, type_get context t = TForall T
end.
(* Untyped lambda-terms.
Still de Bruijn indices. *)
Inductive term : Type :=
| Var : nat -> term
| Abs : term -> term
| App : term -> term -> term.
(* Erasure from Church-style System F
terms to untyped (Curry-style) terms *)
Fixpoint fterm_to_term (t : fterm) : term :=
match t with
| FVar n => Var n
......@@ -71,6 +90,8 @@ Fixpoint fterm_to_term (t : fterm) : term :=
| FTAbs t => fterm_to_term t
| FTApp t T => fterm_to_term t
end.
(* "term_equal t u" is true if t and u
are syntactically equal. *)
Fixpoint term_equal (t : term) (u : term) : bool :=
match t, u with
| Var m, Var n => m =? n
......@@ -78,12 +99,17 @@ Fixpoint term_equal (t : term) (u : term) : bool :=
| App t1 t2, App u1 u2 => andb (term_equal t1 u1) (term_equal t2 u2)
| _, _ => false
end.
(* "term_lift n t" increments every free
variable of t with index m >= n. *)
Fixpoint term_lift (n : nat) (t : term) : term :=
match t with
| Var m => if m <? n then Var m else Var (S m)
| Abs t => Abs (term_lift (S n) t)
| App t u => App (term_lift n t) (term_lift n u)
end.
(* "term_subst n t p" is t[p/n]. Every
free variable of t with index > n + |p|
is decremented by |p|. *)
Fixpoint term_subst (n : nat) (t : term) (p : list term) : term :=
match t with
| Var m => if m <? n then Var m else nth (m - n) p (Var (pred m))
......@@ -91,6 +117,16 @@ Fixpoint term_subst (n : nat) (t : term) (p : list term) : term :=
| App t u => App (term_subst n t p) (term_subst n u p)
end.
(* Formulas of the logic. LVar is a constant
in the sense of the logic (it can't be
substituted), while LMetaVar is a variable
in the sense of the logic (it can be
substituted with a term of the logic).
LMetaSubst is the simbol of the logic that
allows to talk formally about substitutions.
LLVar is also a variable in the sense of the
logic, but of sort "list of terms". LLList
is a list of terms of the logic. *)
Inductive logterm : Type :=
| LVar : nat -> logterm
| LAbs : logterm -> logterm
......@@ -100,14 +136,20 @@ Inductive logterm : Type :=
with logtermlist : Type :=
| LLVar : nat -> logtermlist
| LLList : list logterm -> logtermlist.
(* This embeds untyped terms in the logic. *)
Fixpoint term_to_logterm (t : term) : logterm :=
match t with
| Var m => LVar m
| Abs t => LAbs (term_to_logterm t)
| App t u => LApp (term_to_logterm t) (LLList [term_to_logterm u])
end.
(* This embeds lists of untyped terms
in the logic. *)
Fixpoint termlist_to_logtermlist (p : list term) : logtermlist :=
LLList (map term_to_logterm p).
(* "logterm_liftt n t" increments all the
term meta-variables of t of with
index >= n. *)
Fixpoint logterm_liftt (n : nat) (t : logterm) : logterm :=
match t with
| LVar m => LVar m
......@@ -121,6 +163,9 @@ with logtermlist_liftt (n : nat) (p : logtermlist) : logtermlist :=
| LLVar m => LLVar m
| LLList p => LLList (map (logterm_liftt n) p)
end.
(* "logterm_liftp n t" increments all the
stack meta-variables of t with
index >= n. *)
Fixpoint logterm_liftp (n : nat) (t : logterm) : logterm :=
match t with
| LVar m => LVar m
......@@ -134,6 +179,9 @@ with logtermlist_liftp (n : nat) (p : logtermlist) : logtermlist :=
| LLVar m => if m <? n then LLVar m else LLVar (S m)
| LLList p => LLList (map (logterm_liftp n) p)
end.
(* "logterm_substt n t u" is t[u/n].
Term meta-variables of t with
index >= n are decremented. *)
Fixpoint logterm_substt (n : nat) (t : logterm) (u : logterm) : logterm :=
match t with
| LVar n => LVar n
......@@ -152,6 +200,9 @@ with logtermlist_substt (n : nat) (p : logtermlist) (u : logterm) : logtermlist
| LLVar m => LLVar m
| LLList p => LLList (map (fun t => logterm_substt n t u) p)
end.
(* "logterm_substp n t p" is t[p/n].
Stack meta-variables of t with
index >= n are decremented. *)
Fixpoint logterm_substp (n : nat) (t : logterm) (p : logtermlist) : logterm :=
match t with
| LVar n => LVar n
......@@ -170,6 +221,8 @@ with logtermlist_substp (n : nat) (q : logtermlist) (p : logtermlist) : logterml
end
| LLList q => LLList (map (fun t => logterm_substp n t p) q)
end.
(* "logterm_to_term t" maps a term of
the logic into an untyped lambda-term. *)
Fixpoint logterm_to_term (t : logterm) : term :=
match t with
| LVar n => Var n
......@@ -187,6 +240,10 @@ Fixpoint logterm_to_term (t : logterm) : term :=
end
end.
(* Formulas of the logic.
FIn t n is the atom "t∈X"
where X is the 2nd-order variable
with de Bruijn index 0. *)
Inductive form : Type :=
| FIn : logterm -> nat -> form
| FBool : form
......@@ -195,6 +252,29 @@ Inductive form : Type :=
| FForallt : form -> form
| FForallp : form -> form
| FForall2 : form -> form.
(*Fixpoint form_liftt (n : nat) (f : form) : form :=
match f with
| FIn t m => FIn (logterm_liftt n t) m
| FBool => FBool
| FImp f g => FImp (form_liftt n f) (form_liftt n g)
| FConj f g => FConj (form_liftt n f) (form_liftt n g)
| FForallt f => FForallt (form_liftt (S n) f)
| FForallp f => FForallp (form_liftt n f)
| FForall2 f => FForall2 (form_liftt n f)
end.
Fixpoint form_liftp (n : nat) (f : form) : form :=
match f with
| FIn t m => FIn (logterm_liftp n t) m
| FBool => FBool
| FImp f g => FImp (form_liftp n f) (form_liftp n g)
| FConj f g => FConj (form_liftp n f) (form_liftp n g)
| FForallt f => FForallt (form_liftp n f)
| FForallp f => FForallp (form_liftp (S n) f)
| FForall2 f => FForall2 (form_liftp n f)
end.*)
(* "form_substt n f t" is f[t/n].
Term meta-variables of f with
index >= n are decremented. *)
Fixpoint form_substt (n : nat) (f : form) (t : logterm) : form :=
match f with
| FIn u m => FIn (logterm_substt n u t) m
......@@ -205,6 +285,9 @@ Fixpoint form_substt (n : nat) (f : form) (t : logterm) : form :=
| FForallp f => FForallp (form_substt n f t)
| FForall2 f => FForall2 (form_substt n f t)
end.
(* "form_substp n f p" is f[p/n].
Stack meta-variables of f with
index >= n are decremented. *)
Fixpoint form_substp (n : nat) (f : form) (p : logtermlist) : form :=
match f with
| FIn t m => FIn (logterm_substp n t p) m
......@@ -215,26 +298,9 @@ Fixpoint form_substp (n : nat) (f : form) (p : logtermlist) : form :=
| FForallp f => FForallp (form_substp (S n) f (logtermlist_liftp 0 p))
| FForall2 f => FForall2 (form_substp n f p)
end.
Fixpoint form_liftt (n : nat) (f : form) : form :=
match f with
| FIn t m => FIn (logterm_liftt n t) m
| FBool => FBool
| FImp f g => FImp (form_liftt n f) (form_liftt n g)
| FConj f g => FConj (form_liftt n f) (form_liftt n g)
| FForallt f => FForallt (form_liftt (S n) f)
| FForallp f => FForallp (form_liftt n f)
| FForall2 f => FForall2 (form_liftt n f)
end.
Fixpoint form_liftp (n : nat) (f : form) : form :=
match f with
| FIn t m => FIn (logterm_liftp n t) m
| FBool => FBool
| FImp f g => FImp (form_liftp n f) (form_liftp n g)
| FConj f g => FConj (form_liftp n f) (form_liftp n g)
| FForallt f => FForallt (form_liftp n f)
| FForallp f => FForallp (form_liftp (S n) f)
| FForall2 f => FForall2 (form_liftp n f)
end.
(* "form_lift2 n f" increments all the
2nd-order variables of f with
index >= n. *)
Fixpoint form_lift2 (n : nat) (f : form) : form :=
match f with
| FIn t m => if m <? n then FIn t m else FIn t (S m)
......@@ -245,6 +311,9 @@ Fixpoint form_lift2 (n : nat) (f : form) : form :=
| FForallp f => FForallp (form_lift2 n f)
| FForall2 f => FForall2 (form_lift2 (S n) f)
end.
(* "form_subst2 n f g" is f[g/n].
2nd-order variables of f with
index >= n are decremented. *)
Fixpoint form_subst2 (n : nat) (f : form) (g : form) : form :=
match f with
| FIn t m =>
......@@ -261,8 +330,13 @@ Fixpoint form_subst2 (n : nat) (f : form) (g : form) : form :=
| FForall2 f => FForall2 (form_subst2 (S n) f (form_lift2 0 g))
end.
(* This is the skeleton of the "norm" formula.
The formula itself is M ¬∀i M̷↓i. *)
Definition norm : form := FImp (FImp FBool FBool) FBool.
(* This is the formula RedCand(X)
(∀π (̲0π X) t (t X t))
t u ∀π (t[u/0]π X (λ.t)uπ X)) *)
Definition redcand : form :=
FConj
(FConj
......@@ -276,6 +350,8 @@ Definition redcand : form :=
)
))).
(* "rc T" is the formula RC_T with
one free term meta-variable. *)
Fixpoint rc (T : type) : form :=
match T with
| TVar m => FIn (LMetavar 0) m
......@@ -283,6 +359,8 @@ Fixpoint rc (T : type) : form :=
| TForall T => FForall2 (FImp redcand (rc T))
end.
(* "form_to_type f" is the type of
realizers of f. *)
Fixpoint form_to_type (f : form) : Type :=
match f with
| FIn t m => nat
......@@ -440,6 +518,8 @@ rewrite form_to_type_substt.
reflexivity.
Qed.*)
(* This is the measure decreasing
in the definition of repl. *)
Fixpoint form_measure (f : form) : nat :=
match f with
| FIn t m => 0
......@@ -485,6 +565,8 @@ rewrite IHf.
reflexivity.
Qed.
(* "repl n f g h" is the realizer of:
t (g(t) h(t)) g[f/n] h[f/n] *)
Program Fixpoint repl (n : nat) (f : form) {g h : form} (real : form_to_type (FForallt (FConj (FImp g h) (FImp h g)))) {measure (form_measure f)}
: form_to_type (FConj (FImp (form_subst2 n f g) (form_subst2 n f h)) (FImp (form_subst2 n f h) (form_subst2 n f g))) :=
match f with
......@@ -647,6 +729,7 @@ rewrite form_to_type_lift2.
reflexivity.
Qed.
(* "dne f" is the realizer of ¬¬f f *)
Fixpoint dne (f : form) : ((form_to_type f -> nat) -> nat) -> form_to_type f :=
match f with
| FIn t n => fun x => x id
......@@ -657,8 +740,13 @@ Fixpoint dne (f : form) : ((form_to_type f -> nat) -> nat) -> form_to_type f :=
| FForallp f => fun x y => dne f (fun z => x (fun u => z (u y)))
| FForall2 f => dne f
end.
(* "dne f" is the realizer of f *)
Definition exf (f : form) : nat -> form_to_type f := fun x => dne f (fun y => x).
(* This is the bar recursion operator.
We don't want to prove its termination
in Coq so we write it as a parameter
and specify its extracted form. *)
Parameter brec : forall A : Type, ((A -> nat) -> A) -> ((term -> A) -> nat) -> (term -> option A) -> nat.
Extract Constant brec => "
fun f g ->
......@@ -666,19 +754,28 @@ Extract Constant brec => "
g (fun t -> match s t with Some a -> a | None -> f (fun a -> brec_aux (fun u -> if term_equal u t then Some a else s u))) in
brec_aux
".
(* "equiv f" is ̲0 X f *)
Definition equiv (f : form) : form := FConj (FImp (FIn (LVar 0) 0) f) (FImp f (FIn (LVar 0) 0)).
(* "comp f" is the realizer of
the comprehnsion scheme:
¬∀X¬∀t(t X f(t)) *)
Definition comp (f : form) : form_to_type (FImp (FForall2 (FImp (FForallt (equiv f)) FBool)) FBool) :=
fun y => brec (form_to_type (equiv f)) (fun x => exf (equiv f) (x (exf f, fun u => x (fun v => u, fun v => 0)))) y (fun t => None).
Program Definition elim (f : form) (g : form) : form_to_type (FImp (FForall2 f) (form_subst2 0 f g)) :=
fun x => dne (form_subst2 0 f g) (fun y => comp g (fun z => y (fst (repl 0 f z) (rew [id] _ in x)))).
fun x => dne (form_subst2 0 f g) (fun y => comp g (fun (z : form_to_type (FForallt (equiv g))) => y (fst (repl 0 f z) (rew [id] _ in x)))).
Next Obligation.
rewrite form_to_type_subst2_fin.
reflexivity.
Qed.
(* "normrc" is the realizer
of RedCand ({ M | M }) *)
Definition normrc : form_to_type (form_subst2 0 redcand norm) :=
(fun p x => x 0, fun t x => x, fun t u p x y => x (fun i => y (S i))).
(* "isrc tcontext T" is the realizer
of RedCand(X_1) ... RedCand(X_n) RedCand(T)
where X_1...X_n is tcontext *)
Program Fixpoint isrc (tcontext : list (form_to_type redcand)) (T : type) : form_to_type (form_subst2 0 redcand (rc T)) :=
match T return form_to_type (form_subst2 0 redcand (rc T)) with
| TVar m => rew [id] _ in nth m tcontext (exf redcand 0)
......@@ -736,6 +833,13 @@ rewrite form_to_type_substt.
reflexivity.
Qed.
(* "adeq context tcontext t H" (where
context is a list of (u, U, Hu) with
Hu a realizer of u RC_U, tcontext is
a list of realizers of RedCand(X_i) and
H is a proof that t is well-typed
in context context) is the realizer of
RC_{(type_get context t)[U_1...U_n/0]}(t[u_1...u_n/0]) *)
Program Fixpoint adeq (context : list (term * {T : type & form_to_type (rc T)})) (tcontext : list (form_to_type redcand)) (t : fterm) (H : type_correct (map (fun a => projT1 (snd a)) context) t) : form_to_type (rc (type_get (map (fun a => projT1 (snd a)) context) t)) :=
match t with
| FVar n => rew [id] _ in projT2 (snd (nth n context (Var 0, existT _ (TVar 0) 0)))
......@@ -895,8 +999,13 @@ rewrite form_to_type_lift2.
reflexivity.
Qed.
(* "bound t H" (where H is a proof
that t is well-typed in the empty
context) computes a bound a bound
on the number of reduction steps
of t *)
Program Definition bound (t : fterm) (H : type_correct [] t) : nat :=
snd (fst (isrc [] (type_get [] t))) (fterm_to_term t) (adeq [] [] t _) id.
snd (fst (isrc [] (type_get [] t))) (fterm_to_term t) (adeq [] [] t H) id.
Next Obligation.
Admitted.
......
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