From 54333a96257a228756ce85050f927851b1736142 Mon Sep 17 00:00:00 2001
From: Valentin Blot <24938579+vblot@users.noreply.github.com>
Date: Tue, 5 Dec 2017 17:21:02 +0100
Subject: [PATCH] Comments in the Coq file.

---
 Coq/f.v | 153 ++++++++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 131 insertions(+), 22 deletions(-)

diff --git a/Coq/f.v b/Coq/f.v
index e56ab83..1b11d30 100644
--- a/Coq/f.v
+++ b/Coq/f.v
@@ -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(X→X).x(∀X(X→X))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.
 
-- 
GitLab