chore: apply comments

Author: RatCornu

theories/Base.v

@@ -1,5 +1,5 @@
 (**
-  This project contains formalisation in Coq of the 2.7.1 MPRI course:
+  This project contains formalisation in Rocq of the 2.7.1 MPRI course:
   Foundations of proof systems.
 *)
 

theories/FirstOrderLogic/Deduction.v

@@ -83,14 +83,14 @@ Inductive Derivable: list formula -> formula -> Type :=
 
 (**
   This lemma states that if Γ ⊢ φ in our representation of the first-order
-  logic, then it also holds in Coq [Prop].
+  logic, then it also holds in Rocq [Prop].
 *)
 Lemma derivable_correctness (fcts: nat -> list nat -> nat) (preds: nat -> list nat -> Prop)
     (gamma: list formula) (phi: formula):
   Derivable gamma phi ->
-    forall (sigma: list nat),
-      (forall (idx: nat), formula_eval fcts preds sigma (nth idx gamma FTop)) ->
-        formula_eval fcts preds sigma phi.
+    forall (σ: list nat),
+      (forall (idx: nat), formula_eval fcts preds σ (nth idx gamma FTop)) ->
+        formula_eval fcts preds σ phi.
 Proof.
   induction 1 as
     [ | | ? ? _ IHind |
@@ -99,7 +99,7 @@ Proof.
       (* RDisj *) ? ? ? _ IHind | ? ? ? _ IHind | ? ? ? ? _ IHind1 _ IHind2 _ IHind3 |
       (* RForAll *) ? ? _ IHind | ? ? phi _ IHind |
       (* RExists *) ? ? phi _ IHind | ? ? ? _ IHind1 _ IHind2 ];
-    simpl in *; intros sigma IHtree; intros.
+    simpl in *; intros σ IHtree; intros.
 
   (* RAxiom *)
   - apply IHtree.
@@ -109,11 +109,11 @@ Proof.
 
   (* RBot_e *)
   - exfalso.
-    apply (IHind sigma).
+    apply (IHind σ).
     apply IHtree.
 
   (* RImp_i *)
-  - apply (IHind sigma).
+  - apply (IHind σ).
     intros [|].
     + assumption.
     + apply IHtree.
@@ -150,7 +150,7 @@ Proof.
     apply IHtree.
 
   (* RDisj_e *)
-  - destruct (IHind1 sigma IHtree).
+  - destruct (IHind1 σ IHtree).
     + apply IHind2.
       intros [|]; [ assumption | apply IHtree ].
     + apply IHind3.
@@ -159,30 +159,30 @@ Proof.
   (* RForAll_i *)
   - apply IHind; intros n.
     rewrite formula_lift_nth.
-    apply formula_eval_S with (sigma := nil).
+    apply formula_eval_S with (σ := nil).
     apply IHtree.
 
   (* RForAll_e *)
   - rewrite <- (term_lift_0 phi 0).
-    apply formula_eval_subst_lift with (sigma := nil).
+    apply formula_eval_subst_lift with (σ := nil).
     apply IHind.
     apply IHtree.
 
   (* RExists_i *)
-  - exists (term_eval fcts sigma phi).
-    apply formula_eval_subst_lift with (sigma := nil).
+  - exists (term_eval fcts σ phi).
+    apply formula_eval_subst_lift with (σ := nil).
     rewrite term_lift_0.
     apply IHind.
     apply IHtree.
 
   (* RExists_e *)
-  - destruct (IHind1 sigma IHtree) as [ n ? ].
-    apply formula_eval_S with (sigma := nil) (idx := n).
+  - destruct (IHind1 σ IHtree) as [ n ? ].
+    apply formula_eval_S with (σ := nil) (idx := n).
     apply IHind2.
 
     intros [|]; [ assumption |].
     rewrite formula_lift_nth.
-    apply formula_eval_S with (sigma := nil).
+    apply formula_eval_S with (σ := nil).
     apply IHtree.
 Qed.
 

theories/FirstOrderLogic/Definitions.v

@@ -1,7 +1,7 @@
 (**
   This section defines the first-order logic with some properties on derivations.
 
-  This file contains terms, formulas, and an evaluation of formulas into Coq [Prop].
+  This file contains terms, formulas, and an evaluation of formulas into Rocq [Prop].
 *)
 
 From FormArith Require Export Base.
@@ -28,7 +28,7 @@ Inductive term :=
   | TApp : nat -> list term -> term.
 
 (**
-  As Coq cannot induce an induction principle with induction hypothesis for
+  As Rocq cannot induce an induction principle with induction hypothesis for
   indirect terms, for example the ones in lists, here is a better induction
   principle that includes [Forall P terms] in the [TApp] case.
 *)
@@ -91,38 +91,38 @@ Inductive formula :=
 
 (**
   Auxiliary function of [formula_eval] that evaluates a term [t] in the
-  environment [sigma] with the environment of functions [fcts].
+  environment [σ] with the environment of functions [fcts].
 *)
-Fixpoint term_eval (fcts: nat -> list nat -> nat) (sigma: list nat) (t: term): nat :=
+Fixpoint term_eval (fcts: nat -> list nat -> nat) (σ: list nat) (t: term): nat :=
   match t with
-  | TVar idx => nth idx sigma 0
-  | TApp fct_idx terms => fcts fct_idx (map (term_eval fcts sigma) terms)
+  | TVar idx => nth idx σ 0
+  | TApp fct_idx terms => fcts fct_idx (map (term_eval fcts σ) terms)
   end.
 
 (**
-  Evaluates a formula into a Coq [Prop].
+  Evaluates a formula into a Rocq [Prop].
 
   Here, [fcts] is the environment of functions that are used in [term]
   definition: a function is denoted by a natural number, and maps a list of
   [nat] into a [nat].
 
   With the same idea, [preds] is the environment of predicates that are the
   atomic formulas: a predicate is denoted by a natural number, and maps a list
-  of terms to a Coq [Prop].
+  of terms to a Rocq [Prop].
 *)
 Fixpoint formula_eval
     (fcts: nat -> list nat -> nat) (preds : nat -> list nat -> Prop)
-    (sigma: list nat) (phi: formula): Prop :=
+    (σ: list nat) (phi: formula): Prop :=
   match phi with
-  | FAtom pred_idx terms => preds pred_idx (map (term_eval fcts sigma) terms)
+  | FAtom pred_idx terms => preds pred_idx (map (term_eval fcts σ) terms)
 
-  | FConj phi phi' => (formula_eval fcts preds sigma phi) /\ (formula_eval fcts preds sigma phi')
-  | FDisj phi phi' => (formula_eval fcts preds sigma phi) \/ (formula_eval fcts preds sigma phi')
-  | FImp phi phi' => (formula_eval fcts preds sigma phi) -> (formula_eval fcts preds sigma phi')
+  | FConj phi phi' => (formula_eval fcts preds σ phi) /\ (formula_eval fcts preds σ phi')
+  | FDisj phi phi' => (formula_eval fcts preds σ phi) \/ (formula_eval fcts preds σ phi')
+  | FImp phi phi' => (formula_eval fcts preds σ phi) -> (formula_eval fcts preds σ phi')
 
   | FBot => False
   | FTop => True
 
-  | FForAll phi => forall x, formula_eval fcts preds (x :: sigma) phi
-  | FExists phi => exists x, formula_eval fcts preds (x :: sigma) phi
+  | FForAll phi => forall x, formula_eval fcts preds (x :: σ) phi
+  | FExists phi => exists x, formula_eval fcts preds (x :: σ) phi
   end.

theories/FirstOrderLogic/Lifts.v

@@ -351,12 +351,12 @@ Qed.
 
 (** *** Evaluations *)
 
-Lemma term_eval_lift_n (fcts: nat -> list nat -> nat) (sigma sigma': list nat) (idx: nat) (t: term):
-  term_eval fcts (sigma ++ (idx :: sigma')) (term_lift (length sigma) 1 t) =
-    term_eval fcts (sigma ++ sigma') t.
+Lemma term_eval_lift_n (fcts: nat -> list nat -> nat) (σ σ': list nat) (idx: nat) (t: term):
+  term_eval fcts (σ ++ (idx :: σ')) (term_lift (length σ) 1 t) =
+    term_eval fcts (σ ++ σ') t.
 Proof.
   induction t as [ idx' | ? terms IHterms ]; simpl.
-  - destruct (PeanoNat.Nat.ltb_spec idx' (length sigma)); simpl.
+  - destruct (PeanoNat.Nat.ltb_spec idx' (length σ)); simpl.
     + rewrite !app_nth1 by assumption.
       reflexivity.
 
@@ -365,26 +365,26 @@ Proof.
       rewrite PeanoNat.Nat.sub_succ_l by assumption.
       simpl; lia.
 
-  - replace (map _ _) with (map (term_eval fcts (sigma ++ sigma')) terms); [ reflexivity |].
+  - replace (map _ _) with (map (term_eval fcts (σ ++ σ')) terms); [ reflexivity |].
     solve_TApp_case terms IHterms.
 Qed.
 
-Lemma term_eval_lift_0 (fcts: nat -> list nat -> nat) (sigma sigma': list nat) (t: term):
-  term_eval fcts sigma t = term_eval fcts (sigma' ++ sigma) (term_lift 0 (length sigma') t).
+Lemma term_eval_lift_0 (fcts: nat -> list nat -> nat) (σ σ': list nat) (t: term):
+  term_eval fcts σ t = term_eval fcts (σ' ++ σ) (term_lift 0 (length σ') t).
 Proof.
   induction t as [ idx | ? terms IHterms ]; simpl.
   - rewrite app_nth2 by lia.
     replace (idx + _ - _) with idx by lia.
     reflexivity.
 
-  - replace (map _ (map _ _)) with (map (term_eval fcts sigma) terms); [ reflexivity |].
+  - replace (map _ (map _ _)) with (map (term_eval fcts σ) terms); [ reflexivity |].
     solve_TApp_case terms IHterms.
 Qed.
 
 Lemma term_eval_lift_n_iter (fcts: nat -> list nat -> nat)
-    (sigma sigma': list nat) (idx: nat) (terms: list term):
-  map (term_eval fcts (sigma ++ idx :: sigma')) (map (term_lift (length sigma) 1) terms) =
-    map (term_eval fcts (sigma ++ sigma')) terms.
+    (σ σ': list nat) (idx: nat) (terms: list term):
+  map (term_eval fcts (σ ++ idx :: σ')) (map (term_lift (length σ) 1) terms) =
+    map (term_eval fcts (σ ++ σ')) terms.
 Proof.
   induction terms; simpl.
   { reflexivity. }
@@ -393,20 +393,20 @@ Proof.
   f_equal; assumption.
 Qed.
 
-Lemma term_eval_subst_lift (fcts: nat -> list nat -> nat) (sigma sigma': list nat) (t t': term):
-  term_eval fcts (sigma ++ sigma') (term_subst (length sigma) (term_lift 0 (length sigma) t') t)
-    = term_eval fcts (sigma ++ (term_eval fcts sigma' t') :: sigma') t.
+Lemma term_eval_subst_lift (fcts: nat -> list nat -> nat) (σ σ': list nat) (t t': term):
+  term_eval fcts (σ ++ σ') (term_subst (length σ) (term_lift 0 (length σ) t') t)
+    = term_eval fcts (σ ++ (term_eval fcts σ' t') :: σ') t.
 Proof.
   induction t as [ idx | ? terms IHterms ]; simpl.
   2: { f_equal; solve_TApp_case terms IHterms. }
 
-  destruct (PeanoNat.Nat.eqb_spec (length sigma) idx) as [ Heq |]; simpl.
+  destruct (PeanoNat.Nat.eqb_spec (length σ) idx) as [ Heq |]; simpl.
   { rewrite <- Heq.
     rewrite nth_middle.
     rewrite <- term_eval_lift_0.
     reflexivity. }
 
-  destruct (PeanoNat.Nat.ltb_spec (length sigma) idx) as [ Heq |]; simpl.
+  destruct (PeanoNat.Nat.ltb_spec (length σ) idx) as [ Heq |]; simpl.
   { destruct idx; [ lia |]; simpl.
     rewrite PeanoNat.Nat.sub_0_r.
     rewrite !app_nth2; [| lia.. ].
@@ -481,14 +481,14 @@ Proof.
 Qed.
 
 Lemma formula_eval_S (fcts: nat -> list nat -> nat) (preds: nat -> list nat -> Prop)
-    (phi: formula) (sigma sigma': list nat) (idx: nat):
-  formula_eval fcts preds (sigma ++ idx :: sigma') (formula_lift (length sigma) 1 phi) <->
-    formula_eval fcts preds (sigma ++ sigma') phi.
+    (phi: formula) (σ σ': list nat) (idx: nat):
+  formula_eval fcts preds (σ ++ idx :: σ') (formula_lift (length σ) 1 phi) <->
+    formula_eval fcts preds (σ ++ σ') phi.
 Proof.
-  generalize sigma.
+  generalize σ.
 
   induction phi as [ | ? IHphi1 ? IHphi2 | ? IHphi1 ? IHphi2 | ? IHphi1 ? IHphi2 | | | ? IHphi | ? IHphi ];
-    simpl; intros sigma''.
+    simpl; intros σ''.
 
   (* FAtom *)
   - rewrite term_eval_lift_n_iter.
@@ -517,28 +517,28 @@ Proof.
 
   (* FForAll *)
   - split; intros Hphi x.
-    all: apply (IHphi (x :: sigma'')).
+    all: apply (IHphi (x :: σ'')).
     all: apply Hphi.
 
   (* FExists *)
   - split; intros [x Heval].
     all: exists x.
-    all: apply (IHphi (x :: sigma'')).
+    all: apply (IHphi (x :: σ'')).
     all: apply Heval.
 Qed.
 
 Lemma formula_eval_subst_lift (fcts: nat -> list nat -> nat) (preds: nat -> list nat -> Prop)
-    (phi: formula) (sigma sigma': list nat) (t: term):
-  formula_eval fcts preds (sigma ++ sigma') (formula_subst (length sigma) (term_lift 0 (length sigma) t) phi)
-    <-> formula_eval fcts preds (sigma ++ (term_eval fcts sigma' t) :: sigma') phi.
+    (phi: formula) (σ σ': list nat) (t: term):
+  formula_eval fcts preds (σ ++ σ') (formula_subst (length σ) (term_lift 0 (length σ) t) phi)
+    <-> formula_eval fcts preds (σ ++ (term_eval fcts σ' t) :: σ') phi.
 Proof.
-  generalize sigma.
+  generalize σ.
 
   induction phi as [ ? terms | ? IHphi1 ? IHphi2 | ? IHphi1 ? IHphi2 | ? IHphi1 ? IHphi2 | | | ? IHphi | ? IHphi ];
-    simpl; intros sigma''.
+    simpl; intros σ''.
 
   (* FAtom *)
-  - replace (map _ _) with (map (term_eval fcts (sigma'' ++ term_eval fcts sigma' t :: sigma')) terms); [ reflexivity |].
+  - replace (map _ _) with (map (term_eval fcts (σ'' ++ term_eval fcts σ' t :: σ')) terms); [ reflexivity |].
     induction terms as [| ? ? IHterms ]; simpl.
     { reflexivity. }
 
@@ -570,28 +570,28 @@ Proof.
 
   (* FForAll *)
   - split; intros Hphi x; simpl.
-    + apply (IHphi (x :: sigma'')).
-      replace (term_lift _ _ _) with (term_lift 0 1 (term_lift 0 (length sigma'') t)).
+    + apply (IHphi (x :: σ'')).
+      replace (term_lift _ _ _) with (term_lift 0 1 (term_lift 0 (length σ'') t)).
       { apply Hphi. }
 
       rewrite term_lift_0_lift_0.
       reflexivity.
 
-    + specialize (IHphi (x :: sigma'')).
+    + specialize (IHphi (x :: σ'')).
       rewrite term_lift_0_lift_0.
       apply IHphi.
       apply Hphi.
 
   (* FExists *)
   - split; intros [x Hphi]; exists x; simpl.
-    + apply (IHphi (x :: sigma'')).
-      replace (term_lift _ _ _) with (term_lift 0 1 (term_lift 0 (length sigma'') t)).
+    + apply (IHphi (x :: σ'')).
+      replace (term_lift _ _ _) with (term_lift 0 1 (term_lift 0 (length σ'') t)).
       { apply Hphi. }
 
       rewrite term_lift_0_lift_0.
       reflexivity.
 
-    + specialize (IHphi (x :: sigma'')).
+    + specialize (IHphi (x :: σ'')).
       rewrite term_lift_0_lift_0.
       apply IHphi.
       apply Hphi.

theories/SimplyTypedLambdaCalculus/ChurchRosser.v

@@ -10,9 +10,8 @@ From FormArith.SimplyTypedLambdaCalculus Require Import Term.
 
 (** ** Definitions *)
 
-(** *** 
-  Local confluence
-  
+(** *** Local confluence
+
   A rewrite rule → is said to be locally confluent if:
   ∀ t u v, t → u ∧ t → v ⇒ ∃ w, u → w ∧ v → w.
 *)
@@ -22,8 +21,7 @@ Definition local_confluence (P: term -> term -> Prop): Prop :=
     P t v ->
     exists (w : term), P u w /\ P v w.
 
-(** ***
-  Church-Rosser propery
+(** *** Church-Rosser propery
 
   It is defined as the local confluence for the reflexive and transitive
   closure of the rewrite rule.

theories/SimplyTypedLambdaCalculus/StrongNormalisation.v

@@ -14,7 +14,7 @@ From FormArith.SimplyTypedLambdaCalculus Require Import Term Typing.
   Intuitively, a [term] is strongly normalising if all of its successor for the
   β-reduction are also strongly normalising.
 
-  This definition is equivalent but easier to deal with in Coq than the usual
+  This definition is equivalent but easier to deal with in Rocq than the usual
   definition "There is no infinite path starting with this term".
 *)
 Inductive SN: term -> Prop :=