[Coq-Club] Trying to define constant of some inductive type in Coq

[Alex Meyer]

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 of https://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

[Loading Image...

How to declare constant of some inductive type in Coq?<https://stackoverflow.com/questions/51254034/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...

[Carlos Olarte]

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.

Post by Alex Meyer
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).
cte(John)
Cte(John) := fun _ => cte(John)
cl_cte: forall C, closedT(fun _ => cte(C)) - where can I put John here?
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...