Finished adding conjunction.

PropositionalKripke.agda

@@ -64,9 +64,9 @@ module PropositionalKripke (PV : Set) where
     ⟦ zero (next∈ h) ⟧ wΓ = ⟦ zero h ⟧ (proj₂ wΓ)
     ⟦ lam p ⟧ = λ wΓ w≤ w'A → ⟦ p ⟧ ⟨ w'A , mon⊩ᶜ w≤ wΓ ⟩
     ⟦ app p p₁ ⟧ wΓ = ⟦ p ⟧ wΓ refl≤ (⟦ p₁ ⟧ wΓ)
-    ⟦ andi p₁ p₂ ⟧ = {!!}
+    ⟦ andi p₁ p₂ ⟧ wΓ = ⟨ (⟦ p₁ ⟧ wΓ) , (⟦ p₂ ⟧ wΓ) ⟩
-    ⟦ ande₁ p ⟧ = {!!}
+    ⟦ ande₁ p ⟧ wΓ = proj₁ $ ⟦ p ⟧ wΓ
-    ⟦ ande₂ p ⟧ = {!!}
+    ⟦ ande₂ p ⟧ wΓ = proj₂ $ ⟦ p ⟧ wΓ
 
 
 
@@ -91,10 +91,10 @@ module PropositionalKripke (PV : Set) where
     ⊢→⊩ᶠ : {F : Form} → {Γ : Con} → Γ ⊢ F → Γ ⊩ᶠ F
     ⊢→⊩ᶠ {Var x} h = h
     ⊢→⊩ᶠ {F ⇒ F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (lam (app (halftran⊢⁺ (addhyp⊢⁺ (right∈* refl∈*) iq) h) (zero zero∈))) (⊩ᶠ→⊢ hF))
-    ⊢→⊩ᶠ {F ∧∧ G} h = {!!}
+    ⊢→⊩ᶠ {F ∧∧ G} h = ⟨ (⊢→⊩ᶠ {F} (ande₁ h)) , (⊢→⊩ᶠ {G} (ande₂ h)) ⟩
     ⊩ᶠ→⊢ {Var x} h = h
     ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁺ (right∈* refl∈*) refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} (zero zero∈))))
-    ⊩ᶠ→⊢ {F ∧∧ G} ⟨ hF , hG ⟩ = {!!}
+    ⊩ᶠ→⊢ {F ∧∧ G} ⟨ hF , hG ⟩ = andi (⊩ᶠ→⊢ {F} hF) (⊩ᶠ→⊢ {G} hG)
 
     -- Finally, we can deduce completeness of the Kripke model
     completeness : {F : Form} → [] ⊫ F → [] ⊢ F
@@ -124,10 +124,10 @@ module PropositionalKripke (PV : Set) where
   
     ⊢→⊩ᶠ {Var x} h = h
     ⊢→⊩ᶠ {F ⇒ F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (halftran⊢⁰⁺⁰ iq h) (⊩ᶠ→⊢ hF))
-    ⊢→⊩ᶠ {F ∧∧ G} h = ?
+    ⊢→⊩ᶠ {F ∧∧ G} h = ⟨ (⊢→⊩ᶠ {F} (ande₁ h)) , (⊢→⊩ᶠ {G} (ande₂ h)) ⟩
     ⊩ᶠ→⊢ {Var x} h = neu⁰ h
     ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁰⁺ (right∈* refl∈*) refl⊢⁰⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} (zero zero∈))))
-    ⊩ᶠ→⊢ {F ∧∧ G} h = {!!}
+    ⊩ᶠ→⊢ {F ∧∧ G} ⟨ hF , hG ⟩ =  andi (⊩ᶠ→⊢ {F} hF) (⊩ᶠ→⊢ {G} hG)
 
   module OtherProofs where
 

PropositionalKripkeGeneral.agda

@@ -4,7 +4,7 @@ module PropositionalKripkeGeneral (PV : Set) where
 
   open import ListUtil
   open import PropUtil
-  open import PropositionalLogic PV using (Form; Var; _⇒_; Con)
+  open import PropositionalLogic PV using (Form; Var; _⇒_; _∧∧_; Con)
 
   open import PropositionalKripke PV using (Kripke)
 
@@ -24,8 +24,11 @@ module PropositionalKripkeGeneral (PV : Set) where
       _⊢*_ : Con → Form → Prop
       zero : {Γ : Con} → {F : Form} → (F ∷ Γ) ⊢⁰ F
       app : {Γ : Con} → {F G : Form} → Γ ⊢⁰ (F ⇒ G) → Γ ⊢* F → Γ ⊢⁰ G
+      ande₁ : {Γ : Con} → {F G : Form} → Γ ⊢⁰ (F ∧∧ G) → Γ ⊢⁰ F
+      ande₂ : {Γ : Con} → {F G : Form} → Γ ⊢⁰ (F ∧∧ G) → Γ ⊢⁰ G
       neu⁰ : {Γ : Con} → {x : PV} → Γ ⊢⁰ Var x → Γ ⊢* Var x
       lam : {Γ : Con} → {F G : Form} → (F ∷ Γ) ⊢* G → Γ ⊢* (F ⇒ G)
+      andi : {Γ : Con} → {F G : Form} → Γ ⊢* F → Γ ⊢* G → Γ ⊢* (F ∧∧ G)
 
   record NormalizationFrame : Set₁ where
     field
@@ -58,8 +61,11 @@ module PropositionalKripkeGeneral (PV : Set) where
   
     u {Var x} h = h
     u {F ⇒ F₁} h {Γ'} iq hF = u {F₁} (app {Γ'} {F} {F₁} (⊢tran iq h) (q hF))
+    u {F ∧∧ G} h = ⟨ (u {F} (ande₁ h)) , (u {G} (ande₂ h)) ⟩
+    
     q {Var x} h = neu⁰ h
     q {F ⇒ F₁} {Γ} h = lam (q (h (retro (Preorder.refl≤ o)) (u {F} {F ∷ Γ} zero)))
+    q {F ∧∧ G} ⟨ hF , hG ⟩ = andi (q {F} hF) (q {G} hG)
 
 
 
@@ -77,8 +83,11 @@ module PropositionalKripkeGeneral (PV : Set) where
       _⊢*_ = _⊢*_ ;
       zero = zero zero∈ ;
       app = app ;
+      ande₁ = ande₁;
+      ande₂ = ande₂ ;
       neu⁰ = neu⁰ ;
-      lam = lam
+      lam = lam;
+      andi = andi
       }
 
     BiggestNN : NormalAndNeutral
@@ -88,8 +97,11 @@ module PropositionalKripkeGeneral (PV : Set) where
       _⊢*_ = _⊢_ ;
       zero = zero zero∈ ;
       app = app ;
+      ande₁ = ande₁ ;
+      ande₂ = ande₂ ;
       neu⁰ = λ x → x ;
-      lam = lam
+      lam = lam ;
+      andi = andi
       }
 
     PO⊢⁺  = [ order {Con} _⊢⁺_  refl⊢⁺  tran⊢⁺  ]ᵒᵖ

PropositionalLogic.agda

@@ -109,9 +109,12 @@ module PropositionalLogic (PV : Set) where
     data _⊢⁰_ : Con → Form → Prop where
       zero :  A ∈ Γ → Γ ⊢⁰ A
       app : Γ ⊢⁰ (A ⇒ B) → Γ ⊢* A → Γ ⊢⁰ B
+      ande₁ : Γ ⊢⁰ A ∧∧ B → Γ ⊢⁰ A
+      ande₂ : Γ ⊢⁰ A ∧∧ B → Γ ⊢⁰ B
     data _⊢*_ : Con → Form → Prop where
       neu⁰ : Γ ⊢⁰ Var x → Γ ⊢* Var x
       lam : (A ∷ Γ) ⊢* B → Γ ⊢* (A ⇒ B)
+      andi : Γ ⊢* A → Γ ⊢* B → Γ ⊢* (A ∧∧ B)
   infix 5 _⊢⁰_
   infix 5 _⊢*_
 
@@ -120,16 +123,22 @@ module PropositionalLogic (PV : Set) where
   ⊢*→⊢ : Γ ⊢* F → Γ ⊢ F
   ⊢⁰→⊢ (zero h) = zero h
   ⊢⁰→⊢ (app h x) = app (⊢⁰→⊢ h) (⊢*→⊢ x)
+  ⊢⁰→⊢ (ande₁ h) = ande₁ (⊢⁰→⊢ h)
+  ⊢⁰→⊢ (ande₂ h) = ande₂ (⊢⁰→⊢ h)
   ⊢*→⊢ (neu⁰ x) = ⊢⁰→⊢ x
   ⊢*→⊢ (lam h) = lam (⊢*→⊢ h)
+  ⊢*→⊢ (andi h₁ h₂) = andi (⊢*→⊢ h₁) (⊢*→⊢ h₂)
 
   -- We can add hypotheses to a proof
   addhyp⊢⁰ : Γ ∈* Γ' → Γ ⊢⁰ A → Γ' ⊢⁰ A
   addhyp⊢* : Γ ∈* Γ' → Γ ⊢* A → Γ' ⊢* A
   addhyp⊢⁰ s (zero x) = zero (mon∈∈* x s)
   addhyp⊢⁰ s (app h h₁) = app (addhyp⊢⁰ s h) (addhyp⊢* s h₁)
+  addhyp⊢⁰ s (ande₁ h) = ande₁ (addhyp⊢⁰ s h)
+  addhyp⊢⁰ s (ande₂ h) = ande₂ (addhyp⊢⁰ s h)
   addhyp⊢* s (neu⁰ x) = neu⁰ (addhyp⊢⁰ s x)
   addhyp⊢* s (lam h) = lam (addhyp⊢* (both∈* s) h)
+  addhyp⊢* s (andi h₁ h₂) = andi (addhyp⊢* s h₁) (addhyp⊢* s h₂)
 
   -- Extension of ⊢⁰ to contexts
   -- i.e. there is a neutral proof for any element
@@ -163,9 +172,12 @@ module PropositionalLogic (PV : Set) where
   halftran⊢⁰⁺⁰ : {Γ Γ' : Con} → {F : Form} → Γ ⊢⁰⁺ Γ' → Γ' ⊢⁰ F → Γ ⊢⁰ F
   halftran⊢⁰⁺* h⁺ (neu⁰ x) = neu⁰ (halftran⊢⁰⁺⁰ h⁺ x)
   halftran⊢⁰⁺* h⁺ (lam h) = lam (halftran⊢⁰⁺* ⟨ zero zero∈ , addhyp⊢⁰⁺ (right∈* refl∈*) h⁺ ⟩ h)
+  halftran⊢⁰⁺* h⁺ (andi h₁ h₂) = andi (halftran⊢⁰⁺* h⁺ h₁) (halftran⊢⁰⁺* h⁺ h₂)
   halftran⊢⁰⁺⁰ {Γ' = x ∷ Γ'} h⁺ (zero zero∈) = proj₁ h⁺
   halftran⊢⁰⁺⁰ {Γ' = x ∷ Γ'} h⁺ (zero (next∈ h)) = halftran⊢⁰⁺⁰ (proj₂ h⁺) (zero h)
   halftran⊢⁰⁺⁰ h⁺ (app h h') = app (halftran⊢⁰⁺⁰ h⁺ h) (halftran⊢⁰⁺* h⁺ h')
+  halftran⊢⁰⁺⁰ h⁺ (ande₁ h) = ande₁ (halftran⊢⁰⁺⁰ h⁺ h)
+  halftran⊢⁰⁺⁰ h⁺ (ande₂ h) = ande₂ (halftran⊢⁰⁺⁰ h⁺ h)
 
   -- The relation is transitive
   tran⊢⁰⁺ : {Γ Γ' Γ'' : Con} → Γ ⊢⁰⁺ Γ' → Γ' ⊢⁰⁺ Γ'' → Γ ⊢⁰⁺ Γ''