An attempt to define the syntax and semantics of a predicate logic language, with a theorem on conservativity of structure extension. It's a failed attempt, therefore it contains "challenges". If somebody knows how to resolve them -- please let me know"

firstorder.v

(*
Compile to PDF with
coqc firstorder.v ; coqdoc --latex --no-lib-name -s -p "\usepackage{parskip}\renewcommand{\thesection}{\arabic{section}}" firstorder.v ; pdflatex firstorder.tex
*)
Require Import Coq.Strings.String.
Require Import Coq.Vectors.VectorDef.
Require Import Coq.Relations.Relation_Definitions.

Module firstorder.

(**
In this module, I define the syntax and semantics of a simple language of predicate logic. When it
comes to the definition of an interesting "conservativity" theorem (if a structure satisfies a
formula, then all extensions also satisfy it) I run into problems: (1) My ideal version of the
theorem does not type check, therefore I have to resort to a version which is unnecessarily strong,
because it has to assume that the structure and its extension have the same signature for using this
equality in a cast (this rules out all interesting cases, the proper extensions), and (2) I cannot
even prove that version correct.

In the following, I provide all the definitions and in between put some clearly marked challenge
descriptions. There are the two main challenges described above and three more, minor challenges
which are not that important to me, but I'd still be interested in their solution.

I hope that somebody can help me out here, and that the insights gained also help others!

-- Dominic
*)

Section firstorder_syntax.
  Inductive id : Set :=
    | Id : string -> id.
  
  Structure signature : Set := makesig {
    funsymbs : list id ;
    arity  : id -> nat ;
  }.

  Inductive term (sig : signature) : Type :=
    | TVar    : id -> term sig
    | TFunApp : forall f, List.In f (funsymbs sig) -> t (term sig) (arity sig f) -> term sig
  .

  Inductive formula (sig : signature) : Set :=
    | FTrue : formula sig
    | FFalse : formula sig
    | FEq : term sig -> term sig -> formula sig
    | FLe : term sig -> term sig -> formula sig
    | FAnd : formula sig -> formula sig -> formula sig
    | FOr : formula sig -> formula sig -> formula sig
    | FImp : formula sig -> formula sig -> formula sig
    | FNot : formula sig -> formula sig.
End firstorder_syntax.

Section firstorder_semantics.
  Definition function (n : nat) : Set := t nat n -> nat.

  Structure structure : Set := mkStruct {
    sig            : signature ;
    interpretation : forall f, List.In f (funsymbs sig) -> function (arity sig f) ;
  }.
  
  Definition isVar (sig : signature) (t : term sig) : Prop :=
    match t with
    | TVar _ _ => True
    | _ => False
    end.
  
  Definition var_assgn' (sig : signature) := forall (t : term sig), isVar sig t -> nat : Type.
  
  (**
    * CHALLENGE
    
    Variable assignment is, as a matter of fact, independent of the signature. Still, the signature
    occurrs as a type in the definition of [isVar] and [var_assgn']. We can also not create a term
    realizing the following "casting function":
    
    [Definition castVarAssgn (S S' : signature) (v : var_assgn' S) : var_assgn' S'.]
    
    since this leads to the goal
    %\begin{verbatim}
    1 subgoal
    S, S' : signature
    v : forall t : term S, isVar S t -> nat
    ______________________________________(1/1)
    forall t : term S', isVar S' t -> nat
    \end{verbatim}%
    
    which we only could solve by adding an equation [S = S'], but this doesn't help if we later on
    want to prove a lemma about structure extendsion. So, here's the challenge: Can you find a definition
    of [var_assgn'] which does _not_ depend on the signature?
    
    For now, we resort to a simpler version which just maps identifiers to variables.
  *)
  
  Definition var_assgn : Set := id -> nat.

  Fixpoint teval (K : structure) (assgn : var_assgn) (t : (term (sig K))): nat :=
    let S := sig K in
    match t with
    | TVar _ id => assgn id
    | TFunApp _ f HinSig args =>
        (interpretation K f HinSig) (map (fun arg => teval K assgn arg) args)
    end.

  Reserved Notation "'[(' K , asgn ')]' '|=' f" (at level 40).

  Inductive feval (K : structure) (assgn : var_assgn) : formula (sig K) -> Prop :=
    | fevalTrue : [(K, assgn)] |= FTrue (sig K)
    | fevalEq : forall t1 t2, (teval K assgn t1) = (teval K assgn t2) -> [(K, assgn)] |= (FEq (sig K) t1 t2)
    | fevalLe : forall t1 t2, (teval K assgn t1) <= (teval K assgn t2) -> [(K, assgn)] |= (FLe (sig K) t1 t2)
    | fevalFAnd : forall f1 f2, [(K, assgn)] |= f1 /\ [(K, assgn)] |= f2 -> [(K, assgn)] |= (FAnd (sig K) f1 f2)
    | fevalFOr : forall f1 f2, [(K, assgn)] |= f1 \/ [(K, assgn)] |= f2 -> [(K, assgn)] |= (FOr (sig K) f1 f2)
    | fevalFImp : forall f1 f2, [(K, assgn)] |= (FNot (sig K) f1) \/ [(K, assgn)] |= f2 -> [(K, assgn)] |= (FImp (sig K) f1 f2)
    where "'[(' K , asgn ')]' '|=' f" := (feval K asgn f).

  Axiom fevalFNot : forall K assgn f, ~ [(K, assgn)] |= f <-> [(K, assgn)] |= (FNot (sig K) f).
End firstorder_semantics.

Section properties.
  Definition extendsSig : relation signature :=
    fun (s1 s2 : signature) =>
      forall f, List.In f (funsymbs s1) ->
         List.In f (funsymbs s2)
      /\ (arity s1 f) = (arity s2 f).
  
  (* For extension of structures, we already need a cast function *)
  Definition cast {T : Type} {T1 T2 : T} (H : T1 = T2) (f : T -> Type) (x : f T1) : f T2 :=
    eq_rect T1 (fun T3 : T => f T3) x T2 H.
  
  Definition extendsStruct : relation structure :=
    fun (K K' : structure) =>
        extendsSig (sig K) (sig K')
      /\ forall f l (H1 : List.In f (funsymbs (sig K)))
                    (H2 : List.In f (funsymbs (sig K')))
                    (H3 : (arity (sig K) f) = (arity (sig K') f)),
           interpretation K f H1 l = interpretation K' f H2 (cast H3 (fun n => t nat n) l).
  
  (** 
     * (MINOR) CHALLENGE
     
     Create a definition of structure extension which does _not_ rely on a hypothesis such as H3,
     which depends on a fact that is always true in that case, but can be deduced from the fact that
     the signature of K' extends the one of K -- the arity of f cannot change!
  *)
End properties.

(** 
   * (MINOR) CHALLENGE
   
   I had to move that notation outside the above section to be able to access it in the
   next section. Why isn't it sufficient to declare it after feval? Why can I actually
   "override" it so easily? What would be the best way to declare that notation?
*)
Notation "'[(' K , asgn ')]' '|=' f" := (feval K asgn f) (at level 40) : feval_scope.

Section theorems.
  Local Open Scope feval_scope.
  
  (**
    * (1st MAIN) CHALLENGE
    
    For formalizing the "conservativity" of structure extension, I'd ideally like to
    have the following theorem:
    
    [[
    Theorem structureExtensionIsConservative :
      forall K K' assgn, let S := (sig K) in let S' := (sig K') in
        forall (t : formula S),
          extendsStruct K K' ->
            [(K, assgn)] |= t ->
              [(K', assgn)] |= t.
    ]]
    
    However, this (naturally) doesn't type check, with the error message:
    
    <<
    The term "t" has type "formula S" while it is expected to have type "formula (sig K')".
    >>
    
    Or course, this can again be "corrected" with a cast; however, the equation [S = S'] is
    too strong in general, since [S'] could be a proper extension! Here, I'm really lost;
    below you find the type checking version with the equality and cast:
  *)
  
  Theorem structureExtensionIsConservative :
    forall K K' assgn, let S := (sig K) in let S' := (sig K') in
      forall (f : formula S) (H : S = S'),
        extendsStruct K K' ->
          [(K, assgn)] |= f ->
            [(K', assgn)] |= (cast H (formula) f).
  Proof.
    intros K K' assgn S S' f H Hextends Hfeval.
    unfold cast. unfold eq_rect.
    generalize H.
    
(**
  * (2nd MAIN) CHALLENGE
  
  Here, I'd really want to do a [rewrite <- H]; that doesn't work though, since we have
  some dependent type mess going on here; the error message is
  <<The 3rd term has type "formula S'0" which should be coercible to "formula (sig K')">>.
  Makes sense probably... Another generalization [generalize t] can again "help", but then
  we don't have any information about the generalized term, and cannot prove the goal
  (although then we can eliminate the cast). So, here's the challenge: Somehow prove this!
  
  Below, I'll give an unsuccessful induction proof of the problem.
*)
  
  induction f.
  - rewrite -> H. intros. rewrite -> H0. constructor.
  - inversion Hfeval.
  - 
(**

  Applying [rewrite -> H.] fails in this case; error message:
  <<The 2nd term has type "term S" which should be coercible to "term S0".>>
*)
    
    induction t; induction t0.
    + rewrite -> H. intros H'. rewrite -> H'.
      constructor.
      inversion Hfeval.
      inversion H1.
      simpl.
      assumption.
    + 
(**

  Here, we cannot [rewrite -> H], again; the goal is
  
  %\begin{verbatim}
  forall H0 : S = S',
  [(K', assgn)]
  |= match H0 in (_ = y) return (formula y) with
     | eq_refl => FEq S (TVar S i) (TFunApp S f i0 t)
     end
  \end{verbatim}%
  
  I guess the problem is that here, we have a function application and it fails
  to type check for the premise that the symbol [f] is in the signature (since
  when replacing, it's suddenly a different signature...). So, what now? I also
  tried to remove that premise of TFunApp for which the type checking fails, but
  then the error is just a different one: The type [VectorDef.t (term S) (arity S f)]
  cannot be forced to the type [VectorDef.t (term S0) (arity S0 f)].
*)
  Abort.
End theorems.

Section examples.
  Section varAssignExample.
    (** A simple example for my first idea of a variable assignment (of terms). *)
    
    Variable S : signature.
    Definition X := TVar S (Id "X").
    
    Definition myVarAssgn (sig : signature) (t : term sig) : isVar sig t -> nat :=
      match t with
      | TVar _ id => fun _ => match id with
                              | Id "X" => 15
                              | _ => 0
                              end
      | TFunApp _ _ _ _  => fun pf : isVar sig (TFunApp _ _ _ _) => match pf with end
      end.
    
    Check myVarAssgn _ : var_assgn' _.

    Example ex1 : myVarAssgn S X I = 15. reflexivity. Qed.
  End varAssignExample.
End examples.

End firstorder.