\import Function.Meta
\import Logic
\import Logic.FirstOrder.Algebraic
\import Logic.FirstOrder.Term
\import Logic.Meta
\import Paths
\import Paths.Meta
\import Set.Fin

\instance FreeStructure.{u} {T : Theory.{u,u,u}} (X : T -> \Set u) : Structure T \cowith
  | E => QTerm X
  | operation h args => qapply h args
  | relation P args => ∃ (args' : DArray (\lam i => Term X (predDomain P i)))
    (IsTheorem nil (predicate P args'))
    (\Pi (i : Fin (predDomain P).len) -> qinj (args' i) = args i)
  \where {
    \open Theory

    \truncated \data QTerm.{u} {T : Theory.{u,u,u}} (V : T -> \Set u) (s : T) : \Set
      | qinj (Term V s)
      | qapply (f : Symb s) (DArray (\lam j => QTerm V (domain f j)))
      | qquot {t t' : Term V s} (IsTheorem nil (equality t t')) : qinj t = qinj t'
      | qmerge {f : Symb s} (ds : DArray (\lam j => Term V (domain f j))) : qinj (apply f ds) = qapply f (\new DArray { | at j => qinj (ds j) })

    \func qinj-surj.{u} {T : Theory.{u,u,u}} {V : T -> \Set u} {s : T} (q : QTerm V s) : ∃ (t : Term V s) (qinj t = q) \elim q
      | qinj t => inP (t, idp)
      | qapply f d => TruncP.map (FinSet.choice (\lam j => qinj-surj (d j)))
        \lam g => (apply f (\lam j => (g j).), path (qmerge _) *> pmap (\lam x => qapply f (\new DArray (\lam j => QTerm V (domain f j)) x)) (ext \lam j => (g j).))

    \lemma qinj-equality.{u} {T : Theory.{u,u,u}} {V : T -> \Set u} {s : T} {t t' : Term V s} : (qinj t = qinj t') <-> IsTheorem nil (equality t t')
      => (transport (code t) __ (refl idp), \lam p => path (qquot p))
      \where {
        \func code.{u} {T : Theory.{u,u,u}} {V : T -> \Set u} {s : T} (t : Term V s) (q : QTerm V s) : \Prop \elim q
          | qinj t' => IsTheorem nil (equality t t')
          | qapply f d => \Pi (d' : DArray (\lam j => Term V (domain f j))) -> (\Pi (j : Fin (DArray.len {domain f})) -> code (d' j) (d j)) -> IsTheorem nil (equality t (apply f d'))
          | qquot {t1} {t2} p => ext (transitivity __ p, transitivity __ (symmetry p))
          | qmerge {f} ds => ext (\lam t~fds ds' ds'~ds => transitivity t~fds (symmetry (congruence ds'~ds)), \lam g => g ds (\lam j => refl idp))
      }

    \lemma interpret=subst.{u} {T : Theory.{u,u,u}} {X V : T -> \Set u} {rho : \Pi {s : T} -> V s -> Term X s} {s : T} (t : Term V s)
      : (FreeStructure X).interpret (\lam v => qinj (rho v)) t = qinj (subst t rho) \elim t
      | var v => idp
      | apply f d => pmap (qapply f) (exts \lam j => interpret=subst (d j)) *> inv (path (qmerge _))

    \lemma interpretF=substF.{u} {T : Theory.{u,u,u}} {X V : T -> \Set u} (rho : \Pi {s : T} -> V s -> Term X s) (phi : Formula V)
      : (FreeStructure X).IsFormulaTrue (\lam v => qinj (rho v)) phi <-> IsTheorem nil (substF phi (\lam v => rho v)) \elim phi
      | equality t t' => <->trans (<->_=. $ pmap2 (=) (interpret=subst t) (interpret=subst t')) qinj-equality
      | predicate P d => (\lam (inP (d',q,e)) => congruenceP (\lam j => qinj-equality. (e j *> interpret=subst (d j))) q,
                          \lam q => inP (\new DArray { | at j => subst (d j) (\lam {s} => rho) }, q, \lam i => inv (interpret=subst (d i))))

    \func qinterpret.{u} {T : Theory.{u,u,u}} {M : Model T} {V : T -> \Set u} (rho : \Pi {s : T} -> V s -> M s) {s : T} (t : QTerm V s) : M s \elim t
      | qinj t => M.interpret rho t
      | qapply f d => operation f (\lam j => qinterpret rho (d j))
      | qquot p => M.theoremIsTrue p rho (\case __)
      | qmerge {f} ds _ => operation f (\new DArray _ (\lam j => M.interpret rho (ds j)))

    \func qinterpret0.{u} {T : Theory.{u,u,u}} {M : Model T} {s : T} (t : QTerm (\lam _ => Empty) s) : M s
      => qinterpret (\lam {_} => absurd) t
  }

\instance FreeModel.{u} {T : Theory.{u,u,u}} (X : T -> \Set u) : Model T
  | Structure => FreeStructure X
  | isModel S ax rho phiT =>
    \let | (inP (tau',p)) => S..liftDepSurj (\lam {v} => FreeStructure.qinj-surj {_} {X} {v.}) (\lam v => rho v.)
         | tau {s'} v => tau' (s',v)
         | eq : \Pi (phi : Formula {T} S.) -> Structure.IsFormulaTrue rho phi <-> T.IsTheorem nil (substF phi tau)
         => rewrite (path (\lam i {s'} v => inv (p (s',v)) i)) (FreeStructure.interpretF=substF tau)
    \in (eq S.). $ Theory.axiom S ax tau (\lam j => (eq (S. j)). (phiT j)) idp