proof for cAnd

TimothyEarley · Nov 3, 2024 · cbcd091 · cbcd091
1 parent a5a3b58
commit cbcd091
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 2 deletions.
diff --git a/src/proof/Henkin.ard b/src/proof/Henkin.ard
@@ -40,6 +40,6 @@
       : Prf' T (cAnd f g) <-> (\Sigma (Prf' T f) (Prf' T g)) =>
       (
         \lam p => {?},
-        \lam _x => {?}
+        \lam (inP prf1, inP prf2) => inP (and prf1 prf2)
       )
   }
diff --git a/src/proof/PrfCorrect.ard b/src/proof/PrfCorrect.ard
@@ -61,6 +61,7 @@
           (\new Array (Universe {I.structure}) (relArity r) (\lam i => evaluate I (args' i)))
         => ext (ext (\lam j => prfs' j I m))
       \in rewrite h prf'
+  | cAnd a toShow, and prf1 prf2 => \lam I m => (prfCorrectness prf1 I m, prfCorrectness prf2 I m)
   \where {
     -- to work around termintation checking
 

diff --git a/src/proof/PrfFinite.ard b/src/proof/PrfFinite.ard
@@ -124,3 +124,13 @@
           (\lam i => prfWeaken (prfs' i).4 (\lam h => byLeft $ SubsetHelper.subsetFiniteUnion' {_} {S} (i, idp) h))
           (prfWeaken prf'.4 (byRight __))
     )
+  | cAnd a toShow, and prf1 prf2 =>
+    \let
+      | h1 => prfFinite prf1
+      | h2 => prfFinite prf2
+    \in (
+      h1.1 ∪ h2.1,
+      SubsetHelper.subsetUnion h1.2 h2.2,
+      FinSets.FinUnion h1.3 h2.3,
+      and (prfWeaken h1.4 (byLeft __)) (prfWeaken h2.4 (byRight __))
+    )
diff --git a/src/proof/PrfWeaken.ard b/src/proof/PrfWeaken.ard
@@ -23,4 +23,5 @@
   | equal a b, symm prf => symm (prfWeaken prf sub)
   | equal a b, trans prf1 prf2 => trans (prfWeaken prf1 sub) (prfWeaken prf2 sub)
   | equal a b, fcong prfs pa pb => fcong (\lam i => prfWeaken (prfs i) sub) pa pb
-  | atomic r terms, rcong prfs prf => rcong (\lam i => prfWeaken (prfs i) sub) (prfWeaken prf sub)
+  | atomic r terms, rcong prfs prf => rcong (\lam i => prfWeaken (prfs i) sub) (prfWeaken prf sub)
+  | cAnd a b, and prf1 prf2 => and (prfWeaken prf1 sub) (prfWeaken prf2 sub)
diff --git a/src/proof/Proof.ard b/src/proof/Proof.ard
@@ -36,6 +36,8 @@
             (pa : a = apply f args) (pb : b = apply f args')
   }
 
+  | cAnd a b => and (Prf axioms a) (Prf axioms b)
+
 
   -- TODO what is this rule?
   -- ¬(¬f -> g) = ¬(f ∨ g) = ¬f ∧ ¬g