very wip: finite for all intro

src/decidable/FormulaCode.ard

@@ -14,18 +14,18 @@
   | code-encode => formulaCode-encode
   | code-decode => formulaCode-decode
   | decideCode => formulaCode-decide
-\where {
-  \func FormulaCode {_ : Language} {c : Context} (a b : Formula c) : \Prop \elim a, b
-    | equal a b, equal a1 b1 => \Sigma (a = a1) (b = b1)
-    | atomic r terms, atomic r1 terms1 => \Sigma (r = r1) (terms = {Array (Term c)} terms1)
-    | notH a, notH b => FormulaCode a b
-    | impH a a1, impH b b1 => \Sigma (FormulaCode a b) (FormulaCode a1 b1)
-    | cAnd a a1, cAnd b b1 => \Sigma (FormulaCode a b) (FormulaCode a1 b1)
-    | forAllH a, forAllH b => FormulaCode a b
-    | cExists a, cExists b => FormulaCode a b
-    | _, _ => Empty
+  \where {
+    \func FormulaCode {_ : Language} {c : Context} (a b : Formula c) : \Prop \elim a, b
+      | equal a b, equal a1 b1 => \Sigma (a = a1) (b = b1)
+      | atomic r terms, atomic r1 terms1 => \Sigma (r = r1) (terms = {Array (Term c)} terms1)
+      | notH a, notH b => FormulaCode a b
+      | impH a a1, impH b b1 => \Sigma (FormulaCode a b) (FormulaCode a1 b1)
+      | cAnd a a1, cAnd b b1 => \Sigma (FormulaCode a b) (FormulaCode a1 b1)
+      | forAllH a, forAllH b => FormulaCode a b
+      | cExists a, cExists b => FormulaCode a b
+      | _, _ => Empty
 
-  \func formulaCode-encode {_ : Language} {c : Context} {a b : Formula c} (p : a = b) : FormulaCode a b
+    \func formulaCode-encode {_ : Language} {c : Context} {a b : Formula c} (p : a = b) : FormulaCode a b
     \elim a, b, p
       | equal a b, _, idp => (idp, idp)
       | atomic r terms, _, idp => (idp, idp)
@@ -35,7 +35,7 @@
       | forAllH a1, _, idp => formulaCode-encode idp
       | cExists a, _, idp => formulaCode-encode idp
 
-  \func formulaCode-decode {_ : Language} {c : Context} {a b : Formula c} (code : FormulaCode a b) : a = b
+    \func formulaCode-decode {_ : Language} {c : Context} {a b : Formula c} (code : FormulaCode a b) : a = b
     \elim a, b, code
       | equal a b1, equal a1 b, (p,p1) => pmap2 equal p p1
       | atomic r terms, atomic _ terms1, (idp,p1) => pmap (atomic r) (convertArrayEquality p1)
@@ -45,7 +45,7 @@
       | forAllH a, forAllH b, code => pmap forAllH $ formulaCode-decode code
       | cExists a, cExists b, code => pmap cExists $ formulaCode-decode code
 
-  \func formulaCode-decide {L : DecLanguage} {c : Context} (a b : Formula c) : Dec (FormulaCode a b)
+    \func formulaCode-decide {L : DecLanguage} {c : Context} (a b : Formula c) : Dec (FormulaCode a b)
     \elim a, b
       | equal a b, equal a1 b1 => \case TermCodeDec.decideEq a a1, TermCodeDec.decideEq b b1 \with {
         | yes e, yes e1 => yes (e, e1)

src/proof/PrfFinite.ard

@@ -1,6 +1,7 @@
 \import Function.Meta
 \import Logic
 \import Paths
+\import Paths.Meta
 \import Set
 \import Set.Fin
 \import Set.Subset
@@ -9,12 +10,19 @@
 \import proof.PrfWeaken
 \import proof.Proof
 \import syntax.Context
+\import syntax.Free
+\import syntax.Lift
 \import syntax.Substitution
 \import syntax.Syntax
 \import util.SetUtil
 
 \func prfFinite {_ : DecLanguage} {c : Context} {axioms : Theory c} {toShow : Formula c}
-                (prf : Prf axioms toShow) : \Sigma (axioms' : Theory c) (axioms' ⊆ axioms) (FinSet (Elements axioms')) (Prf axioms' toShow)
+                (prf : Prf axioms toShow) :
+  \Sigma
+    (axioms' : Theory c)
+    (axioms' ⊆ axioms)
+    (FinSet (Elements axioms'))
+    (Prf axioms' toShow)
 \elim prf
   | AXM e => (single toShow, SubsetHelper.subsetSingle e, FinSets.FinSingle, AXM idp)
   | contra f prf1 prf2 =>
@@ -163,3 +171,27 @@
     \let
       | h => prfFinite prf
     \in (h.1, h.2, h.3, cAndElim2 h.4 p)
+  | forAllIntro f prf p =>
+    \let
+      | h => prfFinite prf
+      | h3 : FinSet (Elements h.1) => h.3
+      --       | ourSet : Set (Formula c) => mapSet' h.1 (liftFormula 1)
+      | zeroNotFreeInH1 : 0 ∉ {Fin (suc c)} freeVars h.1 => \case \elim __ \with {
+        | inP (f, e, free) => \case h.2 e \with {
+          | inP (f', e', p') => notFreeInLift $ rewriteI p' $ free
+        }
+      }
+      | ourSet : Set (Formula c) => mapSet h.1 (\lam x xe => liftFormula.unliftFormula1 x (\lam free => zeroNotFreeInH1 (inP (x, xe, free))))
+    \in (
+      ourSet,
+    --       \lam e => \case h.2 e \with {
+    --         | inP (x', e', p') => \let z => liftFormula.unliftPath 1 p' \in rewrite z e'
+    --       },
+      \lam {x} => \case \elim x, \elim __ \with {
+        | _, inP (f, e, idp) => \case h.2 {f} e \with {
+          | inP (f', e', p') => \let p'' => p' \in {?}
+        }
+      },
+      {?},
+      forAllIntro f {?} p
+    )

src/semantics/Interpretation.ard

@@ -145,9 +145,9 @@
         \func lifted {_ : Language} {c : Context} {I : Interpretation c} {f : Formula c}
                      {u : I.structure.Universe}
                      (m : I ⊧ f) (dummy : Term c)
-          : extend I u ⊧ liftFormula {_} {1} f => fromSub.substitutionLemma->
+          : extend I u ⊧ liftFormula 1 f => fromSub.substitutionLemma->
             {_}
-            {suc c} {c} {liftFormula {_} {1} f}
+            {suc c} {c} {liftFormula 1 f}
             I {extend I u} {reverseLift.reverse1S dummy}
             (\lam v free => \case \elim v, \elim free \with {
               | 0, free => absurd $ notFreeInLift free

src/syntax/Free.ard

@@ -1,13 +1,13 @@
 \import Data.Fin
-\import Function.Meta
 \import Logic
 \import Logic.Meta
 \import Meta
+\import Set.Subset
 \import syntax.Context
 \import syntax.Lift
 \import syntax.Substitution
 \import syntax.Syntax
-\import util.NatUtil
+\import util.SetUtil
 
 \func FreeinTerm {_ : Language} {c : Context} (t : Term c) (v : Context.variable c) : \Prop
 \elim t
@@ -57,8 +57,18 @@
     }) h
 
 \func notFreeInLift {_ : Language} {c : Context} {f : Formula c}
-                      (h : FreeInFormula (liftFormula {_} {1} f) 0)
+                      (h : FreeInFormula (liftFormula 1 f) 0)
   : Empty
   => notFreeInRename
       (\lam v' (p : 0 = {Fin (suc c)} suc v') => usingOnly p contradiction)
-      h
+      h
+
+\func freeVarsFormula {_ : Language} {c : Context} (f : Formula c) : Set (Context.variable c)
+  => \lam v => FreeInFormula f v
+
+\func freeVars {_ : Language} {c : Context} (T : Theory c) : Set (Context.variable c)
+  => \lam v => ∃ (f : Formula c) (f ∈ T) (FreeInFormula f v)
+
+
+\func RenameFreeTerm {_ : Language} (c c' : Context) (t : Term c) => \Pi (v : Context.variable c) (FreeinTerm t v) -> Context.variable c'
+\func RenameFree {_ : Language} (c c' : Context) (f : Formula c) => \Pi (v : Context.variable c) (FreeInFormula f v) -> Context.variable c'

src/syntax/Lift.ard

@@ -1,9 +1,11 @@
 \import Data.Fin
 \import Function.Meta
+\import Logic
 \import Meta
 \import Paths
 \import Paths.Meta
 \import syntax.Context
+\import syntax.Free
 \import syntax.Substitution
 \import syntax.SubstitutionReverse
 \import syntax.Syntax
@@ -25,6 +27,11 @@
     \elim delta
       | 0 => idp
       | suc delta => pmap suc isActuallyJustAddition
+
+    \func unliftFinPath {delta n : Nat} {i j : Fin n} (p : liftFin i = {Fin (delta + n)} liftFin j) : i = j
+    \elim delta
+      | 0 => p
+      | suc delta => \let p' => unfsuc p \in unliftFinPath p'
   }
 
 \func liftTerm {_ : Language} {delta c : Context} (t : Term c) : Term (delta + c) =>
@@ -40,17 +47,29 @@
       unfold liftTerm Rename.renameTerm.compose
   }
 
-\func liftFormula {_ : Language} {delta c : Context} (f : Formula c) : Formula (delta + c) =>
+\func liftFormula {_ : Language} (delta : Context) {c : Context} (f : Formula c) : Formula (delta + c) =>
   Rename.rename f (\lam v => liftFin v)
   \where {
     \private \func example {_ : Language} :
-      liftFormula {_} {2} (forAllH $ forAllH (equal #0 #1)) = {Formula 5}
+      liftFormula 2 (forAllH $ forAllH (equal #0 #1)) = {Formula 5}
       (forAllH $ forAllH $ equal #0 #1) => idp
+
+    \func unliftFormula1 {_ : Language} {c : Context}
+                        (f : Formula (suc c))
+                        (h : Not (FreeInFormula f 0))
+      : Formula c
+      => Rename.renameFree f (\lam (v : Fin (suc c)) free => \case \elim v, \elim free \with {
+        | 0, free => absurd $ h free
+        | suc v, _ => v
+      })
+
+    \func unliftPath {_ : Language} (delta : Context) {c : Context} {f f' : Formula c} (p : liftFormula delta f = liftFormula delta f')
+      : f = f' => Rename.unrename liftFin.unliftFinPath p
   }
 
 \func reverseLift {_ : Language} {c : Context} {f : Formula c} (dummy : Term c)
-  : Substitution.substitute (liftFormula {_} {1} f) (reverse1S dummy) = f =>
-  reverseRename (\lam v => liftFin {1} v) (reverse1S dummy) (\lam t => reverseTerm)
+  : Substitution.substitute (liftFormula 1 f) (reverse1S dummy) = f =>
+  reverseRename (\lam v => liftFin {1} v) (reverse1S dummy) (\lam _ => reverseTerm)
   \where {
     \func reverse1S {_ : Language} {c : Context} (dummy : Term c) : Substitution (suc c) c =>
       \lam v => \case \elim v \with {
@@ -65,7 +84,7 @@
       | apply f args => pmap (apply f) (ext $ ext (\lam j => reverseTerm {_} {c} {args j}))
   }
 
-\func liftTheory {_ : Language} {delta c : Context} (T : Theory c) : Theory (delta + c) => mapSet T liftFormula
+\func liftTheory {_ : Language} {delta c : Context} (T : Theory c) : Theory (delta + c) => mapSet T (\lam f _ => liftFormula delta f)
 
 \func subsituteLiftTerm1S {_ : Language} {c c' : Context} {t : Term c} {s : Substitution (suc c) c'}
   : Substitution.substituteTerm (liftTerm {_} {1} t) s = Substitution.substituteTerm t (\lam v => s (fsuc v))

src/syntax/Substitution.ard

@@ -1,12 +1,18 @@
 \import Data.Fin
 \import Function
 \import Function.Meta
+\import Logic
+\import Logic.Meta
 \import Meta
 \import Paths
 \import Paths.Meta
+\import decidable.FormulaCode
+\import decidable.TermCode
 \import syntax.Context
+\import syntax.Free
 \import syntax.Lift
 \import syntax.Syntax
+\import util.ArrayUtil
 \open Context
 \open Nat (+)
 
@@ -52,6 +58,11 @@
           | apply f args => pmap (apply f) $ ext $ ext (\lam j => compose {_} {c} {c'} {c''} {args j})
       }
 
+    \func renameTermFree {_ : Language} {c c' : Context} (t : Term c) (remap : RenameFreeTerm c c' t) : Term c'
+      \elim t
+        | var v => var $ remap v idp
+        | apply f args => apply f (\lam i => renameTermFree (args i) (\lam v free => remap v (inP (i, free))))
+
     \func rename {_ : Language} {c c' : Context} (f : Formula c) (r : Rename c c') : Formula c'
     \elim f
       | equal a b => equal (renameTerm a r) (renameTerm b r)
@@ -61,6 +72,79 @@
       | cAnd a b => cAnd (rename a r) (rename b r)
       | forAllH f => forAllH $ rename f (Extend.extend r)
       | cExists f => cExists $ rename f (Extend.extend r)
+
+    -- same as above but we additionally guarantee r is only applied on the free vars
+    \func renameFree {_ : Language} {c c' : Context} (f : Formula c) (r : RenameFree c c' f) : Formula c'
+      \elim f
+        | equal a b => equal (renameTermFree a (\lam v free => r v (byLeft free))) (renameTermFree b (\lam v free => r v (byRight free)))
+        | atomic rel terms => atomic rel $ \lam i => renameTermFree (terms i) {?}
+        | notH f => notH $ renameFree f r
+        | impH antecedent consequent => impH (renameFree antecedent r) (renameFree consequent r)
+        | cAnd a b => cAnd (renameFree a r) (renameFree b r)
+        | forAllH f => forAllH $ renameFree f (Extend.extend r)
+        | cExists f => cExists $ renameFree f (Extend.extend r)
+
+    \func unrenameTerm {_ : Language} {c c' : Context} {t t' : Term c} {r : Rename c c'}
+                       (rInj : \Pi {v v' : variable c} (r v = r v') -> v = v')
+                       (p : renameTerm t r = renameTerm t' r) : t = t'
+    \elim t, t', p
+      | var v, var v1, p => \let p' => TermCodeDec.termCode-encode p \in pmap var $ rInj p'
+      | apply f args, apply f1 args1, p =>
+        \let
+          | (p1, p2) => TermCodeDec.termCode-encode p
+        \in \case \elim f1, \elim args1, p1, p2 \with {
+          | _, args1, idp, p2 => pmap
+              (apply f)
+              (ext $ ext (\lam j => \let p2' => convertArrayEquality p2 | p2Result => pmap (\lam (z : Array _ _) => z j) p2' \in unrenameTerm rInj p2Result))
+        }
+
+    \func unrename {_ : Language} {c c' : Context} {f f' : Formula c} {r : Rename c c'}
+                   (rInj : \Pi {v v' : variable c} (r v = r v') -> v = v')
+                   (p : rename f r = rename f' r) : f = f'
+    \elim f, f', p
+      | equal a b, equal a1 b1, p => \let (p1, p2) => FormulaCodeDec.formulaCode-encode p \in
+        pmap2 equal (unrenameTerm rInj p1) (unrenameTerm rInj p2)
+      | atomic r1 terms, atomic r2 terms1, p =>
+        \let
+          | (p1, p2) => FormulaCodeDec.formulaCode-encode p
+        \in \case \elim r2, \elim terms1, p1, p2 \with {
+          | _, _, idp, p2 => pmap
+              (atomic r1)
+              (ext $ ext (\lam j => \let p2' => convertArrayEquality p2 | p2Result => pmap (\lam (z : Array _ _) => z j) p2' \in unrenameTerm rInj p2Result))
+        }
+      | notH f, notH f', p =>
+        \let p' => FormulaCodeDec.formulaCode-decode $ FormulaCodeDec.formulaCode-encode p
+        \in pmap notH $ unrename rInj p'
+      | impH a f, impH a1 f', p =>
+        \let
+          | (p1, p2) => FormulaCodeDec.formulaCode-encode p
+          | p1' => FormulaCodeDec.formulaCode-decode p1
+          | p2' => FormulaCodeDec.formulaCode-decode p2
+        \in pmap2 impH (unrename rInj p1') (unrename rInj p2')
+      | cAnd a f, cAnd a1 f', p =>
+        \let
+          | (p1, p2) => FormulaCodeDec.formulaCode-encode p
+          | p1' => FormulaCodeDec.formulaCode-decode p1
+          | p2' => FormulaCodeDec.formulaCode-decode p2
+        \in pmap2 cAnd (unrename rInj p1') (unrename rInj p2')
+      | forAllH f, forAllH f', p =>
+        \let
+          | p' => FormulaCodeDec.formulaCode-decode $ FormulaCodeDec.formulaCode-encode p
+        \in pmap forAllH (unrename (\lam {v : variable (suc c)} {v' : variable (suc c)} p => \case \elim v, \elim v', \elim p \with {
+          | 0, 0, p => idp
+          | 0, suc f1, p => \let p : 0 = suc _ => p \in usingOnly p contradiction
+          | suc f1, 0, p => \let p : suc _ = 0 => p \in usingOnly p contradiction
+          | suc f1, suc f2, p => \let p' => unfsuc p \in pmap fsuc (rInj p')
+        }) p')
+      | cExists f, cExists f', p =>
+        \let
+          | p' => FormulaCodeDec.formulaCode-decode $ FormulaCodeDec.formulaCode-encode p
+        \in pmap cExists (unrename (\lam {v : variable (suc c)} {v' : variable (suc c)} p => \case \elim v, \elim v', \elim p \with {
+          | 0, 0, p => idp
+          | 0, suc f1, p => \let p : 0 = suc _ => p \in usingOnly p contradiction
+          | suc f1, 0, p => \let p : suc _ = 0 => p \in usingOnly p contradiction
+          | suc f1, suc f2, p => \let p' => unfsuc p \in pmap fsuc (rInj p')
+        }) p')
   }
 
 \func Substitution {_ : Language} (c c' : Context) => variable c -> Term c'
@@ -84,6 +168,7 @@
       }
 
     -- TODO: this proof seems very complicated. What is the general principle?
+
     \func distributeExtends {_ : Language} {c c' c'' : Context} {s : Substitution c c'} {s' : Substitution c' c''} :
       (\lam v => substituteTerm (Extend.extends s v) (Extend.extends s')) = {Substitution (suc c) (suc c'')}
       Extend.extends (\lam v => substituteTerm (s v) s') => ext (helper s s')
@@ -101,9 +186,9 @@
 
         \private \func helper2 {_ : Language} {c' c'' : Context} (t : Term c') (s' : Substitution c' c'') :
           substituteTerm (Rename.renameTerm t fsuc) (Extend.extends s') = Rename.renameTerm (substituteTerm t s') fsuc
-          \elim t
-            | var v => idp
-            | apply f args => pmap (apply f) (ext $ ext (\lam j => helper2 (args j) s'))
+        \elim t
+          | var v => idp
+          | apply f args => pmap (apply f) (ext $ ext (\lam j => helper2 (args j) s'))
       }
 
     \func substitute {_ : Language} {c c' : Context} (f : Formula c) (s : Substitution c c') : Formula c'