The Coq mailing list

[Carlos Olarte <carlos.olarte AT gmail.com>]

Hi Alex, 
 I see some problems in your expressions. FC1 is used to build function 
symbols (in the first order signature) and A1 builds atomic propositions 
(predicate symbols). As Arthur wrote in your StackOverflow post, ClosedT is 
an inductively defined proposition saying that terms are closed (i.e., they 
cannot have free variables). You don't use it to build constants! 

Below a simple example on how to define John, the father of John (a function) 
and two predicates (Sleep and Think). In the bio-CTC project we implemented 
more automation that will complete Property1 below in one step. However, we 
haven't export all these tactics to the FOLL/LL repository... hope it will be 
done soon. 

Cheers,
Carlos.


Require Export LL.FLLMetaTheory.
Require Export Coq.Strings.String.

(* The whole LL formalization is parametric in the type of 
   the constants. Here an example using strings.
  isPositive is needed to define the polarity of the atomic propositions
  (needed for implementing a focused system for linear logic)
 *)
Module StringSet <: Eqset_dec_pol.
  Definition A := string.
  Definition eqA_dec := string_dec.
  Fixpoint isPositive (n:nat) :=
    match n with
    | 0%nat => false
    | 1%nat => true
    | S (S n) => isPositive n
    end.
End StringSet.

Module SLL := SqBasic StringSet.
Export SLL.

(* Predicate symbols are identified with natural numbers.  *)
Definition Sleep :nat := 1 .
Definition Think :nat:= 3 .

(* Similarly, function symbols are identified with a nat *)
Definition Father:nat := 1 .

Open Scope string_scope.
Definition John := "John"  .

(* These are atomic proposition --AProp -- *)
Definition JohnThinks : AProp := A1 Think (Cte John).

(* A more verbose one not using the constructor A1 *)
Definition JohnThinks' : forall T:Type, aprop T := fun _ => a1 Think (cte 
John).

Goal JohnThinks = JohnThinks'.
  reflexivity.
Qed.

Definition FatherJohnThinks :AProp := A1 Think (FC1 Father (Cte John)).
Definition FatherJohnSleeps :AProp := A1 Sleep (FC1 Father (Cte John)).

(* Proving closeness (of atomic propositions) is easy *)
Example close1: ClosedA FatherJohnThinks.
repeat constructor.
Qed.

Hint Unfold Sleep Think Father John FatherJohnSleeps.

(* Proving in Linear Logic that 
!(forall x(Think(x) -o Sleep(x))) , Think(Father(John)) |- Sleep(Father(John))
Since the system is one sided, the expression above becomes:
?exists x(Think(x) * Sleep(x)^) | Think(Father(John))^ | Sleep(Father(John))
 *)

(* This is the existential formula exists x(Think(x) * Sleep(x)^) *)
Definition Formula1 :Lexp := Ex (fun _ x => tensor (perp (a1 Think (var x) )) 
(atom (a1 Sleep (var x)))).

Example Property1:
|-F- [] ; []  ; UP [? Formula1 ; Atom FatherJohnThinks ; Perp 
FatherJohnSleeps].
Proof with solveF.
  NegPhase. (* Negative phase, storing the formulas in the context *)
  (* Positive phase, focusing on Formula1 *)
  eapply tri_dec2 with (F:=Formula1) ...
  eapply tri_ex with (t:=  (FC1 Father (Cte John))).
  eapply tri_tensor ...
  apply Init1 ...
  eapply tri_rel ...
  reflexivity.
  eapply tri_store ...
  (* Positive phase on Perp FatherJohnSleeps  *)
  eapply tri_dec1 with (F:= Perp FatherJohnSleeps )...
  autounfold;intro.
  inversion H ...
  apply A1InvN in H2;subst.
  simpl in H1.
  inversion H1.
  apply Init1 ...
Qed.






> On 11 Jul 2018, at 17:47, Alex Meyer 
> <alex153 AT outlook.lv>
>  wrote:
> 
> I am reading https://github.com/brunofx86/LL/blob/master/FOLL/LL/SyntaxLL.v 
> and 
> http://subsell.logic.at/bio-CTC/ and I am trying to declare in this 
> encoding of linear logic
> - constant "John"
> - function "thinks(John)"
> (I am trying to apply this framwork for the formal semantics of natural 
> language - e.g. in style 
> ofhttps://www.stergioschatzikyriakidis.com/research-outputs.html etc.), 
> that is why I am having such function).
> 
> I have arrived at the following expressions:
> cte(John)
> Cte(John) := fun _ => cte(John)
> but I don't know how to arrive at the final expression of type ClosedT:
> cl_cte: forall C, closedT(fun _ => cte(C)) - where can I put John here?
> 
> The same thing is with function:
> fc1(1, cte(John))
> FC1(1, Cte(John))
> FC1(1, fun _ => cte(John)) =
> = fun __ => fc1 (1, fun _ => cte(John))
> (note the difference between __ and _ - there is no rease to assume that 
> this is the same variable)
> but again - how to make the final step? forall is again used here and there 
> is no place for John and function number 1?
> 
> I am aware that 
> http://subsell.logic.at/bio-CTC/html/BioFLL.Definitions.html contains 
> Definition EncodeRule that is more complex example how the term of type 
> Closed is formed and therefore that can serve as greate example for my 
> question. Unfortunately, some custom defined syntax is involved here and at 
> present this is too hard example for me. As I skimmed through bio-CTC, then 
> there is not example of terms of type ClosedT or ClosedA, at least I did 
> not managed to find.
> 
> Very promising work, because formal semantics of natural language can have 
> many different logics and this framework could be great to encode many of 
> them, but is hard for novice.
> 
> De Amorim gave answer here 
> https://stackoverflow.com/questions/51254034/how-to-declare-constant-of-some-inductive-type-in-coq/
>  but it is not explicit and it says that several additional steps and 
> proofs are required.
> 
> Alex
> 
> How to declare constant of some inductive type in Coq?
> stackoverflow.com
> I am following 
> https://github.com/brunofx86/LL/blob/master/FOLL/LL/SyntaxLL.v and there 
> the inductive type is defined (parametrized Higher Order Abstract Syntax - 
> PHOAS is used here): (** Closed T...