The Coq mailing list

[Asya Bergal <abergal AT mit.edu>]

It seems like you're looking for is known as a deep embedding of second-order logic in Coq. People are describing to you that you can use a shallow embedding inside of Coq instead, which is true but not useful to you (http://cstheory.stackexchange.com/questions/1370/shallow-versus-deep-embeddings).

I myself needed a deep-embedding of First Order logic for a former of project of mine, and failed to find an reasonable existing one. I've attached the very minimal formalization that I produced in case it's useful to you.

Good luck!

On Wed, Mar 22, 2017 at 10:21 PM, Caitlin McGregor <caitlin.mcgregor AT anu.edu.au> wrote:

Hi,

Ah I see where my lack of clarity is. Indeed, I do realise that Coq understands second order logic at its heart. I am working on proving meta-properties, in particular in correspondence theory. This shows certain correspondences between modal logic and first order logic, and in my case I go via second order logic.

Perhaps examples will help. Here is what I have already for the fragment of second order logic that I am working with:

(* Countably many unary predicates *)

Inductive predicate : Type :=

  Pred (n:nat) : predicate.

(* Countable many first order variables *)

Inductive FOvariable : Type :=

  Var (n:nat) : FOvariable.

(* The fragment of second order logic that I'm working with *)

Inductive SecOrder :=

    predSO : predicate -> FOvariable -> SecOrder

  | eqFO : FOvariable -> FOvariable -> SecOrder

  | allFO : FOvariable -> SecOrder -> SecOrder

  | exFO : FOvariable -> SecOrder -> SecOrder

  | negSO : SecOrder -> SecOrder 

  | conjSO : SecOrder -> SecOrder -> SecOrder 

  | disjSO : SecOrder -> SecOrder -> SecOrder 

  | implSO : SecOrder -> SecOrder -> SecOrder 

  | allSO : predicate -> SecOrder -> SecOrder

  | exSO : predicate -> SecOrder -> SecOrder.

 

Then, I define a satisfaction relation, SOturnst:

(* Iv = interpretation of FOvariables; 

   Ip = interpretation of unary predicates *)

Fixpoint SOturnst (D:Set) (Iv: FOvariable -> D) (Ip: predicate -> D -> Prop)  (alpha:SecOrder) : Prop :=

  match alpha with

    predSO (Pred n) (Var m) => (Ip (Pred n) (Iv (Var m)))

  | eqFO (Var n) (Var m) => (Iv (Var n)) = (Iv (Var m))

  | allFO (Var n) beta => forall d:D, SOturnst D (altered_Iv D Iv d (Var n)) Ip Ir beta

  | exFO (Var n) beta => (exists d:D, SOturnst D (altered_Iv D Iv d (Var n)) Ip Ir beta)

  | negSO beta => ~ SOturnst D Iv Ip Ir beta

  | conjSO beta_1 beta_2 => (SOturnst D Iv Ip Ir beta_1) /\ (SOturnst D Iv Ip Ir beta_2)

  | disjSO beta_1 beta_2 => (SOturnst D Iv Ip Ir beta_1) \/ (SOturnst D Iv Ip Ir beta_2)

  | implSO beta_1 beta_2 => (SOturnst D Iv Ip Ir beta_1) -> (SOturnst D Iv Ip Ir beta_2)

  | allSO (Pred n) beta => forall (pred_asgmt: D -> Prop), 

                               SOturnst D Iv (altered_Ip D Ip pred_asgmt (Pred n)) Ir beta

  | exSO (Pred n) beta => (exists (pred_asgmt: D -> Prop), 

                              (SOturnst D Iv (altered_Ip D Ip pred_asgmt (Pred n)) Ir beta))

  end.

 

(This definition uses two functions that I didn't give definitions to, but it's not important for our purposes.)

Then a small example of what I might want to be able to use might be:

Lemma lem : forall (D : Set) (Iv : FOvariable -> D) (Ip : predicate -> D -> Prop) (alpha : SecOrder) (P : predicate),

SOturnst D Iv Ip (allSO P (allSO P alpha)) ->

SOturnst D Iv Ip (allSO P alpha).

But ideally I don't want to have to prove things like this, if there so happens to be a library that does it for me. It's okay if there isn't; was just wondering if someone had already done something like this.

Is there any other information that would help you answer the questions? Thanks for your help.

Kind regards,
Caitlin

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Pierre Courtieu <pierre.courtieu AT gmail.com>
Sent: Thursday, 23 March 2017 11:41:52 AM
To: Coq Club

Subject: Re: [Coq-Club] Second order logic library?

 

Hi,
Adam means that Coq itself understand second order logic at its heart.
You don't need to develop a library for that, you can just formalize
your problems directly,

For example: "forall (R:nat ->nat -> Prop), forall n, R n n \/ R n 0"
is a formula that coq understands perfectly (although it is not
provable).

The typical situation where you need to formalize formulas by a
concrete type is if you want to prove meta-properties about second
order formulas themselves (like correctness or completeness of some
proof system).

Maybe a more precise description of the problems you want to formalise
and the kind of theorems you would like to prove about them would
help.

Best regards,
Pierre

2017-03-23 1:21 GMT+01:00 Caitlin McGregor <caitlin.mcgregor AT anu.edu.au>:
> Thanks for your response. (Apologies for the first order part of the
> question - that was silly!)
>
>
> The context is that if I wish to formalise some problem that involves second
> order formulas, I would like a library that defines such a type and proves a
> collection of lemmas that are in some sense "obvious" to the mathematician
> and require no explanation.
>
>
> One idea is to define the type myself and then define functions between my
> own second order formulas and some set theoretic notions, and then prove
> inside set theory. But I was wondering if there was a library that was
> explicitly working with second order formulas.
>
>
> Please bear with any misunderstandings that I have. Any help that you could
> provide would be greatly appreciated.
>
>
> Kind regards,
> Caitlin
>
>
> ________________________________
> From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of
> Adam Chlipala <adamc AT csail.mit.edu>
> Sent: Thursday, 23 March 2017 11:06:44 AM
> To: coq-club AT inria.fr
> Subject: Re: [Coq-Club] Second order logic library?
>
> What exactly would be in such a library, considering that, in a reasonable
> sense, second-order logic is a subset of Coq's full logic?
>
> On 03/22/2017 08:03 PM, Caitlin McGregor wrote:
>
> Hi all,
>
>
> I am looking for a second order logic library in Coq, or even a first order
> library. Does anyone know if these are available?
>
>
> Thanks in advance,
>
> Caitlin
>
>

Set Implicit Arguments.
Unset Strict Implicit.

Require Import Coq.Lists.List.
Import ListNotations.

Section Hlist.
  (* Heterogenous list type. *)
  Inductive hlist A (f : A -> Type) : list A -> Type :=
  | hnil : hlist f []
  | hcons : forall x l, f x -> hlist f l -> hlist f (x :: l).

  Definition hmap A (f : A -> Type) B (g : B -> Type)
             (F : A -> B) (F' : forall a, f a -> g (F a))
             (l : list A) (h : hlist f l) : hlist g (map F l).
    induction h; constructor; auto.
  Defined.

  Definition hmap' A (f : A -> Type) (g : A -> Type)
             (F' : forall a, f a -> g a)
             (l : list A) (h : hlist f l) : hlist g l.
    replace l with (map id l).
    apply hmap with (f := f); assumption.
    clear f g F' h.
    induction l as [| x xs IHl]; [| simpl; rewrite IHl]; reflexivity.
  Defined.
End Hlist.

Notation " h[] " := (hnil _).
Infix "h::" := hcons (at level 60, right associativity).

Section FirstOrder.

  Context (sort : Type)
          (func : list sort -> sort -> Type)
          (predicate : list sort -> Type).

  Inductive term : sort -> Type :=
    App : forall {dom cod},
            (func dom cod) -> hlist term dom -> term cod.

  Definition term_terms_rect
             (P : forall s, term s -> Type)
             (Q : forall ss, hlist term ss -> Type)
             (c_app : forall {dom} {cod} (f : func dom cod)
                             (ts : hlist term dom),
                        Q dom ts -> P cod (App f ts))
             (c_nil : Q [] h[])
             (c_cons : forall {s} (t : term s) {ss} (ts : hlist term ss),
                         P s t -> Q ss ts -> Q (s :: ss) (t h:: ts)) :
    forall {s} (t : term s), P s t :=
    fix F {s} (t : term s) : P s t :=
    match t with
      | App f ts =>
        c_app f ts
              ((fix G {ss} (ts : hlist term ss) : Q ss ts :=
                  match ts with
                    | h[] => c_nil
                    | t h:: ts => c_cons t ts (F t) (G ts)
                  end) _ ts)
    end.

  Record model :=
    Model
      {domain :> sort -> Type;
       interp_func : forall dom cod,
                       func dom cod ->
                       hlist domain dom ->
                       domain cod;
       interp_predicate : forall dom,
                            predicate dom ->
                            hlist domain dom -> Prop}.

  Definition interp_term (m : model) s (t : term s) : m s.
    apply term_terms_rect with
    (P := (fun s t => m s))
      (Q := fun ss ts => hlist m ss)
      (t := t); clear s t.
    - (* app *)
      intros dom cod f x IHts.
      apply (interp_func f); assumption.
    - (* nil *)
      constructor.
    - (* cons *)
      constructor; assumption.
  Defined.

  Definition interp_terms (m : model) ss (ts : hlist term ss)
  : hlist m ss :=
    hmap' (interp_term _) ts.

  Section formulas.

    Variable d : sort -> Type.

    Inductive formula : Type :=
    | Predicate : forall ss, predicate ss -> hlist term ss -> formula
    | And : formula -> formula -> formula
    | Or : formula -> formula -> formula
    | Not : formula -> formula
    | Forall : forall s, (d s -> formula) -> formula
    | Exists : forall s, (d s -> formula) -> formula
    | FTrue : formula
    | FFalse : formula.

  End formulas.

  Arguments FTrue {d}.
  Arguments FFalse {d}.

  Definition Formula := forall d : sort -> Type, formula d.

  Fixpoint interp_formula (m : model) (f : formula m) : Prop :=
    match f with
      | Predicate _ p ts => interp_predicate p (interp_terms m ts)
      | And f1 f2 => interp_formula f1 /\ interp_formula f2
      | Or f1 f2 => interp_formula f1 \/ interp_formula f2
      | Not f => ~interp_formula f
      | @Forall _ s f => forall x : m s, interp_formula (f x)
      | @Exists _ s f => exists x : m s, interp_formula (f x)
      | FTrue => True
      | FFalse => False
    end.

  Definition interp_Formula (m : model) (f : Formula) :=
    interp_formula (f m).

End FirstOrder.