From d3cf3cd0e6a54e7e4c20f04557dadb8c92ac4589 Mon Sep 17 00:00:00 2001
From: Mysaa <samy.avrillon@ens-lyon.fr>
Date: Fri, 2 Jun 2023 17:45:13 +0200
Subject: [PATCH] Fixed module names as file names had changed.

---
 InfinitaryFirstOrderKripke.agda        |  4 ++--
 InfinitaryFirstOrderKripkeGeneral.agda |  8 ++++----
 InfinitaryFirstOrderLogic.agda         |  2 +-
 Readme.agda                            | 24 +++++++++++++++++++++++-
 4 files changed, 30 insertions(+), 8 deletions(-)

diff --git a/InfinitaryFirstOrderKripke.agda b/InfinitaryFirstOrderKripke.agda
index 99997f1..ced5a87 100644
--- a/InfinitaryFirstOrderKripke.agda
+++ b/InfinitaryFirstOrderKripke.agda
@@ -2,11 +2,11 @@
 
 open import Agda.Builtin.Nat
 
-module PropositionalKripke (Term : Set) (R : Nat → Set) where
+module InfinitaryFirstOrderKripke (Term : Set) (R : Nat → Set) where
 
   open import ListUtil
   open import PropUtil
-  open import FirstOrderLogic Term R
+  open import InfinitaryFirstOrderLogic Term R
 
   private
     variable
diff --git a/InfinitaryFirstOrderKripkeGeneral.agda b/InfinitaryFirstOrderKripkeGeneral.agda
index 32f4e68..18a5d59 100644
--- a/InfinitaryFirstOrderKripkeGeneral.agda
+++ b/InfinitaryFirstOrderKripkeGeneral.agda
@@ -2,13 +2,13 @@
 
 open import Agda.Builtin.Nat hiding (zero)
 
-module PropositionalKripkeGeneral (Term : Set) (R : Nat → Set) where
+module InfinitaryFirstOrderKripkeGeneral (Term : Set) (R : Nat → Set) where
 
   open import ListUtil
   open import PropUtil
-  open import FirstOrderLogic Term R using (Form; Args; Rel; _⇒_; _∧∧_; ⊤⊤; ∀∀; Con)
+  open import InfinitaryFirstOrderLogic Term R using (Form; Args; Rel; _⇒_; _∧∧_; ⊤⊤; ∀∀; Con)
 
-  open import PropositionalKripke Term R using (Kripke)
+  open import InfinitaryFirstOrderKripke Term R using (Kripke)
 
   record Preorder (T : Set₀) : Set₁ where
     constructor order
@@ -78,7 +78,7 @@ module PropositionalKripkeGeneral (Term : Set) (R : Nat → Set) where
   module NormalizationTests where
 
     {- Now using our records -}
-    open import FirstOrderLogic Term R hiding (Form; _⇒_; Con)
+    open import InfinitaryFirstOrderLogic Term R hiding (Form; _⇒_; Con)
 
 
     ClassicNN : NormalAndNeutral
diff --git a/InfinitaryFirstOrderLogic.agda b/InfinitaryFirstOrderLogic.agda
index 288a91e..c32b5a9 100644
--- a/InfinitaryFirstOrderLogic.agda
+++ b/InfinitaryFirstOrderLogic.agda
@@ -2,7 +2,7 @@
 
 open import Agda.Builtin.Nat
 
-module FirstOrderLogic (Term : Set) (R : Nat → Set) where
+module InfinitaryFirstOrderLogic (Term : Set) (R : Nat → Set) where
 
   open import PropUtil
   open import ListUtil
diff --git a/Readme.agda b/Readme.agda
index e4360b8..5a5f249 100644
--- a/Readme.agda
+++ b/Readme.agda
@@ -1,4 +1,5 @@
 {-# OPTIONS --prop #-}
+
 module Readme where
 
 -- We will use String as propositional variables
@@ -115,7 +116,7 @@ module PierceDisproof where
   PierceNotProvable h = Pierce⊥w₁ (⟦ h ⟧ {w₁} tt)
   
   
-module CompletenessAndNormalization where
+module GeneralizationInPropositionalLogic where
 
   -- With Kripke models, we can even prove completeness
   -- Using the Universal Kripke Model
@@ -145,5 +146,26 @@ module CompletenessAndNormalization where
   u6 = NormalizationFrame.u NormalizationTests.Frame⊆
   q6 = NormalizationFrame.q NormalizationTests.Frame⊆
 
+module GeneralizationInInfinitaryFirstOrderLogic where
+
+  -- We also did implement infinitary first order logic
+  -- (i.e. ∀ is like an infinitary ∧)
+  -- The proofs works the same with only little modifications
+
+  open import InfinitaryFirstOrderKripkeGeneral String (λ n → String)
+
+  u1 = NormalizationFrame.u NormalizationTests.Frame⊢
+  q1 = NormalizationFrame.q NormalizationTests.Frame⊢
+  u2 = NormalizationFrame.u NormalizationTests.Frame⊢⁰
+  q2 = NormalizationFrame.q NormalizationTests.Frame⊢⁰
+  u3 = NormalizationFrame.u NormalizationTests.Frame∈*
+  q3 = NormalizationFrame.q NormalizationTests.Frame∈*
+  u4 = NormalizationFrame.u NormalizationTests.Frame⊂⁺
+  q4 = NormalizationFrame.q NormalizationTests.Frame⊂⁺
+  u5 = NormalizationFrame.u NormalizationTests.Frame⊂
+  q5 = NormalizationFrame.q NormalizationTests.Frame⊂
+  u6 = NormalizationFrame.u NormalizationTests.Frame⊆
+  q6 = NormalizationFrame.q NormalizationTests.Frame⊆
+